other
(in-package "ACL2")
find-callmutual-recursion
(mutual-recursion (defun find-call (fn x) (declare (xargs :guard (and (symbolp fn) (pseudo-termp x)))) (cond ((or (variablep x) (fquotep x)) nil) ((eq fn (car x)) x) (t (find-call-lst fn (cdr x))))) (defun find-call-lst (fn x) (declare (xargs :guard (and (symbolp fn) (pseudo-term-listp x)))) (if (endp x) nil (or (find-call fn (car x)) (find-call-lst fn (cdr x))))))
find-callsmutual-recursion
(mutual-recursion (defun find-calls (fn x) (declare (xargs :guard (and (symbolp fn) (pseudo-termp x)))) (cond ((or (variablep x) (fquotep x)) nil) ((eq fn (car x)) (cons x (find-calls-lst fn (cdr x)))) (t (find-calls-lst fn (cdr x))))) (defun find-calls-lst (fn x) (declare (xargs :guard (and (symbolp fn) (pseudo-term-listp x)))) (if (endp x) nil (append (find-calls fn (car x)) (find-calls-lst fn (cdr x))))))
find-calls-of-fnsmutual-recursion
(mutual-recursion (defun find-calls-of-fns (fns x) (declare (xargs :guard (and (symbol-listp fns) (pseudo-termp x)))) (cond ((or (variablep x) (fquotep x)) nil) ((member (car x) fns) (cons x (find-calls-of-fns-lst fns (cdr x)))) (t (find-calls-of-fns-lst fns (cdr x))))) (defun find-calls-of-fns-lst (fns x) (declare (xargs :guard (and (symbol-listp fns) (pseudo-term-listp x)))) (if (endp x) nil (append (find-calls-of-fns fns (car x)) (find-calls-of-fns-lst fns (cdr x))))))