		Search-engine friendly clone of the ACL2 documentation.

Atj-library-extensions

Atj-fn-body

Return the unnormalized body or attachment of a function.

Signature
(atj-fn-body fn wrld) → body
Arguments: fn — Guard (symbolp fn).; wrld — Guard (plist-worldp wrld).
Returns: body — Type (pseudo-termp body).

This function extends ubody+ as follows: if fn has no unnormalized body, but it has an attachment fn2, we consider (fn2 x1 ... xn) to be the body of fn, where x1, ..., xn are the formals of fn. For the purpose of ATJ's code generation, the attachment of fn2 to fn is equivalent to fn2 being defined to call fn with the same arguments.

The attachment is in the acl2::attachment property of fn. The property has the form ((fn . fn2)). If the property is absent or does not have this form, fn is regarded as not being defined, and ATJ will stop because it cannot generate code for it.

Definitions and Theorems

Function: atj-fn-body

(defun atj-fn-body (fn wrld)
  (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld))))
  (let ((__function__ 'atj-fn-body))
    (declare (ignorable __function__))
    (b* ((ubody (ubody+ fn wrld))
         ((when ubody) ubody)
         (attachment (getpropc fn 'acl2::attachment
                               nil wrld))
         ((unless (tuplep 1 attachment)) nil)
         (element (car attachment)))
      (if (and (consp element)
               (eq (car element) fn)
               (symbolp (cdr element))
               (not (eq (cdr element) 'quote)))
          (fcons-term (cdr element)
                      (formals+ fn wrld))
        nil))))

Theorem: pseudo-termp-of-atj-fn-body

(defthm pseudo-termp-of-atj-fn-body
  (b* ((body (atj-fn-body fn wrld)))
    (pseudo-termp body))
  :rule-classes :rewrite)