diff --git a/test/Test_ana_action.re b/test/Test_ana_action.re index 4872e8a..e8c9583 100644 --- a/test/Test_ana_action.re +++ b/test/Test_ana_action.re @@ -208,5 +208,5 @@ let ana_action_tests = [ ("test_aaconnumlit_1", `Quick, test_aaconnumlit_1), ("test_aaconnumlit_2", `Quick, test_aaconnumlit_2), ("test_aafinish_1", `Quick, test_aafinish_1), - //("test_aafinish_2", `Quick, test_aafinish_2), + ("test_aafinish_2", `Quick, test_aafinish_2), ]; diff --git a/test/Test_sample1.re b/test/Test_sample1.re index 9e8fc5d..fefd48c 100644 --- a/test/Test_sample1.re +++ b/test/Test_sample1.re @@ -5,7 +5,7 @@ module Hazelnut = Hazelnut_lib.Hazelnut; module TypCtx = Map.Make(String); type typctx = Hazelnut.TypCtx.t(Hazelnut.Htyp.t); -let test_st1 = () => { +let test_syn_step_1 = () => { let ctx: typctx = TypCtx.empty; let ze: Hazelnut.Zexp.t = Cursor(EHole); let t: Hazelnut.Htyp.t = Hole; @@ -20,7 +20,7 @@ let test_st1 = () => { check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); }; -let test_ast1 = () => { +let test_ana_step_1 = () => { let ctx: typctx = TypCtx.empty; let ze: Hazelnut.Zexp.t = Cursor(EHole); let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Lam("x")); @@ -30,7 +30,7 @@ let test_ast1 = () => { check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); }; -let test_st2 = () => { +let test_syn_step_2 = () => { let ctx: typctx = TypCtx.empty; let ze: Hazelnut.Zexp.t = RAsc(Lam("x", EHole), LArrow(Cursor(Hole), Hole)); @@ -46,7 +46,7 @@ let test_st2 = () => { check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); }; -let test_ast2 = () => { +let test_ana_step_2 = () => { let ctx: typctx = TypCtx.empty; let ze: Hazelnut.Zexp.t = RAsc(Lam("x", EHole), LArrow(Cursor(Hole), Hole)); @@ -58,7 +58,7 @@ let test_ast2 = () => { check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); }; -let test_st3 = () => { +let test_syn_step_3 = () => { let ctx: typctx = TypCtx.empty; let ze: Hazelnut.Zexp.t = RAsc(Lam("x", EHole), LArrow(Cursor(Num), Hole)); @@ -74,7 +74,7 @@ let test_st3 = () => { check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); }; -let test_ast3 = () => { +let test_ana_step_3 = () => { let ctx: typctx = TypCtx.empty; let ze: Hazelnut.Zexp.t = RAsc(Lam("x", EHole), LArrow(Cursor(Num), Hole)); @@ -86,7 +86,7 @@ let test_ast3 = () => { check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); }; -let test_st4 = () => { +let test_syn_step_4 = () => { let ctx: typctx = TypCtx.empty; let ze: Hazelnut.Zexp.t = RAsc(Lam("x", EHole), Cursor(Arrow(Num, Hole))); @@ -102,7 +102,7 @@ let test_st4 = () => { check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); }; -let test_ast4 = () => { +let test_ana_step_4 = () => { let ctx: typctx = TypCtx.empty; let ze: Hazelnut.Zexp.t = RAsc(Lam("x", EHole), Cursor(Arrow(Num, Hole))); @@ -114,7 +114,7 @@ let test_ast4 = () => { check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); }; -let test_st5 = () => { +let test_syn_step_5 = () => { let ctx: typctx = TypCtx.empty; let ze: Hazelnut.Zexp.t = RAsc(Lam("x", EHole), RArrow(Num, Cursor(Hole))); @@ -130,7 +130,7 @@ let test_st5 = () => { check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); }; -let test_ast5 = () => { +let test_ana_step_5 = () => { let ctx: typctx = TypCtx.empty; let ze: Hazelnut.Zexp.t = RAsc(Lam("x", EHole), RArrow(Num, Cursor(Hole))); @@ -142,7 +142,7 @@ let test_ast5 = () => { check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); }; -let test_st6 = () => { +let test_syn_step_6 = () => { let ctx: typctx = TypCtx.empty; let ze: Hazelnut.Zexp.t = RAsc(Lam("x", EHole), RArrow(Num, Cursor(Num))); @@ -158,7 +158,7 @@ let test_st6 = () => { check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); }; -let test_ast6 = () => { +let test_ana_step_6 = () => { let ctx: typctx = TypCtx.empty; let ze: Hazelnut.Zexp.t = RAsc(Lam("x", EHole), RArrow(Num, Cursor(Num))); @@ -170,7 +170,7 @@ let test_ast6 = () => { check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); }; -let test_st7 = () => { +let test_syn_step_7 = () => { let ctx: typctx = TypCtx.empty; let ze: Hazelnut.Zexp.t = RAsc(Lam("x", EHole), Cursor(Arrow(Num, Num))); let t: Hazelnut.Htyp.t = Arrow(Num, Num); @@ -185,7 +185,7 @@ let test_st7 = () => { check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); }; -let test_ast7 = () => { +let test_ana_step_7 = () => { let ctx: typctx = TypCtx.empty; let ze: Hazelnut.Zexp.t = RAsc(Lam("x", EHole), Cursor(Arrow(Num, Num))); let a: Hazelnut.Action.t = Move(Parent); @@ -196,7 +196,7 @@ let test_ast7 = () => { check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); }; -let test_st8 = () => { +let test_syn_step_8 = () => { let ctx: typctx = TypCtx.empty; let ze: Hazelnut.Zexp.t = Cursor(Asc(Lam("x", EHole), Arrow(Num, Num))); let t: Hazelnut.Htyp.t = Arrow(Num, Num); @@ -211,7 +211,7 @@ let test_st8 = () => { check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); }; -let test_ast8 = () => { +let test_ana_step_8 = () => { let ctx: typctx = TypCtx.empty; let ze: Hazelnut.Zexp.t = Cursor(Asc(Lam("x", EHole), Arrow(Num, Num))); let a: Hazelnut.Action.t = Move(Child(One)); @@ -222,7 +222,7 @@ let test_ast8 = () => { check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); }; -let test_st9 = () => { +let test_syn_step_9 = () => { let ctx: typctx = TypCtx.empty; let ze: Hazelnut.Zexp.t = LAsc(Cursor(Lam("x", EHole)), Arrow(Num, Num)); let t: Hazelnut.Htyp.t = Arrow(Num, Num); @@ -237,7 +237,7 @@ let test_st9 = () => { check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); }; -let test_ast9 = () => { +let test_ana_step_9 = () => { let ctx: typctx = TypCtx.empty; let ze: Hazelnut.Zexp.t = LAsc(Cursor(Lam("x", EHole)), Arrow(Num, Num)); let a: Hazelnut.Action.t = Move(Child(One)); @@ -248,7 +248,7 @@ let test_ast9 = () => { check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); }; -let test_st10 = () => { +let test_syn_step_10 = () => { let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Num); let ze: Hazelnut.Zexp.t = LAsc(Lam("x", Cursor(EHole)), Arrow(Num, Num)); let t: Hazelnut.Htyp.t = Arrow(Num, Num); @@ -263,7 +263,7 @@ let test_st10 = () => { check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); }; -let test_ast10 = () => { +let test_ana_step_10 = () => { let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Num); let ze: Hazelnut.Zexp.t = LAsc(Lam("x", Cursor(EHole)), Arrow(Num, Num)); let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Var("x")); @@ -274,7 +274,7 @@ let test_ast10 = () => { check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); }; -let test_st11 = () => { +let test_syn_step_11 = () => { let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Num); let ze: Hazelnut.Zexp.t = LAsc(Lam("x", Cursor(Var("x"))), Arrow(Num, Num)); @@ -290,7 +290,7 @@ let test_st11 = () => { check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); }; -let test_ast11 = () => { +let test_ana_step_11 = () => { let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Num); let ze: Hazelnut.Zexp.t = LAsc(Lam("x", Cursor(Var("x"))), Arrow(Num, Num)); @@ -304,7 +304,7 @@ let test_ast11 = () => { check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); }; -let test_st12 = () => { +let test_syn_step_12 = () => { let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Num); let ze: Hazelnut.Zexp.t = LAsc(Lam("x", RPlus(Var("x"), Cursor(EHole))), Arrow(Num, Num)); @@ -320,7 +320,7 @@ let test_st12 = () => { check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); }; -let test_ast12 = () => { +let test_ana_step_12 = () => { let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Num); let ze: Hazelnut.Zexp.t = LAsc(Lam("x", RPlus(Var("x"), Cursor(EHole))), Arrow(Num, Num)); @@ -335,28 +335,28 @@ let test_ast12 = () => { }; let sample1_tests = [ - ("test_st1", `Quick, test_st1), - ("test_ast1", `Quick, test_ast1), - ("test_st2", `Quick, test_st2), - ("test_ast2", `Quick, test_ast2), - ("test_st3", `Quick, test_st3), - ("test_ast3", `Quick, test_ast3), - ("test_st4", `Quick, test_st4), - ("test_ast4", `Quick, test_ast4), - ("test_st5", `Quick, test_st5), - ("test_ast5", `Quick, test_ast5), - ("test_st6", `Quick, test_st6), - ("test_ast6", `Quick, test_ast6), - ("test_st7", `Quick, test_st7), - ("test_ast7", `Quick, test_ast7), - ("test_st8", `Quick, test_st8), - ("test_ast8", `Quick, test_ast8), - ("test_st9", `Quick, test_st9), - ("test_ast9", `Quick, test_ast9), - ("test_st10", `Quick, test_st10), - ("test_ast10", `Quick, test_ast10), - ("test_st11", `Quick, test_st11), - ("test_ast11", `Quick, test_ast11), - ("test_st12", `Quick, test_st12), - ("test_ast12", `Quick, test_st12), + ("test_syn_step_1", `Quick, test_syn_step_1), + ("test_ana_step_1", `Quick, test_ana_step_1), + ("test_syn_step_2", `Quick, test_syn_step_2), + ("test_ana_step_2", `Quick, test_ana_step_2), + ("test_syn_step_3", `Quick, test_syn_step_3), + ("test_ana_step_3", `Quick, test_ana_step_3), + ("test_syn_step_4", `Quick, test_syn_step_4), + ("test_ana_step_4", `Quick, test_ana_step_4), + ("test_syn_step_5", `Quick, test_syn_step_5), + ("test_ana_step_5", `Quick, test_ana_step_5), + ("test_syn_step_6", `Quick, test_syn_step_6), + ("test_ana_step_6", `Quick, test_ana_step_6), + ("test_syn_step_7", `Quick, test_syn_step_7), + ("test_ana_step_7", `Quick, test_ana_step_7), + ("test_syn_step_8", `Quick, test_syn_step_8), + ("test_ana_step_8", `Quick, test_ana_step_8), + ("test_syn_step_9", `Quick, test_syn_step_9), + ("test_ana_step_9", `Quick, test_ana_step_9), + ("test_syn_step_10", `Quick, test_syn_step_10), + ("test_ana_step_10", `Quick, test_ana_step_10), + ("test_syn_step_11", `Quick, test_syn_step_11), + ("test_ana_step_11", `Quick, test_ana_step_11), + ("test_syn_step_12", `Quick, test_syn_step_12), + ("test_ana_step_12", `Quick, test_ana_step_12), ]; diff --git a/test/Test_sample2.re b/test/Test_sample2.re index aa1679c..4b87fe1 100644 --- a/test/Test_sample2.re +++ b/test/Test_sample2.re @@ -215,20 +215,20 @@ let test_ast21 = () => { }; let sample2_tests = [ - ("test_st14", `Quick, test_st14), - ("test_ast14", `Quick, test_ast14), - ("test_st15", `Quick, test_st15), - ("test_ast15", `Quick, test_ast15), - ("test_st16", `Quick, test_st16), - ("test_ast16", `Quick, test_ast16), - ("test_st17", `Quick, test_st17), - ("test_ast17", `Quick, test_ast17), - ("test_st18", `Quick, test_st18), - ("test_ast18", `Quick, test_ast18), - ("test_st19", `Quick, test_st19), - ("test_ast19", `Quick, test_ast19), - ("test_st20", `Quick, test_st20), - ("test_ast20", `Quick, test_ast20), - ("test_st21", `Quick, test_st21), - ("test_ast21", `Quick, test_ast21), + ("test_syn_step_14", `Quick, test_st14), + ("test_ana_step_14", `Quick, test_ast14), + ("test_syn_step_15", `Quick, test_st15), + ("test_ana_step_15", `Quick, test_ast15), + ("test_syn_step_16", `Quick, test_st16), + ("test_ana_step_16", `Quick, test_ast16), + ("test_syn_step_17", `Quick, test_st17), + ("test_ana_step_17", `Quick, test_ast17), + ("test_syn_step_18", `Quick, test_st18), + ("test_ana_step_18", `Quick, test_ast18), + ("test_syn_step_19", `Quick, test_st19), + ("test_ana_step_19", `Quick, test_ast19), + ("test_syn_step_20", `Quick, test_st20), + ("test_ana_step_20", `Quick, test_ast20), + ("test_syn_step_21", `Quick, test_st21), + ("test_ana_step_21", `Quick, test_ast21), ]; diff --git a/test/Test_syn_action.re b/test/Test_syn_action.re index 9d528c0..1d2b85f 100644 --- a/test/Test_syn_action.re +++ b/test/Test_syn_action.re @@ -4,7 +4,52 @@ module Hazelnut = Hazelnut_lib.Hazelnut; module TypCtx = Map.Make(String); type typctx = Hazelnut.TypCtx.t(Hazelnut.Htyp.t); -let test_samove_1 = () => { +// MOVE TESTS BEGIN +let test_samove_asc1 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = Cursor(Asc(Lit(1), Num)); + let t: Hazelnut.Htyp.t = Num; + let a: Hazelnut.Action.t = Move(Child(One)); + let given: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Hazelnut.syn_action(ctx, (ze, t), a); + let expected: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Some((LAsc(Cursor(Lit(1)), Num),Num)); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_samove_asc2 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = Cursor(Asc(Lit(1), Num)); + let t: Hazelnut.Htyp.t = Num; + let a: Hazelnut.Action.t = Move(Child(Two)); + let given: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Hazelnut.syn_action(ctx, (ze, t), a); + let expected: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Some((RAsc(Lit(1), Cursor(Num)),Num)); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_samove_asc3 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = LAsc(Cursor(Lit(1)), Num); + let t: Hazelnut.Htyp.t = Num; + let a: Hazelnut.Action.t = Move(Parent); + let given: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Hazelnut.syn_action(ctx, (ze, t), a); + let expected: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Some((Cursor(Asc(Lit(1), Num)), Num)); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_samove_asc4 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = RAsc(Lit(1), Cursor(Num)); + let t: Hazelnut.Htyp.t = Num; + let a: Hazelnut.Action.t = Move(Parent); + let given: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Hazelnut.syn_action(ctx, (ze, t), a); + let expected: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Some((Cursor(Asc(Lit(1), Num)), Num)); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_samove_lam1 = () => { let ctx: typctx = TypCtx.empty; let ze: Hazelnut.Zexp.t = LAsc(Cursor(Lam("x", EHole)), Arrow(Hole, Hole)); @@ -19,6 +64,174 @@ let test_samove_1 = () => { )); check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); }; +let test_samove_lam2 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = + LAsc(Lam("x", Cursor(EHole)), Arrow(Hole, Hole)); + let t: Hazelnut.Htyp.t = Arrow(Hole, Hole); + let a: Hazelnut.Action.t = Move(Parent); + let given: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Hazelnut.syn_action(ctx, (ze, t), a); + let expected: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Some(( + LAsc(Cursor(Lam("x", EHole)), Arrow(Hole, Hole)), + Arrow(Hole, Hole), + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_samove_plus1 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = + Cursor(Plus(Lit(1),Lit(2))); + let t: Hazelnut.Htyp.t = Num; + let a: Hazelnut.Action.t = Move(Child(One)); + let given: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Hazelnut.syn_action(ctx, (ze, t), a); + let expected: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Some(( + LPlus(Cursor(Lit(1)), Lit(2)), + Num, + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_samove_plus2 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = + Cursor(Plus(Lit(1),Lit(2))); + let t: Hazelnut.Htyp.t = Num; + let a: Hazelnut.Action.t = Move(Child(Two)); + let given: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Hazelnut.syn_action(ctx, (ze, t), a); + let expected: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Some(( + RPlus(Lit(1), Cursor(Lit(2))), + Num, + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_samove_plus3 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = + LPlus(Cursor(Lit(1)), Lit(2)); + let t: Hazelnut.Htyp.t = Num; + let a: Hazelnut.Action.t = Move(Parent); + let given: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Hazelnut.syn_action(ctx, (ze, t), a); + let expected: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Some(( + Cursor(Plus(Lit(1),Lit(2))), + Num, + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_samove_plus4 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = + RPlus(Lit(1), Cursor(Lit(2))); + let t: Hazelnut.Htyp.t = Num; + let a: Hazelnut.Action.t = Move(Parent); + let given: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Hazelnut.syn_action(ctx, (ze, t), a); + let expected: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Some(( + Cursor(Plus(Lit(1),Lit(2))), + Num, + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_samove_ap1 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = + Cursor(Ap(Lam("x", EHole), EHole)); + let t: Hazelnut.Htyp.t = Hole; + let a: Hazelnut.Action.t = Move(Child(One)); + let given: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Hazelnut.syn_action(ctx, (ze, t), a); + let expected: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Some(( + LAp(Cursor(Lam("x", EHole)), EHole), + Hole, + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_samove_ap2 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = + Cursor(Ap(Lam("x", EHole), EHole)); + let t: Hazelnut.Htyp.t = Hole; + let a: Hazelnut.Action.t = Move(Child(Two)); + let given: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Hazelnut.syn_action(ctx, (ze, t), a); + let expected: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Some(( + RAp(Lam("x", EHole), Cursor(EHole)), + Hole, + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_samove_ap3 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = + LAp(Cursor(Lam("x", EHole)), EHole); + let t: Hazelnut.Htyp.t = Hole; + let a: Hazelnut.Action.t = Move(Parent); + let given: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Hazelnut.syn_action(ctx, (ze, t), a); + let expected: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Some(( + Cursor(Ap(Lam("x", EHole), EHole)), + Hole, + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_samove_ap4 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = + RAp(Lam("x", EHole), Cursor(EHole)); + let t: Hazelnut.Htyp.t = Hole; + let a: Hazelnut.Action.t = Move(Parent); + let given: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Hazelnut.syn_action(ctx, (ze, t), a); + let expected: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Some(( + Cursor(Ap(Lam("x", EHole), EHole)), + Hole, + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_samove_neh1 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = + Cursor(NEHole(Lit(1))); + let t: Hazelnut.Htyp.t = Hole; + let a: Hazelnut.Action.t = Move(Child(One)); + let given: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Hazelnut.syn_action(ctx, (ze, t), a); + let expected: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Some(( + NEHole(Cursor(Lit(1))), + Hole, + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_samove_neh2 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = + NEHole(Cursor(Lit(1))); + let t: Hazelnut.Htyp.t = Hole; + let a: Hazelnut.Action.t = Move(Parent); + let given: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Hazelnut.syn_action(ctx, (ze, t), a); + let expected: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Some(( + (Cursor(NEHole(Lit(1)))), + Hole, + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +// MOVE TESTS COMPLETE + + let test_sadel_1 = () => { let ctx: typctx = TypCtx.empty; let ze: Hazelnut.Zexp.t = Cursor(Lit(1)); @@ -258,7 +471,22 @@ let test_safinish_2 = () => { check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); }; let syn_action_tests = [ - ("test_samove_1", `Quick, test_sadel_1), + ("test_samove_asc1", `Quick, test_samove_asc1), + ("test_samove_asc2", `Quick, test_samove_asc2), + ("test_samove_asc3", `Quick, test_samove_asc3), + ("test_samove_asc4", `Quick, test_samove_asc4), + ("test_samove_lam1", `Quick, test_samove_lam1), + ("test_samove_lam2", `Quick, test_samove_lam2), + ("test_samove_plus1", `Quick, test_samove_plus1), + ("test_samove_plus2", `Quick, test_samove_plus2), + ("test_samove_plus3", `Quick, test_samove_plus3), + ("test_samove_plus4", `Quick, test_samove_plus4), + ("test_samove_ap1", `Quick, test_samove_ap1), + ("test_samove_ap2", `Quick, test_samove_ap2), + ("test_samove_ap3", `Quick, test_samove_ap3), + ("test_samove_ap4", `Quick, test_samove_ap4), + ("test_samove_neh1", `Quick, test_samove_neh1), + ("test_samove_neh2", `Quick, test_samove_neh2), ("test_sadel_1", `Quick, test_sadel_1), ("test_sadel_2", `Quick, test_sadel_2), ("test_safinish_1", `Quick, test_safinish_1), diff --git a/test/Test_type_action.re b/test/Test_type_action.re new file mode 100644 index 0000000..7286b6b --- /dev/null +++ b/test/Test_type_action.re @@ -0,0 +1,94 @@ +open Alcotest; +open Test_interface; +module Hazelnut = Hazelnut_lib.Hazelnut; + +module TypCtx = Map.Make(String); +type typctx = Hazelnut.TypCtx.t(Hazelnut.Htyp.t); + +let test_type_move1 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = RAsc(Lam("x", EHole), Cursor(Arrow(Hole, Hole))); + let t: Hazelnut.Htyp.t = Arrow(Hole,Hole); + let a: Hazelnut.Action.t = Move(Child(One)); + let given: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Hazelnut.syn_action(ctx, (ze, t), a); + let expected: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Some((RAsc(Lam("x", EHole), LArrow(Cursor(Hole), Hole)), Arrow(Hole,Hole))); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_type_move2 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = RAsc(Lam("x", EHole), Cursor(Arrow(Hole, Hole))); + let t: Hazelnut.Htyp.t = Arrow(Hole,Hole); + let a: Hazelnut.Action.t = Move(Child(Two)); + let given: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Hazelnut.syn_action(ctx, (ze, t), a); + let expected: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Some((RAsc(Lam("x", EHole), RArrow(Hole, Cursor(Hole))), Arrow(Hole,Hole))); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_type_move3 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = RAsc(Lam("x", EHole), RArrow(Hole, Cursor(Hole))); + let t: Hazelnut.Htyp.t = Arrow(Hole,Hole); + let a: Hazelnut.Action.t = Move(Parent); + let given: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Hazelnut.syn_action(ctx, (ze, t), a); + let expected: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Some((RAsc(Lam("x", EHole), Cursor(Arrow(Hole, Hole))), Arrow(Hole,Hole))); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_type_move4 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = RAsc(Lam("x", EHole), LArrow(Cursor(Hole), Hole)); + let t: Hazelnut.Htyp.t = Arrow(Hole,Hole); + let a: Hazelnut.Action.t = Move(Parent); + let given: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Hazelnut.syn_action(ctx, (ze, t), a); + let expected: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Some((RAsc(Lam("x", EHole), Cursor(Arrow(Hole, Hole))), Arrow(Hole,Hole))); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_type_del = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = RAsc(Lit(1), Cursor(Num)); + let t: Hazelnut.Htyp.t = Num; + let a: Hazelnut.Action.t = Del; + let given: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Hazelnut.syn_action(ctx, (ze, t), a); + let expected: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Some((RAsc(Lit(1), Cursor(Hole)), Hole)); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_type_conarr = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = RAsc(Lit(1), Cursor(Num)); + let t: Hazelnut.Htyp.t = Num; + let a: Hazelnut.Action.t = Construct(Arrow); + let given: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Hazelnut.syn_action(ctx, (ze, t), a); + let expected: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Some((RAsc(Lit(1), RArrow(Num,Cursor(Hole))), Arrow(Num,Hole))); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_type_connum = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = RAsc(Lit(1), Cursor(Hole)); + let t: Hazelnut.Htyp.t = Hole; + let a: Hazelnut.Action.t = Construct(Num); + let given: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Hazelnut.syn_action(ctx, (ze, t), a); + let expected: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)) = + Some((RAsc(Lit(1), Cursor(Num)), Num)); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; + +let type_action_tests = [ + ("test_type_move1", `Quick, test_type_move1), + ("test_type_move2", `Quick, test_type_move2), + ("test_type_move3", `Quick, test_type_move3), + ("test_type_move4", `Quick, test_type_move4), + ("test_type_del", `Quick, test_type_del), + ("test_type_conarr", `Quick, test_type_conarr), + ("test_type_connum", `Quick, test_type_connum), +]; diff --git a/test/hazelnut_test.re b/test/hazelnut_test.re index f88d4f1..1edc33f 100644 --- a/test/hazelnut_test.re +++ b/test/hazelnut_test.re @@ -11,5 +11,6 @@ let () = ("syn_action", Test_syn_action.syn_action_tests), ("sample 1", Test_sample1.sample1_tests), ("sample 2", Test_sample2.sample2_tests), + ("type_action", Test_type_action.type_action_tests), ], );