\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#3})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

# 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 `1` can be interpreted as the natural number `S O` then `2` is interpreted as `S (S O)`, then `2 * 2` as `Nat.mul (S (S O)) (S (S O))` and finally our whole term as `Nat.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.

Other versions v: 9.2

Versions
  dev
  stable
  9.2
  9.1
  9.0
  8.20
  8.19
  8.18
  8.17
  8.16
  8.15
  8.14
  8.13
  8.12
  8.11
  8.10
  8.9
  8.8
  8.7
  8.6
  8.5
  8.4
  8.3
  8.2
  8.1
  8.0

Downloads
  PDF