diff --git a/src/haz3lmenhir/AST.re b/src/haz3lmenhir/AST.re index d1b9b230a..c743afa84 100644 --- 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 index 18c39bdb5..3e5e9faba 100644 --- 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 index ba54cb6c0..7b334fc4e 100644 --- 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 index 67bb0e6de..593793028 100644 --- a/src/haz3lmenhir/Parser.mly +++ b/src/haz3lmenhir/Parser.mly @@ -4,7 +4,7 @@ open AST - +%token NAMED_FUN %token UNDEF %token 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 exp %start 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 index caacbbee3..038ffccc5 100644 --- 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, diff --git a/test/Test_Menhir.re b/test/Test_Menhir.re index 40f4bcabd..0bb114bf5 100644 --- a/test/Test_Menhir.re +++ b/test/Test_Menhir.re @@ -15,24 +15,47 @@ let exp_typ = let alco_check = exp_typ |> Alcotest.check; -let mk_map = Statics.mk(CoreSettings.on, Builtins.ctx_init); -let dhexp_of_uexp = u => Elaborator.elaborate(mk_map(u), u) |> fst; +// Existing recovering parser +let make_term_parse = (s: string) => + MakeTerm.from_zip_for_sem(Option.get(Printer.zipper_of_string(s))).term; -//exp = expected, menhir = test -let parser_test = (name: string, exp: Term.Exp.t, menhir: string, ()) => +let menhir_matches = (name: string, exp: Term.Exp.t, actual: string) => alco_check( - name, + name ++ " matches expected type", exp, - dhexp_of_uexp( - Haz3lmenhir.Conversion.Exp.of_menhir_ast( - Haz3lmenhir.Interface.parse_program(menhir), - ), + Haz3lmenhir.Conversion.Exp.of_menhir_ast( + Haz3lmenhir.Interface.parse_program(actual), ), ); +let menhir_only_test = (name: string, exp: Term.Exp.t, actual: string) => + test_case(name, `Quick, () => {menhir_matches(name, exp, actual)}); + +// TODO Assert against result instead of exception for parse failure for better error messages +let parser_test = (name: string, exp: Term.Exp.t, actual: string) => + test_case( + name, + `Quick, + () => { + alco_check("Does not match MakeTerm", exp, make_term_parse(actual)); + + menhir_matches(name, exp, actual); + }, + ); + +let menhir_maketerm_equivalent_test = (name: string, actual: string) => + test_case(name, `Quick, () => { + alco_check( + "Does not match MakeTerm", + make_term_parse(actual), + Haz3lmenhir.Conversion.Exp.of_menhir_ast( + Haz3lmenhir.Interface.parse_program(actual), + ), + ) + }); + let fun_exp: Exp.t = Fun(Var("x") |> Pat.fresh, Var("x") |> Exp.fresh, None, None) |> Exp.fresh; -let fun_str = "fun x -> x"; //Test for a let function let let_fun_uexp: Exp.t = @@ -77,7 +100,7 @@ let free_var_uexp: Exp.t = { let free_var_test = () => parser_test( "Nonempty hole with free variable (menhir)", - dhexp_of_uexp(free_var_uexp), + free_var_uexp, "y", ); @@ -88,11 +111,7 @@ let bin_op_uexp: Exp.t = let bin_op_str = "1 + 2"; let bin_op_test = () => - parser_test( - "binary integer operation (plus)", - dhexp_of_uexp(bin_op_uexp), - bin_op_str, - ); + parser_test("binary integer operation (plus)", bin_op_uexp, bin_op_str); //Inconsistent branches menhir test let case_menhir_str = " @@ -133,11 +152,7 @@ let ap_fun_str = " (fun x -> 4 + 5)(y) "; let ap_fun_test = () => - parser_test( - "Application of a function (menhir)", - dhexp_of_uexp(ap_fun_uexp), - ap_fun_str, - ); + parser_test("Application of a function (menhir)", ap_fun_uexp, ap_fun_str); //Consistent if statement menhir test let consistent_if_uexp: Exp.t = @@ -150,7 +165,7 @@ let consistent_if_str = " let consistent_if_menhir = () => parser_test( "Consistent case with rules (BoolLit(true), IntLit(8)) and (BoolLit(false), IntLit(6))", - dhexp_of_uexp(consistent_if_uexp), + consistent_if_uexp, consistent_if_str, ); @@ -168,66 +183,184 @@ let single_integer_menhir = () => single_int_str, ); -// //Menhir let expression test -// let let_exp_str = "let (a, b) = (4, 6) in a - b"; -// let let_exp_uexp: Exp.t = -// Let( -// Tuple([Var("a") |> Pat.fresh, Var("b") |> Pat.fresh]) |> Pat.fresh, -// Tuple([Int(4) |> Exp.fresh, Int(6) |> Exp.fresh]) |> Exp.fresh, -// BinOp(Int(Minus), Var("a") |> Exp.fresh, Var("b") |> Exp.fresh) -// |> Exp.fresh, -// ) -// |> Exp.fresh; -// let let_exp_menhir = () => -// alco_check_menhir( -// "Let expression for tuple (a, b) (menhir)", -// let_exp_str, -// let_exp_uexp, -// ); -// -// let typ_ap_str = "(typfun x -> 4) @ "; -// let typ_ap_uexp: Exp.t = -// TypAp( -// TypFun(Var("x") |> TPat.fresh, Int(4) |> Exp.fresh, None) |> Exp.fresh, -// Int |> Typ.fresh, -// ) -// |> Exp.fresh; -// let typ_ap_menhir = () => -// alco_check_menhir("Type ap test (menhir)", typ_ap_str, typ_ap_uexp); -// -// let failed_cast_str = "1 ? String>"; -// let failed_cast_uexp: Exp.t = -// FailedCast(Int(1) |> Exp.fresh, Int |> Typ.fresh, String |> Typ.fresh) -// |> Exp.fresh; -// let failed_cast_menhir = () => -// alco_check_menhir( -// "Failed cast test (menhir)", -// failed_cast_str, -// failed_cast_uexp, -// ); - let tests = [ - test_case( - "Integer Literal", - `Quick, - parser_test("Same Integer", Int(8) |> Exp.fresh, "8"), - ), - test_case("Fun", `Quick, parser_test("Fun", fun_exp, fun_str)), - test_case( + parser_test("Integer Literal", Int(8) |> Exp.fresh, "8"), + parser_test("Fun", fun_exp, "fun x -> x"), + parser_test( "String Literal", - `Quick, - parser_test( - "Same String", - String("Hello World") |> Exp.fresh, - "\"Hello World\"", - ), + String("Hello World") |> Exp.fresh, + "\"Hello World\"", ), - //NOTE: leaving out deferrals for now due to bug - // test_case( - // "Deferred Ap", - // `Quick, - // parser_test("Deferred Ap", , "x(_)"), + parser_test("Bool Literal", Bool(true) |> Exp.fresh, "true"), + parser_test("Empty Hole", EmptyHole |> Exp.fresh, "?"), + parser_test("Var", Var("x") |> Exp.fresh, "x"), + parser_test("Parens", Parens(Var("y") |> Exp.fresh) |> Exp.fresh, "(y)"), + parser_test( + "BinOp", + BinOp(Int(Plus), Int(4) |> Exp.fresh, Int(5) |> Exp.fresh) |> Exp.fresh, + "4 + 5", + ), + parser_test( + "Let", + Let(Var("x") |> Pat.fresh, Int(5) |> Exp.fresh, Var("x") |> Exp.fresh) + |> Exp.fresh, + "let x = 5 in x", + ), + parser_test( + "Tuple", + Tuple([Int(4) |> Exp.fresh, Int(5) |> Exp.fresh]) |> Exp.fresh, + "(4, 5)" // TODO Verify with maketerm. Should this be parens or not + ), + parser_test( + "Match", + Match( + Int(4) |> Exp.fresh, + [ + (Int(1) |> Pat.fresh, String("hello") |> Exp.fresh), + (Wild |> Pat.fresh, String("world") |> Exp.fresh), + ], + ) + |> Exp.fresh, + {|case 4 + | 1 => "hello" + | _ => "world" + end|}, + ), + parser_test( + "If", + If(Bool(true) |> Exp.fresh, Int(8) |> Exp.fresh, Int(6) |> Exp.fresh) + |> Exp.fresh, + "if true then 8 else 6", + ), + parser_test( + "Deferred Ap", + DeferredAp(Var("x") |> Exp.fresh, [Deferral(InAp) |> Exp.fresh]) + |> Exp.fresh, + "x(_)", + ), + parser_test( + "Cons", + Cons(Int(1) |> Exp.fresh, ListLit([]) |> Exp.fresh) |> Exp.fresh, + "1 :: []", + ), + parser_test( + "ListLit", + ListLit([ + Int(1) |> Exp.fresh, + Int(2) |> Exp.fresh, + Int(3) |> Exp.fresh, + ]) + |> Exp.fresh, + "[1, 2, 3]", + ), + 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. + ), + parser_test( + "Type Alias", + TyAlias(Var("x") |> TPat.fresh, Int |> Typ.fresh, Int(1) |> Exp.fresh) + |> Exp.fresh, + "type x = Int in 1", + ), + parser_test( + "Test", + Test( + BinOp(Int(Equals), Int(3) |> Exp.fresh, Int(3) |> Exp.fresh) + |> Exp.fresh, + ) + |> Exp.fresh, + "test 3 == 3 end", + ), + parser_test( + "Filter", + Filter( + Filter({act: (Eval, All), pat: Int(3) |> Exp.fresh}), + Int(3) |> Exp.fresh, + ) + |> Exp.fresh, + "eval 3 in 3" // TODO Use other filter commands + ), + parser_test( + "List Concat", + ListConcat( + ListLit([Int(1) |> Exp.fresh, Int(2) |> Exp.fresh]) |> Exp.fresh, + ListLit([Int(3) |> Exp.fresh, Int(4) |> Exp.fresh]) |> Exp.fresh, + ) + |> Exp.fresh, + "[1, 2] @ [3, 4]", + ), + // parser_test( + // "Integer Ops", + // BinOp( + // Int(GreaterThanOrEqual), + // BinOp( + // Int(Minus), + // BinOp( + // Int(Plus), + // UnOp(Int(Minus), Int(1) |> Exp.fresh) |> Exp.fresh, + // Int(2) |> Exp.fresh, + // ) + // |> Exp.fresh, + // BinOp( + // Int(Divide), + // Int(3) |> Exp.fresh, + // BinOp( + // Int(Times), + // Int(4) |> Exp.fresh, + // BinOp(Int(Power), Int(5) |> Exp.fresh, Int(6) |> Exp.fresh) + // |> Exp.fresh, + // ) + // |> Exp.fresh, + // ) + // |> Exp.fresh, + // ) + // |> Exp.fresh, + // Int(8) |> Exp.fresh, + // ) + // |> Exp.fresh, + // "-1 + 2 - 3 / 4 * 5 ** 6 >= 8" // TODO Add the remaining operators. < is also currently broken // ), - test_case("Ap Fun", `Quick, ap_fun_test()), - test_case("Single integer", `Quick, single_integer_menhir()), + parser_test( + "Let binding with type ascription", + Let( + Cast( + Var("x") |> Pat.fresh, + Int |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Pat.fresh, + Int(5) |> Exp.fresh, + Var("x") |> Exp.fresh, + ) + |> Exp.fresh, + "let (x: Int) = 5 in x", + ), + menhir_only_test( + "named_function", + Fun( + Pat.Var("x") |> Pat.fresh, + BinOp(Int(Plus), Var("x") |> Exp.fresh, Int(5) |> Exp.fresh) + |> Exp.fresh, + None, + Some("f"), + ) + |> Exp.fresh, + "named_fun f x -> x + 5", + ), + // { + // let strip_comments = str => { + // let re = Str.regexp("#[^#]*#"); + // Str.global_replace(re, "", str); + // }; + // let basic_reference = + // Haz3lweb.Init.startup.documentation + // |> (((_, slides, _)) => slides) + // |> List.assoc("Basic Reference") + // |> (slide => strip_comments(slide.backup_text)); + // print_endline(basic_reference); + // + // menhir_maketerm_equivalent_test("Basic Reference", basic_reference); + // }, ]; diff --git a/test/dune b/test/dune index 38823aef0..3097b7985 100644 --- a/test/dune +++ b/test/dune @@ -4,6 +4,7 @@ (name haz3ltest) (libraries haz3lcore + haz3lweb alcotest sexplib base