Check if a type definition in a type recursion is statically well-formed.
(check-type-definition-in-recursion typedef ctxt) → (mv err? obligs)
A type recursion is a top-level construct that immediately contains type definition. Thus, when checking a type definition in a type recursion, in general the context has no functions, variables, obligation variables, or obligation hypotheses. However, it will have the names of the recursive types being defined, and in particular the one whose definition is checked here; see check-type-recursion. This motivates the extra guard conditions of this ACL2 function.
We ensure that the type is not already defined. Unlike check-type-definition, we do not augment the context, because check-type-recursion already adds the type names.
Function:
(defun check-type-definition-in-recursion (typedef ctxt) (declare (xargs :guard (and (type-definitionp typedef) (contextp ctxt)))) (declare (xargs :guard (and (member-equal (type-definition->name typedef) (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-definition-in-recursion)) (declare (ignorable __function__)) (b* (((type-definition typedef) typedef) ((when (get-type-definition typedef.name (context->tops ctxt))) (mv (list :type-already-defined typedef.name) nil))) (check-type-definer typedef.body ctxt))))
Theorem:
(defthm proof-obligation-listp-of-check-type-definition-in-recursion.obligs (b* (((mv ?err? ?obligs) (check-type-definition-in-recursion typedef ctxt))) (proof-obligation-listp obligs)) :rule-classes :rewrite)
Theorem:
(defthm check-type-definition-in-recursion-of-type-definition-fix-typedef (equal (check-type-definition-in-recursion (type-definition-fix typedef) ctxt) (check-type-definition-in-recursion typedef ctxt)))
Theorem:
(defthm check-type-definition-in-recursion-type-definition-equiv-congruence-on-typedef (implies (type-definition-equiv typedef typedef-equiv) (equal (check-type-definition-in-recursion typedef ctxt) (check-type-definition-in-recursion typedef-equiv ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-type-definition-in-recursion-of-context-fix-ctxt (equal (check-type-definition-in-recursion typedef (context-fix ctxt)) (check-type-definition-in-recursion typedef ctxt)))
Theorem:
(defthm check-type-definition-in-recursion-context-equiv-congruence-on-ctxt (implies (context-equiv ctxt ctxt-equiv) (equal (check-type-definition-in-recursion typedef ctxt) (check-type-definition-in-recursion typedef ctxt-equiv))) :rule-classes :congruence)