		Search-engine friendly clone of the ACL2 documentation.

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)