		Search-engine friendly clone of the ACL2 documentation.

Deffold-map-event-generation

Deffold-map-gen-sum-case

Generate the map for the fields of a product type.

Signature
(deffold-map-gen-sum-case type fix prod suffix targets extra-args fty-table) → term
Arguments: type — Guard (symbolp type).; fix — Guard (symbolp fix).; prod — Guard (flexprod-p prod).; suffix — Guard (symbolp suffix).; targets — Guard (symbol-listp targets).; extra-args — Guard (true-listp extra-args).; fty-table — Guard (alistp fty-table).

This is the term returned, in the absence of overriding, by the map function of a defprod, or by a case of the map function of a deftagsum. See deffold-map.

For each field, we apply the relevant map if it is in the target list. If there exists at least one targeted field, we return the application of the product constructor to each potentially mapped field. If no field is targeted, we instead return the fixed argument without deconstructing it.

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)

Function: deffold-map-gen-sum-case

(defun deffold-map-gen-sum-case
       (type fix prod
             suffix targets extra-args fty-table)
  (declare (xargs :guard (and (symbolp type)
                              (symbolp fix)
                              (flexprod-p prod)
                              (symbolp suffix)
                              (symbol-listp targets)
                              (true-listp extra-args)
                              (alistp fty-table))))
  (let ((__function__ 'deffold-map-gen-sum-case))
    (declare (ignorable __function__))
    (b* ((fields (flexprod->fields prod))
         ((unless (flexprod-field-listp fields))
          (raise "Internal error: malformed fields ~x0."
                 fields))
         ((mv maps targeted)
          (deffold-map-gen-sum-case-loop
               type fields
               suffix targets extra-args fty-table)))
      (if targeted (cons (flexprod->ctor-name prod) maps)
        (list fix type)))))