• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • C
        • Soft
        • Bv
        • Imp-language
        • Ethereum
        • Event-macros
        • 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
        • Riscv
        • Bitcoin
        • Zcash
        • Yul
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Axe
        • Lists-light
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • 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.