Merge pull request #304 from FissoreD/abs_with_types

[parser] allow to type binders in lambda abstractions + tests
LPCIC · Jan 6, 2025 · 8f747f8 · 8f747f8
2 parents dd169fc + cf09bfc
commit 8f747f8
Show file tree

Hide file tree

Showing 7 changed files with 102 additions and 30 deletions.
diff --git 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
@@ -99,6 +98,7 @@ program: AFTER CONJ2 VDASH
 goal: AFTER DDARROW VDASH
 goal: LBRACKET AFTER DDARROW VDASH
 program: AFTER DDARROW VDASH
+program: EXPORTDEF AFTER AFTER ARROW VDASH
 
 This infix operator expects a right hand side.
 
@@ -155,7 +155,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 +164,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 +199,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,16 +230,21 @@ 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
 goal: LBRACKET AFTER DDARROW FLOAT USE_SIG
 program: AFTER DDARROW FLOAT USE_SIG
+goal: AFTER BIND VDASH
+goal: LPAREN USE_SIG
+program: EXPORTDEF AFTER AFTER ARROW LPAREN AFTER RPAREN VDASH
+program: EXPORTDEF AFTER AFTER VDASH
+program: EXPORTDEF AFTER AFTER LPAREN USE_SIG
+program: EXPORTDEF AFTER AFTER LPAREN AFTER FULLSTOP
+program: EXPORTDEF AFTER AFTER AFTER VDASH
 
 Term expected, got keyword.
 
-goal: LPAREN USE_SIG
 goal: LPAREN FAMILY_TILDE VDASH
 
 Mixfix symbol or term expected.
@@ -334,7 +338,6 @@ type (++) list A -> list A -> list A.
 program: RULE LPAREN USE_SIG
 program: RULE VDASH
 program: RULE IFF AFTER VDASH
-program: RULE LPAREN AFTER COLON VDASH
 program: RULE AFTER VDASH
 program: RULE BIND VDASH
 program: RULE BIND AFTER VDASH
@@ -343,6 +346,7 @@ program: RULE PIPE FLOAT USE_SIG
 program: RULE IFF VDASH
 program: RULE LPAREN AFTER RTRI VDASH
 program: RULE LPAREN AFTER RTRI FLOAT USE_SIG
+program: RULE LPAREN AFTER USE_SIG
 
 Malformed CHR rule declaration. Examples:
 rule (match this).
@@ -362,12 +366,11 @@ accumulate foo, bar.
 accumulate "foo/bar".
 
 goal: LBRACKET AFTER AFTER RPAREN
-
-Closing '[' with ')'.
-
 goal: LBRACKET PIPE VDASH
 goal: LBRACKET AFTER PIPE VDASH
 goal: LBRACKET AFTER CONJ2 VDASH
+goal: LBRACKET AFTER USE_SIG
+goal: LBRACKET AFTER BIND FLOAT USE_SIG
 
 List expected. Examples:
 [ this , that | More ].
@@ -453,29 +456,18 @@ program: FUNC VDASH
 program: FUNC AFTER VDASH
 program: FUNC AFTER AFTER RPAREN
 program: FUNC AFTER ARROW VDASH
+program: FUNC AFTER LPAREN FUNC AFTER FULLSTOP
+program: FUNC AFTER LPAREN FUNC VDASH
+program: FUNC AFTER LPAREN FUNC ARROW VDASH
 
 Predicate declaration expected. Examples:
 pred append i:list A, i:list A, o:list A.
 pred append i:list A i:list A o:list A.
 pred mapR i:list A, i:(pred i:A, o:B), o:list B.
 func map list A, (func A -> B) -> list B.
 
-program: EXPORTDEF AFTER LPAREN USE_SIG
-program: EXPORTDEF AFTER LPAREN AFTER FULLSTOP
-program: EXPORTDEF AFTER AFTER ARROW VDASH
-program: EXPORTDEF AFTER AFTER ARROW LPAREN AFTER RPAREN VDASH
-program: EXPORTDEF AFTER AFTER VDASH
-program: EXPORTDEF AFTER AFTER LPAREN USE_SIG
-program: EXPORTDEF AFTER AFTER LPAREN AFTER FULLSTOP
-program: EXPORTDEF AFTER AFTER AFTER VDASH
-program: EXPORTDEF VDASH
 program: EXPORTDEF AFTER TYPE
-program: EXPORTDEF AFTER LPAREN PRED VDASH
-program: EXPORTDEF AFTER AFTER LPAREN PRED IO_COLON AFTER FULLSTOP
-program: EXPORTDEF AFTER LPAREN PRED IO_COLON AFTER FULLSTOP
-program: EXPORTDEF AFTER LPAREN FUNC VDASH
-program: EXPORTDEF AFTER LPAREN FUNC AFTER FULLSTOP
-program: EXPORTDEF AFTER LPAREN FUNC ARROW VDASH
+program: EXPORTDEF VDASH
 
 Definition export directive expected (Teyjus compatibility, ignored by Elpi).
 Examples:
@@ -548,10 +540,32 @@ 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
+goal: AFTER COLON VDASH
+goal: AFTER COLON AFTER RPAREN
+goal: AFTER COLON AFTER BIND VDASH
+goal: AFTER COLON AFTER BIND FLOAT USE_SIG
+goal: LBRACKET AFTER COLON VDASH
+goal: LPAREN AFTER COLON VDASH
+goal: LPAREN AFTER COLON AFTER IO_COLON
+goal: AFTER COLON LPAREN USE_SIG
 
-Illformed binder after type cast.
-You cannot ascribe a type to bound variables.
+Illformed type cast.
+Examples:
+(x : ty)
+pi x : ty \ t
+lam (x : ty \ t)
 
 program: LPAREN FLOAT COLON AFTER RPAREN VDASH
 
 You cannot ascribe a type on the head predicate.
+
+goal: AFTER COLON LPAREN PRED VDASH
+goal: AFTER COLON AFTER LPAREN FUNC ARROW AFTER ARROW
+goal: AFTER COLON LPAREN AFTER IO_COLON
+goal: AFTER COLON LPAREN FUNC ARROW AFTER ARROW
+
+Anonymous predicate declaration expected.
+Examples:
+(pred i:ty, o:ty)
+(pred)
diff --git 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 https://github.com/LPCIC/elpi/pull/304
+*/
 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
@@ -242,9 +242,10 @@ let _ =
   test  "p :- f \".*\\\\.aux\"." 1 17 1 0 [] (app ":-" 2 [c 0 "p";app "f" 5  [str 7 17 ".*\\.aux"]]);
   test  "p :- (f x : y)."   1 14 1 0 [] (app ":-" 2 [c 0 "p"; cast 5 14 (app "f" 6 [c 8 "x"]) (ct 13 "y")]);
   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 *)
+  (*     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")]]);
+  test  "p :- f (x : y \\ z as Y)." 1 23 1 0 [] (app ":-" 2 [c 0 "p"; app "f" 5 [app "as" ~parenl:true ~parenr:1 18 [lam "x" 9 ~ty:(ct 13 "y") (c 16 "z"); c 21 "Y"]]]);
   (*    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
@@ -0,0 +1,17 @@
+% Test for the correct parsing of binders with types
+
+pred test1.
+test1 :-
+  X = (x : bool\ x),
+  Y = X tt,
+  print Y.
+
+pred test2.
+test2 :-
+  _ = (x : bool\ x as Z),
+  Y = Z tt,
+  print Y.
+
+main :-
+  test1,
+  test2.
diff --git a/tests/sources/lambda5.elpi 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
diff --git a/tests/sources/lambda6.elpi b/tests/sources/lambda6.elpi
@@ -0,0 +1,7 @@
+% Test for the correct parsing of binders with types
+% Similar to test lambda5 but with type_checking error
+% using the as constructor
+
+main :-
+  _ = (x : bool\ x as Y),
+  _ = Y 1. % Here type error
diff --git a/tests/suite/correctness_HO.ml b/tests/suite/correctness_HO.ml
@@ -202,6 +202,23 @@ 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 "lambda6"
+  ~source_elpi:"lambda6.elpi"
+  ~description:"simple type checker"
+  ~expectation:Failure
+  ()
+
 let () = declare "hilbert"
   ~source_elpi:"hilbert/hilbert.mod"
   ~source_teyjus:"hilbert/hilbert.mod"