Switch to req_value

hazelgrove · Oct 4, 2024 · 1144e63 · 1144e63
1 parent 8d4ead1
commit 1144e63
Show file tree

Hide file tree

Showing 2 changed files with 37 additions and 29 deletions.
diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re
@@ -336,7 +336,7 @@ module Transition = (EV: EV_MODE) => {
     | Ap(dir, d1, d2) =>
       let. _ = otherwise(env, (d1, (d2, _)) => Ap(dir, d1, d2) |> rewrap)
       and. d1' =
-        req_final(req(state, env), d1 => Ap1(dir, d1, d2) |> wrap_ctx, d1)
+        req_value(req(state, env), d1 => Ap1(dir, d1, d2) |> wrap_ctx, d1)
       and. (d2', d2_is_value) =
         req_final_or_value(
           req(state, env),

diff --git a/test/Test_Evaluator.re b/test/Test_Evaluator.re
@@ -56,46 +56,54 @@ let tet_ap_of_hole_deferral = () =>
     Ap(
       Forward,
       Cast(
-        EmptyHole |> Exp.fresh,
-        Unknown(Internal) |> Typ.fresh,
+        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,
-      )
-      |> Exp.fresh,
-      Cast(
-        Tuple([
-          Cast(
-            Float(1.) |> Exp.fresh,
-            Float |> Typ.fresh,
+        Arrow(
+          Prod([
             Unknown(Internal) |> Typ.fresh,
-          )
-          |> Exp.fresh,
-          Cast(
-            Bool(true) |> Exp.fresh,
-            Bool |> Typ.fresh,
             Unknown(Internal) |> Typ.fresh,
-          )
-          |> Exp.fresh,
-          Cast(
-            Int(3) |> Exp.fresh,
-            Int |> Typ.fresh,
             Unknown(Internal) |> Typ.fresh,
-          )
-          |> Exp.fresh,
-        ])
-        |> Exp.fresh,
-        Prod([
-          Unknown(Internal) |> Typ.fresh,
-          Unknown(Internal) |> Typ.fresh,
+          ])
+          |> Typ.fresh,
           Unknown(Internal) |> Typ.fresh,
-        ])
+        )
         |> Typ.fresh,
-        Unknown(Internal) |> Typ.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,
+        Cast(
+          Int(3) |> Exp.fresh,
+          Int |> Typ.fresh,
+          Unknown(Internal) |> Typ.fresh,
+        )
+        |> Exp.fresh,
+      ])
+      |> Exp.fresh,
     )
     |> Exp.fresh,
     Ap(