Top

Atj-java-abstract-syntax

Jliteral

Java literals [JLS14:3.10].

This is a tagged union type, introduced by fty::deftagsum.

Member Tags → Types

:integer → jliteral-integer
:floating → jliteral-floating
:boolean → jliteral-boolean
:character → jliteral-character
:string → jliteral-string
:null → jliteral-null

We use the integer literals from the language formalization.

We only support a very limited form of floating-point literals for now, whose value is actually just a natural number.

We use ACL2 characters and strings for Java character and string literals. See the discussion in atj-java-abstract-syntax about that.

Subtopics

Jliteral-fix: Fixing function for jliteral structures.
Jliteral-case: Case macro for the different kinds of jliteral structures.
Jliteralp: Recognizer for jliteral structures.
Jliteral-equiv: Basic equivalence relation for jliteral structures.
Jliteral-string
Jliteral-integer
Jliteral-floating
Jliteral-character
Jliteral-boolean
Jliteral-kind: Get the kind (tag) of a jliteral structure.
Jliteral-null