		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-gen-shallow-fndef-method

Generate a Java method with the given types for an ACL2 function definition.

Signature
(atj-gen-shallow-fndef-method fn fns-that-may-throw fn-type formals body method-name qconsts pkg-class-names fn-method-names curr-pkg mv-typess guards$ no-aij-types$ wrld) → (mv method new-qconsts new-mv-typess)
Arguments: fn — Guard (symbolp fn).; fns-that-may-throw — Guard (symbol-listp fns-that-may-throw).; fn-type — Guard (atj-function-type-p fn-type).; formals — Guard (symbol-listp formals).; body — Guard (pseudo-termp body).; method-name — Guard (stringp method-name).; qconsts — Guard (atj-qconstants-p qconsts).; pkg-class-names — Guard (string-string-alistp pkg-class-names).; fn-method-names — Guard (symbol-string-alistp fn-method-names).; curr-pkg — Guard (stringp curr-pkg).; mv-typess — Guard (atj-type-list-listp mv-typess).; guards$ — Guard (booleanp guards$).; no-aij-types$ — Guard (booleanp no-aij-types$).; wrld — Guard (plist-worldp wrld).
Returns: method — Type (jmethodp method).; new-qconsts — Type (atj-qconstants-p new-qconsts), given (atj-qconstants-p qconsts).; new-mv-typess — Type (and (atj-type-list-listp new-mv-typess) (cons-listp new-mv-typess)).

In the shallow embedding approach, each ACL2 function definition is turned into a Java method. This is a public static method with the same number of parameters as the ACL2 function. More precisely, we generate an overloaded method for each primary and secondary function type associated to the function via atj-main-function-type and atj-other-function-type.

This function generates one such method, based on the (primary or secondary) function type passed as input. First, we pre-translate the function. Then, we translate the pre-translated function to a Java method. Finally, we post-translate the Java method.

We also collect all the quoted constants in the pre-translated function body, and add it to the collection that it threaded through.

The formals and body of the function, as well as the method name, are the same for all the overloaded methods, so they are calculated once and passed to this function. However, the generation of the Java method (pre-translation, translation, and post-translation) must be done afresh for each overloaded methods, because it is affected by the function types, which are turned into the method's argument and result types: with different types, there may be different type annotations, and in particular different type conversions. In fact, it is expected that, with narrower types, there will be fewer type conversions. The pre-translation steps before the type annotation step could be actually factored out and done once, but for greater implementation simplicity here we repeat them for every overloaded method.

We collect all the mv types in the body for which we will need to generate mv classes.

Definitions and Theorems

Function: atj-gen-shallow-fndef-method

(defun atj-gen-shallow-fndef-method
       (fn fns-that-may-throw
           fn-type formals body method-name qconsts
           pkg-class-names fn-method-names curr-pkg
           mv-typess guards$ no-aij-types$ wrld)
 (declare (xargs :guard (and (symbolp fn)
                             (symbol-listp fns-that-may-throw)
                             (atj-function-type-p fn-type)
                             (symbol-listp formals)
                             (pseudo-termp body)
                             (stringp method-name)
                             (atj-qconstants-p qconsts)
                             (string-string-alistp pkg-class-names)
                             (symbol-string-alistp fn-method-names)
                             (stringp curr-pkg)
                             (atj-type-list-listp mv-typess)
                             (booleanp guards$)
                             (booleanp no-aij-types$)
                             (plist-worldp wrld))))
 (declare (xargs :guard (and (not (aij-nativep fn))
                             (not (equal curr-pkg ""))
                             (cons-listp mv-typess))))
 (let ((__function__ 'atj-gen-shallow-fndef-method))
  (declare (ignorable __function__))
  (b*
   ((in-types (atj-function-type->inputs fn-type))
    (out-types (atj-function-type->outputs fn-type))
    (out-arrays (atj-function-type->arrays fn-type))
    ((unless (= (len in-types) (len formals)))
     (raise
      "Internal error: ~
                the number ~x0 of parameters of ~x1 ~
                does not match the number ~x2 of input types of ~x1."
      (len formals)
      fn (len in-types))
     (mv (ec-call (jmethod-fix :irrelevant))
         qconsts nil))
    ((unless (consp out-types))
     (raise "Internal error: no output types ~x0 for ~x1."
            out-types fn)
     (mv (ec-call (jmethod-fix :irrelevant))
         qconsts nil))
    ((mv formals body mv-typess)
     (atj-pre-translate fn formals body
                        in-types out-types out-arrays mv-typess
                        nil guards$ no-aij-types$ wrld))
    (qconsts (atj-add-qconstants-in-term body qconsts))
    ((mv formals &)
     (atj-unmark-vars formals))
    (formals (atj-type-unannotate-vars formals))
    (method-params
        (atj-gen-paramlist (symbol-name-lst formals)
                           (atj-type-list-to-jitype-list in-types)))
    ((mv body-block body-expr &)
     (atj-gen-shallow-term body
                           "$tmp" 1 pkg-class-names fn-method-names
                           curr-pkg (atj-qconstants->pairs qconsts)
                           guards$ wrld))
    (method-body (append body-block (jblock-return body-expr)))
    (tailrecp (and (logicp fn wrld)
                   (= 1 (len (irecursivep fn wrld)))
                   (tail-recursive-p fn wrld)))
    (method-body
       (atj-post-translate-body method-name
                                method-params method-body tailrecp))
    ((unless (consp out-types))
     (raise
      "Internal error: ~
                the function ~x0 has no output types ~x1."
      fn out-types)
     (mv (ec-call (jmethod-fix :irrelevant))
         qconsts nil))
    (out-jtype (atj-gen-shallow-jtype out-types))
    (throws (and (member-eq fn fns-that-may-throw)
                 (list *aij-class-undef-pkg-exc*)))
    (method (make-jmethod :access (jaccess-public)
                          :abstract? nil
                          :static? t
                          :final? nil
                          :synchronized? nil
                          :native? nil
                          :strictfp? nil
                          :result (jresult-type out-jtype)
                          :name method-name
                          :params method-params
                          :throws throws
                          :body method-body)))
   (mv method qconsts mv-typess))))

Theorem: jmethodp-of-atj-gen-shallow-fndef-method.method

(defthm jmethodp-of-atj-gen-shallow-fndef-method.method
  (b* (((mv common-lisp::?method
            ?new-qconsts ?new-mv-typess)
        (atj-gen-shallow-fndef-method
             fn fns-that-may-throw
             fn-type formals body method-name qconsts
             pkg-class-names fn-method-names curr-pkg
             mv-typess guards$ no-aij-types$ wrld)))
    (jmethodp method))
  :rule-classes :rewrite)

Theorem: atj-qconstants-p-of-atj-gen-shallow-fndef-method.new-qconsts

(defthm atj-qconstants-p-of-atj-gen-shallow-fndef-method.new-qconsts
  (implies (atj-qconstants-p qconsts)
           (b* (((mv common-lisp::?method
                     ?new-qconsts ?new-mv-typess)
                 (atj-gen-shallow-fndef-method
                      fn fns-that-may-throw
                      fn-type formals body method-name qconsts
                      pkg-class-names fn-method-names curr-pkg
                      mv-typess guards$ no-aij-types$ wrld)))
             (atj-qconstants-p new-qconsts)))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-gen-shallow-fndef-method.new-mv-typess

(defthm return-type-of-atj-gen-shallow-fndef-method.new-mv-typess
  (b* (((mv common-lisp::?method
            ?new-qconsts ?new-mv-typess)
        (atj-gen-shallow-fndef-method
             fn fns-that-may-throw
             fn-type formals body method-name qconsts
             pkg-class-names fn-method-names curr-pkg
             mv-typess guards$ no-aij-types$ wrld)))
    (and (atj-type-list-listp new-mv-typess)
         (cons-listp new-mv-typess)))
  :rule-classes :rewrite)