register-data-constructor

other

(in-package "DEFDATA")

other

(include-book "defdata-util")

other

(table data-constructor-table
  nil
  nil
  :clear)

other

(def-const *register-data-constructor-keywords*
  '(:verbose :hints :proper :rule-classes :local-events :export-defthms :theory-name :recordp))

(defmacro register-data-constructor
  (recog-constr-pair pred-dex-lst
    &rest
    keys)
  (declare (xargs :guard (and (consp recog-constr-pair)
        (proper-symbolp (car recog-constr-pair))
        (proper-symbolp (cadr recog-constr-pair))
        (symbol-doublet-listp pred-dex-lst))))
  (let* ((verbosep (let ((lst (member :verbose keys)))
         (and lst (cadr lst)))) (ctx 'register-data-constructor))
    `(with-output ,@(AND (NOT DEFDATA::VERBOSEP) '(:OFF :ALL))
      :stack :push (make-event (register-data-constructor-fn ',DEFDATA::RECOG-CONSTR-PAIR
          ',DEFDATA::PRED-DEX-LST
          ',DEFDATA::KEYS
          ',DEFDATA::CTX
          (current-package state)
          (w state))))))

get-proper-dex-theorems1function

(defun get-proper-dex-theorems1
  (conx-name dex-names
    rem-dex-names)
  (declare (xargs :guard (and (symbol-listp dex-names)
        (symbol-listp rem-dex-names))))
  (if (endp rem-dex-names)
    nil
    (cons `(equal (,(CAR DEFDATA::REM-DEX-NAMES) (,DEFDATA::CONX-NAME . ,DEFDATA::DEX-NAMES))
        ,(CAR DEFDATA::REM-DEX-NAMES))
      (get-proper-dex-theorems1 conx-name
        dex-names
        (cdr rem-dex-names)))))

get-proper-dex-theoremsfunction

(defun get-proper-dex-theorems
  (conx-name dex-names)
  (declare (xargs :guard (and (symbolp conx-name)
        (symbol-listp dex-names))))
  (get-proper-dex-theorems1 conx-name
    dex-names
    dex-names))

apply-to-x-lstfunction

(defun apply-to-x-lst
  (fns pkg)
  (b* ((x (fix-intern$ "X" pkg)))
    (list-up-lists fns
      (make-list (len fns)
        :initial-element x))))

(defun register-data-constructor-fn
  (recog-constr-pair pred-dex-lst
    keys
    ctx
    pkg
    wrld)
  (declare (ignorable wrld))
  (b* (((mv kwd-alist rest) (extract-keywords ctx
         *register-data-constructor-keywords*
         keys
         nil
         nil)) ((when rest) (er hard?
          ctx
          "~| Error: Extra args: ~x0~%"
          rest))
      ((list recog conx-name) recog-constr-pair)
      (dex-names (strip-cadrs pred-dex-lst))
      (dpreds (strip-cars pred-dex-lst))
      (hyps (build-one-param-calls dpreds
          dex-names))
      (hyp (if (and (consp hyps) (consp (cdr hyps)))
          (cons 'and hyps)
          (if (consp hyps)
            (car hyps)
            t)))
      (rule-classes (if (member :rule-classes keys)
          (get1 :rule-classes kwd-alist)
          (list :rewrite)))
      (hints (get1 :hints kwd-alist))
      (proper (if (assoc :proper kwd-alist)
          (get1 :proper kwd-alist)
          t))
      (recordp (get1 :recordp kwd-alist))
      (dest-pred-alist (pairlis$ dex-names dpreds))
      (x (fix-intern$ "X" pkg))
      (kwd-alist (acons :arity (len dex-names)
          (acons :recog recog
            (acons :dest-pred-alist dest-pred-alist
              kwd-alist)))))
    `(encapsulate nil
      (logic)
      (with-output :summary-off (:other-than form)
        :on (error)
        (progn (defthm ,(DEFDATA::S+ DEFDATA::CONX-NAME 'DEFDATA::-CONSTRUCTOR-PRED :PKG DEFDATA::PKG)
            (implies ,DEFDATA::HYP
              (,DEFDATA::RECOG (,DEFDATA::CONX-NAME . ,DEFDATA::DEX-NAMES)))
            :hints ,DEFDATA::HINTS
            :rule-classes ,DEFDATA::RULE-CLASSES)
          (defthm ,(DEFDATA::S+ DEFDATA::CONX-NAME 'DEFDATA::-CONSTRUCTOR-DESTRUCTORS :PKG
  DEFDATA::PKG)
            (implies (,DEFDATA::RECOG ,DEFDATA::X)
              (and . ,(DEFDATA::LIST-UP-LISTS DEFDATA::DPREDS
  (DEFDATA::APPLY-TO-X-LST DEFDATA::DEX-NAMES DEFDATA::PKG))))
            :hints ,DEFDATA::HINTS
            :rule-classes ,(IF DEFDATA::RECORDP
     (CONS ':GENERALIZE DEFDATA::RULE-CLASSES)
     DEFDATA::RULE-CLASSES))
          ,@(AND DEFDATA::PROPER
       `((DEFDATA::DEFTHM
          ,(DEFDATA::S+ DEFDATA::CONX-NAME 'DEFDATA::-ELIM-RULE :PKG
            DEFDATA::PKG)
          (DEFDATA::IMPLIES (,DEFDATA::RECOG ,DEFDATA::X)
           (EQUAL
            (,DEFDATA::CONX-NAME
             . ,(DEFDATA::APPLY-TO-X-LST DEFDATA::DEX-NAMES DEFDATA::PKG))
            ,DEFDATA::X))
          :HINTS ,DEFDATA::HINTS :RULE-CLASSES
          ,(IF (OR DEFDATA::RECORDP DEFDATA::RULE-CLASSES)
               '(:ELIM)
               DEFDATA::RULE-CLASSES))
         (DEFDATA::DEFTHM
          ,(DEFDATA::S+ DEFDATA::CONX-NAME
            'DEFDATA::-CONSTRUCTOR-DESTRUCTORS-PROPER :PKG DEFDATA::PKG)
          (DEFDATA::IMPLIES ,DEFDATA::HYP
           (AND
            . ,(DEFDATA::GET-PROPER-DEX-THEOREMS DEFDATA::CONX-NAME
                DEFDATA::DEX-NAMES)))
          :HINTS ,DEFDATA::HINTS :RULE-CLASSES ,DEFDATA::RULE-CLASSES)))
          (table data-constructor-table
            ',DEFDATA::CONX-NAME
            ',DEFDATA::KWD-ALIST)
          (value-triple :registered))))))