		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-quoted-constant-generation

Atj-gen-shallow-symbol-field

Generate a Java field for an ACL2 quoted symbol.

Signature
(atj-gen-shallow-symbol-field symbol) → field
Arguments: symbol — Guard (symbolp symbol).
Returns: field — Type (jfieldp field).

This is a package-private static final field with an initializer, which constructs the string value. Unlike the fields for other types of quoted constants, this one is declared in the class for the package of the symbol (or for a pacakge that imports the symbol). This field cannot be private, otherwise the classes for other packages could not access it.

Definitions and Theorems

Function: atj-gen-shallow-symbol-field

(defun atj-gen-shallow-symbol-field (symbol)
  (declare (xargs :guard (symbolp symbol)))
  (let ((__function__ 'atj-gen-shallow-symbol-field))
    (declare (ignorable __function__))
    (b* ((name (atj-gen-shallow-symbol-field-name symbol))
         (init (atj-gen-symbol symbol t nil))
         (type *aij-type-symbol*))
      (make-jfield :access (jaccess-default)
                   :static? t
                   :final? t
                   :transient? nil
                   :volatile? nil
                   :type type
                   :name name
                   :init? init))))

Theorem: jfieldp-of-atj-gen-shallow-symbol-field

(defthm jfieldp-of-atj-gen-shallow-symbol-field
  (b* ((field (atj-gen-shallow-symbol-field symbol)))
    (jfieldp field))
  :rule-classes :rewrite)