Top

Atj-java-abstract-syntax

Jcunit

Java compilation units [JLS14:7.3].

This is a product type introduced by fty::defprod.

Fields

package? — maybe-string
imports — jimport-list
types — jclass-list

We only capture ordinary compilation units, not modular ones. Thus, we do not capture module declarations either.

We capture the package declaration [JLS14:7.4] as an ACL2 string for the name. This declaration is optional.

We do not capture interfaces, so a type declaration [JLS14:7.6] is always a class declaration.

Subtopics

Jcunit-fix: Fixing function for jcunit structures.
Jcunit-equiv: Basic equivalence relation for jcunit structures.
Make-jcunit: Basic constructor macro for jcunit structures.
Jcunitp: Recognizer for jcunit structures.
Jcunit->package?: Get the package? field from a jcunit.
Change-jcunit: Modifying constructor for jcunit structures.
Jcunit->types: Get the types field from a jcunit.
Jcunit->imports: Get the imports field from a jcunit.