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

-- | 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, LocalMetaStores
newMetas) <- m a -> m (a, LocalMetaStores)
forall (m :: * -> *) a.
ReadTCState m =>
m a -> m (a, LocalMetaStores)
metasCreatedBy m a
f
  LocalMetaStore -> m ()
forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m) =>
LocalMetaStore -> m ()
defaultLevelsToZero (LocalMetaStores -> LocalMetaStore
openMetas LocalMetaStores
newMetas)
  a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
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
      [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 :: * -> *}. 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 a b. m a -> (a -> m b) -> m b
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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse MetaId -> m Type
forall (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
               Maybe (Either RemoteMetaVariable MetaVariable)
m <- MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe (Either RemoteMetaVariable 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 :: * -> *). 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
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> 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 a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
             m Bool -> (TCErr -> m Bool) -> m Bool
forall a. m a -> (TCErr -> m a) -> m a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
_ -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
           | Bool
otherwise -> Bool -> m Bool
forall a. a -> m a
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 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 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 :: * -> *). 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
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> 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