wip

src/Core/Domain.hs

@@ -173,13 +173,7 @@ instance Semigroup Spine where
 instance Monoid Spine where
   mempty = Empty
 
-matchSpinePrefix :: Spine -> Spine -> Maybe (Spine, Spine)
-matchSpinePrefix (Spine sargs srest) (Spine pargs Seq.Empty)
-  | Seq.length sargs >= Seq.length pargs = do
-      let (prefix, suffix) = Seq.splitAt (Seq.length pargs) sargs
-      Just (Spine prefix Seq.Empty, Spine suffix srest)
-matchSpinePrefix (Spine sargs ((sbrs, sargs') Seq.:<| srest)) (Spine pargs ((_, pargs') Seq.:<| prest))
-  | Seq.length sargs == Seq.length pargs = do
-      (Spine prefixArgs prefix, suffix) <- matchSpinePrefix (Spine sargs' srest) (Spine pargs' prest)
-      Just (Spine sargs ((sbrs, prefixArgs) Seq.:<| prefix), suffix)
-matchSpinePrefix _ _ = Nothing
+matchArgsPrefix :: Args -> Args -> Maybe (Args, Args)
+matchArgsPrefix sargs pargs
+  | Seq.length sargs >= Seq.length pargs = Just $ Seq.splitAt (Seq.length pargs) sargs
+  | otherwise = Nothing

src/Core/Evaluation.hs

@@ -144,7 +144,7 @@ chooseConstructorBranch
 chooseConstructorBranch outerEnv qualifiedConstr@(Name.QualifiedConstructor _ constr) outerArgs branches defaultBranch =
   case (OrderedHashMap.lookup constr branches, defaultBranch) of
     (Nothing, Nothing) ->
-      panic "chooseBranch no branches"
+      panic "chooseConstructorBranch no branches"
     (Nothing, Just branch) ->
       evaluate outerEnv branch
     (Just (_, tele), _) -> do
@@ -163,7 +163,7 @@ chooseConstructorBranch outerEnv qualifiedConstr@(Name.QualifiedConstructor _ co
           | plicity1 == plicity2 ->
               dropTypeArgs tele' args'
         _ ->
-          panic "chooseBranch arg mismatch"
+          panic "chooseConstructorBranch arg mismatch"
 
     go
       :: Domain.Environment v

src/Elaboration.hs

@@ -785,7 +785,7 @@ elaborateLets context declaredNames undefinedVars definedVars lets body mode = d
     defines =
       foldr' \(var, value) context' ->
         if isJust $ Context.lookupVarIndex var context'
-          then Context.defineWellOrdered context' (Domain.Var var) Domain.Empty value
+          then Context.defineWellOrdered context' (Domain.Var var) Seq.Empty value
           else context'
 
 forceExpectedTypeHead :: Context v -> Mode result -> M (Mode result)

src/Elaboration/Context.hs

@@ -32,8 +32,10 @@ import Data.EnumSet (EnumSet)
 import qualified Data.EnumSet as EnumSet
 import qualified Data.HashMap.Lazy as HashMap
 import Data.HashSet (HashSet)
+import qualified Data.HashSet as HashSet
 import Data.IORef.Lifted
 import qualified Data.IntSeq as IntSeq
+import qualified Data.OrderedHashMap as OrderedHashMap
 import qualified Data.Sequence as Seq
 import qualified Data.Set as Set
 import qualified Data.Tsil as Tsil
@@ -78,17 +80,17 @@ toEnvironment context =
     , values =
         EnumMap.fromList
           $ mapMaybe
-            ( \(head_, spines) ->
+            ( \(head_, argEqualities) ->
                 case head_ of
                   Domain.Var var -> do
                     let emptySpineValues =
                           mapMaybe
-                            ( \(spine, value) ->
-                                case spine of
-                                  Domain.Empty -> Just (var, value)
+                            ( \(args, value) ->
+                                case args of
+                                  Seq.Empty -> Just (var, value)
                                   _ -> Nothing
                             )
-                            spines
+                            argEqualities
                     case emptySpineValues of
                       [value] -> Just value
                       [] -> Nothing
@@ -149,45 +151,45 @@ spanned s context =
     }
 
 -------------------------------------------------------------------------------
-coveredConstructorsAndLiterals :: Context v -> Domain.Head -> Domain.Spine -> M (HashSet Name.QualifiedConstructor, HashSet Literal)
-coveredConstructorsAndLiterals context head_ spine =
+coveredConstructorsAndLiterals :: Context v -> Domain.Head -> Domain.Args -> M (HashSet Name.QualifiedConstructor, HashSet Literal)
+coveredConstructorsAndLiterals context head_ args =
   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'
+          ( \(args', constructors, literals) -> do
+              eq <- Unification.equalArgs context args args'
               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
+coveredConstructors :: Context v -> Domain.Head -> Domain.Args -> M (HashSet Name.QualifiedConstructor)
+coveredConstructors context head_ args = fst <$> coveredConstructorsAndLiterals context head_ args
 
-coveredLiterals :: Context v -> Domain.Head -> Domain.Spine -> M (HashSet Literal)
-coveredLiterals context head_ spine = snd <$> coveredConstructorsAndLiterals context head_ spine
+coveredLiterals :: Context v -> Domain.Head -> Domain.Args -> M (HashSet Literal)
+coveredLiterals context head_ args = snd <$> coveredConstructorsAndLiterals context head_ args
 
-withCoveredConstructors :: Context v -> Domain.Head -> Domain.Spine -> HashSet Name.QualifiedConstructor -> Context v
-withCoveredConstructors context head_ spine constructors =
+withCoveredConstructors :: Context v -> Domain.Head -> Domain.Args -> HashSet Name.QualifiedConstructor -> Context v
+withCoveredConstructors context head_ args constructors =
   context
     { equations =
         context.equations
           { notEqual =
-              HashMap.insertWith (<>) head_ [(spine, constructors, mempty)] context.equations.notEqual
+              HashMap.insertWith (<>) head_ [(args, constructors, mempty)] context.equations.notEqual
           }
     }
 
-withCoveredLiterals :: Context v -> Domain.Head -> Domain.Spine -> HashSet Literal -> Context v
-withCoveredLiterals context head_ spine literals =
+withCoveredLiterals :: Context v -> Domain.Head -> Domain.Args -> HashSet Literal -> Context v
+withCoveredLiterals context head_ args literals =
   context
     { equations =
         context.equations
           { notEqual =
               HashMap.insertWith
                 (<>)
                 head_
-                [(spine, mempty, literals)]
+                [(args, mempty, literals)]
                 context.equations.notEqual
           }
     }
@@ -245,7 +247,7 @@ extendSurfaceDef context surfaceName@(Name.Surface nameText) value type_ = do
         , indices = context.indices Index.Map.:> var
         , equations =
             context.equations
-              { equal = HashMap.insert (Domain.Var var) [(Domain.Empty, value)] context.equations.equal
+              { equal = HashMap.insert (Domain.Var var) [(Seq.Empty, value)] context.equations.equal
               }
         , types = EnumMap.insert var type_ context.types
         }
@@ -272,7 +274,7 @@ extendDef context name value type_ = do
         , indices = context.indices Index.Map.:> var
         , equations =
             context.equations
-              { equal = HashMap.insert (Domain.Var var) [(Domain.Empty, value)] context.equations.equal
+              { equal = HashMap.insert (Domain.Var var) [(Seq.Empty, value)] context.equations.equal
               }
         , types = EnumMap.insert var type_ context.types
         }
@@ -300,15 +302,15 @@ extendBefore context beforeVar binding type_ = do
     , var
     )
 
-defineWellOrdered :: Context v -> Domain.Head -> Domain.Spine -> Domain.Value -> Context v
-defineWellOrdered context head_ spine value =
+defineWellOrdered :: Context v -> Domain.Head -> Domain.Args -> Domain.Value -> Context v
+defineWellOrdered context head_ args value =
   context
     { equations =
         context.equations
-          { equal = HashMap.insertWith (<>) head_ [(spine, value)] context.equations.equal
+          { equal = HashMap.insertWith (<>) head_ [(args, value)] context.equations.equal
           }
-    , boundVars = case (head_, spine) of
-        (Domain.Var var, Domain.Empty) -> IntSeq.delete var context.boundVars
+    , boundVars = case (head_, args) of
+        (Domain.Var var, Seq.Empty) -> IntSeq.delete var context.boundVars
         _ -> context.boundVars
     }
 
@@ -317,10 +319,10 @@ skip context = do
   (context', _) <- extendDef context "skip" Builtin.Type Builtin.Type
   pure context'
 
-define :: Context v -> Domain.Head -> Domain.Spine -> Domain.Value -> M (Context v)
-define context head_ spine value = do
+define :: Context v -> Domain.Head -> Domain.Args -> Domain.Value -> M (Context v)
+define context head_ args value = do
   deps <- evalStateT (freeVars context value) mempty
-  let context' = defineWellOrdered context head_ spine value
+  let context' = defineWellOrdered context head_ args value
       context''
         | EnumSet.null deps = context'
         | otherwise =
@@ -643,19 +645,53 @@ 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_ (Domain.Spine args caseSpine)
+      | Just argEqualities <- 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
+              go ((eqArgs, eqValue) : rest)
+                | Just (argsPrefix, argsSuffix) <- Domain.matchArgsPrefix args eqArgs = do
+                    eq <- Unification.equalArgs context argsPrefix eqArgs
                     if eq
                       then do
-                        value' <- Evaluation.applySpine eqValue spineSuffix
+                        value' <- Evaluation.applySpine eqValue $ Domain.Spine argsSuffix caseSpine
                         forceHead context value'
                       else go rest
               go (_ : rest) = go rest
-          go spineValues
+          go argEqualities
+    Domain.Neutral
+      head_
+      ( Domain.Spine
+          args1
+          ( ( Domain.Branches env' (Syntax.ConstructorBranches typeName cbrs) (Just defaultBranch)
+              , args2
+              )
+              Seq.:<| caseSpine
+            )
+        ) -> do
+        covered <- coveredConstructors context head_ args1
+        if all (\c -> HashSet.member (Name.QualifiedConstructor typeName c) covered) $ OrderedHashMap.keys cbrs
+          then do
+            branchValue <- Evaluation.evaluate env' defaultBranch
+            value' <- Evaluation.applySpine branchValue $ Domain.Spine args2 caseSpine
+            forceHead context value'
+          else pure value
+    Domain.Neutral
+      head_
+      ( Domain.Spine
+          args1
+          ( ( Domain.Branches env' (Syntax.LiteralBranches lbrs) (Just defaultBranch)
+              , args2
+              )
+              Seq.:<| caseSpine
+            )
+        ) -> do
+        covered <- coveredLiterals context head_ args1
+        if all (`HashSet.member` covered) $ OrderedHashMap.keys lbrs
+          then do
+            branchValue <- Evaluation.evaluate env' defaultBranch
+            value' <- Evaluation.applySpine branchValue $ Domain.Spine args2 caseSpine
+            forceHead context value'
+          else pure value
     Domain.Glued _ _ value' ->
       forceHead context value'
     Domain.Lazy lazyValue -> do
@@ -682,19 +718,57 @@ 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@(Domain.Spine args caseSpine)
+      | Just argEqualities <- 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
+              go ((eqArgs, eqValue) : rest)
+                | Just (argsPrefix, argsSuffix) <- Domain.matchArgsPrefix args eqArgs = do
+                    eq <- Unification.equalArgs context argsPrefix eqArgs
                     if eq
                       then do
-                        lazyValue <- lazy $ Evaluation.applySpine eqValue spineSuffix
+                        lazyValue <- lazy $ Evaluation.applySpine eqValue $ Domain.Spine argsSuffix caseSpine
                         pure $ Domain.Glued head_ spine $ Domain.Lazy lazyValue
                       else go rest
               go (_ : rest) = go rest
-          go spineValues
+          go argEqualities
+    Domain.Neutral
+      head_
+      spine@( Domain.Spine
+                args1
+                ( ( Domain.Branches env' (Syntax.ConstructorBranches typeName cbrs) (Just defaultBranch)
+                    , args2
+                    )
+                    Seq.:<| caseSpine
+                  )
+              ) -> do
+        covered <- coveredConstructors context head_ args1
+        if all (\c -> HashSet.member (Name.QualifiedConstructor typeName c) covered) $ OrderedHashMap.keys cbrs
+          then do
+            lazyValue <- lazy do
+              branchValue <- Evaluation.evaluate env' defaultBranch
+              value' <- Evaluation.applySpine branchValue $ Domain.Spine args2 caseSpine
+              forceHead context value'
+            pure $ Domain.Glued head_ spine $ Domain.Lazy lazyValue
+          else pure value
+    Domain.Neutral
+      head_
+      spine@( Domain.Spine
+                args1
+                ( ( Domain.Branches env' (Syntax.LiteralBranches lbrs) (Just defaultBranch)
+                    , args2
+                    )
+                    Seq.:<| caseSpine
+                  )
+              ) -> do
+        covered <- coveredLiterals context head_ args1
+        if all (`HashSet.member` covered) $ OrderedHashMap.keys lbrs
+          then do
+            lazyValue <- lazy do
+              branchValue <- Evaluation.evaluate env' defaultBranch
+              value' <- Evaluation.applySpine branchValue $ Domain.Spine args2 caseSpine
+              forceHead context value'
+            pure $ Domain.Glued head_ spine $ Domain.Lazy lazyValue
+          else pure value
     Domain.Lazy lazyValue -> do
       value' <- force lazyValue
       forceHeadGlue context value'

src/Elaboration/Context/Type.hs

@@ -42,8 +42,8 @@ data Context (v :: Data.Kind.Type) = Context
   }
 
 data Equations = Equations
-  { equal :: HashMap Domain.Head [(Domain.Spine, Domain.Value)]
-  , notEqual :: HashMap Domain.Head [(Domain.Spine, HashSet Name.QualifiedConstructor, HashSet Literal)]
+  { equal :: HashMap Domain.Head [(Domain.Args, Domain.Value)]
+  , notEqual :: HashMap Domain.Head [(Domain.Args, HashSet Name.QualifiedConstructor, HashSet Literal)]
   }
 
 type CoveredConstructors = EnumMap Var (HashSet Name.QualifiedConstructor)

src/Elaboration/Equation.hs

@@ -89,42 +89,43 @@ equateM flexibility value1 value2 = do
           equateM flexibility target1 target2
 
     -- Neutrals
-    (Domain.Neutral head1 spine1, Domain.Neutral head2 spine2)
+    (Domain.Neutral head1 (Domain.Apps args1), Domain.Neutral head2 (Domain.Apps args2))
       | Flexibility.Rigid <- max (Domain.headFlexibility head1) flexibility
-      , Flexibility.Rigid <- max (Domain.headFlexibility head2) flexibility -> do
+      , Flexibility.Rigid <- max (Domain.headFlexibility head2) flexibility
+      , (fst <$> args1) == (fst <$> args2) -> do
           -- TODO: check both directions?
           ordering <- lift $ compareHeadDepths head1 head2
           case ordering of
-            LT -> solve head2 spine2 value1'
-            GT -> solve head1 spine1 value2'
-            EQ -> solve head2 spine2 value1'
-    (Domain.Neutral head1 spine1, _)
+            LT -> solve head2 args2 value1'
+            GT -> solve head1 args1 value2'
+            EQ -> solve head2 args2 value1'
+    (Domain.Neutral head1 (Domain.Apps args1), _)
       | Flexibility.Rigid <- max (Domain.headFlexibility head1) flexibility ->
-          solve head1 spine1 value2
-    (_, Domain.Neutral head2 spine2)
+          solve head1 args1 value2
+    (_, Domain.Neutral head2 (Domain.Apps args2))
       | Flexibility.Rigid <- max (Domain.headFlexibility head2) flexibility ->
-          solve head2 spine2 value1
+          solve head2 args2 value1
     _ ->
       throwIO Dunno
 
-solve :: Domain.Head -> Domain.Spine -> Domain.Value -> Equate v ()
-solve head_ spine value = do
+solve :: Domain.Head -> Domain.Args -> Domain.Value -> Equate v ()
+solve head_ args value = do
   context <- get
   context' <- lift do
     value' <- Context.forceHead context value
     case value' of
       Domain.Con con _ -> do
-        covered <- Context.coveredConstructors context head_ spine
+        covered <- Context.coveredConstructors context head_ args
         when (con `HashSet.member` covered) $
           throwIO Nope
       Domain.Lit lit -> do
-        covered <- Context.coveredLiterals context head_ spine
+        covered <- Context.coveredLiterals context head_ args
         when (lit `HashSet.member` covered) $
           throwIO Nope
       _ -> pure ()
     occurs context (== head_) Flexibility.Rigid value
-    occursSpine context isMeta Flexibility.Rigid spine
-    Context.define context head_ spine value
+    mapM_ (occurs context isMeta Flexibility.Rigid . snd) args
+    Context.define context head_ args value
   put context'
   where
     isMeta (Domain.Meta _) = True