		Search-engine friendly clone of the ACL2 documentation.

Deffold-reduce-event-generation

Deffoldred-gen-clique-fold/folds

Generate a fold function, or a clique of mutually recursive fold functions, for a clique of types.

Signature
(deffoldred-gen-clique-fold/folds clique suffix targets extra-args result default combine overrides fty-table) → events
Arguments: clique — Guard (flextypes-p clique).; 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: events — Type (acl2::pseudo-event-form-listp events).

The function or clique of functions may be followed by theorems. This is why this function returns a list of events.

If the clique is empty, it is an internal error. If the clique is a singleton, we generate a single function, which may be recursive or not, based on the flag we read from the information about the type. If the clique consists of two or more types, we generate a clique of mutually recursive functions, with a deffixequiv-mutual after the ///, and with the deferred events after that; the name of the clique of functions is derived from the name of the clique of types.

We also generate a :flag-local nil to export the flag macro defthm-<name>-flag, where <name> is the name of the defines clique. This facilitates proving theorems by induction on the functions.

We also generate a form to allow bogus mutual recursion, since we have no control on how the user overrides the boilerplate. Note that this form is automatically local to the defines.

Definitions and Theorems

Function: deffoldred-gen-clique-fold/folds

(defun deffoldred-gen-clique-fold/folds
       (clique suffix targets extra-args result
               default combine overrides fty-table)
 (declare (xargs :guard (and (flextypes-p clique)
                             (symbolp suffix)
                             (symbol-listp targets)
                             (true-listp extra-args)
                             (symbolp result)
                             (symbolp combine)
                             (alistp overrides)
                             (alistp fty-table))))
 (let ((__function__ 'deffoldred-gen-clique-fold/folds))
  (declare (ignorable __function__))
  (b*
   ((members (flextypes->types clique))
    ((unless (true-listp members))
     (raise "Internal error: malformed members of type clique ~x0."
            clique))
    ((when (endp members))
     (raise "Internal error: empty type clique ~x0."
            clique))
    ((when (endp (cdr members)))
     (b* (((mv fn-event thm-events)
           (deffoldred-gen-type-fold
                (car members)
                nil suffix targets extra-args result
                default combine overrides fty-table)))
       (cons fn-event thm-events)))
    (clique-name (flextypes->name clique))
    ((unless (symbolp clique-name))
     (raise "Internal error: malformed clique name ~x0."
            clique-name))
    (clique-name-suffix
         (deffoldred-gen-fold-name clique-name suffix))
    ((mv fn-events thm-events)
     (deffoldred-gen-types-folds
          members
          t suffix targets extra-args result
          default combine overrides fty-table)))
   (cons
    (cons
     'defines
     (cons
      clique-name-suffix
      (cons
       ':parents
       (cons
        (cons (deffoldred-gen-topic-name suffix)
              'nil)
        (append
         fn-events
         (cons
          ':hints
          (cons
           '(("Goal" :in-theory (enable o< o-finp)))
           (cons
            ':verify-guards
            (cons
             ':after-returns
             (cons
              ':flag-local
              (cons
               'nil
               (cons
                ':prepwork
                (cons
                 '((set-bogus-mutual-recursion-ok t))
                 (cons
                  '///
                  (cons
                   (cons
                    'deffixequiv-mutual
                    (cons
                     clique-name-suffix
                     '(:hints
                        (("Goal"
                              :in-theory (disable (tau-system)))))))
                   'nil)))))))))))))))
    thm-events))))

Theorem: pseudo-event-form-listp-of-deffoldred-gen-clique-fold/folds

(defthm pseudo-event-form-listp-of-deffoldred-gen-clique-fold/folds
  (b* ((events (deffoldred-gen-clique-fold/folds
                    clique suffix targets extra-args result
                    default combine overrides fty-table)))
    (acl2::pseudo-event-form-listp events))
  :rule-classes :rewrite)