Filtering...

find-subterms

books/clause-processors/find-subterms
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))))))