Check if a type definition (at the top level) is statically well-formed.
(check-type-definition typedef ctxt) → (mv err? obligs)
This is used on top-level type definitions; we use check-type-definition-in-recursion for type definitions in type recursions.
At the top level, the context has no types being defined, functions being defined, variables in scope, obligation variables, or obligation hypotheses. This motivates the extra guard condition of this ACL2 function.
We ensure that the type being defined here is not already defined. In order to allow (singly) recursive type definitions, we augment the context with the name of the type being defined, and then we check the definition body. For now we allow any form of recursion, but we will add checks to constrain it to be well-formed, so that we can generate a termination proof when we translate the type definition to ACL2. (For now, ACL2 will stop with an error if it cannot automatically prove termination.
Function:
(defun check-type-definition (typedef ctxt) (declare (xargs :guard (and (type-definitionp typedef) (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-definition)) (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)) (ctxt (change-context ctxt :types (cons typedef.name (context->types ctxt))))) (check-type-definer typedef.body ctxt))))
Theorem:
(defthm proof-obligation-listp-of-check-type-definition.obligs (b* (((mv ?err? ?obligs) (check-type-definition typedef ctxt))) (proof-obligation-listp obligs)) :rule-classes :rewrite)
Theorem:
(defthm check-type-definition-of-type-definition-fix-typedef (equal (check-type-definition (type-definition-fix typedef) ctxt) (check-type-definition typedef ctxt)))
Theorem:
(defthm check-type-definition-type-definition-equiv-congruence-on-typedef (implies (type-definition-equiv typedef typedef-equiv) (equal (check-type-definition typedef ctxt) (check-type-definition typedef-equiv ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-type-definition-of-context-fix-ctxt (equal (check-type-definition typedef (context-fix ctxt)) (check-type-definition typedef ctxt)))
Theorem:
(defthm check-type-definition-context-equiv-congruence-on-ctxt (implies (context-equiv ctxt ctxt-equiv) (equal (check-type-definition typedef ctxt) (check-type-definition typedef ctxt-equiv))) :rule-classes :congruence)