{-# 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

-- | Run the given action. At the end take all new metavariables of
--   type level for which the only constraints are upper bounds on the
--   level, and instantiate them to the lowest level.
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
  (a
result , MetaStore
newMetas) <- m a -> m (a, MetaStore)
forall (m :: * -> *) a. ReadTCState m => m a -> m (a, MetaStore)
metasCreatedBy m a
f
  MetaStore -> m ()
forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m) =>
MetaStore -> m ()
defaultLevelsToZero MetaStore
newMetas
  a -> m a
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 ([MetaId] -> m ()) -> m [MetaId] -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [MetaId] -> m [MetaId]
openLevelMetas ((Key -> MetaId) -> [Key] -> [MetaId]
forall a b. (a -> b) -> [a] -> [b]
map Key -> MetaId
MetaId ([Key] -> [MetaId]) -> [Key] -> [MetaId]
forall a b. (a -> b) -> a -> b
$ MetaStore -> [Key]
forall a. IntMap a -> [Key]
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 (MetaInstantiation -> Bool)
-> (MetaVariable -> MetaInstantiation) -> MetaVariable -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> MetaInstantiation
mvInstantiation (MetaVariable -> Bool) -> f MetaVariable -> f Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> f MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
x
      [MetaId]
xs <- (MetaId -> m Bool) -> [MetaId] -> m [MetaId]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM MetaId -> m Bool
forall {f :: * -> *}.
(MonadFail f, ReadTCState f) =>
MetaId -> f Bool
isOpen [MetaId]
xs
      [Type]
allMetaTypes <- m [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
getOpenMetas m [MetaId] -> ([MetaId] -> m [Type]) -> m [Type]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (MetaId -> m Type) -> [MetaId] -> m [Type]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse MetaId -> m Type
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
metaType
      let notInTypeOfMeta :: MetaId -> Bool
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
      [Bool]
progress <- [MetaId] -> (MetaId -> m Bool) -> m [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [MetaId]
xs ((MetaId -> m Bool) -> m [Bool]) -> (MetaId -> m Bool) -> m [Bool]
forall a b. (a -> b) -> a -> b
$ \MetaId
x -> do
        [ProblemConstraint]
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 | MetaId -> Bool
notInTypeOfMeta MetaId
x , (ProblemConstraint -> Bool) -> [ProblemConstraint] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (ProblemConstraint -> MetaId -> Bool
`isUpperBoundFor` MetaId
x) [ProblemConstraint]
cs -> do
               MetaVariable
m <- MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
x
               TelV Tele (Dom Type)
tel Type
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 :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
metaType MetaId
x
               Tele (Dom Type) -> m () -> m ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
tel (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ CompareDirection -> MetaId -> Args -> Term -> CompareAs -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
CompareDirection -> MetaId -> Args -> Term -> CompareAs -> m ()
assignV CompareDirection
DirEq MetaId
x (Tele (Dom Type) -> Args
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
tel) (Level -> Term
Level (Level -> Term) -> Level -> Term
forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
0) (Type -> CompareAs
AsTermsOf Type
t)
               Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
             m Bool -> (TCErr -> m Bool) -> m Bool
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
_ -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
           | Bool
otherwise -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
progress) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ ([MetaId] -> m ()
loop [MetaId]
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 (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 (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 :: * -> *).
(ReadTCState m, MonadFail m) =>
MetaId -> m DoGeneralize
isGeneralizableMeta)
      m [MetaId] -> ([MetaId] -> m [MetaId]) -> m [MetaId]
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 Tele (Dom Type)
tel Type
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 :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
metaType MetaId
x
      Tele (Dom Type) -> m Bool -> m Bool
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
tel (m Bool -> m Bool) -> m Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Type -> m Bool
forall (m :: * -> *). PureTCM m => Type -> m Bool
isLevelType Type
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