## MUTUAL-RECURSION

define some mutually recursive functions
```Major Section:  EVENTS
```

```Example:
(mutual-recursion
(defun evenlp (x)
(if (consp x) (oddlp (cdr x)) t))
(defun oddlp (x)
(if (consp x) (evenlp (cdr x)) nil)))

General Form:
(mutual-recursion def1 ... defn)
where each defi is a DEFUN form.
```
When mutually recursive functions are introduced it is necessary to do the termination analysis on the entire clique of definitions. Each `defun` form specifies its own measure, either with the `:measure` keyword `xarg` (see xargs) or by default to `acl2-count`. When a function in the clique calls a function in the clique, the measure of the callee's actuals must be smaller than the measure of the caller's formals -- just as in the case of a simply recursive function. But with mutual recursion, the callee's actuals are measured as specified by the callee's `defun` while the caller's formals are measured as specified by the caller's `defun`. These two measures may be different but must be comparable in the sense that `e0-ord-<` decreases through calls.

The `guard` analysis must also be done for all of the functions at the same time. If any one of the `defun`s specifies the `:``verify-guards` `xarg` to be `nil`, then guard verification is omitted for all of the functions.

Technical Note: Each `defi` above must be of the form `(defun ...)`. In particular, it is not permitted for a `defi` to be a form that will macroexpand into a `defun` form. This is because `mutual-recursion` is itself a macro, and since macroexpansion occurs from the outside in, at the time `(mutual-recursion def1 ... defk)` is expanded the `defi` have not yet been. But `mutual-recursion` must decompose the `defi`. We therefore insist that they be explicitly presented as `defun`s.

Suppose you have defined your own `defun`-like macro and wish to use it in a `mutual-recursion` expression. Well, you can't. (!) But you can define your own version of `mutual-recursion` that allows your `defun`-like form. Here is an example. Suppose you define

```(defmacro my-defun (&rest args) (my-defun-fn args))
```
where `my-defun-fn` takes the arguments of the `my-defun` form and produces from them a `defun` form. As noted above, you are not allowed to write `(mutual-recursion (my-defun ...) ...)`. But you can define the macro `my-mutual-recursion` so that
```(my-mutual-recursion (my-defun ...) ... (my-defun ...))
```
expands into `(mutual-recursion (defun ...) ... (defun ...))` by applying `my-defun-fn` to each of the arguments of `my-mutual-recursion`.
```(defun my-mutual-recursion-fn (lst)
(declare (xargs :guard (alistp lst)))

; Each element of lst must be a consp (whose car, we assume, is always
; MY-DEFUN).  We apply my-defun-fn to the arguments of each element and
; collect the resulting list of DEFUNs.

(cond ((atom lst) nil)
(t (cons (my-defun-fn (cdr (car lst)))
(my-mutual-recursion-fn (cdr lst))))))

(defmacro my-mutual-recursion (&rest lst)

; Each element of lst must be a consp (whose car, we assume, is always
; MY-DEFUN).  We obtain the DEFUN corresponding to each and list them
; all inside a MUTUAL-RECURSION form.

(declare (xargs :guard (alistp lst)))
(cons 'mutual-recursion (my-mutual-recursion-fn lst))).
```