|
|
|---|
|
|
|
|---|
Representation of quoted constants in the shallow embedding.
In the shallow embedding approach, each quoted constant in the ACL2 code is translated to a Java static final field that is calculated once at class initialization time and then just referenced in the Java code. Since ACL2 values are objects, this avoids recalculating the object (whether it is created or reused, e.g. when interned) every time the shallowly embedded quoted constant is executed in the Java code.
We extract all the quoted constants from the pre-translated bodies of the ACL2 functions, and we create a static final field for each. The fields for these quoted constants are declared in the generated main class; they are named in a way that describes their value, e.g. see atj-gen-shallow-number-field-name.