Filtering...

type-set-a

type-set-a
other
(in-package "ACL2")
other
(def-basic-type-sets *ts-zero*
  *ts-one*
  *ts-integer>1*
  *ts-positive-ratio*
  *ts-negative-integer*
  *ts-negative-ratio*
  *ts-complex-rational*
  *ts-nil*
  *ts-t*
  *ts-non-t-non-nil-symbol*
  *ts-proper-cons*
  *ts-improper-cons*
  *ts-string*
  *ts-character*)
*ts-positive-integer*constant
(defconst *ts-positive-integer*
  (ts-union0 *ts-one* *ts-integer>1*))
*ts-non-negative-integer*constant
(defconst *ts-non-negative-integer*
  (ts-union0 *ts-zero* *ts-positive-integer*))
*ts-non-positive-integer*constant
(defconst *ts-non-positive-integer*
  (ts-union0 *ts-zero* *ts-negative-integer*))
*ts-integer*constant
(defconst *ts-integer*
  (ts-union0 *ts-positive-integer*
    *ts-zero*
    *ts-negative-integer*))
*ts-rational*constant
(defconst *ts-rational*
  (ts-union0 *ts-integer*
    *ts-positive-ratio*
    *ts-negative-ratio*))
*ts-acl2-number*constant
(defconst *ts-acl2-number*
  (ts-union0 *ts-rational* *ts-complex-rational*))
*ts-rational-acl2-number*constant
(defconst *ts-rational-acl2-number*
  (ts-union0 *ts-rational* *ts-complex-rational*))
*ts-negative-rational*constant
(defconst *ts-negative-rational*
  (ts-union0 *ts-negative-integer* *ts-negative-ratio*))
*ts-positive-rational*constant
(defconst *ts-positive-rational*
  (ts-union0 *ts-positive-integer* *ts-positive-ratio*))
*ts-non-positive-rational*constant
(defconst *ts-non-positive-rational*
  (ts-union0 *ts-zero* *ts-negative-rational*))
*ts-non-negative-rational*constant
(defconst *ts-non-negative-rational*
  (ts-union0 *ts-zero* *ts-positive-rational*))
*ts-ratio*constant
(defconst *ts-ratio*
  (ts-union0 *ts-positive-ratio* *ts-negative-ratio*))
*ts-bit*constant
(defconst *ts-bit* (ts-union0 *ts-zero* *ts-one*))
*ts-cons*constant
(defconst *ts-cons*
  (ts-union0 *ts-proper-cons* *ts-improper-cons*))
*ts-boolean*constant
(defconst *ts-boolean* (ts-union0 *ts-nil* *ts-t*))
*ts-true-list*constant
(defconst *ts-true-list*
  (ts-union0 *ts-nil* *ts-proper-cons*))
*ts-non-nil*constant
(defconst *ts-non-nil* (ts-complement0 *ts-nil*))
*ts-symbol*constant
(defconst *ts-symbol*
  (ts-union0 *ts-nil* *ts-t* *ts-non-t-non-nil-symbol*))
*ts-true-list-or-string*constant
(defconst *ts-true-list-or-string*
  (ts-union0 *ts-true-list* *ts-string*))
*ts-empty*constant
(defconst *ts-empty* 0)
*ts-unknown*constant
(defconst *ts-unknown* -1)
one-bit-type-setpfunction
(defun one-bit-type-setp
  (ts)
  (or (= (the-type-set ts) *ts-zero*)
    (= (the-type-set ts) *ts-one*)
    (= (the-type-set ts) *ts-integer>1*)
    (= (the-type-set ts) *ts-positive-ratio*)
    (= (the-type-set ts) *ts-negative-integer*)
    (= (the-type-set ts) *ts-negative-ratio*)
    (= (the-type-set ts) *ts-complex-rational*)
    (= (the-type-set ts) *ts-nil*)
    (= (the-type-set ts) *ts-t*)
    (= (the-type-set ts) *ts-non-t-non-nil-symbol*)
    (= (the-type-set ts) *ts-proper-cons*)
    (= (the-type-set ts) *ts-improper-cons*)
    (= (the-type-set ts) *ts-string*)
    (= (the-type-set ts) *ts-character*)))
*code-type-set-alist*constant
(defconst *code-type-set-alist*
  (list (cons '*ts-unknown* *ts-unknown*)
    (cons '*ts-non-nil* *ts-non-nil*)
    (cons '*ts-acl2-number* *ts-acl2-number*)
    (cons '*ts-rational-acl2-number* *ts-rational-acl2-number*)
    (cons '*ts-rational* *ts-rational*)
    (cons '*ts-true-list-or-string* *ts-true-list-or-string*)
    (cons '*ts-symbol* *ts-symbol*)
    (cons '*ts-integer* *ts-integer*)
    (cons '*ts-non-positive-rational*
      *ts-non-positive-rational*)
    (cons '*ts-non-negative-rational*
      *ts-non-negative-rational*)
    (cons '*ts-negative-rational* *ts-negative-rational*)
    (cons '*ts-positive-rational* *ts-positive-rational*)
    (cons '*ts-non-negative-integer* *ts-non-negative-integer*)
    (cons '*ts-non-positive-integer* *ts-non-positive-integer*)
    (cons '*ts-positive-integer* *ts-positive-integer*)
    (cons '*ts-bit* *ts-bit*)
    (cons '*ts-ratio* *ts-ratio*)
    (cons '*ts-cons* *ts-cons*)
    (cons '*ts-boolean* *ts-boolean*)
    (cons '*ts-true-list* *ts-true-list*)
    (cons '*ts-integer>1* *ts-integer>1*)
    (cons '*ts-zero* *ts-zero*)
    (cons '*ts-one* *ts-one*)
    (cons '*ts-positive-ratio* *ts-positive-ratio*)
    (cons '*ts-negative-integer* *ts-negative-integer*)
    (cons '*ts-negative-ratio* *ts-negative-ratio*)
    (cons '*ts-complex-rational* *ts-complex-rational*)
    (cons '*ts-nil* *ts-nil*)
    (cons '*ts-t* *ts-t*)
    (cons '*ts-non-t-non-nil-symbol* *ts-non-t-non-nil-symbol*)
    (cons '*ts-proper-cons* *ts-proper-cons*)
    (cons '*ts-improper-cons* *ts-improper-cons*)
    (cons '*ts-string* *ts-string*)
    (cons '*ts-character* *ts-character*)
    (cons '*ts-empty* *ts-empty*)))
logior-lstfunction
(defun logior-lst
  (lst ans)
  (cond ((null lst) ans)
    (t (logior-lst (cdr lst) (logior (car lst) ans)))))
logand-lstfunction
(defun logand-lst
  (lst ans)
  (cond ((null lst) ans)
    (t (logand-lst (cdr lst) (logand (car lst) ans)))))
ts-complement-fnmutual-recursion
(mutual-recursion (defun ts-complement-fn
    (x)
    (let ((y (eval-type-set x)))
      (if (integerp y)
        (lognot y)
        (list 'lognot (list 'the-type-set y)))))
  (defun ts-union-fn
    (x)
    (cond ((null x) '*ts-empty*)
      ((null (cdr x)) (eval-type-set (car x)))
      (t (let ((lst (eval-type-set-lst x)))
          (cond ((integer-listp lst) (logior-lst lst *ts-empty*))
            (t (xxxjoin 'logior lst)))))))
  (defun ts-intersection-fn
    (x)
    (cond ((null x) '*ts-unknown*)
      ((null (cdr x)) (eval-type-set (car x)))
      (t (let ((lst (eval-type-set-lst x)))
          (cond ((integer-listp lst) (logand-lst lst *ts-unknown*))
            (t (xxxjoin 'logand lst)))))))
  (defun eval-type-set
    (x)
    (cond ((and (symbolp x) (legal-constantp1 x)) (or (cdr (assoc-eq x *code-type-set-alist*))
          (er hard
            'eval-type-set
            "The constant ~x0 appears as an argument to a ts- function but is ~
             not known to *code-type-set-alist*, whose current value ~
             is:~%~x1. You should redefine that constant or define your own ~
             ts- functions if you want to avoid this problem."
            x
            *code-type-set-alist*)))
      ((atom x) x)
      (t (case (car x)
          '(if (integerp (cadr x))
            (cadr x)
            x)
          (ts-union (ts-union-fn (cdr x)))
          (ts-intersection (ts-intersection-fn (cdr x)))
          (ts-complement (ts-complement-fn (cadr x)))
          (t x)))))
  (defun eval-type-set-lst
    (x)
    (cond ((consp x) (let ((y (eval-type-set (car x))))
          (cons (if (integerp y)
              y
              (list 'the-type-set y))
            (eval-type-set-lst (cdr x)))))
      (t nil))))
ts-complementmacro
(defmacro ts-complement
  (x)
  (list 'the-type-set (ts-complement-fn x)))
ts-intersectionmacro
(defmacro ts-intersection
  (&rest x)
  (list 'the-type-set (ts-intersection-fn x)))
ts-unionmacro
(defmacro ts-union
  (&rest x)
  (list 'the-type-set (ts-union-fn x)))
ts-subsetpmacro
(defmacro ts-subsetp
  (ts1 ts2)
  (list 'let
    (list (list 'ts1 ts1) (list 'ts2 ts2))
    `(declare (type (integer ,*MIN-TYPE-SET* ,*MAX-TYPE-SET*) ts1 ts2))
    '(ts= (ts-intersection ts1 ts2) ts1)))
type-set-binary-+-alist-entryfunction
(defun type-set-binary-+-alist-entry
  (ts1 ts2)
  (ts-builder ts1
    (*ts-zero* ts2)
    (*ts-one* (ts-builder ts2
        (*ts-zero* ts1)
        (*ts-one* *ts-integer>1*)
        (*ts-integer>1* *ts-integer>1*)
        (*ts-negative-integer* *ts-non-positive-integer*)
        (*ts-positive-ratio* *ts-positive-ratio*)
        (*ts-negative-ratio* *ts-ratio*)
        (*ts-complex-rational* *ts-complex-rational*)))
    (*ts-integer>1* (ts-builder ts2
        (*ts-zero* ts1)
        (*ts-one* *ts-integer>1*)
        (*ts-integer>1* *ts-integer>1*)
        (*ts-negative-integer* *ts-integer*)
        (*ts-positive-ratio* *ts-positive-ratio*)
        (*ts-negative-ratio* *ts-ratio*)
        (*ts-complex-rational* *ts-complex-rational*)))
    (*ts-negative-integer* (ts-builder ts2
        (*ts-zero* ts1)
        (*ts-one* *ts-non-positive-integer*)
        (*ts-integer>1* *ts-integer*)
        (*ts-negative-integer* *ts-negative-integer*)
        (*ts-positive-ratio* *ts-ratio*)
        (*ts-negative-ratio* *ts-negative-ratio*)
        (*ts-complex-rational* *ts-complex-rational*)))
    (*ts-positive-ratio* (ts-builder ts2
        (*ts-zero* ts1)
        (*ts-one* *ts-positive-ratio*)
        (*ts-integer>1* *ts-positive-ratio*)
        (*ts-negative-integer* *ts-ratio*)
        (*ts-positive-ratio* *ts-positive-rational*)
        (*ts-negative-ratio* *ts-rational*)
        (*ts-complex-rational* *ts-complex-rational*)))
    (*ts-negative-ratio* (ts-builder ts2
        (*ts-zero* ts1)
        (*ts-one* *ts-ratio*)
        (*ts-integer>1* *ts-ratio*)
        (*ts-negative-integer* *ts-negative-ratio*)
        (*ts-positive-ratio* *ts-rational*)
        (*ts-negative-ratio* *ts-negative-rational*)
        (*ts-complex-rational* *ts-complex-rational*)))
    (*ts-complex-rational* (ts-builder ts2
        (*ts-zero* ts1)
        (*ts-one* *ts-complex-rational*)
        (*ts-integer>1* *ts-complex-rational*)
        (*ts-negative-integer* *ts-complex-rational*)
        (*ts-positive-ratio* *ts-complex-rational*)
        (*ts-negative-ratio* *ts-complex-rational*)
        (*ts-complex-rational* *ts-rational-acl2-number*)))))
type-set-binary-+-alist1function
(defun type-set-binary-+-alist1
  (i j lst)
  (cond ((< j 0) lst)
    (t (let ((x (type-set-binary-+-alist-entry i j)))
        (cond ((= x *ts-unknown*) (type-set-binary-+-alist1 i (1- j) lst))
          (t (type-set-binary-+-alist1 i
              (1- j)
              (cons (cons (cons i j) x) lst))))))))
type-set-binary-+-alistfunction
(defun type-set-binary-+-alist
  (i j lst)
  (cond ((< i 0) lst)
    (t (type-set-binary-+-alist (1- i)
        j
        (type-set-binary-+-alist1 i j lst)))))
type-set-binary-*-alist-entryfunction
(defun type-set-binary-*-alist-entry
  (ts1 ts2)
  (ts-builder ts1
    (*ts-zero* *ts-zero*)
    (*ts-one* ts2)
    (*ts-integer>1* (ts-builder ts2
        (*ts-zero* *ts-zero*)
        (*ts-one* ts1)
        (*ts-integer>1* *ts-integer>1*)
        (*ts-negative-integer* *ts-negative-integer*)
        (*ts-positive-ratio* *ts-positive-rational*)
        (*ts-negative-ratio* *ts-negative-rational*)
        (*ts-complex-rational* *ts-complex-rational*)))
    (*ts-negative-integer* (ts-builder ts2
        (*ts-zero* *ts-zero*)
        (*ts-one* ts1)
        (*ts-integer>1* *ts-negative-integer*)
        (*ts-negative-integer* *ts-positive-integer*)
        (*ts-positive-ratio* *ts-negative-rational*)
        (*ts-negative-ratio* *ts-positive-rational*)
        (*ts-complex-rational* *ts-complex-rational*)))
    (*ts-positive-ratio* (ts-builder ts2
        (*ts-zero* *ts-zero*)
        (*ts-one* ts1)
        (*ts-integer>1* *ts-positive-rational*)
        (*ts-negative-integer* *ts-negative-rational*)
        (*ts-positive-ratio* *ts-positive-rational*)
        (*ts-negative-ratio* *ts-negative-rational*)
        (*ts-complex-rational* *ts-complex-rational*)))
    (*ts-negative-ratio* (ts-builder ts2
        (*ts-zero* *ts-zero*)
        (*ts-one* ts1)
        (*ts-integer>1* *ts-negative-rational*)
        (*ts-negative-integer* *ts-positive-rational*)
        (*ts-positive-ratio* *ts-negative-rational*)
        (*ts-negative-ratio* *ts-positive-rational*)
        (*ts-complex-rational* *ts-complex-rational*)))
    (*ts-complex-rational* (ts-builder ts2
        (*ts-zero* *ts-zero*)
        (*ts-one* ts1)
        (*ts-integer>1* *ts-complex-rational*)
        (*ts-negative-integer* *ts-complex-rational*)
        (*ts-positive-ratio* *ts-complex-rational*)
        (*ts-negative-ratio* *ts-complex-rational*)
        (*ts-complex-rational* (ts-intersection0 *ts-rational-acl2-number*
            (ts-complement0 *ts-zero*)))))))
type-set-binary-*-alist1function
(defun type-set-binary-*-alist1
  (i j lst)
  (cond ((< j 0) lst)
    (t (let ((x (type-set-binary-*-alist-entry i j)))
        (cond ((= x *ts-unknown*) (type-set-binary-*-alist1 i (1- j) lst))
          (t (type-set-binary-*-alist1 i
              (1- j)
              (cons (cons (cons i j) x) lst))))))))
type-set-binary-*-alistfunction
(defun type-set-binary-*-alist
  (i j lst)
  (cond ((< i 0) lst)
    (t (type-set-binary-*-alist (1- i)
        j
        (type-set-binary-*-alist1 i j lst)))))
type-set-<-alist-entryfunction
(defun type-set-<-alist-entry
  (ts1 ts2)
  (ts-builder ts1
    (*ts-zero* (ts-builder ts2
        (*ts-zero* *ts-nil*)
        (*ts-one* *ts-t*)
        (*ts-integer>1* *ts-t*)
        (*ts-negative-integer* *ts-nil*)
        (*ts-positive-ratio* *ts-t*)
        (*ts-negative-ratio* *ts-nil*)))
    (*ts-one* (ts-builder ts2
        (*ts-zero* *ts-nil*)
        (*ts-one* *ts-nil*)
        (*ts-integer>1* *ts-t*)
        (*ts-negative-integer* *ts-nil*)
        (*ts-positive-ratio* *ts-boolean*)
        (*ts-negative-ratio* *ts-nil*)))
    (*ts-integer>1* (ts-builder ts2
        (*ts-zero* *ts-nil*)
        (*ts-one* *ts-nil*)
        (*ts-integer>1* *ts-boolean*)
        (*ts-negative-integer* *ts-nil*)
        (*ts-positive-ratio* *ts-boolean*)
        (*ts-negative-ratio* *ts-nil*)))
    (*ts-negative-integer* (ts-builder ts2
        (*ts-zero* *ts-t*)
        (*ts-one* *ts-t*)
        (*ts-integer>1* *ts-t*)
        (*ts-negative-integer* *ts-boolean*)
        (*ts-positive-ratio* *ts-t*)
        (*ts-negative-ratio* *ts-boolean*)))
    (*ts-positive-ratio* (ts-builder ts2
        (*ts-zero* *ts-nil*)
        (*ts-one* *ts-boolean*)
        (*ts-integer>1* *ts-boolean*)
        (*ts-negative-integer* *ts-nil*)
        (*ts-positive-ratio* *ts-boolean*)
        (*ts-negative-ratio* *ts-nil*)))
    (*ts-negative-ratio* (ts-builder ts2
        (*ts-zero* *ts-t*)
        (*ts-one* *ts-t*)
        (*ts-integer>1* *ts-t*)
        (*ts-negative-integer* *ts-boolean*)
        (*ts-positive-ratio* *ts-t*)
        (*ts-negative-ratio* *ts-boolean*)))))
type-set-<-alist1function
(defun type-set-<-alist1
  (i j lst)
  (cond ((< j 0) lst)
    (t (let ((x (type-set-<-alist-entry i j)))
        (cond ((= x *ts-unknown*) (type-set-<-alist1 i (1- j) lst))
          (t (type-set-<-alist1 i (1- j) (cons (cons (cons i j) x) lst))))))))
type-set-<-alistfunction
(defun type-set-<-alist
  (i j lst)
  (cond ((< i 0) lst)
    (t (type-set-<-alist (1- i) j (type-set-<-alist1 i j lst)))))