Allow --prefix, --infix and --postfix pragmas to refer to later constant declarations

[MartyO256]

Motivation

Before v1.1, it was possible to declare an identifier as an operator before any constant declaration was attached to that identifier.

For instance, the following snippet first defines ~ as an infix operator, then declares an LF type-level constant with identifier ~. This made it possible to use that infix notation in the definition of LF term-level constants.

--infix ~ 1 right.

LF ~ : tm → exp → type =
  | tr_unit : unit ~ unit'
  | tr_pair : M ~ E → N ~ F
              → (pair M N) ~ (pair' E F)

The re-write of the parser in #266 to support shadowing of constants and the definition of namespaces broke that feature. Indeed, it became necessary for fixity pragmas to refer to constants that are already bound. This meant that parsing the pragma --infix ~ 1 right. would result in an "Unbound identifier ~" exception to be thrown.

The reason why this breaking change occurred is because in the disambiguation state, the notation for an identifier has to be attached to the constant it is meant to affect. This is necessary because opening a module with the --open pragma has to bring that notation back in scope.

Changes

This PR re-introduces the feature of having a --prefix, --infix or --postfix pragma before the declaration it is meant to affect. During the disambiguation of Beluga signatures, when a fixity pragma is encountered, a lookahead is performed to determine if the closest declaration that follows the pragma introduces a constant with the same identifier as the target of the pragma. If it is the case that this next declaration introduces the pragma's target, then the fixity pragma is said to be postponed, in the sense that it is applied once that constant is added to the disambiguation state.

Put more precisely, if P is a fixity pragma with target identifier c, and D is a declaration that introduces a constant with identifier c, then P is a postponed fixity pragma if we have the following in a Beluga signature file:

P (<prefix-pragma> | <infix-pragma> | <postfix-pragma> | <documentation-comment>)* D

This makes it possible to write snippets like the following:

--assoc right.

--infix app 1 none.
--prefix lam 1.
--prefix red 2.

LF term : type =
| app: term -> term -> term =
| lam: (term -> term) -> term
| red: term -> term;

The ./t/code/success/infix/postponed.bel test case is added to showcase this feature.

If a fixity pragma is found not to be postponed, then it affects a constant declared earlier in the signature, like it did in v1.1. The proposed lookahead solution does not introduce ambiguity in the placement of fixity pragmas. If the pragma is between two declarations that use the same identifier, then the pragma is postponed. Attaching the pragma to the earlier declaration would not be useful since that constant is immediately shadowed by the other declaration.

This change affects all the areas where fixity pragmas are involved, namely:

• Signature disambiguation
• Pretty-printing of the external syntax
• Pretty-printing of the external syntax to HTML pages
• Pretty-printing of the internal syntax (using the legacy OpPragmas store, which is constructed during signature reconstruction)