		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-function-recursion

Check if a function recursion is statically well-formed.

Signature
(check-function-recursion funrec ctxt) → (mv err? obligs)
Arguments: funrec — Guard (function-recursionp funrec).; ctxt — Guard (contextp ctxt).
Returns: obligs — Type (proof-obligation-listp obligs).

This is always at the top level, so the context has no types or functions being defined, no variables in scope, and no obligation variables and hypotheses.

We ensure that there are at least two functions, otherwise it would not be a mutual recursion. We also ensure that the function names are all distinct. We add the headers to the context and check all the definitions.

Definitions and Theorems

Function: check-function-recursion

(defun check-function-recursion (funrec ctxt)
 (declare (xargs :guard (and (function-recursionp funrec)
                             (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-function-recursion))
   (declare (ignorable __function__))
   (b*
    ((fundefs (function-recursion->definitions funrec))
     (headers (function-definition-list->header-list fundefs))
     (names (function-header-list->name-list headers))
     ((unless (>= (len names) 2))
      (mv (list :function-recursion-less-than-two-functions fundefs)
          nil))
     ((unless (no-duplicatesp-equal names))
      (mv (list :duplicate-recursive-functions names)
          nil))
     (ctxt (change-context ctxt
                           :functions headers)))
    (check-function-definition-list fundefs ctxt))))

Theorem: proof-obligation-listp-of-check-function-recursion.obligs

(defthm proof-obligation-listp-of-check-function-recursion.obligs
  (b* (((mv ?err? ?obligs)
        (check-function-recursion funrec ctxt)))
    (proof-obligation-listp obligs))
  :rule-classes :rewrite)

Theorem: check-function-recursion-of-function-recursion-fix-funrec

(defthm check-function-recursion-of-function-recursion-fix-funrec
  (equal (check-function-recursion (function-recursion-fix funrec)
                                   ctxt)
         (check-function-recursion funrec ctxt)))

Theorem: check-function-recursion-function-recursion-equiv-congruence-on-funrec

(defthm
 check-function-recursion-function-recursion-equiv-congruence-on-funrec
 (implies (function-recursion-equiv funrec funrec-equiv)
          (equal (check-function-recursion funrec ctxt)
                 (check-function-recursion funrec-equiv ctxt)))
 :rule-classes :congruence)

Theorem: check-function-recursion-of-context-fix-ctxt

(defthm check-function-recursion-of-context-fix-ctxt
  (equal (check-function-recursion funrec (context-fix ctxt))
         (check-function-recursion funrec ctxt)))

Theorem: check-function-recursion-context-equiv-congruence-on-ctxt

(defthm check-function-recursion-context-equiv-congruence-on-ctxt
  (implies (context-equiv ctxt ctxt-equiv)
           (equal (check-function-recursion funrec ctxt)
                  (check-function-recursion funrec ctxt-equiv)))
  :rule-classes :congruence)