		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-symbol

Generate Java code to build an ACL2 symbol.

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

In the shallow embedding with guards, for the symbols t and nil we generate the Java literals true and false. This is because, in the shallow embedding with guards, ACL2 booleans are represented as Java booleans.

In all other cases, we generate an expression of type Acl2Symbol. Since AIJ has a number of constants (i.e. static final fields) for certain common symbols, we just reference the appropriate constant if the symbol in question is among those symbols. Otherwise, we build it in the general way.

Definitions and Theorems

Function: atj-gen-symbol

(defun atj-gen-symbol (symbol deep$ guards$)
  (declare (xargs :guard (and (symbolp symbol)
                              (symbolp deep$)
                              (symbolp guards$))))
  (let ((__function__ 'atj-gen-symbol))
    (declare (ignorable __function__))
    (if (and (booleanp symbol)
             (not deep$)
             guards$)
        (if symbol (jexpr-literal-true)
          (jexpr-literal-false))
      (b* ((pair (assoc-eq symbol *aij-symbol-constants*)))
        (if pair (jexpr-name (str::cat "Acl2Symbol." (cdr pair)))
          (jexpr-smethod
               *aij-type-symbol* "make"
               (list (atj-gen-jstring (symbol-package-name symbol))
                     (atj-gen-jstring (symbol-name symbol)))))))))

Theorem: jexprp-of-atj-gen-symbol

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