Atj-gen-shallow-fnnative-method
Generate a Java method with the given types
for an ACL2 function that is natively implemented in AIJ.
- Signature
(atj-gen-shallow-fnnative-method
fn
fns-that-may-throw fn-type method-name
method-param-names method-body)
→
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).
- method-name — Guard (stringp method-name).
- method-param-names — Guard (string-listp method-param-names).
- method-body — Guard (jblockp method-body).
- Returns
- method — Type (jmethodp method).
AIJ's Acl2NativeFunction class provides native Java implementations
of certain ACL2 functions, as public static Java methods.
Thus, in the shallow embedding approach,
we could translate references to these ACL2 functions
to the names of those public static Java methods.
However, for greater uniformity and readability,
we generate wrapper Java methods
for these natively implemented ACL2 functions.
The names of these methods are constructed in the same way as
the Java methods for the non-natively implemented ACL2 functions.
These methods reside in the Java classes generated for
the ACL2 packages of the ACL2 functions.
For each of these natively implemented ACL2 functions,
Acl2NativeFunction has a corresponding Java method
that takes Acl2Value objects as arguments.
For some of these functions,
Acl2NativeFunction also has overloaded Java methods
that take argument objects of narrower types
that correspond to the primary and (if present) secondary ATJ types
associated to the ACL2 function via the macros
atj-main-function-type and
atj-other-function-type.
For the natively implemented functions that return booleans,
Acl2NativeFunction also has Java methods that return
the primitive Java type boolean instead of Acl2Symbol;
these are not overloaded, they have different names
(that end with Boolean).
These boolean-returning methods are
alternatives to the Acl2Symbol-returning ones,
which are selected when :guards is t;
see atj-fnnative-method-name.
We generate a wrapper method for each such overloaded method
(or its boolean-returning alternative; see above):
the argument and return types of the wrapper method
are the same as the ones of the wrapped method in Acl2NativeFunction.
This function generates one of these methods,
as determined by the function type supplied as input.
The types are the only thing that varies across the wrapper methods:
their names, bodies, and other attributes are all the same;
thus, these are calculated once and passed as inputs to this function.
Note that the bodies of the wrapper methods automatically call
different methods in Acl2NativeFunction based on the types;
the called methods are resolved by the Java compiler.
Definitions and Theorems
Function: atj-gen-shallow-fnnative-method
(defun atj-gen-shallow-fnnative-method
(fn fns-that-may-throw fn-type method-name
method-param-names method-body)
(declare (xargs :guard (and (symbolp fn)
(symbol-listp fns-that-may-throw)
(atj-function-type-p fn-type)
(stringp method-name)
(string-listp method-param-names)
(jblockp method-body))))
(declare (xargs :guard (aij-nativep fn)))
(let ((__function__ 'atj-gen-shallow-fnnative-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))
((unless (= (len in-types)
(len method-param-names)))
(raise
"Internal error: ~
the number ~x0 of input types for ~x1 ~
differs from the number ~x2 of calculated method arguments."
(len in-types)
fn (len method-param-names))
(ec-call (jmethod-fix :irrelevant)))
(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
(atj-gen-paramlist method-param-names
(atj-type-list-to-jitype-list in-types))
:throws throws
:body method-body))))
Theorem: jmethodp-of-atj-gen-shallow-fnnative-method
(defthm jmethodp-of-atj-gen-shallow-fnnative-method
(b* ((method (atj-gen-shallow-fnnative-method
fn
fns-that-may-throw fn-type method-name
method-param-names method-body)))
(jmethodp method))
:rule-classes :rewrite)