Check if a type subset is statically well-formed.
(check-type-subset tsub ctxt) → (mv err? obligs)
The guard assumptions on the context are motivated as in check-type-product.
The supertype must be well-formed. We check the restriction expression in a context with the type subset variable as the only one; the expression must be boolean-valued. If a witness expression is present, we check it in a context with no variables (so it has to be a ground expression); we ensures it matches the supertype (which may generate proof obligations) and we generate a proof obligation saying that the expression satisfies the restriction.
Function:
(defun check-type-subset (tsub ctxt) (declare (xargs :guard (and (type-subsetp tsub) (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-subset)) (declare (ignorable __function__)) (b* (((type-subset tsub) tsub) ((when (not (check-type tsub.supertype ctxt))) (mv (list :malformed-supertype (type-subset-fix tsub)) nil)) (tvar (make-typed-variable :name tsub.variable :type tsub.supertype)) (var-ctxt (typed-variables-to-variable-context (list tvar))) (ctxt-restr (change-context ctxt :variables var-ctxt :obligation-vars (list tvar) :obligation-hyps nil)) (result-restr (check-expression tsub.restriction ctxt-restr))) (type-result-case result-restr :err (mv result-restr.info nil) :ok (b* ((type (ensure-single-type result-restr.types)) ((when (not type)) (mv (list :multi-valued-restriction (type-subset-fix tsub)) nil)) ((unless (subtypep type (type-boolean) (context->tops ctxt))) (mv (list :non-boolean-restriction (type-subset-fix tsub)) nil)) ((when (not tsub.witness)) (mv nil result-restr.obligations)) (result-wit (check-expression tsub.witness ctxt))) (type-result-case result-wit :err (mv result-wit.info nil) :ok (b* ((type (ensure-single-type result-wit.types)) ((when (not type)) (mv (list :multi-valued-restriction (type-subset-fix tsub)) nil)) ((mv okp obligs) (match-type tsub.witness type tsub.supertype ctxt)) ((when (not okp)) (mv (list :type-mismatch-witness (type-subset-fix tsub)) nil)) (subst (omap::update tsub.variable tsub.witness nil)) (formula (subst-expression subst tsub.restriction)) (oblig? (non-trivial-proof-obligation nil nil formula (expression-literal (literal-string "type-subset"))))) (mv nil (append result-restr.obligations result-wit.obligations obligs oblig?)))))))))
Theorem:
(defthm proof-obligation-listp-of-check-type-subset.obligs (b* (((mv ?err? ?obligs) (check-type-subset tsub ctxt))) (proof-obligation-listp obligs)) :rule-classes :rewrite)
Theorem:
(defthm check-type-subset-of-type-subset-fix-tsub (equal (check-type-subset (type-subset-fix tsub) ctxt) (check-type-subset tsub ctxt)))
Theorem:
(defthm check-type-subset-type-subset-equiv-congruence-on-tsub (implies (type-subset-equiv tsub tsub-equiv) (equal (check-type-subset tsub ctxt) (check-type-subset tsub-equiv ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-type-subset-of-context-fix-ctxt (equal (check-type-subset tsub (context-fix ctxt)) (check-type-subset tsub ctxt)))
Theorem:
(defthm check-type-subset-context-equiv-congruence-on-ctxt (implies (context-equiv ctxt ctxt-equiv) (equal (check-type-subset tsub ctxt) (check-type-subset tsub ctxt-equiv))) :rule-classes :congruence)