    {-# 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 ((Nat -> MetaId) -> [Nat] -> [MetaId]
    forall a b. (a -> b) -> [a] -> [b]
    map Nat -> MetaId
    MetaId ([Nat] -> [MetaId]) -> [Nat] -> [MetaId]
    forall a b. (a -> b) -> a -> b
    $ MetaStore -> [Nat]
    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 (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