From 2a1cb1be6a98dca58f48491b05182f6af86f678c Mon Sep 17 00:00:00 2001
From: Olle Fredriksson <fredriksson.olle@gmail.com>
Date: Fri, 22 Mar 2024 08:37:03 +0100
Subject: [PATCH] isStuck

---
 src/Elaboration/Context.hs | 42 +++++++++++++++++---------------------
 1 file changed, 19 insertions(+), 23 deletions(-)

diff --git a/src/Elaboration/Context.hs b/src/Elaboration/Context.hs
index 46f5f25..1aca592 100644
--- a/src/Elaboration/Context.hs
+++ b/src/Elaboration/Context.hs
@@ -684,21 +684,19 @@ forceNeutral context head_ spine
             pure Nothing
       _ -> pure Nothing
 
-unstuck :: Context v -> Domain.Value -> M (Maybe Domain.Value)
-unstuck context headApp = do
-  headApp' <- forceHeadGlue context headApp
+isStuck :: Context v -> Domain.Value -> M Bool
+isStuck context headApp = do
+  headApp' <- forceHead context headApp
   case headApp' of
-    Domain.AnyNeutral _ (Domain.Apps _) -> pure $ Just headApp'
-    Domain.Glued _ (Domain.Apps _) _ -> pure $ Just headApp'
-    Domain.Glued _ _ value -> unstuck context value
-    Domain.Con {} -> pure $ Just headApp'
-    Domain.Lit {} -> pure $ Just headApp'
-    Domain.Pi {} -> pure $ Just headApp'
-    Domain.Fun {} -> pure $ Just headApp'
+    Domain.AnyNeutral _ (Domain.Apps _) -> pure False
+    Domain.Con {} -> pure False
+    Domain.Lit {} -> pure False
+    Domain.Pi {} -> pure False
+    Domain.Fun {} -> pure False
     _ -> do
       -- putText "unstuck.stuck:"
       -- dumpValue context headApp'
-      pure Nothing
+      pure True
 
 -- | Evaluate the head of a value further, if (now) possible due to meta
 -- solutions or new value bindings. Also evaluates through glued values.
@@ -710,12 +708,11 @@ forceHead context value =
   case value of
     Domain.Neutral head_ spine -> neutral head_ spine
     Domain.Stuck head_ args headApp spine -> do
-      maybeUnstuck <- unstuck context headApp
-      case maybeUnstuck of
-        Nothing ->
-          neutral head_ $ Domain.Apps args <> spine
-        Just unstuckValue -> do
-          value' <- Evaluation.applySpine unstuckValue spine
+      stuck <- isStuck context headApp
+      if stuck
+        then neutral head_ $ Domain.Apps args <> spine
+        else do
+          value' <- Evaluation.applySpine headApp spine
           forceHead context value'
     Domain.Glued _ _ value' ->
       forceHead context value'
@@ -745,12 +742,11 @@ forceHeadGlue context value =
     Domain.Neutral head_ spine -> neutral head_ spine
     Domain.Stuck head_ args headApp spine -> do
       let spine' = Domain.Apps args <> spine
-      maybeUnstuck <- unstuck context headApp
-      case maybeUnstuck of
-        Nothing ->
-          neutral head_ spine'
-        Just unstuckValue -> do
-          lazyValue <- lazy $ Evaluation.applySpine unstuckValue spine
+      stuck <- isStuck context headApp
+      if stuck
+        then neutral head_ spine'
+        else do
+          lazyValue <- lazy $ Evaluation.applySpine headApp spine
           pure $ Domain.Glued head_ spine' $ Domain.Lazy lazyValue
     Domain.Lazy lazyValue -> do
       value' <- force lazyValue