From 814fc23f60ba84318a3dfea112e6d98fd0293835 Mon Sep 17 00:00:00 2001 From: Christophe Rhodes Date: Sun, 9 Feb 2003 20:20:40 +0000 Subject: [PATCH] 0.7.12.31: 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 | 1 + src/code/early-extensions.lisp | 21 ++++++ src/code/early-type.lisp | 2 +- src/code/late-type.lisp | 145 +++++++++++++++++++++++++++++++++++++--- tests/type.pure.lisp | 9 +++ version.lisp-expr | 2 +- 6 files changed, 167 insertions(+), 13 deletions(-) diff --git a/package-data-list.lisp-expr b/package-data-list.lisp-expr index 357908f..62f29db 100644 --- a/package-data-list.lisp-expr +++ b/package-data-list.lisp-expr @@ -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" diff --git a/src/code/early-extensions.lisp b/src/code/early-extensions.lisp index 5163fe1..58a2de9 100644 --- a/src/code/early-extensions.lisp +++ b/src/code/early-extensions.lisp @@ -573,6 +573,27 @@ (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))) ;;;; package idioms diff --git a/src/code/early-type.lisp b/src/code/early-type.lisp index 0af4281..4bb7c97 100644 --- a/src/code/early-type.lisp +++ b/src/code/early-type.lisp @@ -314,7 +314,7 @@ (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))) diff --git a/src/code/late-type.lisp b/src/code/late-type.lisp index 5d3b845..5da5929 100644 --- a/src/code/late-type.lisp +++ b/src/code/late-type.lisp @@ -1057,7 +1057,7 @@ (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)))) @@ -1218,6 +1218,23 @@ 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)) @@ -1229,11 +1246,58 @@ ;; 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)) @@ -2180,8 +2244,17 @@ (!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*)) ;;;; intersection types ;;;; @@ -2208,7 +2281,7 @@ ;;; 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 @@ -2240,17 +2313,66 @@ 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 @@ -2269,6 +2391,7 @@ ((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 diff --git a/tests/type.pure.lisp b/tests/type.pure.lisp index 8026733..8b4d624 100644 --- a/tests/type.pure.lisp +++ b/tests/type.pure.lisp @@ -172,3 +172,12 @@ #+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))) diff --git a/version.lisp-expr b/version.lisp-expr index 6f9f60b..81a55db 100644 --- a/version.lisp-expr +++ b/version.lisp-expr @@ -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" -- 1.7.10.4