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 diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re index d50d462064..27ec1ef5b3 100644 --- a/src/haz3lcore/dynamics/Elaborator.re +++ b/src/haz3lcore/dynamics/Elaborator.re @@ -342,7 +342,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), ); - 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/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 a54c9d18d8..5c936426b9 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' = @@ -392,18 +393,25 @@ 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( - 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))) { diff --git a/src/haz3lcore/dynamics/ValueChecker.re b/src/haz3lcore/dynamics/ValueChecker.re index d6af00f4a4..a6e5ab30f0 100644 --- a/src/haz3lcore/dynamics/ValueChecker.re +++ b/src/haz3lcore/dynamics/ValueChecker.re @@ -68,6 +68,7 @@ module ValueCheckerEVMode: { | (_, _, Constructor) => r | (_, Expr, Indet) => Expr | (_, _, Indet) => Indet + | (_, _, Value) => Value | (true, _, Step(_)) => Expr | (false, _, Step(_)) => r }; diff --git a/src/util/ListUtil.re b/src/util/ListUtil.re index 9c6bed90b0..8481df4f0a 100644 --- a/src/util/ListUtil.re +++ b/src/util/ListUtil.re @@ -1,12 +1,5 @@ let rev_if = (b: bool) => b ? List.rev : Fun.id; -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], @@ -14,9 +7,22 @@ let dedup_f = (f, xs) => [], ); -let are_duplicates = xs => - List.length(List.sort_uniq(compare, xs)) == List.length(xs); +let dedup = xs => dedup_f((==), 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. + + @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) => { @@ -32,7 +38,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) { @@ -171,7 +177,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")) + | 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_Elaboration.re b/test/Test_Elaboration.re index 2516f25227..c515487535 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,106 @@ 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, + ), + ); + +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, ), ); @@ -220,4 +335,14 @@ let elaboration_tests = [ `Quick, deferral, ), + test_case( + "Function application with a single remaining argument after deferral", + `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 9e4ade6651..37fcaba764 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: Int(8) |> Exp.fresh}); - let evaluation_test = (msg, expected, unevaluated) => check( dhexp_typ, @@ -38,7 +22,156 @@ 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 tet_ap_of_hole_deferral = () => + evaluation_test( + "?(_, _, 3)(1., true)", + Ap( + Forward, + 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, + 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( + 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), ]; diff --git a/test/Test_ListUtil.re b/test/Test_ListUtil.re new file mode 100644 index 0000000000..9abfca4f07 --- /dev/null +++ b/test/Test_ListUtil.re @@ -0,0 +1,610 @@ +open Alcotest; +open Util; + +let tests = ( + "ListUtil", + [ + test_case( + "rev_if with false", + `Quick, + () => { + let xs = [1, 2, 3]; + check(list(int), "Same list", xs, ListUtil.rev_if(false, xs)); + }, + ), + test_case( + "rev_if with true", + `Quick, + () => { + let xs = [1, 2, 3]; + check( + list(int), + "Reversed list", + [3, 2, 1], + ListUtil.rev_if(true, xs), + ); + }, + ), + 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 + }, + ), + 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 + }, + ), + 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), + ); + }, + ), + 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), + ); + }, + ), + test_case("range generates sequential integers [1,6)", `Quick, () => { + check(list(int), "1-5", [1, 2, 3, 4, 5], ListUtil.range(~lo=1, 6)) + }), + test_case("range defaults lower bound to 0", `Quick, () => { + check(list(int), "0-5", [0, 1, 2, 3, 4, 5], ListUtil.range(6)) + }), + test_case("range lo = hi is empty", `Quick, () => { + check(list(int), "empty list", [], ListUtil.range(~lo=1, 1)) + }), + test_case("Invalid range raises error", `Quick, () => { + check_raises( + "Invalid range", + Invalid_argument("ListUtil.range"), + () => { + let _ = ListUtil.range(~lo=2, 1); + (); + }, + ) + }), + 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), + ); + }, + ), + 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), + ); + }, + ), + 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); + (); + }, + ); + }, + ), + 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); + (); + }, + ); + }, + ), + 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( + "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)), + ); + }, + ), + 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]), + ); + }, + ), + 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)); + }, + ), + 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), + ); + }, + ), + 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), + ); + }, + ), + 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), + ); + }, + ), + 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); + (); + }, + ); + }, + ), + ], +); diff --git a/test/Test_MakeTerm.re b/test/Test_MakeTerm.re new file mode 100644 index 0000000000..46818664a9 --- /dev/null +++ b/test/Test_MakeTerm.re @@ -0,0 +1,82 @@ +/** + * 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); + +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 ", + ) + }), + 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", + ) + }), +]; diff --git a/test/haz3ltest.re b/test/haz3ltest.re index 3e13ae44b7..03cebe774c 100644 --- a/test/haz3ltest.re +++ b/test/haz3ltest.re @@ -3,11 +3,13 @@ open Junit_alcotest; let (suite, _) = run_and_report( ~and_exit=false, - "Dynamics", + "HazelTests", [ ("Elaboration", Test_Elaboration.elaboration_tests), ("Statics", Test_Statics.tests), ("Evaluator", Test_Evaluator.tests), + Test_ListUtil.tests, + ("MakeTerm", Test_MakeTerm.tests), ], ); Junit.to_file(Junit.make([suite]), "junit_tests.xml");