wip

src/Core/Domain.hs

@@ -93,9 +93,25 @@ pattern Empty :: Spine
 pattern Empty =
   Spine Seq.Empty Seq.Empty
 
+pattern (:<) :: Elimination -> Spine -> Spine
+pattern elimination :< spine <-
+  (eliminationViewL -> Just (elimination, spine))
+  where
+    elim :< Spine spine args =
+      case elim of
+        App plicity arg ->
+          case spine of
+            Seq.Empty -> Spine Seq.Empty ((plicity, arg) Seq.:<| args)
+            (apps, brs) Seq.:<| spine' ->
+              Spine (((plicity, arg) Seq.:<| apps, brs) Seq.:<| spine') args
+        Case brs ->
+          Spine ((Seq.Empty, brs) Seq.:<| spine) args
+
+{-# COMPLETE Empty, (:<) #-}
+
 pattern (:>) :: Spine -> Elimination -> Spine
 pattern spine :> elimination <-
-  (eliminationView -> Just (spine, elimination))
+  (eliminationViewR -> Just (spine, elimination))
   where
     Spine spine args :> elim =
       case elim of
@@ -113,8 +129,19 @@ pattern Apps args <-
     Apps args =
       Spine Seq.Empty args
 
-eliminationView :: Spine -> Maybe (Spine, Elimination)
-eliminationView (Spine spine apps) =
+eliminationViewL :: Spine -> Maybe (Elimination, Spine)
+eliminationViewL (Spine spine apps) =
+  case spine of
+    Seq.Empty -> case apps of
+      Seq.Empty -> Nothing
+      (plicity, arg) Seq.:<| apps' -> Just (App plicity arg, Spine spine apps')
+    (Seq.Empty, brs) Seq.:<| spine' ->
+      Just (Case brs, Spine spine' apps)
+    ((plicity, arg) Seq.:<| apps', brs) Seq.:<| spine' ->
+      Just (App plicity arg, Spine ((apps', brs) Seq.:<| spine') apps)
+
+eliminationViewR :: Spine -> Maybe (Spine, Elimination)
+eliminationViewR (Spine spine apps) =
   case apps of
     Seq.Empty ->
       case spine of

src/Elaboration/Context.hs

@@ -275,13 +275,13 @@ extendBefore context beforeVar binding type_ = do
     )
 
 defineWellOrdered :: Context v -> Domain.Head -> Domain.Spine -> Domain.Value -> Context v
-defineWellOrdered context head spine value =
+defineWellOrdered context head_ spine value =
   context
     { equations =
         context.equations
-          { equal = HashMap.insertWith (<>) head [(spine, value)] context.equations.equal
+          { equal = HashMap.insertWith (<>) head_ [(spine, value)] context.equations.equal
           }
-    , boundVars = case (head, spine) of
+    , boundVars = case (head_, spine) of
         (Domain.Var var, Domain.Empty) -> IntSeq.delete var context.boundVars
         _ -> context.boundVars
     }
@@ -292,9 +292,9 @@ skip context = do
   pure context'
 
 define :: Context v -> Domain.Head -> Domain.Spine -> Domain.Value -> M (Context v)
-define context head spine value = do
+define context head_ spine value = do
   deps <- evalStateT (freeVars context value) mempty
-  let context' = defineWellOrdered context head spine value
+  let context' = defineWellOrdered context head_ spine value
       (pre, post) =
         Tsil.partition (`EnumSet.member` deps) $
           IntSeq.toTsil context'.boundVars
@@ -598,8 +598,8 @@ forceHead context value =
           forceHead context value'
         Meta.EagerUnsolved {} ->
           pure value
-    Domain.Neutral head spine
-      | Just spineValues <- HashMap.lookup head context.equations.equal -> do
+    Domain.Neutral head_ spine
+      | Just spineValues <- HashMap.lookup head_ context.equations.equal -> do
           let go [] = pure value
               go ((eqSpine, eqValue) : rest)
                 | Just (spinePrefix, spineSuffix) <- Domain.matchSpinePrefix spine eqSpine = do
@@ -637,16 +637,16 @@ forceHeadGlue context value =
           pure $ Domain.Glued (Domain.Meta metaIndex) spine $ Domain.Lazy lazyValue
         Meta.EagerUnsolved {} ->
           pure value
-    Domain.Neutral head spine
-      | Just spineValues <- HashMap.lookup head context.equations.equal -> do
+    Domain.Neutral head_ spine
+      | Just spineValues <- HashMap.lookup head_ context.equations.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
+                        pure $ Domain.Glued head_ spine $ Domain.Lazy lazyValue
                       else go rest
               go (_ : rest) = go rest
           go spineValues

src/Elaboration/Depth.hs

@@ -0,0 +1,28 @@
+{-# LANGUAGE BlockArguments #-}
+
+module Elaboration.Depth where
+
+import qualified Core.Domain as Domain
+import Monad
+import Protolude
+import qualified Query
+import qualified Query.Mapped as Mapped
+import Rock
+
+-- | Try to find out which of two heads might refer to the other so we can
+-- unfold glued values that are defined later first (see "depth" in
+-- https://arxiv.org/pdf/1505.04324.pdf).
+compareHeadDepths :: Domain.Head -> Domain.Head -> M Ordering
+compareHeadDepths head1 head2 =
+  case (head1, head2) of
+    (Domain.Global global1, Domain.Global global2) -> do
+      global1DependsOn2 <- fetch $ Query.TransitiveDependencies global2 $ Mapped.Query global1
+      global2DependsOn1 <- fetch $ Query.TransitiveDependencies global1 $ Mapped.Query global2
+      pure case (global1DependsOn2, global2DependsOn1) of
+        (Just _, Nothing) -> GT
+        (Nothing, Just _) -> LT
+        _ -> EQ
+    (_, Domain.Global _) -> pure LT
+    (Domain.Global _, _) -> pure GT
+    (Domain.Var v1, Domain.Var v2) -> pure $ compare v1 v2
+    _ -> pure EQ