From 04d63981dce075b19fc45aea7013cf9d83b65178 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sat, 10 Aug 2024 12:47:24 -0400 Subject: [PATCH 01/23] Starting adding tests for util modules --- test/Test_ListUtil.re | 29 +++++++++++++++++++++++++++++ test/haz3ltest.re | 7 +++++-- 2 files changed, 34 insertions(+), 2 deletions(-) create mode 100644 test/Test_ListUtil.re diff --git a/test/Test_ListUtil.re b/test/Test_ListUtil.re new file mode 100644 index 0000000000..76881fcb75 --- /dev/null +++ b/test/Test_ListUtil.re @@ -0,0 +1,29 @@ +open Alcotest; +open Util; + +let tests = ( + "ListUtil", + [ + Alcotest.test_case( + "rev_if with false", + `Quick, + () => { + let xs = [1, 2, 3]; + check(list(int), "Same list", ListUtil.rev_if(false, xs), xs); + }, + ), + Alcotest.test_case( + "rev_if with true", + `Quick, + () => { + let xs = [1, 2, 3]; + check( + list(int), + "Reversed list", + ListUtil.rev_if(true, xs), + [3, 2, 1], + ); + }, + ), + ], +); diff --git a/test/haz3ltest.re b/test/haz3ltest.re index e405fba7b8..fbef084c43 100644 --- a/test/haz3ltest.re +++ b/test/haz3ltest.re @@ -3,7 +3,10 @@ open Junit_alcotest; let (suite, _) = run_and_report( ~and_exit=false, - "Dynamics", - [("Elaboration", Test_Elaboration.elaboration_tests)], + "HazelTests", + [ + ("Elaboration", Test_Elaboration.elaboration_tests), + Test_ListUtil.tests, + ], ); Junit.to_file(Junit.make([suite]), "junit_tests.xml"); From 0990af40c2d63c3d57ea602ee24efdaf66c0d3ab Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sat, 10 Aug 2024 13:49:46 -0400 Subject: [PATCH 02/23] Mas tests --- src/util/ListUtil.re | 2 ++ test/Test_ListUtil.re | 41 +++++++++++++++++++++++++++++++++++++++-- 2 files changed, 41 insertions(+), 2 deletions(-) diff --git a/src/util/ListUtil.re b/src/util/ListUtil.re index 9c6bed90b0..f01a5c1af1 100644 --- a/src/util/ListUtil.re +++ b/src/util/ListUtil.re @@ -1,5 +1,6 @@ let rev_if = (b: bool) => b ? List.rev : Fun.id; +// TODO: Replace with dedup_f((==)); let dedup = xs => List.fold_right( (x, deduped) => List.mem(x, deduped) ? deduped : [x, ...deduped], @@ -14,6 +15,7 @@ let dedup_f = (f, xs) => [], ); +// TODO: Rename is_unique? let are_duplicates = xs => List.length(List.sort_uniq(compare, xs)) == List.length(xs); diff --git a/test/Test_ListUtil.re b/test/Test_ListUtil.re index 76881fcb75..57ad521c7b 100644 --- a/test/Test_ListUtil.re +++ b/test/Test_ListUtil.re @@ -9,7 +9,7 @@ let tests = ( `Quick, () => { let xs = [1, 2, 3]; - check(list(int), "Same list", ListUtil.rev_if(false, xs), xs); + check(list(int), "Same list", xs, ListUtil.rev_if(false, xs)); }, ), Alcotest.test_case( @@ -20,10 +20,47 @@ let tests = ( check( list(int), "Reversed list", - ListUtil.rev_if(true, xs), [3, 2, 1], + ListUtil.rev_if(true, xs), ); }, ), + Alcotest.test_case( + "dedup", + `Quick, + () => { + let xs = [1, 2, 3, 2]; + check(list(int), "Unique list", [1, 3, 2], ListUtil.dedup(xs)); // TODO: Interesting the order here is messed up because of fold_right + }, + ), + Alcotest.test_case( + "dedup_f", + `Quick, + () => { + let xs = [1, 2, 3, 2]; + check( + list(int), + "Unique list", + [1, 3, 2], + ListUtil.dedup_f((==), xs), + ); // TODO: Interesting the order here is messed up because of fold_right + }, + ), + Alcotest.test_case( + "are_duplicates has duplicates", + `Quick, + () => { + let xs = [1, 2, 3, 2]; + check(bool, "Returns false", false, ListUtil.are_duplicates(xs)); // TODO: Interesting the order here is messed up because of fold_right + }, + ), + Alcotest.test_case( + "are_duplicates has no duplicates", + `Quick, + () => { + let xs = [1, 2, 3]; + check(bool, "Returns true", true, ListUtil.are_duplicates(xs)); // TODO: Interesting the order here is messed up because of fold_right + }, + ), ], ); From 1ad604f2247ec43ee5eaf91674976a1c5f31ea74 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sat, 10 Aug 2024 21:22:37 -0400 Subject: [PATCH 03/23] Tests --- src/util/ListUtil.re | 3 +- test/Test_ListUtil.re | 114 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 116 insertions(+), 1 deletion(-) diff --git a/src/util/ListUtil.re b/src/util/ListUtil.re index f01a5c1af1..7deb4d41d8 100644 --- a/src/util/ListUtil.re +++ b/src/util/ListUtil.re @@ -19,6 +19,7 @@ let dedup_f = (f, xs) => let are_duplicates = xs => List.length(List.sort_uniq(compare, xs)) == List.length(xs); +// TODO Interesting that this reverses the list inside the groups let group_by = (key: 'x => 'k, xs: list('x)): list(('k, list('x))) => List.fold_left( (grouped, x) => { @@ -34,7 +35,7 @@ let group_by = (key: 'x => 'k, xs: list('x)): list(('k, list('x))) => xs, ); -let rec range = (~lo=0, hi) => +let rec range = (~lo: int=0, hi: int) => if (lo > hi) { raise(Invalid_argument("ListUtil.range")); } else if (lo == hi) { diff --git a/test/Test_ListUtil.re b/test/Test_ListUtil.re index 57ad521c7b..7714342b8c 100644 --- a/test/Test_ListUtil.re +++ b/test/Test_ListUtil.re @@ -62,5 +62,119 @@ let tests = ( check(bool, "Returns true", true, ListUtil.are_duplicates(xs)); // TODO: Interesting the order here is messed up because of fold_right }, ), + Alcotest.test_case( + "group_by with constant function preserves list", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + list(pair(unit, list(int))), + "singleton group", + [((), List.rev(xs))], + ListUtil.group_by(__ => (), xs), + ); + }, + ), + Alcotest.test_case( + "group_by groups into evens/odds", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + list(pair(int, list(int))), + "odds and evens", + [(1, [5, 3, 1]), (0, [4, 2])], + ListUtil.group_by(x => x mod 2, xs), + ); + }, + ), + Alcotest.test_case("range generates sequential integers [1,6)", `Quick, () => { + check(list(int), "1-5", [1, 2, 3, 4, 5], ListUtil.range(~lo=1, 6)) + }), + Alcotest.test_case("range defaults lower bound to 0", `Quick, () => { + check(list(int), "0-5", [0, 1, 2, 3, 4, 5], ListUtil.range(6)) + }), + Alcotest.test_case("range lo = hi is empty", `Quick, () => { + check(list(int), "empty list", [], ListUtil.range(~lo=1, 1)) + }), + Alcotest.test_case("Invalid range raises error", `Quick, () => { + check_raises( + "Invalid range", + Invalid_argument("ListUtil.range"), + () => { + let _ = ListUtil.range(~lo=2, 1); + (); + }, + ) + }), + Alcotest.test_case( + "mk_frame creates a frame from the beginning", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + pair(list(int), list(int)), + "frame", + ([], xs), + ListUtil.mk_frame(0, xs), + ); + }, + ), + Alcotest.test_case( + "mk_frame creates a frame from the end", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + pair(list(int), list(int)), + "frame", + (List.rev(xs), []), + ListUtil.mk_frame(5, xs), + ); + }, + ), + Alcotest.test_case( + "mk_frame raises when making a frame past the end", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check_raises( + "raises invalid argument", + Invalid_argument("ListUtil.mk_frame"), + () => { + let _ = ListUtil.mk_frame(6, xs); + (); + }, + ); + }, + ), + Alcotest.test_case( + "mk_frame raises when making a frame before the beginning", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check_raises( + "raises invalid argument", + Invalid_argument("ListUtil.mk_frame"), + () => { + let _ = ListUtil.mk_frame(-1, xs); + (); + }, + ); + }, + ), + Alcotest.test_case( + "mk_frame makes a frame splitting the list", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + pair(list(int), list(int)), + "frame", + (List.rev([1, 2, 3]), [4, 5]), + ListUtil.mk_frame(3, xs), + ); + }, + ), ], ); From 2a83a0451ad1581f3d99eaf85015f85de7c06f59 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sat, 10 Aug 2024 22:03:13 -0400 Subject: [PATCH 04/23] Stop qualifying import and even more tests --- test/Test_ListUtil.re | 86 ++++++++++++++++++++++++++++++++++--------- 1 file changed, 69 insertions(+), 17 deletions(-) diff --git a/test/Test_ListUtil.re b/test/Test_ListUtil.re index 7714342b8c..c0618dd6f5 100644 --- a/test/Test_ListUtil.re +++ b/test/Test_ListUtil.re @@ -4,7 +4,7 @@ open Util; let tests = ( "ListUtil", [ - Alcotest.test_case( + test_case( "rev_if with false", `Quick, () => { @@ -12,7 +12,7 @@ let tests = ( check(list(int), "Same list", xs, ListUtil.rev_if(false, xs)); }, ), - Alcotest.test_case( + test_case( "rev_if with true", `Quick, () => { @@ -25,7 +25,7 @@ let tests = ( ); }, ), - Alcotest.test_case( + test_case( "dedup", `Quick, () => { @@ -33,7 +33,7 @@ let tests = ( check(list(int), "Unique list", [1, 3, 2], ListUtil.dedup(xs)); // TODO: Interesting the order here is messed up because of fold_right }, ), - Alcotest.test_case( + test_case( "dedup_f", `Quick, () => { @@ -46,7 +46,7 @@ let tests = ( ); // TODO: Interesting the order here is messed up because of fold_right }, ), - Alcotest.test_case( + test_case( "are_duplicates has duplicates", `Quick, () => { @@ -54,7 +54,7 @@ let tests = ( check(bool, "Returns false", false, ListUtil.are_duplicates(xs)); // TODO: Interesting the order here is messed up because of fold_right }, ), - Alcotest.test_case( + test_case( "are_duplicates has no duplicates", `Quick, () => { @@ -62,7 +62,7 @@ let tests = ( check(bool, "Returns true", true, ListUtil.are_duplicates(xs)); // TODO: Interesting the order here is messed up because of fold_right }, ), - Alcotest.test_case( + test_case( "group_by with constant function preserves list", `Quick, () => { @@ -75,7 +75,7 @@ let tests = ( ); }, ), - Alcotest.test_case( + test_case( "group_by groups into evens/odds", `Quick, () => { @@ -88,16 +88,16 @@ let tests = ( ); }, ), - Alcotest.test_case("range generates sequential integers [1,6)", `Quick, () => { + test_case("range generates sequential integers [1,6)", `Quick, () => { check(list(int), "1-5", [1, 2, 3, 4, 5], ListUtil.range(~lo=1, 6)) }), - Alcotest.test_case("range defaults lower bound to 0", `Quick, () => { + test_case("range defaults lower bound to 0", `Quick, () => { check(list(int), "0-5", [0, 1, 2, 3, 4, 5], ListUtil.range(6)) }), - Alcotest.test_case("range lo = hi is empty", `Quick, () => { + test_case("range lo = hi is empty", `Quick, () => { check(list(int), "empty list", [], ListUtil.range(~lo=1, 1)) }), - Alcotest.test_case("Invalid range raises error", `Quick, () => { + test_case("Invalid range raises error", `Quick, () => { check_raises( "Invalid range", Invalid_argument("ListUtil.range"), @@ -107,7 +107,7 @@ let tests = ( }, ) }), - Alcotest.test_case( + test_case( "mk_frame creates a frame from the beginning", `Quick, () => { @@ -120,7 +120,7 @@ let tests = ( ); }, ), - Alcotest.test_case( + test_case( "mk_frame creates a frame from the end", `Quick, () => { @@ -133,7 +133,7 @@ let tests = ( ); }, ), - Alcotest.test_case( + test_case( "mk_frame raises when making a frame past the end", `Quick, () => { @@ -148,7 +148,7 @@ let tests = ( ); }, ), - Alcotest.test_case( + test_case( "mk_frame raises when making a frame before the beginning", `Quick, () => { @@ -163,7 +163,7 @@ let tests = ( ); }, ), - Alcotest.test_case( + test_case( "mk_frame makes a frame splitting the list", `Quick, () => { @@ -176,5 +176,57 @@ let tests = ( ); }, ), + test_case( + "mk_frame makes a frame splitting the list", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + pair(list(int), list(int)), + "frame", + (List.rev([1, 2, 3]), [4, 5]), + ListUtil.mk_frame(3, xs), + ); + }, + ), + test_case( + "split with no found element returns the original list", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + triple(list(int), option(int), list(int)), + "split", + (xs, None, []), + ListUtil.split(xs, __ => false), + ); + }, + ), + test_case( + "split with first found returns the head and tail", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + triple(list(int), option(int), list(int)), + "split", + ([], Some(1), [2, 3, 4, 5]), + ListUtil.split(xs, __ => true), + ); + }, + ), + test_case( + "splits on the middle element", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + triple(list(int), option(int), list(int)), + "split", + ([1, 2], Some(3), [4, 5]), + ListUtil.split(xs, (==)(3)), + ); + }, + ), ], ); From 701bf5c07d755c21fbcfdd78a4279679cf8b2c35 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Tue, 13 Aug 2024 14:47:51 -0400 Subject: [PATCH 05/23] Another test --- test/Test_ListUtil.re | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/test/Test_ListUtil.re b/test/Test_ListUtil.re index c0618dd6f5..bb22b4fe1c 100644 --- a/test/Test_ListUtil.re +++ b/test/Test_ListUtil.re @@ -228,5 +228,29 @@ let tests = ( ); }, ), + test_case( + "combine_opt", + `Quick, + () => { + check( + option(list(pair(string, int))), + "Same size lists", + Some([("a", 1), ("b", 2), ("c", 3)]), + ListUtil.combine_opt(["a", "b", "c"], [1, 2, 3]), + ); + check( + option(list(pair(string, int))), + "Empty Lists", + Some([]), + ListUtil.combine_opt([], []), + ); + check( + option(list(pair(string, int))), + "Inconsistent size lists", + None, + ListUtil.combine_opt(["a"], [1, 2]), + ); + }, + ), ], ); From 4a7570e29b8f11dc92c6a473d252b8980ae0a8a1 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sat, 17 Aug 2024 15:38:18 -0400 Subject: [PATCH 06/23] Additional tests --- test/Test_ListUtil.re | 48 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) diff --git a/test/Test_ListUtil.re b/test/Test_ListUtil.re index bb22b4fe1c..4a3c0f519e 100644 --- a/test/Test_ListUtil.re +++ b/test/Test_ListUtil.re @@ -252,5 +252,53 @@ let tests = ( ); }, ), + test_case( + "is_empty with empty list", + `Quick, + () => { + let xs = []; + check(bool, "Returns true", true, ListUtil.is_empty(xs)); + }, + ), + test_case( + "is_empty with non-empty list", + `Quick, + () => { + let xs = [1, 2, 3]; + check(bool, "Returns false", false, ListUtil.is_empty(xs)); + }, + ), + test_case( + "flat_map with empty list", + `Quick, + () => { + let xs = []; + let f = x => [x, x]; + check(list(int), "Empty list", [], ListUtil.flat_map(f, xs)); + }, + ), + test_case( + "flat_map with non-empty list", + `Quick, + () => { + let xs = [1, 2, 3]; + let f = x => [x, x]; + check( + list(int), + "Doubled list", + [1, 1, 2, 2, 3, 3], + ListUtil.flat_map(f, xs), + ); + }, + ), + test_case( + "flat_map with non-empty list and empty result", + `Quick, + () => { + let xs = [1, 2, 3]; + let f = _ => []; + check(list(int), "Empty list", [], ListUtil.flat_map(f, xs)); + }, + ), ], ); From 3e2bc890bed624905e32701d572a34bd460d0cb1 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sat, 17 Aug 2024 15:53:29 -0400 Subject: [PATCH 07/23] Add tests for ListUtil module --- src/util/ListUtil.re | 2 +- test/Test_ListUtil.re | 320 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 321 insertions(+), 1 deletion(-) diff --git a/src/util/ListUtil.re b/src/util/ListUtil.re index 7deb4d41d8..aed1539298 100644 --- a/src/util/ListUtil.re +++ b/src/util/ListUtil.re @@ -174,7 +174,7 @@ let split_sublist_opt = let split_sublist = (i: int, j: int, xs: list('x)): (list('x), list('x), list('x)) => switch (split_sublist_opt(i, j, xs)) { - | None => raise(Invalid_argument("ListUtil.split_sublist")) + | None => raise(Invalid_argument("ListUtil.split_sublist: " ++ string_of_int(i) ++ ", " ++ string_of_int(j))) | Some(r) => r }; let sublist = ((i, j), xs: list('x)): list('x) => { diff --git a/test/Test_ListUtil.re b/test/Test_ListUtil.re index 4a3c0f519e..509fa9f634 100644 --- a/test/Test_ListUtil.re +++ b/test/Test_ListUtil.re @@ -300,5 +300,325 @@ let tests = ( check(list(int), "Empty list", [], ListUtil.flat_map(f, xs)); }, ), + test_case( + "join with empty list", + `Quick, + () => { + let xs = []; + check(list(string), "Empty list", ListUtil.join(",", xs), []); + }, + ), + test_case( + "join with single element list", + `Quick, + () => { + let xs = ["a"]; + check(list(string), "Single element list", ListUtil.join(",", xs), ["a"]); + }, + ), + test_case( + "join with multiple element list", + `Quick, + () => { + let xs = ["a", "b", "c"]; + check( + list(string), + "Multiple element list", + ListUtil.join(",", xs), + ["a", ",", "b", ",", "c"], + ); + }, + ), + test_case( + "hd_opt with empty list", + `Quick, + () => { + let xs = []; + check(option(int), "None", None, ListUtil.hd_opt(xs)); + }, + ), + test_case( + "hd_opt with non-empty list", + `Quick, + () => { + let xs = [1, 2, 3]; + check(option(int), "Some", Some(1), ListUtil.hd_opt(xs)); + }, + ), + test_case( + "nth_opt with empty list", + `Quick, + () => { + let xs = []; + check(option(int), "None", None, ListUtil.nth_opt(0, xs)); + }, + ), + test_case( + "nth_opt with non-empty list", + `Quick, + () => { + let xs = [1, 2, 3]; + check(option(int), "Some", Some(2), ListUtil.nth_opt(1, xs)); + }, + ), + test_case( + "nth_opt with out of bounds index", + `Quick, + () => { + let xs = [1, 2, 3]; + check(option(int), "None", None, ListUtil.nth_opt(3, xs)); + }, + ), + test_case( + "split_n_opt with empty list", + `Quick, + () => { + let xs = []; + check( + option(pair(list(int), list(int))), + "Empty list", + Some(([], [])), + ListUtil.split_n_opt(0, xs), + ); + }, + ), + test_case( + "split_n_opt with non-empty list", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + option(pair(list(int), list(int))), + "Split list", + Some(([1, 2, 3], [4, 5])), + ListUtil.split_n_opt(3, xs), + ); + }, + ), + test_case( + "split_n_opt with out of bounds index", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + option(pair(list(int), list(int))), + "None", + None, + ListUtil.split_n_opt(6, xs), + ); + }, + ), + test_case( + "split_n_opt with zero index", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + option(pair(list(int), list(int))), + "Empty first part", + Some(([], xs)), + ListUtil.split_n_opt(0, xs), + ); + }, + ), + // split_n + test_case( + "split_n with empty list", + `Quick, + () => { + let xs = []; + check( + pair(list(int), list(int)), + "Empty list", + ([], []), + ListUtil.split_n(0, xs), + ); + }, + ), + test_case( + "split_n with non-empty list", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + pair(list(int), list(int)), + "Split list", + ([1, 2, 3], [4, 5]), + ListUtil.split_n(3, xs), + ); + }, + ), + test_case( + "split_n with out of bounds index", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check_raises( + "raises invalid argument", + Invalid_argument("ListUtil.split_n: 6"), + () => { + let _ = ListUtil.split_n(6, xs); + (); + }, + ); + }, + ), + test_case( + "split_n with zero index", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + pair(list(int), list(int)), + "Empty first part", + ([], xs), + ListUtil.split_n(0, xs), + ); + }, + ), + // split_sublist_opt + test_case( + "split_sublist_opt with empty list", + `Quick, + () => { + let xs = []; + check( + option(triple(list(int), list(int), list(int))), + "Empty list", + Some(([], [], [])), + ListUtil.split_sublist_opt(0, 0, xs), + ); + }, + ), + test_case( + "split_sublist_opt with non-empty list", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + option(triple(list(int), list(int), list(int))), + "Split list", + Some(([1, 2], [3, 4], [5])), + ListUtil.split_sublist_opt(2, 4, xs), + ); + }, + ), + test_case( + "split_sublist_opt with out of bounds index", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + option(triple(list(int), list(int), list(int))), + "None", + None, + ListUtil.split_sublist_opt(6, 7, xs), + ); + }, + ), + test_case( + "split_sublist_opt with zero index", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + option(triple(list(int), list(int), list(int))), + "Empty first part", + Some(([], [], xs)), + ListUtil.split_sublist_opt(0, 0, xs), + ); + }, + ), + test_case( + "split_sublist with empty list", + `Quick, + () => { + let xs = []; + check( + triple(list(int), list(int), list(int)), + "Empty list", + ([], [], []), + ListUtil.split_sublist(0, 0, xs), + ); + }, + ), + test_case( + "split_sublist with non-empty list", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + triple(list(int), list(int), list(int)), + "Split list", + ([1, 2], [3, 4], [5]), + ListUtil.split_sublist(2, 4, xs), + ); + }, + ), + test_case( + "split_sublist with out of bounds index", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check_raises( + "raises invalid argument", + Invalid_argument("ListUtil.split_sublist: 6, 7"), + () => { + let _ = ListUtil.split_sublist(6, 7, xs); + (); + }, + ); + }, + ), + test_case( + "split_sublist with zero index", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + triple(list(int), list(int), list(int)), + "Empty first part", + ([], [], xs), + ListUtil.split_sublist(0, 0, xs), + ); + }, + ), + //sublist + test_case( + "sublist with empty list", + `Quick, + () => { + let xs = []; + check(list(int), "Empty list", [], ListUtil.sublist((0, 0), xs)); + }, + ), + test_case( + "sublist with non-empty list", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + list(int), + "Sublist", + [2, 3, 4], + ListUtil.sublist((1, 4), xs), + ); + }, + ), + test_case( + "sublist with out of bounds index", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check_raises( + "raises invalid argument", + Invalid_argument("ListUtil.split_sublist: 6, 7"), + () => { + let _ = ListUtil.sublist((6, 7), xs); + (); + }, + ); + }, + ), ], ); From 0826944e3a8663ea9f05aa5c8cd39ec3c43e17fe Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sat, 17 Aug 2024 16:00:30 -0400 Subject: [PATCH 08/23] Formatting --- src/util/ListUtil.re | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/util/ListUtil.re b/src/util/ListUtil.re index aed1539298..f7162e5ace 100644 --- a/src/util/ListUtil.re +++ b/src/util/ListUtil.re @@ -174,7 +174,15 @@ let split_sublist_opt = let split_sublist = (i: int, j: int, xs: list('x)): (list('x), list('x), list('x)) => switch (split_sublist_opt(i, j, xs)) { - | None => raise(Invalid_argument("ListUtil.split_sublist: " ++ string_of_int(i) ++ ", " ++ string_of_int(j))) + | None => + raise( + Invalid_argument( + "ListUtil.split_sublist: " + ++ string_of_int(i) + ++ ", " + ++ string_of_int(j), + ), + ) | Some(r) => r }; let sublist = ((i, j), xs: list('x)): list('x) => { From db7eb961a3fe31fcc009426f4defc80aa571a436 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sat, 17 Aug 2024 16:10:10 -0400 Subject: [PATCH 09/23] Remove comments --- test/Test_ListUtil.re | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/test/Test_ListUtil.re b/test/Test_ListUtil.re index 509fa9f634..a21ef071d7 100644 --- a/test/Test_ListUtil.re +++ b/test/Test_ListUtil.re @@ -313,7 +313,12 @@ let tests = ( `Quick, () => { let xs = ["a"]; - check(list(string), "Single element list", ListUtil.join(",", xs), ["a"]); + check( + list(string), + "Single element list", + ListUtil.join(",", xs), + ["a"], + ); }, ), test_case( @@ -421,7 +426,6 @@ let tests = ( ); }, ), - // split_n test_case( "split_n with empty list", `Quick, @@ -476,7 +480,6 @@ let tests = ( ); }, ), - // split_sublist_opt test_case( "split_sublist_opt with empty list", `Quick, @@ -583,7 +586,6 @@ let tests = ( ); }, ), - //sublist test_case( "sublist with empty list", `Quick, From 1cddc4ef668d895189cbe171f436cd8f48631d9b Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Mon, 19 Aug 2024 11:41:54 -0400 Subject: [PATCH 10/23] TODOne --- src/util/ListUtil.re | 26 ++++++++++++++++---------- 1 file changed, 16 insertions(+), 10 deletions(-) diff --git a/src/util/ListUtil.re b/src/util/ListUtil.re index f7162e5ace..d2c9a4bbef 100644 --- a/src/util/ListUtil.re +++ b/src/util/ListUtil.re @@ -1,13 +1,5 @@ let rev_if = (b: bool) => b ? List.rev : Fun.id; -// TODO: Replace with dedup_f((==)); -let dedup = xs => - List.fold_right( - (x, deduped) => List.mem(x, deduped) ? deduped : [x, ...deduped], - xs, - [], - ); - let dedup_f = (f, xs) => List.fold_right( (x, deduped) => List.exists(f(x), deduped) ? deduped : [x, ...deduped], @@ -15,11 +7,25 @@ let dedup_f = (f, xs) => [], ); -// TODO: Rename is_unique? +let dedup = xs => dedup_f((==), xs); + let are_duplicates = xs => List.length(List.sort_uniq(compare, xs)) == List.length(xs); -// TODO Interesting that this reverses the list inside the groups +/** + Groups elements of a list by a specified key. + + {b Note: The groups are not guaranteed to preserve the order of elements from the original list. } + + @param key + The key function used to determine the grouping key. + + @param xs + The list of elements to be grouped. + + @return + A list of tuples where each tuple contains the grouping key and a list of elements that belong to that group. +*/ let group_by = (key: 'x => 'k, xs: list('x)): list(('k, list('x))) => List.fold_left( (grouped, x) => { From b93ba919be6fba07adaa53acf1f4255a8260ae4c Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Mon, 19 Aug 2024 11:56:30 -0400 Subject: [PATCH 11/23] Remove unnecessary whitespace in ListUtil.re --- src/util/ListUtil.re | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/ListUtil.re b/src/util/ListUtil.re index d2c9a4bbef..39a2d5994e 100644 --- a/src/util/ListUtil.re +++ b/src/util/ListUtil.re @@ -16,7 +16,7 @@ let are_duplicates = xs => Groups elements of a list by a specified key. {b Note: The groups are not guaranteed to preserve the order of elements from the original list. } - + @param key The key function used to determine the grouping key. From 2eddbdc1696ef48e16c9424abc627fbd850a4415 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Mon, 19 Aug 2024 12:01:45 -0400 Subject: [PATCH 12/23] Remove comment --- test/Test_ListUtil.re | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/Test_ListUtil.re b/test/Test_ListUtil.re index a21ef071d7..017c2e6d96 100644 --- a/test/Test_ListUtil.re +++ b/test/Test_ListUtil.re @@ -59,7 +59,7 @@ let tests = ( `Quick, () => { let xs = [1, 2, 3]; - check(bool, "Returns true", true, ListUtil.are_duplicates(xs)); // TODO: Interesting the order here is messed up because of fold_right + check(bool, "Returns true", true, ListUtil.are_duplicates(xs)); }, ), test_case( From fb5b2eb71a67899338f447a8879e91d65a76c0f5 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Fri, 23 Aug 2024 16:48:22 -0400 Subject: [PATCH 13/23] Removed are_duplicates --- src/util/ListUtil.re | 3 --- test/Test_ListUtil.re | 16 ---------------- 2 files changed, 19 deletions(-) diff --git a/src/util/ListUtil.re b/src/util/ListUtil.re index 39a2d5994e..8481df4f0a 100644 --- a/src/util/ListUtil.re +++ b/src/util/ListUtil.re @@ -9,9 +9,6 @@ let dedup_f = (f, xs) => let dedup = xs => dedup_f((==), xs); -let are_duplicates = xs => - List.length(List.sort_uniq(compare, xs)) == List.length(xs); - /** Groups elements of a list by a specified key. diff --git a/test/Test_ListUtil.re b/test/Test_ListUtil.re index 017c2e6d96..9abfca4f07 100644 --- a/test/Test_ListUtil.re +++ b/test/Test_ListUtil.re @@ -46,22 +46,6 @@ let tests = ( ); // TODO: Interesting the order here is messed up because of fold_right }, ), - test_case( - "are_duplicates has duplicates", - `Quick, - () => { - let xs = [1, 2, 3, 2]; - check(bool, "Returns false", false, ListUtil.are_duplicates(xs)); // TODO: Interesting the order here is messed up because of fold_right - }, - ), - test_case( - "are_duplicates has no duplicates", - `Quick, - () => { - let xs = [1, 2, 3]; - check(bool, "Returns true", true, ListUtil.are_duplicates(xs)); - }, - ), test_case( "group_by with constant function preserves list", `Quick, From 9e5570a352f7ba08ea2d02078a124e40822f421e Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Tue, 1 Oct 2024 13:25:55 -0400 Subject: [PATCH 14/23] Potentially fix deferrals --- src/haz3lcore/dynamics/Elaborator.re | 5 +++ src/haz3lcore/dynamics/Transition.re | 21 ++++++++----- test/Test_Evaluator.re | 46 ++++++++++++++++++---------- 3 files changed, 48 insertions(+), 24 deletions(-) diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re index c1f3aa12d7..0f2287bef4 100644 --- a/src/haz3lcore/dynamics/Elaborator.re +++ b/src/haz3lcore/dynamics/Elaborator.re @@ -350,6 +350,11 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { ((arg, _)) => Exp.is_deferral(arg), List.combine(args, ty_fargs), ); + // TODO Should this be a product in the singleton case or not + // let remaining_arg_ty = + // List.length(remaining_args) == 1 + // ? snd(List.hd(remaining_args)) + // : Prod(List.map(snd, remaining_args)) |> Typ.temp; let remaining_arg_ty = Prod(List.map(snd, remaining_args)) |> Typ.temp; DeferredAp(f'', args'') |> rewrap diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re index a54c9d18d8..6a17a78d2f 100644 --- a/src/haz3lcore/dynamics/Transition.re +++ b/src/haz3lcore/dynamics/Transition.re @@ -333,9 +333,10 @@ module Transition = (EV: EV_MODE) => { ); Constructor; | Ap(dir, d1, d2) => + // TODO I don't know why this needs to be final let. _ = otherwise(env, (d1, (d2, _)) => Ap(dir, d1, d2) |> rewrap) and. d1' = - req_value(req(state, env), d1 => Ap1(dir, d1, d2) |> wrap_ctx, d1) + req_final(req(state, env), d1 => Ap1(dir, d1, d2) |> wrap_ctx, d1) and. (d2', d2_is_value) = req_final_or_value( req(state, env), @@ -396,14 +397,22 @@ module Transition = (EV: EV_MODE) => { | DeferredAp(d3, d4s) => let n_args = List.length( - List.map( + List.filter( fun | {term: Deferral(_), _} => true | _ => false: Exp.t => bool, d4s, ), ); - let-unbox args = (Tuple(n_args), d2); + let-unbox args = + if (n_args == 1) { + ( + Tuple(n_args), + Tuple([d2]) |> fresh // TODO Should we not be going to a tuple? + ); + } else { + (Tuple(n_args), d2); + }; let new_args = { let rec go = (deferred, args) => switch ((deferred: list(Exp.t))) { @@ -424,11 +433,7 @@ module Transition = (EV: EV_MODE) => { }); | Cast(_) | FailedCast(_) => Indet - | FixF(_) => - print_endline(Exp.show(d1)); - print_endline(Exp.show(d1')); - print_endline("FIXF"); - failwith("FixF in Ap"); + | FixF(_) => failwith("FixF in Ap") | _ => Step({ expr: { diff --git a/test/Test_Evaluator.re b/test/Test_Evaluator.re index fc159425b2..c6417b5737 100644 --- a/test/Test_Evaluator.re +++ b/test/Test_Evaluator.re @@ -2,22 +2,6 @@ open Alcotest; open Haz3lcore; let dhexp_typ = testable(Fmt.using(Exp.show, Fmt.string), DHExp.fast_equal); -let ids = List.init(12, _ => Id.mk()); -let id_at = x => x |> List.nth(ids); -let statics = Statics.mk(CoreSettings.on, Builtins.ctx_init); - -// Get the type from the statics -let type_of = f => { - let s = statics(f); - switch (Id.Map.find(IdTagged.rep_id(f), s)) { - | InfoExp({ty, _}) => Some(ty) - | _ => None - }; -}; - -let int_evaluation = - Evaluator.evaluate(Builtins.env_init, {d: Exp.Int(8) |> Exp.fresh}); - let evaluation_test = (msg, expected, unevaluated) => check( dhexp_typ, @@ -38,7 +22,37 @@ let test_sum = () => BinOp(Int(Plus), Int(4) |> Exp.fresh, Int(5) |> Exp.fresh) |> Exp.fresh, ); +let test_function_application = () => + evaluation_test( + "float_of_int(1)", + Float(1.0) |> Exp.fresh, + Ap(Forward, Var("float_of_int") |> Exp.fresh, Int(1) |> Exp.fresh) + |> Exp.fresh, + ); + +let test_function_deferral = () => + evaluation_test( + "string_sub(\"hello\", 1, _)(2)", + String("el") |> Exp.fresh, + Ap( + Forward, + DeferredAp( + Var("string_sub") |> Exp.fresh, + [ + String("hello") |> Exp.fresh, + Int(1) |> Exp.fresh, + Deferral(InAp) |> Exp.fresh, + ], + ) + |> Exp.fresh, + Int(2) |> Exp.fresh, + ) + |> Exp.fresh, + ); + let tests = [ test_case("Integer literal", `Quick, test_int), test_case("Integer sum", `Quick, test_sum), + test_case("Function application", `Quick, test_function_application), + test_case("Function deferral", `Quick, test_function_deferral), ]; From 50440ea2ab3d92f4790b8f8711d9bfc9a31122de Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Wed, 2 Oct 2024 09:33:19 -0400 Subject: [PATCH 15/23] Fix function deferral for when there's a single remaining argument --- src/haz3lcore/dynamics/Elaborator.re | 10 +++---- src/haz3lcore/dynamics/Transition.re | 7 +++-- test/Test_Elaboration.re | 40 +++++++++++++++++++++++++++- 3 files changed, 48 insertions(+), 9 deletions(-) diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re index 0f2287bef4..bdc5baf621 100644 --- a/src/haz3lcore/dynamics/Elaborator.re +++ b/src/haz3lcore/dynamics/Elaborator.re @@ -350,12 +350,10 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { ((arg, _)) => Exp.is_deferral(arg), List.combine(args, ty_fargs), ); - // TODO Should this be a product in the singleton case or not - // let remaining_arg_ty = - // List.length(remaining_args) == 1 - // ? snd(List.hd(remaining_args)) - // : Prod(List.map(snd, remaining_args)) |> Typ.temp; - let remaining_arg_ty = Prod(List.map(snd, remaining_args)) |> Typ.temp; + let remaining_arg_ty = + List.length(remaining_args) == 1 + ? snd(List.hd(remaining_args)) + : Prod(List.map(snd, remaining_args)) |> Typ.temp; DeferredAp(f'', args'') |> rewrap |> cast_from(Arrow(remaining_arg_ty, tyf2) |> Typ.temp); diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re index 6a17a78d2f..e0c278d2b7 100644 --- a/src/haz3lcore/dynamics/Transition.re +++ b/src/haz3lcore/dynamics/Transition.re @@ -333,7 +333,6 @@ module Transition = (EV: EV_MODE) => { ); Constructor; | Ap(dir, d1, d2) => - // TODO I don't know why this needs to be final let. _ = otherwise(env, (d1, (d2, _)) => Ap(dir, d1, d2) |> rewrap) and. d1' = req_final(req(state, env), d1 => Ap1(dir, d1, d2) |> wrap_ctx, d1) @@ -433,7 +432,11 @@ module Transition = (EV: EV_MODE) => { }); | Cast(_) | FailedCast(_) => Indet - | FixF(_) => failwith("FixF in Ap") + | FixF(_) => + print_endline(Exp.show(d1)); + print_endline(Exp.show(d1')); + print_endline("FIXF"); + failwith("FixF in Ap"); | _ => Step({ expr: { diff --git a/test/Test_Elaboration.re b/test/Test_Elaboration.re index 2516f25227..d5d25d9334 100644 --- a/test/Test_Elaboration.re +++ b/test/Test_Elaboration.re @@ -180,6 +180,15 @@ let let_fun = () => let deferral = () => alco_check( "string_sub(\"hello\", 1, _)", + DeferredAp( + Var("string_sub") |> Exp.fresh, + [ + String("hello") |> Exp.fresh, + Int(1) |> Exp.fresh, + Deferral(InAp) |> Exp.fresh, + ], + ) + |> Exp.fresh, dhexp_of_uexp( DeferredAp( Var("string_sub") |> Exp.fresh, @@ -191,7 +200,13 @@ let deferral = () => ) |> Exp.fresh, ), - dhexp_of_uexp( + ); + +let ap_deferral_single_argument = () => + alco_check( + "string_sub(\"hello\", 1, _)(2)", + Ap( + Forward, DeferredAp( Var("string_sub") |> Exp.fresh, [ @@ -201,6 +216,24 @@ let deferral = () => ], ) |> Exp.fresh, + Int(2) |> Exp.fresh, + ) + |> Exp.fresh, + dhexp_of_uexp( + Ap( + Forward, + DeferredAp( + Var("string_sub") |> Exp.fresh, + [ + String("hello") |> Exp.fresh, + Int(1) |> Exp.fresh, + Deferral(InAp) |> Exp.fresh, + ], + ) + |> Exp.fresh, + Int(2) |> Exp.fresh, + ) + |> Exp.fresh, ), ); @@ -220,4 +253,9 @@ let elaboration_tests = [ `Quick, deferral, ), + test_case( + "Function application with a single remaining argument after deferral", + `Quick, + ap_deferral_single_argument, + ), ]; From 666b137ba0a9ddc5e9655a0de95184b3fdf847b8 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 3 Oct 2024 09:47:28 -0400 Subject: [PATCH 16/23] Make DeferredAp a Value --- src/haz3lcore/dynamics/Evaluator.re | 1 + src/haz3lcore/dynamics/EvaluatorStep.re | 2 ++ src/haz3lcore/dynamics/Transition.re | 5 +++-- src/haz3lcore/dynamics/ValueChecker.re | 1 + 4 files changed, 7 insertions(+), 2 deletions(-) diff --git a/src/haz3lcore/dynamics/Evaluator.re b/src/haz3lcore/dynamics/Evaluator.re index fb877accd7..628b493e1d 100644 --- a/src/haz3lcore/dynamics/Evaluator.re +++ b/src/haz3lcore/dynamics/Evaluator.re @@ -118,6 +118,7 @@ module EvaluatorEVMode: { | (BoxedReady, Constructor) => (BoxedValue, c) | (IndetReady, Constructor) => (Indet, c) | (IndetBlocked, _) => (Indet, c) + | (_, Value) => (BoxedValue, c) | (_, Indet) => (Indet, c) }; }; diff --git a/src/haz3lcore/dynamics/EvaluatorStep.re b/src/haz3lcore/dynamics/EvaluatorStep.re index f25f25603f..0882fa223f 100644 --- a/src/haz3lcore/dynamics/EvaluatorStep.re +++ b/src/haz3lcore/dynamics/EvaluatorStep.re @@ -136,6 +136,7 @@ module Decompose = { | (undo, Result.BoxedValue, env, v) => switch (rl(v)) { | Constructor => Result.BoxedValue + | Value => Result.BoxedValue | Indet => Result.Indet | Step(s) => Result.Step([EvalObj.mk(Mark, env, undo, s.kind)]) // TODO: Actually show these exceptions to the user! @@ -187,6 +188,7 @@ module TakeStep = { state_update(); Some(expr); | Constructor + | Value | Indet => None }; diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re index e0c278d2b7..d6b9fa7825 100644 --- a/src/haz3lcore/dynamics/Transition.re +++ b/src/haz3lcore/dynamics/Transition.re @@ -91,7 +91,8 @@ type rule = is_value: bool, }) | Constructor - | Indet; + | Indet + | Value; let (let-unbox) = ((request, v), f) => switch (Unboxing.unbox(request, v)) { @@ -331,7 +332,7 @@ module Transition = (EV: EV_MODE) => { (d2, ds) => DeferredAp2(d1, d2, ds) |> wrap_ctx, ds, ); - Constructor; + Value; | Ap(dir, d1, d2) => let. _ = otherwise(env, (d1, (d2, _)) => Ap(dir, d1, d2) |> rewrap) and. d1' = diff --git a/src/haz3lcore/dynamics/ValueChecker.re b/src/haz3lcore/dynamics/ValueChecker.re index 39f43daeed..c99a90db6f 100644 --- a/src/haz3lcore/dynamics/ValueChecker.re +++ b/src/haz3lcore/dynamics/ValueChecker.re @@ -69,6 +69,7 @@ module ValueCheckerEVMode: { | (_, _, Constructor) => r | (_, Expr, Indet) => Expr | (_, _, Indet) => Indet + | (_, _, Value) => Value | (true, _, Step(_)) => Expr | (false, _, Step(_)) => r }; From ab9f98182f2b097af4fdde616309a5e7db43c61c Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 3 Oct 2024 10:05:59 -0400 Subject: [PATCH 17/23] Remove invalid comment --- src/haz3lcore/dynamics/Transition.re | 1 - 1 file changed, 1 deletion(-) diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re index d6b9fa7825..7a9e8f16bf 100644 --- a/src/haz3lcore/dynamics/Transition.re +++ b/src/haz3lcore/dynamics/Transition.re @@ -393,7 +393,6 @@ module Transition = (EV: EV_MODE) => { } else { Indet; } - /* This case isn't currently used because deferrals are elaborated away */ | DeferredAp(d3, d4s) => let n_args = List.length( From 8d4ead15c678f20ef494ee1508bd00e5fa213a05 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 3 Oct 2024 10:39:20 -0400 Subject: [PATCH 18/23] Add elavorator and evaluator tests for deferral applied to a hole --- test/Test_Elaboration.re | 87 ++++++++++++++++++++++++++++++ test/Test_Evaluator.re | 111 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 198 insertions(+) diff --git a/test/Test_Elaboration.re b/test/Test_Elaboration.re index d5d25d9334..c515487535 100644 --- a/test/Test_Elaboration.re +++ b/test/Test_Elaboration.re @@ -237,6 +237,88 @@ let ap_deferral_single_argument = () => ), ); +let ap_of_deferral_of_hole = () => + alco_check( + "?(_, _, 3)(1., true)", + Ap( + Forward, + DeferredAp( + Cast( + Cast( + EmptyHole |> Exp.fresh, + Unknown(Internal) |> Typ.fresh, + Arrow( + Unknown(Internal) |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Typ.fresh, + ) + |> Exp.fresh, + Arrow( + Unknown(Internal) |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Typ.fresh, + Arrow( + Prod([ + Unknown(Internal) |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ]) + |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Typ.fresh, + ) + |> Exp.fresh, + [ + Deferral(InAp) |> Exp.fresh, + Deferral(InAp) |> Exp.fresh, + Cast( + Int(3) |> Exp.fresh, + Int |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + ], + ) + |> Exp.fresh, + Tuple([ + Cast( + Float(1.) |> Exp.fresh, + Float |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + Cast( + Bool(true) |> Exp.fresh, + Bool |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + ]) + |> Exp.fresh, + ) + |> Exp.fresh, + dhexp_of_uexp( + Ap( + Forward, + DeferredAp( + EmptyHole |> Exp.fresh, + [ + Deferral(InAp) |> Exp.fresh, + Deferral(InAp) |> Exp.fresh, + Int(3) |> Exp.fresh, + ], + ) + |> Exp.fresh, + Tuple([Float(1.) |> Exp.fresh, Bool(true) |> Exp.fresh]) + |> Exp.fresh, + ) + |> Exp.fresh, + ), + ); + let elaboration_tests = [ test_case("Single integer", `Quick, single_integer), test_case("Empty hole", `Quick, empty_hole), @@ -258,4 +340,9 @@ let elaboration_tests = [ `Quick, ap_deferral_single_argument, ), + test_case( + "Function application with a deferral of a hole", + `Quick, + ap_of_deferral_of_hole, + ), ]; diff --git a/test/Test_Evaluator.re b/test/Test_Evaluator.re index c6417b5737..ca85062226 100644 --- a/test/Test_Evaluator.re +++ b/test/Test_Evaluator.re @@ -50,9 +50,120 @@ let test_function_deferral = () => |> Exp.fresh, ); +let tet_ap_of_hole_deferral = () => + evaluation_test( + "?(_, _, 3)(1., true)", + Ap( + Forward, + Cast( + EmptyHole |> Exp.fresh, + Unknown(Internal) |> Typ.fresh, + Arrow( + Unknown(Internal) |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Typ.fresh, + ) + |> Exp.fresh, + Cast( + Tuple([ + Cast( + Float(1.) |> Exp.fresh, + Float |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + Cast( + Bool(true) |> Exp.fresh, + Bool |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + Cast( + Int(3) |> Exp.fresh, + Int |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + ]) + |> Exp.fresh, + Prod([ + Unknown(Internal) |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ]) + |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + ) + |> Exp.fresh, + Ap( + Forward, + DeferredAp( + Cast( + Cast( + EmptyHole |> Exp.fresh, + Unknown(Internal) |> Typ.fresh, + Arrow( + Unknown(Internal) |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Typ.fresh, + ) + |> Exp.fresh, + Arrow( + Unknown(Internal) |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Typ.fresh, + Arrow( + Prod([ + Unknown(Internal) |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ]) + |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Typ.fresh, + ) + |> Exp.fresh, + [ + Deferral(InAp) |> Exp.fresh, + Deferral(InAp) |> Exp.fresh, + Cast( + Int(3) |> Exp.fresh, + Int |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + ], + ) + |> Exp.fresh, + Tuple([ + Cast( + Float(1.) |> Exp.fresh, + Float |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + Cast( + Bool(true) |> Exp.fresh, + Bool |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + ]) + |> Exp.fresh, + ) + |> Exp.fresh, + ); + let tests = [ test_case("Integer literal", `Quick, test_int), test_case("Integer sum", `Quick, test_sum), test_case("Function application", `Quick, test_function_application), test_case("Function deferral", `Quick, test_function_deferral), + test_case("Deferral applied to hole", `Quick, tet_ap_of_hole_deferral), ]; From 1144e631fb9e26cddfeeb70c1f368a1f262fedac Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Fri, 4 Oct 2024 16:53:22 -0400 Subject: [PATCH 19/23] Switch to req_value --- src/haz3lcore/dynamics/Transition.re | 2 +- test/Test_Evaluator.re | 64 ++++++++++++++++------------ 2 files changed, 37 insertions(+), 29 deletions(-) diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re index 7a9e8f16bf..5c936426b9 100644 --- a/src/haz3lcore/dynamics/Transition.re +++ b/src/haz3lcore/dynamics/Transition.re @@ -336,7 +336,7 @@ module Transition = (EV: EV_MODE) => { | Ap(dir, d1, d2) => let. _ = otherwise(env, (d1, (d2, _)) => Ap(dir, d1, d2) |> rewrap) and. d1' = - req_final(req(state, env), d1 => Ap1(dir, d1, d2) |> wrap_ctx, d1) + req_value(req(state, env), d1 => Ap1(dir, d1, d2) |> wrap_ctx, d1) and. (d2', d2_is_value) = req_final_or_value( req(state, env), diff --git a/test/Test_Evaluator.re b/test/Test_Evaluator.re index ca85062226..37fcaba764 100644 --- a/test/Test_Evaluator.re +++ b/test/Test_Evaluator.re @@ -56,46 +56,54 @@ let tet_ap_of_hole_deferral = () => Ap( Forward, Cast( - EmptyHole |> Exp.fresh, - Unknown(Internal) |> Typ.fresh, + Cast( + EmptyHole |> Exp.fresh, + Unknown(Internal) |> Typ.fresh, + Arrow( + Unknown(Internal) |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Typ.fresh, + ) + |> Exp.fresh, Arrow( Unknown(Internal) |> Typ.fresh, Unknown(Internal) |> Typ.fresh, ) |> Typ.fresh, - ) - |> Exp.fresh, - Cast( - Tuple([ - Cast( - Float(1.) |> Exp.fresh, - Float |> Typ.fresh, + Arrow( + Prod([ Unknown(Internal) |> Typ.fresh, - ) - |> Exp.fresh, - Cast( - Bool(true) |> Exp.fresh, - Bool |> Typ.fresh, Unknown(Internal) |> Typ.fresh, - ) - |> Exp.fresh, - Cast( - Int(3) |> Exp.fresh, - Int |> Typ.fresh, Unknown(Internal) |> Typ.fresh, - ) - |> Exp.fresh, - ]) - |> Exp.fresh, - Prod([ - Unknown(Internal) |> Typ.fresh, - Unknown(Internal) |> Typ.fresh, + ]) + |> Typ.fresh, Unknown(Internal) |> Typ.fresh, - ]) + ) |> Typ.fresh, - Unknown(Internal) |> Typ.fresh, ) |> Exp.fresh, + Tuple([ + Cast( + Float(1.) |> Exp.fresh, + Float |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + Cast( + Bool(true) |> Exp.fresh, + Bool |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + Cast( + Int(3) |> Exp.fresh, + Int |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + ]) + |> Exp.fresh, ) |> Exp.fresh, Ap( From 805b6ea5105d42d25d398b0382b4ee85cbf613a8 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Tue, 8 Oct 2024 13:56:01 -0400 Subject: [PATCH 20/23] Run @ocaml-index as part of building --- Makefile | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Makefile b/Makefile index c1f5943d07..516016ddf8 100644 --- a/Makefile +++ b/Makefile @@ -25,7 +25,7 @@ setup-student: dev-helper: dune fmt --auto-promote || true - dune build @src/fmt --auto-promote src --profile dev + dune build @ocaml-index @src/fmt --auto-promote src --profile dev dev: setup-instructor dev-helper @@ -35,7 +35,7 @@ fmt: dune fmt --auto-promote watch: setup-instructor - dune build @src/fmt --auto-promote src --profile dev --watch + dune build @ocaml-index @src/fmt --auto-promote src --profile dev --watch watch-release: setup-instructor dune build @src/fmt --auto-promote src --profile release --watch @@ -60,11 +60,11 @@ repl: test: dune fmt --auto-promote || true - dune build @src/fmt @test/fmt --auto-promote src test --profile dev + dune build @ocaml-index @src/fmt @test/fmt --auto-promote src test --profile dev node $(TEST_DIR)/haz3ltest.bc.js watch-test: - dune build @fmt @runtest --auto-promote --watch + dune build @ocaml-index @fmt @runtest --auto-promote --watch clean: dune clean From 2003c7607e55a701eeaa4a8387b561bb7bd11f42 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Mon, 7 Oct 2024 10:39:39 -0400 Subject: [PATCH 21/23] Add MakeTerm tests to test regular hazel parsing --- test/Test_MakeTerm.re | 70 +++++++++++++++++++++++++++++++++++++++++++ test/haz3ltest.re | 1 + 2 files changed, 71 insertions(+) create mode 100644 test/Test_MakeTerm.re diff --git a/test/Test_MakeTerm.re b/test/Test_MakeTerm.re new file mode 100644 index 0000000000..82eee683b6 --- /dev/null +++ b/test/Test_MakeTerm.re @@ -0,0 +1,70 @@ +/** + * This file contains tests to validate the `MakeTerm` module's ability to convert + * zippers into expressions. + */ +open Alcotest; +open Haz3lcore; + +let exp_typ = testable(Fmt.using(Exp.show, Fmt.string), Exp.fast_equal); + +// TODO Assertion if it doesn't parse +let parse_exp = (s: string) => + MakeTerm.from_zip_for_sem(Option.get(Printer.zipper_of_string(s))).term; +let exp_check = (expected, actual) => + check(exp_typ, actual, expected, parse_exp(actual)); + +let tests = [ + test_case("Integer Literal", `Quick, () => { + exp_check(Int(0) |> Exp.fresh, "0") + }), + test_case("Empty Hole", `Quick, () => { + exp_check(EmptyHole |> Exp.fresh, "?") + }), + test_case("Free Variable", `Quick, () => { + exp_check(Var("x") |> Exp.fresh, "x") + }), + test_case("Parenthesized Expression", `Quick, () => { + exp_check(Parens(Int(0) |> Exp.fresh) |> Exp.fresh, "(0)") + }), + test_case("Let Expression", `Quick, () => { + exp_check( + Let( + Var("x") |> Pat.fresh, + Int(1) |> Exp.fresh, + Var("x") |> Exp.fresh, + ) + |> Exp.fresh, + "let x = 1 in x", + ) + }), + test_case("Function Application", `Quick, () => { + exp_check( + Ap(Forward, Var("f") |> Exp.fresh, Var("x") |> Exp.fresh) |> Exp.fresh, + "f(x)", + ) + }), + test_case("Named Function Definition", `Quick, () => { + exp_check( + Let( + Var("f") |> Pat.fresh, + Fun(Var("x") |> Pat.fresh, Var("x") |> Exp.fresh, None, None) // It seems as though the function naming happens during elaboration and not during parsing + |> Exp.fresh, + Int(1) |> Exp.fresh, + ) + |> Exp.fresh, + "let f = fun x -> x in 1", + ) + }), + test_case("Incomplete Function Definition", `Quick, () => { + exp_check( + Let( + EmptyHole |> Pat.fresh, + Fun(Var("x") |> Pat.fresh, EmptyHole |> Exp.fresh, None, None) + |> Exp.fresh, + EmptyHole |> Exp.fresh, + ) + |> Exp.fresh, + "let = fun x -> in ", + ) + }), +]; diff --git a/test/haz3ltest.re b/test/haz3ltest.re index 3e13ae44b7..3c6cbb6098 100644 --- a/test/haz3ltest.re +++ b/test/haz3ltest.re @@ -8,6 +8,7 @@ let (suite, _) = ("Elaboration", Test_Elaboration.elaboration_tests), ("Statics", Test_Statics.tests), ("Evaluator", Test_Evaluator.tests), + ("MakeTerm", Test_MakeTerm.tests), ], ); Junit.to_file(Junit.make([suite]), "junit_tests.xml"); From 5b82cae1ac1e4b56487301e85d91b57336bd3526 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sun, 13 Oct 2024 09:54:38 -0400 Subject: [PATCH 22/23] Remove todo --- test/Test_MakeTerm.re | 1 - 1 file changed, 1 deletion(-) diff --git a/test/Test_MakeTerm.re b/test/Test_MakeTerm.re index 82eee683b6..be365e9edb 100644 --- a/test/Test_MakeTerm.re +++ b/test/Test_MakeTerm.re @@ -7,7 +7,6 @@ open Haz3lcore; let exp_typ = testable(Fmt.using(Exp.show, Fmt.string), Exp.fast_equal); -// TODO Assertion if it doesn't parse let parse_exp = (s: string) => MakeTerm.from_zip_for_sem(Option.get(Printer.zipper_of_string(s))).term; let exp_check = (expected, actual) => From bc19bf60845760683588eda83c90013e6459075e Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 24 Oct 2024 10:58:23 -0400 Subject: [PATCH 23/23] Added additional tests --- test/Test_MakeTerm.re | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/test/Test_MakeTerm.re b/test/Test_MakeTerm.re index be365e9edb..46818664a9 100644 --- a/test/Test_MakeTerm.re +++ b/test/Test_MakeTerm.re @@ -66,4 +66,17 @@ let tests = [ "let = fun x -> in ", ) }), + test_case("Constructor", `Quick, () => { + exp_check( + Constructor("A", Unknown(Internal) |> Typ.fresh) |> Exp.fresh, + "A", + ) + }), + test_case("Type Alias", `Quick, () => { + exp_check( + TyAlias(Var("x") |> TPat.fresh, Int |> Typ.fresh, Int(1) |> Exp.fresh) + |> Exp.fresh, + "type x = Int in 1", + ) + }), ];