		Search-engine friendly clone of the ACL2 documentation.

Deffold-map-event-generation

Deffold-map-gen-sum-map

Generate the map function for a sum type.

Signature
(deffold-map-gen-sum-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, 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 deffold-map-gen-sum-cases.

We also generate an `ignorable' declaration, in case the overriding term does not mention the formal.

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

Definitions and Theorems

Function: deffold-map-gen-sum-map

(defun deffold-map-gen-sum-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)
                            'deftagsum)))
 (let ((__function__ 'deffold-map-gen-sum-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))
       (type-case (flexsum->case sum))
       (prods (flexsum->prods sum))
       ((unless (flexprod-listp prods))
        (raise "Internal error: products ~x0 have the wrong type."
               prods))
       (cases
        (deffold-map-gen-sum-cases type fix prods suffix targets
                                   extra-args overrides fty-table)))
      (cons type-case (cons type cases))))
    (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-sum-map

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