    {-# OPTIONS_GHC -Wunused-imports #-}

    module Agda.TypeChecking.Level.Solve where

    import Control.Monad.Except ( catchError )

    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.
    --   If @--cumulativity@ is off, that's it.
    --
    --   Otherwise, 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
      (result, newMetas) <- m a -> m (a, LocalMetaStores)
    forall (m :: * -> *) a.
    ReadTCState m =>
    m a -> m (a, LocalMetaStores)
    metasCreatedBy m a
    f
      defaultLevelsToZero (openMetas newMetas)
      return 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
          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
          allMetaTypes <- getOpenMetas >>= traverse metaType
          let 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
          progress <- forM xs $ \MetaId
    x -> do
            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 | notInTypeOfMeta x , all (`isUpperBoundFor` x) cs -> do
                   m <- lookupMeta x
                   TelV tel t <- telView =<< metaType x
                   addContext tel $ assignV DirEq x (teleArgs tel) (Level $ ClosedLevel 0) (AsTermsOf t)
                   return True
                 `catchError` \TCErr
    _ -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
               | otherwise -> return False

          when (or progress) $ (loop 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 tel 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
          addContext tel $ isLevelType 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