Command level processing
When a command, for instance Check 1 + 2 * 2. is fed to Rocq, it
goes through several successive processing steps:
lexing splits the input string into a sequence of tokens ;
parsing converts the sequence of tokens into a syntax tree ;
synterp does just enough to be able to proceed parsing the file (that is, executes the few commands that can modify the lexer or parser) ;
interp executes the bulk of the parsed commands.
Note
Understanding the distinction between lexing and parsing is sometimes required to make good use of the notation features. The synterp/interp distinction, while important for developers, should be mostly transparent for users.
Lexing
The first step, lexing splits the input into a sequence of
tokens, for instance the string "Check 1 + 2 * 2." is split into
the sequence of seven tokens 'Check' '1' '+' '2' '*' '2' '.'. A set
of basic tokens are predefined and can be
extended, in particular by
reserving notations.
Parsing
During parsing the sequence of tokens is interpreted as a tree, for instance here:
Check
|
+
/ \
1 *
/ \
2 2
The parsed grammar can be modified, for instance by reserving notations.
Synterp
In addition to the above lexing and parsing, the synterp phase
does just enough to be able to parse the remaining commands.
Typically, this means applying the effects of Reserved Notation
commands. Plugins loading, Require and Import commands
can also have synterp effects.
Interp
The interp phase performs the specific effect of each command. If the command contains terms, they will be processed in distinct steps as explained below.
Note
Depending on the Rocq interface used (rocq compile, rocq
top or various IDEs), Rocq may run the interp phase for each
command immediately after its synterp phase, or it may run the
synterp phase for every command in the file before running any
interp step, or any other interleaving.
Term level processing
It is in theory possible to write down every term explicitly
as described in the Core Language part of this
manual, for instance
Nat.add (S O) (Nat.mul (S (S O)) (S (S O))). However, this would
be very tedious and error-prone and takes us away from our usual
mathematical practice. To circumvent this, Rocq offers multiple
preprocessing mechanisms to help fill the gap between what the users
would like to input to the system and the fully formal core language
expected by the kernel. We give an overview of all these steps below.
For instance, the notation mechanisms reflect the eponymous mathematical
practice and allows to write 1 + 2 * 2 instead of the above
term. Those mechanisms range from simple Abbreviations to full
fledged Notations with user defined syntaxes. Multiple interpretations can be given to the
same syntax in different contexts thanks to the scope mechanism. For instance (1 + 2 * 2)%N can be
the above natural number expression while (1 + 2 * 2)%Z can be
an expression with integers.
In order to take the best part of all these preprocessing mechanisms, one needs a basic understanding of the multiple steps needed to transform an inputted term (possibly with notations) into the valid Gallina term which Rocq will ultimately use internally. Terms given as input to Rocq go through several successive steps:
First, lexing, then parsing, are performed as part of any command processing, as described above.
During internalization a number of things are resolved. This includes name resolution, notation interpretation and introduction of holes for implicit arguments. Notation interpretation translates each syntactic element to a term, for instance
1can be interpreted as the natural numberS Othen2is interpreted asS (S O), then2 * 2asNat.mul (S (S O)) (S (S O))and finally our whole term asNat.add (S O) (Nat.mul (S (S O)) (S (S O))). The same expression can be given multiple interpretations in various contexts thanks to Notation scopes.Finally, type inference, can use the various mechanisms described in this section to fill gaps (for instance with canonical structures or Typeclasses) or fix terms (for instance with coercions) to obtain fully detailed terms in the Core Language.
For each term, Rocq performs these steps successively and independently. Then, the result goes through the type checking phases discussed in previous chapter. None of the steps has any impact on the previous ones. In particular, no typechecking is involved during parsing or internalization. Also note that none of the features resolved during these phases, like unqualified names, implicit arguments or notations, remains during the later type inference and type checking phases.
Note
The type inference phase together with, all or part of, the previous steps is sometimes called elaboration in the literature.
Example: Simple interleaving of intern and type inference phases
The command Definition foo : T := body. has a trivial
synterp phase. Indeed, it doesn't influence any further
parsing. Its interp phase will internalize T and infer
types in it, then it will internalize body and infer types in
it, using T as expected type. Note that the result of type
inference in T matters in internalization of body, for
instance for selecting notation scopes. Finally, the resulting
foo : T := body is sent to the kernel.
Example: Delayed steps
Ltac foo := exact term. will internalize term and save
the result. Only when the foo tactic will be called, will the
type inference on the resulting term be run, with the type of
the current goal as expected type. If this succeeds, the proof
state will be updated to fill the goal, and the kernel will see the
result at Qed.
Example: Reserved notation
The command Reserved Notation "x + y" (at level 50, left
associativity). has a non trivial synterp phase, as it extends the
parser so that _ + _ can later be parsed. Its interp phase is
then trivial, as there is nothing left to do.