		Search-engine friendly clone of the ACL2 documentation.

Atj-deep-code-generation

Atj-gen-deep-fndef-method

Generate a Java method that builds a deeply embedded ACL2 function definition.

Signature
(atj-gen-deep-fndef-method fn guards$ verbose$ wrld) → method
Arguments: fn — Guard (symbolp fn).; guards$ — Guard (booleanp guards$).; verbose$ — Guard (booleanp verbose$).; wrld — Guard (plist-worldp wrld).
Returns: method — Type (jmethodp method).

This is a private static method that contains a sequence of statements to store the function's name into a local variable, store an array of the function's formal arguments into a local variable, store the function's body into a local variable, and use these local variables to add the function's definition.

If the :guards input is t, we remove all the :logic parts of mbes; if the :guards input is nil, we remove all the :exec parts of mbes. We also remove all the non-last arguments of prog2$s and progn$s. This should remove any occurrences of return-last. See this discussion for background.

The indices of the local variables to build values, terms, and lambda expressions are all reset to 1, because each function definition is built in its own method (thus, there are no cross-references).

Definitions and Theorems

Function: atj-gen-deep-fndef-method

(defun atj-gen-deep-fndef-method (fn guards$ verbose$ wrld)
 (declare (xargs :guard (and (symbolp fn)
                             (booleanp guards$)
                             (booleanp verbose$)
                             (plist-worldp wrld))))
 (let ((__function__ 'atj-gen-deep-fndef-method))
  (declare (ignorable __function__))
  (b*
   (((run-when verbose$) (cw "  ~s0~%" fn))
    (method-name (atj-gen-deep-fndef-method-name fn))
    (jvar-function "function")
    (jvar-formals "formals")
    (jvar-body "body")
    (formals (formals+ fn wrld))
    (body (atj-fn-body fn wrld))
    (in-types (repeat (len formals)
                      (atj-type-acl2 (atj-atype-value))))
    (out-types (list (atj-type-acl2 (atj-atype-value))))
    (out-arrays (list nil))
    ((mv formals body &)
     (atj-pre-translate fn formals body in-types out-types
                        out-arrays nil t guards$ nil wrld))
    (fn-block
         (jblock-locvar
              *aij-type-named-fn* jvar-function
              (jexpr-smethod *aij-type-named-fn* "make"
                             (list (atj-gen-symbol fn t nil)))))
    (formals-block (jblock-locvar (jtype-array *aij-type-symbol*)
                                  jvar-formals
                                  (atj-gen-deep-formals formals)))
    ((mv body-block body-expr & & &)
     (atj-gen-deep-term body
                        "value" 1 "term" 1 "lambda" 1 guards$))
    (body-block
       (append body-block
               (jblock-locvar *aij-type-term* jvar-body body-expr)))
    (def-block (jblock-method (str::cat jvar-function ".define")
                              (list (jexpr-name jvar-formals)
                                    (jexpr-name jvar-body))))
    (method-body (append fn-block
                         formals-block body-block def-block)))
   (make-jmethod :access (jaccess-private)
                 :abstract? nil
                 :static? t
                 :final? nil
                 :synchronized? nil
                 :native? nil
                 :strictfp? nil
                 :result (jresult-void)
                 :name method-name
                 :params nil
                 :throws nil
                 :body method-body))))

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

(defthm jmethodp-of-atj-gen-deep-fndef-method
 (b* ((method (atj-gen-deep-fndef-method fn guards$ verbose$ wrld)))
   (jmethodp method))
 :rule-classes :rewrite)