Merge remote-tracking branch 'origin/dev' into remove_termbase_modules

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

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);

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)
     };
 };

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
       };
 

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))) {

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
     };

src/util/ListUtil.re

@@ -1,22 +1,28 @@
 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],
     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) => {

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,
+  ),
 ];