Rules for well-formed parsers

With Parser and ParserDescr/syntax, we have two levels of abstraction for defining parsers. In both cases, however, it is possible to define parsers that break as-of-yet unwritten rules, confusing meta programs such as quotations and the pretty printer. We should define these rules, ideally enforce them at least for syntax by construction, and possibly lint them for Parser.

Abstract rule

The abstract rule is that the structure of the parser output should uniquely determine the parser call graph/grammar derivation tree that produced it. By "structure" (of a Syntax tree) we mean the tree modulo atoms, i.e. exactly what is considered when matching against quotations. An example of a parser breaking this rule is "foo" >> ident <|> "bar" >> term: ignoring atoms, we cannot know which alternative accepted the input bar x. Note that ident <|> term itself would be unambiguous because <|> is left biased. In theory, term <|> ident would also be acceptable, but we would need to know whether ident is part of the term category (or rather, whether the produced kind is so) to decide this case in practice.

Another counter example is many and other repetition combinators. In many p, if p is of unknown "arity" (# of produced nodes), we don't know which syntax node child belongs to which "sequence element". This was "fixed", but that fix is no good either: if we encounter a null node inside of a many p output, we don't know in general whether many introduced it because of arity > 1 or whether it was produced by p itself. We either have to wrap every sequence element in a node, which would be wasteful, or demand that p is of constant arity 1.

In practice, we should strengthen this abstract rule: it should be possible to efficiently determine the grammar derivation based on a reasonable amount of static information. For example, we might not want to add new metadata that lets us decide whether ident is in term like we would need to above. And ideally we would like to decide <|> by looking at the root kind of the output alone instead of having to dive further into the syntax tree.

Implementation for syntax

Based on the above rule, here is a proposal for a conservative approximation for syntax, to be implemented in the translation to ParserDescr:

• For each stx subterm, we compute the arity and, for arity 1, the produced kind, if known and unique
  • for parser aliases, we specify this metadata at registration time
  • categories have arity 1 and an unknown kind
  • for references to parser definitions (of type ParserDescr or Parser), we assume the arity is 1 and the kind is the declaration name. This is correct for syntax ... := and ... := leading/trailing_parser ... declarations, but obviously not in general. We could inspect the definition to be sure, except we can't if we want to make effective use of the module system. Alternatively, we could store the information in an environment extension.
• In many p and other repetition combinators, we check that p is of arity 1
• In p <|> q, we conservatively check that p has a unique produced kind that is not null (since for null we should not assume that there is a unique parser producing it), and that the RHS is of arity 1.
  • We might also want to allow $strLit <|> $strLit as a special case. However, this is not a great way to define e.g. Unicode alternatives since it ignores pp.unicode.
  • We might allow p of kind null if q also has a kind, and it is not null. This would not work with p <|> q <|> r, however.
• In Notation.lean, the only syntax declaration that does not already fulfill these rules should be

syntax location := withPosition("at " locationWildcard <|> locationHyp)

With the additional null rule mentioned above, it should be acceptable with group("at " locationWildcard).

Implementation for Parser & removal of backtracking in the pretty printer

TBD

Start by reading the abstract rule and the proposed translation to ParserDescr, then inspect Notation.lean and the Parser, ParserDescr, and syntax implementations mentioned in the issue. Determine how arity and produced-kind metadata are represented and which existing syntax declarations satisfy the proposed checks. Done means the rules are defined and enforced or linted as scoped, with the pretty-printer and Parser work explicitly resolved rather than left as TBD.