		Search-engine friendly clone of the ACL2 documentation.

Defmake-self-event-generation

Defmake-self-gen-sum-case

Generate the ``make-self'' calls for the fields of a product type.

Signature
(defmake-self-gen-sum-case type prod member-names fty-table make-self-table) → term
Arguments: type — Guard (symbolp type).; prod — Guard (flexprod-p prod).; member-names — Guard (symbol-listp member-names).; fty-table — Guard (alistp fty-table).; make-self-table — Guard (alistp make-self-table).

Definitions and Theorems

Function: defmake-self-gen-sum-case-loop

(defun defmake-self-gen-sum-case-loop
       (type fields
             member-names fty-table make-self-table)
 (declare (xargs :guard (and (symbolp type)
                             (flexprod-field-listp fields)
                             (symbol-listp member-names)
                             (alistp fty-table)
                             (alistp make-self-table))))
 (let ((__function__ 'defmake-self-gen-sum-case-loop))
  (declare (ignorable __function__))
  (b*
   (((when (endp fields)) nil)
    (field (car fields))
    (recog (flexprod-field->type field))
    ((unless (symbolp recog))
     (raise "Internal error: malformed field recognizer ~x0."
            recog))
    (info (flextype-with-recognizer recog fty-table))
    (field-type (and info (flextype->name info)))
    (accessor (flexprod-field->acc-name field))
    ((unless field-type)
     (b*
      ((make-selfs
        (defmake-self-gen-sum-case-loop type (cdr fields)
                                        member-names
                                        fty-table make-self-table)))
      (cons (cons accessor (cons type 'nil))
            make-selfs)))
    ((mv erp field-type-make-self)
     (defmake-self-get-make-self-fn field-type make-self-table))
    ((when erp) (raise "~@0~%" erp))
    (make-self (cons field-type-make-self
                     (cons (cons accessor (cons type 'nil))
                           'nil)))
    (make-selfs
        (defmake-self-gen-sum-case-loop type (cdr fields)
                                        member-names
                                        fty-table make-self-table)))
   (cons make-self make-selfs))))

Theorem: true-listp-of-defmake-self-gen-sum-case-loop

(defthm true-listp-of-defmake-self-gen-sum-case-loop
 (b*
  ((make-selfs
        (defmake-self-gen-sum-case-loop type fields member-names
                                        fty-table make-self-table)))
  (true-listp make-selfs))
 :rule-classes :rewrite)

Function: defmake-self-gen-sum-case

(defun defmake-self-gen-sum-case
       (type prod
             member-names fty-table make-self-table)
 (declare (xargs :guard (and (symbolp type)
                             (flexprod-p prod)
                             (symbol-listp member-names)
                             (alistp fty-table)
                             (alistp make-self-table))))
 (let ((__function__ 'defmake-self-gen-sum-case))
  (declare (ignorable __function__))
  (b*
   ((fields (flexprod->fields prod))
    ((unless (flexprod-field-listp fields))
     (raise "Internal error: malformed fields ~x0."
            fields))
    (make-selfs
        (defmake-self-gen-sum-case-loop type fields member-names
                                        fty-table make-self-table)))
   (list* 'list
          (list 'quote (flexprod->ctor-name prod))
          make-selfs))))