		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-quoted-constant-generation

Atj-gen-shallow-symbol

Generate a shallowly embedded ACL2 quoted symbol.

Signature
(atj-gen-shallow-symbol symbol pkg-class-names curr-pkg guards$) → expr
Arguments: symbol — Guard (symbolp symbol).; pkg-class-names — Guard (string-string-alistp pkg-class-names).; curr-pkg — Guard (stringp curr-pkg).; guards$ — Guard (booleanp guards$).
Returns: expr — Type (jexprp expr).

If guards are assumed and the symbol is an ACL2 boolean, we generate the corresponding Java boolean literal.

In all other cases, the generated expression depends on the current package, i.e. the package of the function where the quoted symbol occurs. If the current package is the same as the symbol's package, or if the current package imports the symbol, then we just generate the simple name of the field, because the field will be declared in the class for the current package. Otherwise, we generate a qualified name, preceded by the name of the class for the symbol's package. This mirrors the rules for symbol references in ACL2.

Definitions and Theorems

Function: atj-gen-shallow-symbol

(defun atj-gen-shallow-symbol
       (symbol pkg-class-names curr-pkg guards$)
 (declare (xargs :guard (and (symbolp symbol)
                             (string-string-alistp pkg-class-names)
                             (stringp curr-pkg)
                             (booleanp guards$))))
 (let ((__function__ 'atj-gen-shallow-symbol))
   (declare (ignorable __function__))
   (b*
     (((when (and guards$ (booleanp symbol)))
       (if symbol (jexpr-literal-true)
         (jexpr-literal-false)))
      (sym-pkg (symbol-package-name symbol))
      (simple-name (atj-gen-shallow-symbol-field-name symbol))
      ((when (or (equal sym-pkg curr-pkg)
                 (member-eq symbol (pkg-imports curr-pkg))))
       (jexpr-name simple-name))
      (class-name (atj-get-pkg-class-name sym-pkg pkg-class-names)))
     (jexpr-name (str::cat class-name "." simple-name)))))

Theorem: jexprp-of-atj-gen-shallow-symbol

(defthm jexprp-of-atj-gen-shallow-symbol
 (b*
  ((expr (atj-gen-shallow-symbol symbol
                                 pkg-class-names curr-pkg guards$)))
  (jexprp expr))
 :rule-classes :rewrite)