		Search-engine friendly clone of the ACL2 documentation.

Soft-implementation-core

Funvars-of-plain-fn

Function variables depended on by a plain second-order function or by an instance of it.

Signature
(funvars-of-plain-fn fun wrld) → funvars
Arguments: fun — Guard (symbolp fun).; wrld — Guard (plist-worldp wrld).
Returns: funvars — A funvar-listp.

Plain second-order functions and their instances may depend on function variables via their defining bodies, via their measures (absent in non-recursive functions), and via their guards. For now recursive second-order functions (which are all plain) and their instances are only allowed to use o< as their well-founded relation, and so plain second-order functions and their instances may not depend on function variables via their well-founded relations.

Note that if the function is recursive, the variable measure in the following code is nil, and funvars-of-term applied to that yields nil.

The returned list may contain duplicates.

Definitions and Theorems

Function: funvars-of-plain-fn

(defun funvars-of-plain-fn (fun wrld)
  (declare (xargs :guard (and (symbolp fun)
                              (plist-worldp wrld))))
  (let ((__function__ 'funvars-of-plain-fn))
    (declare (ignorable __function__))
    (let* ((body (ubody fun wrld))
           (measure (if (recursivep fun nil wrld)
                        (get-measure fun wrld)
                      nil))
           (guard (uguard fun wrld))
           (body-funvars (funvars-of-term body wrld))
           (measure-funvars (funvars-of-term measure wrld))
           (guard-funvars (funvars-of-term guard wrld)))
      (append body-funvars
              measure-funvars guard-funvars))))