Check if a product construction expression is statically well-formed.
(check-product-construct-expression type inits inits-result expr ctxt) → result
The identifier must be the name of a product type in the context. We match the field types calculated for the initializers with the field types of the product type. If the product type has an invariant, we also generate a proof obligation saying that the initializers satisfy the invariant. The type of the expression is the product type.
Function:
(defun check-product-construct-expression (type inits inits-result expr ctxt) (declare (xargs :guard (and (identifierp type) (initializer-listp inits) (type-resultp inits-result) (expressionp expr) (contextp ctxt)))) (declare (xargs :guard (type-result-case inits-result :err t :ok (= (len inits-result.types) (len inits))))) (let ((__function__ 'check-product-construct-expression)) (declare (ignorable __function__)) (type-result-case inits-result :err (type-result-err inits-result.info) :ok (b* ((product (get-type-product (type-defined type) (context->tops ctxt))) ((when (not product)) (type-result-err (list :product-construct-type-mismatch (identifier-fix type)))) (fields (type-product->fields product)) ((mv okp obligs unmatched-fields) (match-field-list inits inits-result.types fields ctxt)) ((when (not okp)) (type-result-err (list :field-type-mismatch (identifier-fix type) (initializer-list-fix inits) fields))) ((when (consp unmatched-fields)) (type-result-err (list :unmatched-fields (identifier-fix type) (initializer-list-fix inits) fields))) (inv (type-product->invariant product)) (inv-oblig? (if inv (b* ((subst (initializers-to-variable-substitution inits))) (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-defined type)) :obligations (append inits-result.obligations obligs inv-oblig?))))))
Theorem:
(defthm type-resultp-of-check-product-construct-expression (b* ((result (check-product-construct-expression type inits inits-result expr ctxt))) (type-resultp result)) :rule-classes :rewrite)
Theorem:
(defthm check-product-construct-expression-of-identifier-fix-type (equal (check-product-construct-expression (identifier-fix type) inits inits-result expr ctxt) (check-product-construct-expression type inits inits-result expr ctxt)))
Theorem:
(defthm check-product-construct-expression-identifier-equiv-congruence-on-type (implies (identifier-equiv type type-equiv) (equal (check-product-construct-expression type inits inits-result expr ctxt) (check-product-construct-expression type-equiv inits inits-result expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-product-construct-expression-of-initializer-list-fix-inits (equal (check-product-construct-expression type (initializer-list-fix inits) inits-result expr ctxt) (check-product-construct-expression type inits inits-result expr ctxt)))
Theorem:
(defthm check-product-construct-expression-initializer-list-equiv-congruence-on-inits (implies (initializer-list-equiv inits inits-equiv) (equal (check-product-construct-expression type inits inits-result expr ctxt) (check-product-construct-expression type inits-equiv inits-result expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-product-construct-expression-of-type-result-fix-inits-result (equal (check-product-construct-expression type inits (type-result-fix inits-result) expr ctxt) (check-product-construct-expression type inits inits-result expr ctxt)))
Theorem:
(defthm check-product-construct-expression-type-result-equiv-congruence-on-inits-result (implies (type-result-equiv inits-result inits-result-equiv) (equal (check-product-construct-expression type inits inits-result expr ctxt) (check-product-construct-expression type inits inits-result-equiv expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-product-construct-expression-of-expression-fix-expr (equal (check-product-construct-expression type inits inits-result (expression-fix expr) ctxt) (check-product-construct-expression type inits inits-result expr ctxt)))
Theorem:
(defthm check-product-construct-expression-expression-equiv-congruence-on-expr (implies (expression-equiv expr expr-equiv) (equal (check-product-construct-expression type inits inits-result expr ctxt) (check-product-construct-expression type inits inits-result expr-equiv ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-product-construct-expression-of-context-fix-ctxt (equal (check-product-construct-expression type inits inits-result expr (context-fix ctxt)) (check-product-construct-expression type inits inits-result expr ctxt)))
Theorem:
(defthm check-product-construct-expression-context-equiv-congruence-on-ctxt (implies (context-equiv ctxt ctxt-equiv) (equal (check-product-construct-expression type inits inits-result expr ctxt) (check-product-construct-expression type inits inits-result expr ctxt-equiv))) :rule-classes :congruence)