Check if a list of function definitions is statically well-formed.
(check-function-definition-list fundefs ctxt) → (mv err? obligs)
This is only used on function definitions inside a function recursion, i.e. not at the top level.
Function:
(defun check-function-definition-list (fundefs ctxt) (declare (xargs :guard (and (function-definition-listp fundefs) (contextp ctxt)))) (declare (xargs :guard (and (null (context->types ctxt)) (subsetp-equal (function-definition-list->header-list fundefs) (context->functions ctxt)) (omap::emptyp (context->variables ctxt)) (null (context->obligation-vars ctxt)) (null (context->obligation-hyps ctxt))))) (let ((__function__ 'check-function-definition-list)) (declare (ignorable __function__)) (b* (((when (endp fundefs)) (mv nil nil)) ((mv err? obligs) (check-function-definition-top/nontop (car fundefs) ctxt)) ((when err?) (mv err? nil)) ((mv err? more-obligs) (check-function-definition-list (cdr fundefs) ctxt)) ((when err?) (mv err? nil))) (mv nil (append obligs more-obligs)))))
Theorem:
(defthm proof-obligation-listp-of-check-function-definition-list.obligs (b* (((mv ?err? ?obligs) (check-function-definition-list fundefs ctxt))) (proof-obligation-listp obligs)) :rule-classes :rewrite)
Theorem:
(defthm check-function-definition-list-of-function-definition-list-fix-fundefs (equal (check-function-definition-list (function-definition-list-fix fundefs) ctxt) (check-function-definition-list fundefs ctxt)))
Theorem:
(defthm check-function-definition-list-function-definition-list-equiv-congruence-on-fundefs (implies (function-definition-list-equiv fundefs fundefs-equiv) (equal (check-function-definition-list fundefs ctxt) (check-function-definition-list fundefs-equiv ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-function-definition-list-of-context-fix-ctxt (equal (check-function-definition-list fundefs (context-fix ctxt)) (check-function-definition-list fundefs ctxt)))
Theorem:
(defthm check-function-definition-list-context-equiv-congruence-on-ctxt (implies (context-equiv ctxt ctxt-equiv) (equal (check-function-definition-list fundefs ctxt) (check-function-definition-list fundefs ctxt-equiv))) :rule-classes :congruence)