		Search-engine friendly clone of the ACL2 documentation.

Deffold-map-event-generation

Deffold-map-gen-sum-case-loop

Signature
(deffold-map-gen-sum-case-loop type fields suffix targets extra-args fty-table) → (mv maps targeted)
Arguments: type — Guard (symbolp type).; fields — Guard (flexprod-field-listp fields).; suffix — Guard (symbolp suffix).; targets — Guard (symbol-listp targets).; extra-args — Guard (true-listp extra-args).; fty-table — Guard (alistp fty-table).
Returns: maps — Type (true-listp maps).; targeted — Type (booleanp targeted).

Definitions and Theorems

Function: deffold-map-gen-sum-case-loop

(defun deffold-map-gen-sum-case-loop
       (type fields
             suffix targets extra-args fty-table)
 (declare (xargs :guard (and (symbolp type)
                             (flexprod-field-listp fields)
                             (symbolp suffix)
                             (symbol-listp targets)
                             (true-listp extra-args)
                             (alistp fty-table))))
 (let ((__function__ 'deffold-map-gen-sum-case-loop))
  (declare (ignorable __function__))
  (b*
   (((when (endp fields)) (mv nil nil))
    (field (car fields))
    (recog (flexprod-field->type field))
    ((unless (symbolp recog))
     (raise "Internal error: malformed field recognizer ~x0."
            recog)
     (mv nil nil))
    (info (flextype-with-recognizer recog fty-table))
    (field-type (and info (flextype->name info)))
    (accessor (flexprod-field->acc-name field))
    (field-type-suffix (deffold-map-gen-map-name field-type suffix))
    ((unless (and field-type
                  (member-eq field-type targets)))
     (b* (((mv maps targeted)
           (deffold-map-gen-sum-case-loop
                type (cdr fields)
                suffix targets extra-args fty-table)))
       (mv (cons (cons accessor (cons type 'nil))
                 maps)
           targeted)))
    (extra-args-names (deffold-map-extra-args-to-names extra-args))
    (map (cons field-type-suffix
               (cons (cons accessor (cons type 'nil))
                     extra-args-names)))
    ((mv maps -)
     (deffold-map-gen-sum-case-loop
          type (cdr fields)
          suffix targets extra-args fty-table)))
   (mv (cons map maps) t))))

Theorem: true-listp-of-deffold-map-gen-sum-case-loop.maps

(defthm true-listp-of-deffold-map-gen-sum-case-loop.maps
  (b* (((mv ?maps ?targeted)
        (deffold-map-gen-sum-case-loop
             type fields
             suffix targets extra-args fty-table)))
    (true-listp maps))
  :rule-classes :rewrite)

Theorem: booleanp-of-deffold-map-gen-sum-case-loop.targeted

(defthm booleanp-of-deffold-map-gen-sum-case-loop.targeted
  (b* (((mv ?maps ?targeted)
        (deffold-map-gen-sum-case-loop
             type fields
             suffix targets extra-args fty-table)))
    (booleanp targeted))
  :rule-classes :rewrite)