{-# LANGUAGE ScopedTypeVariables #-}
module Agda.TypeChecking.Level.Solve where
import Control.Monad
import Control.Monad.Except
import qualified Data.IntMap as IntMap
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 = forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (PragmaOptions -> Bool
optCumulativity forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) m a
f forall a b. (a -> b) -> a -> b
$ do
(a
result , MetaStore
newMetas) <- forall (m :: * -> *) a. ReadTCState m => m a -> m (a, MetaStore)
metasCreatedBy m a
f
forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m) =>
MetaStore -> m ()
defaultLevelsToZero MetaStore
newMetas
forall (m :: * -> *) a. Monad m => a -> m a
return a
result
defaultLevelsToZero :: forall m. (PureTCM m, MonadMetaSolver m) => MetaStore -> m ()
defaultLevelsToZero :: forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m) =>
MetaStore -> m ()
defaultLevelsToZero MetaStore
xs = [MetaId] -> m ()
loop forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [MetaId] -> m [MetaId]
openLevelMetas (forall a b. (a -> b) -> [a] -> [b]
map Nat -> MetaId
MetaId forall a b. (a -> b) -> a -> b
$ forall a. IntMap a -> [Nat]
IntMap.keys MetaStore
xs)
where
loop :: [MetaId] -> m ()
loop :: [MetaId] -> m ()
loop [MetaId]
xs = do
let isOpen :: MetaId -> f Bool
isOpen MetaId
x = MetaInstantiation -> Bool
isOpenMeta forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> MetaInstantiation
mvInstantiation forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
x
[MetaId]
xs <- forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM forall {f :: * -> *}.
(MonadFail f, ReadTCState f) =>
MetaId -> f Bool
isOpen [MetaId]
xs
[Type]
allMetaTypes <- forall (m :: * -> *). ReadTCState m => m [MetaId]
getOpenMetas forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
metaType
let notInTypeOfMeta :: MetaId -> Bool
notInTypeOfMeta MetaId
x = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall t. MentionsMeta t => MetaId -> t -> Bool
mentionsMeta MetaId
x [Type]
allMetaTypes
[Bool]
progress <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [MetaId]
xs forall a b. (a -> b) -> a -> b
$ \MetaId
x -> do
[ProblemConstraint]
cs <- forall a. (a -> Bool) -> [a] -> [a]
filter (forall t. MentionsMeta t => MetaId -> t -> Bool
mentionsMeta MetaId
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m [ProblemConstraint]
getAllConstraints
if | MetaId -> Bool
notInTypeOfMeta MetaId
x , forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (ProblemConstraint -> MetaId -> Bool
`isUpperBoundFor` MetaId
x) [ProblemConstraint]
cs -> do
MetaVariable
m <- forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
x
TelV Tele (Dom Type)
tel Type
t <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
metaType MetaId
x
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadMetaSolver m =>
CompareDirection -> MetaId -> Args -> Term -> CompareAs -> m ()
assignV CompareDirection
DirEq MetaId
x (forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
tel) (Level -> Term
Level forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
0) (Type -> CompareAs
AsTermsOf Type
t)
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
| Bool
otherwise -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
progress) forall a b. (a -> b) -> a -> b
$ ([MetaId] -> m ()
loop [MetaId]
xs)
openLevelMetas :: [MetaId] -> m [MetaId]
openLevelMetas :: [MetaId] -> m [MetaId]
openLevelMetas [MetaId]
xs = forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (forall a. Maybe a -> Bool
isNothing forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe InteractionId)
isInteractionMeta) [MetaId]
xs
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Eq a => a -> a -> Bool
== DoGeneralize
NoGeneralize) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
(ReadTCState m, MonadFail m) =>
MetaId -> m DoGeneralize
isGeneralizableMeta)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= 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 Tele (Dom Type)
tel Type
t <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
metaType MetaId
x
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). PureTCM m => Type -> m Bool
isLevelType Type
t
isUpperBoundFor :: ProblemConstraint -> MetaId -> Bool
isUpperBoundFor :: ProblemConstraint -> MetaId -> Bool
isUpperBoundFor ProblemConstraint
c MetaId
x = case forall a. Closure a -> a
clValue (ProblemConstraint -> Closure Constraint
theConstraint ProblemConstraint
c) of
LevelCmp Comparison
CmpLeq Level
l Level
u -> Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall t. MentionsMeta t => MetaId -> t -> Bool
mentionsMeta MetaId
x Level
u
Constraint
_ -> Bool
False