0.7.12.31:
authorChristophe Rhodes <csr21@cam.ac.uk>
Sun, 9 Feb 2003 20:20:40 +0000 (20:20 +0000)
committerChristophe Rhodes <csr21@cam.ac.uk>
Sun, 9 Feb 2003 20:20:40 +0000 (20:20 +0000)
Yet another incremental extension to the type system algorithms.
In the presence of types such as (MEMBER 1 "foo" (X)), we
cannot hash VALUES-SPECIFIER-TYPE on EQUAL, because two
such types can contain the same or different (under EQL)
"foo" or (X), and yet be the same under EQUALity. So
... define a new function EQUAL-BUT-NO-CAR-RECURSION, which is
almost but not quite what it sounds (it tests strings
bit-vectors and lists by EQL, not EQUAL);
... use it as the new test function for the
VALUES-SPECIFIER-TYPE hash table.
The presence of numeric types in NOT types can be problematic,
as Paul Dietz' test of (OR BIGNUM FIXNUM) showed.  So
... work a lot harder in the NOT type translator, to bring
numeric types out: we treat (NOT (INTEGER a b)) as
(OR (NOT INTEGER) (INTEGER * a) (INTEGER b *)), with the
obvious generalizations.
Now (AND INTEGER (NOT FIXNUM)) parses as
`(OR (INTEGER * ,(1- MOST-NEGATIVE-FIXNUM))
                     (INTEGER ,(1+ MOST-POSITIVE-FIXNUM))
which is right, but no longer an intersection type, so
... move BIGNUM unparsing from INTERSECTION-TYPE to UNION-TYPE.
Even with all this, we don't get (OR INTEGER RATIO) right, so
... teach the type system some more set theory, with new
HAIRY-TYPE and INTERSECTION union methods.
Now (SUBTYPEP 'RATIONAL '(OR INTEGER RATIO)) returns T, T
(and all the people rejoiced!)

package-data-list.lisp-expr
src/code/early-extensions.lisp
src/code/early-type.lisp
src/code/late-type.lisp
tests/type.pure.lisp
version.lisp-expr

index 357908f..62f29db 100644 (file)
@@ -737,6 +737,7 @@ retained, possibly temporariliy, because it might be used internally."
             "COMPOUND-OBJECT-P"
              "SWAPPED-ARGS-FUN"
              "ANY/TYPE" "EVERY/TYPE"
+            "EQUAL-BUT-NO-CAR-RECURSION"
              "TYPE-BOUND-NUMBER"
              "CONSTANTLY-T" "CONSTANTLY-NIL" "CONSTANTLY-0"
              "PSXHASH"
index 5163fe1..58a2de9 100644 (file)
        (defun ,name (&rest args)
          (,cached-name args)))))
 
+;;; FIXME: maybe not the best place
+;;;
+;;; FIXME: think of a better name -- not only does this not have the
+;;; CAR recursion of EQUAL, it also doesn't have the special treatment
+;;; of pathnames, bit-vectors and strings.
+;;;
+;;; KLUDGE: This means that we will no longer cache specifiers of the
+;;; form '(INTEGER (0) 4).  This is probably not a disaster.
+;;;
+;;; A helper function for the type system, which is the main user of
+;;; these caches: we must be more conservative than EQUAL for some of
+;;; our equality tests, because MEMBER and friends refer to EQLity.
+;;; So:
+(defun equal-but-no-car-recursion (x y)
+  (cond
+    ((eql x y) t)
+    ((consp x)
+     (and (consp y)
+         (eql (car x) (car y))
+         (equal-but-no-car-recursion (cdr x) (cdr y))))
+    (t nil)))
 \f
 ;;;; package idioms
 
index 0af4281..4bb7c97 100644 (file)
                                 (logand (sxhash x) #x3FF))
               :hash-bits 10
               :init-wrapper !cold-init-forms)
-             ((orig equal))
+             ((orig equal-but-no-car-recursion))
   (let ((u (uncross orig)))
     (or (info :type :builtin u)
        (let ((spec (type-expand u)))
index 5d3b845..5da5929 100644 (file)
         (invoke-complex-subtypep-arg1-method type1 type2))
        (t
         ;; FIXME: This seems to rely on there only being 2 or 3
-        ;; HAIRY-TYPE values, and the exclusion of various
+        ;; NAMED-TYPE values, and the exclusion of various
         ;; possibilities above. It would be good to explain it and/or
         ;; rewrite it so that it's clearer.
         (values (not (eq type2 *empty-type*)) t))))
            nil)
        nil)))
        
+(!define-type-method (hairy :simple-union2) 
+                    (type1 type2)
+  (if (type= type1 type2)
+      type1
+      nil))
+
+(!define-type-method (hairy :complex-union2)
+                    (type1 type2)
+  (aver (hairy-type-p type2))
+  (let ((hairy-type-spec (type-specifier type2)))
+    (if (and (consp hairy-type-spec)
+            (eq (car hairy-type-spec) 'not))
+       (if (csubtypep (specifier-type (cadr hairy-type-spec)) type1)
+           *universal-type*
+           nil)
+       nil)))
+
 (!define-type-method (hairy :simple-=) (type1 type2)
   (if (equal (hairy-type-specifier type1)
             (hairy-type-specifier type2))
   ;; Check legality of arguments.
   (destructuring-bind (not typespec) whole
     (declare (ignore not))
-    (let ((spec (type-specifier (specifier-type typespec)))) ; must be legal typespec
-      (if (and (listp spec) (eq (car spec) 'not))
-         ;; canonicalize (not (not foo))
-         (specifier-type (cadr spec))
-         (make-hairy-type :specifier whole)))))
+    ;; must be legal typespec
+    (let* ((not-type (specifier-type typespec))
+          (spec (type-specifier not-type)))
+      (cond
+       ;; canonicalize (not (not foo))
+       ((and (listp spec) (eq (car spec) 'not))
+        (specifier-type (cadr spec)))
+       ((eq not-type *empty-type*) *universal-type*)
+       ((eq not-type *universal-type*) *empty-type*)
+       ((and (numeric-type-p not-type)
+             (null (numeric-type-low not-type))
+             (null (numeric-type-high not-type)))
+        (make-hairy-type :specifier whole))
+       ;; FIXME: this is insufficiently general.  We need to
+       ;; canonicalize over intersections and unions, too.  However,
+       ;; this will probably suffice to get BIGNUM right, and more
+       ;; code will be written when someone (probably Paul Dietz)
+       ;; comes up with a test case that demonstrates a failure,
+       ;; because right now I can't construct one.
+       ((numeric-type-p not-type)
+        (type-union
+         ;; FIXME: so much effort for parsing?  This seems overly
+         ;; compute-heavy.
+         (specifier-type `(not ,(type-specifier
+                                 (modified-numeric-type not-type
+                                                        :low nil
+                                                        :high nil))))
+         (cond
+           ((null (numeric-type-low not-type))
+            (modified-numeric-type
+             not-type
+             :low (let ((h (numeric-type-high not-type)))
+                    (if (consp h) h (list h)))
+             :high nil))
+           ((null (numeric-type-high not-type))
+            (modified-numeric-type
+             not-type
+             :low nil
+             :high (let ((l (numeric-type-low not-type)))
+                     (if (consp l) l (list l)))))
+           (t (type-union
+               (modified-numeric-type
+                not-type
+                :low nil
+                :high (let ((l (numeric-type-low not-type)))
+                        (if (consp l) l (list l))))
+               (modified-numeric-type
+                not-type
+                :low (let ((h (numeric-type-high not-type)))
+                       (if (consp h) h (list h)))
+                :high nil))))))
+       (t (make-hairy-type :specifier whole))))))
 
 (!def-type-translator satisfies (&whole whole fun)
   (declare (ignore fun))
 
 (!def-type-translator member (&rest members)
   (if members
-    (make-member-type :members (remove-duplicates members))
-    *empty-type*))
+      (let (ms numbers)
+       (dolist (m (remove-duplicates members))
+         (typecase m
+           (number (push (ctype-of m) numbers))
+           (t (push m ms))))
+       (apply #'type-union
+              (if ms
+                  (make-member-type :members ms)
+                  *empty-type*)
+              (nreverse numbers)))
+      *empty-type*))
 \f
 ;;;; intersection types
 ;;;;
 ;;; mechanically unparsed.
 (!define-type-method (intersection :unparse) (type)
   (declare (type ctype type))
-  (or (find type '(ratio bignum keyword) :key #'specifier-type :test #'type=)
+  (or (find type '(ratio keyword) :key #'specifier-type :test #'type=)
       `(and ,@(mapcar #'type-specifier (intersection-type-types type)))))
 
 ;;; shared machinery for type equality: true if every type in the set
            type2
            (intersection-type-types type1)))
 
-(!define-type-method (intersection :simple-subtypep) (type1 type2)
+(defun %intersection-simple-subtypep (type1 type2)
   (every/type #'%intersection-complex-subtypep-arg1
              type1
              (intersection-type-types type2)))
 
+(!define-type-method (intersection :simple-subtypep) (type1 type2)
+  (%intersection-simple-subtypep type1 type2))
+  
 (!define-type-method (intersection :complex-subtypep-arg1) (type1 type2)
   (%intersection-complex-subtypep-arg1 type1 type2))
 
-(!define-type-method (intersection :complex-subtypep-arg2) (type1 type2)
+(defun %intersection-complex-subtypep-arg2 (type1 type2)
   (every/type #'csubtypep type1 (intersection-type-types type2)))
 
+(!define-type-method (intersection :complex-subtypep-arg2) (type1 type2)
+  (%intersection-complex-subtypep-arg2 type1 type2))
+
+;;; FIXME: This will look eeriely familiar to readers of the UNION
+;;; :SIMPLE-INTERSECTION2 :COMPLEX-INTERSECTION2 method.  That's
+;;; because it was generated by cut'n'paste methods.  Given that
+;;; intersections and unions have all sorts of symmetries known to
+;;; mathematics, it shouldn't be beyond the ken of some programmers to
+;;; reflect those symmetries in code in a way that ties them together
+;;; more strongly than having two independent near-copies :-/
+(!define-type-method (intersection :simple-union2 :complex-union2)
+                    (type1 type2)
+  ;; Within this method, type2 is guaranteed to be an intersection
+  ;; type:
+  (aver (intersection-type-p type2))
+  ;; Make sure to call only the applicable methods...
+  (cond ((and (intersection-type-p type1)
+             (%intersection-simple-subtypep type1 type2)) type2)
+       ((and (intersection-type-p type1)
+             (%intersection-simple-subtypep type2 type1)) type1)
+       ((and (not (intersection-type-p type1))
+             (%intersection-complex-subtypep-arg2 type1 type2))
+        type2)
+       ((and (not (intersection-type-p type1))
+             (%intersection-complex-subtypep-arg1 type2 type1))
+        type1)
+       (t
+        (let ((accumulator *universal-type*))
+          (dolist (t2 (intersection-type-types type2) accumulator)
+            (let ((union (type-union type1 t2)))
+              (when (union-type-p union)
+                ;; we give up here -- there are all sorts of ordering
+                ;; worries, but it's better than before.  Doing
+                ;; exactly the same as in the UNION
+                ;; :SIMPLE/:COMPLEX-INTERSECTION2 method causes stack
+                ;; overflow with the mutual recursion never bottoming
+                ;; out.
+                (return nil))
+              (setf accumulator
+                    (type-intersection2 accumulator union))
+              ;; When our result isn't simple any more (because
+              ;; TYPE-INTERSECTION2 was unable to give us a simple
+              ;; result)
+              (unless accumulator
+                (return nil))))))))
+        
 (!def-type-translator and (&whole whole &rest type-specifiers)
   (apply #'type-intersection
         (mapcar #'specifier-type
     ((type= type (specifier-type 'float)) 'float)
     ((type= type (specifier-type 'real)) 'real)
     ((type= type (specifier-type 'sequence)) 'sequence)
+    ((type= type (specifier-type 'bignum)) 'bignum)
     (t `(or ,@(mapcar #'type-specifier (union-type-types type))))))
 
 ;;; Two union types are equal if they are each subtypes of each
index 8026733..8b4d624 100644 (file)
 #+nil
 (assert (and (subtypep 'function '(function))
              (subtypep '(function) 'function)))
+
+;;; Absent any exciting generalizations of |R, the type RATIONAL is
+;;; partitioned by RATIO and INTEGER.  Ensure that the type system
+;;; knows about this.  [ the type system is permitted to return NIL,
+;;; NIL for these, so if future maintenance breaks these tests that
+;;; way, that's fine.  What the SUBTYPEP calls are _not_ allowed to
+;;; return is NIL, T, because that's completely wrong. ]
+(assert (subtypep '(or integer ratio) 'rational))
+(assert (subtypep 'rational '(or integer ratio)))
index 6f9f60b..81a55db 100644 (file)
@@ -18,4 +18,4 @@
 ;;; versions, especially for internal versions off the main CVS
 ;;; branch, it gets hairier, e.g. "0.pre7.14.flaky4.13".)
 
-"0.7.12.30"
+"0.7.12.31"