Filtering...

defdata-util

books/acl2s/defdata/defdata-util
other
(in-package "DEFDATA")
other
(set-verify-guards-eagerness 2)
other
(include-book "std/util/bstar" :dir :system)
other
(include-book "acl2s/utilities" :dir :system)
str/sym-listpfunction
(defun str/sym-listp
  (x)
  (declare (xargs :guard t))
  (if (atom x)
    (null x)
    (and (or (stringp (car x)) (symbolp (car x)))
      (str/sym-listp (cdr x)))))
join-namesfunction
(defun join-names
  (xs separator)
  (declare (xargs :guard (and (str/sym-listp xs)
        (stringp separator))))
  (if (endp xs)
    ""
    (if (endp (cdr xs))
      (concatenate 'string
        (if (symbolp (car xs))
          (symbol-name (car xs))
          (car xs))
        "")
      (concatenate 'string
        (if (symbolp (car xs))
          (symbol-name (car xs))
          (car xs))
        (concatenate 'string
          separator
          (join-names (cdr xs) separator))))))
other
(defthm join-names-is-stringp
  (stringp (join-names x sep)))
other
(in-theory (disable join-names))
extract-kwd-val-fnfunction
(defun extract-kwd-val-fn
  (key args default)
  (declare (xargs :guard (and (keywordp key)
        (true-listp args))))
  (let* ((lst (member key args)) (val (and (consp lst)
          (consp (cdr lst))
          (cadr lst))))
    (or val default)))
extract-kwd-valmacro
(defmacro extract-kwd-val
  (key args &key default)
  `(extract-kwd-val-fn ,DEFDATA::KEY
    ,DEFDATA::ARGS
    ,DEFDATA::DEFAULT))
keyword-listpfunction
(defun keyword-listp
  (x)
  (declare (xargs :guard t))
  (if (atom x)
    (null x)
    (and (keywordp (car x))
      (keyword-listp (cdr x)))))
remove-keywordsfunction
(defun remove-keywords
  (keys kwd-val-list)
  (declare (xargs :guard (and (keyword-listp keys)
        (keyword-value-listp kwd-val-list))))
  (if (endp keys)
    kwd-val-list
    (remove-keywords (cdr keys)
      (remove-keyword (car keys) kwd-val-list))))
remove-keywords-from-argsfunction
(defun remove-keywords-from-args
  (keys args)
  (declare (xargs :guard (and (keyword-listp keys)
        (true-listp args))))
  (if (endp args)
    'nil
    (if (keyword-value-listp args)
      (remove-keywords keys args)
      (cons (car args)
        (remove-keywords-from-args keys
          (cdr args))))))
s+macro
(defmacro s+
  (&rest args)
  "string/symbol(s) concat to return a symbol.
  :pkg and :separator keyword args recognized."
  (let* ((sep (extract-kwd-val :separator args
         :default "")) (pkg (extract-kwd-val :pkg args))
      (args (remove-keywords-from-args '(:separator :pkg)
          args)))
    `(s+-fn (list ,@DEFDATA::ARGS)
      ,DEFDATA::SEP
      ,DEFDATA::PKG)))
s+-fnfunction
(defun s+-fn
  (ss sep pkg)
  (declare (xargs :guard (and (str/sym-listp ss)
        (stringp sep))))
  (b* (((unless (consp ss)) (er hard?
         's+
         "~| Expect at least one string/symbol arg, but given ~x0 ~%"
         ss)) (s1 (car ss))
      (pkg~ (or (and (pkgp pkg) pkg)
          (and (symbolp s1)
            (symbol-package-name s1))
          "DEFDATA")))
    (fix-intern$ (join-names ss sep)
      pkg~)))
modify-symbol-lstfunction
(defun modify-symbol-lst
  (prefix syms
    postfix
    pkg)
  (declare (xargs :guard (and (symbol-listp syms)
        (stringp prefix)
        (stringp postfix)
        (pkgp pkg))))
  (if (endp syms)
    nil
    (cons (s+ prefix
        (car syms)
        postfix
        :pkg pkg)
      (modify-symbol-lst prefix
        (cdr syms)
        postfix
        pkg))))
get-dest-prefixfunction
(defun get-dest-prefix
  (conx-name)
  (declare (xargs :guard (symbolp conx-name)))
  (concatenate 'string (symbol-name conx-name) "-"))
get-modifier-prefixfunction
(defun get-modifier-prefix
  (conx-name)
  (declare (xargs :guard (symbolp conx-name)))
  (concatenate 'string
    "SET-"
    (symbol-name conx-name)
    "-"))
other
(include-book "data-structures/utilities" :dir :system)
other
(defloop symbol-names
  (syms)
  (declare (xargs :guard (symbol-listp syms)))
  (for ((sym in syms))
    (collect (symbol-name sym))))
other
(verify-termination >=-len)
other
(verify-termination all->=-len)
strip-cadrsfunction
(defun strip-cadrs
  (x)
  (declare (xargs :guard (all->=-len x 2)))
  (cond ((endp x) nil)
    (t (cons (cadar x)
        (strip-cadrs (cdr x))))))
other
(def-const *defthm-aliases*
  '(defthm defthmd
    defthm+
    defrule
    defaxiom
    test-then-skip-proofs
    defcong
    defrefinement
    defequiv
    skip-proofs
    defthm-no-test
    defthm-test-no-proof))
other
(defloop get-event-names
  (xs)
  "get names from defthm events"
  (declare (xargs :guard (all->=-len xs 2)))
  (for ((x in xs))
    (append (and (member-eq (car x)
          *defthm-aliases*)
        (list (cadr x))))))
keywordifyfunction
(defun keywordify
  (sym)
  (declare (xargs :guard (symbolp sym)))
  (fix-intern-in-pkg-of-sym (symbol-name sym)
    :a))
acl2-getpropmacro
(defmacro acl2-getprop
  (name prop
    w
    &key
    default)
  `(getprop ,DEFDATA::NAME
    ,DEFDATA::PROP
    ,DEFDATA::DEFAULT
    'current-acl2-world
    ,DEFDATA::W))
list-up-listsfunction
(defun list-up-lists
  (l1 l2)
  (declare (xargs :guard (and (true-listp l1)
        (true-listp l2)
        (= (len l1) (len l2)))))
  "same as listlis"
  (if (endp l1)
    nil
    (cons (list (car l1) (car l2))
      (list-up-lists (cdr l1) (cdr l2)))))
other
(verify-termination legal-variable-or-constant-namep)
other
(verify-termination legal-constantp)
other
(verify-termination legal-variablep)
other
(verify-termination lambda-keywordp)
other
(verify-guards lambda-keywordp)
other
(verify-guards legal-constantp)
proper-symbolpfunction
(defun proper-symbolp
  (x)
  (declare (xargs :guard t))
  (and (symbolp x)
    (not (or (keywordp x)
        (booleanp x)
        (legal-constantp x)))))
other
(defthm keyword-list-is-symbol-list
  (implies (keyword-listp x)
    (symbol-listp x))
  :rule-classes (:forward-chaining))
other
(defthm proper-symbol-is-symbol
  (implies (proper-symbolp x)
    (symbolp x))
  :rule-classes (:compound-recognizer :forward-chaining))
other
(defthm proper-symbol-disjoint-with-keys
  (implies (keywordp x)
    (not (proper-symbolp x)))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))
other
(defthm proper-symbol-disjoint-with-bool
  (implies (booleanp x)
    (not (proper-symbolp x)))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))
other
(in-theory (disable proper-symbolp))
proper-symbol-listpfunction
(defun proper-symbol-listp
  (xs)
  (declare (xargs :guard t))
  (if (atom xs)
    (null xs)
    (and (proper-symbolp (car xs))
      (proper-symbol-listp (cdr xs)))))
other
(defthm proper-symbol-listp-is-symbol-list
  (implies (proper-symbol-listp x)
    (symbol-listp x))
  :rule-classes (:forward-chaining (:rewrite :backchain-limit-lst 1)))
other
(in-theory (disable proper-symbol-listp))
tau-predicate-pfunction
(defun tau-predicate-p
  (pred world)
  (declare (xargs :mode :program))
  (b* ((td (tau-data-fn pred world)) ((unless (consp td)) nil)
      (entry (assoc-eq 'recognizer-index (cdr td)))
      ((unless (and (consp entry) (consp (cdr entry)))) nil))
    (natp (cadr entry))))
other
(table type-metadata-table nil nil :clear)
other
(table pred-alias-table nil nil :clear)
other
(table type-alias-table nil nil :clear)
type-metadata-tablefunction
(defun type-metadata-table
  (wrld)
  "api to get the alist representing defdata type metadata table"
  (declare (xargs :guard (plist-worldp wrld)))
  (table-alist 'type-metadata-table
    wrld))
type-alias-tablefunction
(defun type-alias-table
  (wrld)
  "api to get the alist representing defdata type-alias table"
  (declare (xargs :guard (plist-worldp wrld)))
  (table-alist 'type-alias-table
    wrld))
pred-alias-tablefunction
(defun pred-alias-table
  (wrld)
  "api to get the alist representing defdata pred-alias table"
  (declare (xargs :guard (plist-worldp wrld)))
  (table-alist 'pred-alias-table
    wrld))
sym-aalist1pfunction
(defun sym-aalist1p
  (x)
  (declare (xargs :guard t))
  (if (consp x)
    (and (consp (car x))
      (symbolp (caar x))
      (symbol-alistp (cdar x))
      (sym-aalist1p (cdr x)))
    (null x)))
base-alias-typefunction
(defun base-alias-type
  (type a)
  (declare (xargs :guard (sym-aalist1p a)))
  (b* (((unless (symbolp type)) type) (atype (assoc-equal :type (get-alist type a))))
    (if (consp atype)
      (cdr atype)
      type)))
base-alias-predfunction
(defun base-alias-pred
  (pred ptbl)
  (declare (xargs :guard (sym-aalist1p ptbl)))
  (b* (((unless (symbolp pred)) pred) (ppred (assoc-equal :predicate (get-alist pred ptbl))))
    (if (consp ppred)
      (cdr ppred)
      pred)))
is-allp-aliasfunction
(defun is-allp-alias
  (p wrld)
  "is predicate P an alias of allp?"
  (declare (xargs :verify-guards nil))
  (b* ((ptbl (table-alist 'pred-alias-table
         wrld)) (p (base-alias-pred p ptbl)))
    (or (eq p 'allp)
      (assoc p
        (table-alist 'allp-aliases-table
          wrld)))))
is-topfunction
(defun is-top
  (typename wrld)
  "is typename an alias of acl2s::all?"
  (declare (xargs :verify-guards nil))
  (b* ((atbl (table-alist 'type-alias-table
         wrld)) (typename (base-alias-type typename atbl)))
    (or (eq typename 'all)
      (rassoc typename
        (table-alist 'allp-aliases-table
          wrld)))))
subtype-pfunction
(defun subtype-p
  (p1 p2 wrld)
  "Is P1 => P2 in tau-database?"
  (declare (xargs :verify-guards nil
      :guard (and (symbolp p1)
        (symbolp p2)
        (plist-worldp wrld))))
  (b* (((when (is-allp-alias p2 wrld)) t) ((when (eq p1 p2)) t)
      (p2-neg-implicants-tau (getprop p2
          'neg-implicants
          *tau-empty*
          'current-acl2-world
          wrld))
      (p2-neg-pairs (access tau p2-neg-implicants-tau :neg-pairs)))
    (rassoc-eq p1 p2-neg-pairs)))
other
(verify-termination upper-bound-<)
other
(verify-termination lower-bound->)
other
(verify-termination squeeze-k)
other
(set-verify-guards-eagerness 1)
other
(verify-termination conjoin-intervals)
other
(set-verify-guards-eagerness 2)
range-subtype-pfunction
(defun range-subtype-p
  (interval1 interval2)
  (declare (xargs :verify-guards nil))
  (equal (conjoin-intervals interval1 interval2)
    interval1))
disjoint-pfunction
(defun disjoint-p
  (p1 p2 wrld)
  "Is P1 x => (not (P2 x)) in tau-database?"
  (declare (xargs :verify-guards nil
      :guard (and (symbolp p1)
        (symbolp p2)
        (plist-worldp wrld))))
  (b* (((when (or (is-allp-alias p1 wrld)
          (is-allp-alias p2 wrld))) nil) ((when (eq p1 p2)) nil)
      (p1-pos-implicants-tau (getprop p1
          'pos-implicants
          *tau-empty*
          'current-acl2-world
          wrld))
      (p1-neg-pairs (access tau p1-pos-implicants-tau :neg-pairs)))
    (rassoc-eq p2 p1-neg-pairs)))
other
(local (defthm valid-subseq-of-string-is-string
    (implies (and (stringp pname)
        (< x (length pname))
        (< y (length pname))
        (<= x y))
      (stringp (subseq pname x y)))
    :rule-classes :type-prescription))
get-typesymbol-from-pred-p-naming-conventionfunction
(defun get-typesymbol-from-pred-p-naming-convention
  (sym)
  (declare (xargs :guard (and (symbolp sym))
      :guard-hints (("Goal" :in-theory (disable length subseq)))))
  (let* ((pred-name (symbol-name sym)) (len-predname (length pred-name)))
    (if (and (< 1 len-predname)
        (equal #\P
          (char pred-name (1- len-predname))))
      (let ((typename (subseq pred-name 0 (1- len-predname))))
        (fix-intern-in-pkg-of-sym typename
          sym))
      nil)))
make-predicate-symbolfunction
(defun make-predicate-symbol
  (sym pkg)
  (declare (xargs :guard (and (symbolp sym) (pkgp pkg))))
  (s+ sym "P" :pkg pkg))
make-predicate-symbol-lstfunction
(defun make-predicate-symbol-lst
  (syms pkg)
  (declare (xargs :guard (and (symbol-listp syms)
        (pkgp pkg))))
  (if (endp syms)
    nil
    (cons (make-predicate-symbol (car syms)
        pkg)
      (make-predicate-symbol-lst (cdr syms)
        pkg))))
make-enumerator-symbolfunction
(defun make-enumerator-symbol
  (sym pkg)
  (declare (xargs :guard (and (symbolp sym) (pkgp pkg))))
  (s+ "NTH-" sym :pkg pkg))
make-uniform-enumerator-symbolfunction
(defun make-uniform-enumerator-symbol
  (sym pkg)
  (declare (xargs :guard (and (symbolp sym) (pkgp pkg))))
  (s+ "NTH-" sym "/ACC" :pkg pkg))
optional-macro-args-allow-arityfunction
(defun optional-macro-args-allow-arity
  (margs n)
  (declare (xargs :guard (and (true-listp margs)
        (integerp n))))
  (cond ((<= n 0) t)
    ((endp margs) nil)
    ((member-eq (car margs) '(&rest &body)) t)
    ((lambda-keywordp (car margs)) nil)
    (t (optional-macro-args-allow-arity (cdr margs)
        (1- n)))))
macro-args-allow-arityfunction
(defun macro-args-allow-arity
  (margs n)
  (declare (xargs :guard (and (true-listp margs)
        (integerp n))))
  (cond ((< n 0) nil)
    ((endp margs) (= n 0))
    ((lambda-keywordp (car margs)) (cond ((eq (car margs) '&whole) (macro-args-allow-arity (cdr margs)
            (1+ n)))
        ((eq (car margs) '&optional) (optional-macro-args-allow-arity (cdr margs)
            n))
        ((member-eq (car margs) '(&rest &body)) t)
        ((member-eq (car margs)
           '(&key &allow-other-keys)) (= n 0))
        (t nil)))
    (t (macro-args-allow-arity (cdr margs)
        (1- n)))))
allows-arityfunction
(defun allows-arity
  (name n world)
  (declare (xargs :guard (and (symbolp name)
        (natp n)
        (plist-worldp world))))
  (if (function-symbolp name world)
    (= n
      (len (acl2-getprop name
          'formals
          world)))
    (let ((margs (acl2-getprop name
           'macro-args
           world
           :default :undefined)))
      (and (true-listp margs)
        (macro-args-allow-arity margs n)))))
defined-fun-or-macropfunction
(defun defined-fun-or-macrop
  (name world)
  (declare (xargs :guard (plist-worldp world)))
  (and (symbolp name)
    (or (function-symbolp name world)
      (true-listp (acl2-getprop name
          'macro-args
          world
          :default :undefined)))))
allow-arity-lstfunction
(defun allow-arity-lst
  (name-lst n world)
  (declare (xargs :guard (and (symbol-listp name-lst)
        (natp n)
        (plist-worldp world))))
  (or (endp name-lst)
    (and (allows-arity (car name-lst)
        n
        world)
      (allow-arity-lst (cdr name-lst)
        n
        world))))
plausible-predicate-functionpfunction
(defun plausible-predicate-functionp
  (name world)
  (declare (xargs :guard (and (symbolp name)
        (plist-worldp world))))
  (allows-arity name 1 world))
plausible-predicate-function-listpfunction
(defun plausible-predicate-function-listp
  (name-lst world)
  (declare (xargs :guard (and (symbol-listp name-lst)
        (plist-worldp world))))
  (or (endp name-lst)
    (and (plausible-predicate-functionp (car name-lst)
        world)
      (plausible-predicate-function-listp (cdr name-lst)
        world))))
possible-constant-value-pfunction
(defun possible-constant-value-p
  (def)
  (declare (xargs :guard t))
  (if (consp def)
    (and (eq 'quote (car def))
      (consp (cdr def))
      (null (cddr def)))
    (or (not (symbolp def))
      (keywordp def)
      (booleanp def)
      (legal-constantp def))))
put2-fnfunction
(defun put2-fn
  (nm key val al)
  (declare (xargs :guard (eqlable-alistp al)))
  (let ((lookup1 (assoc nm al)))
    (if (and (consp lookup1)
        (eqlable-alistp (cdr lookup1)))
      (put-assoc nm
        (put-assoc key
          val
          (cdr lookup1))
        al)
      al)))
get2-fnfunction
(defun get2-fn
  (nm key al default)
  (declare (xargs :guard (eqlable-alistp al)))
  (let ((lookup1 (assoc nm al)))
    (if (and (consp lookup1)
        (eqlable-alistp (cdr lookup1)))
      (let ((lookup2 (assoc key (cdr lookup1))))
        (or (and lookup2 (cdr lookup2))
          default))
      default)))
get2macro
(defmacro get2
  (name key
    al
    &optional
    default)
  `(get2-fn ,DEFDATA::NAME
    ,DEFDATA::KEY
    ,DEFDATA::AL
    ,DEFDATA::DEFAULT))
get1-fnfunction
(defun get1-fn
  (key al default)
  (declare (xargs :guard (eqlable-alistp al)))
  (let* ((lookup (assoc key al)))
    (or (and lookup (cdr lookup))
      default)))
get1macro
(defmacro get1
  (key kwd-alist &optional default)
  `(get1-fn ,DEFDATA::KEY
    ,DEFDATA::KWD-ALIST
    ,DEFDATA::DEFAULT))
other
(defloop rget2
  (key2 val2 al)
  "return the key which has alist containing key2=val2"
  (declare (xargs :verify-guards nil))
  (for ((entry in al))
    (when (eql val2
        (get1 key2 (cdr entry)))
      (return (car entry)))))
type-namefunction
(defun type-name
  (pred wrld)
  (declare (xargs :verify-guards nil))
  (b* ((m (type-metadata-table wrld)) (ptbl (table-alist 'pred-alias-table
          wrld))
      (ptype (assoc-equal :type (get-alist pred ptbl))))
    (if ptype
      (cdr ptype)
      (rget2 :predicate pred m))))
add-pre-post-hookmacro
(defmacro add-pre-post-hook
  (nm key val)
  "top-level table event. append val onto entry of key in table nm"
  `(make-event '(table ,DEFDATA::NM
      ,DEFDATA::KEY
      (union-equal (cdr (assoc ,DEFDATA::KEY
            (table-alist ',DEFDATA::NM world)))
        ,DEFDATA::VAL))))
get-allfunction
(defun get-all
  (key d)
  (declare (xargs :guard (eqlable-alistp d)))
  (if (endp d)
    'nil
    (if (eql key (caar d))
      (cons (cdar d)
        (get-all key (cdr d)))
      (get-all key (cdr d)))))
apply-mget-to-xvar-lstfunction
(defun apply-mget-to-xvar-lst
  (var fields quotep)
  (declare (xargs :guard (and (symbolp var)
        (booleanp quotep)
        (symbol-listp fields))))
  (if (endp fields)
    nil
    (let ((d-keyword-name (intern (symbol-name (car fields)) "KEYWORD")))
      (cons (list 'mget
          (if quotep
            (kwote d-keyword-name)
            d-keyword-name)
          var)
        (apply-mget-to-xvar-lst var
          (cdr fields)
          quotep)))))
find-recursive-recordsfunction
(defun find-recursive-records
  (preds new-constructors)
  (declare (xargs :guard (and (eqlable-alistp new-constructors)
        (symbol-listp preds))))
  (if (endp new-constructors)
    nil
    (b* (((cons & conx-al) (car new-constructors)) (ctx 'find-recursive-records)
        ((when (not (eqlable-alistp conx-al))) (er hard?
            ctx
            "~| ~x0 is not eqlable-alist. ~%"
            conx-al))
        (dex-pairs (get1 :dest-pred-alist conx-al))
        ((when (not (eqlable-alistp dex-pairs))) (er hard?
            ctx
            "~| ~x0 is not eqlable-alist. ~%"
            dex-pairs)))
      (if (intersection-eq preds
          (strip-cdrs dex-pairs))
        (cons (car new-constructors)
          (find-recursive-records preds
            (cdr new-constructors)))
        (find-recursive-records preds
          (cdr new-constructors))))))
runes-to-be-disabled1function
(defun runes-to-be-disabled1
  (names wrld ans)
  (declare (xargs :mode :program))
  (if (endp names)
    ans
    (b* ((name (car names)))
      (if (rule-name-designatorp name nil wrld)
        (runes-to-be-disabled1 (cdr names)
          wrld
          (cons name ans))
        (runes-to-be-disabled1 (cdr names)
          wrld
          ans)))))
runes-to-be-disabledfunction
(defun runes-to-be-disabled
  (names wrld)
  (declare (xargs :mode :program))
  (remove-duplicates-equal (runes-to-be-disabled1 names
      wrld
      'nil)))
build-one-param-callsfunction
(defun build-one-param-calls
  (fns params)
  (declare (xargs :guard (and (symbol-listp fns)
        (symbol-listp params)
        (= (len fns)
          (len params)))))
  (if (endp fns)
    nil
    (if (eq (car fns) 'allp)
      (build-one-param-calls (cdr fns)
        (cdr params))
      (cons (list (car fns) (car params))
        (build-one-param-calls (cdr fns)
          (cdr params))))))
other
(include-book "coi/symbol-fns/symbol-fns" :dir :system)
numbered-varsfunction
(defun numbered-vars
  (x k)
  (declare (xargs :guard (and (symbolp x) (natp k))))
  (reverse (item-to-numbered-symbol-list-rec x
      k)))
defdata-aliasmacro
(defmacro defdata-alias
  (alias type &rest args)
  (b* ((verbosep (let ((lst (member :verbose args)))
         (and lst (cadr lst)))) (pred (let ((lst (member :pred args)))
          (and lst (cadr lst))))
      (- (cw "~%")))
    `(with-output ,@(AND (NOT DEFDATA::VERBOSEP)
       '(:OFF :ALL :ON (DEFDATA::SUMMARY ERROR DEFDATA::COMMENT) :SUMMARY-OFF
         (:OTHER-THAN FORM TIME)))
      :gag-mode t
      :stack :push (make-event (b* ((pkg (current-package state)) (m (type-metadata-table (w state)))
            (a (type-alias-table (w state)))
            (pred (if ',DEFDATA::PRED
                ',DEFDATA::PRED
                (make-predicate-symbol ',DEFDATA::ALIAS
                  pkg)))
            (type (base-alias-type ',TYPE a))
            (type-alist (get-alist type m))
            (predicate (get-alist :predicate type-alist))
            (def (get-alist :def type-alist))
            (record? (and (consp def)
                (equal 'record (car def))))
            (base-enum (enumerator-name type a m))
            (base-enum/acc (enum/acc-name type a m))
            (alias-enum (make-symbl `(nth- ,',DEFDATA::ALIAS)
                pkg))
            (alias-enum-acc (make-symbl `(,DEFDATA::ALIAS-ENUM /acc)
                pkg))
            (x (fix-intern$ "X" pkg))
            (seed (fix-intern$ "SEED" pkg))
            ((unless predicate) (er hard
                'defdata-alias
                "~%**Unknown type**: ~x0 is not a known type name.~%"
                ',TYPE))
            ((when record?) (er hard
                'defdata-alias
                "~%**Record type**: ~x0 is a record and records cannot be aliased.~%"
                ',TYPE)))
          `(encapsulate nil
            (table type-alias-table
              ',',DEFDATA::ALIAS
              '((:pred . ,DEFDATA::PRED) (:type . ,TYPE)
                (:predicate . ,DEFDATA::PREDICATE))
              :put)
            (table pred-alias-table
              ',DEFDATA::PRED
              '((:alias . ,',DEFDATA::ALIAS) (:type . ,TYPE)
                (:predicate . ,DEFDATA::PREDICATE))
              :put)
            (defmacro ,DEFDATA::PRED
              (,DEFDATA::X)
              `(,',DEFDATA::PREDICATE ,,DEFDATA::X))
            (defmacro ,DEFDATA::ALIAS-ENUM
              (,DEFDATA::X)
              `(,',DEFDATA::BASE-ENUM ,,DEFDATA::X))
            (defmacro ,DEFDATA::ALIAS-ENUM-ACC
              (,DEFDATA::X ,DEFDATA::SEED)
              `(,',DEFDATA::BASE-ENUM/ACC ,,DEFDATA::X ,,DEFDATA::SEED))
            (add-macro-alias ,DEFDATA::PRED
              ,DEFDATA::PREDICATE)))))))
predicate-namemacro
(defmacro predicate-name
  (tname &optional a m)
  (if (and a m)
    `(get2 (base-alias-type ,DEFDATA::TNAME ,DEFDATA::A)
      :predicate ,DEFDATA::M)
    `(get2 (base-alias-type ,DEFDATA::TNAME
        (type-alias-table wrld))
      :predicate (type-metadata-table wrld))))
enumerator-namemacro
(defmacro enumerator-name
  (tname &optional a m)
  (if (and a m)
    `(get1 :enumerator (get1 (base-alias-type ,DEFDATA::TNAME ,DEFDATA::A)
        ,DEFDATA::M))
    `(get1 :enumerator (get1 (base-alias-type ,DEFDATA::TNAME
          (type-alias-table wrld))
        (type-metadata-table wrld)))))
enum/acc-namemacro
(defmacro enum/acc-name
  (tname &optional a m)
  (if (and a m)
    `(get1 :enum/acc (get1 (base-alias-type ,DEFDATA::TNAME ,DEFDATA::A)
        ,DEFDATA::M))
    `(get1 :enum/acc (get1 (base-alias-type ,DEFDATA::TNAME
          (type-alias-table wrld))
        (type-metadata-table wrld)))))
other
(defloop predicate-names-fn
  (tnames a m)
  (declare (xargs :guard (and (symbol-listp tnames)
        (sym-aalist1p a)
        (sym-aalist1p m))))
  (for ((tname in tnames))
    (collect (predicate-name tname
        a
        m))))
predicate-namesmacro
(defmacro predicate-names
  (tnames &optional a m)
  (if (and a m)
    `(predicate-names-fn ,DEFDATA::TNAMES
      ,DEFDATA::A
      ,DEFDATA::M)
    `(predicate-names-fn ,DEFDATA::TNAMES
      (type-alias-table wrld)
      (type-metadata-table wrld))))
other
(defloop possible-constant-values-p
  (xs)
  (for ((x in xs))
    (always (possible-constant-value-p x))))
other
(mutual-recursion (defun texp-constituent-types1
    (texp tnames
      wrld
      include-recursive-references-p)
    (declare (xargs :verify-guards nil))
    (cond ((possible-constant-value-p texp) nil)
      ((proper-symbolp texp) (cond ((member texp tnames) (and include-recursive-references-p
              (list texp)))
          ((predicate-name texp) (list texp))
          (t nil)))
      ((atom texp) nil)
      ((not (true-listp texp)) (texp-constituent-types1 (cdr texp)
          tnames
          wrld
          include-recursive-references-p))
      (t (texp-constituent-types1-lst (cdr texp)
          tnames
          wrld
          include-recursive-references-p))))
  (defun texp-constituent-types1-lst
    (texps tnames
      wrld
      include-recursive-references-p)
    (if (atom texps)
      nil
      (append (texp-constituent-types1 (car texps)
          tnames
          wrld
          include-recursive-references-p)
        (texp-constituent-types1-lst (cdr texps)
          tnames
          wrld
          include-recursive-references-p)))))
texp-constituent-typesmacro
(defmacro texp-constituent-types
  (texp tnames
    wrld
    &key
    include-recursive-references-p)
  `(texp-constituent-types1 ,DEFDATA::TEXP
    ,DEFDATA::TNAMES
    ,DEFDATA::WRLD
    ,DEFDATA::INCLUDE-RECURSIVE-REFERENCES-P))
is-recursive-type-expfunction
(defun is-recursive-type-exp
  (texp tnames wrld)
  (declare (xargs :verify-guards nil))
  (intersection-eq tnames
    (texp-constituent-types texp
      tnames
      wrld
      :include-recursive-references-p t)))
recursive-type-pfunction
(defun recursive-type-p
  (type-name wrld)
  (declare (xargs :verify-guards nil))
  (b* ((table (type-metadata-table wrld)) (type-name (base-alias-type type-name
          (type-alias-table wrld)))
      (norm-def (get2 type-name
          :normalized-def table))
      (clique-names (get2 type-name :clique table)))
    (is-recursive-type-exp norm-def
      clique-names
      wrld)))
constituent-types1function
(defun constituent-types1
  (p wrld)
  (declare (xargs :verify-guards nil))
  (b* (((cons & a) p) ((assocs ndef new-types) a)
      (tnames (strip-cars new-types)))
    (texp-constituent-types ndef
      tnames
      wrld)))
other
(defloop constituent-types
  (ps wrld)
  (declare (xargs :verify-guards nil))
  (for ((p in ps))
    (append (constituent-types1 p wrld))))
named-defdata-exp-pfunction
(defun named-defdata-exp-p
  (texp)
  "is it named, i.e of form (name . typename)"
  (and (not (possible-constant-value-p texp))
    (consp texp)
    (not (true-listp texp))
    (proper-symbolp (cdr texp))))
bind-names-vals1function
(defun bind-names-vals1
  (texp val)
  (and (named-defdata-exp-p texp)
    (list (list (car texp) val))))
other
(defloop bind-names-vals
  (texps vals)
  "let binding for each name decl texp -> corresponding val"
  (for ((texp in texps) (val in vals))
    (append (bind-names-vals1 texp val))))
other
(defloop replace-calls-with-names
  (calls texps)
  "calls and texps are 1-1.
   return calls but if the corresponding texp is named, replace the call with the name"
  (for ((texp in texps) (call in calls))
    (collect (if (named-defdata-exp-p texp)
        (car texp)
        call))))
to-string1function
(defun to-string1
  (xstr alst)
  (declare (xargs :mode :program))
  (b* (((mv & str) (fmt1!-to-string xstr alst 0)))
    str))
other
(defttag :ev-fncall-w-ok)
other
(remove-untouchable ev-fncall-w t)
other
(defttag nil)
funcall-wfunction
(defun funcall-w
  (fn args ctx w)
  (declare (xargs :mode :program))
  (b* (((mv erp result) (ev-fncall-w fn
         args
         w
         nil
         nil
         t
         nil
         t)) ((when erp) (er hard?
          ctx
          "~s0"
          (to-string1 (car result)
            (cdr result)))))
    result))
other
(push-untouchable ev-fncall-w t)
other
(mutual-recursion (defun expand-lambda
    (term)
    (declare (xargs :verify-guards nil
        :guard (pseudo-termp term)))
    (cond ((variablep term) term)
      ((fquotep term) term)
      ((eq (ffn-symb term) 'hide) term)
      (t (let* ((expanded-args (expand-lambda-lst (fargs term))) (fn (ffn-symb term)))
          (cond ((flambdap fn) (subcor-var (lambda-formals fn)
                expanded-args
                (expand-lambda (lambda-body fn))))
            (t (cons-term fn expanded-args)))))))
  (defun expand-lambda-lst
    (term-lst)
    (declare (xargs :guard (pseudo-term-listp term-lst)))
    (cond ((endp term-lst) 'nil)
      (t (cons (expand-lambda (car term-lst))
          (expand-lambda-lst (cdr term-lst)))))))
separate-kwd-argsfunction
(defun separate-kwd-args
  (args defs-ans)
  (declare (xargs :guard (true-listp defs-ans)))
  (if (atom args)
    (mv defs-ans nil)
    (if (keyword-value-listp args)
      (mv defs-ans args)
      (separate-kwd-args (cdr args)
        (append defs-ans (list (car args)))))))
make-numlist-fromfunction
(defun make-numlist-from
  (curr size)
  (declare (xargs :guard (and (natp curr)
        (natp size))))
  (if (zp size)
    'nil
    (cons curr
      (make-numlist-from (1+ curr)
        (1- size)))))
other
(mutual-recursion (defun keep-names
    (texp)
    (cond ((atom texp) texp)
      ((possible-constant-value-p texp) texp)
      ((not (true-listp texp)) (car texp))
      (t (cons (car texp)
          (keep-names-lst (cdr texp))))))
  (defun keep-names-lst
    (texps)
    "collect names from all named texps"
    (if (atom texps)
      nil
      (cons (keep-names (car texps))
        (keep-names-lst (cdr texps))))))
other
(mutual-recursion (defun remove-names
    (texp)
    (cond ((atom texp) texp)
      ((possible-constant-value-p texp) texp)
      ((not (true-listp texp)) (cdr texp))
      (t (cons (car texp)
          (remove-names-lst (cdr texp))))))
  (defun remove-names-lst
    (texps)
    "remove names from all named texps"
    (if (atom texps)
      nil
      (cons (remove-names (car texps))
        (remove-names-lst (cdr texps))))))
commentarymacro
(defmacro commentary
  (yes &rest args)
  `(value-triple (prog2$ (cw? ,DEFDATA::YES ,@DEFDATA::ARGS)
      :invisible)))
other
(defloop pair-prefix
  (prefix xs)
  (declare (xargs :guard (true-listp xs)))
  (for ((x in xs))
    (collect (cons prefix x))))
extract-keywordsfunction
(defun extract-keywords
  (ctx legal-kwds
    args
    kwd-alist
    ok-dup-kwds)
  "Returns (mv kwd-alist other-args)"
  (declare (xargs :guard (and (symbol-listp legal-kwds)
        (no-duplicatesp legal-kwds)
        (alistp kwd-alist)
        (symbol-listp ok-dup-kwds))))
  (b* (((when (atom args)) (mv (revappend kwd-alist nil)
         args)) (arg1 (first args))
      ((unless (keywordp arg1)) (b* (((mv kwd-alist other-args) (extract-keywords ctx
               legal-kwds
               (cdr args)
               kwd-alist
               ok-dup-kwds)))
          (mv kwd-alist
            (cons arg1 other-args))))
      ((unless (member arg1 legal-kwds)) (er hard?
          ctx
          (concatenate 'string
            "~x0: invalid keyword ~x1."
            (if legal-kwds
              "  Valid keywords: ~&2."
              "  No keywords are valid here."))
          ctx
          arg1
          legal-kwds)
        (mv nil nil))
      ((when (atom (rest args))) (er hard?
          ctx
          "~x0: keyword ~x1 has no argument."
          ctx
          arg1)
        (mv nil nil))
      ((when (and (not (member-equal arg1 ok-dup-kwds))
           (assoc arg1 kwd-alist))) (er hard?
          ctx
          "~x0: multiple occurrences of keyword ~x1."
          ctx
          arg1)
        (mv nil nil))
      (value (second args))
      (kwd-alist (acons arg1 value kwd-alist)))
    (extract-keywords ctx
      legal-kwds
      (cddr args)
      kwd-alist
      ok-dup-kwds)))
other
(defstub is-type-predicate
  (* *)
  =>
  *)
other
(defstub is-a-typename
  (* *)
  =>
  *)
other
(defstub forbidden-names
  nil
  =>
  *)
forbidden-names-builtinfunction
(defun forbidden-names-builtin
  nil
  '(x x x))
other
(defattach forbidden-names
  forbidden-names-builtin)
remove1-assoc-allfunction
(defun remove1-assoc-all
  (key alst)
  "delete from alst all entries with key"
  (declare (xargs :guard (alistp alst)))
  (if (endp alst)
    'nil
    (if (equal key (caar alst))
      (remove1-assoc-all key
        (cdr alst))
      (cons (car alst)
        (remove1-assoc-all key
          (cdr alst))))))
union-alist2function
(defun union-alist2
  (al1 al2)
  "union ke-val entries of al1 with al2, with al1 entries taking preference."
  (declare (xargs :guard (and (alistp al1)
        (alistp al2))))
  (if (endp al1)
    al2
    (cons (car al1)
      (union-alist2 (cdr al1)
        (remove1-assoc-all (caar al1)
          al2)))))
alist-equivfunction
(defun alist-equiv
  (a1 a2)
  (declare (xargs :guard (and (alistp a1)
        (alistp a2))))
  (if (endp a1)
    (endp a2)
    (b* ((key (caar a1)))
      (and (equal (assoc-equal key a1)
          (assoc-equal key a2))
        (alist-equiv (remove1-assoc-all key a1)
          (remove1-assoc-all key a2))))))
other
(defloop collect-declares
  (xs)
  (for ((x in xs))
    (append (and (consp x)
        (equal 'declare (car x))
        (true-listp x)
        (cdr x)))))
extract-guard-from-edeclsfunction
(defun extract-guard-from-edecls
  (edecls)
  "edecls is list of forms which can occur inside a declare form i.e. the di in (declare d1 ... dn)"
  (declare (xargs :guard (true-listp edecls)))
  (if (endp edecls)
    t
    (if (and (consp (car edecls))
        (eq (caar edecls) 'xargs)
        (keyword-value-listp (cdar edecls))
        (assoc-keyword :guard (cdar edecls)))
      (or (cadr (assoc-keyword :guard (cdar edecls)))
        't)
      (extract-guard-from-edecls (cdr edecls)))))
convert-listpairs-to-conspairsfunction
(defun convert-listpairs-to-conspairs
  (listpairs)
  (declare (xargs :guard (symbol-doublet-listp listpairs)))
  (if (endp listpairs)
    nil
    (cons (let* ((lstpair (car listpairs)) (fst (car lstpair))
          (snd (cadr lstpair)))
        (cons fst snd))
      (convert-listpairs-to-conspairs (cdr listpairs)))))
convert-conspairs-to-listpairsfunction
(defun convert-conspairs-to-listpairs
  (conspairs)
  (declare (xargs :guard (symbol-alistp conspairs)))
  (if (endp conspairs)
    nil
    (cons (let* ((conspair (car conspairs)) (fst (car conspair))
          (snd (cdr conspair)))
        (list fst snd))
      (convert-conspairs-to-listpairs (cdr conspairs)))))
get-tau-intfunction
(defun get-tau-int
  (domain rexp)
  (declare (xargs :verify-guards t))
  (let ((dom (if (eq domain 'integer)
         'integerp
         'rationalp)))
    (case-match rexp
      ((lo lo-rel-sym
         '_
         hi-rel-sym
         hi) (b* ((lo-rel (eq lo-rel-sym '<)) (hi-rel (eq hi-rel-sym '<))
            (lo (and (rationalp lo) lo))
            (hi (and (rationalp hi) hi)))
          (make-tau-interval dom
            lo-rel
            lo
            hi-rel
            hi))))))
other
(defloop flatten-ands
  (terms)
  (declare (xargs :guard (pseudo-term-listp terms)))
  (for ((term in terms))
    (append (if (and (consp term) (eq (car term) 'and))
        (cdr term)
        (list term)))))
other
(mutual-recursion (defun get-vars1
    (term ans)
    (declare (xargs :verify-guards nil
        :guard (proper-symbol-listp ans)))
    (cond ((atom term) (if (proper-symbolp term)
          (add-to-set-eq term ans)
          ans))
      ((equal (car term) 'quote) ans)
      (t (get-vars1-lst (cdr term) ans))))
  (defun get-vars1-lst
    (terms ans)
    (declare (xargs :verify-guards nil
        :guard (and (true-listp terms)
          (proper-symbol-listp ans))))
    (if (endp terms)
      ans
      (get-vars1-lst (cdr terms)
        (get-vars1 (car terms) ans)))))
get-varsfunction
(defun get-vars
  (term)
  (declare (xargs :verify-guards nil))
  (get-vars1 term 'nil))
filter-terms-with-varsfunction
(defun filter-terms-with-vars
  (terms vars)
  (declare (xargs :verify-guards nil
      :guard (and (pseudo-term-listp terms)
        (proper-symbol-listp vars))))
  (if (endp terms)
    'nil
    (if (subsetp-equal (get-vars (car terms))
        vars)
      (cons (car terms)
        (filter-terms-with-vars (cdr terms)
          vars))
      (filter-terms-with-vars (cdr terms)
        vars))))
other
(defloop var-or-quoted-listp
  (xs)
  (declare (xargs :guard (true-listp xs)))
  (for ((x in xs))
    (always (or (proper-symbolp x)
        (rquotep x)))))