		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Match-field

Match a source field to some target field.

Signature
(match-field init source targets ctxt) → (mv yes/no obligs rest-targets)
Arguments: init — Guard (initializerp init).; source — Guard (typep source).; targets — Guard (field-listp targets).; ctxt — Guard (contextp ctxt).
Returns: yes/no — Type (booleanp yes/no).; obligs — Type (proof-obligation-listp obligs).; rest-targets — Type (field-listp rest-targets).

This is used when checking the static semantics of initializers in product/sum constructions and updates: each initializer in such expressions (the init input) with its own calculated type (the type input), must correspond to a field in the product or sum type (one in the targets input). Thus, we look for a field, with the same name as the initializer, in the target fields; if it is not found, it is an error; if it is found, we match the types and remove the target field from further consideration, by returning a list of the remaining fields. This function is called repeatedly by match-field-list.

Definitions and Theorems

Function: match-field

(defun match-field (init source targets ctxt)
  (declare (xargs :guard (and (initializerp init)
                              (typep source)
                              (field-listp targets)
                              (contextp ctxt))))
  (let ((__function__ 'match-field))
    (declare (ignorable __function__))
    (b* (((when (endp targets)) (mv nil nil nil))
         (target (field-fix (car targets)))
         ((when (not (equal (field->name target)
                            (initializer->field init))))
          (b* (((mv okp obligs rest-targets)
                (match-field init source (cdr targets)
                             ctxt))
               ((when (not okp)) (mv nil nil nil)))
            (mv t obligs (cons target rest-targets))))
         ((mv okp obligs)
          (match-type (initializer->value init)
                      source (field->type target)
                      ctxt))
         ((when (not okp)) (mv nil nil nil)))
      (mv t obligs
          (field-list-fix (cdr targets))))))

Theorem: booleanp-of-match-field.yes/no

(defthm booleanp-of-match-field.yes/no
  (b* (((mv ?yes/no ?obligs ?rest-targets)
        (match-field init source targets ctxt)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: proof-obligation-listp-of-match-field.obligs

(defthm proof-obligation-listp-of-match-field.obligs
  (b* (((mv ?yes/no ?obligs ?rest-targets)
        (match-field init source targets ctxt)))
    (proof-obligation-listp obligs))
  :rule-classes :rewrite)

Theorem: field-listp-of-match-field.rest-targets

(defthm field-listp-of-match-field.rest-targets
  (b* (((mv ?yes/no ?obligs ?rest-targets)
        (match-field init source targets ctxt)))
    (field-listp rest-targets))
  :rule-classes :rewrite)

Theorem: match-field-of-initializer-fix-init

(defthm match-field-of-initializer-fix-init
  (equal (match-field (initializer-fix init)
                      source targets ctxt)
         (match-field init source targets ctxt)))

Theorem: match-field-initializer-equiv-congruence-on-init

(defthm match-field-initializer-equiv-congruence-on-init
  (implies (initializer-equiv init init-equiv)
           (equal (match-field init source targets ctxt)
                  (match-field init-equiv source targets ctxt)))
  :rule-classes :congruence)

Theorem: match-field-of-type-fix-source

(defthm match-field-of-type-fix-source
  (equal (match-field init (type-fix source)
                      targets ctxt)
         (match-field init source targets ctxt)))

Theorem: match-field-type-equiv-congruence-on-source

(defthm match-field-type-equiv-congruence-on-source
  (implies (type-equiv source source-equiv)
           (equal (match-field init source targets ctxt)
                  (match-field init source-equiv targets ctxt)))
  :rule-classes :congruence)

Theorem: match-field-of-field-list-fix-targets

(defthm match-field-of-field-list-fix-targets
  (equal (match-field init source (field-list-fix targets)
                      ctxt)
         (match-field init source targets ctxt)))

Theorem: match-field-field-list-equiv-congruence-on-targets

(defthm match-field-field-list-equiv-congruence-on-targets
  (implies (field-list-equiv targets targets-equiv)
           (equal (match-field init source targets ctxt)
                  (match-field init source targets-equiv ctxt)))
  :rule-classes :congruence)

Theorem: match-field-of-context-fix-ctxt

(defthm match-field-of-context-fix-ctxt
  (equal (match-field init source targets (context-fix ctxt))
         (match-field init source targets ctxt)))

Theorem: match-field-context-equiv-congruence-on-ctxt

(defthm match-field-context-equiv-congruence-on-ctxt
  (implies (context-equiv ctxt ctxt-equiv)
           (equal (match-field init source targets ctxt)
                  (match-field init source targets ctxt-equiv)))
  :rule-classes :congruence)