Add string_split (#1429)

hazelgrove · Dec 17, 2024 · 82d39a9 · 82d39a9
2 parents b429e57 + 863b329
commit 82d39a9
Show file tree

Hide file tree

Showing 8 changed files with 196 additions and 103 deletions.
diff --git a/src/haz3lcore/dynamics/Builtins.re b/src/haz3lcore/dynamics/Builtins.re
@@ -289,6 +289,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;
@@ -356,6 +372,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
@@ -36,6 +36,11 @@ let replace = Js_of_ocaml.Regexp.global_replace;
 
 let split = Js_of_ocaml.Regexp.split;
 
+let plain_split: (string, string) => list(string) =
+  (str, sep) => {
+    split(Js_of_ocaml.Regexp.regexp_string(sep), str);
+  };
+
 let to_lines = String.split_on_char('\n');
 
 let line_widths = (s: string): list(int) =>

diff --git 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
@@ -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
@@ -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
@@ -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/Test_StringUtil.re b/test/Test_StringUtil.re
@@ -0,0 +1,49 @@
+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"),
+      )
+    }),
+    test_case("regexp special character in separator", `Quick, () => {
+      check(
+        list(string),
+        "split",
+        ["a", "c"],
+        StringUtil.plain_split("a.*c", ".*"),
+      )
+    }),
+  ],
+);
diff --git a/test/haz3ltest.re b/test/haz3ltest.re
@@ -5,11 +5,12 @@ let (suite, _) =
     ~and_exit=false,
     "HazelTests",
     [
-      ("Elaboration", Test_Elaboration.elaboration_tests),
-      ("Statics", Test_Statics.tests),
-      ("Evaluator", Test_Evaluator.tests),
+      Test_Elaboration.elaboration_tests,
+      Test_StringUtil.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");