diff --git a/src/Elaboration.hs b/src/Elaboration.hs index 7a21f94..5367c85 100644 --- a/src/Elaboration.hs +++ b/src/Elaboration.hs @@ -759,11 +759,9 @@ elaborateLets context declaredNames undefinedVars definedVars lets body mode = d . Syntax.Let bindings Index.Zero boundTerm <$> lets'' Just (previousSpan, var) -> do - case Context.lookupVarValue var context of - Just _ -> do - Context.report (Context.spanned span context) $ Error.DuplicateLetName surfaceName previousSpan - elaborateLets context declaredNames undefinedVars definedVars lets' body mode - Nothing -> do + value <- Context.forceHead context (Domain.Neutral (Domain.Var var) Domain.Empty) + case value of + (Domain.Neutral (Domain.Var sameVar) Domain.Empty) | var == sameVar -> do let type_ = Context.lookupVarType var context boundTerm <- Clauses.check context clauses' type_ @@ -781,12 +779,15 @@ elaborateLets context declaredNames undefinedVars definedVars lets body mode = d pure $ defines context values lets'' <- elaborateLets redefinedContext declaredNames undefinedVars' definedVars' lets' body mode pure $ Syntax.Let bindings index boundTerm <$> lets'' + _ -> do + Context.report (Context.spanned span context) $ Error.DuplicateLetName surfaceName previousSpan + elaborateLets context declaredNames undefinedVars definedVars lets' body mode where defines :: Context v -> Tsil (Var, Domain.Value) -> Context v defines = foldr' \(var, value) context' -> if isJust $ Context.lookupVarIndex var context' - then Context.defineWellOrdered context' var value + then Context.defineWellOrdered context' (Domain.Var var) Domain.Empty value else context' forceExpectedTypeHead :: Context v -> Mode result -> M (Mode result) diff --git a/src/Elaboration/Context.hs b/src/Elaboration/Context.hs index 3bd4222..c575894 100644 --- a/src/Elaboration/Context.hs +++ b/src/Elaboration/Context.hs @@ -30,6 +30,7 @@ import qualified Data.EnumSet as EnumSet import Data.HashMap.Lazy (HashMap) import qualified Data.HashMap.Lazy as HashMap import Data.HashSet (HashSet) +import qualified Data.HashSet as HashSet import Data.IORef.Lifted import Data.IntSeq (IntSeq) import qualified Data.IntSeq as IntSeq @@ -96,7 +97,27 @@ toEnvironment toEnvironment context = Environment { indices = context.indices - , values = mempty + , values = + EnumMap.fromList + $ mapMaybe + ( \(head_, spines) -> + case head_ of + Domain.Var var -> do + let emptySpineValues = + mapMaybe + ( \(spine, value) -> + case spine of + Domain.Empty -> Just (var, value) + _ -> Nothing + ) + spines + case emptySpineValues of + [value] -> Just value + [] -> Nothing + _ -> panic "multiple spine values" + _ -> Nothing + ) + $ HashMap.toList context.equations.equal , glueableBefore = Index.Zero } @@ -166,6 +187,14 @@ coveredConstructors context head_ spine = fst <$> coveredConstructorsAndLiterals coveredLiterals :: Context v -> Domain.Head -> Domain.Spine -> M (HashSet Literal) coveredLiterals context head_ spine = snd <$> coveredConstructorsAndLiterals context head_ spine +withCoveredConstructors :: Context v -> Domain.Head -> Domain.Spine -> HashSet Name.QualifiedConstructor -> Context v +withCoveredConstructors context head spine constructors = + context {equations = context.equations {notEqual = HashMap.insertWith (<>) head [(spine, constructors, mempty)] context.equations.notEqual}} + +withCoveredLiterals :: Context v -> Domain.Head -> Domain.Spine -> HashSet Literal -> Context v +withCoveredLiterals context head spine literals = + context {equations = context.equations {notEqual = HashMap.insertWith (<>) head [(spine, mempty, literals)] context.equations.notEqual}} + ------------------------------------------------------------------------------- -- Extension @@ -295,14 +324,15 @@ define :: Context v -> Domain.Head -> Domain.Spine -> Domain.Value -> M (Context define context head_ spine value = do deps <- evalStateT (freeVars context value) mempty let context' = defineWellOrdered context head_ spine value - (pre, post) = - Tsil.partition (`EnumSet.member` deps) $ - IntSeq.toTsil context'.boundVars - pure - context' - { boundVars = - IntSeq.fromTsil pre <> IntSeq.fromTsil post - } + context'' + | EnumSet.null deps = context' + | otherwise = + context' + { boundVars = + IntSeq.fromTsil pre <> IntSeq.fromTsil post + } + (pre, post) = Tsil.partition (`EnumSet.member` deps) $ IntSeq.toTsil context'.boundVars + pure context'' -- TODO: Move freeVars diff --git a/src/Elaboration/Equation.hs b/src/Elaboration/Equation.hs index 0f7f611..6aa80e9 100644 --- a/src/Elaboration/Equation.hs +++ b/src/Elaboration/Equation.hs @@ -1,7 +1,5 @@ {-# LANGUAGE BlockArguments #-} {-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE OverloadedRecordDot #-} -{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE NoFieldSelectors #-} @@ -15,9 +13,7 @@ import qualified Core.Bindings as Bindings import qualified Core.Domain as Domain import qualified Core.Evaluation as Evaluation import qualified Core.Syntax as Syntax -import qualified Data.EnumMap as EnumMap -import qualified Data.IntSeq as IntSeq -import qualified Data.OrderedHashMap as OrderedHashMap +import qualified Data.HashSet as HashSet import qualified Data.Tsil as Tsil import Elaboration.Context (Context) import qualified Elaboration.Context as Context @@ -25,83 +21,29 @@ import Elaboration.Depth (compareHeadDepths) import qualified Environment import Flexibility (Flexibility) import qualified Flexibility -import Index -import qualified Index.Map import Monad -import Name (Name) import Protolude hiding (catch, force, throwIO) import Telescope (Telescope) import qualified Telescope -import Var data Error = Nope | Dunno deriving (Eq, Ord, Show, Exception) -data EquationState v = EquationState - { context :: !(Context v) - , touchableBefore :: !(Index (Succ v)) - } - -type Equate v = StateT (EquationState v) M +type Equate v = StateT (Context v) M equate :: Context v -> Flexibility -> Domain.Value -> Domain.Value -> M (Context v) equate context flexibility value1 value2 = - (.context) - <$> execStateT - (equateM flexibility value1 value2) - EquationState - { context = context - , touchableBefore = Index.Zero - } - -isTouchableVar :: Var -> Equate v Bool -isTouchableVar var = do - touchableIndex <- gets (.touchableBefore) - context <- gets (.context) - pure case Context.lookupVarIndex var context of - Just varIndex -> Index.Succ varIndex > touchableIndex - Nothing -> False - -isTouchable :: Domain.Head -> Equate v Bool -isTouchable head_ = case head_ of - Domain.Meta _ -> pure False - Domain.Var var -> isTouchableVar var - Domain.Global _ -> pure True - -extend :: Name -> Domain.Type -> (Var -> Equate (Succ v) a) -> Equate v a -extend name type_ k = do - st <- get - (result, st') <- lift do - (context', var) <- Context.extend st.context name type_ - runStateT (k var) st {context = context', touchableBefore = Index.Succ st.touchableBefore} - put st' {context = unextend st'.context, touchableBefore = st.touchableBefore} - pure result - -unextend :: Context (Succ v) -> Context v -unextend context = - case (context.indices, context.boundVars) of - (indices Index.Map.:> var, boundVars IntSeq.:> _) -> - context - { Context.varNames = EnumMap.delete var context.varNames - , Context.indices = indices - , Context.types = EnumMap.delete var context.types - , Context.boundVars = boundVars - } - _ -> - panic "Equation.unextend" + execStateT + (equateM flexibility value1 value2) + context contextual1 :: (Context v -> a -> M b) -> a -> Equate v b contextual1 f x = do - c <- gets (.context) + c <- get lift $ f c x -contextual2 :: (Context v -> a -> b -> M c) -> a -> b -> Equate v c -contextual2 f x y = do - c <- gets (.context) - lift $ f c x y - equateM :: Flexibility -> Domain.Value -> Domain.Value -> Equate v () equateM flexibility value1 value2 = do value1' <- contextual1 Context.forceHeadGlue value1 @@ -137,71 +79,43 @@ equateM flexibility value1 value2 = do equateM flexibility value1'' value2' (_, Domain.Glued _ _ value2'') -> equateM flexibility value1' value2'' - (Domain.Lam bindings1 type1 plicity1 closure1, Domain.Lam _ type2 plicity2 closure2) - | plicity1 == plicity2 -> - equateAbstraction (Bindings.toName bindings1) type1 closure1 type2 closure2 - (Domain.Pi binding1 domain1 plicity1 targetClosure1, Domain.Pi _ domain2 plicity2 targetClosure2) - | plicity1 == plicity2 -> - equateAbstraction (Binding.toName binding1) domain1 targetClosure1 domain2 targetClosure2 - (Domain.Pi binding1 domain1 plicity1 targetClosure1, Domain.Fun domain2 plicity2 target2) - | plicity1 == plicity2 -> do - equateM flexibility domain2 domain1 - extend (Binding.toName binding1) domain1 \var -> do - target1 <- lift $ Evaluation.evaluateClosure targetClosure1 $ Domain.var var - equateM flexibility target1 target2 - (Domain.Fun domain1 plicity1 target1, Domain.Pi binding2 domain2 plicity2 targetClosure2) - | plicity1 == plicity2 -> do - equateM flexibility domain2 domain1 - extend (Binding.toName binding2) domain2 \var -> do - target2 <- lift $ Evaluation.evaluateClosure targetClosure2 $ Domain.var var - equateM flexibility target1 target2 (Domain.Fun domain1 plicity1 target1, Domain.Fun domain2 plicity2 target2) | plicity1 == plicity2 -> do equateM flexibility domain2 domain1 equateM flexibility target1 target2 - -- Eta expand - (Domain.Lam bindings1 type1 plicity1 closure1, v2) -> - extend (Bindings.toName bindings1) type1 \var -> do - let varValue = Domain.var var - body1 <- lift $ Evaluation.evaluateClosure closure1 varValue - body2 <- lift $ Evaluation.apply v2 plicity1 varValue - equateM flexibility body1 body2 - (v1, Domain.Lam bindings2 type2 plicity2 closure2) -> - extend (Bindings.toName bindings2) type2 \var -> do - let varValue = Domain.var var - body1 <- lift $ Evaluation.apply v1 plicity2 varValue - body2 <- lift $ Evaluation.evaluateClosure closure2 varValue - equateM flexibility body1 body2 - -- Vars (Domain.Neutral head1 spine1, _) - | Flexibility.Rigid <- flexibility -> - solve head1 spine1 value2' + | Flexibility.Rigid <- max (Domain.headFlexibility head1) flexibility -> + solve head1 spine1 value2 (_, Domain.Neutral head2 spine2) - | Flexibility.Rigid <- flexibility -> - solve head2 spine2 value1' + | Flexibility.Rigid <- max (Domain.headFlexibility head2) flexibility -> + solve head2 spine2 value1 _ -> throwIO Dunno - where - equateAbstraction name type1 closure1 type2 closure2 = do - equateM flexibility type1 type2 - - extend name type1 \var -> do - let varValue = Domain.var var - body1 <- lift $ Evaluation.evaluateClosure closure1 varValue - body2 <- lift $ Evaluation.evaluateClosure closure2 varValue - equateM flexibility body1 body2 - solve head_ spine value = do - touchable <- isTouchable head_ - if touchable - then do - occurs head_ Flexibility.Rigid value - spine' <- touchableSpine spine - context' <- contextual2 Context.define head_ spine' value - modify \st -> st {context = context'} - else throwIO Dunno +solve :: Domain.Head -> Domain.Spine -> Domain.Value -> Equate v () +solve head_ spine 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 + when (con `HashSet.member` covered) $ + throwIO Nope + Domain.Lit lit -> do + covered <- Context.coveredLiterals context head_ spine + 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 + put context' + where + isMeta (Domain.Meta _) = True + isMeta _ = False equateSpines :: Flexibility @@ -218,188 +132,78 @@ equateSpines flexibility spine1 spine2 = _ -> throwIO Dunno -withInstantiatedTele - :: Domain.Environment v1 - -> Telescope Bindings Syntax.Type Syntax.Term v1 - -> (forall v'. Domain.Value -> Equate v' k) - -> Equate v k -withInstantiatedTele env tele k = - case tele of - Telescope.Empty body -> do - body' <- lift $ Evaluation.evaluate env body - k body' - Telescope.Extend bindings type_ _plicity tele' -> do - type' <- lift $ Evaluation.evaluate env type_ - extend (Bindings.toName bindings) type' \var -> - withInstantiatedTele (Environment.extendVar env var) tele' k - -occurs :: Domain.Head -> Flexibility -> Domain.Value -> Equate v () -occurs occ flexibility value = do - value' <- contextual1 Context.forceHeadGlue value +occurs :: Context v -> (Domain.Head -> Bool) -> Flexibility -> Domain.Value -> M () +occurs context occ flexibility value = do + value' <- Context.forceHeadGlue context value case value' of - Domain.Neutral hd spine -> do - occursHead occ flexibility hd - Domain.mapM_ (occursElimination occ (max (Domain.headFlexibility hd) flexibility)) spine + Domain.Neutral hd spine + | occ hd -> + throwIO case flexibility of + Flexibility.Rigid -> Nope + Flexibility.Flexible -> Dunno + | otherwise -> + occursSpine context occ (max (Domain.headFlexibility hd) flexibility) spine Domain.Con _ args -> - mapM_ (occurs occ flexibility . snd) args + mapM_ (occurs context occ flexibility . snd) args Domain.Lit _ -> pure () Domain.Glued (Domain.Var _) _ value'' -> - occurs occ flexibility value'' + occurs context occ flexibility value'' Domain.Glued hd spine value'' -> - occurs occ Flexibility.Flexible (Domain.Neutral hd spine) `catch` \(_ :: Error) -> - occurs occ flexibility value'' + occurs context occ Flexibility.Flexible (Domain.Neutral hd spine) `catch` \(_ :: Error) -> + occurs context occ flexibility value'' Domain.Lazy lazyValue -> do - value'' <- lift $ force lazyValue - occurs occ flexibility value'' + value'' <- force lazyValue + occurs context occ flexibility value'' Domain.Lam bindings type_ _ closure -> occursAbstraction (Bindings.toName bindings) type_ closure Domain.Pi binding domain _ targetClosure -> occursAbstraction (Binding.toName binding) domain targetClosure Domain.Fun domain _ target -> do - occurs occ flexibility domain - occurs occ flexibility target + occurs context occ flexibility domain + occurs context occ flexibility target where occursAbstraction name type_ closure = do - occurs occ flexibility type_ - extend name type_ \var -> do - let varValue = Domain.var var - body <- lift $ Evaluation.evaluateClosure closure varValue - occurs occ flexibility body - -occursHead :: Domain.Head -> Flexibility -> Domain.Head -> Equate v () -occursHead occ flexibility hd - | hd == occ = throwIO case flexibility of - Flexibility.Rigid -> Nope - Flexibility.Flexible -> Dunno - | otherwise = - case hd of - Domain.Var var -> do - touchable <- isTouchableVar var - unless touchable $ - throwIO case flexibility of - Flexibility.Rigid -> Nope - Flexibility.Flexible -> Dunno - Domain.Global _ -> pure () - Domain.Meta _ -> pure () - -occursElimination :: Domain.Head -> Flexibility -> Domain.Elimination -> Equate v () -occursElimination occ flexibility elimination = + occurs context occ flexibility type_ + (context', var) <- Context.extend context name type_ + let varValue = Domain.var var + body <- Evaluation.evaluateClosure closure varValue + occurs context' occ flexibility body + +occursSpine :: Context v -> (Domain.Head -> Bool) -> Flexibility -> Domain.Spine -> M () +occursSpine context occ flexibility = + Domain.mapM_ $ occursElimination context occ flexibility + +occursElimination :: Context v -> (Domain.Head -> Bool) -> Flexibility -> Domain.Elimination -> M () +occursElimination context occ flexibility elimination = case elimination of - Domain.App _plicity arg -> occurs occ flexibility arg - Domain.Case branches -> occursBranches occ flexibility branches + Domain.App _plicity arg -> occurs context occ flexibility arg + Domain.Case branches -> occursBranches context occ flexibility branches -occursBranches :: Domain.Head -> Flexibility -> Domain.Branches -> Equate v () -occursBranches occ flexibility (Domain.Branches outerEnv branches defaultBranch) = do +occursBranches :: Context v -> (Domain.Head -> Bool) -> Flexibility -> Domain.Branches -> M () +occursBranches context occ flexibility (Domain.Branches outerEnv branches defaultBranch) = do case branches of Syntax.ConstructorBranches _ constructorBranches -> - forM_ constructorBranches $ mapM_ $ occursTele outerEnv + forM_ constructorBranches $ mapM_ $ occursTele context outerEnv Syntax.LiteralBranches literalBranches -> forM_ literalBranches $ - mapM_ \branch -> - occursTele outerEnv $ Telescope.Empty branch - forM_ defaultBranch \branch -> - occursTele outerEnv $ Telescope.Empty branch + mapM_ $ + occursTele context outerEnv . Telescope.Empty + forM_ defaultBranch $ + occursTele context outerEnv . Telescope.Empty where occursTele - :: Domain.Environment v1 - -> Telescope Bindings Syntax.Type Syntax.Term v1 - -> Equate v () - occursTele env tele = - case tele of - Telescope.Extend bindings type_ _plicity tele' -> do - type' <- lift $ Evaluation.evaluate env type_ - occurs occ flexibility type' - extend (Bindings.toName bindings) type' \var -> - occursTele - (Environment.extendVar env var) - tele' - Telescope.Empty body -> do - body' <- lift $ Evaluation.evaluate env body - occurs occ flexibility body' - -touchableValue :: Index (Succ v) -> Domain.Value -> Equate v Domain.Value -touchableValue locals value = do - value' <- contextual1 Context.forceHeadGlue value - case value' of - Domain.Neutral hd spine -> do - touchableHead locals hd - Domain.mapM_ (touchableElimination locals) spine - Domain.Con _ args -> - mapM_ (touchableValue locals . snd) args - Domain.Lit _ -> - pure () - Domain.Glued (Domain.Var _) _ value'' -> - touchableValue locals value'' - Domain.Glued hd spine value'' -> - touchableValue locals (Domain.Neutral hd spine) `catch` \(_ :: Error) -> - touchableValue locals value'' - Domain.Lazy lazyValue -> do - value'' <- lift $ force lazyValue - touchableValue locals value'' - Domain.Lam bindings type_ _ closure -> - occursAbstraction (Bindings.toName bindings) type_ closure - Domain.Pi binding domain _ targetClosure -> - occursAbstraction (Binding.toName binding) domain targetClosure - Domain.Fun domain _ target -> do - touchableValue locals domain - touchableValue locals target - where - occursAbstraction name type_ closure = do - touchableValue locals type_ - extend name type_ \var -> do - let varValue = Domain.var var - body <- lift $ Evaluation.evaluateClosure closure varValue - touchableValue locals body - -touchableHead :: Index (Succ v) -> Domain.Head -> Equate v Domain.Head -touchableHead locals hd = - case hd of - Domain.Var var -> do - context <- gets (.context) - case Context.lookupVarIndex var context of - Just varIndex - | Index.Succ varIndex <= locals -> pure hd - | otherwise -> do - touchable <- isTouchableVar var - unless touchable $ throwIO Dunno - Nothing -> throwIO Dunno - Domain.Global _ -> pure hd - Domain.Meta _ -> throwIO Dunno - -touchableElimination :: Index (Succ v) -> Domain.Elimination -> Equate v Domain.Elimination -touchableElimination locals elimination = - case elimination of - Domain.App _plicity arg -> touchableValue locals arg - Domain.Case branches -> touchableBranches locals branches - -touchableBranches :: Index (Succ v) -> Domain.Branches -> Equate v Domain.Branches -touchableBranches locals (Domain.Branches outerEnv branches defaultBranch) = do - case branches of - Syntax.ConstructorBranches _ constructorBranches -> - forM_ constructorBranches $ mapM_ $ touchableTele outerEnv - Syntax.LiteralBranches literalBranches -> - forM_ literalBranches $ - mapM_ \branch -> - touchableTele locals outerEnv $ Telescope.Empty branch - forM_ defaultBranch \branch -> - touchableTele outerEnv locals $ Telescope.Empty branch - where - touchableTele - :: Index (Succ v) - -> Domain.Environment v1 - -> Telescope Bindings Syntax.Type Syntax.Term v1 - -> Equate v (Telescope Bindings Syntax.Type Syntax.Term v1) - touchableTele locals' env tele = + :: Context v1 + -> Domain.Environment v2 + -> Telescope Bindings Syntax.Type Syntax.Term v2 + -> M () + occursTele context' env tele = case tele of Telescope.Extend bindings type_ _plicity tele' -> do - type' <- lift $ Evaluation.evaluate env type_ - touchableValue locals type' - extend (Bindings.toName bindings) type' \var -> - touchableTele - (Index.Succ locals') - (Environment.extendVar env var) - tele' + type' <- Evaluation.evaluate env type_ + occurs context' occ flexibility type' + (context'', var) <- Context.extend context (Bindings.toName bindings) type' + occursTele context'' (Environment.extendVar env var) tele' Telescope.Empty body -> do - body' <- lift $ Evaluation.evaluate env body - touchableValue locals body' + body' <- Evaluation.evaluate env body + occurs context' occ flexibility body' diff --git a/src/Elaboration/Matching.hs b/src/Elaboration/Matching.hs index fa0ba4a..6dca3f5 100644 --- a/src/Elaboration/Matching.hs +++ b/src/Elaboration/Matching.hs @@ -39,10 +39,10 @@ import qualified Data.Tsil as Tsil import {-# SOURCE #-} qualified Elaboration import Elaboration.Context (Context) import qualified Elaboration.Context as Context +import qualified Elaboration.Equation as Equation 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 import qualified Error import qualified Flexibility @@ -635,10 +635,10 @@ splitConstructorOr context config matches k = k match : matches' -> case match of - Match scrutinee (Domain.Neutral head spine) _ (Pattern span (Con _ constr _)) type_ -> - splitConstructor context config scrutinee head spine span constr type_ - Match scrutinee (Domain.Neutral head spine) _ (Pattern span (Lit lit)) type_ -> - splitLiteral context config scrutinee head spine span lit type_ + Match scrutinee (Domain.Neutral head_ spine) _ (Pattern span (Con _ constr _)) type_ -> + splitConstructor context config scrutinee head_ spine span constr type_ + Match scrutinee (Domain.Neutral head_ spine) _ (Pattern span (Lit lit)) type_ -> + splitLiteral context config scrutinee head_ spine span lit type_ _ -> splitConstructorOr context config matches' k @@ -695,9 +695,9 @@ splitConstructor outerContext config scrutineeValue scrutineeHead scrutineeSpine matchedConstructors <- OrderedHashMap.fromListWith (<>) . concat - <$> takeWhileM - (fmap $ not . null) - (findConstructorMatches scrutineeVar . (.matches) <$> config.clauses) + <$> mapWhileM + (fmap $ \xs -> if null xs then Nothing else Just xs) + (findConstructorMatches context scrutineeHead scrutineeSpine . (.matches) <$> config.clauses) branches <- forM (OrderedHashMap.toList matchedConstructors) \(qualifiedConstr@(Name.QualifiedConstructor _ constr), patterns) -> do let constrType = @@ -715,20 +715,13 @@ splitConstructor outerContext config scrutineeValue scrutineeHead scrutineeSpine defaultBranch <- if OrderedHashMap.size matchedConstructors == length constructors then pure Nothing - else - Just - <$> check - context - -- TODO - -- { Context.coveredConstructors = - -- EnumMap.insertWith - -- (<>) - -- scrutineeVar - -- (HashSet.fromMap $ void $ OrderedHashMap.toMap matchedConstructors) - -- context.coveredConstructors - -- } - config - Postponement.CanPostpone + else do + let context' = + Context.withCoveredConstructors context scrutineeHead scrutineeSpine $ + HashSet.fromMap $ + void $ + OrderedHashMap.toMap matchedConstructors + Just <$> check context' config Postponement.CanPostpone scrutinee <- Elaboration.readback context scrutineeValue @@ -761,7 +754,7 @@ splitConstructor outerContext config scrutineeValue scrutineeHead scrutineeSpine Constraint -> pure (Bindings.Unspanned piName, patterns) - (context', fieldVar) <- Context.extendBefore context scrutineeVar bindings domain + (context', fieldVar) <- Context.extend context (Bindings.toName bindings) domain let fieldValue = Domain.var fieldVar conArgs' = conArgs Tsil.:> (plicity, fieldValue) target <- Evaluation.evaluateClosure targetClosure fieldValue @@ -777,26 +770,25 @@ splitConstructor outerContext config scrutineeValue scrutineeHead scrutineeSpine SuggestedName.nextImplicit context "x" patterns Constraint -> pure (Bindings.Unspanned "x", patterns) - (context', fieldVar) <- Context.extendBefore context scrutineeVar bindings domain + (context', fieldVar) <- Context.extend context (Bindings.toName bindings) domain let fieldValue = Domain.var fieldVar conArgs' = conArgs Tsil.:> (plicity, fieldValue) tele <- goConstrFields context' constr conArgs' target patterns' pure $ Telescope.Extend bindings domain'' plicity tele _ -> do - let context' = - Context.defineWellOrdered context scrutineeVar $ Domain.Con constr conArgs + context' <- Equation.equate context Flexibility.Rigid scrutineeValue $ Domain.Con constr conArgs result <- check context' config Postponement.CanPostpone pure $ Telescope.Empty result -takeWhileM :: Monad m => (a -> m Bool) -> [a] -> m [a] -takeWhileM p as = +mapWhileM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b] +mapWhileM f as = case as of [] -> pure [] a : as' -> do - b <- p a - if p a - then (a :) <$> takeWhileM p as' - else takeWhileM p as' + mb <- f a + case mb of + Nothing -> pure [] + Just b -> (b :) <$> mapWhileM f as' findConstructorMatches :: Context v @@ -809,7 +801,7 @@ findConstructorMatches context head_ spine matches = [] -> pure [] Match _ (Domain.Neutral head' spine') _ (Pattern _ (Con span constr patterns)) _ : matches' - | head == head' -> do + | head_ == head' -> do eq <- Unification.equalSpines context spine spine' if eq then ((constr, [(span, patterns)]) :) <$> findConstructorMatches context head_ spine matches' @@ -830,32 +822,24 @@ splitLiteral splitLiteral context config scrutineeValue scrutineeHead scrutineeSpine span lit outerType = do matchedLiterals <- OrderedHashMap.fromListWith (<>) . concat - <$> takeWhileM - (fmap $ not . null) - (findLiteralMatches scrutineeHead spine . (.matches) <$> config.clauses) + <$> mapWhileM + (fmap $ \xs -> if null xs then Nothing else Just xs) + (findLiteralMatches context scrutineeHead scrutineeSpine . (.matches) <$> config.clauses) f <- Unification.tryUnify (Context.spanned span context) (Elaboration.inferLiteral lit) outerType branches <- forM (OrderedHashMap.toList matchedLiterals) \(int, spans) -> do - let context' = - Context.defineWellOrdered context scrutineeVar $ Domain.Lit int + let context' = Context.defineWellOrdered context scrutineeHead scrutineeSpine $ Domain.Lit int result <- check context' config Postponement.CanPostpone pure (int, (spans, f result)) - defaultBranch <- - Just - <$> check - context - -- TODO - -- { Context.coveredLiterals = - -- EnumMap.insertWith - -- (<>) - -- scrutineeVar - -- (HashSet.fromMap $ void $ OrderedHashMap.toMap matchedLiterals) - -- context.coveredLiterals - -- } - config - Postponement.CanPostpone + defaultBranch <- do + let context' = + Context.withCoveredLiterals context scrutineeHead scrutineeSpine $ + HashSet.fromMap $ + void $ + OrderedHashMap.toMap matchedLiterals + Just <$> check context' config Postponement.CanPostpone scrutinee <- Elaboration.readback context scrutineeValue @@ -870,13 +854,13 @@ findLiteralMatches findLiteralMatches context head_ spine matches = case matches of [] -> - [] + pure [] Match _ (Domain.Neutral head' spine') _ (Pattern span (Lit lit)) _ : matches' | head_ == head' -> do eq <- Unification.equalSpines context spine spine' if eq - then ((lit, [span]) :) <$> findLiteralMatches context_ head_ spine matches' - else findLiteralMatches context_ head_ spine matches' + then ((lit, [span]) :) <$> findLiteralMatches context head_ spine matches' + else findLiteralMatches context head_ spine matches' _ : matches' -> findLiteralMatches context head_ spine matches' @@ -895,24 +879,22 @@ splitEqualityOr context config matches k = match : matches' -> case match of Match - _ - (Domain.Neutral (Domain.Var var) Domain.Empty) + scrutineeValue + scrutineeValue' _ (Pattern _ Wildcard) (Builtin.Equals type_ value1 value2) -> do - unificationResult <- try $ Indices.unify context Flexibility.Rigid value1 value2 + unificationResult <- try $ do + context' <- Equation.equate context Flexibility.Rigid value1 value2 + Equation.equate context' Flexibility.Rigid scrutineeValue' $ Builtin.Refl type_ value1 value2 case unificationResult of - Left Indices.Nope -> - check - context - config {clauses = drop 1 config.clauses} - Postponement.CanPostpone - Left Indices.Dunno -> + Left Equation.Nope -> + check context config {clauses = drop 1 config.clauses} Postponement.CanPostpone + Left Equation.Dunno -> splitEqualityOr context config matches' k Right context' -> do - context'' <- Context.define context' var $ Builtin.Refl type_ value1 value2 - result <- check context'' config Postponement.CanPostpone - scrutinee <- Elaboration.readback context'' $ Domain.var var + result <- check context' config Postponement.CanPostpone + scrutinee <- Elaboration.readback context' scrutineeValue pure $ Syntax.Case scrutinee @@ -964,11 +946,11 @@ uninhabitedType context fuel covered type_ = do type' <- Context.forceHead context type_ case type' of Builtin.Equals _ value1 value2 -> do - result <- try $ Indices.unify context Flexibility.Rigid value1 value2 + result <- try $ Equation.equate context Flexibility.Rigid value1 value2 pure $ case result of - Left Indices.Nope -> + Left Equation.Nope -> True - Left Indices.Dunno -> + Left Equation.Dunno -> False Right _ -> False diff --git a/src/Elaboration/Unification.hs b/src/Elaboration/Unification.hs index a874361..e43d3e3 100644 --- a/src/Elaboration/Unification.hs +++ b/src/Elaboration/Unification.hs @@ -1,6 +1,5 @@ {-# LANGUAGE BlockArguments #-} {-# LANGUAGE DuplicateRecordFields #-} -{-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -28,7 +27,6 @@ import Elaboration.Context (Context) import qualified Elaboration.Context as Context import Elaboration.Depth (compareHeadDepths) import qualified Elaboration.Meta as Meta -import Environment (Environment (Environment)) import qualified Environment import qualified Error import Extra @@ -44,7 +42,6 @@ import qualified Name import Plicity import Protolude hiding (catch, check, evaluate, force, head, throwIO) import qualified Query -import qualified Query.Mapped as Mapped import Rock import Telescope (Telescope) import qualified Telescope @@ -334,7 +331,7 @@ unifySpines context flexibility spine1 spine2 = equalSpines :: Context v -> Domain.Spine -> Domain.Spine -> M Bool equalSpines context spine1 spine2 = (True <$ unifySpines context Flexibility.Flexible spine1 spine2) - `catch` \(_ :: Error) -> pure False + `catch` \(_ :: Error.Elaboration) -> pure False unifyBranches :: Context v @@ -612,10 +609,9 @@ checkSolution outerContext meta vars value = do PartialRenaming { occurs = Just meta , environment = - Environment - { indices = Index.Map indices - , values = outerContext.values - , glueableBefore = Index $ IntSeq.length indices + (Context.toEnvironment outerContext) + { Environment.indices = Index.Map indices + , Environment.glueableBefore = Index $ IntSeq.length indices } , renamingFlexibility = Flexibility.Rigid } @@ -648,10 +644,9 @@ addAndRenameLambdas outerContext meta plicities vars term = PartialRenaming { occurs = Just meta , environment = - Environment - { indices = Index.Map vars' - , values = outerContext.values - , glueableBefore = Index $ IntSeq.length vars' + (Context.toEnvironment outerContext) + { Environment.indices = Index.Map vars' + , Environment.glueableBefore = Index $ IntSeq.length vars' } , renamingFlexibility = Flexibility.Rigid } @@ -712,7 +707,7 @@ renameValue outerContext renaming value = do if EnumSet.member occursMeta metas then -- The meta solution might contain `occurs`, so we need to force. renameValue outerContext renaming value'' - else -- The solved meta (`meta`) does contain the meta we're solving + else -- The solved meta (`meta`) doesn't contain the meta we're solving -- (`occursMeta`) in scope, so we can try without unfolding -- `meta`.