• 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-gen-value
                  • Atj-chars-to-jhexcodes
                  • Atj-gen-test-value
                  • Atj-gen-test-main-method
                  • Atj-gen-value-flat
                  • Atj-gen-test-values
                  • Atj-gen-jlocvar-indexed
                  • Atj-gen-pkg-method
                  • Atj-gen-symbol
                  • Atj-gen-jstring
                  • Atj-gen-init-method
                  • Atj-gen-char
                  • Atj-gen-string
                  • Atj-gen-pkg-name
                  • Atj-gen-integer
                  • Atj-gen-test-method-name
                  • Atj-gen-paramlist
                  • Atj-gen-pkg-method-name
                  • Atj-gen-run-tests
                  • Atj-gen-jshort-array
                  • Atj-gen-jboolean-array
                  • Atj-gen-test-failures-field
                  • Atj-gen-pkgs
                  • Atj-gen-jlong-array
                  • Atj-gen-jint-array
                  • Atj-gen-jchar-array
                  • Atj-gen-jchar
                  • Atj-gen-jbyte-array
                  • Atj-char-to-jhexcode
                  • Atj-gen-pkg-methods
                  • Atj-gen-number
                  • Atj-gen-symbols
                  • Atj-gen-static-initializer
                  • Atj-gen-rational
                  • Atj-gen-jlong
                  • Atj-gen-jboolean
                  • Atj-gen-jbigint
                  • Atj-gen-jshort
                  • Atj-gen-jint
                  • Atj-gen-jbyte
                  • *atj-gen-pkg-name-alist*
                • 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
        • 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-common-code-generation

Code generation that is common to the deep and shallow embedding approaches.

Subtopics

Atj-gen-value
Generate Java code to build an ACL2 value.
Atj-chars-to-jhexcodes
Lift atj-char-to-jhexcode to lists.
Atj-gen-test-value
Generate the Java code for a test value.
Atj-gen-test-main-method
Generate the Java main method for the test Java class.
Atj-gen-value-flat
Generate flat Java code to build an ACL2 value.
Atj-gen-test-values
Lift atj-gen-test-value to lists.
Atj-gen-jlocvar-indexed
Generate a Java declaration for an indexed local variable.
Atj-gen-pkg-method
Generate a Java method that adds an ACL2 package definition.
Atj-gen-symbol
Generate Java code to build an ACL2 symbol.
Atj-gen-jstring
Generate Java code to build a Java string from an ACL2 string.
Atj-gen-init-method
Generate the Java public method to initialize the ACL2 environment.
Atj-gen-char
Generate Java code to build an ACL2 character.
Atj-gen-string
Generate Java code to build an ACL2 string.
Atj-gen-pkg-name
Generate Java code to build an ACL2 package name.
Atj-gen-integer
Generate Java code to build an ACL2 integer.
Atj-gen-test-method-name
Name of the Java method to run one of the specified tests.
Atj-gen-paramlist
Generate a Java formal parameter list from the specified names and Java types.
Atj-gen-pkg-method-name
Name of the Java method that adds an ACL2 package definition.
Atj-gen-run-tests
Generate Java code to run the specified tests.
Atj-gen-jshort-array
Generate Java code to build a Java short array.
Atj-gen-jboolean-array
Generate Java code to build a Java boolean array.
Atj-gen-test-failures-field
Generate the Java field that keeps track of failures in the test Java class.
Atj-gen-pkgs
Generate Java code to build the ACL2 packages.
Atj-gen-jlong-array
Generate Java code to build a Java long array.
Atj-gen-jint-array
Generate Java code to build a Java int array.
Atj-gen-jchar-array
Generate Java code to build a Java char array.
Atj-gen-jchar
Generate Java code to build a Java char from an unsigned 16-bit ACL2 integer.
Atj-gen-jbyte-array
Generate Java code to build a Java byte array.
Atj-char-to-jhexcode
Turn an ACL2 character into a Java hexadecimal literal expression corresponding to the character code.
Atj-gen-pkg-methods
Generate all the Java methods that add the ACL2 package definitions.
Atj-gen-number
Generate Java code to build an ACL2 number.
Atj-gen-symbols
Lift atj-gen-symbol to lists.
Atj-gen-static-initializer
Generate the static initializer of the main Java class.
Atj-gen-rational
Generate Java code to build an ACL2 rational.
Atj-gen-jlong
Generate Java code to build a Java long from a signed 64-bit ACL2 integer.
Atj-gen-jboolean
Generate Java code to build a Java boolean from an ACL2 boolean.
Atj-gen-jbigint
Generate Java code to build a Java BigInteger from an ACL2 integer.
Atj-gen-jshort
Generate Java code to build a Java short from a signed 16-bit signed ACL2 integer.
Atj-gen-jint
Generate Java code to build a Java int from a signed 32-bit ACL2 integer.
Atj-gen-jbyte
Generate Java code to build a Java byte from a signed 8-bit ACL2 integer.
*atj-gen-pkg-name-alist*