		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-string

Generate Java code to build an ACL2 string.

Signature
(atj-gen-string string deep$ guards$) → expr
Arguments: string — Guard (stringp string).; deep$ — Guard (symbolp deep$).; guards$ — Guard (symbolp guards$).
Returns: expr — Type (jexprp expr).

In the shallow embedding with guards, we translate ACL2 Strings to Java string expression. This is because, in the shallow embedding with guards, ACL2 strings are represented as Java strings.

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

Definitions and Theorems

Function: atj-gen-string

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

Theorem: jexprp-of-atj-gen-string

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