wip

src/Core/Domain.hs

@@ -175,3 +175,31 @@ instance Semigroup Spine where
 
 instance Monoid Spine where
   mempty = Empty
+
+matchSpinePrefix :: Spine -> Spine -> Maybe (Spine, Spine)
+matchSpinePrefix (Spine Seq.Empty sargs) (Spine Seq.Empty pargs)
+  | Seq.length sargs >= Seq.length pargs = do
+      let (prefix, suffix) = Seq.splitAt (Seq.length pargs) sargs
+      Just (Spine Seq.Empty prefix, Spine Seq.Empty suffix)
+matchSpinePrefix (Spine ((sargs, sbrs) Seq.:<| srest) sargs') (Spine ((pargs, _) Seq.:<| prest) pargs')
+  | Seq.length sargs == Seq.length pargs = do
+      (Spine prefix prefixArgs, suffix) <- matchSpinePrefix (Spine srest sargs') (Spine prest pargs')
+      Just (Spine ((sargs, sbrs) Seq.:<| prefix) prefixArgs, suffix)
+matchSpinePrefix _ _ = Nothing
+
+-- where
+--   suffixArgs
+--     | Seq.length sargs >= Seq.length pargs = do
+--       let (prefix', suffix) = Seq.splitAt (Seq.length pargs) sargs
+--       Just (prefix', suffix)
+-- \| Seq.length sargs >=
+
+-- case (spine, prefix) of
+--   (Spine Seq.Empty sargs, Spine Seq.Empty pargs) |
+--     Seq.length sargs >= Seq.length pargs -> do
+--       let (prefix', suffix) = Seq.splitAt (Seq.length pargs) spine
+--       Just (Spine Seq.Empty prefix', Spine Seq.Empty suffix)
+--     | otherwise -> Nothing
+--   (Spine ((sargs, sbranch) Seq.:|> srest) sargs', Spine ((pargs, pbranch) Seq.:|> prest) pargs') ->
+
+--   _ -> Nothing

src/Elaboration/Context.hs

@@ -39,6 +39,7 @@ import Data.Tsil (Tsil)
 import qualified Data.Tsil as Tsil
 import qualified Elaboration.Meta as Meta
 import qualified Elaboration.Postponed as Postponed
+import {-# SOURCE #-} Elaboration.Unification as Unification
 import Environment (Environment (Environment))
 import qualified Environment
 import Error (Error)
@@ -148,6 +149,26 @@ spanned s context =
     { span = s
     }
 
+-------------------------------------------------------------------------------
+coveredConstructorsAndLiterals :: Context v -> Domain.Head -> Domain.Spine -> M (HashSet Name.QualifiedConstructor, HashSet Literal)
+coveredConstructorsAndLiterals context head_ spine =
+  case HashMap.lookup head_ context.equations.notEqual of
+    Nothing -> pure mempty
+    Just spines ->
+      fold
+        <$> mapM
+          ( \(spine', constructors, literals) -> do
+              eq <- Unification.equalSpines context spine spine'
+              pure if eq then (constructors, literals) else mempty
+          )
+          spines
+
+coveredConstructors :: Context v -> Domain.Head -> Domain.Spine -> M (HashSet Name.QualifiedConstructor)
+coveredConstructors context head_ spine = fst <$> coveredConstructorsAndLiterals context head_ spine
+
+coveredLiterals :: Context v -> Domain.Head -> Domain.Spine -> M (HashSet Literal)
+coveredLiterals context head_ spine = snd <$> coveredConstructorsAndLiterals context head_ spine
+
 -------------------------------------------------------------------------------
 -- Extension
 
@@ -250,7 +271,7 @@ extendBefore context beforeVar binding type_ = do
     , var
     )
 
-defineWellOrdered :: Context v -> Var -> Domain.Value -> Context v
+defineWellOrdered :: Context v -> Domain.Head -> Domain.Spine -> Domain.Value -> Context v
 defineWellOrdered context var value =
   context
     { values = EnumMap.insert var value context.values
@@ -562,27 +583,35 @@ metaSolutionMetas context index = do
 -------------------------------------------------------------------------------
 
 -- | Evaluate the head of a value further, if (now) possible due to meta
--- solutions or new value bindings. Also evalutes through glued values.
+-- solutions or new value bindings. Also evaluates through glued values.
 forceHead
   :: Context v
   -> Domain.Value
   -> M Domain.Value
 forceHead context value =
   case value of
-    Domain.Neutral (Domain.Var var) spine
-      | Just headValue <- lookupVarValue var context -> do
-          value' <- Evaluation.applySpine headValue spine
-          forceHead context value'
     Domain.Neutral (Domain.Meta metaIndex) spine -> do
       meta <- lookupEagerMeta context metaIndex
-
       case meta of
         Meta.EagerSolved headValue _ _ -> do
           headValue' <- Evaluation.evaluate Environment.empty headValue
           value' <- Evaluation.applySpine headValue' spine
           forceHead context value'
         Meta.EagerUnsolved {} ->
           pure value
+    Domain.Neutral head spine
+      | Just spineValues <- HashMap.lookup head context.equalities.equal -> do
+          let go [] = pure value
+              go ((eqSpine, eqValue) : rest)
+                | Just (spinePrefix, spineSuffix) <- Domain.matchSpinePrefix spine eqSpine = do
+                    eq <- Unification.equalSpines context spinePrefix eqSpine
+                    if eq
+                      then do
+                        value' <- Evaluation.applySpine eqValue spineSuffix
+                        forceHead context value'
+                      else go rest
+              go (_ : rest) = go rest
+          go spineValues
     Domain.Glued _ _ value' ->
       forceHead context value'
     Domain.Lazy lazyValue -> do
@@ -599,23 +628,29 @@ forceHeadGlue
   -> M Domain.Value
 forceHeadGlue context value =
   case value of
-    Domain.Neutral (Domain.Var var) spine
-      | Just headValue <- lookupVarValue var context -> do
-          lazyValue <- lazy $ do
-            value' <- Evaluation.applySpine headValue spine
-            forceHeadGlue context value'
-          pure $ Domain.Glued (Domain.Var var) spine $ Domain.Lazy lazyValue
     Domain.Neutral (Domain.Meta metaIndex) spine -> do
       meta <- lookupEagerMeta context metaIndex
       case meta of
         Meta.EagerSolved headValue _ _ -> do
-          lazyValue <- lazy $ do
+          lazyValue <- lazy do
             headValue' <- Evaluation.evaluate Environment.empty headValue
-            value' <- Evaluation.applySpine headValue' spine
-            forceHeadGlue context value'
+            Evaluation.applySpine headValue' spine
           pure $ Domain.Glued (Domain.Meta metaIndex) spine $ Domain.Lazy lazyValue
         Meta.EagerUnsolved {} ->
           pure value
+    Domain.Neutral head spine
+      | Just spineValues <- HashMap.lookup head context.equalities.equal -> do
+          let go [] = pure value
+              go ((eqSpine, eqValue) : rest)
+                | Just (spinePrefix, spineSuffix) <- Domain.matchSpinePrefix spine eqSpine = do
+                    eq <- Unification.equalSpines context spinePrefix eqSpine
+                    if eq
+                      then do
+                        lazyValue <- lazy $ Evaluation.applySpine eqValue spineSuffix
+                        pure $ Domain.Glued head spine $ Domain.Lazy lazyValue
+                      else go rest
+              go (_ : rest) = go rest
+          go spineValues
     Domain.Lazy lazyValue -> do
       value' <- force lazyValue
       forceHeadGlue context value'

src/Elaboration/Context.hs-boot

@@ -0,0 +1,6 @@
+{-# language RoleAnnotations #-}
+module Elaboration.Context where
+
+data Context v
+
+type role Context phantom