Atj-tutorial-customization
ATJ tutorial: Customization Options for Generated Code.
ATJ provides some options to customize the generated Java code,
in the form of keyword inputs, which are listed in the ATJ reference documentation. This tutorial page covers the simpler options,
which apply to both deep and shallow embedding approaches. The more complex options are covered elsewhere in this tutorial,
each by one or more pages.
Java Package
The Java code generated for
the factorial function in atj-tutorial-deep
has no package declarations,
which means that the generated classes are in an unnamed package.
This (i.e. the absence of a package declaration) is the default,
which can be overridden via ATJ's :java-package option.
For the example in atj-tutorial-deep, the ATJ call
(java::atj fact :deep t :guards nil :java-package "mypkg")
generates files Acl2Code.java and Acl2CodeEnvironment.java
that are the same as before but with the package declaration
package mypkg;
at the beginning.
Now that the generated code is in the mypkg package,
the external Java code exemplified in atj-tutorial-deep
must be adapted, e.g. by putting it into mypkg as well,
or by referencing the generated Java class
via the fully qualified name mypkg.Acl2Code,
or by importing the class via a declaration import mypkg.Acl2Code;.
The string passed as the :java-package option
must be not only a valid Java package name,
but also consist only of ASCII characters.
ATJ does not currently support the generation of
package names with non-ASCII characters.
Note that the files are generated in the current directory,
not in a mypkg directory,
as may be expected based on Java's typical source file organization.
The directory where the files are generated
can be customized via the :output-dir option, described below.
Java Class
The Java class generated for
the factorial function in atj-tutorial-deep
is called Acl2Code;
the generated file is called Acl2Code.java,
thus satisfying the constraint that a public class resides in a file
whose name is obtained by adding the .java extension
to the class name.
The same applies to the class Acl2CodeEnvironment,
generated in the file Acl2CodeEnvironment.java.
These class (and thus file) names are the default,
which can be overridden via ATJ's :java-class option.
For the example in atj-tutorial-deep, the ATJ call
(java::atj fact :deep t :guards nil :java-class "Fact")
generates files Fact.java and FactEnvironment.java
that is the same as before but with Fact and FactEnvironment
as the name of the classes.
Now that the main generated class is called Fact,
the external Java code exemplified in atj-tutorial-deep
must be adapted, by referencing the generated Java class as Fact.
The string passed as the :java-class option
must be not only a valid Java class name,
but also consist only of ASCII characters.
ATJ does not currently support the generation of
class names with non-ASCII characters.
Output Directory
The Java files generated for
the factorial function in atj-tutorial-deep
reside in the current directory.
This is the default,
which can be overridden via ATJ's :output-dir option.
For the example in atj-tutorial-deep, the ATJ call
(java::atj fact :deep t :guards nil :output-dir "java")
generates the same files
Acl2Code.java and Acl2CodeEnvironment.java as before,
but in a subdirectory java of the current directory.
The subdirectory must already exist; ATJ does not create it.
Needless to say, the invocations of the javac and java commands
must be adapted to the location of the .java and .class files.
The string must be a valid absolute or relative path
in the file system of the underlying operating system.
If it is a relative path, it is relative to the current directory.
When running ATJ interactively from the ACL2 shell,
the current directory is the one returned by :cbd. When running ATJ as part of book certification,
the current directory should be the same one
where the .lisp file with the ATJ call resides.
If the :java-package option is also used (see above),
the :output-dir option can be used to generate the file
in a subdirectory consistent with the package name,
according to the typical organization of Java source files.
For example, if :java-package is "mypkg",
:output-dir can be set to "mypkg" as well.
As another example, if :java-package is "my.new.pkg",
:output-dir can be set to "my/new/pkg",
assuming a Unix-like operating system
with forward slashes that separate file path elements.
As already noted above, all these directories must exist;
ATJ does not create them.
Previous: ACL2 Evaluator Written in Java
Next: Control of the Screen Output
