Atj-name-translation
Translation of ACL2 names to Java names performed by ATJ.
Translating ACL2 to Java involves
translating ACL2 names (of packages, functions, and variables)
to corresponding Java names.
The rules for what constitutes a valid Java name
differ from the rules for what constitutes a valid ACL2 name,
necessitating a non-identity translation mapping.
For certain purposes, we also need to translate ACL2 characters and strings
to (parts of) valid Java identifiers.
The issues here are similar to the ones arising
when converting ACL2 names to Java names.
Subtopics
- Atj-var-to-jvar
- Turn an ACL2 variable into a Java variable.
- Atj-char-to-jchars-id
- Turn an ACL2 character into one or more Java characters
for an ASCII Java identifier.
- Atj-fn-to-method
- Turn an ACL2 function symbol into a Java method name.
- Atj-pkg-to-class
- Turn an ACL2 package name into a Java class name.
- Atj-fns-to-methods
- Generate the mapping from ACL2 function symbols to Java method names.
- *atj-disallowed-class-names*
- Disallowed Java class names.
- Atj-pkgs-to-classes
- Generate the mapping from ACL2 package names to Java class names.
- *atj-predefined-method-names*
- Predefined Java method names for certain ACL2 functions.
- Atj-chars-to-jchars-id
- Lift atj-char-to-jchars-id to lists.
- *atj-disallowed-jvar-names*
- Disallowed Java variable names.
- Atj-get-pkg-class-name
- Retrieve the Java class name for an ACL2 package name
from the mapping, ensuring that the name is present.
- Atj-get-fn-method-name
- Retrieve the Java method name for an ACL2 function name
from the mapping, ensuring that the name is present.
- Atj-var-add-index
- Append a numeric index to a variable.
- *atj-disallowed-method-names*
- Disallowed Java method names.
