isStuck

ollef · Mar 22, 2024 · 2a1cb1b · 2a1cb1b
1 parent d27e1d2
commit 2a1cb1b
Showing 1 changed file with 19 additions and 23 deletions.
diff --git 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