diff --git a/.gitignore b/.gitignore index e35d885..ea46c2f 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,4 @@ -_build +/_build/ + +.DS_Store +node_modules/ diff --git a/Makefile b/Makefile index c30b2a1..b65e599 100644 --- a/Makefile +++ b/Makefile @@ -17,7 +17,7 @@ clean: dune clean deps: - opam install dune reason incr_dom ocaml-lsp-server + opam install dune reason incr_dom ocaml-lsp-server ppx_deriving .PHONY: test test: diff --git a/hazelnut/dune b/hazelnut/dune index 98e0ea8..dda838e 100644 --- a/hazelnut/dune +++ b/hazelnut/dune @@ -2,4 +2,4 @@ (name hazelnut_lib) (libraries core incr_dom monad_lib) (preprocess - (pps ppx_jane))) + (pps ppx_jane ppx_deriving.show))) diff --git a/hazelnut/hazelnut.re b/hazelnut/hazelnut.re index 3113d9f..2eb4ce9 100644 --- a/hazelnut/hazelnut.re +++ b/hazelnut/hazelnut.re @@ -5,7 +5,7 @@ let compare_string = String.compare; let compare_int = Int.compare; module Htyp = { - [@deriving (sexp, compare)] + [@deriving (sexp, compare, show({with_path: false}))] type t = | Arrow(t, t) | Num @@ -13,7 +13,7 @@ module Htyp = { }; module Hexp = { - [@deriving (sexp, compare)] + [@deriving (sexp, compare, show({with_path: false}))] type t = | Var(string) | Lam(string, t) @@ -26,7 +26,7 @@ module Hexp = { }; module Ztyp = { - [@deriving (sexp, compare)] + [@deriving (sexp, compare, show({with_path: false}))] type t = | Cursor(Htyp.t) | LArrow(t, Htyp.t) @@ -34,7 +34,7 @@ module Ztyp = { }; module Zexp = { - [@deriving (sexp, compare)] + [@deriving (sexp, compare, show({with_path: false}))] type t = | Cursor(Hexp.t) | Lam(string, t) diff --git a/hazelnut/hazelnut.rei b/hazelnut/hazelnut.rei index f74011d..b12f8bd 100644 --- a/hazelnut/hazelnut.rei +++ b/hazelnut/hazelnut.rei @@ -1,5 +1,5 @@ module Htyp: { - [@deriving (sexp, compare)] + [@deriving (sexp, compare, show({with_path: false}))] type t = | Arrow(t, t) | Num @@ -7,7 +7,7 @@ module Htyp: { }; module Hexp: { - [@deriving (sexp, compare)] + [@deriving (sexp, compare, show({with_path: false}))] type t = | Var(string) | Lam(string, t) @@ -20,7 +20,7 @@ module Hexp: { }; module Ztyp: { - [@deriving (sexp, compare)] + [@deriving (sexp, compare, show({with_path: false}))] type t = | Cursor(Htyp.t) | LArrow(t, Htyp.t) @@ -28,7 +28,7 @@ module Ztyp: { }; module Zexp: { - [@deriving (sexp, compare)] + [@deriving (sexp, compare, show({with_path: false}))] type t = | Cursor(Hexp.t) | Lam(string, t) diff --git a/test/Test_ana.re b/test/Test_ana.re new file mode 100644 index 0000000..d12c1dd --- /dev/null +++ b/test/Test_ana.re @@ -0,0 +1,68 @@ +open Alcotest; +module Hazelnut = Hazelnut_lib.Hazelnut; + +module TypCtx = Map.Make(String); +type typctx = Hazelnut.TypCtx.t(Hazelnut.Htyp.t); + +let test_asubsume_1 = () => { + let ctx: typctx = TypCtx.empty; + let he: Hazelnut.Hexp.t = Lit(1); + let ht: Hazelnut.Htyp.t = Arrow(Num, Num); + let given: bool = Hazelnut.ana(ctx, he, ht); + let expected: bool = false; + check(bool, "same bool", given, expected); +}; + +let test_asubsume_2 = () => { + let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Num); + let he: Hazelnut.Hexp.t = Var("x"); + let ht: Hazelnut.Htyp.t = Num; + let given: bool = Hazelnut.ana(ctx, he, ht); + let expected: bool = true; + check(bool, "same bool", given, expected); +}; + +let test_asubsume_3 = () => { + let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Arrow(Num, Num)); + let he: Hazelnut.Hexp.t = Var("x"); + let ht: Hazelnut.Htyp.t = Hole; + let given: bool = Hazelnut.ana(ctx, he, ht); + let expected: bool = true; + check(bool, "same bool", given, expected); +}; + +let test_alam_1 = () => { + let ctx: typctx = TypCtx.empty; + let he: Hazelnut.Hexp.t = Lam("x", Plus(Lit(1), Lit(2))); + let ht: Hazelnut.Htyp.t = Arrow(Arrow(Num, Num), Num); + let given: bool = Hazelnut.ana(ctx, he, ht); + let expected: bool = true; + check(bool, "same bool", given, expected); +}; + +let test_alam_2 = () => { + let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Num); + let he: Hazelnut.Hexp.t = Lam("f", Plus(Var("x"), Lit(2))); + let ht: Hazelnut.Htyp.t = Arrow(Num, Num); + let given: bool = Hazelnut.ana(ctx, he, ht); + let expected: bool = true; + check(bool, "same bool", given, expected); +}; + +let test_alam_3 = () => { + let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Arrow(Num, Num)); + let he: Hazelnut.Hexp.t = Lam("f", Plus(Var("x"), Lit(2))); + let ht: Hazelnut.Htyp.t = Arrow(Num, Num); + let given: bool = Hazelnut.ana(ctx, he, ht); + let expected: bool = false; + check(bool, "same bool", given, expected); +}; + +let ana_tests = [ + ("test_asubsume_1", `Quick, test_asubsume_1), + ("test_asubsume_2", `Quick, test_asubsume_2), + ("test_asubsume_3", `Quick, test_asubsume_3), + ("test_alam_1", `Quick, test_alam_1), + ("test_alam_2", `Quick, test_alam_2), + ("test_alam_3", `Quick, test_alam_3), +]; diff --git a/test/Test_ana_action.re b/test/Test_ana_action.re new file mode 100644 index 0000000..e8c9583 --- /dev/null +++ b/test/Test_ana_action.re @@ -0,0 +1,212 @@ +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_aamove_1 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = Cursor(Lam("f", Plus(Lit(1), Lit(2)))); + let a: Hazelnut.Action.t = Move(Child(One)); + let ht: Hazelnut.Htyp.t = Num; + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some(Lam("f", Cursor(Plus(Lit(1), Lit(2))))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_aamove_2 = () => { + let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Num); + let ze: Hazelnut.Zexp.t = Cursor(Ap(Lam("f", Lit(1)), Var("x"))); + let a: Hazelnut.Action.t = Move(Child(Two)); + let ht: Hazelnut.Htyp.t = Num; + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some(RAp(Lam("f", Lit(1)), Cursor(Var("x")))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_aamove_3 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = + RAsc(Lam("f", Lit(1)), Cursor(Arrow(Num, Num))); + let a: Hazelnut.Action.t = Move(Parent); + let ht: Hazelnut.Htyp.t = Arrow(Num, Num); + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some(Cursor(Asc(Lam("f", Lit(1)), Arrow(Num, Num)))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_aadel_1 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = + RAsc(Lam("f", Lit(1)), Cursor(Arrow(Num, Num))); + let a: Hazelnut.Action.t = Del; + let ht: Hazelnut.Htyp.t = Arrow(Num, Num); + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some(RAsc(Lam("f", Lit(1)), Cursor(Hole))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_aadel_2 = () => { + let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Num); + let ze: Hazelnut.Zexp.t = + RAsc(Lam("f", Plus(Lit(1), Var("x"))), RArrow(Num, Cursor(Num))); + let a: Hazelnut.Action.t = Del; + let ht: Hazelnut.Htyp.t = Arrow(Num, Num); + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some( + RAsc(Lam("f", Plus(Lit(1), Var("x"))), RArrow(Num, Cursor(Hole))), + ); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_aaconasc_1 = () => { + let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Num); + let ze: Hazelnut.Zexp.t = Cursor(Var("x")); + let a: Hazelnut.Action.t = Construct(Asc); + let ht: Hazelnut.Htyp.t = Num; + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some(RAsc(Var("x"), Cursor(Num))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_aaconasc_2 = () => { + let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Arrow(Num, Num)); + let ze: Hazelnut.Zexp.t = Cursor(Var("x")); + let a: Hazelnut.Action.t = Construct(Asc); + let ht: Hazelnut.Htyp.t = Arrow(Num, Num); + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some(RAsc(Var("x"), Cursor(Arrow(Num, Num)))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_aaconvar_1 = () => { + let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Arrow(Num, Num)); + let ze: Hazelnut.Zexp.t = Cursor(EHole); + let a: Hazelnut.Action.t = Construct(Var("x")); + let ht: Hazelnut.Htyp.t = Num; + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = Some(NEHole(Cursor(Var("x")))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_aaconvar_2 = () => { + let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Num); + let ze: Hazelnut.Zexp.t = Cursor(EHole); + let a: Hazelnut.Action.t = Construct(Var("x")); + let ht: Hazelnut.Htyp.t = Num; + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = Some(Cursor(Var("x"))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_aaconlam1_1 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = Cursor(EHole); + let a: Hazelnut.Action.t = Construct(Lam("x")); + let ht: Hazelnut.Htyp.t = Arrow(Num, Num); + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = Some(Lam("x", Cursor(EHole))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_aaconlam1_2 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = Cursor(EHole); + let a: Hazelnut.Action.t = Construct(Lam("x")); + let ht: Hazelnut.Htyp.t = Arrow(Hole, Hole); + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = Some(Lam("x", Cursor(EHole))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_aaconlam2_1 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = Cursor(EHole); + let a: Hazelnut.Action.t = Construct(Lam("x")); + let ht: Hazelnut.Htyp.t = Num; + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some(NEHole(RAsc(Lam("x", EHole), LArrow(Cursor(Hole), Hole)))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_aaconlam2_2 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = Cursor(EHole); + let a: Hazelnut.Action.t = Construct(Lam("y")); + let ht: Hazelnut.Htyp.t = Num; + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some(NEHole(RAsc(Lam("y", EHole), LArrow(Cursor(Hole), Hole)))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_aaconnumlit_1 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = Cursor(EHole); + let a: Hazelnut.Action.t = Construct(Lit(1)); + let ht: Hazelnut.Htyp.t = Arrow(Num, Num); + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = Some(NEHole(Cursor(Lit(1)))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_aaconnumlit_2 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = Cursor(EHole); + let a: Hazelnut.Action.t = Construct(Lit(-1)); + let ht: Hazelnut.Htyp.t = Num; + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = Some(Cursor(Lit(-1))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_aafinish_1 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = Cursor(NEHole(Plus(Lit(1), Lit(1)))); + let a: Hazelnut.Action.t = Finish; + let ht: Hazelnut.Htyp.t = Num; + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some(Cursor(Plus(Lit(1), Lit(1)))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_aafinish_2 = () => { + let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Num); + let ze: Hazelnut.Zexp.t = + Cursor(NEHole(NEHole(Lam("f", Plus(Var("x"), Var("x")))))); + let a: Hazelnut.Action.t = Finish; + let ht: Hazelnut.Htyp.t = Hole; + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = None; + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let ana_action_tests = [ + ("test_aamove_1", `Quick, test_aamove_1), + ("test_aamove_2", `Quick, test_aamove_2), + ("test_aamove_3", `Quick, test_aamove_3), + ("test_aadel_1", `Quick, test_aadel_1), + ("test_aadel_2", `Quick, test_aadel_2), + ("test_aaconasc_1", `Quick, test_aaconasc_1), + ("test_aaconasc_2", `Quick, test_aaconasc_2), + ("test_aaconvar_1", `Quick, test_aaconvar_1), + ("test_aaconvar_2", `Quick, test_aaconvar_2), + ("test_aaconlam1_1", `Quick, test_aaconlam1_1), + ("test_aaconlam1_2", `Quick, test_aaconlam1_2), + ("test_aaconlam2_1", `Quick, test_aaconlam2_1), + ("test_aaconlam2_2", `Quick, test_aaconlam2_2), + ("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), +]; diff --git a/test/Test_sample1.re b/test/Test_sample1.re new file mode 100644 index 0000000..fefd48c --- /dev/null +++ b/test/Test_sample1.re @@ -0,0 +1,362 @@ +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_syn_step_1 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = Cursor(EHole); + let t: Hazelnut.Htyp.t = Hole; + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Lam("x")); + 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_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")); + let ht: Hazelnut.Htyp.t = Arrow(Hole, Hole); + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = Some(Lam("x", Cursor(EHole))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_syn_step_2 = () => { + 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 = Construct(Hazelnut.Shape.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(Lam("x", EHole), LArrow(Cursor(Num), Hole)), + Arrow(Num, Hole), + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; + +let test_ana_step_2 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = + RAsc(Lam("x", EHole), LArrow(Cursor(Hole), Hole)); + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Num); + let ht: Hazelnut.Htyp.t = Arrow(Num, Hole); + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some(RAsc(Lam("x", EHole), LArrow(Cursor(Num), Hole))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_syn_step_3 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = + RAsc(Lam("x", EHole), LArrow(Cursor(Num), Hole)); + let t: Hazelnut.Htyp.t = Arrow(Num, 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(Num, Hole))), + Arrow(Num, Hole), + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; + +let test_ana_step_3 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = + RAsc(Lam("x", EHole), LArrow(Cursor(Num), Hole)); + let a: Hazelnut.Action.t = Move(Parent); + let ht: Hazelnut.Htyp.t = Arrow(Num, Hole); + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some(RAsc(Lam("x", EHole), Cursor(Arrow(Num, Hole)))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_syn_step_4 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = + RAsc(Lam("x", EHole), Cursor(Arrow(Num, Hole))); + let t: Hazelnut.Htyp.t = Arrow(Num, 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(Num, Cursor(Hole))), + Arrow(Num, Hole), + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; + +let test_ana_step_4 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = + RAsc(Lam("x", EHole), Cursor(Arrow(Num, Hole))); + let a: Hazelnut.Action.t = Move(Child(Two)); + let ht: Hazelnut.Htyp.t = Arrow(Num, Hole); + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some(RAsc(Lam("x", EHole), RArrow(Num, Cursor(Hole)))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_syn_step_5 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = + RAsc(Lam("x", EHole), RArrow(Num, Cursor(Hole))); + let t: Hazelnut.Htyp.t = Arrow(Num, Hole); + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.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(Lam("x", EHole), RArrow(Num, Cursor(Num))), + Arrow(Num, Num), + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; + +let test_ana_step_5 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = + RAsc(Lam("x", EHole), RArrow(Num, Cursor(Hole))); + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Num); + let ht: Hazelnut.Htyp.t = Arrow(Num, Num); + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some(RAsc(Lam("x", EHole), RArrow(Num, Cursor(Num)))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_syn_step_6 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = + RAsc(Lam("x", EHole), RArrow(Num, Cursor(Num))); + let t: Hazelnut.Htyp.t = Arrow(Num, 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(( + RAsc(Lam("x", EHole), Cursor(Arrow(Num, Num))), + Arrow(Num, Num), + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; + +let test_ana_step_6 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = + RAsc(Lam("x", EHole), RArrow(Num, Cursor(Num))); + let a: Hazelnut.Action.t = Move(Parent); + let ht: Hazelnut.Htyp.t = Arrow(Num, Num); + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some(RAsc(Lam("x", EHole), Cursor(Arrow(Num, Num)))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +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); + 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(Lam("x", EHole), Arrow(Num, Num))), + Arrow(Num, Num), + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; + +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); + let ht: Hazelnut.Htyp.t = Arrow(Num, Num); + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some(Cursor(Asc(Lam("x", EHole), Arrow(Num, Num)))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +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); + 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(Lam("x", EHole)), Arrow(Num, Num)), + Arrow(Num, Num), + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; + +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)); + let ht: Hazelnut.Htyp.t = Arrow(Num, Num); + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some(LAsc(Cursor(Lam("x", EHole)), Arrow(Num, Num))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +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); + 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(Lam("x", Cursor(EHole)), Arrow(Num, Num)), + Arrow(Num, Num), + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; + +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)); + let ht: Hazelnut.Htyp.t = Arrow(Num, Num); + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some(LAsc(Lam("x", Cursor(EHole)), Arrow(Num, Num))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +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); + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Var("x")); + 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(Lam("x", Cursor(Var("x"))), Arrow(Num, Num)), + Arrow(Num, Num), + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; + +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")); + let ht: Hazelnut.Htyp.t = Arrow(Num, Num); + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some(LAsc(Lam("x", Cursor(Var("x"))), Arrow(Num, Num))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +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)); + let t: Hazelnut.Htyp.t = Arrow(Num, Num); + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Plus); + 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(Lam("x", RPlus(Var("x"), Cursor(EHole))), Arrow(Num, Num)), + Arrow(Num, Num), + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; + +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)); + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Plus); + let ht: Hazelnut.Htyp.t = Arrow(Num, Num); + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some( + LAsc(Lam("x", RPlus(Var("x"), Cursor(EHole))), Arrow(Num, Num)), + ); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +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)); + let t: Hazelnut.Htyp.t = Arrow(Num, Num); + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Lit(1)); + 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(Lam("x", RPlus(Var("x"), Cursor(Lit(1)))), Arrow(Num, Num)), + Arrow(Num, Num), + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; + +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)); + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Lit(1)); + let ht: Hazelnut.Htyp.t = Arrow(Num, Num); + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some( + LAsc(Lam("x", RPlus(Var("x"), Cursor(Lit(1)))), Arrow(Num, Num)), + ); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let sample1_tests = [ + ("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 new file mode 100644 index 0000000..4b87fe1 --- /dev/null +++ b/test/Test_sample2.re @@ -0,0 +1,234 @@ +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_st14 = () => { + let ctx: typctx = TypCtx.singleton("incr", Hazelnut.Htyp.Arrow(Num, Num)); + let ze: Hazelnut.Zexp.t = Cursor(EHole); + let t: Hazelnut.Htyp.t = Hole; + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Var("incr")); + 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(Var("incr")), Arrow(Num, Num))); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; + +let test_ast14 = () => { + let ctx: typctx = TypCtx.singleton("incr", Hazelnut.Htyp.Arrow(Num, Num)); + let ze: Hazelnut.Zexp.t = Cursor(EHole); + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Var("incr")); + let ht: Hazelnut.Htyp.t = Arrow(Num, Num); + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = Some(Cursor(Var("incr"))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_st15 = () => { + let ctx: typctx = TypCtx.singleton("incr", Hazelnut.Htyp.Arrow(Num, Num)); + let ze: Hazelnut.Zexp.t = Cursor(Var("incr")); + let t: Hazelnut.Htyp.t = Arrow(Num, Num); + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Ap); + 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(Var("incr"), Cursor(EHole)), Num)); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; + +let test_ast15 = () => { + let ctx: typctx = TypCtx.singleton("incr", Hazelnut.Htyp.Arrow(Num, Num)); + let ze: Hazelnut.Zexp.t = Cursor(Var("incr")); + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Ap); + let ht: Hazelnut.Htyp.t = Num; + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some(RAp(Var("incr"), Cursor(EHole))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_st16 = () => { + let ctx: typctx = TypCtx.singleton("incr", Hazelnut.Htyp.Arrow(Num, Num)); + let ze: Hazelnut.Zexp.t = RAp(Var("incr"), Cursor(EHole)); + let t: Hazelnut.Htyp.t = Num; + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Var("incr")); + 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(Var("incr"), NEHole(Cursor(Var("incr")))), + Num, + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; + +let test_ast16 = () => { + let ctx: typctx = TypCtx.singleton("incr", Hazelnut.Htyp.Arrow(Num, Num)); + let ze: Hazelnut.Zexp.t = RAp(Var("incr"), Cursor(EHole)); + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Var("incr")); + let ht: Hazelnut.Htyp.t = Num; + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some(RAp(Var("incr"), NEHole(Cursor(Var("incr"))))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_st17 = () => { + let ctx: typctx = TypCtx.singleton("incr", Hazelnut.Htyp.Arrow(Num, Num)); + let ze: Hazelnut.Zexp.t = RAp(Var("incr"), NEHole(Cursor(Var("incr")))); + let t: Hazelnut.Htyp.t = Num; + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Ap); + 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(Var("incr"), NEHole(RAp(Var("incr"), Cursor(EHole)))), + Num, + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; + +let test_ast17 = () => { + let ctx: typctx = TypCtx.singleton("incr", Hazelnut.Htyp.Arrow(Num, Num)); + let ze: Hazelnut.Zexp.t = RAp(Var("incr"), NEHole(Cursor(Var("incr")))); + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Ap); + let ht: Hazelnut.Htyp.t = Num; + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some(RAp(Var("incr"), NEHole(RAp(Var("incr"), Cursor(EHole))))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_st18 = () => { + let ctx: typctx = TypCtx.singleton("incr", Hazelnut.Htyp.Arrow(Num, Num)); + let ze: Hazelnut.Zexp.t = + RAp(Var("incr"), NEHole(RAp(Var("incr"), Cursor(EHole)))); + let t: Hazelnut.Htyp.t = Num; + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Lit(3)); + 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(Var("incr"), NEHole(RAp(Var("incr"), Cursor(Lit(3))))), + Num, + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; + +let test_ast18 = () => { + let ctx: typctx = TypCtx.singleton("incr", Hazelnut.Htyp.Arrow(Num, Num)); + let ze: Hazelnut.Zexp.t = + RAp(Var("incr"), NEHole(RAp(Var("incr"), Cursor(EHole)))); + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Lit(3)); + let ht: Hazelnut.Htyp.t = Num; + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some(RAp(Var("incr"), NEHole(RAp(Var("incr"), Cursor(Lit(3)))))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_st19 = () => { + let ctx: typctx = TypCtx.singleton("incr", Hazelnut.Htyp.Arrow(Num, Num)); + let ze: Hazelnut.Zexp.t = + RAp(Var("incr"), NEHole(RAp(Var("incr"), Cursor(Lit(3))))); + 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(( + RAp(Var("incr"), NEHole(Cursor(Ap(Var("incr"), Lit(3))))), + Num, + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; + +let test_ast19 = () => { + let ctx: typctx = TypCtx.singleton("incr", Hazelnut.Htyp.Arrow(Num, Num)); + let ze: Hazelnut.Zexp.t = + RAp(Var("incr"), NEHole(RAp(Var("incr"), Cursor(Lit(3))))); + let a: Hazelnut.Action.t = Move(Parent); + let ht: Hazelnut.Htyp.t = Num; + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some(RAp(Var("incr"), NEHole(Cursor(Ap(Var("incr"), Lit(3)))))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_st20 = () => { + let ctx: typctx = TypCtx.singleton("incr", Hazelnut.Htyp.Arrow(Num, Num)); + let ze: Hazelnut.Zexp.t = + RAp(Var("incr"), NEHole(Cursor(Ap(Var("incr"), Lit(3))))); + 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(( + RAp(Var("incr"), Cursor(NEHole(Ap(Var("incr"), Lit(3))))), + Num, + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; + +let test_ast20 = () => { + let ctx: typctx = TypCtx.singleton("incr", Hazelnut.Htyp.Arrow(Num, Num)); + let ze: Hazelnut.Zexp.t = + RAp(Var("incr"), NEHole(Cursor(Ap(Var("incr"), Lit(3))))); + let a: Hazelnut.Action.t = Move(Parent); + let ht: Hazelnut.Htyp.t = Num; + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some(RAp(Var("incr"), Cursor(NEHole(Ap(Var("incr"), Lit(3)))))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let test_st21 = () => { + let ctx: typctx = TypCtx.singleton("incr", Hazelnut.Htyp.Arrow(Num, Num)); + let ze: Hazelnut.Zexp.t = + RAp(Var("incr"), Cursor(NEHole(Ap(Var("incr"), Lit(3))))); + let t: Hazelnut.Htyp.t = Num; + let a: Hazelnut.Action.t = Finish; + 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(Var("incr"), Cursor(Ap(Var("incr"), Lit(3)))), + Num, + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; + +let test_ast21 = () => { + let ctx: typctx = TypCtx.singleton("incr", Hazelnut.Htyp.Arrow(Num, Num)); + let ze: Hazelnut.Zexp.t = + RAp(Var("incr"), Cursor(NEHole(Ap(Var("incr"), Lit(3))))); + let a: Hazelnut.Action.t = Finish; + let ht: Hazelnut.Htyp.t = Num; + let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht); + let expected: option(Hazelnut.Zexp.t) = + Some(RAp(Var("incr"), Cursor(Ap(Var("incr"), Lit(3))))); + check(zexp_typ, "same Hazelnut.Zexp.t", given, expected); +}; + +let sample2_tests = [ + ("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 new file mode 100644 index 0000000..1d2b85f --- /dev/null +++ b/test/Test_syn_action.re @@ -0,0 +1,511 @@ +open Alcotest; +open Test_interface; +module Hazelnut = Hazelnut_lib.Hazelnut; +module TypCtx = Map.Make(String); +type typctx = Hazelnut.TypCtx.t(Hazelnut.Htyp.t); + +// 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)); + 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(( + LAsc(Lam("x", Cursor(EHole)), Arrow(Hole, Hole)), + Arrow(Hole, Hole), + )); + 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)); + 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((Cursor(EHole), Hole)); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_sadel_2 = () => { + 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 = 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((NEHole(Cursor(EHole)), Hole)); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_saconasc_1 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = Cursor(Lit(1)); + let t: Hazelnut.Htyp.t = Num; + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Asc); + 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_saconasc_2 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = Cursor(EHole); + let t: Hazelnut.Htyp.t = Hole; + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Asc); + 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(EHole, Cursor(Hole)), Hole)); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_saconasc_3 = () => { + 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 = Construct(Hazelnut.Shape.Asc); + 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(RAsc(Lit(1), Cursor(Num))), Hole)); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_saconvar_1 = () => { + let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Num); + let ze: Hazelnut.Zexp.t = Cursor(EHole); + let t: Hazelnut.Htyp.t = Hole; + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Var("x")); + 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(Var("x")), Num)); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_saconvar_2 = () => { + let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Num); + let ze: Hazelnut.Zexp.t = NEHole(Cursor(EHole)); + let t: Hazelnut.Htyp.t = Hole; + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Var("x")); + 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(Var("x"))), Hole)); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_saconlam_1 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = Cursor(EHole); + let t: Hazelnut.Htyp.t = Hole; + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Lam("x")); + 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_saconlam_2 = () => { + //CHECK THIS ONE + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = NEHole(Cursor(EHole)); + let t: Hazelnut.Htyp.t = Hole; + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Lam("x")); + 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(RAsc(Lam("x", EHole), LArrow(Cursor(Hole), Hole))), + Hole, + )); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_saconnumlit_1 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = Cursor(EHole); + let t: Hazelnut.Htyp.t = Hole; + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Lit(1)); + 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(Lit(1)), Num)); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_saconnumlit_2 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = NEHole(Cursor(EHole)); + let t: Hazelnut.Htyp.t = Hole; + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Lit(1)); + 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_saconnehole_1 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = Cursor(Lit(1)); + let t: Hazelnut.Htyp.t = Num; + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.NEHole); + 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_saconnehole_2 = () => { + 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 = Construct(Hazelnut.Shape.NEHole); + 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(NEHole(Cursor(Lit(1)))), Hole)); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_saconaparr_1 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = Cursor(Lam("x", EHole)); + let t: Hazelnut.Htyp.t = Arrow(Hole, Hole); + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Ap); + 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_saconapotw_1 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = Cursor(Lit(1)); + let t: Hazelnut.Htyp.t = Num; + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Ap); + 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(NEHole(Lit(1)), Cursor(EHole)), Hole)); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_saconapotw_2 = () => { + 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 = Construct(Hazelnut.Shape.Ap); + 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(RAp(NEHole(Lit(1)), Cursor(EHole))), Hole)); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_saconplus1_1 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = Cursor(Lit(1)); + let t: Hazelnut.Htyp.t = Num; + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Plus); + 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(EHole)), Num)); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_saconplus1_2 = () => { + 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 = Construct(Hazelnut.Shape.Plus); + 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(RPlus(Lit(1), Cursor(EHole))), Hole)); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_saconplus2_1 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = Cursor(Lam("x", EHole)); + let t: Hazelnut.Htyp.t = Arrow(Hole, Hole); + let a: Hazelnut.Action.t = Construct(Hazelnut.Shape.Plus); + 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(NEHole(Lam("x", EHole)), Cursor(EHole)), Num)); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_safinish_1 = () => { + 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 = Finish; + 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(Lit(1)), Num)); + check(zexp_htyp, "same option(Hazelnut.Zexp.t)", given, expected); +}; +let test_safinish_2 = () => { + let ctx: typctx = TypCtx.empty; + let ze: Hazelnut.Zexp.t = NEHole(Cursor(NEHole(Lit(1)))); + let t: Hazelnut.Htyp.t = Hole; + let a: Hazelnut.Action.t = Finish; + 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 syn_action_tests = [ + ("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), + ("test_safinish_2", `Quick, test_safinish_2), + ("test_saconasc_1", `Quick, test_saconasc_1), + ("test_saconasc_2", `Quick, test_saconasc_2), + ("test_saconasc_3", `Quick, test_saconasc_3), + ("test_saconvar_1", `Quick, test_saconvar_1), + ("test_saconvar_2", `Quick, test_saconvar_2), + ("test_saconlam_1", `Quick, test_saconlam_1), + ("test_saconlam_2", `Quick, test_saconlam_2), + ("test_saconnumlit_1", `Quick, test_saconnumlit_1), + ("test_saconnumlit_2", `Quick, test_saconnumlit_2), + ("test_saconnehole_1", `Quick, test_saconnehole_1), + ("test_saconnehole_2", `Quick, test_saconnehole_2), + ("test_saconaparr_1", `Quick, test_saconaparr_1), + ("test_saconapotw_1", `Quick, test_saconapotw_1), + ("test_saconapotw_2", `Quick, test_saconapotw_2), + ("test_saconplus1_1", `Quick, test_saconplus1_1), + ("test_saconplus1_2", `Quick, test_saconplus1_2), + ("test_saconplus2_1", `Quick, test_saconplus2_1), +]; diff --git a/test/Test_type_action.re b/test/Test_type_action.re new file mode 100644 index 0000000..8a1d312 --- /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(Lam("x", 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(Lam("x", 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/dune b/test/dune index fd6fb35..cdc5c6d 100644 --- a/test/dune +++ b/test/dune @@ -1,3 +1,4 @@ (test (name hazelnut_test) (libraries hazelnut_lib alcotest)) + \ No newline at end of file diff --git a/test/hazelnut_test.re b/test/hazelnut_test.re index ed930a9..1edc33f 100644 --- a/test/hazelnut_test.re +++ b/test/hazelnut_test.re @@ -6,5 +6,11 @@ let () = [ ("erase_exp", Test_erase_exp.erase_exp_tests), ("syn", Test_syn.syn_tests), + ("ana", Test_ana.ana_tests), + ("ana_action", Test_ana_action.ana_action_tests), + ("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), ], ); diff --git a/test/test_interface.re b/test/test_interface.re index a42f442..5947d83 100644 --- a/test/test_interface.re +++ b/test/test_interface.re @@ -4,7 +4,7 @@ module Hazelnut = Hazelnut_lib.Hazelnut; let hexp_eq = (he1: Hazelnut.Hexp.t, he2: Hazelnut.Hexp.t): bool => Hazelnut.Hexp.compare(he1, he2) == 0; -let hexp_print = (_: Hazelnut.Hexp.t): string => "hexp"; +let hexp_print = (e: Hazelnut.Hexp.t): string => Hazelnut.Hexp.show(e); let hexp_typ = testable(Fmt.using(hexp_print, Fmt.string), hexp_eq); @@ -18,8 +18,46 @@ let htyp_eq = let htyp_print = (ht: option(Hazelnut.Htyp.t)): string => switch (ht) { - | Some(_) => "htyp" + | Some(t) => Hazelnut.Htyp.show(t) | _ => "None" }; let htyp_typ = testable(Fmt.using(htyp_print, Fmt.string), htyp_eq); + +let zexp_eq = + (ze1: option(Hazelnut.Zexp.t), ze2: option(Hazelnut.Zexp.t)): bool => + switch (ze1, ze2) { + | (Some(e1), Some(e2)) => Hazelnut.Zexp.compare(e1, e2) == 0 + | (None, None) => true + | _ => false + }; + +let zexp_print = (ze: option(Hazelnut.Zexp.t)): string => + switch (ze) { + | Some(e) => Hazelnut.Zexp.show(e) + | _ => "None" + }; + +let zexp_typ = testable(Fmt.using(zexp_print, Fmt.string), zexp_eq); + +let zexp_htyp_eq = + ( + ze_t1: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)), + ze_t2: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t)), + ) + : bool => + switch (ze_t1, ze_t2) { + | (Some((e1, t1)), Some((e2, t2))) => + Hazelnut.Zexp.compare(e1, e2) == 0 && Hazelnut.Htyp.compare(t1, t2) == 0 + | _ => false + }; + +let zexp_htyp_print = + (ze_t: option((Hazelnut.Zexp.t, Hazelnut.Htyp.t))): string => + switch (ze_t) { + | Some((e, _)) => Hazelnut.Zexp.show(e) // have to show both somehow + | _ => "None" + }; + +let zexp_htyp = + testable(Fmt.using(zexp_htyp_print, Fmt.string), zexp_htyp_eq);