Atj-var-to-jvar
Turn an ACL2 variable into a Java variable.
- Signature
(atj-var-to-jvar var curr-pkg vars-by-name) → jvar
- Arguments
- var — Guard (symbolp var).
- curr-pkg — Guard (stringp curr-pkg).
- vars-by-name — Guard (string-symbollist-alistp vars-by-name).
- Returns
- jvar — Type (symbolp jvar).
If var has name name and package name pname,
in general we return the symbol java::<pname>$$<name>,
where <pname> and <name> are representations of the ACL2 names
that are valid for Java identifiers.
This is not necessarily the final name of the Java variable:
in general, a numeric index is added at the end,
via atj-var-add-index.
So the final name of the Java variable has generally the form
java::<pname>$$<name>$<index>.
Back to this function, which just produces java::<pname>$$<name>,
note that the package of the new symbol is always "JAVA".
Other choices are possible, but the point is that we want to ignore it.
We incorporate the original package name pname
into the new symbol name and deal with just the symbol name afterwards,
for greater simplicity.
If this package is ever changed,
it must be changed accordingly in *atj-init-indices*.
Systematically prefixing, in the generated Java variables,
every symbol name with the package prefix affects readability.
In ACL2, package prefixes are normally omitted
for symbols in the current ACL2 package.
Here we do something similar for the Java variable names,
where the notion of current package is as follows:
in the shallow embedding approach,
each ACL2 function is turned into a Java method,
and this method is inside a Java class whose name is derived from
the ACL2 package name of the function name;
thus, the ``current package'' in this context is
the one of the function name, which is the curr-pkg parameter.
If <pname> is the same as the current package,
we omit <pname>$$.
We omit <pname>$$ also when the variable
is the only one with name <name>
within the ``current'' ACL2 function:
since the scope of Java method parameters and local variables
is limited to the method where they occur,
no naming conflict may arise in this case.
The parameter vars-by-name consists of
all the variables in the current ACL2 function,
organized by symbol name for easy lookup.
We retrieve the variables with the same name of the variable,
we remove the variable being processed from them,
and we check if the result is empty:
in this case, this is the only variable with that name.
The reason why we use a double $$ instead of a single $,
to separate <pname> from <name>,
is to avoid a possible name conflict
in case <name> happens to be
one of the escape descriptions discussed in atj-char-to-jchars-id:
a variable |p!X| in the current package
and a variable P::bangX in a different package
would both be turned into P$BANGx.
We call atj-chars-to-jchars-id to create
<pname> and <name> from pname and name.
If there is a package prefix, the startp flag is t
only for pname, but not for name,
because <name> is not the start of the Java identifier.
Otherwise, startp is t for name
if there is no package prefix.
The variable var passed to this function
is without markings or annotations. The caller removes them before calling this function.
Definitions and Theorems
Function: atj-var-to-jvar
(defun atj-var-to-jvar (var curr-pkg vars-by-name)
(declare
(xargs :guard (and (symbolp var)
(stringp curr-pkg)
(string-symbollist-alistp vars-by-name))))
(let ((__function__ 'atj-var-to-jvar))
(declare (ignorable __function__))
(b*
((pname (symbol-package-name var))
(name (symbol-name var))
(omit-pname?
(or (equal pname curr-pkg)
(null (remove-eq var
(cdr (assoc-equal name vars-by-name))))))
(pname$$-jchars
(if omit-pname? nil
(append (atj-chars-to-jchars-id (explode pname)
t
:dash t)
(list #\$ #\$))))
(name-jchars (atj-chars-to-jchars-id (explode name)
(endp pname$$-jchars)
:dash t))
(jchars (append pname$$-jchars name-jchars))
(new-name (implode jchars))
(new-var (intern$ new-name "JAVA")))
new-var)))
Theorem: symbolp-of-atj-var-to-jvar
(defthm symbolp-of-atj-var-to-jvar
(b* ((jvar (atj-var-to-jvar var curr-pkg vars-by-name)))
(symbolp jvar))
:rule-classes :rewrite)
