		Search-engine friendly clone of the ACL2 documentation.

Deffold-reduce-event-generation

Deffoldred-gen-prod-fold

Generate the fold function for a product type.

Signature
(deffoldred-gen-prod-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, product types are stored as a sum types, but with an indication of defprod as the type macro. This sum type must have a single product entry.

If the override alist includes an entry for this product type, we use that as the body of the function.

If there is no overriding term, the body is the combination returned by deffoldred-gen-prod-combination, which is never expected to be empty.

We also generate an `ignorable' declaration for the main formal, in case the overriding term does not mention the formal, or in case the combination is just the default.

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

Definitions and Theorems

Function: deffoldred-gen-prod-fold

(defun deffoldred-gen-prod-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) 'defprod)))
 (let ((__function__ 'deffoldred-gen-prod-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 fn-body thm-events)
     (b* ((term-assoc (assoc-equal type overrides))
          ((when term-assoc)
           (mv (cdr term-assoc) nil))
          (prods (flexsum->prods sum))
          ((unless (flexprod-listp prods))
           (raise "Internal error: malformed products ~x0."
                  prods)
           (mv nil nil))
          ((unless (and (consp prods) (endp (cdr prods))))
           (raise "Internal error: non-singleton product ~x0."
                  prods)
           (mv nil nil))
          (prod (car prods)))
       (deffoldred-gen-prod-combination+theorem
            type type nil nil prod suffix targets
            extra-args default combine fty-table)))
    (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
              fn-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-prod-fold.fn-event

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

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