Coq's built-in extensible parser, although quite convenient in many cases, does have some limitations. On one hand, some syntax extensions that one might like to write cannot be expressed in it. Furthermore, the extensions are not first-class, having to be defined outside of the core language. We will see how to implement some interesting syntax extensions in Coq using just coercions and regular Coq functions. Besides being first-class, we will see that the mechanism can be used for defining extensions that cannot be expressed just with Coq's extensible parser. We want to describe each syntax extension with a few Coq types and functions that determine how it should be parsed. Our first attempt might look like this:

Our parser works by reading tokens and returning a value of type result at the end of the process. It does this by starting with some value initial_result and updating that value with each token read, using function read_token. For instance, here's a function that returns the result of parsing three tokens:

We can use this definition as a syntax extension by declaring read_token as a coercion from result to Funclass, allowing us to use each result as if it were a function. Then, applying initial_result p to a sequence of tokens will correspond to calling our parser on that sequence.

This works because each application of read_token returns a result, so trying to apply that updated result to another token triggers yet another coercion, allowing the process to continue indefinitely. We can check that both definitions of read_three_tokens yield the same function, meaning that the coercion is behaving as expected:

To make the mechanism more robust, we wrap our parser in a new type, ensuring that the Coq type checker will not fail to perform some coercion by reducing result more than it should.

As a last tweak, we declare another coercion and a notation to make using our embedded parsers more similar to other systems, like in Template Haskell:

Now, we can invoke a parser simply by writing [name_of_parser <list of tokens>]:

As a first example, we can define an alternative syntax for Coq lists that doesn't need separators between the elements.

The listp parser is parameterized by X, the type of the elements on the list. We initialize the parser with an empty list, and each token that we read is an element of X, which will be progressively added at the end of our list.

More parsers

While nice, listp is not especially interesting as a parser, since it doesn't really analyze the tokens it reads. In contrast, parsers usually treat tokens differently, depending on what it has been read so far. To take such dependencies into account, we introduce some new fields to our record:

The state field represents the internal state of our parser at a given point. It is set initially set to initial_state, and is updated using function next. We also change read_token to pass it the current state as an additional argument. While more general, this version isn't quite good yet. We require our parsers to carry around a complete result value that it can return after having read any sequence of tokens. Usually, however, parsing can result in errors, and there is no meaningful value that can be returned by the parser until it finishes its job. To solve this problem, we introduce one last change to our definition: dependent types.

Now, the type of tokens expected by the parser, as well as its type of partial results, can depend on the current parsing state, and the parsing functions have been updated to take this dependency into account. With dependent types, the type of the value being built, partial_result, can change during the parsing process, allowing us to distinguish a complete, successfully parsed result, from one that still needs more tokens, or even from a message describing a parse error. By making token depend on the current state, we can constrain which tokens can be read at each parsing state, allowing us to expose parse errors as type errors. For listp, there is no need to use anything interesting for the state type. For more complicated parsers, however, state comes in handy. To see how, we will define parsers for prefix and postfix arithmetic expressions. This is also a nice example because prefix and postfix expressions cannot be handled by Coq's extensible parser alone. Expressions can involve three operations: addition, subtraction and multiplication.

The parsers will read tokens that can be natural numbers or one of the above operations. We group those in a common type exp_token.

Let's consider how to deal with prefix expressions first. At any point during parsing, the parser is waiting for some number of additional expressions it must read in order to complete the top-level expression. We will use this number as the parser state. Initially, the parser wants to read just one expression, so we will use that as the initial state. Once the state reaches zero, there are no more expressions to read, so we know that the parser is done.

If our current state is zero, any additional tokens fed to the parser should result in a parse error. To implement this behavior, we define the type of tokens for that state to be Empty_set. Trying to feed an extra token to parser at that point will result in a type error, signaling that a parse error just occurred. If the parser still expects expressions (i.e., if the current state is greater than zero), we just use exp_token for the token type.

The value built by the parser will be a continuation that expects n numbers, one for each expression that the parser still needs to read.

We must define how the parser actually interprets the tokens it reads. If the parser expects n expressions, reading a constant will make this number go down by one, since a constant is a complete expression. If it reads an operation, on the other hand, that number is increased by one. If n = 0, there is no token to be read, hence no next state, so we perform an empty pattern match to show that can't happen.

How do we update the result? If we read a constant, we just feed it to the continuation. If we read an operation, we compose that operation with the continuation, which has the net effect of adding one argument to it. Here, ap_op is a function that maps each op to the corresponding Coq function.

We can now package our definitions as a complete parser and try it on some examples:

We can also see that invalid expressions are rejected, as expected.

Error: The term "1" has type "nat" while it is expected to have type
"token pre (next pre (next pre (next pre (initial_state pre) '+) 1) 1)".

A parser for postfix expressions is in some sense the dual of the one we've just seen: instead of carrying around a continuation that expects arguments, we construct a stack of numbers on which we can perform our operations. Our state will also be a number, denoting the number of elements on our stack. Since our stack start empty, the initial state will be zero.

Since our operations need at least two numbers on the stack, we restrict our parser to accept only numbers if the stack doesn't have the appropriate size:

The partial_result type is a length-indexed list of natural numbers with one small twist: we ensure that partial_result 1 = nat definitionally, so that we can use postfix expressions as having type nat without the need for any projections.

next and read_token are dual to the definitions of the previous parser: reading a constant increases the stack size by one, while reading an operation decreases the stack size by one.

We now have a full parser for postfix expressions, which we can test on some examples.

Summary

We've seen how we can use coercions to extend the syntax of Coq. While useful, this technique is complementary to Coq's own extensible parser, having its own limitations. Despite being very programmable, there are also syntax extensions that cannot be defined with this technique in a seamless way, such as anything involving variable binding. Being first class can also be a disadvantage, since the parser and parsing functions are part of the resulting term, possibly affecting conversion and unification. Finally, regular syntax extensions are defined with a high-level declarative syntax, while this mechanism requires one to write a custom parser for each extension.