Return Stuck values for (potentially) recursive terms

And check if they are "unstuck" before unfolding them.

src/Core/Evaluation.hs

@@ -16,6 +16,7 @@ import qualified Core.Domain.Telescope as Domain.Telescope
 import qualified Core.Syntax as Syntax
 import Data.OrderedHashMap (OrderedHashMap)
 import qualified Data.OrderedHashMap as OrderedHashMap
+import qualified Data.Sequence as Seq
 import Data.Some (Some)
 import Data.Tsil (Tsil)
 import qualified Data.Tsil as Tsil
@@ -28,6 +29,7 @@ import Plicity
 import Protolude hiding (IntMap, Seq, evaluate, force, head, try)
 import Query (Query)
 import qualified Query
+import qualified Query.Mapped as Mapped
 import Rock
 import Telescope (Telescope)
 import qualified Telescope
@@ -61,15 +63,19 @@ evaluate env term =
           Domain.var var
         Just value
           | Index.Succ index > Environment.glueableBefore env ->
-              Domain.Glued (Domain.Var var) mempty value
+              Domain.Glued (Domain.Var var) mempty $ Domain.Stuck (Domain.Var var) mempty value mempty
           | otherwise ->
               value
     Syntax.Global name -> do
       result <- try $ fetch $ Query.ElaboratedDefinition name
       case result of
         Right (Syntax.ConstantDefinition term', _) -> do
+          recursive <- fetch $ Query.TransitiveDependencies name $ Mapped.Query name
           value <- lazyEvaluate Environment.empty term'
-          pure $ Domain.Glued (Domain.Global name) mempty value
+          pure
+            if isJust recursive
+              then Domain.Glued (Domain.Global name) mempty $ Domain.Stuck (Domain.Global name) mempty value mempty
+              else Domain.Glued (Domain.Global name) mempty value
         Left (Cyclic (_ :: Some Query)) ->
           pure $ Domain.global name
         _ ->
@@ -207,6 +213,9 @@ apply fun plicity arg =
           panic "Core.Evaluation: plicity mismatch"
     Domain.Neutral hd spine ->
       pure $ Domain.Neutral hd $ spine Domain.:> Domain.App plicity arg
+    Domain.Stuck hd args headApp Domain.Empty -> do
+      headApp' <- apply headApp plicity arg
+      pure $ Domain.Stuck hd (args Seq.:|> (plicity, arg)) headApp' Domain.Empty
     Domain.Stuck hd args value spine ->
       pure $ Domain.Stuck hd args value $ spine Domain.:> Domain.App plicity arg
     Domain.Glued hd spine value -> do

src/Elaboration/Context.hs

@@ -684,6 +684,40 @@ forceNeutral context head_ spine
             pure Nothing
       _ -> pure Nothing
 
+isStuck :: Context v -> Domain.Value -> M Bool
+isStuck outerContext outerHeadApp =
+  fmap (either identity (\() -> False)) $ runExceptT $ go True outerContext outerHeadApp
+  where
+    go :: Bool -> Context v -> Domain.Value -> ExceptT Bool M ()
+    go lamIsStuck context headApp = do
+      headApp' <- lift $ forceHeadGlue context headApp
+      -- putText "isStuck.go:"
+      -- lift $ dumpValue context headApp'
+      case headApp' of
+        Domain.Glued _ (Domain.Apps args) value -> do
+          argsStuck <- lift $ fmap (either identity (\() -> False)) $ runExceptT $ mapM_ (mapM_ $ go False context) args
+          if not argsStuck
+            then pure ()
+            else go False context value
+        Domain.Glued _ _ value ->
+          go False context value
+        Domain.AnyNeutral _ (Domain.Apps args) -> mapM_ (mapM_ $ go False context) args
+        Domain.Con _ args -> mapM_ (mapM_ $ go False context) args
+        Domain.Lit {} -> pure ()
+        Domain.Pi binding domain _ targetClosure -> do
+          go False context domain
+          (context', var) <- lift $ extend context (Binding.toName binding) domain
+          target <- lift $ Evaluation.evaluateClosure targetClosure $ Domain.var var
+          go False context' target
+        Domain.Fun domain _ target -> do
+          go False context domain
+          go False context target
+        Domain.Lam {} | not lamIsStuck -> pure ()
+        _ -> do
+          -- putText "isStuck.stuck:"
+          -- lift $ dumpValue context headApp'
+          throwError True
+
 -- | Evaluate the head of a value further, if (now) possible due to meta
 -- solutions or new value bindings. Also evaluates through glued values.
 forceHead
@@ -692,23 +726,32 @@ forceHead
   -> M Domain.Value
 forceHead context value =
   case value of
-    Domain.Neutral head_ spine -> do
-      maybeEqValue <- forceNeutral context head_ spine
-      case maybeEqValue of
-        Just meqValue -> do
-          value'' <- meqValue
-          forceHead context value''
-        Nothing ->
-          pure value
-    Domain.Stuck head_ args value' spine ->
-      undefined -- TODO
+    Domain.Neutral head_ spine -> neutral head_ spine
+    Domain.Stuck head_ args headApp spine -> do
+      stuck <- isStuck context headApp
+      if stuck
+        then neutral head_ $ Domain.Apps args <> spine
+        else do
+          -- putText "forceHead.unstuck:"
+          -- dumpValue context headApp
+          value' <- Evaluation.applySpine headApp spine
+          forceHead context value'
     Domain.Glued _ _ value' ->
       forceHead context value'
     Domain.Lazy lazyValue -> do
       value' <- force lazyValue
       forceHead context value'
     _ ->
       pure value
+  where
+    neutral head_ spine = do
+      maybeEqValue <- forceNeutral context head_ spine
+      case maybeEqValue of
+        Just meqValue -> do
+          value' <- meqValue
+          forceHead context value'
+        Nothing ->
+          pure value
 
 -- | Evaluate the head of a value further, if (now) possible due to meta
 -- solutions or new value bindings, returning glued values.
@@ -718,21 +761,31 @@ forceHeadGlue
   -> M Domain.Value
 forceHeadGlue context value =
   case value of
-    Domain.Neutral head_ spine -> do
+    Domain.Neutral head_ spine -> neutral head_ spine
+    Domain.Stuck head_ args headApp spine -> do
+      let spine' = Domain.Apps args <> spine
+      stuck <- isStuck context headApp
+      if stuck
+        then neutral head_ spine'
+        else do
+          -- putText "forceHeadGlue.unstuck:"
+          -- dumpValue context headApp
+          value' <- Evaluation.applySpine headApp spine
+          forceHeadGlue context value'
+    Domain.Lazy lazyValue -> do
+      value' <- force lazyValue
+      forceHeadGlue context value'
+    _ ->
+      pure value
+  where
+    neutral head_ spine = do
       maybeEqValue <- forceNeutral context head_ spine
       case maybeEqValue of
         Just meqValue -> do
           lazyValue <- lazy meqValue
           pure $ Domain.Glued head_ spine $ Domain.Lazy lazyValue
         Nothing ->
           pure value
-    Domain.Stuck head_ args value' spine ->
-      undefined -- TODO
-    Domain.Lazy lazyValue -> do
-      value' <- force lazyValue
-      forceHeadGlue context value'
-    _ ->
-      pure value
 
 instantiateType
   :: Context v