Make DeferredAp a Value

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) =>
       // TODO I don't know why this needs to be final
       let. _ = otherwise(env, (d1, (d2, _)) => Ap(dir, d1, d2) |> rewrap)

src/haz3lcore/dynamics/ValueChecker.re

@@ -69,6 +69,7 @@ module ValueCheckerEVMode: {
     | (_, _, Constructor) => r
     | (_, Expr, Indet) => Expr
     | (_, _, Indet) => Indet
+    | (_, _, Value) => Value
     | (true, _, Step(_)) => Expr
     | (false, _, Step(_)) => r
     };