		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-jstring

Generate Java code to build a Java string from an ACL2 string.

Signature
(atj-gen-jstring string) → expr
Arguments: string — Guard (stringp string).
Returns: expr — Type (jexprp expr).

Often, an ACL2 string can be turned into a Java string literal that is valid when pretty-printed. Examples are "abc" or "x-y @ 5.A".

However, if the ACL2 string includes characters like #Return, attempting to turn that into a Java string literal may result in an invalid one when pretty-printed. In this case, a safe way to build the Java string is via a Java character array with an initializer consisting of the codes of the ACL2 string.

If the ACL2 string consists of only pritable ASCII characters (i.e. space and visible ASCII characters), we turn it into a Java string literal. Otherwise, we turn it into a Java array creation expression that is passed as argument to a Java class instance creation expression for a String object.

Definitions and Theorems

Function: atj-gen-jstring

(defun atj-gen-jstring (string)
 (declare (xargs :guard (stringp string)))
 (let ((__function__ 'atj-gen-jstring))
  (declare (ignorable __function__))
  (b* ((chars (explode string)))
   (if (str::printable-charlist-p chars)
       (jexpr-literal-string string)
    (jexpr-newclass
     (jtype-class "String")
     (list
          (jexpr-newarray-init (jtype-char)
                               (atj-chars-to-jhexcodes chars))))))))

Theorem: jexprp-of-atj-gen-jstring

(defthm jexprp-of-atj-gen-jstring
  (b* ((expr (atj-gen-jstring string)))
    (jexprp expr))
  :rule-classes :rewrite)