		Search-engine friendly clone of the ACL2 documentation.

Std/system/function-queries

Recursive-calls

Recursive calls of a named non-mutually-recursive function, along with the controlling tests.

Signature
(recursive-calls fn wrld) → calls-with-tests
Arguments: fn — Guard (symbolp fn).; wrld — Guard (plist-worldp wrld).
Returns: calls-with-tests — A pseudo-tests-and-call-listp.

For singly recursive logic-mode functions, this is similar to the result of induction-machine, but each record has one recursive call (instead of zero or more), and there is exactly one record for each recursive call.

This utility works on both logic-mode and program-mode functions (if the program-mode functions have an unnormalized-body property). This utility should not be called on a function that is mutually recursive with other functions; it must be called only on singly recursive functions, or on non-recursive functions (the result is nil in this case).

This utility may be extended to handle also mutually recursive functions.

If the function is in logic mode and recursive, we obtain its ruler extenders and pass them to the built-in function termination-machine. Otherwise, we pass the default ruler extenders.

Definitions and Theorems

Function: recursive-calls

(defun recursive-calls (fn wrld)
  (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld))))
  (let ((__function__ 'recursive-calls))
    (declare (ignorable __function__))
    (b* ((ruler-extenders (if (and (logicp fn wrld)
                                   (irecursivep fn wrld))
                              (ruler-extenders fn wrld)
                            (default-ruler-extenders wrld))))
      (termination-machine nil nil (list fn)
                           nil (ubody fn wrld)
                           nil nil ruler-extenders))))