types-aux.lsp 6.57 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12
;-*- Mode:     Lisp -*-
;;;; Author:   Paul Dietz
;;;; Created:  Mon Jun 21 20:14:38 2004
;;;; Contains: Aux. functions for types tests

(in-package :cl-test)

(defun classes-are-disjoint (c1 c2)
  "If either c1 or c2 is a builtin class or the name of a builtin
   class, then check for disjointness.  Return a non-NIL list
   of failed subtypep relationships, if any."
  (and (or (is-builtin-class c1)
sds's avatar
sds committed
13
           (is-builtin-class c2))
14 15 16 17 18 19 20 21 22 23
       (check-disjointness c1 c2)))

(declaim (special *subtype-table*))

(defun types.6-body ()
  (loop
      for p in *subtype-table*
      for tp = (car p)
      append
      (and (not (member tp '(sequence cons list t)))
sds's avatar
sds committed
24 25
           (let ((message (check-subtypep tp 'atom t t)))
             (if message (list message))))))
26 27 28 29 30 31

(defparameter *type-list* nil)
(defparameter *supertype-table* nil)

(defun types.9-body ()
  (let ((tp-list (append '(keyword atom list)
sds's avatar
sds committed
32 33
                         (loop for p in *subtype-table* collect (car p))))
        (result-list))
34 35 36 37 38 39 40 41
    (setf tp-list (remove-duplicates tp-list))
    ;; TP-LIST is now a list of unique CL type names
    ;; Store it in *TYPE-LIST* so we can inspect it later if this test
    ;; fails.  The variable is also used in test TYPES.9A
    (setf *type-list* tp-list)
    ;; Compute all pairwise SUBTYPEP relationships among
    ;; the elements of *TYPE-LIST*.
    (let ((subs (make-hash-table :test #'eq))
sds's avatar
sds committed
42
          (sups (make-hash-table :test #'eq)))
43
      (loop
sds's avatar
sds committed
44 45 46 47 48 49 50 51 52
          for x in tp-list do
            (loop
                for y in tp-list do
                  (multiple-value-bind (result good)
                      (subtypep* x y)
                    (declare (ignore good))
                    (when result
                      (pushnew x (gethash y subs))
                      (pushnew y (gethash x sups))))))
53 54 55 56 57 58
      ;; Store the supertype relations for later inspection
      ;; and use in test TYPES.9A
      (setf *supertype-table* sups)
      ;; Check that the relation we just computed is transitive.
      ;; Return a list of triples on which transitivity fails.
      (loop
sds's avatar
sds committed
59 60 61 62 63 64 65 66 67 68 69 70 71
          for x in tp-list do
            (let ((sub-list (gethash x subs))
                  (sup-list (gethash x sups)))
              (loop
                  for t1 in sub-list do
                    (loop
                        for t2 in sup-list do
                          (multiple-value-bind (result good)
                              (subtypep* t1 t2)
                            (when (and good (not result))
                              (pushnew (list t1 x t2) result-list
                                       :test #'equal)))))))

72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89
      result-list)))

;;; TYPES.9-BODY returns a list of triples (T1 T2 T3)
;;; where (AND (SUBTYPEP T1 T2) (SUBTYPEP T2 T3) (NOT (SUBTYPEP T1 T3)))
;;;  (and where SUBTYPEP succeeds in each case, returning true as its
;;;   second return value.)

(defun types.9a-body ()
  (cond
   ((not (and *type-list* *supertype-table*))
    (format nil "Run test type.9 first~%")
    nil)
   (t
    (loop
     for tp in *type-list*
     sum
     (let ((sups (gethash tp *supertype-table*)))
       (loop
sds's avatar
sds committed
90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109
        for x in *universe*
        sum
        (handler-case
         (cond
          ((not (typep x tp)) 0)
          (t
           (loop
            for tp2 in sups
            count
            (handler-case
             (and (not (typep x tp2))
                  (progn
                    (format t "Found element of ~S not in ~S: ~S~%"
                            tp tp2 x)
                    t))
             (condition (c) (format t "Error ~S occured: ~S~%"
                                    c tp2)
                        t)))))
         (condition (c) (format t "Error ~S occured: ~S~%" c tp)
                    1))))))))
110 111 112 113 114 115 116 117

(defun check-subtypep (type1 type2 is-sub &optional should-be-valid)
  (multiple-value-bind
      (sub valid)
      (subtypep type1 type2)
    (unless (constantp type1) (setq type1 (list 'quote type1)))
    (unless (constantp type2) (setq type2 (list 'quote type2)))
    (if (or (and valid sub (not is-sub))
sds's avatar
sds committed
118 119 120
            (and valid (not sub) is-sub)
            (and (not valid) should-be-valid))
        `(((SUBTYPEP ,type1 ,type2) :==> ,sub ,valid))
121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
      nil)))

;;; Check that the subtype relationships implied
;;; by disjointness are not contradicted.  Return NIL
;;; if ok, or a list of error messages if not.

;;; Assumes the types are nonempty.

(defun check-disjointness (type1 type2)
  (append
   (check-subtypep type1 type2 nil)
   (check-subtypep type2 type1 nil)
   (check-subtypep type1 `(not ,type2) t)
   (check-subtypep type2 `(not ,type1) t)
   (check-subtypep `(and ,type1 ,type2) nil t)
   (check-subtypep `(and ,type2 ,type1) nil t)
   (check-subtypep `(and ,type1 (not ,type2)) type1 t)
   (check-subtypep `(and (not ,type2) ,type1) type1 t)
   (check-subtypep `(and ,type2 (not ,type1)) type2 t)
   (check-subtypep `(and (not ,type1) ,type2) type2 t)
;;;   (check-subtypep type1 `(or ,type1 (not ,type2)) t)
;;;   (check-subtypep type1 `(or (not ,type2) ,type1) t)
;;;   (check-subtypep type2 `(or ,type2 (not ,type1)) t)
;;;   (check-subtypep type2 `(or (not ,type1) ,type2) t)
   (check-subtypep t `(or (not ,type1) (not ,type2)) t)
   (check-subtypep t `(or (not ,type2) (not ,type1)) t)
   ))

(defun check-equivalence (type1 type2)
  (append
   (check-subtypep type1 type2 t)
   (check-subtypep type2 type1 t)
   (check-subtypep `(not ,type1) `(not ,type2) t)
   (check-subtypep `(not ,type2) `(not ,type1) t)
   (check-subtypep `(and ,type1 (not ,type2)) nil t)
   (check-subtypep `(and ,type2 (not ,type1)) nil t)
   (check-subtypep `(and (not ,type2) ,type1) nil t)
   (check-subtypep `(and (not ,type1) ,type2) nil t)
   (check-subtypep t `(or ,type1 (not ,type2)) t)
   (check-subtypep t `(or ,type2 (not ,type1)) t)
   (check-subtypep t `(or (not ,type2) ,type1) t)
   (check-subtypep t `(or (not ,type1) ,type2) t)))

(defun check-all-subtypep (type1 type2)
  (append
   (check-subtypep type1 type2 t)
   (check-subtypep `(not ,type2) `(not ,type1) t)
   (check-subtypep `(and ,type1 (not ,type2)) nil t)
   (check-subtypep t `(or (not ,type1) ,type2) t)))

(defun check-all-not-subtypep (type1 type2)
  (append
   (check-subtypep type1 type2 nil)
   (check-subtypep `(not ,type2) `(not ,type1) nil)))

(defun subtypep-and-contrapositive-are-consistent (t1 t2)
  (multiple-value-bind (sub1 success1)
      (subtypep* t1 t2)
    (multiple-value-bind (sub2 success2)
sds's avatar
sds committed
180
        (subtypep* `(not ,t2) `(not ,t1))
181
      (or (not success1)
sds's avatar
sds committed
182 183
          (not success2)
          (eqlt sub1 sub2)))))
184 185 186 187

;;; For use in deftype tests
(deftype even-array (&optional type size)
  `(and (array ,type ,size)
sds's avatar
sds committed
188
        (satisfies even-size-p)))