From 1c8d27ba829cb8ff096f49597c7e2973e04ccf79 Mon Sep 17 00:00:00 2001
From: Alexander Bandukwala <7h3kk1d@gmail.com>
Date: Thu, 3 Oct 2024 09:47:28 -0400
Subject: [PATCH] Make DeferredAp a Value

---
 src/haz3lcore/dynamics/Evaluator.re     | 1 +
 src/haz3lcore/dynamics/EvaluatorStep.re | 2 ++
 src/haz3lcore/dynamics/Transition.re    | 5 +++--
 src/haz3lcore/dynamics/ValueChecker.re  | 1 +
 4 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/haz3lcore/dynamics/Evaluator.re b/src/haz3lcore/dynamics/Evaluator.re
index fb877accd7..628b493e1d 100644
--- a/src/haz3lcore/dynamics/Evaluator.re
+++ b/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)
     };
 };
diff --git a/src/haz3lcore/dynamics/EvaluatorStep.re b/src/haz3lcore/dynamics/EvaluatorStep.re
index f25f25603f..0882fa223f 100644
--- a/src/haz3lcore/dynamics/EvaluatorStep.re
+++ b/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
       };
 
diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re
index 6a17a78d2f..79bbbad38a 100644
--- a/src/haz3lcore/dynamics/Transition.re
+++ b/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)
diff --git a/src/haz3lcore/dynamics/ValueChecker.re b/src/haz3lcore/dynamics/ValueChecker.re
index 39f43daeed..c99a90db6f 100644
--- a/src/haz3lcore/dynamics/ValueChecker.re
+++ b/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
     };