Add some additional tests to be useful for the labeled tuples branch (#…

…1401)

src/haz3lcore/lang/term/IdTagged.re

@@ -14,6 +14,11 @@ type t('a) = {
   term: 'a,
 };
 
+// To be used if you want to remove the id from the debug output
+// let pp: ((Format.formatter, 'a) => unit, Format.formatter, t('a)) => unit =
+//   (fmt_a, formatter, ta) => {
+//     fmt_a(formatter, ta.term);
+//   };
 let fresh = term => {
   {ids: [Id.mk()], copied: false, term};
 };

test/Test_Elaboration.re

@@ -74,20 +74,18 @@ let consistent_if = () =>
     dhexp_of_uexp(u6),
   );
 
-let u7: Exp.t =
-  Ap(
-    Forward,
-    Fun(
-      Var("x") |> Pat.fresh,
-      BinOp(Int(Plus), Int(4) |> Exp.fresh, Int(5) |> Exp.fresh)
-      |> Exp.fresh,
-      None,
-      None,
-    )
-    |> Exp.fresh,
-    Var("y") |> Exp.fresh,
+// x => 4 + 5
+let f =
+  Fun(
+    Var("x") |> Pat.fresh,
+    BinOp(Int(Plus), Int(4) |> Exp.fresh, Int(5) |> Exp.fresh) |> Exp.fresh,
+    None,
+    None,
   )
   |> Exp.fresh;
+let unapplied_function = () => alco_check("A function", f, dhexp_of_uexp(f));
+
+let u7: Exp.t = Ap(Forward, f, Var("y") |> Exp.fresh) |> Exp.fresh;
 
 let ap_fun = () =>
   alco_check("Application of a function", u7, dhexp_of_uexp(u7));
@@ -179,14 +177,47 @@ let let_fun = () =>
     dhexp_of_uexp(u9),
   );
 
+let deferral = () =>
+  alco_check(
+    "string_sub(\"hello\", 1, _)",
+    dhexp_of_uexp(
+      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,
+        [
+          String("hello") |> Exp.fresh,
+          Int(1) |> Exp.fresh,
+          Deferral(InAp) |> Exp.fresh,
+        ],
+      )
+      |> Exp.fresh,
+    ),
+  );
+
 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/Test_Evaluator.re

@@ -0,0 +1,44 @@
+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,
+    msg,
+    expected,
+    Evaluator.Result.unbox(
+      snd(Evaluator.evaluate(Builtins.env_init, {d: unevaluated})),
+    ),
+  );
+
+let test_int = () =>
+  evaluation_test("8", Int(8) |> Exp.fresh, Int(8) |> Exp.fresh);
+
+let test_sum = () =>
+  evaluation_test(
+    "4 + 5",
+    Int(9) |> Exp.fresh,
+    BinOp(Int(Plus), Int(4) |> Exp.fresh, Int(5) |> Exp.fresh) |> Exp.fresh,
+  );
+
+let tests = [
+  test_case("Integer literal", `Quick, test_int),
+  test_case("Integer sum", `Quick, test_sum),
+];

test/Test_Statics.re

@@ -0,0 +1,126 @@
+open Alcotest;
+open Haz3lcore;
+
+let testable_typ = testable(Fmt.using(Typ.show, Fmt.string), Typ.fast_equal);
+module FreshId = {
+  let arrow = (a, b) => Arrow(a, b) |> Typ.fresh;
+  let unknown = a => Unknown(a) |> Typ.fresh;
+  let int = Typ.fresh(Int);
+  let float = Typ.fresh(Float);
+  let prod = a => Prod(a) |> Typ.fresh;
+  let string = Typ.fresh(String);
+};
+let ids = List.init(12, _ => Id.mk());
+let id_at = x => x |> List.nth(ids);
+let statics = Statics.mk(CoreSettings.on, Builtins.ctx_init);
+let alco_check = Alcotest.option(testable_typ) |> Alcotest.check;
+
+// 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 unapplied_function = () =>
+  alco_check(
+    "Unknown param",
+    Some(FreshId.(arrow(unknown(Internal), int))),
+    type_of(
+      Fun(
+        Var("x") |> Pat.fresh,
+        BinOp(Int(Plus), Int(4) |> Exp.fresh, Int(5) |> Exp.fresh)
+        |> Exp.fresh,
+        None,
+        None,
+      )
+      |> Exp.fresh,
+    ),
+  );
+
+let tests =
+  FreshId.[
+    test_case("Function with unknown param", `Quick, () =>
+      alco_check(
+        "x => 4 + 5",
+        Some(arrow(unknown(Internal), int)),
+        type_of(
+          Fun(
+            Var("x") |> Pat.fresh,
+            BinOp(Int(Plus), Int(4) |> Exp.fresh, Int(5) |> Exp.fresh)
+            |> Exp.fresh,
+            None,
+            None,
+          )
+          |> Exp.fresh,
+        ),
+      )
+    ),
+    test_case("Function with known param", `Quick, () =>
+      alco_check(
+        "x : Int => 4 + 5",
+        Some(arrow(int, int)),
+        type_of(
+          Fun(
+            Cast(Var("x") |> Pat.fresh, int, unknown(Internal)) |> Pat.fresh,
+            BinOp(Int(Plus), Int(4) |> Exp.fresh, Int(5) |> Exp.fresh)
+            |> Exp.fresh,
+            None,
+            None,
+          )
+          |> Exp.fresh,
+        ),
+      )
+    ),
+    test_case("bifunction", `Quick, () =>
+      alco_check(
+        "x : Int, y: Int => x + y",
+        Some(arrow(prod([int, int]), int)),
+        type_of(
+          Fun(
+            Tuple([
+              Cast(Var("x") |> Pat.fresh, int, unknown(Internal))
+              |> Pat.fresh,
+              Cast(Var("y") |> Pat.fresh, int, unknown(Internal))
+              |> Pat.fresh,
+            ])
+            |> Pat.fresh,
+            BinOp(Int(Plus), Var("x") |> Exp.fresh, Var("y") |> Exp.fresh)
+            |> Exp.fresh,
+            None,
+            None,
+          )
+          |> Exp.fresh,
+        ),
+      )
+    ),
+    test_case("function application", `Quick, () =>
+      alco_check(
+        "float_of_int(1)",
+        Some(float),
+        type_of(
+          Ap(Forward, Var("float_of_int") |> Exp.fresh, Int(1) |> Exp.fresh)
+          |> Exp.fresh,
+        ),
+      )
+    ),
+    test_case("function deferral", `Quick, () =>
+      alco_check(
+        "string_sub(\"hello\", 1, _)",
+        Some(arrow(int, string)),
+        type_of(
+          DeferredAp(
+            Var("string_sub") |> Exp.fresh,
+            [
+              String("hello") |> Exp.fresh,
+              Int(1) |> Exp.fresh,
+              Deferral(InAp) |> Exp.fresh,
+            ],
+          )
+          |> Exp.fresh,
+        ),
+      )
+    ),
+  ];

test/haz3ltest.re

@@ -4,6 +4,10 @@ let (suite, _) =
   run_and_report(
     ~and_exit=false,
     "Dynamics",
-    [("Elaboration", Test_Elaboration.elaboration_tests)],
+    [
+      ("Elaboration", Test_Elaboration.elaboration_tests),
+      ("Statics", Test_Statics.tests),
+      ("Evaluator", Test_Evaluator.tests),
+    ],
   );
 Junit.to_file(Junit.make([suite]), "junit_tests.xml");