		Search-engine friendly clone of the ACL2 documentation.

Deffold-reduce-event-generation

Deffoldred-gen-prod/sum/option-fold

Generate the fold function for a product, sum, or option type.

Signature
(deffoldred-gen-prod/sum/option-fold sum mutrecp suffix targets extra-args result default combine overrides fty-table) → (mv fn-event thm-events)
Arguments: sum — Guard (flexsum-p sum).; mutrecp — Guard (booleanp mutrecp).; suffix — Guard (symbolp suffix).; targets — Guard (symbol-listp targets).; extra-args — Guard (true-listp extra-args).; result — Guard (symbolp result).; combine — Guard (symbolp combine).; overrides — Guard (alistp overrides).; fty-table — Guard (alistp fty-table).
Returns: fn-event — Type (acl2::pseudo-event-formp fn-event).; thm-events — Type (acl2::pseudo-event-form-listp thm-events).

In the FTY table, these are all stored as sum types, but with a discriminator as the type macro.

Definitions and Theorems

Function: deffoldred-gen-prod/sum/option-fold

(defun deffoldred-gen-prod/sum/option-fold
       (sum mutrecp suffix targets extra-args result
            default combine overrides fty-table)
 (declare (xargs :guard (and (flexsum-p sum)
                             (booleanp mutrecp)
                             (symbolp suffix)
                             (symbol-listp targets)
                             (true-listp extra-args)
                             (symbolp result)
                             (symbolp combine)
                             (alistp overrides)
                             (alistp fty-table))))
 (let ((__function__ 'deffoldred-gen-prod/sum/option-fold))
  (declare (ignorable __function__))
  (b* ((typemacro (flexsum->typemacro sum)))
   (cond
     ((eq typemacro 'defprod)
      (deffoldred-gen-prod-fold
           sum
           mutrecp suffix targets extra-args result
           default combine overrides fty-table))
     ((eq typemacro 'deftagsum)
      (deffoldred-gen-sum-fold
           sum
           mutrecp suffix targets extra-args result
           default combine overrides fty-table))
     ((eq typemacro 'defoption)
      (deffoldred-gen-option-fold sum mutrecp suffix extra-args
                                  result default combine fty-table))
     (t (prog2$ (raise "Internal error: unsupported sum type ~x0."
                       sum)
                (mv '(_) nil)))))))

Theorem: pseudo-event-formp-of-deffoldred-gen-prod/sum/option-fold.fn-event

(defthm
 pseudo-event-formp-of-deffoldred-gen-prod/sum/option-fold.fn-event
 (b* (((mv ?fn-event ?thm-events)
       (deffoldred-gen-prod/sum/option-fold
            sum
            mutrecp suffix targets extra-args result
            default combine overrides fty-table)))
   (acl2::pseudo-event-formp fn-event))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deffoldred-gen-prod/sum/option-fold.thm-events

(defthm
 pseudo-event-form-listp-of-deffoldred-gen-prod/sum/option-fold.thm-events
 (b* (((mv ?fn-event ?thm-events)
       (deffoldred-gen-prod/sum/option-fold
            sum
            mutrecp suffix targets extra-args result
            default combine overrides fty-table)))
   (acl2::pseudo-event-form-listp thm-events))
 :rule-classes :rewrite)