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

- no shift-head reduce error when adding types to abstractions
- conflict_COLON.md contains a description about the resolution of the error
- add some tests (one positive and one negative)

src/parser/conflict_COLON.md

@@ -0,0 +1,110 @@
+# Explanation of the shift-reduce error with typed binders
+(At the end of the file there is a copy paste of the original conflict message)
+
+## 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, with the derivation tree:
+
+```
+  (     .         as   y )           # from the closed term AS rule
+     x : ty \ y                      # from the binder with type rule
+```
+
+To solve the issue, we want the `constant` production of the `head_term` rule to
+have lower priority than the `COLON` token. To do so we add to the grammar:
+
+```
+%nonassoc colon_minus1
+%nonassoc COLON
+```
+
+where `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 . 
+```

src/parser/error_messages.txt

@@ -76,7 +76,6 @@ goal: LBRACKET AFTER DARROW VDASH
 goal: LBRACKET AFTER ARROW VDASH
 goal: LBRACKET AFTER QDASH VDASH
 goal: LPAREN AFTER AS VDASH
-goal: AFTER BIND VDASH
 goal: LBRACKET AFTER CONJ VDASH
 goal: LBRACKET AFTER BIND VDASH
 goal: AFTER MINUSs VDASH
@@ -155,7 +154,6 @@ goal: LBRACKET AFTER FAMILY_BTICK FLOAT USE_SIG
 goal: LBRACKET AFTER CONS FLOAT USE_SIG
 goal: LBRACKET AFTER FAMILY_GT FLOAT USE_SIG
 goal: LBRACKET AFTER FAMILY_EQ FLOAT USE_SIG
-goal: LBRACKET AFTER BIND FLOAT USE_SIG
 goal: LBRACKET AFTER OR FLOAT USE_SIG
 goal: LBRACKET AFTER IS FLOAT USE_SIG
 goal: LBRACKET AFTER EQ FLOAT USE_SIG
@@ -165,7 +163,6 @@ goal: FAMILY_TILDE FLOAT USE_SIG
 goal: LPAREN AFTER AS FLOAT USE_SIG
 goal: FLOAT USE_SIG
 goal: AFTER QDASH FLOAT USE_SIG
-goal: LBRACKET AFTER USE_SIG
 goal: AFTER OR FLOAT USE_SIG
 goal: AFTER IS FLOAT USE_SIG
 goal: AFTER CONS FLOAT USE_SIG
@@ -201,6 +198,7 @@ goal: LBRACKET AFTER QDASH FLOAT USE_SIG
 goal: LBRACKET AFTER PIPE FLOAT USE_SIG
 program: FAMILY_TILDE FLOAT USE_SIG
 goal: LPAREN LBRACKET RBRACKET USE_SIG
+goal: LPAREN AFTER USE_SIG
 program: LPAREN AFTER RPAREN USE_SIG
 goal: AFTER MINUSs FLOAT USE_SIG
 goal: AFTER MINUSr FLOAT USE_SIG
@@ -231,7 +229,6 @@ goal: PI AFTER COLON VDASH
 goal: LBRACKET FLOAT USE_SIG
 goal: AFTER AFTER BIND VDASH
 goal: AFTER AFTER BIND FLOAT USE_SIG
-goal: LBRACKET AFTER COLON VDASH
 goal: LBRACKET AFTER COLON AFTER RPAREN
 goal: LBRACKET AFTER COLON AFTER BIND VDASH
 goal: AFTER DDARROW FLOAT USE_SIG
@@ -548,6 +545,7 @@ sigma X\ p X
 sigma X Y Z\ p X, q Y Z
 
 goal: LPAREN FLOAT COLON AFTER IO_COLON
+goal: LPAREN FLOAT COLON VDASH
 
 Illformed binder after type cast.
 You cannot ascribe a type to bound variables.

src/parser/grammar.mly

@@ -142,6 +142,9 @@ let mode_of_IO io =
 %type < 'a TypeExpression.t > type_term
 %type < 'a TypeExpression.t > atype_term
 
+%nonassoc colon_minus1
+%nonassoc COLON
+
 (* entry points *)
 %start program
 %start goal
@@ -385,9 +388,14 @@ closed_term:
 | l = LCURLY; t = term; RCURLY { mkAppF (loc $loc) (loc $loc(l),Func.spillf) [t] }
 | t = head_term { t }
 
+/*
+Here we set the precedence to the 'constant' production of head_term.
+See conflict_COLON.md for a brief explanation
+*/
 head_term:
-| t = constant { mkConst (loc $loc) t }
+| t = constant %prec colon_minus1 { mkConst (loc $loc) t }
 | LPAREN; t = term; RPAREN { mkParens_if_impl_or_conj (loc $loc) t }
+| LPAREN; t = constant; COLON; ty = type_term RPAREN { mkCast (loc $loc) (mkConst (loc $loc(t)) t) ty }
 | LPAREN; t = term; COLON; ty = type_term RPAREN { mkCast (loc $loc) t ty }
 
 list_items:
@@ -402,7 +410,7 @@ list_items_tail:
 
 binder_term:
 | t = constant; BIND; b = term { mkLam (loc $loc) (Func.show t) None b }
-// | t = constant; COLON; ty = type_term; BIND; b = term { mkLam (loc $loc) (Func.show t) (Some ty) b }
+| t = constant; COLON; ty = type_term; BIND; b = term { mkLam (loc $loc) (Func.show t) (Some ty) b }
 
 binder_body_no_ty:
 | bind = BIND; b = term { (loc $loc(bind), None, b) }

src/parser/test_parser.ml

@@ -244,7 +244,7 @@ let _ =
   test  "p :- pi x : y \\ z."   1 17 1 0 [] (app ":-" 2 [c 0 "p"; app "pi" 5 [lam "x" 9 ~ty:(ct 13 "y") (c 16  "z")]]);
   (*    01234567890123456789012345 *)
   test  "p :- f (x : y)."   1 14 1 0 [] (app ":-" 2 [c 0 "p"; app "f" 5 [cast 7 14 (c 8 "x") (ct 13 "y")]]);
-  testF "p :- f (x : y \\ z)." 15 "Illformed binder";
+  test  "p :- f (x : y \\ z)." 1 18 1 0 [] (app ":-" 2 [c 0 "p"; app ~parenr:1 "f" 5 [lam "x" 9 ~ty:(ct 13 "y") (c 16 "z")]]);
   (*    01234567890123456789012345 *)
   testT "func x int, int -> bool, bool."          ();
   testT "func x int, list int -> bool."           ();

tests/sources/lambda4.elpi

@@ -0,0 +1,6 @@
+% Test for the correct parsing of binders with types
+
+main :-
+  X = (x : bool\ x),
+  Y = X tt,
+  print Y.

tests/sources/lambda5.elpi

@@ -0,0 +1,8 @@
+% Test for the correct parsing of binders with types
+% Similar to test lambda4 but with type_checking error
+% since the lambda term is applied to a term with 
+% an unexpected type
+
+main :-
+  X = (x : bool\ x),
+  Y = X 1. % Here type error

tests/suite/correctness_HO.ml

@@ -202,6 +202,17 @@ let () = declare "lambda_arrow2"
   ~description:"simple type checker"
   ()
 
+let () = declare "lambda4"
+  ~source_elpi:"lambda4.elpi"
+  ~description:"simple type checker"
+  ()
+
+let () = declare "lambda5"
+  ~source_elpi:"lambda5.elpi"
+  ~description:"simple type checker"
+  ~expectation:Failure
+  ()
+
 let () = declare "hilbert"
   ~source_elpi:"hilbert/hilbert.mod"
   ~source_teyjus:"hilbert/hilbert.mod"