		Search-engine friendly clone of the ACL2 documentation.

Deffold-map-event-generation

Deffold-map-gen-sum-cases

Generate the code for the cases of a sum type.

Signature
(deffold-map-gen-sum-cases type fix prods suffix targets extra-args overrides fty-table) → keyword+term-list
Arguments: type — Guard (symbolp type).; fix — Guard (symbolp fix).; prods — Guard (flexprod-listp prods).; suffix — Guard (symbolp suffix).; targets — Guard (symbol-listp targets).; extra-args — Guard (true-listp extra-args).; overrides — Guard (alistp overrides).; fty-table — Guard (alistp fty-table).
Returns: keyword+term-list — Type (true-listp keyword+term-list).

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 map over the fields.

Definitions and Theorems

Function: deffold-map-gen-sum-cases

(defun deffold-map-gen-sum-cases
       (type fix prods suffix
             targets extra-args overrides fty-table)
 (declare (xargs :guard (and (symbolp type)
                             (symbolp fix)
                             (flexprod-listp prods)
                             (symbolp suffix)
                             (symbol-listp targets)
                             (true-listp extra-args)
                             (alistp overrides)
                             (alistp fty-table))))
 (let ((__function__ 'deffold-map-gen-sum-cases))
  (declare (ignorable __function__))
  (b* (((when (endp prods)) nil)
       (prod (car prods))
       (kind (flexprod->kind prod))
       ((unless (keywordp kind))
        (raise "Internal error: kind ~x0 is not a keyword."
               kind))
       (term (b* ((term-assoc (assoc-equal (cons type kind)
                                           overrides))
                  ((when term-assoc) (cdr term-assoc)))
               (deffold-map-gen-sum-case
                    type fix prod
                    suffix targets extra-args fty-table))))
   (list*
      kind term
      (deffold-map-gen-sum-cases type fix (cdr prods)
                                 suffix targets
                                 extra-args overrides fty-table)))))

Theorem: true-listp-of-deffold-map-gen-sum-cases

(defthm true-listp-of-deffold-map-gen-sum-cases
 (b*
  ((keyword+term-list
        (deffold-map-gen-sum-cases type fix prods suffix targets
                                   extra-args overrides fty-table)))
  (true-listp keyword+term-list))
 :rule-classes :rewrite)