Java expressions [JLS14:15].
We do not capture lambda expressions, class literals, and method references.
For expression names [JLS14:6.5], we use ACL2 strings,
which allow dot-separated identifiers,
as well as
We only capture monodimensional array creation expressions with either an explicit size that is an expression or an array initializer that is a sequence of expressions. The type field is the primitive or class/interface element type, not the array type, which is implicitly the one whose element type if the one in the type field.
In an array access expression, we allow any expression as the first one.
We only capture class instance creation expressions
that consist of
In a field access expression, we allow any expression as the first one.
We capture method invocations of three kinds: static (which start with a type), instance (which start with an expression), and generic (which start with the method name). The generic ones may be static or instance, depending on how the Java compiler resolves them. This is a rough model of Java method invocation expressions, but it suffices for ATJ's purposes.
We also include parenthesized expressions, which normally do not belong to an abstract syntax because the tree structure of the abstract syntax provides the intended grouping of the nested expressions. However, having explicit parenthesized expressions in the abstract syntax provides more flexibility, e.g. to capture parentheses that would not be needed for corectness but could perhaps improve clarity and readability.
The abstract syntax allows any type, not just reference types,
as the right-hand side of