Filtering...

defdata-core

books/acl2s/defdata/defdata-core
other
(in-package "DEFDATA")
other
(include-book "acl2s/cgen/acl2s-parameter" :dir :system)
other
(include-book "data-structures/utilities" :dir :system)
other
(include-book "coi/symbol-fns/symbol-fns" :dir :system)
other
(include-book "tools/templates" :dir :system)
other
(include-book "defdata-util")
other
(include-book "builtin-combinators")
other
(program)
other
(set-state-ok t)
apply-mget-to-var-lstfunction
(defun apply-mget-to-var-lst
  (fields xvar)
  (if (endp fields)
    nil
    (let ((d-keyword-name (intern (symbol-name (car fields)) "KEYWORD")))
      (cons (list 'mget d-keyword-name xvar)
        (apply-mget-to-var-lst (cdr fields)
          xvar)))))
tag=macro
(defmacro tag=
  (x tag)
  `(and (consp ,DEFDATA::X)
    (equal (mget :0tag ,DEFDATA::X) ,DEFDATA::TAG)))
make-pred-i...macro
(defmacro make-pred-i...
  (s x)
  `(make-pred-i ,DEFDATA::S
    ,DEFDATA::X
    kwd-alist
    a
    m
    c
    b
    wrld))
make-pred-is...macro
(defmacro make-pred-is...
  (ss xs)
  `(make-pred-is ,DEFDATA::SS
    ,DEFDATA::XS
    kwd-alist
    a
    m
    c
    b
    wrld))
other
(mutual-recursion (defun make-pred-i
    (s x
      kwd-alist
      a
      m
      c
      b
      wrld)
    "predicate interpretation/expression for core defdata exp s.
x is the name of the expr that currently names the argument under question/predication
kwd-alist gives some defaults.
M is type metadata table + some basic info for the clique of types being defined.
C is the constructor table + some basic info for new constructors.
B is the builtin combinator table."
    (cond ((possible-constant-value-p s) `(equal ,DEFDATA::X ,DEFDATA::S))
      ((proper-symbolp s) (if (assoc-eq s m)
          `(,(DEFDATA::PREDICATE-NAME DEFDATA::S DEFDATA::A DEFDATA::M) ,DEFDATA::X)
          `(equal ,DEFDATA::X ,DEFDATA::S)))
      ((not (true-listp s)) (make-pred-i... (cdr s) x))
      ((assoc-eq (car s) b) (b* ((pred-i-fn (get2 (car s) :pred-i b)))
          (if pred-i-fn
            (funcall-w pred-i-fn
              (list x s)
              'make-pred-i
              wrld)
            `(,(CAR DEFDATA::S) . ,(DEFDATA::MAKE-PRED-IS... (CDR DEFDATA::S)
  (MAKE-LIST (DEFDATA::LEN (CDR DEFDATA::S)) :INITIAL-ELEMENT DEFDATA::X))))))
      ((assoc-eq (car s) c) (b* ((conx (car s)) ((mv recog dest-pred-alist) (mv (get2 conx :recog c)
                (get2 conx :dest-pred-alist c)))
            (dest-calls (list-up-lists (strip-cars dest-pred-alist)
                (make-list (len (cdr s))
                  :initial-element x)))
            (field-pred-alist (get2 conx :field-pred-alist c))
            (mget-dex-calls (and field-pred-alist
                (apply-mget-to-var-lst (strip-cars field-pred-alist)
                  x)))
            (dest-calls (or (and (get1 :recp kwd-alist)
                  mget-dex-calls)
                dest-calls))
            (binding (bind-names-vals (cdr s)
                dest-calls))
            (call-exprs (replace-calls-with-names dest-calls
                (cdr s)))
            (rst (make-pred-is... (cdr s)
                call-exprs))
            (recog-calls (list (list recog x))))
          (if binding
            `(and ,@DEFDATA::RECOG-CALLS
              (let ,DEFDATA::BINDING
                (and . ,DEFDATA::RST)))
            `(and ,@DEFDATA::RECOG-CALLS ,@DEFDATA::RST))))
      (t `(,(CAR DEFDATA::S) . ,(DEFDATA::MAKE-PRED-IS... (CDR DEFDATA::S)
  (MAKE-LIST (DEFDATA::LEN (CDR DEFDATA::S)) :INITIAL-ELEMENT DEFDATA::X))))))
  (defun make-pred-is
    (texps xs
      kwd-alist
      a
      m
      c
      b
      wrld)
    (if (endp texps)
      'nil
      (cons (make-pred-i... (car texps)
          (car xs))
        (make-pred-is... (cdr texps)
          (cdr xs))))))
make-pred-declare-formsfunction
(defun make-pred-declare-forms
  (xvar kwd-alist)
  (b* ((guard-lambda (get1 :pred-guard kwd-alist)) (actuals (list xvar)))
    (if guard-lambda
      `((declare (xargs :guard ,(DEFDATA::EXPAND-LAMBDA (CONS DEFDATA::GUARD-LAMBDA DEFDATA::ACTUALS)))))
      'nil)))
other
(defloop funcalls-append
  (fs args wrld)
  (for ((f in fs))
    (append (funcall-w f
        args
        'defdata-events
        wrld))))
pred-eventfunction
(defun pred-event
  (p top-kwd-alist wrld)
  "make a predicate defun event."
  (b* (((cons name a) p) (curr-pkg (get1 :current-package top-kwd-alist))
      (pred-name (make-predicate-symbol name
          curr-pkg))
      ((when (allows-arity pred-name 1 wrld)) nil)
      ((assocs ndef
         ?n
         new-constructors
         new-types
         kwd-alist) a)
      (recp (get1 :recp kwd-alist))
      ((when (and new-constructors (not recp))) nil)
      (m (append new-types
          (table-alist 'type-metadata-table
            wrld)))
      (a (table-alist 'type-alias-table
          wrld))
      (c (append new-constructors
          (table-alist 'data-constructor-table
            wrld)))
      (b (table-alist 'builtin-combinator-table
          wrld))
      (kwd-alist (append kwd-alist top-kwd-alist))
      (pkg (get1 :current-package kwd-alist))
      (d (fix-intern$ "D" pkg))
      (avoid-lst (append (forbidden-names)
          (strip-cars n)))
      (xvar (if (member-eq d avoid-lst)
          d
          (generate-variable d
            avoid-lst
            nil
            nil
            wrld)))
      (pred-body (make-pred-i ndef
          xvar
          kwd-alist
          a
          m
          c
          b
          wrld))
      (pred-decls (make-pred-declare-forms xvar
          kwd-alist))
      (pred-name (predicate-name name
          a
          m))
      (def (if (and (not recp)
            (get1 :disable-non-recursive-p kwd-alist))
          'defund
          'defun)))
    `((,DEFDATA::DEF ,DEFDATA::PRED-NAME
       (,DEFDATA::XVAR)
       ,@DEFDATA::PRED-DECLS
       ,DEFDATA::PRED-BODY))))
other
(defloop pred-events
  (ps kwd-alist wrld)
  (for ((p in ps))
    (append (pred-event p
        kwd-alist
        wrld))))
already-defined-pred-defthm-eventfunction
(defun already-defined-pred-defthm-event
  (p top-kwd-alist wrld)
  (b* (((cons name a) p) (curr-pkg (get1 :current-package top-kwd-alist))
      (pred-name (make-predicate-symbol name
          curr-pkg))
      ((unless (allows-arity pred-name 1 wrld)) nil)
      ((assocs ndef
         ?n
         new-types
         kwd-alist) a)
      (c (table-alist 'data-constructor-table
          wrld))
      (m (append new-types
          (table-alist 'type-metadata-table
            wrld)))
      (a (table-alist 'type-alias-table
          wrld))
      (b (table-alist 'builtin-combinator-table
          wrld))
      (kwd-alist (append kwd-alist top-kwd-alist))
      (avoid-lst (append (forbidden-names)
          (strip-cars n)))
      (d (fix-intern$ "D" curr-pkg))
      (xvar (if (member-eq d avoid-lst)
          d
          (generate-variable d
            avoid-lst
            nil
            nil
            wrld)))
      (pred-body (make-pred-i ndef
          xvar
          kwd-alist
          a
          m
          c
          b
          wrld))
      (defthm-body `(equal (,DEFDATA::PRED-NAME ,DEFDATA::XVAR)
          ,DEFDATA::PRED-BODY))
      (defthm-name (s+ name
          "P-TESTTHM"
          :pkg curr-pkg)))
    `((defthm ,DEFDATA::DEFTHM-NAME
       ,DEFDATA::DEFTHM-BODY
       :rule-classes nil
       :hints ,(DEFDATA::GET1 :HINTS DEFDATA::KWD-ALIST)) (verify-guards ,DEFDATA::DEFTHM-NAME))))
other
(defloop already-defined-pred-defthm-events
  (ps kwd-alist wrld)
  (for ((p in ps))
    (append (already-defined-pred-defthm-event p
        kwd-alist
        wrld))))
predicate-events1function
(defun predicate-events1
  (d kwd-alist wrld)
  (b* ((already-defined-pred-defthm-events (already-defined-pred-defthm-events d
         kwd-alist
         wrld)) (pred-events (append (pred-events d
            kwd-alist
            wrld)
          (funcalls-append (get1 :in-pred-hook-fns kwd-alist)
            (list d kwd-alist wrld)
            wrld))))
    (if (and (consp pred-events)
        (consp (cdr pred-events)))
      `((mutual-recursion ,@DEFDATA::PRED-EVENTS))
      (append already-defined-pred-defthm-events
        pred-events))))
collect-keyword-evfunction
(defun collect-keyword-ev
  (p key)
  (b* (((cons & a) p) ((assocs kwd-alist) a)
      (all-ev (get1 key kwd-alist)))
    all-ev))
other
(defloop collect-events1
  (ps key)
  (for ((p in ps))
    (append (collect-keyword-ev p key))))
collect-eventsfunction
(defun collect-events
  (key d kwd-alist)
  (append (get1 key kwd-alist)
    (collect-events1 d key)))
pred-rule-disablepfunction
(defun pred-rule-disablep
  (rule)
  (b* (((unless (eq (access rewrite-rule rule :subclass)
          'abbreviation)) t) ((when (symbolp (cadr (access rewrite-rule rule :lhs)))) t)
      ((unless (equal (access rewrite-rule rule :rhs) ''t)) t))
    nil))
collect-pred-runes-to-disablefunction
(defun collect-pred-runes-to-disable
  (rules)
  (if (atom rules)
    nil
    (if (pred-rule-disablep (car rules))
      (cons (access rewrite-rule (car rules) :rune)
        (collect-pred-runes-to-disable (cdr rules)))
      (collect-pred-runes-to-disable (cdr rules)))))
other
(defloop collect-disable-runes-preds
  (preds wrld)
  (for ((pred in preds))
    (append (collect-pred-runes-to-disable (acl2-getprop pred 'lemmas wrld)))))
collect-keyword-evfunction
(defun collect-keyword-ev
  (p key)
  (b* (((cons & a) p) ((assocs kwd-alist) a)
      (all-ev (get1 key kwd-alist)))
    all-ev))
predicate-eventsfunction
(defun predicate-events
  (d kwd-alist wrld)
  (b* ((disable-rules (collect-disable-runes-preds (predicate-names (constituent-types d wrld))
         wrld)))
    `(,@(DEFDATA::FUNCALLS-APPEND
   (DEFDATA::GET1 :PRE-PRED-HOOK-FNS DEFDATA::KWD-ALIST)
   (LIST DEFDATA::D DEFDATA::KWD-ALIST DEFDATA::WRLD) DEFDATA::WRLD) ,@(DEFDATA::COLLECT-EVENTS :PRE-PRED-EVENTS DEFDATA::D DEFDATA::KWD-ALIST)
      (commentary ,(DEFDATA::GET1 :PRINT-COMMENTARY DEFDATA::KWD-ALIST)
        "~| Predicate events...~%")
      ,@(DEFDATA::PREDICATE-EVENTS1 DEFDATA::D DEFDATA::KWD-ALIST DEFDATA::WRLD)
      (local (in-theory (disable* . ,DEFDATA::DISABLE-RULES)))
      (local (in-theory (enable ,@(DEFDATA::MAKE-PREDICATE-SYMBOL-LST (DEFDATA::STRIP-CARS DEFDATA::D)
   (DEFDATA::GET1 :CURRENT-PACKAGE DEFDATA::KWD-ALIST)))))
      ,@(DEFDATA::COLLECT-EVENTS :POST-PRED-EVENTS DEFDATA::D DEFDATA::KWD-ALIST)
      ,@(DEFDATA::FUNCALLS-APPEND
   (DEFDATA::GET1 :POST-PRED-HOOK-FNS DEFDATA::KWD-ALIST)
   (LIST DEFDATA::D DEFDATA::KWD-ALIST DEFDATA::WRLD) DEFDATA::WRLD))))
register-type-eventfunction
(defun register-type-event
  (p top-kwd-alist wrld)
  (declare (ignorable top-kwd-alist))
  (b* (((cons name a) p) ((assocs ndef
         odef
         pdef
         new-types
         kwd-alist) a)
      (m (append new-types
          (table-alist 'type-metadata-table
            wrld)))
      (at (table-alist 'type-alias-table
          wrld))
      (?kwd-alist (append kwd-alist top-kwd-alist)))
    `(register-type ,DEFDATA::NAME
      :predicate ,(DEFDATA::PREDICATE-NAME DEFDATA::NAME DEFDATA::AT DEFDATA::M)
      :enumerator ,(DEFDATA::ENUMERATOR-NAME DEFDATA::NAME DEFDATA::AT DEFDATA::M)
      :enum/acc ,(DEFDATA::GET2 DEFDATA::NAME :ENUM/ACC DEFDATA::M)
      :clique ,(DEFDATA::STRIP-CARS DEFDATA::NEW-TYPES)
      :theory-name ,(DEFDATA::GET1 :THEORY-NAME DEFDATA::KWD-ALIST)
      :def ,DEFDATA::ODEF
      :normalized-def ,DEFDATA::NDEF
      :prettyified-def ,DEFDATA::PDEF
      :min-rec-depth ,(DEFDATA::GET1 :MIN-REC-DEPTH DEFDATA::KWD-ALIST)
      :max-rec-depth ,(DEFDATA::GET1 :MAX-REC-DEPTH DEFDATA::KWD-ALIST)
      :recp ,(DEFDATA::GET1 :RECP DEFDATA::KWD-ALIST)
      :satisfies ,(DEFDATA::GET1 :SATISFIES DEFDATA::KWD-ALIST)
      :satisfies-fixer ,(DEFDATA::GET1 :SATISFIES-FIXER DEFDATA::KWD-ALIST))))
other
(defloop register-type-events1
  (ps kwd-alist wrld)
  (for ((p in ps))
    (collect (register-type-event p
        kwd-alist
        wrld))))
register-type-eventsfunction
(defun register-type-events
  (ps kwd-alist wrld)
  (cons `(commentary ,(DEFDATA::GET1 :PRINT-COMMENTARY DEFDATA::KWD-ALIST)
      "~| Registering type...~%")
    (register-type-events1 ps
      kwd-alist
      wrld)))
defdata-core-eventsfunction
(defun defdata-core-events
  (a1 wrld)
  (b* (((list d kwd-alist) a1))
    `(with-output :on (summary error comment)
      :off (prove event observation)
      :summary-off (:other-than form time)
      (progn ,@(DEFDATA::COLLECT-EVENTS :PRE-EVENTS DEFDATA::D DEFDATA::KWD-ALIST)
        ,@(DEFDATA::FUNCALLS-APPEND (DEFDATA::GET1 :PRE-HOOK-FNS DEFDATA::KWD-ALIST)
   (LIST DEFDATA::D DEFDATA::KWD-ALIST DEFDATA::WRLD) DEFDATA::WRLD)
        (encapsulate nil
          (logic)
          (with-output :summary-off (:other-than form)
            :on (error)
            (progn (set-bogus-defun-hints-ok t)
              (set-ignore-ok t)
              (set-irrelevant-formals-ok t)
              ,@(DEFDATA::PREDICATE-EVENTS DEFDATA::D DEFDATA::KWD-ALIST DEFDATA::WRLD)
              ,@(DEFDATA::FUNCALLS-APPEND (DEFDATA::GET1 :CGEN-HOOK-FNS DEFDATA::KWD-ALIST)
   (LIST DEFDATA::D DEFDATA::KWD-ALIST DEFDATA::WRLD) DEFDATA::WRLD))))
        ,@(DEFDATA::REGISTER-TYPE-EVENTS DEFDATA::D DEFDATA::KWD-ALIST DEFDATA::WRLD)
        ,@(DEFDATA::FUNCALLS-APPEND (DEFDATA::GET1 :POST-HOOK-FNS DEFDATA::KWD-ALIST)
   (LIST DEFDATA::D DEFDATA::KWD-ALIST DEFDATA::WRLD) DEFDATA::WRLD)
        ,@(DEFDATA::COLLECT-EVENTS :POST-EVENTS DEFDATA::D DEFDATA::KWD-ALIST)))))
other
(logic)
substitute-symfunction
(defun substitute-sym
  (new old form)
  (declare (xargs :guard (symbolp old)))
  (cond ((symbolp form) (cond ((eq form old) new)
        (t form)))
    ((atom form) form)
    ((quotep form) form)
    (t (cons (substitute-sym new
          old
          (car form))
        (substitute-sym new
          old
          (cdr form))))))
match-alistfunction
(defun match-alist
  (name key val a)
  (declare (xargs :guard (and (symbolp name)
        (eqlable-2-alistp a))))
  (if (endp a)
    nil
    (b* ((lookup (assoc key (cdar a))) ((unless lookup) (match-alist name
            key
            val
            (cdr a)))
        (aval (cdr lookup))
        (aname (caar a))
        (nval (if (symbolp aname)
            (substitute-sym aname
              name
              val)
            val)))
      (if (equal aval nval)
        aname
        (match-alist name
          key
          val
          (cdr a))))))
other
(program)
defdata-eventsfunction
(defun defdata-events
  (a1 wrld)
  (b* (((list d kwd-alist) a1) (d-alist (cdar d))
      (name (get1 'name d-alist))
      (odef (get1 'odef (cdar d)))
      (pdef (get1 'pdef (cdar d)))
      (ndef (get1 'ndef (cdar d)))
      (record? (and (consp odef)
          (equal 'record (car odef))))
      (global-alias-off? (not (get-acl2s-defaults :defdata-aliasing-enabled wrld)))
      (do-not-alias? (or record?
          global-alias-off?
          (get1 :do-not-alias kwd-alist)))
      (m (type-metadata-table wrld))
      (match-def (match-alist name
          :def odef
          m))
      (match-def (or match-def
          (match-alist name
            :prettyified-def pdef
            m)))
      (match-def (or match-def
          (match-alist name
            :normalized-def ndef
            m))))
    (if (and match-def (not do-not-alias?))
      `(defdata-alias ,DEFDATA::NAME ,DEFDATA::MATCH-DEF)
      (defdata-core-events a1 wrld))))
other
(defloop deref-combinator-alias
  (comb table)
  (for ((entry in table))
    (when (member-eq comb
        (get1 :aliases (cdr entry)))
      (return (car entry)))))
other
(mutual-recursion (defun collect-names-texp
    (texp parent-comb
      ctx
      b
      wrld)
    (cond ((possible-constant-value-p texp) 'nil)
      ((atom texp) 'nil)
      ((not (true-listp texp)) (b* ((atbl (table-alist 'type-alias-table
               wrld)) ((cons name u) texp)
            (u (base-alias-type u atbl))
            ((unless (proper-symbolp name)) (er hard?
                ctx
                "~| Expecting ~x0 to be a name symbol.~%"
                name))
            ((unless (proper-symbolp u)) (er hard?
                ctx
                "~| Expecting ~x0 to be a (type) name symbol.~%"
                u))
            ((when parent-comb) (er hard?
                ctx
                "~| Name declaration not allowed under ~x0 scope.~%"
                parent-comb)))
          (acons name u 'nil)))
      (t (b* ((atbl (table-alist 'type-alias-table
               wrld)) (comb (base-alias-type (car texp) atbl))
            ((unless (proper-symbolp comb)) (er hard?
                ctx
                "~| Expecting ~x0 to be a symbol.~%"
                comb))
            (ccomb (deref-combinator-alias comb b))
            ((when (member-eq ccomb '(range member))) 'nil))
          (collect-names-texps (cdr texp)
            ccomb
            ctx
            b
            wrld)))))
  (defun collect-names-texps
    (texps parent-comb
      ctx
      b
      wrld)
    (if (atom texps)
      (if (null texps)
        'nil
        (er hard?
          ctx
          "~| ~x0 is not null. Arguments of a combinator/constructor is expected to be a true-list.~%"
          texps))
      (b* ((n1 (collect-names-texp (car texps)
             parent-comb
             ctx
             b
             wrld)) (n2 (collect-names-texps (cdr texps)
              parent-comb
              ctx
              b
              wrld))
          (non-unique-names (intersection-eq (strip-cars n1)
              (strip-cars n2)))
          ((when (consp non-unique-names)) (er hard?
              ctx
              "~| Names ~x0 being used more than once.~%"
              non-unique-names)))
        (append n1 n2)))))
get-arityfunction
(defun get-arity
  (comb wrld)
  (or (let ((b (table-alist 'builtin-combinator-table
           wrld)))
      (get2 (deref-combinator-alias comb b)
        :arity b))
    (let ((u (table-alist 'user-combinator-table
           wrld)))
      (get2 (deref-combinator-alias comb u)
        :arity u))
    (get2 comb
      :arity (table-alist 'data-constructor-table
        wrld))))
other
(mutual-recursion (defun check-syntax-texp
    (texp scope
      tnames
      ctx
      wrld)
    (cond ((possible-constant-value-p texp) t)
      ((proper-symbolp texp) (let* ((tbl (table-alist 'type-metadata-table
               wrld)) (atbl (table-alist 'type-alias-table
                wrld))
            (texp (base-alias-type texp atbl)))
          (or (member-eq texp tnames)
            (assoc-eq texp tbl)
            (assoc-eq texp scope)
            (er hard?
              ctx
              "~| ~x0 should be a recognized name.~%"
              texp))))
      ((atom texp) (er hard?
          ctx
          "~| ~x0 should be a constant or a name symbol.~%"
          texp))
      ((not (true-listp texp)) (check-syntax-texp (cdr texp)
          scope
          tnames
          ctx
          wrld))
      (t (b* (((unless (true-listp texp)) (er hard?
               ctx
               "~| ~x0 should be a true-list.~%"
               texp)) (comb (car texp))
            (arity (get-arity comb wrld))
            ((unless (or (not (natp arity))
                 (equal (len (cdr texp)) arity))) (er hard?
                ctx
                "~| Arity mismatch! ~x0 expects ~x1 arguments but got ~x2.~%"
                comb
                arity
                (len (cdr texp))))
            (b (table-alist 'builtin-combinator-table
                wrld))
            (bcomb (deref-combinator-alias comb b))
            ((when bcomb) (case bcomb
                (range (or (member-eq (cadr texp)
                      '(integer rational))
                    (er hard?
                      ctx
                      "~| Range domain ~x0 should be one of integer or rational.~%"
                      (cadr texp))))
                (member t)
                (or (if (> (len (remove-duplicates-equal (cdr texp)))
                      1)
                    (check-syntax-texps (cdr texp)
                      scope
                      tnames
                      ctx
                      wrld)
                    (er hard?
                      ctx
                      "~| ~x0 expects atleast 2 (distinct) arguments.~%"
                      comb)))
                (otherwise (check-syntax-texps (cdr texp)
                    scope
                    tnames
                    ctx
                    wrld))))
            ((when (assoc-eq (car texp)
                 (table-alist 'data-constructor-table
                   wrld))) (check-syntax-texps (cdr texp)
                (append (collect-names-texps (cdr texp)
                    nil
                    ctx
                    b
                    wrld)
                  scope)
                tnames
                ctx
                wrld)))
          (check-syntax-texps (cdr texp)
            scope
            tnames
            ctx
            wrld)))))
  (defun check-syntax-texps
    (texps scope
      tnames
      ctx
      wrld)
    (if (endp texps)
      t
      (and (check-syntax-texp (car texps)
          scope
          tnames
          ctx
          wrld)
        (check-syntax-texps (cdr texps)
          scope
          tnames
          ctx
          wrld)))))
other
(defloop find-recursive-texps
  (texps tnames wrld)
  (for ((texp in texps))
    (append (and (is-recursive-type-exp texp
          tnames
          wrld)
        (list texp)))))
normalize-union-texpsfunction
(defun normalize-union-texps
  (texps tnames wrld)
  "remove duplicates and put base cases before recursive texps"
  (b* ((texps (remove-duplicates-equal texps)) (recursive-texps (find-recursive-texps texps
          tnames
          wrld))
      (base-texps (set-difference-equal texps
          recursive-texps)))
    (append base-texps recursive-texps)))
other
(mutual-recursion (defun parse-texp
    (texp tnames ctx wrld)
    (b* ((texp (base-alias-type texp
           (table-alist 'type-alias-table
             wrld))))
      (cond ((possible-constant-value-p texp) (if (and (quotep texp)
              (or (booleanp (second texp))
                (characterp (second texp))
                (stringp (second texp))
                (acl2-numberp (second texp))
                (keywordp (second texp))))
            (second texp)
            texp))
        ((proper-symbolp texp) texp)
        ((not (true-listp texp)) (cons (base-alias-type (car texp)
              (table-alist 'type-alias-table
                wrld))
            (parse-texp (cdr texp)
              tnames
              ctx
              wrld)))
        (t (b* ((b (table-alist 'builtin-combinator-table
                 wrld)) (comb (base-alias-type (car texp)
                  (table-alist 'type-alias-table
                    wrld)))
              (bcomb (deref-combinator-alias comb b))
              (c (table-alist 'data-constructor-table
                  wrld)))
            (cond (bcomb (case bcomb
                  (range (parse-range-exp (third texp)
                      (cadr texp)
                      ctx
                      wrld))
                  (member (parse-enum-exp (cadr texp)
                      ctx
                      wrld))
                  (or (b* ((rest (normalize-union-texps (parse-texps (cdr texp)
                             tnames
                             ctx
                             wrld)
                           tnames
                           wrld)))
                      (if (consp (cdr rest))
                        (cons 'or rest)
                        (car rest))))
                  (t (cons bcomb
                      (parse-texps (cdr texp)
                        tnames
                        ctx
                        wrld)))))
              ((assoc-eq comb c) (cons comb
                  (parse-texps (cdr texp)
                    tnames
                    ctx
                    wrld)))
              ((true-listp (acl2-getprop (car texp)
                   'macro-args
                   wrld
                   :default :undefined)) (b* (((mv erp ans) (macroexpand1-cmp (cons (base-alias-type (car texp)
                           (table-alist 'type-alias-table
                             wrld))
                         (parse-texps (cdr texp)
                           tnames
                           ctx
                           wrld))
                       ctx
                       wrld
                       (make state-vars))) ((when erp) (er hard?
                        ctx
                        "~| Macroexpanding ~x0 failed!~%"
                        texp)))
                  ans))
              (t (cons (base-alias-type (car texp)
                    (table-alist 'type-alias-table
                      wrld))
                  (parse-texps (cdr texp)
                    tnames
                    ctx
                    wrld)))))))))
  (defun parse-texps
    (texps tnames ctx wrld)
    (if (endp texps)
      'nil
      (cons (parse-texp (car texps)
          tnames
          ctx
          wrld)
        (parse-texps (cdr texps)
          tnames
          ctx
          wrld)))))
parse-top-texpfunction
(defun parse-top-texp
  (name texp
    tnames
    ctx
    wrld)
  (cond ((atom texp) (parse-texp texp
        tnames
        ctx
        wrld))
    ((not (true-listp texp)) (cons (car texp)
        (parse-texp (cdr texp)
          tnames
          ctx
          wrld)))
    (t (b* ((u (table-alist 'user-combinator-table
             wrld)) (ucomb (deref-combinator-alias (car texp)
              u))
          ((when ucomb) (b* ((f (get2 ucomb
                   :syntax-restriction-fn u)) (exp-l (get2 ucomb :expansion u))
                (parsed-args (parse-texps (cdr texp)
                    tnames
                    ctx
                    wrld)))
              (if (or (not f)
                  (funcall-w f
                    (list (cdr texp))
                    ctx
                    wrld))
                (b* ((eexp (expand-lambda (cons exp-l
                         (list (kwote name)
                           (kwote parsed-args))))) ((mv erp result) (trans-my-ev-w eexp
                        ctx
                        wrld
                        nil))
                    ((when erp) (er hard?
                        ctx
                        "~| Eval failed in user-combinator expansion of ~x0.~%"
                        texp)))
                  result)
                (b* ((x0-str (get2 ucomb
                       :syntax-restriction-msg u)) (msg (to-string1 x0-str
                        (acons #\0 (cdr texp) 'nil))))
                  (er hard?
                    ctx
                    "~| ~s0 ~%"
                    msg))))))
        (parse-texp texp
          tnames
          ctx
          wrld)))))
valid-record-field-pfunction
(defun valid-record-field-p
  (x n)
  (and (assoc-eq x n)
    (let ((texp (cdr (assoc-eq x n))))
      (and (proper-symbolp texp)
        (not (assoc-eq texp n))))))
other
(defloop valid-record-fields-p
  (xs n)
  (for ((x in xs))
    (always (and (consp x)
        (valid-record-field-p (car x) n)))))
other
(mutual-recursion (defun undefined-product-texp
    (texp ctx n wrld)
    (cond ((possible-constant-value-p texp) nil)
      ((proper-symbolp texp) nil)
      ((not (true-listp texp)) nil)
      (t (b* ((comb (car texp)) (b (table-alist 'builtin-combinator-table
                wrld))
            (c (table-alist 'data-constructor-table
                wrld)))
          (cond ((assoc-eq comb b) (case comb
                (range nil)
                (member nil)
                (t (undefined-product-texps (cdr texp)
                    ctx
                    n
                    wrld))))
            ((assoc-eq comb c) (undefined-product-texps (cdr texp)
                ctx
                (append (collect-names-texps (cdr texp)
                    nil
                    ctx
                    b
                    wrld)
                  n)
                wrld))
            (t (if (not (new-namep (car texp) wrld))
                (er hard?
                  ctx
                  "~| ~x0 should be a fresh logical name.~%"
                  (car texp))
                (if (valid-record-fields-p (cdr texp)
                    (append (collect-names-texps (cdr texp)
                        nil
                        ctx
                        b
                        wrld)
                      n))
                  (list texp)
                  (er hard?
                    ctx
                    "~| Bad Syntax! Did you want to define a new record? Each record argument should be of form (field-name . type-name). There should be no name overlap among fields and types.~%")))))))))
  (defun undefined-product-texps
    (texps ctx n wrld)
    (if (endp texps)
      'nil
      (append (undefined-product-texp (car texps)
          ctx
          n
          wrld)
        (undefined-product-texps (cdr texps)
          ctx
          n
          wrld)))))
untrans-top-texpfunction
(defun untrans-top-texp
  (name nbody conx-entries)
  "prettyify a normalized/core defdata top texp"
  (let ((tname name))
    (case-match nbody
      (('or 'nil
         ('acons key val !tname)) (list 'alistof key val))
      (('or 'nil
         ('cons ('cons key val) !tname)) (list 'alistof key val))
      (('or 'nil
         ('mset key val !tname)) (list 'map key val))
      (('listof ('cons key val)) (list 'alistof key val))
      (('or 'nil ('cons x !tname)) (list 'listof x))
      ((!tname . args) (if (assoc-eq name conx-entries)
          (cons 'record args)
          (cons name args)))
      (('range dom range-exp) (list 'range
          dom
          (kwote range-exp)))
      (& nbody))))
data-constructor-basisfunction
(defun data-constructor-basis
  (prod curr-pkg a m)
  (b* ((conx-name (car prod)) (fname-tname-alist (cdr prod))
      (fnames (strip-cars fname-tname-alist))
      (preds (predicate-names (strip-cdrs fname-tname-alist)
          a
          m))
      (recog (make-predicate-symbol conx-name
          curr-pkg))
      (fname-pred-alist (pairlis$ fnames preds))
      (prefix (get-dest-prefix conx-name))
      (selector-fn-names (modify-symbol-lst prefix
          fnames
          ""
          curr-pkg))
      (dest-pred-alist (pairlis$ selector-fn-names
          preds)))
    (cons conx-name
      (acons :arity (len (cdr prod))
        (acons :recog recog
          (acons :dest-pred-alist dest-pred-alist
            (acons :field-pred-alist fname-pred-alist 'nil)))))))
other
(defloop data-constructor-bases
  (prods curr-pkg a m)
  (for ((prod in prods))
    (collect (data-constructor-basis prod
        curr-pkg
        a
        m))))
type-metadata-basisfunction
(defun type-metadata-basis
  (tname curr-pkg)
  (declare (xargs :guard (symbolp tname)))
  (b* ((minimal-vals (list (make-predicate-symbol tname
           curr-pkg)
         (s+ "NTH-"
           tname
           "-BUILTIN"
           :pkg curr-pkg)
         (s+ "NTH-"
           tname
           "/ACC-BUILTIN"
           :pkg curr-pkg))) (minimal-keys '(:predicate :enumerator :enum/acc)))
    (cons tname
      (pairlis$ minimal-keys
        minimal-vals))))
other
(defloop type-metadata-bases
  (tnames curr-pkg)
  (declare (xargs :guard (symbol-listp tnames)))
  (for ((tname in tnames))
    (collect (type-metadata-basis tname
        curr-pkg))))
other
(def-const *per-def-keywords*
  '(:satisfies :satisfies-fixer :min-rec-depth :max-rec-depth))
parse-data-deffunction
(defun parse-data-def
  (def tnames
    args
    curr-pkg
    ctx
    wrld)
  (declare (ignorable args))
  (b* ((atbl (table-alist 'type-alias-table
         wrld)) ((unless (consp def)) (er hard?
          ctx
          "~| def ~x0 is empty.~%"
          def))
      ((list* tname body kwd-val-list) def)
      ((unless (symbolp tname)) (er hard?
          ctx
          "~| name ~x0 should be a symbol.~%"
          tname))
      ((mv kwd-alist ?rest) (extract-keywords ctx
          *per-def-keywords*
          kwd-val-list
          'nil
          nil))
      (n (collect-names-texp body
          'top
          ctx
          (table-alist 'builtin-combinator-table
            wrld)
          wrld))
      (m (table-alist 'type-metadata-table
          wrld))
      (a (table-alist 'type-alias-table
          wrld))
      (cmn-nms (intersection-eq (strip-cars n)
          (strip-cars (append m atbl))))
      ((when cmn-nms) (er hard?
          ctx
          "~| Naming of defdata expressions should be disjoint from the type namespace (~x0 are types).~%"
          cmn-nms))
      (fbd-nms (intersection-eq (strip-cars n)
          (forbidden-names)))
      ((when fbd-nms) (er hard?
          ctx
          "~| These names (~x0) are not allowed. Please choose different names and try again.~%"
          fbd-nms))
      (- (check-syntax-texp body
          'nil
          tnames
          ctx
          wrld))
      (nbody (parse-top-texp tname
          body
          tnames
          ctx
          wrld))
      (prods (undefined-product-texp nbody
          ctx
          'nil
          wrld))
      (new-types (type-metadata-bases tnames
          curr-pkg))
      (new-constructors (data-constructor-bases prods
          curr-pkg
          a
          (append new-types m)))
      (new-preds (predicate-names tnames
          a
          (append new-types m)))
      (recp (or (consp (find-recursive-records new-preds
              new-constructors))
          (intersection-eq (texp-constituent-types nbody
              tnames
              wrld
              :include-recursive-references-p t)
            tnames)))
      (kwd-alist (put-assoc-eq :recp recp
          kwd-alist))
      (allp-alias-events (and (proper-symbolp nbody)
          (is-allp-alias nbody wrld)
          `((table allp-aliases-table
             ',(DEFDATA::PREDICATE-NAME DEFDATA::TNAME DEFDATA::A DEFDATA::NEW-TYPES)
             ',DEFDATA::TNAME
             :put))))
      (kwd-alist (put-assoc-eq :post-pred-events (append (get1 :post-pred-events kwd-alist)
            allp-alias-events)
          kwd-alist))
      (pbody (untrans-top-texp tname
          nbody
          new-constructors))
      (new-types (put2-fn tname
          :prettyified-def pbody
          new-types)))
    (cons tname
      (list (cons 'name tname)
        (cons 'ndef nbody)
        (cons 'n n)
        (cons 'pdef pbody)
        (cons 'odef body)
        (cons 'new-constructors new-constructors)
        (cons 'new-types new-types)
        (cons 'kwd-alist kwd-alist)))))
other
(defloop parse-data-defs
  (ds tnames
    kwd-args
    curr-pkg
    ctx
    wrld)
  (for ((d in ds))
    (collect (parse-data-def d
        tnames
        kwd-args
        curr-pkg
        ctx
        wrld))))
other
(def-const *defdata-keywords*
  (append '(:pred-prefix :theory-name :debug :print-commentary :print-summary :time-track :testing-enabled :do-not-alias)
    '(:hints :verbose)
    *per-def-keywords*))
remove1-assoc-eq-lstfunction
(defun remove1-assoc-eq-lst
  (keys alst)
  (if (endp keys)
    alst
    (remove1-assoc-eq-lst (cdr keys)
      (remove1-assoc-eq (car keys)
        alst))))
parse-defdatafunction
(defun parse-defdata
  (args curr-pkg wrld)
  (b* (((mv ds kwd-val-list) (separate-kwd-args args 'nil)) (ctx 'parse)
      (defaults-alst (table-alist 'defdata-defaults-table
          wrld))
      (defaults-alst (remove1-assoc-eq-lst (evens kwd-val-list)
          defaults-alst))
      ((mv kwd-alist rest-args) (extract-keywords ctx
          *defdata-keywords*
          kwd-val-list
          defaults-alst
          nil))
      (acl2-defaults-tbl (table-alist 'acl2-defaults-table wrld))
      (current-termination-method-entry (assoc :termination-method acl2-defaults-tbl))
      (kwd-alist (put-assoc-eq :termination-method current-termination-method-entry
          kwd-alist))
      (tnames (if (symbolp (car ds))
          (list (car ds))
          (strip-cars ds)))
      (theory-name (s+ (car tnames)
          "-THEORY"
          :pkg curr-pkg))
      (kwd-alist (put-assoc-eq :theory-name theory-name
          kwd-alist))
      (kwd-alist (put-assoc-eq :clique tnames
          kwd-alist))
      (kwd-alist (put-assoc-eq :current-package curr-pkg
          kwd-alist))
      (preds (make-predicate-symbol-lst tnames
          curr-pkg))
      (kwd-alist (put-assoc-eq :post-pred-events `((def-ruleset! ,DEFDATA::THEORY-NAME ',DEFDATA::PREDS))
          kwd-alist))
      ((unless (and (consp ds) (true-listp ds))) (er hard?
          ctx
          "~| Empty form not allowed.~%"))
      ((when (and (not (symbolp (car ds)))
           (consp (cdr ds)))) (list (parse-data-defs ds
            tnames
            rest-args
            curr-pkg
            ctx
            wrld)
          kwd-alist))
      (d (if (symbolp (car ds))
          ds
          (car ds)))
      ((unless (> (len d) 1)) (er hard?
          ctx
          "~| Empty definition.~%"))
      ((unless (null (cddr d))) (er hard?
          ctx
          "~| Definitions that are not mutually-recursive should be ~
                      of form (defdata <id> <type-exp> [:hints <hints>
                     ...]).~%")))
    (list (parse-data-defs (list d)
        tnames
        args
        curr-pkg
        ctx
        wrld)
      kwd-alist)))
defdatamacro
(defmacro defdata
  (&rest args)
  (b* ((verbosep (let ((lst (member :verbose args)))
         (and lst (cadr lst)))))
    `(with-output ,@(AND (NOT DEFDATA::VERBOSEP)
       '(:OFF :ALL :ON (DEFDATA::SUMMARY ERROR) :SUMMARY-OFF
         (:OTHER-THAN FORM TIME)))
      :gag-mode t
      :stack :push (encapsulate nil
        (with-output ,@(AND (NOT DEFDATA::VERBOSEP) '(:OFF :ALL :ON DEFDATA::COMMENT))
          :gag-mode t
          :stack :push (make-event (defdata-events (parse-defdata ',DEFDATA::ARGS
                (current-package state)
                (w state))
              (w state))))))))
make-subsumes-relation-namefunction
(defun make-subsumes-relation-name
  (t1 t2 curr-pkg)
  (let* ((str1 (symbol-name t1)) (str2 (symbol-name t2))
      (str11 (string-append str1 "-IS-SUBTYPE-OF-"))
      (str (string-append str11 str2)))
    (fix-intern$ str curr-pkg)))
make-disjoint-relation-namefunction
(defun make-disjoint-relation-name
  (t1 t2 curr-pkg)
  (let* ((str1 (symbol-name t1)) (str2 (symbol-name t2))
      (str11 (string-append str1 "-IS-DISJOINT-WITH-"))
      (str (string-append str11 str2)))
    (fix-intern$ str curr-pkg)))
make-equal-relation-namefunction
(defun make-equal-relation-name
  (t1 t2 curr-pkg)
  (let* ((str1 (symbol-name t1)) (str2 (symbol-name t2))
      (str11 (string-append str1 "-IS-EQUAL-TO-"))
      (str (string-append str11 str2)))
    (fix-intern$ str curr-pkg)))
compute-defdata-relationfunction
(defun compute-defdata-relation
  (t1 t2
    hints
    rule-classes
    strictp
    otf-flg
    ctx
    curr-pkg
    wrld)
  (b* ((m (table-alist 'type-metadata-table
         wrld)) (a (table-alist 'type-alias-table
          wrld))
      (t1 (base-alias-type t1 a))
      (t2 (base-alias-type t2 a))
      (t1p (predicate-name t1))
      (t2p (predicate-name t2))
      ((unless (and (assoc-eq t1 m)
           (assoc-eq t2 m))) (er hard
          ctx
          "~|One of ~x0 and ~x1 is not a defined type!~%"
          t1
          t2))
      (x (fix-intern$ "X" curr-pkg))
      (rule-classes (cond ((or (is-allp-alias t1p wrld)
             (is-allp-alias t2p wrld)
             (equal t1p t2p)) 'nil)
          ((eq ctx 'defdata-equal) `((:rewrite) (:tau-system :corollary (implies (,DEFDATA::T1P ,DEFDATA::X)
                  (,DEFDATA::T2P ,DEFDATA::X)))
              (:tau-system :corollary (implies (,DEFDATA::T2P ,DEFDATA::X)
                  (,DEFDATA::T1P ,DEFDATA::X)))))
          (t rule-classes)))
      (form (cond ((eq ctx 'defdata-disjoint) `(implies (,DEFDATA::T1P ,DEFDATA::X)
              (not (,DEFDATA::T2P ,DEFDATA::X))))
          ((eq ctx 'defdata-subtype) `(implies (,DEFDATA::T1P ,DEFDATA::X)
              (,DEFDATA::T2P ,DEFDATA::X)))
          (t `(equal (,DEFDATA::T1P ,DEFDATA::X)
              (,DEFDATA::T2P ,DEFDATA::X)))))
      (nm (cond ((eq ctx 'defdata-disjoint) (make-disjoint-relation-name t1
              t2
              curr-pkg))
          ((eq ctx 'defdata-subtype) (make-subsumes-relation-name t1
              t2
              curr-pkg))
          (t (make-equal-relation-name t1
              t2
              curr-pkg))))
      (defthm-form `(defthm ,DEFDATA::NM
          ,DEFDATA::FORM
          :hints ,DEFDATA::HINTS
          :rule-classes ,DEFDATA::RULE-CLASSES
          :otf-flg ,DEFDATA::OTF-FLG))
      (form-to-print `(defthm ,DEFDATA::NM
          ,DEFDATA::FORM
          ,@(AND DEFDATA::HINTS `(:HINTS ,DEFDATA::HINTS))
          ,@(AND DEFDATA::RULE-CLASSES `(:RULE-CLASSES ,DEFDATA::RULE-CLASSES))
          ,@(AND DEFDATA::OTF-FLG `(:OTF-FLG ,DEFDATA::OTF-FLG))))
      (final-form (if strictp
          defthm-form
          `(encapsulate nil
            (make-event '(:or ,DEFDATA::DEFTHM-FORM
                (value-triple :defdata-form-failed))))))
      (- (cw "~|Submitting ~x0~|" form-to-print)))
    `,DEFDATA::FINAL-FORM))
defdata-subtypemacro
(defmacro defdata-subtype
  (t1 t2
    &key
    (rule-classes '((:tau-system) (:forward-chaining)))
    strictp
    verbose
    hints
    otf-flg)
  (declare (xargs :guard (and (proper-symbolp t1)
        (proper-symbolp t2))))
  `(with-output ,@(AND (NOT DEFDATA::VERBOSE)
       '(:OFF
         (WARNING DEFDATA::WARNING! DEFDATA::OBSERVATION DEFDATA::PROVE
          DEFDATA::PROOF-BUILDER DEFDATA::EVENT DEFDATA::HISTORY
          DEFDATA::SUMMARY DEFDATA::PROOF-TREE)))
    :stack :push (make-event (compute-defdata-relation ',DEFDATA::T1
        ',DEFDATA::T2
        ',DEFDATA::HINTS
        ',DEFDATA::RULE-CLASSES
        ',DEFDATA::STRICTP
        ',DEFDATA::OTF-FLG
        'defdata-subtype
        (current-package state)
        (w state)))))
defdata-disjointmacro
(defmacro defdata-disjoint
  (t1 t2
    &key
    (rule-classes '((:tau-system) (:forward-chaining)))
    strictp
    verbose
    hints
    otf-flg)
  (declare (xargs :guard (and (proper-symbolp t1)
        (proper-symbolp t2))))
  `(with-output ,@(AND (NOT DEFDATA::VERBOSE)
       '(:OFF
         (WARNING DEFDATA::WARNING! DEFDATA::OBSERVATION DEFDATA::PROVE
          DEFDATA::PROOF-BUILDER DEFDATA::EVENT DEFDATA::HISTORY
          DEFDATA::SUMMARY DEFDATA::PROOF-TREE)))
    :stack :push (make-event (compute-defdata-relation ',DEFDATA::T1
        ',DEFDATA::T2
        ',DEFDATA::HINTS
        ',DEFDATA::RULE-CLASSES
        ',DEFDATA::STRICTP
        ',DEFDATA::OTF-FLG
        'defdata-disjoint
        (current-package state)
        (w state)))))
defdata-equalmacro
(defmacro defdata-equal
  (t1 t2
    &key
    (rule-classes '((:tau-system)))
    strictp
    verbose
    hints
    otf-flg)
  (declare (xargs :guard (and (proper-symbolp t1)
        (proper-symbolp t2))))
  `(with-output ,@(AND (NOT DEFDATA::VERBOSE)
       '(:OFF
         (WARNING DEFDATA::WARNING! DEFDATA::OBSERVATION DEFDATA::PROVE
          DEFDATA::PROOF-BUILDER DEFDATA::EVENT DEFDATA::HISTORY
          DEFDATA::SUMMARY DEFDATA::PROOF-TREE)))
    :stack :push (make-event (compute-defdata-relation ',DEFDATA::T1
        ',DEFDATA::T2
        ',DEFDATA::HINTS
        ',DEFDATA::RULE-CLASSES
        ',DEFDATA::STRICTP
        ',DEFDATA::OTF-FLG
        'defdata-equal
        (current-package state)
        (w state)))))
defdata-subtype-strictmacro
(defmacro defdata-subtype-strict
  (t1 t2
    &key
    (rule-classes '((:tau-system) (:forward-chaining)))
    verbose
    hints
    otf-flg)
  (declare (xargs :guard (and (proper-symbolp t1)
        (proper-symbolp t2))))
  `(defdata-subtype ,DEFDATA::T1
    ,DEFDATA::T2
    :rule-classes ,DEFDATA::RULE-CLASSES
    :strictp t
    :verbose ,DEFDATA::VERBOSE
    :hints ,DEFDATA::HINTS
    :otf-flg ,DEFDATA::OTF-FLG))
defdata-disjoint-strictmacro
(defmacro defdata-disjoint-strict
  (t1 t2
    &key
    (rule-classes '((:tau-system) (:forward-chaining)))
    verbose
    hints
    otf-flg)
  (declare (xargs :guard (and (proper-symbolp t1)
        (proper-symbolp t2))))
  `(defdata-disjoint ,DEFDATA::T1
    ,DEFDATA::T2
    :rule-classes ,DEFDATA::RULE-CLASSES
    :strictp t
    :verbose ,DEFDATA::VERBOSE
    :hints ,DEFDATA::HINTS
    :otf-flg ,DEFDATA::OTF-FLG))
defdata-equal-strictmacro
(defmacro defdata-equal-strict
  (t1 t2
    &key
    (rule-classes '((:tau-system)))
    verbose
    hints
    otf-flg)
  (declare (xargs :guard (and (proper-symbolp t1)
        (proper-symbolp t2))))
  `(defdata-equal ,DEFDATA::T1
    ,DEFDATA::T2
    :rule-classes ,DEFDATA::RULE-CLASSES
    :strictp t
    :verbose ,DEFDATA::VERBOSE
    :hints ,DEFDATA::HINTS
    :otf-flg ,DEFDATA::OTF-FLG))
defdatas-disjoint-car-fnfunction
(defun defdatas-disjoint-car-fn
  (l rule-classes
    strictp
    verbose
    hints
    otf-flg)
  (if (endp (cdr l))
    nil
    (cons `(defdata-disjoint ,(CAR DEFDATA::L)
        ,(SECOND DEFDATA::L)
        :rule-classes ,DEFDATA::RULE-CLASSES
        :strictp ,DEFDATA::STRICTP
        :verbose ,DEFDATA::VERBOSE
        :hints ,DEFDATA::HINTS
        :otf-flg ,DEFDATA::OTF-FLG)
      (defdatas-disjoint-car-fn (cons (car l) (cddr l))
        rule-classes
        strictp
        verbose
        hints
        otf-flg))))
defdatas-disjoint-fnfunction
(defun defdatas-disjoint-fn
  (l rule-classes
    strictp
    verbose
    hints
    otf-flg)
  (if (endp (cdr l))
    nil
    (append (defdatas-disjoint-car-fn l
        rule-classes
        strictp
        verbose
        hints
        otf-flg)
      (defdatas-disjoint-fn (cdr l)
        rule-classes
        strictp
        verbose
        hints
        otf-flg))))
defdatas-disjointmacro
(defmacro defdatas-disjoint
  (l &key
    (rule-classes '((:tau-system) (:forward-chaining)))
    strictp
    verbose
    hints
    otf-flg)
  (declare (xargs :guard (proper-symbol-listp l)))
  `(with-output ,@(AND (NOT DEFDATA::VERBOSE)
       '(:OFF
         (WARNING DEFDATA::WARNING! DEFDATA::OBSERVATION DEFDATA::PROVE
          DEFDATA::PROOF-BUILDER DEFDATA::EVENT DEFDATA::HISTORY
          DEFDATA::SUMMARY DEFDATA::PROOF-TREE)))
    :stack :push (encapsulate nil
      ,@(DEFDATA::DEFDATAS-DISJOINT-FN DEFDATA::L DEFDATA::RULE-CLASSES
   DEFDATA::STRICTP DEFDATA::VERBOSE DEFDATA::HINTS DEFDATA::OTF-FLG))))
defdatas-disjoint-strictmacro
(defmacro defdatas-disjoint-strict
  (l &key
    (rule-classes '((:tau-system) (:forward-chaining)))
    verbose
    hints
    otf-flg)
  (declare (xargs :guard (proper-symbol-listp l)))
  `(defdatas-disjoint ,DEFDATA::L
    :rule-classes ,DEFDATA::RULE-CLASSES
    :strictp t
    :verbose ,DEFDATA::VERBOSE
    :hints ,DEFDATA::HINTS
    :otf-flg ,DEFDATA::OTF-FLG))
defdatas-subtype-fnfunction
(defun defdatas-subtype-fn
  (l rule-classes
    strictp
    verbose
    hints
    otf-flg)
  (if (endp (cdr l))
    nil
    (cons `(defdata-subtype ,(CAR DEFDATA::L)
        ,(SECOND DEFDATA::L)
        :rule-classes ,DEFDATA::RULE-CLASSES
        :strictp ,DEFDATA::STRICTP
        :verbose ,DEFDATA::VERBOSE
        :hints ,DEFDATA::HINTS
        :otf-flg ,DEFDATA::OTF-FLG)
      (defdatas-subtype-fn (cdr l)
        rule-classes
        strictp
        verbose
        hints
        otf-flg))))
defdatas-subtypemacro
(defmacro defdatas-subtype
  (l &key
    (rule-classes '((:tau-system) (:forward-chaining)))
    strictp
    verbose
    hints
    otf-flg)
  (declare (xargs :guard (proper-symbol-listp l)))
  `(with-output ,@(AND (NOT DEFDATA::VERBOSE)
       '(:OFF
         (WARNING DEFDATA::WARNING! DEFDATA::OBSERVATION DEFDATA::PROVE
          DEFDATA::PROOF-BUILDER DEFDATA::EVENT DEFDATA::HISTORY
          DEFDATA::SUMMARY DEFDATA::PROOF-TREE)))
    :stack :push (encapsulate nil
      ,@(DEFDATA::DEFDATAS-SUBTYPE-FN DEFDATA::L DEFDATA::RULE-CLASSES
   DEFDATA::STRICTP DEFDATA::VERBOSE DEFDATA::HINTS DEFDATA::OTF-FLG))))
defdatas-subtype-strictmacro
(defmacro defdatas-subtype-strict
  (l &key
    (rule-classes '((:tau-system) (:forward-chaining)))
    verbose
    hints
    otf-flg)
  (declare (xargs :guard (proper-symbol-listp l)))
  `(defdatas-subtype ,DEFDATA::L
    :rule-classes ,DEFDATA::RULE-CLASSES
    :strictp t
    :verbose ,DEFDATA::VERBOSE
    :hints ,DEFDATA::HINTS
    :otf-flg ,DEFDATA::OTF-FLG))
defdatas-equal-fnfunction
(defun defdatas-equal-fn
  (l rule-classes
    strictp
    verbose
    hints
    otf-flg)
  (if (endp (cdr l))
    nil
    (cons `(defdata-equal ,(CAR DEFDATA::L)
        ,(SECOND DEFDATA::L)
        :rule-classes ,DEFDATA::RULE-CLASSES
        :strictp ,DEFDATA::STRICTP
        :verbose ,DEFDATA::VERBOSE
        :hints ,DEFDATA::HINTS
        :otf-flg ,DEFDATA::OTF-FLG)
      (defdatas-equal-fn (cdr l)
        rule-classes
        strictp
        verbose
        hints
        otf-flg))))
defdatas-equalmacro
(defmacro defdatas-equal
  (l &key
    (rule-classes '((:tau-system) (:forward-chaining)))
    strictp
    verbose
    hints
    otf-flg)
  (declare (xargs :guard (proper-symbol-listp l)))
  `(with-output ,@(AND (NOT DEFDATA::VERBOSE)
       '(:OFF
         (WARNING DEFDATA::WARNING! DEFDATA::OBSERVATION DEFDATA::PROVE
          DEFDATA::PROOF-BUILDER DEFDATA::EVENT DEFDATA::HISTORY
          DEFDATA::SUMMARY DEFDATA::PROOF-TREE)))
    :stack :push (encapsulate nil
      ,@(DEFDATA::DEFDATAS-EQUAL-FN DEFDATA::L DEFDATA::RULE-CLASSES DEFDATA::STRICTP
   DEFDATA::VERBOSE DEFDATA::HINTS DEFDATA::OTF-FLG))))
defdatas-equal-strictmacro
(defmacro defdatas-equal-strict
  (l &key
    (rule-classes '((:tau-system) (:forward-chaining)))
    verbose
    hints
    otf-flg)
  (declare (xargs :guard (proper-symbol-listp l)))
  `(defdatas-equal ,DEFDATA::L
    :rule-classes ,DEFDATA::RULE-CLASSES
    :strictp t
    :verbose ,DEFDATA::VERBOSE
    :hints ,DEFDATA::HINTS
    :otf-flg ,DEFDATA::OTF-FLG))
other
(logic)
is-datadef-type-predicatefunction
(defun is-datadef-type-predicate
  (fn-name m)
  (declare (xargs :verify-guards nil
      :guard (and (symbolp fn-name)
        (symbol-alistp m))))
  (if (endp m)
    nil
    (b* (((cons typ al) (car m)))
      (if (eq fn-name
          (cdr (assoc-eq :predicate al)))
        typ
        (is-datadef-type-predicate fn-name
          (cdr m))))))
is-type-predicate-currentfunction
(defun is-type-predicate-current
  (fn-name wrld)
  (declare (xargs :verify-guards nil
      :guard (plist-worldp wrld)))
  (let ((pred (case-match fn-name
         (('lambda (x) (p x)) (declare (ignorable x))
           p)
         (y y))))
    (and (symbolp pred)
      (is-datadef-type-predicate (base-alias-pred pred
          (table-alist 'pred-alias-table
            wrld))
        (table-alist 'type-metadata-table
          wrld)))))
is-type-predicate-gvfunction
(defun is-type-predicate-gv
  (fn w)
  (declare (xargs :guard t))
  (ec-call (is-type-predicate-current fn w)))
other
(defattach is-type-predicate
  is-type-predicate-gv)
is-a-typename-currentfunction
(defun is-a-typename-current
  (type wrld)
  (declare (xargs :verify-guards nil))
  (predicate-name type))
is-a-typename-gvfunction
(defun is-a-typename-gv
  (type wrld)
  (declare (xargs :guard t))
  (ec-call (is-a-typename-current type wrld)))
other
(defattach is-a-typename
  is-a-typename-gv)