Generate a Java method with the given types for an ACL2 function synonym.
(atj-gen-shallow-synonym-method fn fns-that-may-throw fn-type pkg-class-names fn-method-names wrld) → 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
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
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
The
We pass the symbol-package-name of
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.
Function:
(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:
(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)