Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Kestrel-books
Crypto-hdwallet
Apt
Error-checking
Abnf
Fty-extensions
Isar
Kestrel-utilities
Soft
Bv
Imp-language
Event-macros
C
Java
Atj
Atj-implementation
Atj-types
Atj-java-primitive-array-model
Atj-java-abstract-syntax
Atj-input-processing
Atj-java-pretty-printer
Atj-code-generation
Atj-gen-test-method
Atj-shallow-code-generation
Atj-gen-shallow-term-fns
String-jmethodlist-alistp
Atj-gen-shallow-fndef-method
String-jfieldlist-alistp
Atj-gen-shallow-test-code
Atj-adapt-expr-to-type
Atj-gen-shallow-fn-call
Atj-check-marked-annotated-mv-let-call
Atj-gen-shallow-main-class
Atj-gen-shallow-fnnative-method
Atj-gen-shallow-synonym-method
Atj-gen-shallow-if-call
Atj-gen-shallow-and-call
Atj-gen-shallow-pkg-methods
Atj-convert-expr-to-jprim
Atj-gen-shallow-or-call
Atj-convert-expr-from-jprimarr-method
Atj-adapt-expr-to-types
Atj-gen-shallow-all-pkg-methods
Atj-convert-expr-to-jprimarr-method
Atj-gen-shallow-fndef-all-methods
Atj-convert-expr-from-jprim
Atj-gen-shallow-mv-class
Atj-gen-shallow-main-cunit
Atj-gen-shallow-fndef-methods
Atj-gen-shallow-mv-class-name
Atj-shallow-fns-that-may-throw
Atj-gen-shallow-term
Atj-gen-shallow-let-bindings
Atj-gen-shallow-fn-methods
Atj-gen-shallow-jprimarr-new-init-call
Atj-gen-shallow-fnname
Atj-gen-shallow-all-fn-methods
Atj-gen-shallow-not-call
Atj-fnnative-method-name
Atj-gen-shallow-mv-let
Atj-gen-shallow-jprim-constr-call
Atj-gen-shallow-jprimarr-write-call
Atj-gen-shallow-fnnative-all-methods
Atj-gen-shallow-pkg-class
Atj-gen-shallow-jprimarr-length-call
Atj-gen-shallow-pkg-fields
Atj-all-mv-output-types
Atj-gen-shallow-mv-call
Atj-gen-shallow-jprim-binop-call
Atj-gen-shallow-jprim-conv-call
Atj-gen-shallow-primarray-write-method
Atj-gen-shallow-mv-fields
Atj-gen-shallow-jprimarr-read-call
Atj-gen-shallow-jprimarr-new-len-call
Atj-gen-shallow-jprimarr-conv-tolist-call
Atj-gen-shallow-jprimarr-conv-fromlist-call
Atj-gen-shallow-synonym-all-methods
Atj-gen-shallow-jprim-deconstr-call
Atj-gen-shallow-all-pkg-fields
Atj-gen-shallow-test-code-asgs
Atj-gen-shallow-lambda
Atj-gen-shallow-jprim-unop-call
Atj-jprim-binop-fn-to-jbinop
Atj-gen-shallow-mv-asgs
Atj-gen-shallow-env-class
Atj-gen-shallow-mv-params
Atj-gen-shallow-fnnative-methods
Atj-gen-shallow-pkg-classes
Atj-gen-shallow-env-cunit
Atj-gen-shallow-all-synonym-methods
Atj-convert-expr-to-jprimarr
Atj-convert-expr-from-jprimarr
Atj-jprim-constr-fn-of-qconst-to-expr
Atj-gen-shallow-test-code-mv-asgs
Atj-gen-shallow-synonym-methods
Atj-gen-shallow-synonym-method-params
Atj-convert-expr-to-jprimarr-method-name
Atj-convert-expr-from-jprimarr-method-name
Atj-jexpr-list-to-3-jexprs
Atj-jblock-list-to-3-jblocks
Atj-gen-shallow-test-code-comps
Atj-jprim-conv-fn-to-jtype
Atj-gen-shallow-terms
Atj-gen-shallow-mv-field-name
Atj-adapt-exprs-to-types
Atj-jblock-list-to-2-jblocks
Atj-gen-shallow-primarray-write-methods
Atj-gen-shallow-mv-classes
Atj-gen-shallow-jtype
Atj-gen-shallow-build-method
Atj-jexpr-list-to-2-jexprs
Atj-jprimarr-write-to-method-name
Atj-gen-shallow-all-jprimarr-conv-methods
Atj-jprimarr-new-len-fn-to-comp-jtype
Atj-jprimarr-new-init-fn-to-comp-jtype
Atj-jprim-unop-fn-to-junop
*atj-gen-cond-exprs*
Atj-primarray-write-method-name
Atj-gen-shallow-jprimarr-fromlist-methods
Atj-gen-shallow-jprimarr-tolist-methods
Atj-gen-shallow-mv-classes-guard
*atj-mv-singleton-field-name*
*atj-mv-factory-method-name*
Atj-common-code-generation
Atj-shallow-quoted-constant-generation
Atj-pre-translation
Atj-gen-everything
Atj-name-translation
Atj-gen-test-cunit
Atj-gen-test-class
Atj-gen-main-file
Atj-post-translation
Atj-deep-code-generation
Atj-gen-test-methods
Atj-gen-test-file
Atj-gen-env-file
Atj-gen-output-subdir
Atj-java-primitives
Atj-java-primitive-arrays
Atj-type-macros
Atj-java-syntax-operations
Atj-fn
Atj-library-extensions
Atj-java-input-types
Atj-test-structures
Aij-notions
Atj-macro-definition
Atj-tutorial
Aij
Language
Bitcoin
Ethereum
Yul
Zcash
ACL2-programming-language
Prime-fields
Json
Syntheto
File-io-light
Number-theory
Cryptography
Lists-light
Builtins
Axe
Solidity
Helpers
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Execloader
Math
Testing-utilities
Atj-code-generation
Atj-shallow-code-generation
Code generation that is specific to the shallow embedding approach.
Subtopics
Atj-gen-shallow-term-fns
Functions to generate shallowly embedded ACL2 terms.
String-jmethodlist-alistp
Alists from package names (strings) to lists of Java methods.
Atj-gen-shallow-fndef-method
Generate a Java method with the given types for an ACL2 function definition.
String-jfieldlist-alistp
Alists from package names (strings) to lists of Java fields.
Atj-gen-shallow-test-code
Generate the code of a test method that is specific to the shallow embedding approach.
Atj-adapt-expr-to-type
Adapt a Java expression from a source type to a destination type.
Atj-gen-shallow-fn-call
Generate a shallowly embedded ACL2 named function call.
Atj-check-marked-annotated-mv-let-call
Recognize translated
mv-let
s after pre-translation.
Atj-gen-shallow-main-class
Generate the main (i.e. non-test) Java class declaration, in the shallow embedding approach.
Atj-gen-shallow-fnnative-method
Generate a Java method with the given types for an ACL2 function that is natively implemented in AIJ.
Atj-gen-shallow-synonym-method
Generate a Java method with the given types for an ACL2 function synonym.
Atj-gen-shallow-if-call
Generate a shallowly embedded ACL2
if
call.
Atj-gen-shallow-and-call
Generate a shallowly embedded ACL2
and
call.
Atj-gen-shallow-pkg-methods
Generate all the methods of the class for an ACL2 package.
Atj-convert-expr-to-jprim
Convert a Java expression to a Java primitive type.
Atj-gen-shallow-or-call
Generate a shallowly embedded ACL2
or
call.
Atj-convert-expr-from-jprimarr-method
Method to convert a Java expression from a Java primitive array type.
Atj-adapt-expr-to-types
Adapt a Java expression from source types to destination types.
Atj-gen-shallow-all-pkg-methods
Generate all the methods of the classes for all the ACL2 packages.
Atj-convert-expr-to-jprimarr-method
Method to convert a Java expression to a Java primitive array type.
Atj-gen-shallow-fndef-all-methods
Generate all the overloaded Java methods for an ACL2 function definition.
Atj-convert-expr-from-jprim
Convert a Java expression from a Java primitive type.
Atj-gen-shallow-mv-class
Generate the
mv
class for the given types.
Atj-gen-shallow-main-cunit
Generate the main Java compilation unit, in the shallow embedding approach.
Atj-gen-shallow-fndef-methods
Lift
atj-gen-shallow-fndef-method
to lists of function types.
Atj-gen-shallow-mv-class-name
Generate the name of the
mv
class for the given types.
Atj-shallow-fns-that-may-throw
Calculate the functions whose corresponding Java methods may throw an
Acl2UndefinedPackageException
.
Atj-gen-shallow-term
Generate a shallowly embedded ACL2 term.
Atj-gen-shallow-let-bindings
Generate shallowly embedded ACL2
let
bindings.
Atj-gen-shallow-fn-methods
Generate all the overloaded Java methods for an ACL2 function natively implemented in AIJ or for an ACL2 function definition.
Atj-gen-shallow-jprimarr-new-init-call
Generate a shallowly embedded ACL2 call of a Java primitive array creation from components.
Atj-gen-shallow-fnname
Generate a shallowly embedded ACL2 function name.
Atj-gen-shallow-all-fn-methods
Lift
atj-gen-shallow-fn-methods
to lists of functions.
Atj-gen-shallow-not-call
Generate a shallowly embedded ACL2
not
call.
Atj-fnnative-method-name
Name of the AIJ method that natively implements an ACL2 function.
Atj-gen-shallow-mv-let
Generate a shallowly embedded ACL2
mv-let
.
Atj-gen-shallow-jprim-constr-call
Generate a shallowly embedded ACL2 call of a Java primitive constructor.
Atj-gen-shallow-jprimarr-write-call
Generate a shallowly embedded ACL2 call of a Java primitive write operation.
Atj-gen-shallow-fnnative-all-methods
Generate all the overloaded Java methods for an ACL2 function that is natively implemented in AIJ.
Atj-gen-shallow-pkg-class
Generate the class for an ACL2 package.
Atj-gen-shallow-jprimarr-length-call
Generate a shallowly embedded ACL2 call of a Java primitive array length operation.
Atj-gen-shallow-pkg-fields
Generate all the fields of the class for an ACL2 package.
Atj-all-mv-output-types
Collect the output types of functions that return multiple values.
Atj-gen-shallow-mv-call
Generate a shallowly embedded ACL2 call of
mv
.
Atj-gen-shallow-jprim-binop-call
Generate a shallowly embedded ACL2 call of a Java primitive binary operation.
Atj-gen-shallow-jprim-conv-call
Generate a shallowly embedded ACL2 call of a Java primitive conversion.
Atj-gen-shallow-primarray-write-method
Generate a Java method to write a primitive array component.
Atj-gen-shallow-mv-fields
Generate the fields of the
mv
class for the given types.
Atj-gen-shallow-jprimarr-read-call
Generate a shallowly embedded ACL2 call of a Java primitive array read operation.
Atj-gen-shallow-jprimarr-new-len-call
Generate a shallowly embedded ACL2 call of a Java primitive array creation from a length.
Atj-gen-shallow-jprimarr-conv-tolist-call
Generate a shallowly embedded ACL2 call of a Java primitive array conversion to list.
Atj-gen-shallow-jprimarr-conv-fromlist-call
Generate a shallowly embedded ACL2 call of a Java primitive array conversion from list.
Atj-gen-shallow-synonym-all-methods
Generate all the overloaded Java methods for an ACL2 function synonym.
Atj-gen-shallow-jprim-deconstr-call
Generate a shallowly embedded ACL2 call of a Java primitive deconstructor.
Atj-gen-shallow-all-pkg-fields
Generate all the fields of the class for all the ACL2 packages.
Atj-gen-shallow-test-code-asgs
Atj-gen-shallow-lambda
Generate a shallowly embedded ACL2 lambda expression, applied to given Java expressions as arguments.
Atj-gen-shallow-jprim-unop-call
Generate a shallowly embedded ACL2 call of a Java primitive unary operation.
Atj-jprim-binop-fn-to-jbinop
Map an ACL2 function that models a Java primitive binary operation to the corresponding binary operator in the Java abstract syntax.
Atj-gen-shallow-mv-asgs
Generate the assignments in the factory method of the
mv
class for the given types.
Atj-gen-shallow-env-class
Generate the declaration of the environment Java class, in the shallow embedding approach.
Atj-gen-shallow-mv-params
Generate the parameters of the factory method of the
mv
class for the given types.
Atj-gen-shallow-fnnative-methods
Lift
atj-gen-shallow-fnnative-method
to lists of function types.
Atj-gen-shallow-pkg-classes
Lift
atj-gen-shallow-pkg-class
to lists.
Atj-gen-shallow-env-cunit
Generate the Java compilation unit with the environment Java class, in the shallow embedding approach.
Atj-gen-shallow-all-synonym-methods
Lift
atj-gen-shallow-synonym-all-methods
to lists of functions.
Atj-convert-expr-to-jprimarr
Convert a Java expression to a Java primitive array type.
Atj-convert-expr-from-jprimarr
Convert a Java expression from a Java primitive array type.
Atj-jprim-constr-fn-of-qconst-to-expr
Map an ACL2 function that models a Java primitive constructor to the Java expression that constructs the primitive value, when the argument of the constructor is a quoted constant.
Atj-gen-shallow-test-code-mv-asgs
Atj-gen-shallow-synonym-methods
Lift
atj-gen-shallow-synonym-method
to lists of function types.
Atj-gen-shallow-synonym-method-params
Generate shallowly embedded formal parameters for the function synonyms generated by
atj-gen-shallow-synonym-method
.
Atj-convert-expr-to-jprimarr-method-name
Name of the method to convert a Java expression to a Java primitive array type.
Atj-convert-expr-from-jprimarr-method-name
Name of the method to convert a Java expression from a Java primitive array type.
Atj-jexpr-list-to-3-jexprs
Turn a list of three expressions into the three expressions.
Atj-jblock-list-to-3-jblocks
Turn a list of three blocks into the three blocks.
Atj-gen-shallow-test-code-comps
Atj-jprim-conv-fn-to-jtype
Map an ACL2 function that models a Java primitive conversion to the result Java type of the conversion.
Atj-gen-shallow-terms
Lift
atj-gen-shallow-term
to lists.
Atj-gen-shallow-mv-field-name
Generate the name of the field with the given index in an
mv
class.
Atj-adapt-exprs-to-types
Lift
atj-adapt-expr-to-type
to lists.
Atj-jblock-list-to-2-jblocks
Turn a list of two blocks into the two blocks.
Atj-gen-shallow-primarray-write-methods
Generate all the eight methods to write primitive arrays.
Atj-gen-shallow-mv-classes
Lift
atj-gen-shallow-mv-class
to lists.
Atj-gen-shallow-jtype
Generate a Java type, in the shallow embedding approach.
Atj-gen-shallow-build-method
Generate the method to build the ACL2 environment, in the shallow embedding approach.
Atj-jexpr-list-to-2-jexprs
Turn a list of two expressions into the two expressions.
Atj-jprimarr-write-to-method-name
Map an ACL2 function that models a Java primitive array write operation to the corresponding Java method name.
Atj-gen-shallow-all-jprimarr-conv-methods
Generate all the Java primitive array conversion methods.
Atj-jprimarr-new-len-fn-to-comp-jtype
Map an ACL2 function that models a Java primitive array creation with length to the Java component type.
Atj-jprimarr-new-init-fn-to-comp-jtype
Map an ACL2 function that models a Java primitive array creation with initializer to the Java component type.
Atj-jprim-unop-fn-to-junop
Map an ACL2 function that models a Java primitive unary operation to the corresponding unary operator in the Java abstract syntax.
*atj-gen-cond-exprs*
Flag saying whether ATJ should attempt to generate Java conditional expressions.
Atj-primarray-write-method-name
Name of the method generated by
atj-gen-shallow-primarray-write-method
.
Atj-gen-shallow-jprimarr-fromlist-methods
Generate methods to convert to Java primitive arrays from lists.
Atj-gen-shallow-jprimarr-tolist-methods
Generate methods to convert from Java primitive arrays to lists.
Atj-gen-shallow-mv-classes-guard
*atj-mv-singleton-field-name*
Name of the private static field that stores the singleton instance of an
mv
class.
*atj-mv-factory-method-name*
Name of the package-private static factory method of an
mv
class.