		Search-engine friendly clone of the ACL2 documentation.

Atj-deep-code-generation

Atj-gen-deep-build-method

Generate the method to build the ACL2 environment, in the deep embedding approach.

Signature
(atj-gen-deep-build-method pkgs fns) → method
Arguments: pkgs — Guard (string-listp pkgs).; fns — Guard (symbol-listp fns).
Returns: method — Type (jmethodp method).

This is a package-private static method in the environment Java class. This method is called by the static initializer of the main Java class.

This method builds the Java representation of the ACL2 packages and functions.

Definitions and Theorems

Function: atj-gen-deep-build-method

(defun atj-gen-deep-build-method (pkgs fns)
 (declare (xargs :guard (and (string-listp pkgs)
                             (symbol-listp fns))))
 (let ((__function__ 'atj-gen-deep-build-method))
  (declare (ignorable __function__))
  (b*
   ((body (append (atj-gen-pkgs pkgs)
                  (atj-gen-deep-fndefs fns)
                  (jblock-smethod *aij-type-named-fn*
                                  "validateAllFunctionCalls" nil))))
   (make-jmethod :access (jaccess-default)
                 :abstract? nil
                 :static? t
                 :final? nil
                 :synchronized? nil
                 :native? nil
                 :strictfp? nil
                 :result (jresult-void)
                 :name "build"
                 :params nil
                 :throws nil
                 :body body))))

Theorem: jmethodp-of-atj-gen-deep-build-method

(defthm jmethodp-of-atj-gen-deep-build-method
  (b* ((method (atj-gen-deep-build-method pkgs fns)))
    (jmethodp method))
  :rule-classes :rewrite)