Recursive calls of a named non-mutually-recursive function, along with the controlling tests.
(recursive-calls fn wrld) → calls-with-tests
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
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
(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))))