		Search-engine friendly clone of the ACL2 documentation.

Deffold-map-event-generation

Deffold-map-gen-prod-map

Generate the map function for a product type.

Signature
(deffold-map-gen-prod-map sum mutrecp suffix targets extra-args overrides fty-table) → event
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).; overrides — Guard (alistp overrides).; fty-table — Guard (alistp fty-table).
Returns: event — Type (acl2::pseudo-event-formp event).

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 map returned by deffold-map-gen-sum-case, 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.

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

Definitions and Theorems

Function: deffold-map-gen-prod-map

(defun deffold-map-gen-prod-map
       (sum mutrecp suffix
            targets extra-args overrides fty-table)
 (declare (xargs :guard (and (flexsum-p sum)
                             (booleanp mutrecp)
                             (symbolp suffix)
                             (symbol-listp targets)
                             (true-listp extra-args)
                             (alistp overrides)
                             (alistp fty-table))))
 (declare (xargs :guard (eq (flexsum->typemacro sum) 'defprod)))
 (let ((__function__ 'deffold-map-gen-prod-map))
  (declare (ignorable __function__))
  (b*
   ((type (flexsum->name sum))
    ((unless (symbolp type))
     (raise "Internal error: malformed type name ~x0."
            type)
     '(_))
    (type-suffix (deffold-map-gen-map-name type suffix))
    (type-count (flexsum->count sum))
    (recog (flexsum->pred sum))
    (fix (flexsum->fix sum))
    ((unless (symbolp fix))
     (raise "Internal error: malformed flexsum fix function ~x0."
            fix)
     '(_))
    (recp (flexsum->recp sum))
    (body (b* ((term-assoc (assoc-equal type overrides))
               ((when term-assoc) (cdr term-assoc))
               (prods (flexsum->prods sum))
               ((unless (flexprod-listp prods))
                (raise "Internal error: malformed products ~x0."
                       prods))
               ((unless (and (consp prods) (endp (cdr prods))))
                (raise "Internal error: non-singleton product ~x0."
                       prods))
               (prod (car prods)))
            (deffold-map-gen-sum-case
                 type fix prod
                 suffix targets extra-args fty-table)))
    (extra-args-names (deffold-map-extra-args-to-names extra-args)))
   (cons
    'define
    (cons
     type-suffix
     (cons
      (cons (cons type (cons recog 'nil))
            extra-args)
      (cons
       (cons 'declare
             (cons (cons 'ignorable
                         (cons type extra-args-names))
                   'nil))
       (cons
        ':returns
        (cons
         (cons 'result (cons recog 'nil))
         (cons
          ':parents
          (cons
           (cons (deffold-map-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)))))))))))))))))

Theorem: pseudo-event-formp-of-deffold-map-gen-prod-map

(defthm pseudo-event-formp-of-deffold-map-gen-prod-map
  (b*
   ((event
         (deffold-map-gen-prod-map sum mutrecp suffix targets
                                   extra-args overrides fty-table)))
   (acl2::pseudo-event-formp event))
  :rule-classes :rewrite)