Check if a type recursion is statically well-formed.
(check-type-recursion typerec ctxt) → (mv err? obligs)
A type recursion is a top-level construct, so the context has no types or functions being defined, no variables in scope, and no obligation variables and hypotheses. This motivates the guard of this ACL2 function.
We ensure that there are at least two types and that their names are all distinct. We add the names to the context and we check the type definitions.
For now we allow any form of mutual recursion, but we will add check to constrain the allowed forms so that we can generate ACL2 termination proofs. For now, ACL2 will stop with an error if it cannot prove termination.
Function:
(defun check-type-recursion (typerec ctxt) (declare (xargs :guard (and (type-recursionp typerec) (contextp ctxt)))) (declare (xargs :guard (and (null (context->types ctxt)) (null (context->functions ctxt)) (omap::emptyp (context->variables ctxt)) (null (context->obligation-vars ctxt)) (null (context->obligation-hyps ctxt))))) (let ((__function__ 'check-type-recursion)) (declare (ignorable __function__)) (b* ((typedefs (type-recursion->definitions typerec)) (names (type-definition-list->name-list typedefs)) ((unless (>= (len names) 2)) (mv (list :type-recursion-with-less-than-two-types typedefs) nil)) ((unless (no-duplicatesp-equal names)) (mv (list :duplicate-recursive-types names) nil)) (ctxt (change-context ctxt :types names))) (check-type-definition-list-in-recursion typedefs ctxt))))
Theorem:
(defthm proof-obligation-listp-of-check-type-recursion.obligs (b* (((mv ?err? ?obligs) (check-type-recursion typerec ctxt))) (proof-obligation-listp obligs)) :rule-classes :rewrite)
Theorem:
(defthm check-type-recursion-of-type-recursion-fix-typerec (equal (check-type-recursion (type-recursion-fix typerec) ctxt) (check-type-recursion typerec ctxt)))
Theorem:
(defthm check-type-recursion-type-recursion-equiv-congruence-on-typerec (implies (type-recursion-equiv typerec typerec-equiv) (equal (check-type-recursion typerec ctxt) (check-type-recursion typerec-equiv ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-type-recursion-of-context-fix-ctxt (equal (check-type-recursion typerec (context-fix ctxt)) (check-type-recursion typerec ctxt)))
Theorem:
(defthm check-type-recursion-context-equiv-congruence-on-ctxt (implies (context-equiv ctxt ctxt-equiv) (equal (check-type-recursion typerec ctxt) (check-type-recursion typerec ctxt-equiv))) :rule-classes :congruence)