		Search-engine friendly clone of the ACL2 documentation.

Deffold-reduce-event-generation

Deffoldred-gen-prod-combination

Generate the combination for the fields of a product type or a case of a sum type.

Signature
(deffoldred-gen-prod-combination type fields kind kind-fn suffix targets extra-args default combine fty-table) → (mv fn-term thm-term field-names thm-events)
Arguments: type — Guard (symbolp type).; fields — Guard (flexprod-field-listp fields).; kind — Guard (symbolp kind).; kind-fn — Guard (symbolp kind-fn).; suffix — Guard (symbolp suffix).; targets — Guard (symbol-listp targets).; extra-args — Guard (true-listp extra-args).; combine — Guard (symbolp combine).; fty-table — Guard (alistp fty-table).
Returns: field-names — Type (symbol-listp field-names).; thm-events — Type (acl2::pseudo-event-form-listp thm-events).

The type input is the name of the product or sum type. The fields input consists of the fields of the product type or the case of the sum type (the latter is represented as a product type in the FTY table). The kind input is nil if type is a product type, while it is the keyword kind of the summand if type is a sum type. The kind-fn input is the kind function if type is a sum type, otherwise it is nil.

We generate two combination terms: one for the fold function, and one for an associated theorem. We also return the list of names of the fields, in order.

The fn-term is the term returned, in the absence of overriding, by the fold function of a defprod, or by a case of the fold function of a deftagsum. See deffold-reduce.

The thm-term is the term used, in the absence of overriding, as the right side of the theorem <type>-<suffix>-of-<type> described in the user documentation of deffold-reduce.

We go through the fields, and we return a right-associated nest of the :combine operator of the result of the fold functions applied to the fields for which fold functions are generated, starting with the :default term, but in case of a single (combine X default), we just return X. For each field, we obtain the recognizer name, and from that we obtain the type information. If there is no type information, which means that the field has a built-in type (e.g. nat), then we skip the field. If there is type information, we skip the field unless its type is in targets. If a field is not skipped:

For fn-term, we apply the fold function for the field's type to the accessor of the field applied to a variable with the same name as the product (not field) type. This relies on the fact that the functions we generate use the type names as their formals.
For thm-term, we apply the fold function for the field's type to a variable with the same name as the field. This relies on the fact that the left side of the theorem includes a call of the product type constructor applied to arguments with the same names as the the fields.

Definitions and Theorems

Function: deffoldred-gen-prod-combination

(defun deffoldred-gen-prod-combination
       (type fields kind kind-fn suffix targets
             extra-args default combine fty-table)
 (declare (xargs :guard (and (symbolp type)
                             (flexprod-field-listp fields)
                             (symbolp kind)
                             (symbolp kind-fn)
                             (symbolp suffix)
                             (symbol-listp targets)
                             (true-listp extra-args)
                             (symbolp combine)
                             (alistp fty-table))))
 (let ((__function__ 'deffoldred-gen-prod-combination))
  (declare (ignorable __function__))
  (b*
   (((when (endp fields))
     (mv default default nil nil))
    (field (car fields))
    (name (flexprod-field->name field))
    ((unless (symbolp name))
     (raise "Internal error: malformed field name ~x0."
            name)
     (mv nil nil nil nil))
    (recog (flexprod-field->type field))
    ((unless (symbolp recog))
     (raise "Internal error: malformed field recognizer ~x0."
            recog)
     (mv nil nil nil nil))
    (info (flextype-with-recognizer recog fty-table))
    (field-type (and info (flextype->name info)))
    ((unless (and field-type
                  (member-eq field-type targets)))
     (b* (((mv fn-term thm-term rest-names thm-events)
           (deffoldred-gen-prod-combination
                type (cdr fields)
                kind kind-fn suffix targets
                extra-args default combine fty-table)))
       (mv fn-term thm-term (cons name rest-names)
           thm-events)))
    (accessor (flexprod-field->acc-name field))
    ((unless (symbolp accessor))
     (raise "Internal error: malformed field accessor ~x0."
            accessor)
     (mv nil nil nil nil))
    (type-suffix (deffoldred-gen-fold-name type suffix))
    (field-type-suffix (deffoldred-gen-fold-name field-type suffix))
    (extra-args-names (deffoldred-extra-args-to-names extra-args))
    (fn-term (cons field-type-suffix
                   (cons (cons accessor (cons type 'nil))
                         extra-args-names)))
    (thm-term (cons field-type-suffix
                    (cons name extra-args-names)))
    (field-type-suffix-of-accessor
         (acl2::packn-pos (list field-type suffix '-of- accessor)
                          suffix))
    (thm-events
     (and
      (eq combine 'and)
      (eq default t)
      (cons
       (cons
        'defruled
        (cons
         field-type-suffix-of-accessor
         (cons
          (cons
           'implies
           (cons
            (if kind
             (cons
              'and
              (cons
                   (cons type-suffix
                         (cons type extra-args-names))
                   (cons (cons 'equal
                               (cons (cons kind-fn (cons type 'nil))
                                     (cons kind 'nil)))
                         'nil)))
             (cons type-suffix
                   (cons type extra-args-names)))
            (cons (cons field-type-suffix
                        (cons (cons accessor (cons type 'nil))
                              extra-args-names))
                  'nil)))
          (cons ':expand
                (cons (cons type-suffix
                            (cons type extra-args-names))
                      'nil)))))
       (cons
        (cons
         'add-to-ruleset
         (cons
          (deffoldred-gen-ruleset-name suffix)
          (cons
               (cons 'quote
                     (cons (cons field-type-suffix-of-accessor 'nil)
                           'nil))
               'nil)))
        'nil))))
    ((mv rest-fn-term rest-thm-term
         rest-names more-thm-events)
     (deffoldred-gen-prod-combination
          type (cdr fields)
          kind kind-fn suffix targets
          extra-args default combine fty-table))
    (names (cons name rest-names))
    (all-thm-events (append thm-events more-thm-events))
    ((when (equal rest-fn-term default))
     (mv fn-term thm-term names all-thm-events)))
   (mv (cons combine
             (cons fn-term (cons rest-fn-term 'nil)))
       (cons combine
             (cons thm-term (cons rest-thm-term 'nil)))
       names all-thm-events))))

Theorem: symbol-listp-of-deffoldred-gen-prod-combination.field-names

(defthm symbol-listp-of-deffoldred-gen-prod-combination.field-names
  (b* (((mv ?fn-term
            ?thm-term ?field-names ?thm-events)
        (deffoldred-gen-prod-combination
             type fields kind kind-fn suffix targets
             extra-args default combine fty-table)))
    (symbol-listp field-names))
  :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deffoldred-gen-prod-combination.thm-events

(defthm
 pseudo-event-form-listp-of-deffoldred-gen-prod-combination.thm-events
 (b* (((mv ?fn-term
           ?thm-term ?field-names ?thm-events)
       (deffoldred-gen-prod-combination
            type fields kind kind-fn suffix targets
            extra-args default combine fty-table)))
   (acl2::pseudo-event-form-listp thm-events))
 :rule-classes :rewrite)