Check if a product update expression is statically well-formed.
(check-product-update-expression tname target target-result fields fields-result expr ctxt) → result
The type of the target expression must be a deined product type, or a subtype of a defined product type: we calculate the maximal supertype of the expression's type, and ensure that it is a defined product type; since product types are not subtypes, calculating the maximal supertype cannot ``skip'' a product type.
We match the initializers to the fields of the product type, returning an error if there is any mismatch. Unlike a product construction expression, there may be unmatched fields: in general, a product update expression changes only some of the fields.
If the product type has an invariant, we generate a proof obligation saying that the new product type value satisfies the invariant. This formula is obtained by substituting, in the invariant, the updated field names with the updating expressions, and the non-updated field names with corresponding product field expressions.
Function:
(defun check-product-update-expression (tname target target-result fields fields-result expr ctxt) (declare (xargs :guard (and (identifierp tname) (expressionp target) (type-resultp target-result) (initializer-listp fields) (type-resultp fields-result) (expressionp expr) (contextp ctxt)))) (declare (xargs :guard (type-result-case fields-result :err t :ok (= (len fields-result.types) (len fields))))) (let ((__function__ 'check-product-update-expression)) (declare (ignorable __function__)) (type-result-case target-result :err (type-result-err target-result.info) :ok (type-result-case fields-result :err (type-result-err fields-result.info) :ok (b* ((type (ensure-single-type target-result.types)) ((when (not type)) (type-result-err (list :multi-valued-field-target (expression-fix target) target-result.types))) (type (max-supertype type (context->tops ctxt))) ((when (not type)) (type-result-err (list :no-max-supertype type))) (tprod (get-type-product type (context->tops ctxt))) ((when (not tprod)) (type-result-err (list :product-update-type-mismatch type))) (target-fields (type-product->fields tprod)) ((mv okp obligs unmatched-fields) (match-field-list fields fields-result.types target-fields ctxt)) ((when (not okp)) (type-result-err (list :field-type-mismatch type (initializer-list-fix fields) unmatched-fields))) (inv (type-product->invariant tprod)) (inv-oblig? (if inv (b* ((subst-new (initializers-to-variable-substitution fields)) (names (field-list->name-list unmatched-fields)) (subst-old (omap::from-lists names (expression-product-field-list tname target names))) (subst (omap::update* subst-new subst-old))) (non-trivial-proof-obligation (context->obligation-vars ctxt) (context->obligation-hyps ctxt) (subst-expression subst inv) expr)) nil))) (make-type-result-ok :types (list type) :obligations (append fields-result.obligations obligs inv-oblig?)))))))
Theorem:
(defthm type-resultp-of-check-product-update-expression (b* ((result (check-product-update-expression tname target target-result fields fields-result expr ctxt))) (type-resultp result)) :rule-classes :rewrite)
Theorem:
(defthm check-product-update-expression-of-identifier-fix-tname (equal (check-product-update-expression (identifier-fix tname) target target-result fields fields-result expr ctxt) (check-product-update-expression tname target target-result fields fields-result expr ctxt)))
Theorem:
(defthm check-product-update-expression-identifier-equiv-congruence-on-tname (implies (identifier-equiv tname tname-equiv) (equal (check-product-update-expression tname target target-result fields fields-result expr ctxt) (check-product-update-expression tname-equiv target target-result fields fields-result expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-product-update-expression-of-expression-fix-target (equal (check-product-update-expression tname (expression-fix target) target-result fields fields-result expr ctxt) (check-product-update-expression tname target target-result fields fields-result expr ctxt)))
Theorem:
(defthm check-product-update-expression-expression-equiv-congruence-on-target (implies (expression-equiv target target-equiv) (equal (check-product-update-expression tname target target-result fields fields-result expr ctxt) (check-product-update-expression tname target-equiv target-result fields fields-result expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-product-update-expression-of-type-result-fix-target-result (equal (check-product-update-expression tname target (type-result-fix target-result) fields fields-result expr ctxt) (check-product-update-expression tname target target-result fields fields-result expr ctxt)))
Theorem:
(defthm check-product-update-expression-type-result-equiv-congruence-on-target-result (implies (type-result-equiv target-result target-result-equiv) (equal (check-product-update-expression tname target target-result fields fields-result expr ctxt) (check-product-update-expression tname target target-result-equiv fields fields-result expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-product-update-expression-of-initializer-list-fix-fields (equal (check-product-update-expression tname target target-result (initializer-list-fix fields) fields-result expr ctxt) (check-product-update-expression tname target target-result fields fields-result expr ctxt)))
Theorem:
(defthm check-product-update-expression-initializer-list-equiv-congruence-on-fields (implies (initializer-list-equiv fields fields-equiv) (equal (check-product-update-expression tname target target-result fields fields-result expr ctxt) (check-product-update-expression tname target target-result fields-equiv fields-result expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-product-update-expression-of-type-result-fix-fields-result (equal (check-product-update-expression tname target target-result fields (type-result-fix fields-result) expr ctxt) (check-product-update-expression tname target target-result fields fields-result expr ctxt)))
Theorem:
(defthm check-product-update-expression-type-result-equiv-congruence-on-fields-result (implies (type-result-equiv fields-result fields-result-equiv) (equal (check-product-update-expression tname target target-result fields fields-result expr ctxt) (check-product-update-expression tname target target-result fields fields-result-equiv expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-product-update-expression-of-expression-fix-expr (equal (check-product-update-expression tname target target-result fields fields-result (expression-fix expr) ctxt) (check-product-update-expression tname target target-result fields fields-result expr ctxt)))
Theorem:
(defthm check-product-update-expression-expression-equiv-congruence-on-expr (implies (expression-equiv expr expr-equiv) (equal (check-product-update-expression tname target target-result fields fields-result expr ctxt) (check-product-update-expression tname target target-result fields fields-result expr-equiv ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-product-update-expression-of-context-fix-ctxt (equal (check-product-update-expression tname target target-result fields fields-result expr (context-fix ctxt)) (check-product-update-expression tname target target-result fields fields-result expr ctxt)))
Theorem:
(defthm check-product-update-expression-context-equiv-congruence-on-ctxt (implies (context-equiv ctxt ctxt-equiv) (equal (check-product-update-expression tname target target-result fields fields-result expr ctxt) (check-product-update-expression tname target target-result fields fields-result expr ctxt-equiv))) :rule-classes :congruence)