{-# 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 = 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, LocalMetaStores
newMetas) <- forall (m :: * -> *) a.
ReadTCState m =>
m a -> m (a, LocalMetaStores)
metasCreatedBy m a
f
  forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m) =>
LocalMetaStore -> m ()
defaultLevelsToZero (LocalMetaStores -> LocalMetaStore
openMetas LocalMetaStores
newMetas)
  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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [MetaId] -> m [MetaId]
openLevelMetas (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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
x
      [MetaId]
xs <- forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM forall {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 :: * -> *). 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
               Maybe (Either RemoteMetaVariable MetaVariable)
m <- forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe (Either RemoteMetaVariable 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 :: * -> *). 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 :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState 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 :: * -> *). 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