Fixed some menhir parser precedence bugs; added more menhir parser te…

…sts; issue with LESS_THAN in menhir still persists; disabled the basic_reference test for now (see issue on GitHub)
hazelgrove · Oct 29, 2024 · f5886c3 · f5886c3
2 parents 9d2b7db + ed962c0
commit f5886c3
Show file tree

Hide file tree

Showing 7 changed files with 228 additions and 94 deletions.
diff --git a/src/haz3lmenhir/AST.re b/src/haz3lmenhir/AST.re
@@ -83,6 +83,7 @@ type typ =
 
 [@deriving (show({with_path: false}), sexp)]
 type pat =
+  | CastPat(pat, typ, typ)
   | EmptyHolePat
   | WildPat
   | IntPat(int)

diff --git a/src/haz3lmenhir/Conversion.re b/src/haz3lmenhir/Conversion.re
@@ -255,6 +255,8 @@ and Pat: {
     | InvalidPat(s) => Invalid(s)
     | IntPat(i) => Int(i)
     | FloatPat(f) => Float(f)
+    | CastPat(p, t1, t2) =>
+      Cast(of_menhir_ast(p), Typ.of_menhir_ast(t1), Typ.of_menhir_ast(t2))
     | VarPat(x) => Var(x)
     | ConstructorPat(x, ty) => Constructor(x, Typ.of_menhir_ast(ty))
     | StringPat(s) => String(s)

diff --git a/src/haz3lmenhir/Lexer.mll b/src/haz3lmenhir/Lexer.mll
@@ -109,6 +109,7 @@ rule token =
     | "typfun" {TYP_FUN}
     | "type" {TYP}
     | "$" {DOLLAR_SIGN}
+    | "named_fun" {NAMED_FUN}
     | identifier as i { IDENT(i) }
     | constructor_ident as i { CONSTRUCTOR_IDENT(i)}
     | eof { EOF }

diff --git a/src/haz3lmenhir/Parser.mly b/src/haz3lmenhir/Parser.mly
@@ -4,7 +4,7 @@ open AST
 
 
 
-
+%token NAMED_FUN
 %token UNDEF
 %token <string> SEXP_STRING
 %token DOLLAR_SIGN
@@ -110,16 +110,13 @@ open AST
 %left OPEN_PAREN
 %left QUESTION
 %left COLON
-%left COMMA
+(* %left COMMA *)
 %left AT_SYMBOL
 %left SEMI_COLON
 %left IN
 %left DOLLAR_SIGN
 %left L_NOT L_AND L_OR
 
-(* Might not be correct - milan *)
-%left IDENT
-
 %type <AST.exp> exp
 
 %start <AST.exp> program
@@ -181,13 +178,16 @@ typ:
     | t1 = typ; DASH_ARROW; t2 = typ { ArrowType(t1, t2) }
 
 pat:
+    | p1 = pat; COLON; t1 = typ;  { CastPat(p1, t1, UnknownType(Internal)) }
+    | p1 = pat; LESS_THAN; t1 = typ; EQUAL_ARROW; t2 = typ; GREATER_THAN { CastPat(p1, t1, t2) }
+    | OPEN_PAREN; p = pat; CLOSE_PAREN { p }
+    | OPEN_PAREN; p = pat; COMMA; pats = separated_list(COMMA, pat); CLOSE_PAREN { TuplePat(p :: pats) }
     | QUESTION; s = STRING { InvalidPat(s) }
     | WILD { WildPat }
     | QUESTION { EmptyHolePat }
     | OPEN_SQUARE_BRACKET; l = separated_list(COMMA, pat); CLOSE_SQUARE_BRACKET; { ListPat(l) }
     | c = CONSTRUCTOR_IDENT; COLON; t = typ;  { ConstructorPat(c, t) }
     | p = IDENT { VarPat(p) }
-    | t = patTuple { t }
     | i = INT { IntPat i }
     | f = FLOAT { FloatPat f }
     | s = STRING { StringPat s}
@@ -198,9 +198,6 @@ pat:
     | f = pat; OPEN_PAREN; a = pat; CLOSE_PAREN { ApPat(f, a) }
 
 
-patTuple: 
-    | OPEN_PAREN; pats = separated_list(COMMA, pat); CLOSE_PAREN { TuplePat(pats) }
-
 rul:
     | TURNSTILE; p = pat; EQUAL_ARROW; e = exp; { (p, e) }
 
@@ -209,7 +206,7 @@ case:
 
 funExp: 
     | FUN; p = pat; DASH_ARROW; e1 = exp; { Fun (p, e1, None) }
-    | FUN; p = pat; DASH_ARROW; e1 = exp; name = IDENT { Fun (p, e1, Some(name)) }
+    | NAMED_FUN; name = IDENT; p = pat; DASH_ARROW; e1 = exp { Fun (p, e1, Some(name)) }
 
 
 %inline ifExp:
@@ -254,7 +251,7 @@ exp:
     | FIX;  p = pat; DASH_ARROW; e = exp { FixF(p, e) }
     | TYP_FUN; t = tpat; DASH_ARROW; e = exp {TypFun(t, e)}
     | QUESTION { EmptyHole }
-    | a = filterAction; cond = exp; COMMA; body = exp { Filter(a, cond, body)}
+    | a = filterAction; cond = exp; IN; body = exp { Filter(a, cond, body)}
     | TEST; e = exp; END { Test(e) }
     | e1 = exp; AT_SYMBOL; e2 = exp { ListConcat(e1, e2) }
     | e1 = exp; CONS; e2 = exp { Cons(e1, e2) }

diff --git a/test/Test_Elaboration.re b/test/Test_Elaboration.re
@@ -265,9 +265,8 @@ module MenhirElaborationTests = {
 
   let let_fun_str = "
 let f =
-    fun x ->
+    named_fun f x ->
         1 + x
-    f
     in
 55";
 
@@ -489,7 +488,7 @@ let f =
   let test_menhir = () =>
     alco_check_menhir("Test failed (menhir)", test_str, test_uexp);
 
-  let filter_str = "eval 1, 0";
+  let filter_str = "eval 1 in 0";
   let stepper_filter_kind =
     TermBase.StepperFilterKind.Filter({
       pat: Int(1) |> Exp.fresh,