Filtering...

record

books/acl2s/defdata/record
other
(in-package "DEFDATA")
other
(include-book "data-structures/utilities" :dir :system)
other
(include-book "register-combinator")
other
(include-book "register-data-constructor")
other
(defconst *tag* :0tag)
build-dex-mset-callfunction
(defun build-dex-mset-call
  (dex-names dex-var-names)
  (declare (xargs :guard (and (symbol-listp dex-names)
        (symbol-listp dex-var-names))))
  (if (endp dex-names)
    nil
    (let* ((dname (car dex-names)) (dvar-name (car dex-var-names))
        (d-keyword-name (intern (symbol-name dname) "KEYWORD")))
      `(mset ,DEFDATA::D-KEYWORD-NAME
        ,DEFDATA::DVAR-NAME
        ,(DEFDATA::BUILD-DEX-MSET-CALL (CDR DEFDATA::DEX-NAMES)
  (CDR DEFDATA::DEX-VAR-NAMES))))))
build-dex-recordimpl-bindingsfunction
(defun build-dex-recordimpl-bindings
  (dex-names dex-var-names
    rec-expr)
  (if (endp dex-names)
    nil
    (let* ((dname (car dex-names)) (dname-var (car dex-var-names))
        (d-keyword-name (intern (symbol-name dname) "KEYWORD")))
      (cons (list dname-var
          (list 'mget
            d-keyword-name
            rec-expr))
        (build-dex-recordimpl-bindings (cdr dex-names)
          (cdr dex-var-names)
          rec-expr)))))
make-constructor-predicatefunction
(defun make-constructor-predicate
  (conx-name dex-pairs kwd-alist)
  (declare (ignorable kwd-alist))
  (b* ((dex-orig-names (strip-cars dex-pairs)) (curr-pkg (get1 :current-package kwd-alist))
      (prefix (get-dest-prefix conx-name))
      (dex-names (modify-symbol-lst prefix
          dex-orig-names
          ""
          curr-pkg))
      (dex-var-names (modify-symbol-lst "VAR-"
          dex-names
          ""
          curr-pkg))
      (dex-preds (strip-cdrs dex-pairs))
      (dex-prex-calls (build-one-param-calls dex-preds
          dex-var-names))
      (dex-mset-call (build-dex-mset-call dex-orig-names
          dex-var-names))
      (dex-bindings (build-dex-recordimpl-bindings dex-orig-names
          dex-var-names
          'v))
      (conx-pred (make-predicate-symbol conx-name
          curr-pkg)))
    `((defund ,DEFDATA::CONX-PRED
       (v)
       (declare (xargs :guard t))
       (if (not (non-empty-good-map v))
         nil
         (let ,DEFDATA::DEX-BINDINGS
           (and (equal v
               (mset ,DEFDATA::*TAG*
                 ',DEFDATA::CONX-NAME
                 ,DEFDATA::DEX-MSET-CALL))
             ,@DEFDATA::DEX-PREX-CALLS)))))))
other
(defloop cons-up-conx-prex-ev
  (new-constructors kwd-alist)
  (for ((cx in new-constructors))
    (append (make-constructor-predicate (car cx)
        (get1 :field-pred-alist (cdr cx))
        kwd-alist))))
conx-pred-events--recur/non-recurfunction
(defun conx-pred-events--recur/non-recur
  (recp p
    top-kwd-alist
    wrld)
  (b* (((cons ?name a) p) ((assocs new-constructors
         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))
      (new-preds (predicate-names (strip-cars new-types)
          at
          m))
      (conx-recursive-alst (find-recursive-records new-preds
          new-constructors))
      (conx-non-recur-alst (set-difference-eq new-constructors
          conx-recursive-alst)))
    (if recp
      (cons-up-conx-prex-ev conx-recursive-alst
        kwd-alist)
      (cons-up-conx-prex-ev conx-non-recur-alst
        kwd-alist))))
other
(defloop conx-non-recur-pred-events
  (ps kwd-alist wrld)
  (for ((p in ps))
    (append (conx-pred-events--recur/non-recur nil
        p
        kwd-alist
        wrld))))
other
(defloop conx-recur-pred-events
  (ps kwd-alist wrld)
  (for ((p in ps))
    (append (conx-pred-events--recur/non-recur t
        p
        kwd-alist
        wrld))))
make-constructorfunction
(defun make-constructor
  (conx-name dex-pairs kwd-alist)
  (declare (ignorable kwd-alist))
  (b* ((dex-orig-names (strip-cars dex-pairs)) (curr-pkg (get1 :current-package kwd-alist))
      (prefix (get-dest-prefix conx-name))
      (dex-names (modify-symbol-lst prefix
          dex-orig-names
          ""
          curr-pkg))
      (dex-var-names (modify-symbol-lst "VAR-"
          dex-names
          ""
          curr-pkg))
      (dex-prex (strip-cdrs dex-pairs))
      (dex-prex-calls (build-one-param-calls dex-prex
          dex-var-names))
      (dex-mset-call (build-dex-mset-call dex-orig-names
          dex-var-names)))
    `((defun ,DEFDATA::CONX-NAME
       ,DEFDATA::DEX-VAR-NAMES
       (declare (xargs :guard (and . ,DEFDATA::DEX-PREX-CALLS)))
       (mset ,DEFDATA::*TAG*
         ',DEFDATA::CONX-NAME
         ,DEFDATA::DEX-MSET-CALL)))))
cons-up-dex-defunsfunction
(defun cons-up-dex-defuns
  (conx-pred selector-fn-names
    dex-names)
  (declare (xargs :guard (and (symbol-listp selector-fn-names)
        (symbol-listp dex-names)
        (equal conx-pred conx-pred))))
  (if (endp dex-names)
    nil
    (let* ((sel-fn-name (car selector-fn-names)) (dname (car dex-names))
        (d-keyword-name (intern (symbol-name dname) "KEYWORD")))
      (cons `(defun ,DEFDATA::SEL-FN-NAME
          (v)
          (declare (xargs :guard (,DEFDATA::CONX-PRED v)))
          (mget ,DEFDATA::D-KEYWORD-NAME v))
        (cons-up-dex-defuns conx-pred
          (cdr selector-fn-names)
          (cdr dex-names))))))
destructor-function-namesfunction
(defun destructor-function-names
  (conx-name dex-pairs kwd-alist)
  (declare (ignorable kwd-alist))
  (let* ((dex-names (strip-cars dex-pairs)) (curr-pkg (get1 :current-package kwd-alist))
      (prefix (get-dest-prefix conx-name)))
    (modify-symbol-lst prefix
      dex-names
      ""
      curr-pkg)))
make-destructorsfunction
(defun make-destructors
  (conx-name dex-pairs kwd-alist)
  (let* ((dex-names (strip-cars dex-pairs)) (selector-fn-names (destructor-function-names conx-name
          dex-pairs
          kwd-alist))
      (curr-pkg (get1 :current-package kwd-alist))
      (conx-pred (make-predicate-symbol conx-name
          curr-pkg)))
    (cons-up-dex-defuns conx-pred
      selector-fn-names
      dex-names)))
cons-up-mod-defunsfunction
(defun cons-up-mod-defuns
  (conx-pred modifier-fn-names
    dex-names)
  (declare (xargs :guard (and (symbol-listp modifier-fn-names)
        (symbol-listp dex-names)
        (equal conx-pred conx-pred))))
  (if (endp dex-names)
    nil
    (let* ((mod-fn-name (car modifier-fn-names)) (dname (car dex-names))
        (d-keyword-name (intern (symbol-name dname) "KEYWORD")))
      (cons `(defun ,DEFDATA::MOD-FN-NAME
          (new v)
          (declare (xargs :guard (,DEFDATA::CONX-PRED v)))
          (mset ,DEFDATA::D-KEYWORD-NAME
            new
            v))
        (cons-up-mod-defuns conx-pred
          (cdr modifier-fn-names)
          (cdr dex-names))))))
modifier-function-namesfunction
(defun modifier-function-names
  (conx-name dex-pairs kwd-alist)
  (declare (ignorable kwd-alist))
  (let* ((dex-names (strip-cars dex-pairs)) (curr-pkg (get1 :current-package kwd-alist))
      (prefix (get-modifier-prefix conx-name)))
    (modify-symbol-lst prefix
      dex-names
      ""
      curr-pkg)))
make-modifiersfunction
(defun make-modifiers
  (conx-name dex-pairs kwd-alist)
  (let* ((dex-names (strip-cars dex-pairs)) (modifier-fn-names (modifier-function-names conx-name
          dex-pairs
          kwd-alist))
      (curr-pkg (get1 :current-package kwd-alist))
      (conx-pred (make-predicate-symbol conx-name
          curr-pkg)))
    (cons-up-mod-defuns conx-pred
      modifier-fn-names
      dex-names)))
conx/dex/mod/record-events1function
(defun conx/dex/mod/record-events1
  (cx kwd-alist)
  (b* (((cons conx-name conx-al) cx) (dest-pred-alist (get1 :dest-pred-alist conx-al))
      (field-pred-alist (get1 :field-pred-alist conx-al))
      (theory-name (get1 :theory-name kwd-alist))
      (pkg (get1 :current-package kwd-alist))
      (dest-defs-ruleset-name (s+ theory-name
          "DEST-DEFS"
          :separator "/"
          :pkg pkg)))
    (append `((local (in-theory (enable ,(DEFDATA::GET1 :RECOG DEFDATA::CONX-AL)))))
      (make-constructor conx-name
        field-pred-alist
        kwd-alist)
      (make-destructors conx-name
        field-pred-alist
        kwd-alist)
      (make-modifiers conx-name
        field-pred-alist
        kwd-alist)
      `((def-ruleset! ,DEFDATA::DEST-DEFS-RULESET-NAME
         ',(DEFDATA::DESTRUCTOR-FUNCTION-NAMES DEFDATA::CONX-NAME
  DEFDATA::FIELD-PRED-ALIST DEFDATA::KWD-ALIST)))
      `((def-patbind-macro ,DEFDATA::CONX-NAME
         ,(DEFDATA::STRIP-CARS DEFDATA::DEST-PRED-ALIST))))))
other
(defloop conx/dex/mod/record-events
  (new-constructors kwd-alist)
  (for ((cx in new-constructors))
    (append (conx/dex/mod/record-events1 cx
        kwd-alist))))
new-conx/record-events1function
(defun new-conx/record-events1
  (p top-kwd-alist)
  (b* (((cons ?name a) p) ((assocs new-constructors kwd-alist) a)
      (kwd-alist (append kwd-alist top-kwd-alist)))
    (conx/dex/mod/record-events new-constructors
      kwd-alist)))
other
(defloop new-conx/record-events0
  (ps kwd-alist wrld)
  (declare (ignorable wrld))
  (for ((p in ps))
    (append (new-conx/record-events1 p
        kwd-alist))))
new-conx/record-eventsfunction
(defun new-conx/record-events
  (ps kwd-alist wrld)
  (b* ((events (new-conx/record-events0 ps
         kwd-alist
         wrld)))
    (and (consp events)
      (append `((commentary ,(DEFDATA::GET1 :PRINT-COMMENTARY DEFDATA::KWD-ALIST)
           "~| Record constructor/destructor/modifier events...~%"))
        events))))
register-conx-evfunction
(defun register-conx-ev
  (conx-name dex-pairs kwd-alist)
  (let* ((dex-orig-names (strip-cars dex-pairs)) (curr-pkg (get1 :current-package kwd-alist))
      (prefix (get-dest-prefix conx-name))
      (conx-pred (make-predicate-symbol conx-name
          curr-pkg))
      (dex-names (modify-symbol-lst prefix
          dex-orig-names
          ""
          curr-pkg))
      (dex-prex (strip-cdrs dex-pairs)))
    `((register-data-constructor ,(LIST DEFDATA::CONX-PRED DEFDATA::CONX-NAME)
       ,(DEFDATA::LIST-UP-LISTS DEFDATA::DEX-PREX DEFDATA::DEX-NAMES)
       :recordp t
       :rule-classes (:rewrite)
       :verbose ,(DEFDATA::GET1 :VERBOSE DEFDATA::KWD-ALIST)
       :hints (("Goal" :in-theory (e/d (,DEFDATA::CONX-PRED ,DEFDATA::CONX-NAME)
            (mset-diff-mset2 ,@(REMOVE-DUPLICATES DEFDATA::DEX-PREX)))))))))
other
(defloop reg-record-conx-events
  (new-constructors kwd-alist)
  (for ((cx in new-constructors))
    (append (register-conx-ev (car cx)
        (get1 :field-pred-alist (cdr cx))
        kwd-alist))))
register-record-conx-events1function
(defun register-record-conx-events1
  (p top-kwd-alist)
  (b* (((cons ?name a) p) ((assocs new-constructors kwd-alist) a)
      (kwd-alist (append kwd-alist top-kwd-alist)))
    (reg-record-conx-events new-constructors
      kwd-alist)))
other
(defloop register-record-conx-events
  (ps kwd-alist wrld)
  (declare (ignorable wrld))
  (for ((p in ps))
    (append (register-record-conx-events1 p
        kwd-alist))))
curr-pkg-s+macro
(defmacro curr-pkg-s+
  (&rest args)
  `(s+ ,@DEFDATA::ARGS
    :separator "-"
    :pkg curr-pkg))
record-local-theory-eventsfunction
(defun record-local-theory-events
  (pred conx
    fnames
    disabled-runes
    curr-pkg)
  (b* ((dex-calls (apply-mget-to-xvar-lst 'x
         fnames
         'nil)))
    `((defthm ,(DEFDATA::CURR-PKG-S+ DEFDATA::PRED 'DEFDATA::TAG-BRIDGE-LEMMA1)
       (implies (,DEFDATA::PRED x)
         (equal (equal x (,DEFDATA::CONX ,@DEFDATA::DEX-CALLS))
           t))
       :hints (("Goal" :in-theory (e/d (,DEFDATA::PRED) (,@DEFDATA::DISABLED-RUNES))))
       :rule-classes nil) (defthm ,(DEFDATA::CURR-PKG-S+ DEFDATA::PRED 'DEFDATA::TAG-BRIDGE-LEMMA2)
        (implies (equal x (,DEFDATA::CONX ,@DEFDATA::FNAMES))
          (mget ,DEFDATA::*TAG* x))
        :hints (("Goal" :in-theory (e/d (,DEFDATA::PRED) (,@DEFDATA::DISABLED-RUNES))))
        :rule-classes nil)
      (defthm ,(DEFDATA::CURR-PKG-S+ DEFDATA::PRED 'DEFDATA::TAG-IS-NON-EMPTY)
        (implies (,DEFDATA::PRED x)
          (mget ,DEFDATA::*TAG* x))
        :hints (("goal" :in-theory (e/d nil
             ,(APPEND (LIST DEFDATA::PRED DEFDATA::CONX) DEFDATA::DISABLED-RUNES))
           :use ((:instance ,(DEFDATA::CURR-PKG-S+ DEFDATA::PRED 'DEFDATA::TAG-BRIDGE-LEMMA1)) (:instance ,(DEFDATA::CURR-PKG-S+ DEFDATA::PRED 'DEFDATA::TAG-BRIDGE-LEMMA2)
               ,@(DEFDATA::PAIRLIS$ DEFDATA::FNAMES (PAIRLIS-X2 DEFDATA::DEX-CALLS NIL))))))
        :rule-classes (:forward-chaining))
      (defthm ,(DEFDATA::CURR-PKG-S+ DEFDATA::PRED 'DEFDATA::DEF-CRUX)
        (implies (,DEFDATA::PRED x)
          (equal x (,DEFDATA::CONX ,@DEFDATA::DEX-CALLS)))
        :hints (("Goal" :in-theory (e/d (,DEFDATA::PRED) (,@DEFDATA::DISABLED-RUNES))))
        :rule-classes nil))))
record-predicate-theory-eventsfunction
(defun record-predicate-theory-events
  (pred conx
    fnames
    disabled-runes
    curr-pkg)
  (b* ((dex-calls (apply-mget-to-xvar-lst 'x
         fnames
         'nil)) (dey-calls (apply-mget-to-xvar-lst 'y
          fnames
          'nil))
      (dexy-calls-equal (pairlis-x1 'equal
          (pairlis$ dex-calls
            (pairlis-x2 dey-calls nil)))))
    `((defthm ,(DEFDATA::CURR-PKG-S+ DEFDATA::PRED 'DEFDATA::UNIQUE-TAG)
       (implies (,DEFDATA::PRED x)
         (equal (mget ,DEFDATA::*TAG* x)
           ',DEFDATA::CONX))
       :hints (("goal" :expand ((,DEFDATA::PRED x))
          :in-theory (e/d nil (,@DEFDATA::DISABLED-RUNES))))
       :rule-classes (:forward-chaining :type-prescription)) (defthm ,(DEFDATA::CURR-PKG-S+ DEFDATA::PRED 'DEFDATA::IMPLIES-CONSP)
        (implies (,DEFDATA::PRED x)
          (consp x))
        :rule-classes (:forward-chaining :compound-recognizer))
      (defthm ,(DEFDATA::CURR-PKG-S+ DEFDATA::PRED 'DEFDATA::IMPLIES-GOOD-MAP)
        (implies (,DEFDATA::PRED x)
          (recordp x))
        :hints (("goal" :in-theory (e/d (,DEFDATA::PRED))))
        :rule-classes ((:forward-chaining)))
      (defthm ,(DEFDATA::CURR-PKG-S+ DEFDATA::PRED 'DEFDATA::EXCLUDES-ATOM-LIST)
        (implies (,DEFDATA::PRED x)
          (not (atom-listp x)))
        :hints (("goal" :in-theory (e/d (,DEFDATA::PRED recordp)
             (,@DEFDATA::DISABLED-RUNES))))
        :rule-classes (:tau-system))
      (defthm ,(DEFDATA::CURR-PKG-S+ DEFDATA::PRED 'DEFDATA::FC-EQUALITY)
        (implies (and (,DEFDATA::PRED x)
            (,DEFDATA::PRED y)
            ,@DEFDATA::DEXY-CALLS-EQUAL)
          (equal x y))
        :hints (("goal" :in-theory (e/d (,DEFDATA::CONX) nil)))
        :rule-classes ((:forward-chaining :trigger-terms ((equal ,(CAR DEFDATA::DEX-CALLS) ,(CAR DEFDATA::DEY-CALLS)))))))))
record-per-field-selector-theory-eventsfunction
(defun record-per-field-selector-theory-events
  (fname dpred
    pred
    disabled-runes
    curr-pkg)
  (b* ((kname (keywordify fname)))
    `((defthm ,(DEFDATA::CURR-PKG-S+ DEFDATA::PRED DEFDATA::FNAME 'DEFDATA::SELECTOR)
       (implies (,DEFDATA::PRED x)
         (,DEFDATA::DPRED (mget ,DEFDATA::KNAME x)))
       :hints (("Goal" :in-theory (e/d (,DEFDATA::PRED) (,@DEFDATA::DISABLED-RUNES))))
       :rule-classes (:rewrite (:forward-chaining :trigger-terms ((mget ,DEFDATA::KNAME x))))))))
record-per-field-modifier-theory-eventsfunction
(defun record-per-field-modifier-theory-events
  (fname dpred
    pred
    disabled-runes
    curr-pkg)
  (b* ((kname (keywordify fname)))
    `((defthm ,(DEFDATA::CURR-PKG-S+ DEFDATA::PRED DEFDATA::FNAME 'DEFDATA::MODIFIER)
       (implies (and (,DEFDATA::PRED x)
           (,DEFDATA::DPRED v))
         (,DEFDATA::PRED (mset ,DEFDATA::KNAME v x)))
       :hints (("Goal" :use ((:instance ,(DEFDATA::CURR-PKG-S+ DEFDATA::PRED 'DEFDATA::TAG-IS-NON-EMPTY)))
          :expand (,DEFDATA::PRED (mset ,DEFDATA::KNAME v x))
          :in-theory (e/d (s-diff-entry-tag-is-non-nil s-diff-entry-non-empty-good-map-is-consp2)
            (,DEFDATA::PRED ,(DEFDATA::CURR-PKG-S+ DEFDATA::PRED 'DEFDATA::UNIQUE-TAG)
              (:executable-counterpart mset)
              ,@DEFDATA::DISABLED-RUNES))) (and stable-under-simplificationp
           '(:use ((:instance ,(DEFDATA::CURR-PKG-S+ DEFDATA::PRED 'DEFDATA::DEF-CRUX))))))
       :rule-classes (:rewrite (:forward-chaining :trigger-terms ((mset ,DEFDATA::KNAME v x))))))))
record-per-field-inverse-def-theory-eventsfunction
(defun record-per-field-inverse-def-theory-events
  (conx-name fname
    pred
    disabled-runes
    kwd-alist)
  (declare (ignorable kwd-alist))
  (b* ((kname (keywordify fname)) (curr-pkg (get1 :current-package kwd-alist))
      (sel-name (s+ (get-dest-prefix conx-name)
          fname
          :separator ""
          :pkg curr-pkg)))
    `((defthm ,(DEFDATA::CURR-PKG-S+ DEFDATA::PRED DEFDATA::FNAME 'DEFDATA::INVERSE-DEF)
       (implies (,DEFDATA::PRED x)
         (equal (mget ,DEFDATA::KNAME x)
           (,DEFDATA::SEL-NAME x)))
       :hints (("Goal" :in-theory (e/d nil
            (,@DEFDATA::DISABLED-RUNES)
            (,DEFDATA::SEL-NAME))))))))
other
(defloop collect-inverse-def-theory-events
  (conx fnames
    pred
    disabled-runes
    kwd-alist)
  (for ((fname in fnames))
    (append (record-per-field-inverse-def-theory-events conx
        fname
        pred
        disabled-runes
        kwd-alist))))
collect-per-field-record-eventsfunction
(defun collect-per-field-record-events
  (fnames dprex
    pred
    disabled-runes
    curr-pkg
    flag)
  (if (endp fnames)
    'nil
    (b* ((fname (car fnames)) (dpred (car dprex)))
      (append (case flag
          (:sel (record-per-field-selector-theory-events fname
              dpred
              pred
              disabled-runes
              curr-pkg))
          (:mod (record-per-field-modifier-theory-events fname
              dpred
              pred
              disabled-runes
              curr-pkg))
          (t 'nil))
        (collect-per-field-record-events (cdr fnames)
          (cdr dprex)
          pred
          disabled-runes
          curr-pkg
          flag)))))
term-order-insertfunction
(defun term-order-insert
  (e l)
  (cond ((endp l) (list e))
    ((term-order e (car l)) (cons e l))
    (t (cons (car l)
        (term-order-insert e (cdr l))))))
term-order-sortfunction
(defun term-order-sort
  (l)
  (if (endp l)
    l
    (term-order-insert (car l)
      (term-order-sort (cdr l)))))
intern-symfunction
(defun intern-sym
  (sym pkg-sym)
  (intern-in-package-of-symbol (symbol-name sym)
    pkg-sym))
gen-term-order-thmfunction
(defun gen-term-order-thm
  (type sfields)
  (cond ((endp sfields) nil)
    ((equal (car sfields) *tag*) `(mset ,DEFDATA::*TAG*
        ',TYPE
        ,(DEFDATA::GEN-TERM-ORDER-THM TYPE (CDR DEFDATA::SFIELDS))))
    (t `(mset ,(CAR DEFDATA::SFIELDS)
        ,(DEFDATA::INTERN-SYM (CAR DEFDATA::SFIELDS) TYPE)
        ,(DEFDATA::GEN-TERM-ORDER-THM TYPE (CDR DEFDATA::SFIELDS))))))
make-field-types-form1function
(defun make-field-types-form1
  (type fields types)
  (if (endp fields)
    nil
    (cons `(,(CAR DEFDATA::TYPES) ,(DEFDATA::INTERN-SYM (CAR DEFDATA::FIELDS) TYPE))
      (make-field-types-form1 type
        (cdr fields)
        (cdr types)))))
make-field-types-formfunction
(defun make-field-types-form
  (type fields types)
  (b* ((res (make-field-types-form1 type
         fields
         types)))
    `(and ,@DEFDATA::RES)))
keywordify-lstfunction
(defun keywordify-lst
  (l)
  (if (endp l)
    l
    (cons (keywordify (car l))
      (keywordify-lst (cdr l)))))
record-constructor-rulesfunction
(defun record-constructor-rules
  (type pred fields field-types)
  (b* ((defthm-name (make-symbl `(,TYPE -check)
         (symbol-package-name type))) (fields (keywordify-lst fields))
      (sfields (term-order-sort (cons *tag* fields)))
      (mset-form (gen-term-order-thm type sfields))
      (rhs (make-field-types-form type
          fields
          field-types)))
    `((defthm ,DEFDATA::DEFTHM-NAME
       (equal (,DEFDATA::PRED ,DEFDATA::MSET-FORM) ,DEFDATA::RHS)
       :hints (("goal" :in-theory (enable ,DEFDATA::PRED)))))))
record-theory-events-builtinfunction
(defun record-theory-events-builtin
  (name field-pred-alist
    new-types
    kwd-alist
    wrld)
  (b* ((m (append new-types
         (table-alist 'type-metadata-table
           wrld))) (a (table-alist 'type-alias-table
          wrld))
      (curr-pkg (get1 :current-package kwd-alist))
      (pred (or (predicate-name name
            a
            m)
          (make-predicate-symbol name
            curr-pkg)))
      ((when (not (proper-symbolp pred))) (er hard?
          'record-theory-events
          "~| Couldnt find predicate name for ~x0.~%"
          name))
      (conx name)
      (dprex (strip-cdrs field-pred-alist))
      (fnames (strip-cars field-pred-alist))
      (disabled (get1 :disabled kwd-alist))
      (disabled-runes (union-eq disabled dprex))
      (record-pred-defthms (record-predicate-theory-events pred
          conx
          fnames
          disabled-runes
          curr-pkg))
      (sel-defthms (collect-per-field-record-events fnames
          dprex
          pred
          disabled-runes
          curr-pkg
          :sel))
      (mod-defthms (collect-per-field-record-events fnames
          dprex
          pred
          disabled-runes
          curr-pkg
          :mod))
      (const-defthms (record-constructor-rules name
          pred
          fnames
          dprex))
      (inverse-def-rules (collect-inverse-def-theory-events conx
          fnames
          pred
          disabled-runes
          kwd-alist))
      (export-thm-events (append record-pred-defthms
          sel-defthms
          mod-defthms
          const-defthms))
      (all-defthm-names (get-event-names export-thm-events))
      (theory-name (get1 :theory-name kwd-alist))
      (inv-ruleset-name (s+ theory-name
          "INVERSE-DEST-DEF-RULES"
          :separator "/"
          :pkg curr-pkg)))
    `((local (progn . ,(DEFDATA::RECORD-LOCAL-THEORY-EVENTS DEFDATA::PRED DEFDATA::CONX
  DEFDATA::FNAMES DEFDATA::DISABLED-RUNES DEFDATA::CURR-PKG))) ,@DEFDATA::EXPORT-THM-EVENTS
      (def-ruleset! ,DEFDATA::THEORY-NAME
        ',DEFDATA::ALL-DEFTHM-NAMES)
      ,@DEFDATA::INVERSE-DEF-RULES
      (def-ruleset! ,DEFDATA::INV-RULESET-NAME
        ',(DEFDATA::GET-EVENT-NAMES DEFDATA::INVERSE-DEF-RULES))
      (in-theory (disable* ,DEFDATA::INV-RULESET-NAME)))))
record-theory-events-builtin-gvfunction
(defun record-theory-events-builtin-gv
  (name field-pred-alist
    new-types
    kwd-alist
    wrld)
  (declare (xargs :guard t))
  (ec-call (record-theory-events-builtin name
      field-pred-alist
      new-types
      kwd-alist
      wrld)))
other
(defstub record-theory-events
  (* * * * *)
  =>
  *)
other
(defattach record-theory-events
  record-theory-events-builtin-gv)
other
(defloop record-theory-ev-lst
  (new-constructors new-types
    kwd-alist
    wrld)
  (for ((cx in new-constructors))
    (append (record-theory-events (car cx)
        (get1 :field-pred-alist (cdr cx))
        new-types
        kwd-alist
        wrld))))
user-record-theory-ev1function
(defun user-record-theory-ev1
  (p top-kwd-alist wrld)
  (b* (((cons name a) p) ((assocs pdef
         new-constructors
         new-types
         kwd-alist) a)
      (kwd-alist (append kwd-alist top-kwd-alist)))
    (case-match pdef
      (('record . fname-tname-alist) (b* ((tnames (strip-cdrs fname-tname-alist)) (dprex (predicate-names tnames))
            (field-pred-alist (pairlis$ (strip-cars fname-tname-alist)
                dprex)))
          (record-theory-events name
            field-pred-alist
            new-types
            kwd-alist
            wrld)))
      (& (if new-constructors
          (record-theory-ev-lst new-constructors
            new-types
            kwd-alist
            wrld)
          'nil)))))
other
(defloop user-record-theory-ev
  (ps kwd-alist wrld)
  (for ((p in ps))
    (append (user-record-theory-ev1 p
        kwd-alist
        wrld))))
user-record-theory-eventsfunction
(defun user-record-theory-events
  (ps kwd-alist wrld)
  (b* ((events (user-record-theory-ev ps
         kwd-alist
         wrld)))
    (and (consp events)
      (append `((commentary ,(DEFDATA::GET1 :PRINT-COMMENTARY DEFDATA::KWD-ALIST)
           "~| Record theory events...~%"))
        events))))
other
(deflabel record)
other
(register-user-combinator record
  :arity t
  :verbose t
  :expansion (lambda (_name _s)
    (cons _name _s))
  :syntax-restriction-fn nil
  :aliases (struct struct record)
  :pre-pred-hook-fns (conx-non-recur-pred-events)
  :in-pred-hook-fns (conx-recur-pred-events)
  :post-pred-hook-fns (new-conx/record-events user-record-theory-events
    register-record-conx-events))
listifyfunction
(defun listify
  (x)
  (declare (xargs :guard t))
  (if (true-listp x)
    x
    (list x)))
add-assocfunction
(defun add-assoc
  (key vals al)
  (declare (xargs :guard (and (true-listp vals)
        (eqlable-alistp al))))
  "union vals onto the back of existing entry of key in al. "
  (put-assoc key
    (union-equal (listify (get1 key al))
      vals)
    al))
other
(mutual-recursion (defun collect-mget-var->field-names
    (e a.)
    "collect (mget :field1 x) terms in e into alist A. mapping x to (:field1 ...)"
    (declare (xargs :verify-guards nil
        :guard (pseudo-termp e)))
    (cond ((variablep e) a.)
      ((fquotep e) a.)
      (t (if (and (eq 'g (ffn-symb e))
            (= (len e) 3)
            (= 2 (len (second e)))
            (fquotep (second e))
            (keywordp (unquote (second e)))
            (variablep (third e)))
          (add-assoc (third e)
            (list (unquote (second e)))
            a.)
          (collect-mget-var->field-names-lst (fargs e)
            a.)))))
  (defun collect-mget-var->field-names-lst
    (es a.)
    (declare (xargs :guard (pseudo-term-listp es)))
    (if (endp es)
      a.
      (collect-mget-var->field-names-lst (cdr es)
        (collect-mget-var->field-names (car es)
          a.)))))
other
(mutual-recursion (defun predicate-mapping-for-vars-in-term
    (e vars a.)
    "return x -> (P1 ...) alist where (P1 x) occurs in e"
    (declare (xargs :verify-guards nil
        :guard (and (symbol-listp vars)
          (pseudo-termp e))))
    (cond ((variablep e) a.)
      ((fquotep e) a.)
      (t (if (and (= (len e) 2)
            (variablep (second e))
            (member (second e) vars))
          (add-assoc (second e)
            (list (first e))
            a.)
          (predicate-mapping-for-vars-in-terms (fargs e)
            vars
            a.)))))
  (defun predicate-mapping-for-vars-in-terms
    (es vars a.)
    (declare (xargs :guard (and (symbol-listp vars)
          (pseudo-term-listp es))))
    (if (endp es)
      a.
      (predicate-mapping-for-vars-in-terms (cdr es)
        vars
        (predicate-mapping-for-vars-in-term (car es)
          vars
          a.)))))
deffiltermacro
(defmacro deffilter
  (nm arglst filter-fn)
  `(defloop ,DEFDATA::NM
    (,@DEFDATA::ARGLST)
    (for ((x in ,(CAR DEFDATA::ARGLST)))
      (append (and (,DEFDATA::FILTER-FN x) (list x))))))
other
(deffilter filter-top-level-types
  (tnames kind wrld)
  (lambda (x)
    (b* ((pdef (get2 x
           :prettyified-def (table-alist 'type-metadata-table
             wrld))))
      (and (consp pdef)
        (eq kind (car pdef))))))
other
(program)
other
(mutual-recursion (defun constituent-types-closure1
    (tname wrld ans.)
    (b* ((md (get1 tname
           (table-alist 'type-metadata-table
             wrld))) (ndef (get1 :normalized-def md))
        (cnames (texp-constituent-types ndef
            (get1 :clique md)
            wrld))
        (cnames (remove-duplicates cnames)))
      (constituent-types-closure-lst cnames
        wrld
        (union-eq cnames ans.))))
  (defun constituent-types-closure-lst
    (tnames wrld ans.)
    (if (endp tnames)
      ans.
      (constituent-types-closure-lst (cdr tnames)
        wrld
        (union-eq ans.
          (constituent-types-closure1 (car tnames)
            wrld
            ans.))))))
constituent-types-closurefunction
(defun constituent-types-closure
  (tname wrld)
  "return closure of all constituent types including itself"
  (constituent-types-closure1 tname
    wrld
    (list tname)))
nested-eliminable-typesfunction
(defun nested-eliminable-types
  (tname wrld)
  (filter-top-level-types (constituent-types-closure tname
      wrld)
    'record
    wrld))
find-record-name3function
(defun find-record-name3
  (p fields wrld)
  (b* ((tname (type-name p wrld)) ((when (null tname)) 'nil)
      (md (get1 tname
          (table-alist 'type-metadata-table
            wrld)))
      (pdef (get1 :prettyified-def md)))
    (and (consp pdef)
      (eq 'record (car pdef))
      (subsetp-equal (symbol-names fields)
        (symbol-names (strip-cars (cdr pdef))))
      (nested-eliminable-types tname
        wrld))))
other
(defloop find-record-name2
  (ps fields wrld)
  (for ((p in ps))
    (append (find-record-name3 p
        fields
        wrld))))
other
(defloop find-record-name1
  (xs |FIELDS{}| |PS{}| wrld)
  (for ((x in xs))
    (append (find-record-name2 (get1 x |PS{}|)
        (get1 x |FIELDS{}|)
        wrld))))
find-record-namesfunction
(defun find-record-names
  (|FIELDS{}| |PS{}| wrld)
  (declare (xargs :verify-guards nil
      :guard (and (symbol-alistp |FIELDS{}|)
        (symbol-alistp |PS{}|)
        (plist-worldp wrld))))
  (remove-duplicates-equal (find-record-name1 (strip-cars |FIELDS{}|)
      |FIELDS{}|
      |PS{}|
      wrld)))
other
(defloop inverse-dest-rulesets
  (tnames wrld)
  (for ((tname in tnames))
    (collect (s+ (get2 tname
          :theory-name (table-alist 'type-metadata-table
            wrld))
        "INVERSE-DEST-DEF-RULES"
        :separator "/"))))
other
(defloop dest-defs-rulesets
  (tnames wrld)
  (for ((tname in tnames))
    (collect (s+ (get2 tname
          :theory-name (table-alist 'type-metadata-table
            wrld))
        "DEST-DEFS"
        :separator "/"))))
record-dest-elim-support-fnfunction
(defun record-dest-elim-support-fn
  (stable-under-simplificationp clause
    keyword-alist
    world)
  (b* ((var->fnames (collect-mget-var->field-names-lst clause
         'nil)) (var->ps (predicate-mapping-for-vars-in-terms clause
          (strip-cars var->fnames)
          'nil))
      (record-names (find-record-names var->fnames
          var->ps
          world))
      (enabled (inverse-dest-rulesets record-names
          world))
      (disabled (union-equal record-names
          (dest-defs-rulesets record-names
            world))))
    (if (and stable-under-simplificationp
        (consp record-names))
      (list* ':in-theory
        `(e/d* nil (,@DEFDATA::DISABLED) (,@DEFDATA::ENABLED))
        keyword-alist)
      keyword-alist)))
other
(logic)
record-dest-elim-supportmacro
(defmacro record-dest-elim-support
  nil
  `(record-dest-elim-support-fn stable-under-simplificationp
    clause
    keyword-alist
    world))
enable-record-dest-elimmacro
(defmacro enable-record-dest-elim
  nil
  `(progn (remove-override-hints! '((record-dest-elim-support)))
    (add-override-hints! '((record-dest-elim-support)))))
other
(enable-record-dest-elim)