		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-gen-shallow-build-method

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

Signature
(atj-gen-shallow-build-method pkgs) → method
Arguments: pkgs — Guard (string-listp pkgs).
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.

Definitions and Theorems

Function: atj-gen-shallow-build-method

(defun atj-gen-shallow-build-method (pkgs)
  (declare (xargs :guard (string-listp pkgs)))
  (let ((__function__ 'atj-gen-shallow-build-method))
    (declare (ignorable __function__))
    (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 (atj-gen-pkgs pkgs))))

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

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