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

    Atj-gen-char

    Generate Java code to build an ACL2 character.

    Signature
    (atj-gen-char char deep$ guards$) → expr
    Arguments
    char — Guard (characterp char).
    deep$ — Guard (symbolp deep$).
    guards$ — Guard (symbolp guards$).
    Returns
    expr — Type (jexprp expr).

    In the shallow embedding with guards, we translate ACL2 characters to Java character literals. This is because, in the shallow embedding with guards, ACL2 characters are represented as Java characters.

    In the deep embedding, or in the shallow embedding without guards, we generate an expression of type Acl2Character, by calling the factory method on the Java character literal.

    Definitions and Theorems

    Function: atj-gen-char

    (defun atj-gen-char (char deep$ guards$)
      (declare (xargs :guard (and (characterp char)
                                  (symbolp deep$)
                                  (symbolp guards$))))
      (let ((__function__ 'atj-gen-char))
        (declare (ignorable __function__))
        (if (and (not deep$) guards$)
            (jexpr-literal-character char)
          (jexpr-smethod *aij-type-char* "make"
                         (list (jexpr-literal-character char))))))

    Theorem: jexprp-of-atj-gen-char

    (defthm jexprp-of-atj-gen-char
      (b* ((expr (atj-gen-char char deep$ guards$)))
        (jexprp expr))
      :rule-classes :rewrite)