Syntax abstraction mapping.
We define the mapping from concrete syntax to abstract syntax. The mapping maps concrete syntax trees (CSTs), which are defined by the ABNF grammar, to abstract syntax trees (ASTs), which are defined as fixtypes in the abstract syntax, or to data that is part of those ASTs.
This mapping formalizes the relation between concrete and abstract syntax. In particular, it is needed to express formal properties of our parser and printer.
The definition of this syntax abstraction mapping is work in progress.