Potentially fix deferrals

hazelgrove · Oct 3, 2024 · 9e5570a · 9e5570a
1 parent 35629e9
commit 9e5570a
Show file tree

Hide file tree

Showing 3 changed files with 48 additions and 24 deletions.
diff --git 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
@@ -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
@@ -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),
 ];