		Search-engine friendly clone of the ACL2 documentation.

Atj-java-abstract-syntax

Jexpr-get-field

Build a Java expression to access a field.

Signature
(jexpr-get-field expr name) → get-field-expr
Arguments: expr — Guard (jexprp expr).; name — Guard (stringp name).
Returns: get-field-expr — Type (jexprp get-field-expr).

In the Java grammar, not all expressions that access fields can be derived from field-access. When the target object is an expression name, the field access expression is also an expression name.

Definitions and Theorems

Function: jexpr-get-field

(defun jexpr-get-field (expr name)
  (declare (xargs :guard (and (jexprp expr) (stringp name))))
  (let ((__function__ 'jexpr-get-field))
    (declare (ignorable __function__))
    (if (jexpr-case expr :name)
        (jexpr-name (str::cat (jexpr-name->get expr)
                              "." name))
      (jexpr-field expr name))))

Theorem: jexprp-of-jexpr-get-field

(defthm jexprp-of-jexpr-get-field
  (b* ((get-field-expr (jexpr-get-field expr name)))
    (jexprp get-field-expr))
  :rule-classes :rewrite)