[parser] allow to type binders in lambda abstractions + tests

[FissoreD]

Explanation of the shift-reduce error with typed binders

Informal description of the problem

The extension of the grammar such that it is possible to give types to binders
in lambda abstractions causes a shift/reduce conflict since the sentence:

(x : ty \ t as y) ...

is ambiguous.

It can be shifted by:

  closed_term 
  LPAREN term AS term RPAREN 
        binder_term 
        constant . COLON type_term BIND term 

and reduced by:

  head_term nonempty_list(closed_term) option(binder_body_no_ty) 
  LPAREN term COLON type_term RPAREN // lookahead token appears
        closed_term // lookahead token is inherited
        head_term // lookahead token is inherited
        constant . 

The ambiguity may occur if we had the derivation (meaningless in our grammar):

type_term: type_term BIND term AS term { ... }

Allowing the sentence: (x : ty \ t as y) ... to be derived in two distinct
ways.

Solution of the problem:

The derivation we want is the shifted one:

  (     .         as   y )           # from the closed term AS rule
     x : ty \ y                      # from the binder with type rule

To solve the issue,the constant production of the head_term rule must
have lower priority than the COLON token. Therefore, we add to the grammar:

%nonassoc colon_minus1
%nonassoc COLON

such that colon_minus1 has lower priority than the token COLON. Finally we
attach the tag colon_minus1 to the constant production of the head_term
rule.

This way, the reduction head_term nonempty_list(closed... is neglected in
favour of the the wanted derivation.

Note that the production rule:

head_term: 
  LPAREN; t = constant; COLON; ty = type_term RPAREN 
    { mkCast (loc $loc) (mkConst (loc $loc(t)) t) ty }`

has to be added, otherwise (x : int) could not be parsed, this is because of
the impossibility of parsing the CONSTANT before a COLON in the rule
head_term.

BELOW THE TRACE OF THE SHIFT/REDUCE CONFLICT

** Conflict (shift/reduce) in state 137.
** Token involved: COLON
** This state is reached from goal after reading:

LPAREN constant

** The derivations that appear below have the following common factor:
** (The question mark symbol (?) represents the spot where the derivations begin to differ.)

goal 
term EOF 
(?)

** In state 137, looking ahead at COLON, shifting is permitted
** because of the following sub-derivation:

closed_term 
LPAREN term AS term RPAREN 
       binder_term 
       constant . COLON type_term BIND term 

** In state 137, looking ahead at COLON, reducing production
** head_term -> constant
** is permitted because of the following sub-derivation:

open_term 
head_term nonempty_list(closed_term) option(binder_body_no_ty) 
LPAREN term COLON type_term RPAREN // lookahead token appears
       closed_term // lookahead token is inherited
       head_term // lookahead token is inherited
       constant . 

[FissoreD]

I'm not sure about the error messages added in error_messages.txt

[gares]

Looks great, thanks!!

I don't think supporting the type ascription in head term is relevant, since it is known to be prop. But if it doesn't hurt we can keep it.

I think a shorter description in grammar is enough (just add the ambiguous text), and the rest of the explanation can go to the git commit.

Can you add a unit test with as? From the doc it looks it is still parsed correctly, but I prefer to have some test

[FissoreD]

• update the pr description and in grammar accordingly
• force push tests with as symbol
• not sure how to simply remove the type ascription in head term

[gares]

I think this error should become something like: illformed type annotatio n, here a few examples.