Abstract-syntax
Abstract syntax of Leo.
The abstract syntax of Leo is
a representation of the Leo constructs
obtained by abstracting away some information from the concrete syntax.
The definition of the abstract syntax consists of
fixtypes that represent the constructs
and an abstraction mapping from concrete to abstract syntax.
While the concrete syntax of Leo is prescribed by
the ABNF grammar and visible to the user,
the abstract syntax is internal to the ACL2 formalization:
its purpose is to formalize
static semantics and dynamic semantics
more conveniently on abstract syntax than on concrete syntax;
the chosen form of the abstract syntax, among many possible,
is motivated by this purpose.
This ACL2 abstract syntax of Leo is similar to
the Rust abstract syntax of Leo in the Leo compiler.
However, the two serve slightly different purposes,
and therefore they do not have to be necessarily in strict alignment.
Subtopics
- Expression
- Fixtype of Leo expressions.
- Syntax-abstraction
- Mapping from concrete to abstract syntax, for Leo code.
- Statement
- Fixtype of Leo statements.
- Files
- Leo files.
- Input-files
- Leo input files.
- Identifiers
- Leo identifiers.
- Types
- Leo types.
- Struct-init
- Fixtype of Leo struct component initializers.
- Branch
- Fixtype of Leo branches.
- Statements
- Leo statements.
- Format-strings
- Leo format strings.
- Input-syntax-abstraction
- Mapping from concrete to abstract syntax, for Leo input files.
- Expressions
- Leo expressions.
- Output-files
- Leo output files.
- Addresses
- Leo addresses.
- Literals
- Leo literals.
- Characters
- Leo characters.
- Expression-list
- Fixtype of lists of Leo expressions.
- Statement-list
- Fixtype of lists of Leo statements.
- Output-syntax-abstraction
- Mapping from concrete to abstract syntax, for Leo output files.
- Struct-init-list
- Fixtype of lists of Leo struct component initializers.
- Branch-list
- Fixtype of lists of Leo branches.
- Annotations
- Leo annotations.
- Abstract-syntax-trees
- Abstract syntax trees (ASTs).
- Symbols
- Leo symbols.
- Keywords
- Leo keywords.
- Programs
- Leo programs.
- Packages
- Leo packages.
- Bit-sizes
- Leo integer bit sizes.
