		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-jchar

Generate Java code to build a Java char from an unsigned 16-bit ACL2 integer.

Signature
(atj-gen-jchar char) → expr
Arguments: char — Guard (ubyte16p char).
Returns: expr — Type (jexprp expr).

We generate a character literal if the character is below 256, since currently our Java abstract syntax only supports 8-bit character literals. Otherwise, we cast the value to char.

Definitions and Theorems

Function: atj-gen-jchar

(defun atj-gen-jchar (char)
  (declare (xargs :guard (ubyte16p char)))
  (let ((__function__ 'atj-gen-jchar))
    (declare (ignorable __function__))
    (if (< char 256)
        (jexpr-literal-character (code-char char))
      (jexpr-cast (jtype-char)
                  (jexpr-lit-int-dec-nouscores char)))))

Theorem: jexprp-of-atj-gen-jchar

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