		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-gen-shallow-synonym-method

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

Signature
(atj-gen-shallow-synonym-method fn fns-that-may-throw fn-type pkg-class-names fn-method-names wrld) → method
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).; pkg-class-names — Guard (string-string-alistp pkg-class-names).; fn-method-names — Guard (symbol-string-alistp fn-method-names).; wrld — Guard (plist-worldp wrld).
Returns: method — Type (jmethodp method).

This is used to mimic, as far as name references are concerned, the importing of a function symbol in a package.

For instance, the built-in cons is in the "COMMON-LISP" package (i.e. that is its symbol-package-name), but that symbol is imported by the "ACL2" package, making it referenceable as acl2::cons besides the ``canonical'' common-lisp::cons. In particular, in the "ACL2" package it can be referenced as just cons, which makes ACL2 code much more readable.

In the shallow embedding, we translate these two ACL2 packages to two different Java classes, and the method that corresponds to cons is declared in the class for "COMMON-LISP", where the method can be referenced by simple name, without qualifying it with the class name. But in classes for other packages, e.g. the class for "ACL2", it would have to be qualified.

To avoid this verbosity, we generate a ``synonym'' of the method for cons in each class of a package that imports cons, e.g. in the class for "ACL2". This function generates this synonym method, which is just defined to call the method in the class of its proper package. This makes the generated Java code much more readable. It is hoped that the JVM JIT may optimize the indirection away.

The fn parameter is the name of the ACL2 function in question, e.g. cons in the example above.

We pass the symbol-package-name of fn to atj-gen-shallow-fnname to ensure that the result is the simple name of the method, which goes into the generated method declaration.

Recall that, for each ACL2 function, we generate as many overloaded Java methods as the number of primary and secondary types of the function. Accordingly, we must generate the same number of overloaded methods for the function synonyms. This function generates the overloaded method for the function type passed as argument.

Definitions and Theorems

Function: atj-gen-shallow-synonym-method

(defun atj-gen-shallow-synonym-method
       (fn fns-that-may-throw fn-type
           pkg-class-names fn-method-names wrld)
 (declare (xargs :guard (and (symbolp fn)
                             (symbol-listp fns-that-may-throw)
                             (atj-function-type-p fn-type)
                             (string-string-alistp pkg-class-names)
                             (symbol-string-alistp fn-method-names)
                             (plist-worldp wrld))))
 (let ((__function__ 'atj-gen-shallow-synonym-method))
  (declare (ignorable __function__))
  (b*
   ((in-types (atj-function-type->inputs fn-type))
    (out-types (atj-function-type->outputs fn-type))
    ((unless (consp out-types))
     (raise
      "Internal error: ~
                the function ~x0 has no output types ~x1."
      fn out-types)
     (ec-call (jmethod-fix :irrelevant)))
    (out-jtype (atj-gen-shallow-jtype out-types))
    (fn-pkg (symbol-package-name fn))
    (method-name (atj-gen-shallow-fnname
                      fn
                      pkg-class-names fn-method-names fn-pkg))
    (method-param-names
         (atj-gen-shallow-synonym-method-params (arity+ fn wrld)))
    ((unless (= (len method-param-names)
                (len in-types)))
     (raise
      "Internal error: ~
                the number ~x0 of input types of ~x1 ~
                differs from the arity ~x2 of ~x1."
      (len in-types)
      fn (len method-param-names))
     (ec-call (jmethod-fix :irrelevant)))
    (method-params
        (atj-gen-paramlist method-param-names
                           (atj-type-list-to-jitype-list in-types)))
    (class (atj-get-pkg-class-name fn-pkg pkg-class-names))
    (method-body
         (jblock-return
              (jexpr-smethod (jtype-class class)
                             method-name
                             (jexpr-name-list method-param-names))))
    (throws (and (member-eq fn fns-that-may-throw)
                 (list *aij-class-undef-pkg-exc*))))
   (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))))

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

(defthm jmethodp-of-atj-gen-shallow-synonym-method
  (b* ((method (atj-gen-shallow-synonym-method
                    fn fns-that-may-throw fn-type
                    pkg-class-names fn-method-names wrld)))
    (jmethodp method))
  :rule-classes :rewrite)