From 149f3e3360e058f71c100cc9f108aca30eecacf5 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Wed, 1 Jan 2025 23:42:27 +0100 Subject: [PATCH] [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 | 110 ++++++++++++++++++++++++++++++++++ src/parser/error_messages.txt | 6 +- src/parser/grammar.mly | 12 +++- src/parser/test_parser.ml | 2 +- tests/sources/lambda4.elpi | 6 ++ tests/sources/lambda5.elpi | 8 +++ tests/suite/correctness_HO.ml | 11 ++++ 7 files changed, 148 insertions(+), 7 deletions(-) create mode 100644 src/parser/conflict_COLON.md create mode 100644 tests/sources/lambda4.elpi create mode 100644 tests/sources/lambda5.elpi diff --git a/src/parser/conflict_COLON.md b/src/parser/conflict_COLON.md new file mode 100644 index 000000000..6613de27f --- /dev/null +++ b/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 . +``` \ No newline at end of file diff --git a/src/parser/error_messages.txt b/src/parser/error_messages.txt index d8589e059..d4a755a1d 100644 --- a/src/parser/error_messages.txt +++ b/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. diff --git a/src/parser/grammar.mly b/src/parser/grammar.mly index aeb4d0342..eeef7fda1 100644 --- a/src/parser/grammar.mly +++ b/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) } diff --git a/src/parser/test_parser.ml b/src/parser/test_parser.ml index 32b94e63c..52c8d3de5 100644 --- a/src/parser/test_parser.ml +++ 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." (); diff --git a/tests/sources/lambda4.elpi b/tests/sources/lambda4.elpi new file mode 100644 index 000000000..bb44bd6f4 --- /dev/null +++ b/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. \ No newline at end of file diff --git a/tests/sources/lambda5.elpi b/tests/sources/lambda5.elpi new file mode 100644 index 000000000..21eadfaa3 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/tests/suite/correctness_HO.ml b/tests/suite/correctness_HO.ml index 43d6f9a3b..16d6cd5aa 100644 --- a/tests/suite/correctness_HO.ml +++ b/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"