		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Get-function-definition

Find the definition of a function with a given name in a list of top-level constructs.

Signature
(get-function-definition name tops) → fundef?
Arguments: name — Guard (identifierp name).; tops — Guard (toplevel-listp tops).
Returns: fundef? — Type (maybe-function-definitionp fundef?).

We look both at the function definitions at the top level and at the function definitions inside the function recursions.

We return nil if the function definition is not found.

We look up the top-level constructs in order. In well-formed lists of top-level constructs, the defined function names are unique, so any order would yield the same result.

Definitions and Theorems

Function: get-function-definition

(defun get-function-definition (name tops)
 (declare (xargs :guard (and (identifierp name)
                             (toplevel-listp tops))))
 (let ((__function__ 'get-function-definition))
  (declare (ignorable __function__))
  (b* (((when (endp tops)) nil)
       (top (car tops)))
   (toplevel-case
    top :type
    (get-function-definition name (cdr tops))
    :types
    (get-function-definition name (cdr tops))
    :function
    (if
     (identifier-equiv
      name
      (function-header->name (function-definition->header top.get)))
     top.get
     (get-function-definition name (cdr tops)))
    :functions
    (b* ((fundef? (get-function-definition-in-function-definitions
                       name
                       (function-recursion->definitions top.get))))
      (or fundef?
          (get-function-definition name (cdr tops))))
    :specification (get-function-definition name (cdr tops))
    :theorem (get-function-definition name (cdr tops))
    :transform (get-function-definition name (cdr tops))))))

Theorem: maybe-function-definitionp-of-get-function-definition

(defthm maybe-function-definitionp-of-get-function-definition
  (b* ((fundef? (get-function-definition name tops)))
    (maybe-function-definitionp fundef?))
  :rule-classes :rewrite)

Theorem: get-function-definition-of-identifier-fix-name

(defthm get-function-definition-of-identifier-fix-name
  (equal (get-function-definition (identifier-fix name)
                                  tops)
         (get-function-definition name tops)))

Theorem: get-function-definition-identifier-equiv-congruence-on-name

(defthm get-function-definition-identifier-equiv-congruence-on-name
  (implies (identifier-equiv name name-equiv)
           (equal (get-function-definition name tops)
                  (get-function-definition name-equiv tops)))
  :rule-classes :congruence)

Theorem: get-function-definition-of-toplevel-list-fix-tops

(defthm get-function-definition-of-toplevel-list-fix-tops
  (equal (get-function-definition name (toplevel-list-fix tops))
         (get-function-definition name tops)))

Theorem: get-function-definition-toplevel-list-equiv-congruence-on-tops

(defthm
     get-function-definition-toplevel-list-equiv-congruence-on-tops
  (implies (toplevel-list-equiv tops tops-equiv)
           (equal (get-function-definition name tops)
                  (get-function-definition name tops-equiv)))
  :rule-classes :congruence)