common-lisp/sbcl.sbcl
1
0
Fork 0
mirror of git://git.code.sf.net/p/sbcl/sbcl synced 2026-09-10 15:36:41 -04:00
Code Issues Actions 8 Packages Projects Releases Wiki Activity

0.7.12.39:

Browse source 
Refactor some of the type system:
	... new TYPE-CLASS: NEGATION, for representation of (NOT FOO)
	... in TYPEP/CTYPEP/SOURCE-TRANSFORM-TYPEP, too
	Also add a few smarts to the existing type system
	... give up slightly less often in INTERSECTION-COMPLEX-UNION2
		and UNION-COMPLEX-INTERSECTION2
	... now that we have a distinct NEGATION class, it's possible to
		write sensible UNION and INTERSECTION methods for those,
		too
	Fixes:  (SUBTYPEP T (OR REAL (NOT REAL))),
		(SUBTYPEP T (OR KEYWORD (NOT KEYWORD)))
This commit is contained in:
Christophe Rhodes 2003-02-17 15:22:49 +00:00
parent 2217cdb364
commit 58ff25d134
8 changed files with 263 additions and 207 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
package-data-list.lisp-expr
View file

@ -1133,6 +1133,7 @@ is a good idea, but see SB-SYS re. blurring of boundaries."
"MUTATOR-SELF"
"NAMED-TYPE" "NAMED-TYPE-NAME" "NAMED-TYPE-P"
"NATIVE-BYTE-ORDER" "NEGATE"
"NEGATION-TYPE" "NEGATION-TYPE-TYPE"
"NEVER-SUBTYPEP" "NIL-FUN-RETURNED-ERROR"
"NOT-<=-ERROR" "NOT-=-ERROR"
"NOT-DUMPED-AT-ALL"

12
src/code/early-type.lisp
View file

@ -38,6 +38,18 @@
(defstruct (unknown-type (:include hairy-type)
(:copier nil)))
(defstruct (negation-type (:include ctype
(class-info (type-class-or-lose 'negation))
;; FIXME: is this right? It's
;; what they had before, anyway
(enumerable t)
(might-contain-other-types-p t))
(:copier nil)
#!+cmu (:pure nil))
(type (missing-arg) :type ctype))
(!define-type-class negation)
;;; ARGS-TYPE objects are used both to represent VALUES types and
;;; to represent FUNCTION types.
(defstruct (args-type (:include ctype)

437
src/code/late-type.lisp
View file

@ -1084,221 +1084,40 @@
(!define-type-method (hairy :simple-subtypep) (type1 type2)
(let ((hairy-spec1 (hairy-type-specifier type1))
(hairy-spec2 (hairy-type-specifier type2)))
(cond ((and (consp hairy-spec1) (eq (car hairy-spec1) 'not)
(consp hairy-spec2) (eq (car hairy-spec2) 'not))
(csubtypep (specifier-type (cadr hairy-spec2))
(specifier-type (cadr hairy-spec1))))
((equal hairy-spec1 hairy-spec2)
(cond ((equal-but-no-car-recursion hairy-spec1 hairy-spec2)
(values t t))
(t
(values nil nil)))))
(!define-type-method (hairy :complex-subtypep-arg2) (type1 type2)
(let ((hairy-spec (hairy-type-specifier type2)))
(cond ((and (consp hairy-spec) (eq (car hairy-spec) 'not))
(let* ((complement-type2 (specifier-type (cadr hairy-spec)))
(intersection2 (type-intersection2 type1
complement-type2)))
(if intersection2
(values (eq intersection2 *empty-type*) t)
(invoke-complex-subtypep-arg1-method type1 type2))))
(t
(invoke-complex-subtypep-arg1-method type1 type2)))))
(invoke-complex-subtypep-arg1-method type1 type2))
(!define-type-method (hairy :complex-subtypep-arg1) (type1 type2)
;; "Incrementally extended heuristic algorithms tend inexorably toward the
;; incomprehensible." -- http://www.unlambda.com/~james/lambda/lambda.txt
(let ((hairy-spec (hairy-type-specifier type1)))
(cond ((and (consp hairy-spec) (eq (car hairy-spec) 'not))
;; You may not believe this. I couldn't either. But then I
;; sat down and drew lots of Venn diagrams. Comments
;; involving a and b refer to the call (subtypep '(not a)
;; 'b) -- CSR, 2002-02-27.
(block nil
;; (Several logical truths in this block are true as
;; long as b/=T. As of sbcl-0.7.1.28, it seems
;; impossible to construct a case with b=T where we
;; actually reach this type method, but we'll test for
;; and exclude this case anyway, since future
;; maintenance might make it possible for it to end up
;; in this code.)
(multiple-value-bind (equal certain)
(type= type2 (specifier-type t))
(unless certain
(return (values nil nil)))
(when equal
(return (values t t))))
(let ((complement-type1 (specifier-type (cadr hairy-spec))))
;; Do the special cases first, in order to give us a
;; chance if subtype/supertype relationships are hairy.
(multiple-value-bind (equal certain)
(type= complement-type1 type2)
;; If a = b, ~a is not a subtype of b (unless b=T,
;; which was excluded above).
(unless certain
(return (values nil nil)))
(when equal
(return (values nil t))))
;; KLUDGE: ANSI requires that the SUBTYPEP result
;; between any two built-in atomic type specifiers
;; never be uncertain. This is hard to do cleanly for
;; the built-in types whose definitions include
;; (NOT FOO), i.e. CONS and RATIO. However, we can do
;; it with this hack, which uses our global knowledge
;; that our implementation of the type system uses
;; disjoint implementation types to represent disjoint
;; sets (except when types are contained in other types).
;; (This is a KLUDGE because it's fragile. Various
;; changes in internal representation in the type
;; system could make it start confidently returning
;; incorrect results.) -- WHN 2002-03-08
(unless (or (type-might-contain-other-types-p complement-type1)
(type-might-contain-other-types-p type2))
;; Because of the way our types which don't contain
;; other types are disjoint subsets of the space of
;; possible values, (SUBTYPEP '(NOT AA) 'B)=NIL when
;; AA and B are simple (and B is not T, as checked above).
(return (values nil t)))
;; The old (TYPE= TYPE1 TYPE2) branch would never be
;; taken, as TYPE1 and TYPE2 will only be equal if
;; they're both NOT types, and then the
;; :SIMPLE-SUBTYPEP method would be used instead.
;; But a CSUBTYPEP relationship might still hold:
(multiple-value-bind (equal certain)
(csubtypep complement-type1 type2)
;; If a is a subtype of b, ~a is not a subtype of b
;; (unless b=T, which was excluded above).
(unless certain
(return (values nil nil)))
(when equal
(return (values nil t))))
(multiple-value-bind (equal certain)
(csubtypep type2 complement-type1)
;; If b is a subtype of a, ~a is not a subtype of b.
;; (FIXME: That's not true if a=T. Do we know at
;; this point that a is not T?)
(unless certain
(return (values nil nil)))
(when equal
(return (values nil t))))
;; old CSR comment ca. 0.7.2, now obsoleted by the
;; SIMPLE-CTYPE? KLUDGE case above:
;; Other cases here would rely on being able to catch
;; all possible cases, which the fragility of this
;; type system doesn't inspire me; for instance, if a
;; is type= to ~b, then we want T, T; if this is not
;; the case and the types are disjoint (have an
;; intersection of *empty-type*) then we want NIL, T;
;; else if the union of a and b is the
;; *universal-type* then we want T, T. So currently we
;; still claim to be unsure about e.g. (subtypep '(not
;; fixnum) 'single-float).
)))
(t
(values nil nil)))))
(declare (ignore type1 type2))
(values nil nil))
(!define-type-method (hairy :complex-=) (type1 type2)
(declare (ignore type1 type2))
(values nil nil))
(!define-type-method (hairy :simple-intersection2)
(!define-type-method (hairy :simple-intersection2 :complex-intersection2)
(type1 type2)
(if (type= type1 type2)
type1
nil))
(!define-type-method (hairy :complex-intersection2)
(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 type1 (specifier-type (cadr hairy-type-spec)))
*empty-type*
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))
(if (equal-but-no-car-recursion (hairy-type-specifier type1)
(hairy-type-specifier type2))
(values t t)
(values nil nil)))
(!def-type-translator not (&whole whole type)
(declare (ignore type))
;; Check legality of arguments.
(destructuring-bind (not typespec) whole
(declare (ignore not))
;; 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))
;; Check legality of arguments.
@ -1313,6 +1132,212 @@
;; Create object.
(make-hairy-type :specifier whole))
;;;; negation types
(!define-type-method (negation :unparse) (x)
`(not ,(type-specifier (negation-type-type x))))
(!define-type-method (negation :simple-subtypep) (type1 type2)
(csubtypep (negation-type-type type2) (negation-type-type type1)))
(!define-type-method (negation :complex-subtypep-arg2) (type1 type2)
(let* ((complement-type2 (negation-type-type type2))
(intersection2 (type-intersection2 type1
complement-type2)))
(if intersection2
(values (eq intersection2 *empty-type*) t)
(invoke-complex-subtypep-arg1-method type1 type2))))
(!define-type-method (negation :complex-subtypep-arg1) (type1 type2)
;; "Incrementally extended heuristic algorithms tend inexorably toward the
;; incomprehensible." -- http://www.unlambda.com/~james/lambda/lambda.txt
;;
;; You may not believe this. I couldn't either. But then I sat down
;; and drew lots of Venn diagrams. Comments involving a and b refer
;; to the call (subtypep '(not a) 'b) -- CSR, 2002-02-27.
(block nil
;; (Several logical truths in this block are true as long as
;; b/=T. As of sbcl-0.7.1.28, it seems impossible to construct a
;; case with b=T where we actually reach this type method, but
;; we'll test for and exclude this case anyway, since future
;; maintenance might make it possible for it to end up in this
;; code.)
(multiple-value-bind (equal certain)
(type= type2 *universal-type*)
(unless certain
(return (values nil nil)))
(when equal
(return (values t t))))
(let ((complement-type1 (negation-type-type type1)))
;; Do the special cases first, in order to give us a chance if
;; subtype/supertype relationships are hairy.
(multiple-value-bind (equal certain)
(type= complement-type1 type2)
;; If a = b, ~a is not a subtype of b (unless b=T, which was
;; excluded above).
(unless certain
(return (values nil nil)))
(when equal
(return (values nil t))))
;; KLUDGE: ANSI requires that the SUBTYPEP result between any
;; two built-in atomic type specifiers never be uncertain. This
;; is hard to do cleanly for the built-in types whose
;; definitions include (NOT FOO), i.e. CONS and RATIO. However,
;; we can do it with this hack, which uses our global knowledge
;; that our implementation of the type system uses disjoint
;; implementation types to represent disjoint sets (except when
;; types are contained in other types). (This is a KLUDGE
;; because it's fragile. Various changes in internal
;; representation in the type system could make it start
;; confidently returning incorrect results.) -- WHN 2002-03-08
(unless (or (type-might-contain-other-types-p complement-type1)
(type-might-contain-other-types-p type2))
;; Because of the way our types which don't contain other
;; types are disjoint subsets of the space of possible values,
;; (SUBTYPEP '(NOT AA) 'B)=NIL when AA and B are simple (and B
;; is not T, as checked above).
(return (values nil t)))
;; The old (TYPE= TYPE1 TYPE2) branch would never be taken, as
;; TYPE1 and TYPE2 will only be equal if they're both NOT types,
;; and then the :SIMPLE-SUBTYPEP method would be used instead.
;; But a CSUBTYPEP relationship might still hold:
(multiple-value-bind (equal certain)
(csubtypep complement-type1 type2)
;; If a is a subtype of b, ~a is not a subtype of b (unless
;; b=T, which was excluded above).
(unless certain
(return (values nil nil)))
(when equal
(return (values nil t))))
(multiple-value-bind (equal certain)
(csubtypep type2 complement-type1)
;; If b is a subtype of a, ~a is not a subtype of b. (FIXME:
;; That's not true if a=T. Do we know at this point that a is
;; not T?)
(unless certain
(return (values nil nil)))
(when equal
(return (values nil t))))
;; old CSR comment ca. 0.7.2, now obsoleted by the SIMPLE-CTYPE?
;; KLUDGE case above: Other cases here would rely on being able
;; to catch all possible cases, which the fragility of this type
;; system doesn't inspire me; for instance, if a is type= to ~b,
;; then we want T, T; if this is not the case and the types are
;; disjoint (have an intersection of *empty-type*) then we want
;; NIL, T; else if the union of a and b is the *universal-type*
;; then we want T, T. So currently we still claim to be unsure
;; about e.g. (subtypep '(not fixnum) 'single-float).
;;
;; OTOH we might still get here:
(values nil nil))))
(!define-type-method (negation :complex-=) (type1 type2)
;; (NOT FOO) isn't equivalent to anything that's not a negation
;; type, except possibly a hairy type.
(declare (ignore type2))
(if (hairy-type-p type1)
(values nil nil)
(values nil t)))
(!define-type-method (negation :simple-intersection2) (type1 type2)
(let ((not1 (negation-type-type type1))
(not2 (negation-type-type type2)))
(cond
((csubtypep not1 not2) type2)
((csubtypep not2 not1) type1)
;; Why no analagous clause to the disjoint in the SIMPLE-UNION2
;; method, below? The clause would read
;;
;; ((EQ (TYPE-UNION NOT1 NOT2) *UNIVERSAL-TYPE*) *EMPTY-TYPE*)
;;
;; but with proper canonicalization of negation types, there's
;; no way of constructing two negation types with union of their
;; negations being the universal type.
(t
(aver (not (eq (type-union not1 not2) *universal-type*)))
nil))))
(!define-type-method (negation :complex-intersection2) (type1 type2)
(cond
((csubtypep type1 (negation-type-type type2)) *empty-type*)
((eq (type-intersection type1 (negation-type-type type2)) *empty-type*)
type1)
(t nil)))
(!define-type-method (negation :simple-union2) (type1 type2)
(let ((not1 (negation-type-type type1))
(not2 (negation-type-type type2)))
(cond
((csubtypep not1 not2) type1)
((csubtypep not2 not1) type2)
((eq (type-intersection not1 not2) *empty-type*)
*universal-type*)
(t nil))))
(!define-type-method (negation :complex-union2) (type1 type2)
(cond
((csubtypep (negation-type-type type2) type1) *universal-type*)
((eq (type-intersection type1 (negation-type-type type2)) *empty-type*)
type2)
(t nil)))
(!define-type-method (negation :simple-=) (type1 type2)
(type= (negation-type-type type1) (negation-type-type type2)))
(!def-type-translator not (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)))
;; canonicalize (NOT NIL) and (NOT T)
((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-negation-type :type not-type))
((numeric-type-p not-type)
(type-union
(make-negation-type
:type (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))))))
((intersection-type-p not-type)
(apply #'type-union
(mapcar #'(lambda (x)
(specifier-type `(not ,(type-specifier x))))
(intersection-type-types not-type))))
((union-type-p not-type)
(apply #'type-intersection
(mapcar #'(lambda (x)
(specifier-type `(not ,(type-specifier x))))
(union-type-types not-type))))
(t (make-negation-type :type not-type)))))
;;;; numeric types
(!define-type-class number)
@ -2355,23 +2380,27 @@
type1)
(t
(let ((accumulator *universal-type*))
(dolist (t2 (intersection-type-types type2) accumulator)
(let ((union (type-union type1 t2)))
(do ((t2s (intersection-type-types type2) (cdr t2s)))
((null t2s) accumulator)
(let ((union (type-union type1 (car t2s))))
(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
;; we have to 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))
(if (and (eq accumulator *universal-type*)
(null (cdr t2s)))
;; KLUDGE: if we get here, we have a partially
;; simplified result. While this isn't by any
;; means a universal simplification, including
;; this logic here means that we can get (OR
;; KEYWORD (NOT KEYWORD)) canonicalized to T.
(return union)
(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))))))))
(type-intersection accumulator union))))))))
(!def-type-translator and (&whole whole &rest type-specifiers)
(apply #'type-intersection
@ -2531,12 +2560,8 @@
(let ((accumulator *empty-type*))
(dolist (t2 (union-type-types type2) accumulator)
(setf accumulator
(type-union2 accumulator
(type-intersection type1 t2)))
;; When our result isn't simple any more (because
;; TYPE-UNION2 was unable to give us a simple result)
(unless accumulator
(return nil)))))))
(type-union accumulator
(type-intersection type1 t2))))))))
(!def-type-translator or (&rest type-specifiers)
(apply #'type-union

6
src/code/target-type.lisp
View file

@ -58,6 +58,12 @@
(values nil nil))
(alien-type-type
(values (alien-typep obj (alien-type-type-alien-type type)) t))
(negation-type
(multiple-value-bind (res win)
(ctypep obj (negation-type-type type))
(if win
(values (not res) t)
(values nil nil))))
(hairy-type
;; Now the tricky stuff.
(let* ((hairy-spec (hairy-type-specifier type))

2
src/code/typep.lisp
View file

@ -158,6 +158,8 @@
(error "unknown type specifier: ~S"
(unknown-type-specifier reparse))
(%%typep object reparse))))
(negation-type
(not (%%typep object (negation-type-type type))))
(hairy-type
;; Now the tricky stuff.
(let* ((hairy-spec (hairy-type-specifier type))

7
src/compiler/typetran.lisp
View file

@ -276,6 +276,11 @@
`(typep ,n-obj ',x))
(rest spec))))))))))
(defun source-transform-negation-typep (object type)
(declare (type negation-type type))
(let ((spec (type-specifier (negation-type-type type))))
`(not (typep ,object ',spec))))
;;; Do source transformation for TYPEP of a known union type. If a
;;; union type contains LIST, then we pull that out and make it into a
;;; single LISTP call. Note that if SYMBOL is in the union, then LIST
@ -505,6 +510,8 @@
(typecase type
(hairy-type
(source-transform-hairy-typep object type))
(negation-type
(source-transform-negation-typep object type))
(union-type
(source-transform-union-typep object type))
(intersection-type

3
tests/type.pure.lisp
View file

@ -181,3 +181,6 @@
;;; return is NIL, T, because that's completely wrong. ]
(assert (subtypep '(or integer ratio) 'rational))
(assert (subtypep 'rational '(or integer ratio)))
;;; Likewise, these are allowed to return NIL, NIL:
(assert (subtypep t '(or real (not real))))
(assert (subtypep t '(or keyword (not keyword))))

2
version.lisp-expr
View 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.38"
"0.7.12.39"