Chapter 9: Syntax extensions
In this chapter, we introduce advanced commands to modify the way Coq parses and prints objects, i.e. the translations between the concrete and internal representations of terms and commands. As in most compilers, there is an intermediate structure called Abstract Syntax Tree (AST). Parsing a term is done in two steps( We omit the lexing step, which simply translates a character stream into a token stream. If this translation fails, this is a Lexical error. ):-
An AST is build from the input (a stream of tokens), following
grammar rules. This step consists in deciding whether the input
belongs to the language or not. If it is, the parser transforms the
expression into an AST. If not, this is a syntax error. An expression
belongs to the language if there exists a sequence of grammar rules
that recognizes it. This task is delegated to Camlp4. See the
Reference Manual [29] for details on the parsing
technology. The transformation to AST is performed by executing
successively the actions bound to these rules.
- The AST is translated into the internal representation of commands and terms. At this point, we detect unbound variables and determine the exact section-path of every global value. Then, the term may be typed, computed, ...
In Coq, only the translations between AST's and the concrete representation are extendable. One can modify the set of grammar and printing rules, but one cannot change the way AST's are interpreted in the internal level.
In the following section, we describe the syntax of AST expressions, involved in both parsing and printing. The next two sections deal with extendable grammars and pretty-printers.