		Search-engine friendly clone of the ACL2 documentation.

Atj-deep-code-generation

Atj-gen-deep-fndefs

Generate Java code to build the deeply embedded ACL2 function definitions.

Signature
(atj-gen-deep-fndefs fns) → block
Arguments: fns — Guard (symbol-listp fns).
Returns: block — Type (jblockp block).

This is a sequence of calls to the methods generated by atj-gen-deep-fndef-methods. These calls are part of the code that initializes (the Java representation of) the ACL2 environment.

Definitions and Theorems

Function: atj-gen-deep-fndefs

(defun atj-gen-deep-fndefs (fns)
  (declare (xargs :guard (symbol-listp fns)))
  (let ((__function__ 'atj-gen-deep-fndefs))
    (declare (ignorable __function__))
    (if (endp fns)
        nil
      (b* ((method-name (atj-gen-deep-fndef-method-name (car fns)))
           (first-block (jblock-method method-name nil))
           (rest-block (atj-gen-deep-fndefs (cdr fns))))
        (append first-block rest-block)))))

Theorem: jblockp-of-atj-gen-deep-fndefs

(defthm jblockp-of-atj-gen-deep-fndefs
  (b* ((block (atj-gen-deep-fndefs fns)))
    (jblockp block))
  :rule-classes :rewrite)