From c6a3dcd2b24503b251bb67d7d31e96533f35550c Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Tue, 3 Dec 2024 15:16:50 -0500 Subject: [PATCH 1/3] Add string_split to builtins --- src/haz3lcore/dynamics/Builtins.re | 22 ++++++++++++++++ src/util/StringUtil.re | 11 ++++++++ test/Test_StringUtil.re | 41 ++++++++++++++++++++++++++++++ test/haz3ltest.re | 1 + 4 files changed, 75 insertions(+) create mode 100644 test/Test_StringUtil.re diff --git a/src/haz3lcore/dynamics/Builtins.re b/src/haz3lcore/dynamics/Builtins.re index c47617edc6..894d6ff707 100644 --- a/src/haz3lcore/dynamics/Builtins.re +++ b/src/haz3lcore/dynamics/Builtins.re @@ -278,6 +278,22 @@ module Pervasives = { | (_, _, _) => Error(InvalidBoxedIntLit(d1)) } ); + + let string_split = _ => + binary((d1, d2) => + switch (term_of(d1), term_of(d2)) { + | (String(s), String(sep)) => + Ok( + ListLit( + Util.StringUtil.plain_split(sep, s) + |> List.map(s => DHExp.fresh(String(s))), + ) + |> fresh, + ) + | (String(_), _) => Error(InvalidBoxedStringLit(d2)) + | (_, _) => Error(InvalidBoxedStringLit(d1)) + } + ); }; open Impls; @@ -345,6 +361,12 @@ module Pervasives = { Prod([String |> Typ.fresh, Int |> Typ.fresh, Int |> Typ.fresh]), String, string_sub("string_sub"), + ) + |> fn( + "string_split", + Prod([String |> Typ.fresh, String |> Typ.fresh]), + List(String |> Typ.fresh), + string_split("string_split"), ); }; diff --git a/src/util/StringUtil.re b/src/util/StringUtil.re index a4fedde846..49a5cab221 100644 --- a/src/util/StringUtil.re +++ b/src/util/StringUtil.re @@ -36,6 +36,17 @@ let replace = Js_of_ocaml.Regexp.global_replace; let split = Js_of_ocaml.Regexp.split; +let plain_split: (string, string) => list(string) = + (str, sep) => { + Js_of_ocaml.( + Js.string(str)##split(Js.string(sep)) + |> Js.str_array + |> Js.to_array + |> Array.to_list + |> List.map(Js.to_string) + ); + }; + let to_lines = String.split_on_char('\n'); let line_widths = (s: string): list(int) => diff --git a/test/Test_StringUtil.re b/test/Test_StringUtil.re new file mode 100644 index 0000000000..b9c4973376 --- /dev/null +++ b/test/Test_StringUtil.re @@ -0,0 +1,41 @@ +open Alcotest; +open Util; + +let tests = ( + "StringUtil", + [ + test_case("empty string splits", `Quick, () => { + check(list(string), "split", [], StringUtil.plain_split("", "")) + }), + test_case("split on empty string", `Quick, () => { + check(list(string), "split", ["a"], StringUtil.plain_split("a", "")) + }), + test_case("split with no matches", `Quick, () => { + check(list(string), "split", ["a"], StringUtil.plain_split("a", "b")) + }), + test_case("split with one match", `Quick, () => { + check( + list(string), + "split", + ["a", "c"], + StringUtil.plain_split("abc", "b"), + ) + }), + test_case("split with multiple matches", `Quick, () => { + check( + list(string), + "split", + ["a", "c", "e"], + StringUtil.plain_split("abcbe", "b"), + ) + }), + test_case("split with empty inbetweens", `Quick, () => { + check( + list(string), + "split", + ["a", "", "e"], + StringUtil.plain_split("abbe", "b"), + ) + }), + ], +); diff --git a/test/haz3ltest.re b/test/haz3ltest.re index 8e4a838b0a..a2dfc9a7c4 100644 --- a/test/haz3ltest.re +++ b/test/haz3ltest.re @@ -6,6 +6,7 @@ let (suite, _) = "HazelTests", [ ("Elaboration", Test_Elaboration.elaboration_tests), + Test_StringUtil.tests, ("Statics", Test_Statics.tests), ("Evaluator", Test_Evaluator.tests), Test_ListUtil.tests, From 42a6262cb12e7d33f3d74331ab3cda4172fac2f8 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 5 Dec 2024 09:36:44 -0500 Subject: [PATCH 2/3] Move test module names into modules --- test/Test_Elaboration.re | 57 +++++++++-------- test/Test_Evaluator.re | 17 +++-- test/Test_MakeTerm.re | 134 +++++++++++++++++++++------------------ test/Test_Statics.re | 6 +- test/haz3ltest.re | 8 +-- 5 files changed, 119 insertions(+), 103 deletions(-) diff --git a/test/Test_Elaboration.re b/test/Test_Elaboration.re index c515487535..c30e653f55 100644 --- a/test/Test_Elaboration.re +++ b/test/Test_Elaboration.re @@ -319,30 +319,33 @@ let ap_of_deferral_of_hole = () => ), ); -let elaboration_tests = [ - test_case("Single integer", `Quick, single_integer), - test_case("Empty hole", `Quick, empty_hole), - test_case("Free variable", `Quick, free_var), - test_case("Let expression", `Quick, let_exp), - test_case("Inconsistent binary operation", `Quick, bin_op), - test_case("Consistent if statement", `Quick, consistent_if), - test_case("An unapplied function", `Quick, unapplied_function), - test_case("Application of function on free variable", `Quick, ap_fun), - test_case("Inconsistent case statement", `Quick, inconsistent_case), - test_case("Let expression for a function", `Quick, let_fun), - test_case( - "Function application with a deferred argument", - `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, - ), -]; +let elaboration_tests = ( + "Elaboration", + [ + test_case("Single integer", `Quick, single_integer), + test_case("Empty hole", `Quick, empty_hole), + test_case("Free variable", `Quick, free_var), + test_case("Let expression", `Quick, let_exp), + test_case("Inconsistent binary operation", `Quick, bin_op), + test_case("Consistent if statement", `Quick, consistent_if), + test_case("An unapplied function", `Quick, unapplied_function), + test_case("Application of function on free variable", `Quick, ap_fun), + test_case("Inconsistent case statement", `Quick, inconsistent_case), + test_case("Let expression for a function", `Quick, let_fun), + test_case( + "Function application with a deferred argument", + `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 37fcaba764..b074a52b22 100644 --- a/test/Test_Evaluator.re +++ b/test/Test_Evaluator.re @@ -168,10 +168,13 @@ let tet_ap_of_hole_deferral = () => |> 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), -]; +let tests = ( + "Evaluator", + [ + 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_MakeTerm.re b/test/Test_MakeTerm.re index 46818664a9..003ce7ca65 100644 --- a/test/Test_MakeTerm.re +++ b/test/Test_MakeTerm.re @@ -12,71 +12,79 @@ let parse_exp = (s: string) => 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, +let tests = ( + "MakeTerm", + [ + 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)", ) - |> 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 + }), + 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, - Int(1) |> 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", ) - |> 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) + }), + test_case("Type Alias", `Quick, () => { + exp_check( + TyAlias( + Var("x") |> TPat.fresh, + Int |> Typ.fresh, + Int(1) |> Exp.fresh, + ) |> Exp.fresh, - EmptyHole |> Exp.fresh, + "type x = Int in 1", ) - |> 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/Test_Statics.re b/test/Test_Statics.re index 71fdafc8ba..7bbf7db481 100644 --- a/test/Test_Statics.re +++ b/test/Test_Statics.re @@ -40,7 +40,8 @@ let unapplied_function = () => ), ); -let tests = +let tests = ( + "Statics", FreshId.[ test_case("Function with unknown param", `Quick, () => alco_check( @@ -123,4 +124,5 @@ let tests = ), ) ), - ]; + ], +); diff --git a/test/haz3ltest.re b/test/haz3ltest.re index a2dfc9a7c4..f6bcf3cf6f 100644 --- a/test/haz3ltest.re +++ b/test/haz3ltest.re @@ -5,12 +5,12 @@ let (suite, _) = ~and_exit=false, "HazelTests", [ - ("Elaboration", Test_Elaboration.elaboration_tests), + Test_Elaboration.elaboration_tests, Test_StringUtil.tests, - ("Statics", Test_Statics.tests), - ("Evaluator", Test_Evaluator.tests), + Test_Statics.tests, + Test_Evaluator.tests, Test_ListUtil.tests, - ("MakeTerm", Test_MakeTerm.tests), + Test_MakeTerm.tests, ], ); Junit.to_file(Junit.make([suite]), "junit_tests.xml"); From befc42d15c06b1bac33b3c595c2406a664c6ce17 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Tue, 10 Dec 2024 13:00:31 -0500 Subject: [PATCH 3/3] Use js_of_ocaml regex for split --- src/util/StringUtil.re | 8 +------- test/Test_StringUtil.re | 8 ++++++++ 2 files changed, 9 insertions(+), 7 deletions(-) diff --git a/src/util/StringUtil.re b/src/util/StringUtil.re index 49a5cab221..582290e854 100644 --- a/src/util/StringUtil.re +++ b/src/util/StringUtil.re @@ -38,13 +38,7 @@ let split = Js_of_ocaml.Regexp.split; let plain_split: (string, string) => list(string) = (str, sep) => { - Js_of_ocaml.( - Js.string(str)##split(Js.string(sep)) - |> Js.str_array - |> Js.to_array - |> Array.to_list - |> List.map(Js.to_string) - ); + split(Js_of_ocaml.Regexp.regexp_string(sep), str); }; let to_lines = String.split_on_char('\n'); diff --git a/test/Test_StringUtil.re b/test/Test_StringUtil.re index b9c4973376..fd2be69fd2 100644 --- a/test/Test_StringUtil.re +++ b/test/Test_StringUtil.re @@ -37,5 +37,13 @@ let tests = ( StringUtil.plain_split("abbe", "b"), ) }), + test_case("regexp special character in separator", `Quick, () => { + check( + list(string), + "split", + ["a", "c"], + StringUtil.plain_split("a.*c", ".*"), + ) + }), ], );