wip

src/Elaboration.hs

@@ -626,10 +626,10 @@ elaborateWith context spannedTerm@(Surface.Term span term) mode canPostpone = do
       case mode of
         Infer _ -> do
           expectedType <- Context.newMetaType context
-          term' <- Matching.checkCase context scrutinee' scrutineeType branches expectedType Postponement.CanPostpone
+          term' <- Matching.checkCase context scrutinee' scrutineeType branches expectedType
           pure $ Inferred (Syntax.Spanned span term') expectedType
         Check expectedType -> do
-          term' <- Matching.checkCase context scrutinee' scrutineeType branches expectedType Postponement.CanPostpone
+          term' <- Matching.checkCase context scrutinee' scrutineeType branches expectedType
           pure $ Checked $ Syntax.Spanned span term'
     (Surface.App function@(Surface.Term functionSpan _) argument@(Surface.Term argumentSpan _), _) -> do
       (function', functionType) <- inferAndInsertMetas context UntilExplicit function $ getModeExpectedTypeName context mode

src/Elaboration/Context.hs

@@ -78,18 +78,18 @@ data Context (v :: Data.Kind.Type) = Context
   , boundVars :: IntSeq Var
   , metas :: !(IORef (Meta.State M))
   , postponed :: !(IORef Postponed.Checks)
-  , coveredConstructors :: CoveredConstructors
-  , coveredLiterals :: CoveredLiterals
+  , equations :: !Equations
   , errors :: !(IORef (Tsil Error))
   }
 
+data Equations = Equations
+  { equal :: HashMap Domain.Head [(Domain.Spine, Domain.Value)]
+  , notEqual :: HashMap Domain.Head [(Domain.Spine, HashSet Name.QualifiedConstructor, HashSet Literal)]
+  }
+
 moduleName :: Context v -> Name.Module
 moduleName context = context.definitionName.moduleName
 
-type CoveredConstructors = EnumMap Var (HashSet Name.QualifiedConstructor)
-
-type CoveredLiterals = EnumMap Var (HashSet Literal)
-
 toEnvironment
   :: Context v
   -> Domain.Environment v
@@ -120,8 +120,7 @@ empty definitionKind definitionName = do
       , metas = ms
       , postponed = ps
       , errors = es
-      , coveredConstructors = mempty
-      , coveredLiterals = mempty
+      , equations = Equations mempty mempty
       }
 
 emptyFrom :: Context v -> Context Void
@@ -140,8 +139,7 @@ emptyFrom context =
     , metas = context.metas
     , postponed = context.postponed
     , errors = context.errors
-    , coveredConstructors = mempty
-    , coveredLiterals = mempty
+    , equations = Equations mempty mempty
     }
 
 spanned :: Span.Relative -> Context v -> Context v

src/Elaboration/Matching.hs

@@ -24,9 +24,7 @@ import qualified Core.Domain.Pattern as Domain.Pattern
 import qualified Core.Domain.Telescope as Domain (Telescope)
 import qualified Core.Domain.Telescope as Domain.Telescope
 import qualified Core.Evaluation as Evaluation
-import qualified Core.Readback as Readback
 import qualified Core.Syntax as Syntax
-import qualified Data.EnumMap as EnumMap
 import Data.HashMap.Lazy (HashMap)
 import qualified Data.HashMap.Lazy as HashMap
 import Data.HashSet (HashSet)
@@ -42,6 +40,7 @@ import {-# SOURCE #-} qualified Elaboration
 import Elaboration.Context (Context)
 import qualified Elaboration.Context as Context
 import qualified Elaboration.Matching.SuggestedName as SuggestedName
+import qualified Elaboration.Meta as Meta
 import qualified Elaboration.Unification as Unification
 import qualified Elaboration.Unification.Indices as Indices
 import qualified Environment
@@ -170,105 +169,27 @@ checkCase
   -> Domain.Type
   -> [(Surface.Pattern, Surface.Term)]
   -> Domain.Type
-  -> Postponement.CanPostpone
   -> M (Syntax.Term v)
-checkCase context scrutinee scrutineeType branches expectedType canPostpone = do
+checkCase context scrutinee scrutineeType branches expectedType = do
   skippedContext <- Context.skip context
   scrutineeValue <- Elaboration.evaluate skippedContext scrutinee
-  blockingMetaOrIsPatternScrutinee <- runExceptT $ isPatternValue context scrutineeValue
-  case (canPostpone, blockingMetaOrIsPatternScrutinee) of
-    (Postponement.CanPostpone, Left blockingMeta) ->
-      postponeCaseCheck context scrutinee scrutineeType branches expectedType blockingMeta
-    _ -> do
-      (context', var) <-
-        if fromRight False blockingMetaOrIsPatternScrutinee
-          then Context.extendDef context "scrutinee" scrutineeValue scrutineeType
-          else Context.extend context "scrutinee" scrutineeType
-
-      let scrutineeVarValue =
-            Domain.var var
-      usedClauses <- newIORef mempty
-      term <-
-        checkWithCoverage
-          context'
-          Config
-            { expectedType = expectedType
-            , scrutinees = pure (Explicit, scrutineeVarValue)
-            , clauses =
-                [ Clause
-                  { span = Span.add patSpan rhsSpan
-                  , matches = [Match scrutineeVarValue scrutineeVarValue Explicit (unresolvedPattern pat) scrutineeType]
-                  , rhs = rhs'
-                  }
-                | (pat@(Surface.Pattern patSpan _), rhs'@(Surface.Term rhsSpan _)) <- branches
-                ]
-            , usedClauses = usedClauses
-            , matchKind = Error.Branch
+  usedClauses <- newIORef mempty
+  checkWithCoverage
+    context
+    Config
+      { expectedType = expectedType
+      , scrutinees = pure (Explicit, scrutineeValue)
+      , clauses =
+          [ Clause
+            { span = Span.add patSpan rhsSpan
+            , matches = [Match scrutineeValue scrutineeValue Explicit (unresolvedPattern pat) scrutineeType]
+            , rhs = rhs'
             }
-      scrutineeType' <- Readback.readback (Context.toEnvironment context) scrutineeType
-      pure $
-        Syntax.Lets $
-          Syntax.LetType "scrutinee" scrutineeType' $
-            Syntax.Let "scrutinee" Index.Zero scrutinee $
-              Syntax.In term
-
-postponeCaseCheck
-  :: Context v
-  -> Syntax.Term (Index.Succ v)
-  -> Domain.Type
-  -> [(Surface.Pattern, Surface.Term)]
-  -> Domain.Type
-  -> Meta.Index
-  -> M (Syntax.Term v)
-postponeCaseCheck context scrutinee scrutineeType branches expectedType blockingMeta =
-  Elaboration.postpone context expectedType blockingMeta $
-    checkCase context scrutinee scrutineeType branches expectedType
-
-isPatternValue :: Context v -> Domain.Value -> ExceptT Meta.Index M Bool
-isPatternValue context value = do
-  value' <- lift $ Context.forceHead context value
-  case value' of
-    Domain.Neutral (Domain.Var _) Domain.Empty ->
-      pure True
-    Domain.Neutral (Domain.Var _) (_ Domain.:> _) ->
-      pure False
-    Domain.Neutral (Domain.Global _) _ ->
-      pure False
-    Domain.Neutral (Domain.Meta blockingMeta) _ ->
-      throwError blockingMeta
-    Domain.Lit _ ->
-      pure True
-    Domain.Con constr args -> do
-      constrTypeTele <- fetch $ Query.ConstructorType constr
-      let spine' =
-            dropTypeArgs constrTypeTele $ toList args
-
-      and <$> mapM (isPatternValue context . snd) spine'
-    Domain.Glued _ _ value'' ->
-      isPatternValue context value''
-    Domain.Lazy lazyValue -> do
-      value'' <- lift $ force lazyValue
-      isPatternValue context value''
-    Domain.Lam {} ->
-      pure False
-    Domain.Pi {} ->
-      pure False
-    Domain.Fun {} ->
-      pure False
-  where
-    dropTypeArgs
-      :: Telescope n t t' v
-      -> [(Plicity, value)]
-      -> [(Plicity, value)]
-    dropTypeArgs tele args =
-      case (tele, args) of
-        (Telescope.Empty _, _) ->
-          args
-        (Telescope.Extend _ _ plicity1 tele', (plicity2, _) : args')
-          | plicity1 == plicity2 ->
-              dropTypeArgs tele' args'
-        _ ->
-          panic "chooseBranch arg mismatch"
+          | (pat@(Surface.Pattern patSpan _), rhs'@(Surface.Term rhsSpan _)) <- branches
+          ]
+      , usedClauses = usedClauses
+      , matchKind = Error.Branch
+      }
 
 checkClauses
   :: Context v
@@ -411,17 +332,38 @@ checkForcedPattern context match =
     _ ->
       pure ()
 
+equalSpines :: Context v -> Domain.Spine -> Domain.Spine -> M Bool
+equalSpines context spine1 spine2 =
+  Context.try_ context $ Unification.unifySpines context Flexibility.Flexible spine1 spine2
+
+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 <- 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
+
 uncoveredScrutineePatterns
   :: Context v
   -> Domain.Value
   -> M [Domain.Pattern]
 uncoveredScrutineePatterns context value = do
   value' <- Context.forceHead context value
   case value' of
-    Domain.Neutral (Domain.Var v) Domain.Empty -> do
-      let covered =
-            EnumMap.findWithDefault mempty v context.coveredConstructors
-
+    Domain.Neutral head_ spine -> do
+      covered <- coveredConstructors context head_ spine
       case HashSet.toList covered of
         [] ->
           pure [Domain.Pattern.Wildcard]
@@ -446,12 +388,6 @@ uncoveredScrutineePatterns context value = do
                       ]
             _ ->
               panic "uncoveredScrutineePatterns non-data"
-    Domain.Neutral (Domain.Var _) (_ Domain.:> _) ->
-      pure []
-    Domain.Neutral (Domain.Meta _) _ ->
-      pure []
-    Domain.Neutral (Domain.Global _) _ ->
-      pure []
     Domain.Lit lit ->
       pure [Domain.Pattern.Lit lit]
     Domain.Con constr args -> do
@@ -550,14 +486,16 @@ simplifyMatch context canPostpone match@(Match value forcedValue plicity pat typ
               pure []
           | otherwise ->
               fail "Literal mismatch"
-        (Domain.Neutral (Domain.Var var) Domain.Empty, Con _ constr _)
-          | Just coveredConstrs <- EnumMap.lookup var context.coveredConstructors
-          , HashSet.member constr coveredConstrs ->
-              fail "Constructor already covered"
-        (Domain.Neutral (Domain.Var var) Domain.Empty, Lit lit)
-          | Just coveredLits <- EnumMap.lookup var context.coveredLiterals
-          , HashSet.member lit coveredLits ->
-              fail "Literal already covered"
+        (Domain.Neutral head_ spine, Con _ constr _) -> do
+          covered <- lift $ coveredConstructors context head_ spine
+          if HashSet.member constr covered
+            then fail "Constructor already covered"
+            else pure [match']
+        (Domain.Neutral head_ spine, Lit lit) -> do
+          covered <- lift $ coveredLiterals context head_ spine
+          if HashSet.member lit covered
+            then fail "Literal already covered"
+            else pure [match']
         _ ->
           pure [match']
 
@@ -804,13 +742,14 @@ splitConstructor outerContext config scrutineeValue scrutineeVar span (Name.Qual
                 Just
                   <$> check
                     context
-                      { Context.coveredConstructors =
-                          EnumMap.insertWith
-                            (<>)
-                            scrutineeVar
-                            (HashSet.fromMap $ void $ OrderedHashMap.toMap matchedConstructors)
-                            context.coveredConstructors
-                      }
+                    -- TODO
+                    -- { Context.coveredConstructors =
+                    --     EnumMap.insertWith
+                    --       (<>)
+                    --       scrutineeVar
+                    --       (HashSet.fromMap $ void $ OrderedHashMap.toMap matchedConstructors)
+                    --       context.coveredConstructors
+                    -- }
                     config
                     Postponement.CanPostpone
 
@@ -914,13 +853,14 @@ splitLiteral context config scrutineeValue scrutineeVar span lit outerType = do
     Just
       <$> check
         context
-          { Context.coveredLiterals =
-              EnumMap.insertWith
-                (<>)
-                scrutineeVar
-                (HashSet.fromMap $ void $ OrderedHashMap.toMap matchedLiterals)
-                context.coveredLiterals
-          }
+        -- TODO
+        -- { Context.coveredLiterals =
+        --     EnumMap.insertWith
+        --       (<>)
+        --       scrutineeVar
+        --       (HashSet.fromMap $ void $ OrderedHashMap.toMap matchedLiterals)
+        --       context.coveredLiterals
+        -- }
         config
         Postponement.CanPostpone
 
@@ -987,15 +927,28 @@ splitEqualityOr context config matches k =
           splitEqualityOr context config matches' k
 
 -------------------------------------------------------------------------------
+-- TODO use Core.TypeOf.typeOfHead
+typeOfHead :: Context v -> Domain.Head -> M Domain.Type
+typeOfHead context hd =
+  case hd of
+    Domain.Var var ->
+      pure $ Context.lookupVarType var context
+    Domain.Global global -> do
+      type_ <- fetch $ Query.ElaboratedType global
+      Evaluation.evaluate Environment.empty type_
+    Domain.Meta index -> do
+      solution <- Context.lookupMeta context index
+      Evaluation.evaluate Environment.empty $ Meta.entryType solution
 
 uninhabitedScrutinee :: Context v -> Domain.Value -> M Bool
 uninhabitedScrutinee context value = do
   value' <- Context.forceHead context value
   case value' of
-    Domain.Neutral (Domain.Var var) (Domain.Apps args) -> do
-      let varType = Context.lookupVarType var context
-      type_ <- Context.instantiateType context varType args
-      uninhabitedType context 1 (EnumMap.findWithDefault mempty var context.coveredConstructors) type_
+    Domain.Neutral head_ spine@(Domain.Apps args) -> do
+      headType_ <- typeOfHead context head_
+      type_ <- Context.instantiateType context headType_ args
+      covered <- coveredConstructors context head_ spine
+      uninhabitedType context 1 covered type_
     Domain.Con constr constructorArgs -> do
       constrType <- fetch $ Query.ConstructorType constr
       let args = snd <$> drop (Telescope.length constrType) (toList constructorArgs)
@@ -1009,7 +962,7 @@ uninhabitedType
   -> HashSet Name.QualifiedConstructor
   -> Domain.Type
   -> M Bool
-uninhabitedType context fuel coveredConstructors type_ = do
+uninhabitedType context fuel covered type_ = do
   type' <- Context.forceHead context type_
   case type' of
     Builtin.Equals _ value1 value2 -> do
@@ -1037,7 +990,7 @@ uninhabitedType context fuel coveredConstructors type_ = do
 
                   uncoveredConstructorTypes =
                     toList $
-                      OrderedHashMap.differenceFromMap qualifiedConstructors (HashSet.toMap coveredConstructors)
+                      OrderedHashMap.differenceFromMap qualifiedConstructors (HashSet.toMap covered)
 
               allM (uninhabitedConstrType context fuel) uncoveredConstructorTypes
             _ ->

src/Meta.hs

@@ -1,5 +1,3 @@
-{-# LANGUAGE DeriveAnyClass #-}
-{-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE OverloadedStrings #-}