		Search-engine friendly clone of the ACL2 documentation.

Atj-deep-code-generation

Atj-gen-deep-call-method

Generate the Java method to call ACL2 functions, in the deep embedding approach.

Signature
(atj-gen-deep-call-method) → method
Returns: method — Type (jmethodp method).

This is a public static method, which provides the means for external Java code to call the deeply embedded Java representations of ACL2 functions.

Definitions and Theorems

Function: atj-gen-deep-call-method

(defun atj-gen-deep-call-method nil
 (declare (xargs :guard t))
 (let ((__function__ 'atj-gen-deep-call-method))
   (declare (ignorable __function__))
   (b* ((method-param-function (make-jparam :final? nil
                                            :type *aij-type-symbol*
                                            :name "function"))
        (method-param-arguments
             (make-jparam :final? nil
                          :type (jtype-array *aij-type-value*)
                          :name "arguments"))
        (method-params (list method-param-function
                             method-param-arguments))
        (function-expr
             (jexpr-smethod *aij-type-named-fn*
                            "make" (list (jexpr-name "function"))))
        (call-expr
             (jexpr-imethod function-expr
                            "call" (list (jexpr-name "arguments"))))
        (method-body (jblock-return call-expr)))
     (make-jmethod :access (jaccess-public)
                   :abstract? nil
                   :static? t
                   :final? nil
                   :synchronized? nil
                   :native? nil
                   :strictfp? nil
                   :result (jresult-type *aij-type-value*)
                   :name "call"
                   :params method-params
                   :throws (list *aij-class-undef-pkg-exc*)
                   :body method-body))))

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

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