Reworked the constructor menhir parsing to match maketerm

hazelgrove · Nov 4, 2024 · 574c359 · 574c359
1 parent 6b36552
commit 574c359
Show file tree

Hide file tree

Showing 4 changed files with 19 additions and 5 deletions.
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}
+    | "~" {TILDE}
     | "named_fun" {NAMED_FUN}
     | identifier as i { IDENT(i) }
     | constructor_ident as i { CONSTRUCTOR_IDENT(i)}

diff --git a/src/haz3lmenhir/Parser.mly b/src/haz3lmenhir/Parser.mly
@@ -3,7 +3,7 @@ open AST
 %}
 
 
-
+%token TILDE
 %token NAMED_FUN
 %token UNDEF
 %token <string> SEXP_STRING
@@ -110,6 +110,7 @@ open AST
 %left OPEN_PAREN
 %left QUESTION
 %left COLON
+%left TILDE
 (* %left COMMA *)
 %left AT_SYMBOL
 %left SEMI_COLON
@@ -186,7 +187,8 @@ pat:
     | 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) }
+    | c = CONSTRUCTOR_IDENT { ConstructorPat(c, UnknownType(Internal))}
+    | c = CONSTRUCTOR_IDENT; TILDE; t = typ;  { CastPat(ConstructorPat(c, UnknownType(Internal)), UnknownType(Internal), t) }
     | p = IDENT { VarPat(p) }
     | i = INT { IntPat i }
     | f = FLOAT { FloatPat f }
@@ -234,7 +236,8 @@ exp:
     | i = INT { Int i }
     | f = FLOAT { Float f }
     | v = IDENT { Var v }
-    | c = CONSTRUCTOR_IDENT; COLON; t = typ { Constructor(c, t) }
+    | c = CONSTRUCTOR_IDENT { Constructor(c, UnknownType(Internal))}
+    | c = CONSTRUCTOR_IDENT; TILDE; t = typ;  { Cast(Constructor(c, UnknownType(Internal)), UnknownType(Internal), t) }
     | s = STRING { String s}
     | OPEN_PAREN; e = exp; CLOSE_PAREN { e } 
     | OPEN_PAREN; e = exp; COMMA; l = separated_list(COMMA, exp); CLOSE_PAREN { TupleExp(e :: l) }

diff --git a/test/Test_Elaboration.re b/test/Test_Elaboration.re
@@ -555,7 +555,7 @@ let f =
       failed_cast_uexp,
     );
 
-  let constructor_str = "X: Unknown Internal";
+  let constructor_str = "X";
   let constructor_uexp: Exp.t =
     Constructor("X", Unknown(Internal) |> Typ.fresh) |> Exp.fresh;
   let constructor_menhir = () =>

diff --git a/test/Test_Menhir.re b/test/Test_Menhir.re
@@ -256,7 +256,17 @@ let tests = [
   menhir_only_test(
     "Constructor",
     Constructor("A", Unknown(Internal) |> Typ.fresh) |> Exp.fresh,
-    "A:Unknown Internal" // This is source incompatible with make_term which does not find the type. We also don't allow expression casts.
+    "A",
+  ),
+  menhir_only_test(
+    "Constructor cast",
+    Cast(
+      Constructor("A", Unknown(Internal) |> Typ.fresh) |> Exp.fresh,
+      Unknown(Internal) |> Typ.fresh,
+      Int |> Typ.fresh,
+    )
+    |> Exp.fresh,
+    "A ~ Int",
   ),
   parser_test(
     "Type Alias",