Check if a type sum is statically well-formed.
(check-type-sum tsum ctxt) → (mv err? obligs)
The guard assumptions on the context are motivated as in check-type-product.
The alternatives must have distinct names and be all statically well-formed.
Function:
(defun check-type-sum (tsum ctxt) (declare (xargs :guard (and (type-sump tsum) (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-sum)) (declare (ignorable __function__)) (b* ((alternatives (type-sum->alternatives tsum)) ((unless (no-duplicatesp-equal (alternative-list->name-list alternatives))) (mv (list :duplicate-alternative-names (type-sum-fix tsum)) nil))) (check-alternative-list alternatives ctxt))))
Theorem:
(defthm proof-obligation-listp-of-check-type-sum.obligs (b* (((mv ?err? ?obligs) (check-type-sum tsum ctxt))) (proof-obligation-listp obligs)) :rule-classes :rewrite)
Theorem:
(defthm check-type-sum-of-type-sum-fix-tsum (equal (check-type-sum (type-sum-fix tsum) ctxt) (check-type-sum tsum ctxt)))
Theorem:
(defthm check-type-sum-type-sum-equiv-congruence-on-tsum (implies (type-sum-equiv tsum tsum-equiv) (equal (check-type-sum tsum ctxt) (check-type-sum tsum-equiv ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-type-sum-of-context-fix-ctxt (equal (check-type-sum tsum (context-fix ctxt)) (check-type-sum tsum ctxt)))
Theorem:
(defthm check-type-sum-context-equiv-congruence-on-ctxt (implies (context-equiv ctxt ctxt-equiv) (equal (check-type-sum tsum ctxt) (check-type-sum tsum ctxt-equiv))) :rule-classes :congruence)