Check if a product field expression is statically well-formed.
(check-product-field-expression target target-result field expr ctxt) → result
The type of the expression must be a defined 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 find the type of the field in the product type: this is the type of the whole expression. No additional proof obligations are generated for this expression.
Function:
(defun check-product-field-expression (target target-result field expr ctxt) (declare (xargs :guard (and (expressionp target) (type-resultp target-result) (identifierp field) (expressionp expr) (contextp ctxt)))) (declare (ignorable expr)) (let ((__function__ 'check-product-field-expression)) (declare (ignorable __function__)) (type-result-case target-result :err (type-result-err target-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-field-type-mismatch type))) (ftype (get-field-type field (type-product->fields tprod))) ((when (not ftype)) (type-result-err (list :no-field-in-product (identifier-fix field) tprod)))) (make-type-result-ok :types (list ftype) :obligations target-result.obligations)))))
Theorem:
(defthm type-resultp-of-check-product-field-expression (b* ((result (check-product-field-expression target target-result field expr ctxt))) (type-resultp result)) :rule-classes :rewrite)
Theorem:
(defthm check-product-field-expression-of-expression-fix-target (equal (check-product-field-expression (expression-fix target) target-result field expr ctxt) (check-product-field-expression target target-result field expr ctxt)))
Theorem:
(defthm check-product-field-expression-expression-equiv-congruence-on-target (implies (expression-equiv target target-equiv) (equal (check-product-field-expression target target-result field expr ctxt) (check-product-field-expression target-equiv target-result field expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-product-field-expression-of-type-result-fix-target-result (equal (check-product-field-expression target (type-result-fix target-result) field expr ctxt) (check-product-field-expression target target-result field expr ctxt)))
Theorem:
(defthm check-product-field-expression-type-result-equiv-congruence-on-target-result (implies (type-result-equiv target-result target-result-equiv) (equal (check-product-field-expression target target-result field expr ctxt) (check-product-field-expression target target-result-equiv field expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-product-field-expression-of-identifier-fix-field (equal (check-product-field-expression target target-result (identifier-fix field) expr ctxt) (check-product-field-expression target target-result field expr ctxt)))
Theorem:
(defthm check-product-field-expression-identifier-equiv-congruence-on-field (implies (identifier-equiv field field-equiv) (equal (check-product-field-expression target target-result field expr ctxt) (check-product-field-expression target target-result field-equiv expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-product-field-expression-of-expression-fix-expr (equal (check-product-field-expression target target-result field (expression-fix expr) ctxt) (check-product-field-expression target target-result field expr ctxt)))
Theorem:
(defthm check-product-field-expression-expression-equiv-congruence-on-expr (implies (expression-equiv expr expr-equiv) (equal (check-product-field-expression target target-result field expr ctxt) (check-product-field-expression target target-result field expr-equiv ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-product-field-expression-of-context-fix-ctxt (equal (check-product-field-expression target target-result field expr (context-fix ctxt)) (check-product-field-expression target target-result field expr ctxt)))
Theorem:
(defthm check-product-field-expression-context-equiv-congruence-on-ctxt (implies (context-equiv ctxt ctxt-equiv) (equal (check-product-field-expression target target-result field expr ctxt) (check-product-field-expression target target-result field expr ctxt-equiv))) :rule-classes :congruence)