Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Apt
Acre
Milawa
Smtlink
Abnf
Vwsim
Isar
Wp-gen
Dimacs-reader
Pfcs
Legacy-defrstobj
Proof-checker-array
Soft
Farray
Rp-rewriter
Instant-runoff-voting
Imp-language
Sidekick
Leftist-trees
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-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-deep-term-fns
Atj-gen-deep-test-code
Atj-gen-deep-fndef-method
Atj-gen-deep-fnapp
Atj-gen-deep-env-class
Atj-gen-deep-env-cunit
Atj-gen-deep-lambda
Atj-gen-deep-qconst
Atj-gen-deep-main-class
Atj-gen-deep-term
Atj-gen-deep-terms
Atj-gen-deep-build-method
Atj-gen-deep-call-method
Atj-gen-deep-main-cunit
Atj-gen-deep-fndef-method-name
Atj-gen-deep-fndef-methods
Atj-gen-deep-fndefs
Atj-gen-deep-formals
Atj-gen-deep-var
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
Taspi
Bitcoin
Des
Ethereum
Sha-2
Yul
C
Zcash
Proof-checker-itp13
Bigmem
Regex
ACL2-programming-language
Json
X86isa
Jfkr
Equational
Cryptography
Poseidon
Where-do-i-place-my-book
Builtins
Axe
Execloader
Solidity
Paco
Concurrent-programs
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Atj-code-generation
Atj-deep-code-generation
Code generation that is specific to the deep embedding approach.
Subtopics
Atj-gen-deep-term-fns
Functions to generate Java code to build deeply embedded ACL2 terms.
Atj-gen-deep-test-code
Generate the code of a test method that is specific to the deep embedding approach.
Atj-gen-deep-fndef-method
Generate a Java method that builds a deeply embedded ACL2 function definition.
Atj-gen-deep-fnapp
Generate Java code to build a deeply embedded ACL2 function call.
Atj-gen-deep-env-class
Generate the declaration of the environment Java class, in the deep embedding approach.
Atj-gen-deep-env-cunit
Generate the Java compilation unit with the environment Java class, in the deep embedding approach.
Atj-gen-deep-lambda
Generate Java code to build a deeply embedded ACL2 lambda expression.
Atj-gen-deep-qconst
Generate Java code to build a deeply embedded ACL2 quoted constant.
Atj-gen-deep-main-class
Generate the main (i.e. non-test) Java class declaration, in the deep embedding approach.
Atj-gen-deep-term
Generate Java code to build a deeply embedded ACL2 term.
Atj-gen-deep-terms
Lift
atj-gen-deep-term
to lists.
Atj-gen-deep-build-method
Generate the method to build the ACL2 environment, in the deep embedding approach.
Atj-gen-deep-call-method
Generate the Java method to call ACL2 functions, in the deep embedding approach.
Atj-gen-deep-main-cunit
Generate the main Java compilation unit, in the deep embedding approach.
Atj-gen-deep-fndef-method-name
Name of the Java method that builds a deeply embedded ACL2 function definition.
Atj-gen-deep-fndef-methods
Lift
atj-gen-deep-fndef-method
to lists.
Atj-gen-deep-fndefs
Generate Java code to build the deeply embedded ACL2 function definitions.
Atj-gen-deep-formals
Generate Java code to build a deeply embedded formals parameter list of an ACL2 named function or lambda expression.
Atj-gen-deep-var
Generate Java code to build a deeply embedded ACL2 variable.