Check if a type product is statically well-formed.
(check-type-product tprod ctxt) → (mv err? obligs)
A type product is always checked as part of a type definition (which may or may not be inside a type recursion). Thus, the context in which the type product is checked may have type names, but never has any functions, variables, or obligtion hypotheses.
The fields must have distinct names and well-formed types. If there is an invariant expression, we check it in the context augmented with the typed variables derived from the fields. Note that these are used both to create a variable context and to create the obligation variables. The obligation hypotheses are initially empty.
The expression must return a single boolean value.
Function:
(defun check-type-product (tprod ctxt) (declare (xargs :guard (and (type-productp tprod) (contextp ctxt)))) (declare (xargs :guard (and (null (context->functions ctxt)) (omap::emptyp (context->variables ctxt)) (null (context->obligation-vars ctxt)) (null (context->obligation-hyps ctxt))))) (let ((__function__ 'check-type-product)) (declare (ignorable __function__)) (b* ((fields (type-product->fields tprod)) ((unless (no-duplicatesp-equal (field-list->name-list fields))) (mv (list :duplicate-field-names (type-product-fix tprod)) nil)) ((when (not (check-type-list (field-list->type-list fields) ctxt))) (mv (list :malformed-types (type-product-fix tprod)) nil)) (invariant (type-product->invariant tprod)) ((when (not invariant)) (mv nil nil)) (tvars (field-list-to-typed-variable-list fields)) (var-ctxt (typed-variables-to-variable-context tvars)) (ctxt (change-context ctxt :variables var-ctxt :obligation-vars tvars :obligation-hyps nil)) (result (check-expression invariant ctxt))) (type-result-case result :err (mv result.info nil) :ok (b* ((type (ensure-single-type result.types)) ((when (not type)) (mv (list :multi-valued-invariant (type-product-fix tprod)) nil)) ((unless (subtypep type (type-boolean) (context->tops ctxt))) (mv (list :non-boolean-invariant (type-product-fix tprod)) nil))) (mv nil result.obligations))))))
Theorem:
(defthm proof-obligation-listp-of-check-type-product.obligs (b* (((mv ?err? ?obligs) (check-type-product tprod ctxt))) (proof-obligation-listp obligs)) :rule-classes :rewrite)
Theorem:
(defthm check-type-product-of-type-product-fix-tprod (equal (check-type-product (type-product-fix tprod) ctxt) (check-type-product tprod ctxt)))
Theorem:
(defthm check-type-product-type-product-equiv-congruence-on-tprod (implies (type-product-equiv tprod tprod-equiv) (equal (check-type-product tprod ctxt) (check-type-product tprod-equiv ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-type-product-of-context-fix-ctxt (equal (check-type-product tprod (context-fix ctxt)) (check-type-product tprod ctxt)))
Theorem:
(defthm check-type-product-context-equiv-congruence-on-ctxt (implies (context-equiv ctxt ctxt-equiv) (equal (check-type-product tprod ctxt) (check-type-product tprod ctxt-equiv))) :rule-classes :congruence)