{-# OPTIONS_GHC -Wunused-imports #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Agda.TypeChecking.Level.Solve where
import Control.Monad
import Control.Monad.Except
import qualified Data.Map.Strict as MapS
import Data.Maybe
import Agda.Interaction.Options
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Level
import Agda.TypeChecking.MetaVars.Mention
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.Utils.Functor
import Agda.Utils.Monad
defaultOpenLevelsToZero :: (PureTCM m, MonadMetaSolver m) => m a -> m a
defaultOpenLevelsToZero :: forall (m :: * -> *) a.
(PureTCM m, MonadMetaSolver m) =>
m a -> m a
defaultOpenLevelsToZero m a
f = m Bool -> m a -> m a -> m a
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (PragmaOptions -> Bool
optCumulativity (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) m a
f (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ do
(result, newMetas) <- m a -> m (a, LocalMetaStores)
forall (m :: * -> *) a.
ReadTCState m =>
m a -> m (a, LocalMetaStores)
metasCreatedBy m a
f
defaultLevelsToZero (openMetas newMetas)
return result
defaultLevelsToZero ::
forall m. (PureTCM m, MonadMetaSolver m) => LocalMetaStore -> m ()
defaultLevelsToZero :: forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m) =>
LocalMetaStore -> m ()
defaultLevelsToZero LocalMetaStore
xs = [MetaId] -> m ()
loop ([MetaId] -> m ()) -> m [MetaId] -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [MetaId] -> m [MetaId]
openLevelMetas (LocalMetaStore -> [MetaId]
forall k a. Map k a -> [k]
MapS.keys LocalMetaStore
xs)
where
loop :: [MetaId] -> m ()
loop :: [MetaId] -> m ()
loop [MetaId]
xs = do
let isOpen :: MetaId -> f Bool
isOpen MetaId
x = MetaInstantiation -> Bool
isOpenMeta (MetaInstantiation -> Bool) -> f MetaInstantiation -> f Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> f MetaInstantiation
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
x
xs <- (MetaId -> m Bool) -> [MetaId] -> m [MetaId]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM MetaId -> m Bool
forall {f :: * -> *}. ReadTCState f => MetaId -> f Bool
isOpen [MetaId]
xs
allMetaTypes <- getOpenMetas >>= traverse metaType
let notInTypeOfMeta MetaId
x = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ MetaId -> [Type] -> Bool
forall t. MentionsMeta t => MetaId -> t -> Bool
mentionsMeta MetaId
x [Type]
allMetaTypes
progress <- forM xs $ \MetaId
x -> do
cs <- (ProblemConstraint -> Bool)
-> [ProblemConstraint] -> [ProblemConstraint]
forall a. (a -> Bool) -> [a] -> [a]
filter (MetaId -> ProblemConstraint -> Bool
forall t. MentionsMeta t => MetaId -> t -> Bool
mentionsMeta MetaId
x) ([ProblemConstraint] -> [ProblemConstraint])
-> m [ProblemConstraint] -> m [ProblemConstraint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m [ProblemConstraint]
forall (m :: * -> *). ReadTCState m => m [ProblemConstraint]
getAllConstraints
if | notInTypeOfMeta x , all (`isUpperBoundFor` x) cs -> do
m <- lookupMeta x
TelV tel t <- telView =<< metaType x
addContext tel $ assignV DirEq x (teleArgs tel) (Level $ ClosedLevel 0) (AsTermsOf t)
return True
`catchError` \TCErr
_ -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
| otherwise -> return False
when (or progress) $ (loop xs)
openLevelMetas :: [MetaId] -> m [MetaId]
openLevelMetas :: [MetaId] -> m [MetaId]
openLevelMetas [MetaId]
xs = (MetaId -> m Bool) -> [MetaId] -> m [MetaId]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (Maybe InteractionId -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe InteractionId -> Bool)
-> (MetaId -> m (Maybe InteractionId)) -> MetaId -> m Bool
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> MetaId -> m (Maybe InteractionId)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe InteractionId)
isInteractionMeta) [MetaId]
xs
m [MetaId] -> ([MetaId] -> m [MetaId]) -> m [MetaId]
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (MetaId -> m Bool) -> [MetaId] -> m [MetaId]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM ((DoGeneralize -> Bool) -> m DoGeneralize -> m Bool
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (DoGeneralize -> DoGeneralize -> Bool
forall a. Eq a => a -> a -> Bool
== DoGeneralize
NoGeneralize) (m DoGeneralize -> m Bool)
-> (MetaId -> m DoGeneralize) -> MetaId -> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> m DoGeneralize
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m DoGeneralize
isGeneralizableMeta)
m [MetaId] -> ([MetaId] -> m [MetaId]) -> m [MetaId]
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (MetaId -> m Bool) -> [MetaId] -> m [MetaId]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM MetaId -> m Bool
isLevelMeta
isLevelMeta :: MetaId -> m Bool
isLevelMeta :: MetaId -> m Bool
isLevelMeta MetaId
x = do
TelV tel t <- Type -> m (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView (Type -> m (TelV Type)) -> m Type -> m (TelV Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MetaId -> m Type
forall (m :: * -> *). ReadTCState m => MetaId -> m Type
metaType MetaId
x
addContext tel $ isLevelType t
isUpperBoundFor :: ProblemConstraint -> MetaId -> Bool
isUpperBoundFor :: ProblemConstraint -> MetaId -> Bool
isUpperBoundFor ProblemConstraint
c MetaId
x = case Closure Constraint -> Constraint
forall a. Closure a -> a
clValue (ProblemConstraint -> Closure Constraint
theConstraint ProblemConstraint
c) of
LevelCmp Comparison
CmpLeq Level
l Level
u -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ MetaId -> Level -> Bool
forall t. MentionsMeta t => MetaId -> t -> Bool
mentionsMeta MetaId
x Level
u
Constraint
_ -> Bool
False