		Search-engine friendly clone of the ACL2 documentation.

Deffold-reduce-event-generation

Deffoldred-gen-sum-cases

Generate the code for the cases of a sum type.

Signature
(deffoldred-gen-sum-cases type kind-fn prods suffix targets extra-args default combine overrides fty-table) → (mv keyword+term-list thm-events)
Arguments: type — Guard (symbolp type).; kind-fn — Guard (symbolp kind-fn).; prods — Guard (flexprod-listp prods).; suffix — Guard (symbolp suffix).; targets — Guard (symbol-listp targets).; extra-args — Guard (true-listp extra-args).; combine — Guard (symbolp combine).; overrides — Guard (alistp overrides).; fty-table — Guard (alistp fty-table).
Returns: keyword+term-list — Type (true-listp keyword+term-list).; thm-events — Type (acl2::pseudo-event-form-listp thm-events).

We generate a list (<kind1> <term1> <kind2> <term2> ...), where <kind1>, <kind2>, etc. are the kind keywords of the sum type, and <term1>, <term2>, etc. are the corresponding terms. This list forms the bulk of the body of the generated function for a sum type.

For each case, first we check whether there is an overriding term, in which case we use that as the term for the case. Otherwise, we obtain the combination for the fields.

For now, we do not generate theorems via deffoldred-gen-prod-combination+theorem, but we plan to do that soon.

Definitions and Theorems

Function: deffoldred-gen-sum-cases

(defun deffoldred-gen-sum-cases
       (type kind-fn prods suffix targets extra-args
             default combine overrides fty-table)
  (declare (xargs :guard (and (symbolp type)
                              (symbolp kind-fn)
                              (flexprod-listp prods)
                              (symbolp suffix)
                              (symbol-listp targets)
                              (true-listp extra-args)
                              (symbolp combine)
                              (alistp overrides)
                              (alistp fty-table))))
  (let ((__function__ 'deffoldred-gen-sum-cases))
    (declare (ignorable __function__))
    (b* (((when (endp prods)) (mv nil nil))
         (prod (car prods))
         (kind (flexprod->kind prod))
         ((unless (keywordp kind))
          (raise "Internal error: kind ~x0 is not a keyword."
                 kind)
          (mv nil nil))
         ((mv term thm-events)
          (b* ((term-assoc (assoc-equal (cons type kind)
                                        overrides))
               ((when term-assoc)
                (mv (cdr term-assoc) nil))
               (constr (flexprod->ctor-name prod))
               ((unless (symbolp constr))
                (raise "Internal error: malformed constructor ~x0."
                       constr)
                (mv nil nil)))
            (deffoldred-gen-prod-combination+theorem
                 type
                 constr kind kind-fn prod suffix targets
                 extra-args default combine fty-table)))
         ((mv more-keywords+terms more-thm-events)
          (deffoldred-gen-sum-cases
               type kind-fn (cdr prods)
               suffix targets extra-args
               default combine overrides fty-table)))
      (mv (list* kind term more-keywords+terms)
          (append thm-events more-thm-events)))))

Theorem: true-listp-of-deffoldred-gen-sum-cases.keyword+term-list

(defthm true-listp-of-deffoldred-gen-sum-cases.keyword+term-list
  (b* (((mv ?keyword+term-list ?thm-events)
        (deffoldred-gen-sum-cases
             type
             kind-fn prods suffix targets extra-args
             default combine overrides fty-table)))
    (true-listp keyword+term-list))
  :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deffoldred-gen-sum-cases.thm-events

(defthm
     pseudo-event-form-listp-of-deffoldred-gen-sum-cases.thm-events
  (b* (((mv ?keyword+term-list ?thm-events)
        (deffoldred-gen-sum-cases
             type
             kind-fn prods suffix targets extra-args
             default combine overrides fty-table)))
    (acl2::pseudo-event-form-listp thm-events))
  :rule-classes :rewrite)