From 5c75a6b8a70be8059928da571e633c986e80ad29 Mon Sep 17 00:00:00 2001 From: jpoly1219 Date: Wed, 14 Feb 2024 02:21:34 -0500 Subject: [PATCH 01/19] add tests for erase_exp --- test/Test_erase_exp.re | 78 ++++++++++++++++++++++++++++++++++++++++++ test/dune | 3 ++ test/hazelnut_test.re | 4 +++ test/test_interface.re | 8 +++++ 4 files changed, 93 insertions(+) create mode 100644 test/Test_erase_exp.re create mode 100644 test/dune create mode 100644 test/hazelnut_test.re create mode 100644 test/test_interface.re diff --git a/test/Test_erase_exp.re b/test/Test_erase_exp.re new file mode 100644 index 0000000..2f2a823 --- /dev/null +++ b/test/Test_erase_exp.re @@ -0,0 +1,78 @@ +open Alcotest; +open Hazelnut_lib.Hazelnut; +open Test_interfaces; + +let test_eetop = () => { + let ze: zexp = Cursor(Var("x")); + let given: hexp = erase_exp(ze); + let expected: hexp = Var("x"); + check(hexp_typ, "same hexp", given, expected); +}; + +let test_eeascl = () => { + let ze: zexp = LAsc(Cursor(Lam("f", Lit(1))), Arrow(Num, Num)); + let given: hexp = erase_exp(ze); + let expected: hexp = Asc(Lam("f", Lit(1)), Arrow(Num, Num)); + check(hexp_typ, "same hexp", given, expected); +}; + +let test_eeascr = () => { + let ze: zexp = RAsc(Lam("f", Lit(1)), Cursor(Arrow(Num, Num))); + let given: hexp = erase_exp(ze); + let expected: hexp = Asc(Lam("f", Lit(1)), Arrow(Num, Num)); + check(hexp_typ, "same hexp", given, expected); +}; + +let test_eelam = () => { + let ze: zexp = Lam("f", Cursor(Lit(1))); + let given: hexp = erase_exp(ze); + let expected: hexp = Lam("f", Lit(1)); + check(hexp_typ, "same hexp", given, expected); +}; + +let test_eeapl = () => { + let ze: zexp = LAp(Cursor(Lam("f", Lit(1))), Var("x")); + let given: hexp = erase_exp(ze); + let expected: hexp = Ap(Lam("f", Lit(1)), Var("x")); + check(hexp_typ, "same hexp", given, expected); +}; + +let test_eeapr = () => { + let ze: zexp = RAp(Lam("f", Lit(1)), Cursor(Var("x"))); + let given: hexp = erase_exp(ze); + let expected: hexp = Ap(Lam("f", Lit(1)), Var("x")); + check(hexp_typ, "same hexp", given, expected); +}; + +let test_eeplusl = () => { + let ze: zexp = LPlus(Cursor(Var("x")), Var("y")); + let given: hexp = erase_exp(ze); + let expected: hexp = Plus(Var("x"), Var("y")); + check(hexp_typ, "same hexp", given, expected); +}; + +let test_eeplusr = () => { + let ze: zexp = RPlus(Var("x"), Cursor(Var("y"))); + let given: hexp = erase_exp(ze); + let expected: hexp = Plus(Var("x"), Var("y")); + check(hexp_typ, "same hexp", given, expected); +}; + +let test_eenehole = () => { + let ze: zexp = NEHole(Cursor(Lam("f", Lit(1)))); + let given: hexp = erase_exp(ze); + let expected: hexp = NEHole(Lam("f", Lit(1))); + check(hexp_typ, "same hexp", given, expected); +}; + +let erase_exp_tests = [ + ("test_eetop", `Quick, test_eetop), + ("test_eeascl", `Quick, test_eeascl), + ("test_eeascr", `Quick, test_eeascr), + ("test_eelam", `Quick, test_eelam), + ("test_eeapl", `Quick, test_eeapl), + ("test_eeapr", `Quick, test_eeapr), + ("test_eeplusl", `Quick, test_eeplusl), + ("test_eeplusr", `Quick, test_eeplusr), + ("test_eenehole", `Quick, test_eenehole), +]; diff --git a/test/dune b/test/dune new file mode 100644 index 0000000..fd6fb35 --- /dev/null +++ b/test/dune @@ -0,0 +1,3 @@ +(test + (name hazelnut_test) + (libraries hazelnut_lib alcotest)) diff --git a/test/hazelnut_test.re b/test/hazelnut_test.re new file mode 100644 index 0000000..c64a00a --- /dev/null +++ b/test/hazelnut_test.re @@ -0,0 +1,4 @@ +open Alcotest; + +let () = + run("Hazelnut_tests", [("erase_exp", Test_erase_exp.erase_exp_tests)]); diff --git a/test/test_interface.re b/test/test_interface.re new file mode 100644 index 0000000..c8b85d7 --- /dev/null +++ b/test/test_interface.re @@ -0,0 +1,8 @@ +open Alcotest; +open Hazelnut_lib.Hazelnut; + +let hexp_eq = (he1: hexp, he2: hexp): bool => compare_hexp(he1, he2) == 0; + +let hexp_print = (_: hexp): string => "hexp"; // this needs to be fixed to print a stringified version of the type + +let hexp_typ = testable(Fmt.using(hexp_print, Fmt.string), hexp_eq); From 5e0511289eac95116b8b79bbbbf41fccd665ab02 Mon Sep 17 00:00:00 2001 From: jpoly1219 Date: Thu, 15 Feb 2024 15:49:31 -0500 Subject: [PATCH 02/19] wrap hazelnut types into modules --- hazelnut/hazelnut.re | 156 +++++++++++++++++++++++------------------- hazelnut/hazelnut.rei | 134 ++++++++++++++++++++---------------- 2 files changed, 163 insertions(+), 127 deletions(-) diff --git a/hazelnut/hazelnut.re b/hazelnut/hazelnut.re index 54ac061..3113d9f 100644 --- a/hazelnut/hazelnut.re +++ b/hazelnut/hazelnut.re @@ -4,76 +4,92 @@ open Sexplib.Std; let compare_string = String.compare; let compare_int = Int.compare; -[@deriving (sexp, compare)] -type htyp = - | Arrow(htyp, htyp) - | Num - | Hole; - -[@deriving (sexp, compare)] -type hexp = - | Var(string) - | Lam(string, hexp) - | Ap(hexp, hexp) - | Lit(int) - | Plus(hexp, hexp) - | Asc(hexp, htyp) - | EHole - | NEHole(hexp); - -[@deriving (sexp, compare)] -type ztyp = - | Cursor(htyp) - | LArrow(ztyp, htyp) - | RArrow(htyp, ztyp); - -[@deriving (sexp, compare)] -type zexp = - | Cursor(hexp) - | Lam(string, zexp) - | LAp(zexp, hexp) - | RAp(hexp, zexp) - | LPlus(zexp, hexp) - | RPlus(hexp, zexp) - | LAsc(zexp, htyp) - | RAsc(hexp, ztyp) - | NEHole(zexp); - -[@deriving (sexp, compare)] -type child = - | One - | Two; - -[@deriving (sexp, compare)] -type dir = - | Child(child) - | Parent; - -[@deriving (sexp, compare)] -type shape = - | Arrow - | Num - | Asc - | Var(string) - | Lam(string) - | Ap - | Lit(int) - | Plus - | NEHole; - -[@deriving (sexp, compare)] -type action = - | Move(dir) - | Construct(shape) - | Del - | Finish; +module Htyp = { + [@deriving (sexp, compare)] + type t = + | Arrow(t, t) + | Num + | Hole; +}; + +module Hexp = { + [@deriving (sexp, compare)] + type t = + | Var(string) + | Lam(string, t) + | Ap(t, t) + | Lit(int) + | Plus(t, t) + | Asc(t, Htyp.t) + | EHole + | NEHole(t); +}; + +module Ztyp = { + [@deriving (sexp, compare)] + type t = + | Cursor(Htyp.t) + | LArrow(t, Htyp.t) + | RArrow(Htyp.t, t); +}; + +module Zexp = { + [@deriving (sexp, compare)] + type t = + | Cursor(Hexp.t) + | Lam(string, t) + | LAp(t, Hexp.t) + | RAp(Hexp.t, t) + | LPlus(t, Hexp.t) + | RPlus(Hexp.t, t) + | LAsc(t, Htyp.t) + | RAsc(Hexp.t, Ztyp.t) + | NEHole(t); +}; + +module Child = { + [@deriving (sexp, compare)] + type t = + | One + | Two; +}; + +module Dir = { + [@deriving (sexp, compare)] + type t = + | Child(Child.t) + | Parent; +}; + +module Shape = { + [@deriving (sexp, compare)] + type t = + | Arrow + | Num + | Asc + | Var(string) + | Lam(string) + | Ap + | Lit(int) + | Plus + | NEHole; +}; + +module Action = { + [@deriving (sexp, compare)] + type t = + | Move(Dir.t) + | Construct(Shape.t) + | Del + | Finish; +}; module TypCtx = Map.Make(String); -type typctx = TypCtx.t(htyp); +type typctx = TypCtx.t(Htyp.t); exception Unimplemented; -let erase_exp = (e: zexp): hexp => { +let erase_exp = (e: Zexp.t): Hexp.t => { // Used to suppress unused variable warnings // Okay to remove let _ = e; @@ -81,7 +97,7 @@ let erase_exp = (e: zexp): hexp => { raise(Unimplemented); }; -let syn = (ctx: typctx, e: hexp): option(htyp) => { +let syn = (ctx: typctx, e: Hexp.t): option(Htyp.t) => { // Used to suppress unused variable warnings // Okay to remove let _ = ctx; @@ -90,7 +106,7 @@ let syn = (ctx: typctx, e: hexp): option(htyp) => { raise(Unimplemented); } -and ana = (ctx: typctx, e: hexp, t: htyp): bool => { +and ana = (ctx: typctx, e: Hexp.t, t: Htyp.t): bool => { // Used to suppress unused variable warnings // Okay to remove let _ = ctx; @@ -101,7 +117,8 @@ and ana = (ctx: typctx, e: hexp, t: htyp): bool => { }; let syn_action = - (ctx: typctx, (e: zexp, t: htyp), a: action): option((zexp, htyp)) => { + (ctx: typctx, (e: Zexp.t, t: Htyp.t), a: Action.t) + : option((Zexp.t, Htyp.t)) => { // Used to suppress unused variable warnings // Okay to remove let _ = ctx; @@ -112,7 +129,8 @@ let syn_action = raise(Unimplemented); } -and ana_action = (ctx: typctx, e: zexp, a: action, t: htyp): option(zexp) => { +and ana_action = + (ctx: typctx, e: Zexp.t, a: Action.t, t: Htyp.t): option(Zexp.t) => { // Used to suppress unused variable warnings // Okay to remove let _ = ctx; diff --git a/hazelnut/hazelnut.rei b/hazelnut/hazelnut.rei index 34efc43..f74011d 100644 --- a/hazelnut/hazelnut.rei +++ b/hazelnut/hazelnut.rei @@ -1,73 +1,91 @@ -[@deriving (sexp, compare)] -type htyp = - | Arrow(htyp, htyp) - | Num - | Hole; +module Htyp: { + [@deriving (sexp, compare)] + type t = + | Arrow(t, t) + | Num + | Hole; +}; -[@deriving compare] -type hexp = - | Var(string) - | Lam(string, hexp) - | Ap(hexp, hexp) - | Lit(int) - | Plus(hexp, hexp) - | Asc(hexp, htyp) - | EHole - | NEHole(hexp); +module Hexp: { + [@deriving (sexp, compare)] + type t = + | Var(string) + | Lam(string, t) + | Ap(t, t) + | Lit(int) + | Plus(t, t) + | Asc(t, Htyp.t) + | EHole + | NEHole(t); +}; -type ztyp = - | Cursor(htyp) - | LArrow(ztyp, htyp) - | RArrow(htyp, ztyp); +module Ztyp: { + [@deriving (sexp, compare)] + type t = + | Cursor(Htyp.t) + | LArrow(t, Htyp.t) + | RArrow(Htyp.t, t); +}; -[@deriving (sexp, compare)] -type zexp = - | Cursor(hexp) - | Lam(string, zexp) - | LAp(zexp, hexp) - | RAp(hexp, zexp) - | LPlus(zexp, hexp) - | RPlus(hexp, zexp) - | LAsc(zexp, htyp) - | RAsc(hexp, ztyp) - | NEHole(zexp); +module Zexp: { + [@deriving (sexp, compare)] + type t = + | Cursor(Hexp.t) + | Lam(string, t) + | LAp(t, Hexp.t) + | RAp(Hexp.t, t) + | LPlus(t, Hexp.t) + | RPlus(Hexp.t, t) + | LAsc(t, Htyp.t) + | RAsc(Hexp.t, Ztyp.t) + | NEHole(t); +}; -type child = - | One - | Two; +module Child: { + type t = + | One + | Two; +}; -type dir = - | Child(child) - | Parent; +module Dir: { + type t = + | Child(Child.t) + | Parent; +}; -type shape = - | Arrow - | Num - | Asc - | Var(string) - | Lam(string) - | Ap - | Lit(int) - | Plus - | NEHole; +module Shape: { + type t = + | Arrow + | Num + | Asc + | Var(string) + | Lam(string) + | Ap + | Lit(int) + | Plus + | NEHole; +}; -[@deriving (sexp, compare)] -type action = - | Move(dir) - | Construct(shape) - | Del - | Finish; +module Action: { + [@deriving (sexp, compare)] + type t = + | Move(Dir.t) + | Construct(Shape.t) + | Del + | Finish; +}; module TypCtx: { type t('a) = Map.Make(String).t('a); let empty: t('a); }; -type typctx = TypCtx.t(htyp); +type typctx = TypCtx.t(Htyp.t); exception Unimplemented; -let erase_exp: zexp => hexp; -let syn: (typctx, hexp) => option(htyp); -let ana: (typctx, hexp, htyp) => bool; -let syn_action: (typctx, (zexp, htyp), action) => option((zexp, htyp)); -let ana_action: (typctx, zexp, action, htyp) => option(zexp); +let erase_exp: Zexp.t => Hexp.t; +let syn: (typctx, Hexp.t) => option(Htyp.t); +let ana: (typctx, Hexp.t, Htyp.t) => bool; +let syn_action: + (typctx, (Zexp.t, Htyp.t), Action.t) => option((Zexp.t, Htyp.t)); +let ana_action: (typctx, Zexp.t, Action.t, Htyp.t) => option(Zexp.t); From 75220c17b39067cbae782fc6974ff5e8ddc371c8 Mon Sep 17 00:00:00 2001 From: jpoly1219 Date: Thu, 15 Feb 2024 15:49:40 -0500 Subject: [PATCH 03/19] wrap app types into modules --- lib/app.re | 88 ++++++++++++++++++++++++++++-------------------------- 1 file changed, 46 insertions(+), 42 deletions(-) diff --git a/lib/app.re b/lib/app.re index 44566fa..b854315 100644 --- a/lib/app.re +++ b/lib/app.re @@ -4,26 +4,28 @@ open Monad_lib.Monad; module Hazelnut = Hazelnut_lib.Hazelnut; // A combination of all Hazelnut types for purposes of printing -type pexp = - | Cursor(pexp) - | Arrow(pexp, pexp) - | Num - | Var(string) - | Lam(string, pexp) - | Ap(pexp, pexp) - | Lit(int) - | Plus(pexp, pexp) - | Asc(pexp, pexp) - | EHole - | NEHole(pexp); - -let rec pexp_of_htyp: Hazelnut.htyp => pexp = +module Pexp = { + type t = + | Cursor(t) + | Arrow(t, t) + | Num + | Var(string) + | Lam(string, t) + | Ap(t, t) + | Lit(int) + | Plus(t, t) + | Asc(t, t) + | EHole + | NEHole(t); +}; + +let rec pexp_of_htyp: Hazelnut.Htyp.t => Pexp.t = fun | Arrow(t1, t2) => Arrow(pexp_of_htyp(t1), pexp_of_htyp(t2)) | Num => Num | Hole => EHole; -let rec pexp_of_hexp: Hazelnut.hexp => pexp = +let rec pexp_of_hexp: Hazelnut.Hexp.t => Pexp.t = fun | Var(x) => Var(x) | Lam(x, e) => Lam(x, pexp_of_hexp(e)) @@ -34,13 +36,13 @@ let rec pexp_of_hexp: Hazelnut.hexp => pexp = | EHole => EHole | NEHole(e) => NEHole(pexp_of_hexp(e)); -let rec pexp_of_ztyp: Hazelnut.ztyp => pexp = +let rec pexp_of_ztyp: Hazelnut.Ztyp.t => Pexp.t = fun | Cursor(t) => Cursor(pexp_of_htyp(t)) | LArrow(t1, t2) => Arrow(pexp_of_ztyp(t1), pexp_of_htyp(t2)) | RArrow(t1, t2) => Arrow(pexp_of_htyp(t1), pexp_of_ztyp(t2)); -let rec pexp_of_zexp: Hazelnut.zexp => pexp = +let rec pexp_of_zexp: Hazelnut.Zexp.t => Pexp.t = fun | Cursor(e) => Cursor(pexp_of_hexp(e)) | Lam(x, e) => Lam(x, pexp_of_zexp(e)) @@ -53,7 +55,7 @@ let rec pexp_of_zexp: Hazelnut.zexp => pexp = | NEHole(e) => NEHole(pexp_of_zexp(e)); // Lower is tighter -let rec prec: pexp => int = +let rec prec: Pexp.t => int = fun | Cursor(e) => prec(e) | Arrow(_) => 1 @@ -67,12 +69,14 @@ let rec prec: pexp => int = | EHole => 0 | NEHole(_) => 0; -type side = - | Left - | Right - | Atom; +module Side = { + type t = + | Left + | Right + | Atom; +}; -let rec assoc: pexp => side = +let rec assoc: Pexp.t => Side.t = fun | Cursor(e) => assoc(e) | Arrow(_) => Right @@ -86,25 +90,25 @@ let rec assoc: pexp => side = | EHole => Atom | NEHole(_) => Atom; -let rec string_of_pexp: pexp => string = +let rec string_of_pexp: Pexp.t => string = fun | Cursor(e) => "👉" ++ string_of_pexp(e) ++ "👈" | Arrow(t1, t2) as outer => - paren(t1, outer, Left) ++ " -> " ++ paren(t2, outer, Right) + paren(t1, outer, Side.Left) ++ " -> " ++ paren(t2, outer, Side.Right) | Num => "Num" | Var(x) => x | Lam(x, e) => "fun " ++ x ++ " -> { " ++ string_of_pexp(e) ++ " }" | Ap(e1, e2) as outer => - paren(e1, outer, Left) ++ " " ++ paren(e2, outer, Right) + paren(e1, outer, Side.Left) ++ " " ++ paren(e2, outer, Side.Right) | Lit(n) => string_of_int(n) | Plus(e1, e2) as outer => - paren(e1, outer, Left) ++ " + " ++ paren(e2, outer, Right) + paren(e1, outer, Side.Left) ++ " + " ++ paren(e2, outer, Side.Right) | Asc(e, t) as outer => - paren(e, outer, Left) ++ ": " ++ paren(t, outer, Right) + paren(e, outer, Side.Left) ++ ": " ++ paren(t, outer, Side.Right) | EHole => "[ ]" | NEHole(e) => "[ " ++ string_of_pexp(e) ++ " ]" -and paren = (inner: pexp, outer: pexp, side: side): string => { +and paren = (inner: Pexp.t, outer: Pexp.t, side: Side.t): string => { let unparenned = string_of_pexp(inner); let parenned = "(" ++ unparenned ++ ")"; @@ -117,8 +121,8 @@ and paren = (inner: pexp, outer: pexp, side: side): string => { parenned; } else { switch (assoc(inner), side) { - | (Left, Right) - | (Right, Left) => parenned + | (Side.Left, Side.Right) + | (Side.Right, Side.Left) => parenned | _ => unparenned }; }; @@ -126,11 +130,11 @@ and paren = (inner: pexp, outer: pexp, side: side): string => { let check_for_theorem_violation = ( - a: Hazelnut.action, - e: Hazelnut.zexp, - t: Hazelnut.htyp, - e': Hazelnut.zexp, - t': Hazelnut.htyp, + a: Hazelnut.Action.t, + e: Hazelnut.Zexp.t, + t: Hazelnut.Htyp.t, + e': Hazelnut.Zexp.t, + t': Hazelnut.Htyp.t, ) : option(string) => try({ @@ -142,7 +146,7 @@ let check_for_theorem_violation = switch (Hazelnut.syn(Hazelnut.TypCtx.empty, e')) { | Some(syn_t') => - if (Hazelnut.compare_htyp(t', syn_t') == 0) { + if (Hazelnut.Htyp.compare(t', syn_t') == 0) { None; } else { warning; @@ -154,8 +158,8 @@ let check_for_theorem_violation = let theorem_2 = switch (a) { | Move(_) => - if (Hazelnut.compare_hexp(e, e') == 0 - && Hazelnut.compare_htyp(t, t') == 0) { + if (Hazelnut.Hexp.compare(e, e') == 0 + && Hazelnut.Htyp.compare(t, t') == 0) { None; } else { Some("Theorem 2 violation (movement erasure invariance)"); @@ -174,8 +178,8 @@ let check_for_theorem_violation = [@deriving (sexp, fields, compare)] type state = { - e: Hazelnut.zexp, - t: Hazelnut.htyp, + e: Hazelnut.Zexp.t, + t: Hazelnut.Htyp.t, warning: option(string), var_input: string, lam_input: string, @@ -210,7 +214,7 @@ module Action = { [@deriving sexp] type action = - | HazelnutAction(Hazelnut.action) + | HazelnutAction(Hazelnut.Action.t) | UpdateInput(input_location, string) | ShowWarning(string); From 3a99014dedeca1bf491fd90ac131dc2ddcea7fa8 Mon Sep 17 00:00:00 2001 From: jpoly1219 Date: Thu, 15 Feb 2024 15:50:08 -0500 Subject: [PATCH 04/19] update hazelnut type definitions --- test/test_interface.re | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/test/test_interface.re b/test/test_interface.re index c8b85d7..52d4f63 100644 --- a/test/test_interface.re +++ b/test/test_interface.re @@ -1,8 +1,9 @@ open Alcotest; -open Hazelnut_lib.Hazelnut; +module Hazelnut = Hazelnut_lib.Hazelnut; -let hexp_eq = (he1: hexp, he2: hexp): bool => compare_hexp(he1, he2) == 0; +let hexp_eq = (he1: Hazelnut.Hexp.t, he2: Hazelnut.Hexp.t): bool => + Hazelnut.Hexp.compare(he1, he2) == 0; -let hexp_print = (_: hexp): string => "hexp"; // this needs to be fixed to print a stringified version of the type +let hexp_print = (_: Hazelnut.Hexp.t): string => "hexp"; let hexp_typ = testable(Fmt.using(hexp_print, Fmt.string), hexp_eq); From 30b9f8b915a5b65911caaec4f0fe59c544c40d39 Mon Sep 17 00:00:00 2001 From: jpoly1219 Date: Thu, 15 Feb 2024 16:04:06 -0500 Subject: [PATCH 05/19] add rule for running the test suite --- Makefile | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Makefile b/Makefile index 287bbe5..fdf5730 100644 --- a/Makefile +++ b/Makefile @@ -18,3 +18,6 @@ clean: deps: opam install dune reason incr_dom ocaml-lsp-server + +test_impl: + dune test From d03c5bb45e92e8052b0062c4b0a20de48ae6006e Mon Sep 17 00:00:00 2001 From: jpoly1219 Date: Thu, 15 Feb 2024 16:04:18 -0500 Subject: [PATCH 06/19] add instructions for running the test suite --- README.md | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/README.md b/README.md index 5d675d3..196ead1 100644 --- a/README.md +++ b/README.md @@ -71,6 +71,11 @@ To erase the build: make clean ``` +To test your implementation: +```sh +make test_impl +``` + ## Implementing Hazelnut Now it's your turn to implement Hazelnut! @@ -112,6 +117,10 @@ If anything unexpected happens, a warning will appear at the bottom. Here's what | Unimplemented | You called upon an operation that you haven't implemented yet. | | Theorem violation | Your implementation has a bug that caused it to violate a Hazelnut metatheorem. Note: This won't catch every metatheorem violation, only some of them. | +## Testing your implementation + +We include a test suite to test your implementation. Run `make test_impl` at the root of the project directory to run the test suite. + ## Using the Maybe Monad Have you ever written code that looks like this? From ecfd2bc29cbc3cd445cf944eadce440e5b3c1896 Mon Sep 17 00:00:00 2001 From: jpoly1219 Date: Thu, 15 Feb 2024 16:04:28 -0500 Subject: [PATCH 07/19] update type definitions --- test/Test_erase_exp.re | 78 ++++++++++++++++++++++-------------------- 1 file changed, 40 insertions(+), 38 deletions(-) diff --git a/test/Test_erase_exp.re b/test/Test_erase_exp.re index 2f2a823..4ccb7d1 100644 --- a/test/Test_erase_exp.re +++ b/test/Test_erase_exp.re @@ -1,68 +1,70 @@ open Alcotest; -open Hazelnut_lib.Hazelnut; -open Test_interfaces; +open Test_interface; +module Hazelnut = Hazelnut_lib.Hazelnut; let test_eetop = () => { - let ze: zexp = Cursor(Var("x")); - let given: hexp = erase_exp(ze); - let expected: hexp = Var("x"); - check(hexp_typ, "same hexp", given, expected); + let ze: Hazelnut.Zexp.t = Cursor(Var("x")); + let given: Hazelnut.Hexp.t = Hazelnut.erase_exp(ze); + let expected: Hazelnut.Hexp.t = Var("x"); + check(hexp_typ, "same Hazelnut.Hexp.t", given, expected); }; let test_eeascl = () => { - let ze: zexp = LAsc(Cursor(Lam("f", Lit(1))), Arrow(Num, Num)); - let given: hexp = erase_exp(ze); - let expected: hexp = Asc(Lam("f", Lit(1)), Arrow(Num, Num)); - check(hexp_typ, "same hexp", given, expected); + let ze: Hazelnut.Zexp.t = + LAsc(Cursor(Lam("f", Lit(1))), Arrow(Num, Num)); + let given: Hazelnut.Hexp.t = Hazelnut.erase_exp(ze); + let expected: Hazelnut.Hexp.t = Asc(Lam("f", Lit(1)), Arrow(Num, Num)); + check(hexp_typ, "same Hazelnut.Hexp.t", given, expected); }; let test_eeascr = () => { - let ze: zexp = RAsc(Lam("f", Lit(1)), Cursor(Arrow(Num, Num))); - let given: hexp = erase_exp(ze); - let expected: hexp = Asc(Lam("f", Lit(1)), Arrow(Num, Num)); - check(hexp_typ, "same hexp", given, expected); + let ze: Hazelnut.Zexp.t = + RAsc(Lam("f", Lit(1)), Cursor(Arrow(Num, Num))); + let given: Hazelnut.Hexp.t = Hazelnut.erase_exp(ze); + let expected: Hazelnut.Hexp.t = Asc(Lam("f", Lit(1)), Arrow(Num, Num)); + check(hexp_typ, "same Hazelnut.Hexp.t", given, expected); }; let test_eelam = () => { - let ze: zexp = Lam("f", Cursor(Lit(1))); - let given: hexp = erase_exp(ze); - let expected: hexp = Lam("f", Lit(1)); - check(hexp_typ, "same hexp", given, expected); + let ze: Hazelnut.Zexp.t = Lam("f", Cursor(Lit(1))); + let given: Hazelnut.Hexp.t = Hazelnut.erase_exp(ze); + let expected: Hazelnut.Hexp.t = Lam("f", Lit(1)); + check(hexp_typ, "same Hazelnut.Hexp.t", given, expected); }; let test_eeapl = () => { - let ze: zexp = LAp(Cursor(Lam("f", Lit(1))), Var("x")); - let given: hexp = erase_exp(ze); - let expected: hexp = Ap(Lam("f", Lit(1)), Var("x")); - check(hexp_typ, "same hexp", given, expected); + let ze: Hazelnut.Zexp.t = LAp(Cursor(Lam("f", Lit(1))), Var("x")); + let given: Hazelnut.Hexp.t = Hazelnut.erase_exp(ze); + let expected: Hazelnut.Hexp.t = Ap(Lam("f", Lit(1)), Var("x")); + check(hexp_typ, "same Hazelnut.Hexp.t", given, expected); }; let test_eeapr = () => { - let ze: zexp = RAp(Lam("f", Lit(1)), Cursor(Var("x"))); - let given: hexp = erase_exp(ze); - let expected: hexp = Ap(Lam("f", Lit(1)), Var("x")); - check(hexp_typ, "same hexp", given, expected); + let ze: Hazelnut.Zexp.t = RAp(Lam("f", Lit(1)), Cursor(Var("x"))); + let given: Hazelnut.Hexp.t = Hazelnut.erase_exp(ze); + let expected: Hazelnut.Hexp.t = Ap(Lam("f", Lit(1)), Var("x")); + check(hexp_typ, "same Hazelnut.Hexp.t", given, expected); }; let test_eeplusl = () => { - let ze: zexp = LPlus(Cursor(Var("x")), Var("y")); - let given: hexp = erase_exp(ze); - let expected: hexp = Plus(Var("x"), Var("y")); - check(hexp_typ, "same hexp", given, expected); + let ze: Hazelnut.Zexp.t = LPlus(Cursor(Var("x")), Var("y")); + let given: Hazelnut.Hexp.t = Hazelnut.erase_exp(ze); + let expected: Hazelnut.Hexp.t = Plus(Var("x"), Var("y")); + check(hexp_typ, "same Hazelnut.Hexp.t", given, expected); }; let test_eeplusr = () => { - let ze: zexp = RPlus(Var("x"), Cursor(Var("y"))); - let given: hexp = erase_exp(ze); - let expected: hexp = Plus(Var("x"), Var("y")); - check(hexp_typ, "same hexp", given, expected); + let ze: Hazelnut.Zexp.t = RPlus(Var("x"), Cursor(Var("y"))); + let given: Hazelnut.Hexp.t = Hazelnut.erase_exp(ze); + let expected: Hazelnut.Hexp.t = Plus(Var("x"), Var("y")); + check(hexp_typ, "same Hazelnut.Hexp.t", given, expected); }; let test_eenehole = () => { - let ze: zexp = NEHole(Cursor(Lam("f", Lit(1)))); - let given: hexp = erase_exp(ze); - let expected: hexp = NEHole(Lam("f", Lit(1))); - check(hexp_typ, "same hexp", given, expected); + let ze: Hazelnut.Zexp.t = NEHole(Cursor(Lam("f", Lit(1)))); + let given: Hazelnut.Hexp.t = Hazelnut.erase_exp(ze); + let expected: Hazelnut.Hexp.t = NEHole(Lam("f", Lit(1))); + check(hexp_typ, "same Hazelnut.Hexp.t", given, expected); }; let erase_exp_tests = [ From e8aad3bdc52cd980f34fe8784c94bfea4a85e56c Mon Sep 17 00:00:00 2001 From: jpoly1219 Date: Thu, 15 Feb 2024 23:32:43 -0500 Subject: [PATCH 08/19] add deeper nesting to test for recursion --- test/Test_erase_exp.re | 119 ++++++++++++++++++++++++++++++++++------- 1 file changed, 101 insertions(+), 18 deletions(-) diff --git a/test/Test_erase_exp.re b/test/Test_erase_exp.re index 4ccb7d1..824a4dc 100644 --- a/test/Test_erase_exp.re +++ b/test/Test_erase_exp.re @@ -2,14 +2,21 @@ open Alcotest; open Test_interface; module Hazelnut = Hazelnut_lib.Hazelnut; -let test_eetop = () => { +let test_eetop_1 = () => { let ze: Hazelnut.Zexp.t = Cursor(Var("x")); let given: Hazelnut.Hexp.t = Hazelnut.erase_exp(ze); let expected: Hazelnut.Hexp.t = Var("x"); check(hexp_typ, "same Hazelnut.Hexp.t", given, expected); }; -let test_eeascl = () => { +let test_eetop_2 = () => { + let ze: Hazelnut.Zexp.t = Cursor(EHole); + let given: Hazelnut.Hexp.t = Hazelnut.erase_exp(ze); + let expected: Hazelnut.Hexp.t = EHole; + check(hexp_typ, "same Hazelnut.Hexp.t", given, expected); +}; + +let test_eeascl_1 = () => { let ze: Hazelnut.Zexp.t = LAsc(Cursor(Lam("f", Lit(1))), Arrow(Num, Num)); let given: Hazelnut.Hexp.t = Hazelnut.erase_exp(ze); @@ -17,7 +24,15 @@ let test_eeascl = () => { check(hexp_typ, "same Hazelnut.Hexp.t", given, expected); }; -let test_eeascr = () => { +let test_eeascl_2 = () => { + let ze: Hazelnut.Zexp.t = + LAsc(Lam("f", Cursor(Lit(1))), Arrow(Num, Num)); + let given: Hazelnut.Hexp.t = Hazelnut.erase_exp(ze); + let expected: Hazelnut.Hexp.t = Asc(Lam("f", Lit(1)), Arrow(Num, Num)); + check(hexp_typ, "same Hazelnut.Hexp.t", given, expected); +}; + +let test_eeascr_1 = () => { let ze: Hazelnut.Zexp.t = RAsc(Lam("f", Lit(1)), Cursor(Arrow(Num, Num))); let given: Hazelnut.Hexp.t = Hazelnut.erase_exp(ze); @@ -25,56 +40,124 @@ let test_eeascr = () => { check(hexp_typ, "same Hazelnut.Hexp.t", given, expected); }; -let test_eelam = () => { +let test_eeascr_2 = () => { + let ze: Hazelnut.Zexp.t = RAsc(NEHole(Var("y")), Cursor(Hole)); + let given: Hazelnut.Hexp.t = Hazelnut.erase_exp(ze); + let expected: Hazelnut.Hexp.t = Asc(NEHole(Var("y")), Hole); + check(hexp_typ, "same Hazelnut.Hexp.t", given, expected); +}; + +let test_eelam_1 = () => { let ze: Hazelnut.Zexp.t = Lam("f", Cursor(Lit(1))); let given: Hazelnut.Hexp.t = Hazelnut.erase_exp(ze); let expected: Hazelnut.Hexp.t = Lam("f", Lit(1)); check(hexp_typ, "same Hazelnut.Hexp.t", given, expected); }; -let test_eeapl = () => { +let test_eelam_2 = () => { + let ze: Hazelnut.Zexp.t = + Lam("f", LPlus(RPlus(Lit(1), Cursor(Lit(1))), Lit(2))); + let given: Hazelnut.Hexp.t = Hazelnut.erase_exp(ze); + let expected: Hazelnut.Hexp.t = + Lam("f", Plus(Plus(Lit(1), Lit(1)), Lit(2))); + check(hexp_typ, "same Hazelnut.Hexp.t", given, expected); +}; + +let test_eeapl_1 = () => { let ze: Hazelnut.Zexp.t = LAp(Cursor(Lam("f", Lit(1))), Var("x")); let given: Hazelnut.Hexp.t = Hazelnut.erase_exp(ze); let expected: Hazelnut.Hexp.t = Ap(Lam("f", Lit(1)), Var("x")); check(hexp_typ, "same Hazelnut.Hexp.t", given, expected); }; -let test_eeapr = () => { +let test_eeapl_2 = () => { + let ze: Hazelnut.Zexp.t = + LAp(Lam("f", Lam("g", Cursor(EHole))), Var("x")); + let given: Hazelnut.Hexp.t = Hazelnut.erase_exp(ze); + let expected: Hazelnut.Hexp.t = Ap(Lam("f", Lam("g", EHole)), Var("x")); + check(hexp_typ, "same Hazelnut.Hexp.t", given, expected); +}; + +let test_eeapr_1 = () => { let ze: Hazelnut.Zexp.t = RAp(Lam("f", Lit(1)), Cursor(Var("x"))); let given: Hazelnut.Hexp.t = Hazelnut.erase_exp(ze); let expected: Hazelnut.Hexp.t = Ap(Lam("f", Lit(1)), Var("x")); check(hexp_typ, "same Hazelnut.Hexp.t", given, expected); }; -let test_eeplusl = () => { +let test_eeapr_2 = () => { + let ze: Hazelnut.Zexp.t = + RAp(Lam("f", Lit(1)), LAsc(NEHole(Cursor(Lit(1))), Hole)); + let given: Hazelnut.Hexp.t = Hazelnut.erase_exp(ze); + let expected: Hazelnut.Hexp.t = + Ap(Lam("f", Lit(1)), Asc(NEHole(Lit(1)), Hole)); + check(hexp_typ, "same Hazelnut.Hexp.t", given, expected); +}; + +let test_eeplusl_1 = () => { let ze: Hazelnut.Zexp.t = LPlus(Cursor(Var("x")), Var("y")); let given: Hazelnut.Hexp.t = Hazelnut.erase_exp(ze); let expected: Hazelnut.Hexp.t = Plus(Var("x"), Var("y")); check(hexp_typ, "same Hazelnut.Hexp.t", given, expected); }; -let test_eeplusr = () => { +let test_eeplusl_2 = () => { + let ze: Hazelnut.Zexp.t = + LPlus(Lam("f", RPlus(Lit(1), Cursor(Lit(2)))), Var("y")); + let given: Hazelnut.Hexp.t = Hazelnut.erase_exp(ze); + let expected: Hazelnut.Hexp.t = + Plus(Lam("f", Plus(Lit(1), Lit(2))), Var("y")); + check(hexp_typ, "same Hazelnut.Hexp.t", given, expected); +}; + +let test_eeplusr_1 = () => { let ze: Hazelnut.Zexp.t = RPlus(Var("x"), Cursor(Var("y"))); let given: Hazelnut.Hexp.t = Hazelnut.erase_exp(ze); let expected: Hazelnut.Hexp.t = Plus(Var("x"), Var("y")); check(hexp_typ, "same Hazelnut.Hexp.t", given, expected); }; -let test_eenehole = () => { +let test_eeplusr_2 = () => { + let ze: Hazelnut.Zexp.t = + RPlus(Var("x"), NEHole(NEHole(Cursor(Var("y"))))); + let given: Hazelnut.Hexp.t = Hazelnut.erase_exp(ze); + let expected: Hazelnut.Hexp.t = + Plus(Var("x"), NEHole(NEHole(Var("y")))); + check(hexp_typ, "same Hazelnut.Hexp.t", given, expected); +}; + +let test_eenehole_1 = () => { let ze: Hazelnut.Zexp.t = NEHole(Cursor(Lam("f", Lit(1)))); let given: Hazelnut.Hexp.t = Hazelnut.erase_exp(ze); let expected: Hazelnut.Hexp.t = NEHole(Lam("f", Lit(1))); check(hexp_typ, "same Hazelnut.Hexp.t", given, expected); }; +let test_eenehole_2 = () => { + let ze: Hazelnut.Zexp.t = + NEHole(LAp(NEHole(Cursor(Var("f"))), Var("x"))); + let given: Hazelnut.Hexp.t = Hazelnut.erase_exp(ze); + let expected: Hazelnut.Hexp.t = NEHole(Ap(NEHole(Var("f")), Var("x"))); + check(hexp_typ, "same Hazelnut.Hexp.t", given, expected); +}; + let erase_exp_tests = [ - ("test_eetop", `Quick, test_eetop), - ("test_eeascl", `Quick, test_eeascl), - ("test_eeascr", `Quick, test_eeascr), - ("test_eelam", `Quick, test_eelam), - ("test_eeapl", `Quick, test_eeapl), - ("test_eeapr", `Quick, test_eeapr), - ("test_eeplusl", `Quick, test_eeplusl), - ("test_eeplusr", `Quick, test_eeplusr), - ("test_eenehole", `Quick, test_eenehole), + ("test_eetop_1", `Quick, test_eetop_1), + ("test_eetop_2", `Quick, test_eetop_2), + ("test_eeascl_1", `Quick, test_eeascl_1), + ("test_eeascl_2", `Quick, test_eeascl_2), + ("test_eeascr_1", `Quick, test_eeascr_1), + ("test_eeascr_2", `Quick, test_eeascr_2), + ("test_eelam_1", `Quick, test_eelam_1), + ("test_eelam_2", `Quick, test_eelam_2), + ("test_eeapl_1", `Quick, test_eeapl_1), + ("test_eeapl_2", `Quick, test_eeapl_2), + ("test_eeapr_1", `Quick, test_eeapr_1), + ("test_eeapr_2", `Quick, test_eeapr_2), + ("test_eeplusl_1", `Quick, test_eeplusl_1), + ("test_eeplusl_2", `Quick, test_eeplusl_2), + ("test_eeplusr_1", `Quick, test_eeplusr_1), + ("test_eeplusr_2", `Quick, test_eeplusr_2), + ("test_eenehole_1", `Quick, test_eenehole_1), + ("test_eenehole_2", `Quick, test_eenehole_2), ]; From a122607f8b24c8305930a17945a7f2fabfb461d7 Mon Sep 17 00:00:00 2001 From: jpoly1219 Date: Sat, 17 Feb 2024 01:10:44 -0500 Subject: [PATCH 09/19] remove redundant instructions, update command --- README.md | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/README.md b/README.md index 196ead1..c1ce2a2 100644 --- a/README.md +++ b/README.md @@ -73,7 +73,7 @@ make clean To test your implementation: ```sh -make test_impl +make test ``` ## Implementing Hazelnut @@ -117,9 +117,6 @@ If anything unexpected happens, a warning will appear at the bottom. Here's what | Unimplemented | You called upon an operation that you haven't implemented yet. | | Theorem violation | Your implementation has a bug that caused it to violate a Hazelnut metatheorem. Note: This won't catch every metatheorem violation, only some of them. | -## Testing your implementation - -We include a test suite to test your implementation. Run `make test_impl` at the root of the project directory to run the test suite. ## Using the Maybe Monad From 5ad7d9542b3ef0fc0c6dfa3e49859fc81b854723 Mon Sep 17 00:00:00 2001 From: jpoly1219 Date: Sat, 17 Feb 2024 01:10:57 -0500 Subject: [PATCH 10/19] make test name more concise --- Makefile | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Makefile b/Makefile index fdf5730..c30b2a1 100644 --- a/Makefile +++ b/Makefile @@ -19,5 +19,6 @@ clean: deps: opam install dune reason incr_dom ocaml-lsp-server -test_impl: +.PHONY: test +test: dune test From e99f472d3d0e046c8528aa539742b74f5d92d416 Mon Sep 17 00:00:00 2001 From: jpoly1219 Date: Mon, 19 Feb 2024 13:52:44 -0500 Subject: [PATCH 11/19] run syn tests --- test/hazelnut_test.re | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/test/hazelnut_test.re b/test/hazelnut_test.re index c64a00a..ed930a9 100644 --- a/test/hazelnut_test.re +++ b/test/hazelnut_test.re @@ -1,4 +1,10 @@ open Alcotest; let () = - run("Hazelnut_tests", [("erase_exp", Test_erase_exp.erase_exp_tests)]); + run( + "Hazelnut_tests", + [ + ("erase_exp", Test_erase_exp.erase_exp_tests), + ("syn", Test_syn.syn_tests), + ], + ); From 861117c36acd55a4153871ca57ccc2a5d5b78431 Mon Sep 17 00:00:00 2001 From: jpoly1219 Date: Mon, 19 Feb 2024 13:52:54 -0500 Subject: [PATCH 12/19] add interface for htyp --- test/test_interface.re | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/test/test_interface.re b/test/test_interface.re index 52d4f63..a42f442 100644 --- a/test/test_interface.re +++ b/test/test_interface.re @@ -7,3 +7,19 @@ let hexp_eq = (he1: Hazelnut.Hexp.t, he2: Hazelnut.Hexp.t): bool => let hexp_print = (_: Hazelnut.Hexp.t): string => "hexp"; let hexp_typ = testable(Fmt.using(hexp_print, Fmt.string), hexp_eq); + +let htyp_eq = + (ht1: option(Hazelnut.Htyp.t), ht2: option(Hazelnut.Htyp.t)): bool => + switch (ht1, ht2) { + | (Some(t1), Some(t2)) => Hazelnut.Htyp.compare(t1, t2) == 0 + | (None, None) => true + | _ => false + }; + +let htyp_print = (ht: option(Hazelnut.Htyp.t)): string => + switch (ht) { + | Some(_) => "htyp" + | _ => "None" + }; + +let htyp_typ = testable(Fmt.using(htyp_print, Fmt.string), htyp_eq); From c109c54fda0c22cf5323ff42cb2cc3865a2c934b Mon Sep 17 00:00:00 2001 From: jpoly1219 Date: Mon, 19 Feb 2024 13:53:15 -0500 Subject: [PATCH 13/19] add sasc test cases for syn --- test/Test_syn.re | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) create mode 100644 test/Test_syn.re diff --git a/test/Test_syn.re b/test/Test_syn.re new file mode 100644 index 0000000..14648df --- /dev/null +++ b/test/Test_syn.re @@ -0,0 +1,31 @@ +open Alcotest; +open Test_interface; +module Hazelnut = Hazelnut_lib.Hazelnut; + +// adding context definition here because importing from Hazelnut gives an unbound error +// TODO: fix this +module TypCtx = Map.Make(String); +type typctx = Hazelnut.TypCtx.t(Hazelnut.Htyp.t); + +let test_sasc_1 = () => { + let ctx: typctx = TypCtx.empty; + let he: Hazelnut.Hexp.t = Var("x"); + let given: option(Hazelnut.Htyp.t) = Hazelnut.syn(ctx, he); + let expected: option(Hazelnut.Htyp.t) = None; + + check(htyp_typ, "same option(Hazelnut.Htyp.t)", given, expected); +}; + +let test_sasc_2 = () => { + let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Num); + let he: Hazelnut.Hexp.t = Var("x"); + let given: option(Hazelnut.Htyp.t) = Hazelnut.syn(ctx, he); + let expected: option(Hazelnut.Htyp.t) = Some(Hazelnut.Htyp.Num); + + check(htyp_typ, "same option(Hazelnut.Htyp.t)", given, expected); +}; + +let syn_tests = [ + ("test_sasc_1", `Quick, test_sasc_1), + ("test_sasc_2", `Quick, test_sasc_2), +]; From b71bb2e7d25056e6209bcd796823963d99fbfeac Mon Sep 17 00:00:00 2001 From: jpoly1219 Date: Mon, 19 Feb 2024 16:07:50 -0500 Subject: [PATCH 14/19] rename tests, add sasc and svar tests --- test/Test_syn.re | 22 +++++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) diff --git a/test/Test_syn.re b/test/Test_syn.re index 14648df..c3bf3db 100644 --- a/test/Test_syn.re +++ b/test/Test_syn.re @@ -8,6 +8,24 @@ module TypCtx = Map.Make(String); type typctx = Hazelnut.TypCtx.t(Hazelnut.Htyp.t); let test_sasc_1 = () => { + let ctx: typctx = TypCtx.empty; + let he: Hazelnut.Hexp.t = + Asc(Lam("x", Plus(Lit(1), Lit(2))), Arrow(Num, Num)); + let given: option(Hazelnut.Htyp.t) = Hazelnut.syn(ctx, he); + let expected: option(Hazelnut.Htyp.t) = + Some(Hazelnut.Htyp.Arrow(Num, Num)); + check(htyp_typ, "same option(Hazelnut.Htyp.t)", given, expected); +}; + +let test_sasc_2 = () => { + let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Num); + let he: Hazelnut.Hexp.t = Asc(NEHole(Var("x")), Hole); + let given: option(Hazelnut.Htyp.t) = Hazelnut.syn(ctx, he); + let expected: option(Hazelnut.Htyp.t) = Some(Hazelnut.Htyp.Hole); + check(htyp_typ, "same option(Hazelnut.Htyp.t)", given, expected); +}; + +let test_svar_1 = () => { let ctx: typctx = TypCtx.empty; let he: Hazelnut.Hexp.t = Var("x"); let given: option(Hazelnut.Htyp.t) = Hazelnut.syn(ctx, he); @@ -16,7 +34,7 @@ let test_sasc_1 = () => { check(htyp_typ, "same option(Hazelnut.Htyp.t)", given, expected); }; -let test_sasc_2 = () => { +let test_svar_2 = () => { let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Num); let he: Hazelnut.Hexp.t = Var("x"); let given: option(Hazelnut.Htyp.t) = Hazelnut.syn(ctx, he); @@ -28,4 +46,6 @@ let test_sasc_2 = () => { let syn_tests = [ ("test_sasc_1", `Quick, test_sasc_1), ("test_sasc_2", `Quick, test_sasc_2), + ("test_svar_1", `Quick, test_svar_1), + ("test_svar_2", `Quick, test_svar_2), ]; From ae5e319530bd8a328589bf229b8cfd6c955b18c3 Mon Sep 17 00:00:00 2001 From: jpoly1219 Date: Mon, 19 Feb 2024 16:25:37 -0500 Subject: [PATCH 15/19] add sap tests --- test/Test_syn.re | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/test/Test_syn.re b/test/Test_syn.re index c3bf3db..6c28717 100644 --- a/test/Test_syn.re +++ b/test/Test_syn.re @@ -30,7 +30,6 @@ let test_svar_1 = () => { let he: Hazelnut.Hexp.t = Var("x"); let given: option(Hazelnut.Htyp.t) = Hazelnut.syn(ctx, he); let expected: option(Hazelnut.Htyp.t) = None; - check(htyp_typ, "same option(Hazelnut.Htyp.t)", given, expected); }; @@ -39,7 +38,23 @@ let test_svar_2 = () => { let he: Hazelnut.Hexp.t = Var("x"); let given: option(Hazelnut.Htyp.t) = Hazelnut.syn(ctx, he); let expected: option(Hazelnut.Htyp.t) = Some(Hazelnut.Htyp.Num); + check(htyp_typ, "same option(Hazelnut.Htyp.t)", given, expected); +}; + +let test_sap_1 = () => { + let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Arrow(Num, Num)); + let he: Hazelnut.Hexp.t = Ap(Var("x"), Lit(1)); + let given: option(Hazelnut.Htyp.t) = Hazelnut.syn(ctx, he); + let expected: option(Hazelnut.Htyp.t) = Some(Hazelnut.Htyp.Num); + check(htyp_typ, "same option(Hazelnut.Htyp.t)", given, expected); +}; +let test_sap_2 = () => { + let ctx: typctx = + TypCtx.singleton("x", Hazelnut.Htyp.Arrow(Arrow(Num, Num), Num)); + let he: Hazelnut.Hexp.t = Ap(Var("x"), Lam("y", Lit(1))); + let given: option(Hazelnut.Htyp.t) = Hazelnut.syn(ctx, he); + let expected: option(Hazelnut.Htyp.t) = Some(Hazelnut.Htyp.Num); check(htyp_typ, "same option(Hazelnut.Htyp.t)", given, expected); }; @@ -48,4 +63,6 @@ let syn_tests = [ ("test_sasc_2", `Quick, test_sasc_2), ("test_svar_1", `Quick, test_svar_1), ("test_svar_2", `Quick, test_svar_2), + ("test_sap_1", `Quick, test_sap_1), + ("test_sap_2", `Quick, test_sap_2), ]; From 878d933783d8801c7402bc6420481c507f8654e1 Mon Sep 17 00:00:00 2001 From: jpoly1219 Date: Mon, 19 Feb 2024 16:35:23 -0500 Subject: [PATCH 16/19] add snum tests --- test/Test_syn.re | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/test/Test_syn.re b/test/Test_syn.re index 6c28717..184c711 100644 --- a/test/Test_syn.re +++ b/test/Test_syn.re @@ -58,6 +58,22 @@ let test_sap_2 = () => { check(htyp_typ, "same option(Hazelnut.Htyp.t)", given, expected); }; +let test_snum_1 = () => { + let ctx: typctx = TypCtx.empty; + let he: Hazelnut.Hexp.t = Lit(1); + let given: option(Hazelnut.Htyp.t) = Hazelnut.syn(ctx, he); + let expected: option(Hazelnut.Htyp.t) = Some(Hazelnut.Htyp.Num); + check(htyp_typ, "same option(Hazelnut.Htyp.t)", given, expected); +}; + +let test_snum_2 = () => { + let ctx: typctx = TypCtx.empty; + let he: Hazelnut.Hexp.t = Lit(-1); + let given: option(Hazelnut.Htyp.t) = Hazelnut.syn(ctx, he); + let expected: option(Hazelnut.Htyp.t) = Some(Hazelnut.Htyp.Num); + check(htyp_typ, "same option(Hazelnut.Htyp.t)", given, expected); +}; + let syn_tests = [ ("test_sasc_1", `Quick, test_sasc_1), ("test_sasc_2", `Quick, test_sasc_2), @@ -65,4 +81,6 @@ let syn_tests = [ ("test_svar_2", `Quick, test_svar_2), ("test_sap_1", `Quick, test_sap_1), ("test_sap_2", `Quick, test_sap_2), + ("test_snum_1", `Quick, test_snum_1), + ("test_snum_2", `Quick, test_snum_2), ]; From 92b829f71b6e3f8d56ff0e97bf58ce558234b6bd Mon Sep 17 00:00:00 2001 From: jpoly1219 Date: Mon, 19 Feb 2024 16:39:18 -0500 Subject: [PATCH 17/19] add splus tests --- test/Test_syn.re | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/test/Test_syn.re b/test/Test_syn.re index 184c711..80b9c33 100644 --- a/test/Test_syn.re +++ b/test/Test_syn.re @@ -74,6 +74,22 @@ let test_snum_2 = () => { check(htyp_typ, "same option(Hazelnut.Htyp.t)", given, expected); }; +let test_splus_1 = () => { + let ctx: typctx = TypCtx.empty; + let he: Hazelnut.Hexp.t = Plus(Lit(1), Lit(-1)); + let given: option(Hazelnut.Htyp.t) = Hazelnut.syn(ctx, he); + let expected: option(Hazelnut.Htyp.t) = Some(Hazelnut.Htyp.Num); + check(htyp_typ, "same option(Hazelnut.Htyp.t)", given, expected); +}; + +let test_splus_2 = () => { + let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Num); + let he: Hazelnut.Hexp.t = Plus(Lit(1), Var("x")); + let given: option(Hazelnut.Htyp.t) = Hazelnut.syn(ctx, he); + let expected: option(Hazelnut.Htyp.t) = Some(Hazelnut.Htyp.Num); + check(htyp_typ, "same option(Hazelnut.Htyp.t)", given, expected); +}; + let syn_tests = [ ("test_sasc_1", `Quick, test_sasc_1), ("test_sasc_2", `Quick, test_sasc_2), @@ -83,4 +99,6 @@ let syn_tests = [ ("test_sap_2", `Quick, test_sap_2), ("test_snum_1", `Quick, test_snum_1), ("test_snum_2", `Quick, test_snum_2), + ("test_splus_1", `Quick, test_splus_1), + ("test_splus_2", `Quick, test_splus_2), ]; From 6f998258ced2ae9c7aae8007df6e58c8d718f2a8 Mon Sep 17 00:00:00 2001 From: jpoly1219 Date: Mon, 19 Feb 2024 16:43:04 -0500 Subject: [PATCH 18/19] add shole tests --- test/Test_syn.re | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/test/Test_syn.re b/test/Test_syn.re index 80b9c33..012ad3f 100644 --- a/test/Test_syn.re +++ b/test/Test_syn.re @@ -90,6 +90,22 @@ let test_splus_2 = () => { check(htyp_typ, "same option(Hazelnut.Htyp.t)", given, expected); }; +let test_shole_1 = () => { + let ctx: typctx = TypCtx.empty; + let he: Hazelnut.Hexp.t = EHole; + let given: option(Hazelnut.Htyp.t) = Hazelnut.syn(ctx, he); + let expected: option(Hazelnut.Htyp.t) = Some(Hazelnut.Htyp.Hole); + check(htyp_typ, "same option(Hazelnut.Htyp.t)", given, expected); +}; + +let test_shole_2 = () => { + let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Hole); + let he: Hazelnut.Hexp.t = Var("x"); + let given: option(Hazelnut.Htyp.t) = Hazelnut.syn(ctx, he); + let expected: option(Hazelnut.Htyp.t) = Some(Hazelnut.Htyp.Hole); + check(htyp_typ, "same option(Hazelnut.Htyp.t)", given, expected); +}; + let syn_tests = [ ("test_sasc_1", `Quick, test_sasc_1), ("test_sasc_2", `Quick, test_sasc_2), @@ -101,4 +117,6 @@ let syn_tests = [ ("test_snum_2", `Quick, test_snum_2), ("test_splus_1", `Quick, test_splus_1), ("test_splus_2", `Quick, test_splus_2), + ("test_shole_1", `Quick, test_shole_1), + ("test_shole_2", `Quick, test_shole_2), ]; From 79c4a21c91544d0d63f489da911a6dc0c50bffa4 Mon Sep 17 00:00:00 2001 From: jpoly1219 Date: Mon, 19 Feb 2024 16:47:07 -0500 Subject: [PATCH 19/19] add snehole tests --- test/Test_syn.re | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/test/Test_syn.re b/test/Test_syn.re index 012ad3f..25b0db3 100644 --- a/test/Test_syn.re +++ b/test/Test_syn.re @@ -106,6 +106,22 @@ let test_shole_2 = () => { check(htyp_typ, "same option(Hazelnut.Htyp.t)", given, expected); }; +let test_snehole_1 = () => { + let ctx: typctx = TypCtx.empty; + let he: Hazelnut.Hexp.t = NEHole(EHole); + let given: option(Hazelnut.Htyp.t) = Hazelnut.syn(ctx, he); + let expected: option(Hazelnut.Htyp.t) = Some(Hazelnut.Htyp.Hole); + check(htyp_typ, "same option(Hazelnut.Htyp.t)", given, expected); +}; + +let test_snehole_2 = () => { + let ctx: typctx = TypCtx.singleton("incr", Hazelnut.Htyp.Arrow(Num, Num)); + let he: Hazelnut.Hexp.t = NEHole(Asc(Ap(Var("incr"), Lit(1)), Num)); + let given: option(Hazelnut.Htyp.t) = Hazelnut.syn(ctx, he); + let expected: option(Hazelnut.Htyp.t) = Some(Hazelnut.Htyp.Hole); + check(htyp_typ, "same option(Hazelnut.Htyp.t)", given, expected); +}; + let syn_tests = [ ("test_sasc_1", `Quick, test_sasc_1), ("test_sasc_2", `Quick, test_sasc_2), @@ -119,4 +135,6 @@ let syn_tests = [ ("test_splus_2", `Quick, test_splus_2), ("test_shole_1", `Quick, test_shole_1), ("test_shole_2", `Quick, test_shole_2), + ("test_snehole_1", `Quick, test_snehole_1), + ("test_snehole_2", `Quick, test_snehole_2), ];