From df2f2f0d80b568db5ce089bbb449463dbd3771f6 Mon Sep 17 00:00:00 2001
From: Olle Fredriksson <fredriksson.olle@gmail.com>
Date: Sun, 17 Mar 2024 23:27:57 +0100
Subject: [PATCH] wip

---
 src/Core/Evaluation.hs     |  8 +++--
 src/Elaboration/Context.hs | 61 ++++++++++++++++++++++++++------------
 2 files changed, 48 insertions(+), 21 deletions(-)

diff --git a/src/Core/Evaluation.hs b/src/Core/Evaluation.hs
index 3964ba7..ee22a64 100644
--- a/src/Core/Evaluation.hs
+++ b/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
@@ -61,7 +62,7 @@ evaluate env term =
           Domain.var var
         Just value
           | Index.Succ index > Environment.glueableBefore env ->
-              Domain.Glued (Domain.Var var) mempty value
+              Domain.Stuck (Domain.Var var) mempty value mempty
           | otherwise ->
               value
     Syntax.Global name -> do
@@ -69,7 +70,7 @@ evaluate env term =
       case result of
         Right (Syntax.ConstantDefinition term', _) -> do
           value <- lazyEvaluate Environment.empty term'
-          pure $ Domain.Glued (Domain.Global name) mempty value
+          pure $ Domain.Stuck (Domain.Global name) mempty value mempty
         Left (Cyclic (_ :: Some Query)) ->
           pure $ Domain.global name
         _ ->
@@ -207,6 +208,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
diff --git a/src/Elaboration/Context.hs b/src/Elaboration/Context.hs
index d741caf..dcbba85 100644
--- a/src/Elaboration/Context.hs
+++ b/src/Elaboration/Context.hs
@@ -643,7 +643,7 @@ forceNeutral context head_ spine
     chooseDefaultBranch =
       case spine of
         (Domain.Spine _ (_ Seq.:<| _))
-          | Just spineInequalities <- HashMap.lookup head_ context.notEqual -> do
+          | Just spineInequalities <- HashMap.lookup head_ context.notEqual ->
               findMatchingDefaultBranch spineInequalities
         _ -> metaSolution
 
@@ -680,6 +680,15 @@ forceNeutral context head_ spine
             pure Nothing
       _ -> pure Nothing
 
+isStuck :: Domain.Value -> Bool
+isStuck headApp = case headApp of
+  Domain.AnyNeutral _ (Domain.Apps _) -> False
+  Domain.Con {} -> False
+  Domain.Lit {} -> False
+  Domain.Pi {} -> False
+  Domain.Fun {} -> False
+  _ -> 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
@@ -688,16 +697,14 @@ 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
+      headApp' <- forceHead context headApp
+      if isStuck headApp'
+        then neutral head_ $ Domain.Apps args <> spine
+        else do
+          value' <- Evaluation.applySpine headApp' spine
+          forceHead context value'
     Domain.Glued _ _ value' ->
       forceHead context value'
     Domain.Lazy lazyValue -> do
@@ -705,6 +712,15 @@ forceHead context value =
       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.
@@ -714,7 +730,21 @@ 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
+      headApp' <- forceHead context headApp
+      if isStuck headApp'
+        then neutral head_ $ Domain.Apps args <> spine
+        else do
+          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
@@ -722,13 +752,6 @@ forceHeadGlue context value =
           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