		Search-engine friendly clone of the ACL2 documentation.

Deffold-reduce-event-generation

Deffoldred-gen-sum-fold

Generate the fold function for a sum type.

Signature
(deffoldred-gen-sum-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, sum types are distinguished from other types that are also stored as sum types by an indication of the type macro deftagsum.

If the override alist includes an entry for this (whole) sum type, we use that as the body of the function.

Otherwise, the function is defined by cases, which are generated by deffoldred-gen-sum-cases.

We also generate an `ignorable' declaration, in case the overriding term does not mention the formal, or in case all the cases are just the default.

The mutrecp flag says whether this sum type is part of a mutually recursive clique.

Definitions and Theorems

Function: deffoldred-gen-sum-fold

(defun deffoldred-gen-sum-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))))
 (declare (xargs :guard (eq (flexsum->typemacro sum)
                            'deftagsum)))
 (let ((__function__ 'deffoldred-gen-sum-fold))
  (declare (ignorable __function__))
  (b*
   ((type (flexsum->name sum))
    ((unless (symbolp type))
     (raise "Internal error: malformed type name ~x0."
            type)
     (mv '(_) nil))
    (type-suffix (deffoldred-gen-fold-name type suffix))
    (type-count (flexsum->count sum))
    (recog (flexsum->pred sum))
    (recp (flexsum->recp sum))
    ((mv body thm-events)
     (b*
       ((term-assoc (assoc-equal type overrides))
        ((when term-assoc)
         (mv (cdr term-assoc) nil))
        (type-case (flexsum->case sum))
        (prods (flexsum->prods sum))
        ((unless (flexprod-listp prods))
         (raise "Internal error: products ~x0 have the wrong type."
                prods)
         (mv nil nil))
        (kind-fn (flexsum->kind sum))
        ((unless (symbolp kind-fn))
         (raise "Internal error: malformed kind function ~x0."
                kind-fn)
         (mv nil nil))
        ((mv cases thm-events)
         (deffoldred-gen-sum-cases
              type
              kind-fn prods suffix targets extra-args
              default combine overrides fty-table)))
       (mv (cons type-case (cons type cases))
           thm-events)))
    (fn-event
     (cons
      'define
      (cons
       type-suffix
       (cons
        (cons (cons type (cons recog 'nil))
              extra-args)
        (cons
         (cons 'declare
               (cons (cons 'ignorable (cons type 'nil))
                     'nil))
         (cons
          ':returns
          (cons
           (cons 'result (cons result 'nil))
           (cons
            ':parents
            (cons
             (cons (deffoldred-gen-topic-name suffix)
                   'nil)
             (cons
              body
              (append
                 (and (or mutrecp recp)
                      (cons ':measure
                            (cons (cons type-count (cons type 'nil))
                                  'nil)))
                 (append (and (not mutrecp)
                              '(:verify-guards :after-returns))
                         (and (not mutrecp)
                              '(:hooks (:fix))))))))))))))))
   (mv fn-event thm-events))))

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

(defthm pseudo-event-formp-of-deffoldred-gen-sum-fold.fn-event
  (b* (((mv ?fn-event ?thm-events)
        (deffoldred-gen-sum-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-sum-fold.thm-events

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