Skip to content

Commit

Permalink
Fix ANSI-TEST SUBTYPEP.CONS.43
Browse files Browse the repository at this point in the history
The body of the failing test:

(deftest subtypep.cons.43
  (let* ((n -3.926510009989861d7)
         (t1 '(not (cons float t)))
         (t2 `(or (not (cons (eql 0) (real ,n ,n)))
                  (not (cons t (eql 0))))))
    (multiple-value-bind
     (sub1 good1)
     (subtypep* t1 t2)
     (multiple-value-bind
      (sub2 good2)
      (subtypep* `(not ,t2) `(not ,t1))
      (or (not good1)
          (not good2)
          (and sub1 sub2)
          (and (not sub1) (not sub2))))))
  t)

We are only interested in a part of this test. After simplifying:

(let* ((t1 '(not (cons float t)))
       (t2 `(or (not (cons (eql 0) (real -3.5d0 -3.5d0)))
                (not (cons t (eql 0))))))
  (subtypep t1 t2))

This evaluates to (VALUES NIL T), even though T2 is equivalent to T and
therefore the valid results are (VALUES T T) and (VALUES NIL NIL).

After trying to find a smaller reproducible test case, I have found
that the error is triggered with the following two types:

CCL> (csubtypep (specifier-type
                 '(CONS (NOT FLOAT) T))
                (specifier-type
                 `(OR (CONS (INTEGER 0 0)
                            (OR (REAL * (-3.5D0))
                                (NOT INTEGER)
                                (INTEGER * -1)
                                (REAL (-3.5D0))))
                      (CONS (OR (NOT INTEGER)
                                (INTEGER * -1)
                                (INTEGER 1))
                            T))))
;=> NIL, T

After digging through type methods, I have ended at TYPE=. CCL is sure that
these two are not the same type, which is an error:

CCL> (type= (specifier-type
             `(OR (CONS (INTEGER 0 0)
                        (OR (REAL * (-3.5D0))
                            (NOT INTEGER)
                            (INTEGER * -1)
                            (REAL (-3.5D0))))
                  (CONS (OR (AND (NOT FLOAT) (NOT INTEGER))
                            (INTEGER * -1)
                            (INTEGER 1))
                        T)))
            (specifier-type
             `(CONS (NOT FLOAT) T)))
;=> NIL, T

This is because of how the type method (union :complex-=) behaves:

CCL> (let ((type2 (specifier-type
                   `(OR (CONS (INTEGER 0 0)
                              (OR (REAL * (-3.5D0))
                                  (NOT INTEGER)
                                  (INTEGER * -1)
                                  (REAL (-3.5D0))))
                        (CONS (OR (AND (NOT FLOAT) (NOT INTEGER))
                                  (INTEGER * -1)
                                  (INTEGER 1))
                              T)))))
       (if (some #'type-might-contain-other-types-p
                 (union-ctype-types type2))
           (values nil nil)
           (values nil t)))
;=> NIL, T

So, we are check if any of the types of the union ctype might contain another
type. We do it like this:

(defun type-might-contain-other-types-p (type)
  (or (hairy-ctype-p type)
      (negation-ctype-p type)
      (union-ctype-p type)
      (intersection-ctype-p type)))

This list has no cons type, BUT, as we can see, the following type is a union
type containing CONS types, and these CONS types add up to T:

(OR (CONS (INTEGER 0 0)
          (OR (REAL * (-3.5D0))
              (NOT INTEGER)
              (INTEGER * -1)
              (REAL (-3.5D0))))
    (CONS (OR (NOT INTEGER)
              (INTEGER * -1)
              (INTEGER 1))
          T))

Therefore we have a bug in our implementation -
we implement that fix, the following happens:

CCL> (let* ((t1 '(not (cons float t)))
       (t2 `(or (not (cons (eql 0) (real #1=-3.5d0 #1#)))
                (not (cons t (eql 0)))))
       (c1 (ccl::specifier-type t1))
       (c2 (ccl::specifier-type t2)))
  (union-simple-subtypep c1 c2))
;=> NIL, NIL

Which is not the best that we can do, but, at least, it is correct.
  • Loading branch information
phoe committed Nov 18, 2019
1 parent d1bb819 commit ba28152
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion level-1/l1-typesys.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -470,7 +470,8 @@
(or (hairy-ctype-p type)
(negation-ctype-p type)
(union-ctype-p type)
(intersection-ctype-p type)))
(intersection-ctype-p type)
(cons-ctype-p type)))


(eval-when (:compile-toplevel :execute)
Expand Down

1 comment on commit ba28152

@phoe
Copy link
Author

@phoe phoe commented on ba28152 Nov 18, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

DO NOT USE - this commit might cause SUBTYPEP to behave more poorly and incorrectly return NIL NIL in some situations.

Please sign in to comment.