    module Agda.TypeChecking.Monad.Imports
      ( addImport
      , addImportCycleCheck
      , checkForImportCycle
      , dropDecodedModule
      , getDecodedModule
      , getDecodedModules
      , getImportPath
      , getImports
      , getPrettyVisitedModules
      , getVisitedModule
      , getVisitedModules
      , isImported
      , setDecodedModules
      , setVisitedModules
      , storeDecodedModule
      , visitModule
      , withImportPath
      ) where

    import Control.Arrow   ( (***) )
    import Control.Monad   ( when )

    import Data.Set (Set)
    import qualified Data.Map as Map
    import qualified Data.Set as Set

    import Agda.Syntax.Abstract.Name
    import qualified Agda.Syntax.Concrete.Name as C
    import Agda.TypeChecking.Monad.Base

    import Agda.Utils.List ( caseListM )
    import Agda.Utils.Pretty

    import Agda.Utils.Impossible

    addImport :: ModuleName -> TCM ()
    addImport :: ModuleName -> TCM ()
    addImport ModuleName
    m = Lens' (Set ModuleName) TCState
    -> (Set ModuleName -> Set ModuleName) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    modifyTCLens Lens' (Set ModuleName) TCState
    stImportedModules ((Set ModuleName -> Set ModuleName) -> TCM ())
    -> (Set ModuleName -> Set ModuleName) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> Set ModuleName -> Set ModuleName
    forall a. Ord a => a -> Set a -> Set a
    Set.insert ModuleName
    m

    addImportCycleCheck :: C.TopLevelModuleName -> TCM a -> TCM a
    addImportCycleCheck :: forall a. TopLevelModuleName -> TCM a -> TCM a
    addImportCycleCheck TopLevelModuleName
    m =
        (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a)
    -> (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $ \TCEnv
    e -> TCEnv
    e { envImportPath :: [TopLevelModuleName]
    envImportPath = TopLevelModuleName
    m TopLevelModuleName -> [TopLevelModuleName] -> [TopLevelModuleName]
    forall a. a -> [a] -> [a]
    : TCEnv -> [TopLevelModuleName]
    envImportPath TCEnv
    e }

    getImports :: TCM (Set ModuleName)
    getImports :: TCM (Set ModuleName)
    getImports = Lens' (Set ModuleName) TCState -> TCM (Set ModuleName)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (Set ModuleName) TCState
    stImportedModules

    isImported :: ModuleName -> TCM Bool
    isImported :: ModuleName -> TCM Bool
    isImported ModuleName
    m = ModuleName -> Set ModuleName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member ModuleName
    m (Set ModuleName -> Bool) -> TCM (Set ModuleName) -> TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCM (Set ModuleName)
    getImports

    getImportPath :: TCM [C.TopLevelModuleName]
    getImportPath :: TCM [TopLevelModuleName]
    getImportPath = (TCEnv -> [TopLevelModuleName]) -> TCM [TopLevelModuleName]
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> [TopLevelModuleName]
    envImportPath

    visitModule :: ModuleInfo -> TCM ()
    visitModule :: ModuleInfo -> TCM ()
    visitModule ModuleInfo
    mi =
      Lens' (Map TopLevelModuleName ModuleInfo) TCState
    -> (Map TopLevelModuleName ModuleInfo
        -> Map TopLevelModuleName ModuleInfo)
    -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    modifyTCLens Lens' (Map TopLevelModuleName ModuleInfo) TCState
    stVisitedModules ((Map TopLevelModuleName ModuleInfo
      -> Map TopLevelModuleName ModuleInfo)
     -> TCM ())
    -> (Map TopLevelModuleName ModuleInfo
        -> Map TopLevelModuleName ModuleInfo)
    -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        TopLevelModuleName
    -> ModuleInfo
    -> Map TopLevelModuleName ModuleInfo
    -> Map TopLevelModuleName ModuleInfo
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert (ModuleName -> TopLevelModuleName
    toTopLevelModuleName (ModuleName -> TopLevelModuleName)
    -> ModuleName -> TopLevelModuleName
    forall a b. (a -> b) -> a -> b
    $ Interface -> ModuleName
    iModuleName (Interface -> ModuleName) -> Interface -> ModuleName
    forall a b. (a -> b) -> a -> b
    $ ModuleInfo -> Interface
    miInterface ModuleInfo
    mi) ModuleInfo
    mi

    setVisitedModules :: VisitedModules -> TCM ()
    setVisitedModules :: Map TopLevelModuleName ModuleInfo -> TCM ()
    setVisitedModules Map TopLevelModuleName ModuleInfo
    ms = Lens' (Map TopLevelModuleName ModuleInfo) TCState
    -> Map TopLevelModuleName ModuleInfo -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    setTCLens Lens' (Map TopLevelModuleName ModuleInfo) TCState
    stVisitedModules Map TopLevelModuleName ModuleInfo
    ms

    getVisitedModules :: ReadTCState m => m VisitedModules
    getVisitedModules :: forall (m :: * -> *).
    ReadTCState m =>
    m (Map TopLevelModuleName ModuleInfo)
    getVisitedModules = Lens' (Map TopLevelModuleName ModuleInfo) TCState
    -> m (Map TopLevelModuleName ModuleInfo)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (Map TopLevelModuleName ModuleInfo) TCState
    stVisitedModules

    getPrettyVisitedModules :: ReadTCState m => m Doc
    getPrettyVisitedModules :: forall (m :: * -> *). ReadTCState m => m Doc
    getPrettyVisitedModules = do
      [Doc]
    visited <-  ((TopLevelModuleName, ModuleInfo) -> Doc)
    -> [(TopLevelModuleName, ModuleInfo)] -> [Doc]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Doc -> Doc -> Doc) -> (Doc, Doc) -> Doc
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    (<>) ((Doc, Doc) -> Doc)
    -> ((TopLevelModuleName, ModuleInfo) -> (Doc, Doc))
    -> (TopLevelModuleName, ModuleInfo)
    -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (TopLevelModuleName -> Doc
    forall a. Pretty a => a -> Doc
    pretty (TopLevelModuleName -> Doc)
    -> (ModuleInfo -> Doc)
    -> (TopLevelModuleName, ModuleInfo)
    -> (Doc, Doc)
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    *** (ModuleCheckMode -> Doc
    prettyCheckMode (ModuleCheckMode -> Doc)
    -> (ModuleInfo -> ModuleCheckMode) -> ModuleInfo -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ModuleInfo -> ModuleCheckMode
    miMode))) ([(TopLevelModuleName, ModuleInfo)] -> [Doc])
    -> (Map TopLevelModuleName ModuleInfo
        -> [(TopLevelModuleName, ModuleInfo)])
    -> Map TopLevelModuleName ModuleInfo
    -> [Doc]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Map TopLevelModuleName ModuleInfo
    -> [(TopLevelModuleName, ModuleInfo)]
    forall k a. Map k a -> [(k, a)]
    Map.toList
              (Map TopLevelModuleName ModuleInfo -> [Doc])
    -> m (Map TopLevelModuleName ModuleInfo) -> m [Doc]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Map TopLevelModuleName ModuleInfo)
    forall (m :: * -> *).
    ReadTCState m =>
    m (Map TopLevelModuleName ModuleInfo)
    getVisitedModules
      Doc -> m Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> m Doc) -> Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> [Doc] -> [Doc]
    forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
    punctuate Doc
    ", " [Doc]
    visited
      where
      prettyCheckMode :: ModuleCheckMode -> Doc
      prettyCheckMode :: ModuleCheckMode -> Doc
    prettyCheckMode ModuleCheckMode
    ModuleTypeChecked                  = Doc
    ""
      prettyCheckMode ModuleCheckMode
    ModuleScopeChecked                 = Doc
    " (scope only)"

    getVisitedModule :: ReadTCState m
                     => C.TopLevelModuleName
                     -> m (Maybe ModuleInfo)
    getVisitedModule :: forall (m :: * -> *).
    ReadTCState m =>
    TopLevelModuleName -> m (Maybe ModuleInfo)
    getVisitedModule TopLevelModuleName
    x = TopLevelModuleName
    -> Map TopLevelModuleName ModuleInfo -> Maybe ModuleInfo
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup TopLevelModuleName
    x (Map TopLevelModuleName ModuleInfo -> Maybe ModuleInfo)
    -> m (Map TopLevelModuleName ModuleInfo) -> m (Maybe ModuleInfo)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' (Map TopLevelModuleName ModuleInfo) TCState
    -> m (Map TopLevelModuleName ModuleInfo)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (Map TopLevelModuleName ModuleInfo) TCState
    stVisitedModules

    getDecodedModules :: TCM DecodedModules
    getDecodedModules :: TCM (Map TopLevelModuleName ModuleInfo)
    getDecodedModules = PersistentTCState -> Map TopLevelModuleName ModuleInfo
    stDecodedModules (PersistentTCState -> Map TopLevelModuleName ModuleInfo)
    -> (TCState -> PersistentTCState)
    -> TCState
    -> Map TopLevelModuleName ModuleInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCState -> PersistentTCState
    stPersistentState (TCState -> Map TopLevelModuleName ModuleInfo)
    -> TCMT IO TCState -> TCM (Map TopLevelModuleName ModuleInfo)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC

    setDecodedModules :: DecodedModules -> TCM ()
    setDecodedModules :: Map TopLevelModuleName ModuleInfo -> TCM ()
    setDecodedModules Map TopLevelModuleName ModuleInfo
    ms = (TCState -> TCState) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (TCState -> TCState) -> m ()
    modifyTC ((TCState -> TCState) -> TCM ()) -> (TCState -> TCState) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \TCState
    s ->
      TCState
    s { stPersistentState :: PersistentTCState
    stPersistentState = (TCState -> PersistentTCState
    stPersistentState TCState
    s) { stDecodedModules :: Map TopLevelModuleName ModuleInfo
    stDecodedModules = Map TopLevelModuleName ModuleInfo
    ms } }

    getDecodedModule :: C.TopLevelModuleName -> TCM (Maybe ModuleInfo)
    getDecodedModule :: TopLevelModuleName -> TCM (Maybe ModuleInfo)
    getDecodedModule TopLevelModuleName
    x = TopLevelModuleName
    -> Map TopLevelModuleName ModuleInfo -> Maybe ModuleInfo
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup TopLevelModuleName
    x (Map TopLevelModuleName ModuleInfo -> Maybe ModuleInfo)
    -> (TCState -> Map TopLevelModuleName ModuleInfo)
    -> TCState
    -> Maybe ModuleInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PersistentTCState -> Map TopLevelModuleName ModuleInfo
    stDecodedModules (PersistentTCState -> Map TopLevelModuleName ModuleInfo)
    -> (TCState -> PersistentTCState)
    -> TCState
    -> Map TopLevelModuleName ModuleInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCState -> PersistentTCState
    stPersistentState (TCState -> Maybe ModuleInfo)
    -> TCMT IO TCState -> TCM (Maybe ModuleInfo)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC

    storeDecodedModule :: ModuleInfo -> TCM ()
    storeDecodedModule :: ModuleInfo -> TCM ()
    storeDecodedModule ModuleInfo
    mi = (TCState -> TCState) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (TCState -> TCState) -> m ()
    modifyTC ((TCState -> TCState) -> TCM ()) -> (TCState -> TCState) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \TCState
    s ->
      TCState
    s { stPersistentState :: PersistentTCState
    stPersistentState =
            (TCState -> PersistentTCState
    stPersistentState TCState
    s) { stDecodedModules :: Map TopLevelModuleName ModuleInfo
    stDecodedModules =
              TopLevelModuleName
    -> ModuleInfo
    -> Map TopLevelModuleName ModuleInfo
    -> Map TopLevelModuleName ModuleInfo
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert (ModuleName -> TopLevelModuleName
    toTopLevelModuleName (ModuleName -> TopLevelModuleName)
    -> ModuleName -> TopLevelModuleName
    forall a b. (a -> b) -> a -> b
    $ Interface -> ModuleName
    iModuleName (Interface -> ModuleName) -> Interface -> ModuleName
    forall a b. (a -> b) -> a -> b
    $ ModuleInfo -> Interface
    miInterface ModuleInfo
    mi) ModuleInfo
    mi (Map TopLevelModuleName ModuleInfo
     -> Map TopLevelModuleName ModuleInfo)
    -> Map TopLevelModuleName ModuleInfo
    -> Map TopLevelModuleName ModuleInfo
    forall a b. (a -> b) -> a -> b
    $
                PersistentTCState -> Map TopLevelModuleName ModuleInfo
    stDecodedModules (TCState -> PersistentTCState
    stPersistentState TCState
    s)
            }
      }

    dropDecodedModule :: C.TopLevelModuleName -> TCM ()
    dropDecodedModule :: TopLevelModuleName -> TCM ()
    dropDecodedModule TopLevelModuleName
    x = (TCState -> TCState) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (TCState -> TCState) -> m ()
    modifyTC ((TCState -> TCState) -> TCM ()) -> (TCState -> TCState) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \TCState
    s ->
      TCState
    s { stPersistentState :: PersistentTCState
    stPersistentState =
            (TCState -> PersistentTCState
    stPersistentState TCState
    s) { stDecodedModules :: Map TopLevelModuleName ModuleInfo
    stDecodedModules =
                                      TopLevelModuleName
    -> Map TopLevelModuleName ModuleInfo
    -> Map TopLevelModuleName ModuleInfo
    forall k a. Ord k => k -> Map k a -> Map k a
    Map.delete TopLevelModuleName
    x (Map TopLevelModuleName ModuleInfo
     -> Map TopLevelModuleName ModuleInfo)
    -> Map TopLevelModuleName ModuleInfo
    -> Map TopLevelModuleName ModuleInfo
    forall a b. (a -> b) -> a -> b
    $ PersistentTCState -> Map TopLevelModuleName ModuleInfo
    stDecodedModules (PersistentTCState -> Map TopLevelModuleName ModuleInfo)
    -> PersistentTCState -> Map TopLevelModuleName ModuleInfo
    forall a b. (a -> b) -> a -> b
    $ TCState -> PersistentTCState
    stPersistentState TCState
    s
                                  }
      }

    withImportPath :: [C.TopLevelModuleName] -> TCM a -> TCM a
    withImportPath :: forall a. [TopLevelModuleName] -> TCM a -> TCM a
    withImportPath [TopLevelModuleName]
    path = (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a)
    -> (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $ \TCEnv
    e -> TCEnv
    e { envImportPath :: [TopLevelModuleName]
    envImportPath = [TopLevelModuleName]
    path }

    -- | Assumes that the first module in the import path is the module we are
    --   worried about.
    checkForImportCycle :: TCM ()
    checkForImportCycle :: TCM ()
    checkForImportCycle = do
      TCM [TopLevelModuleName]
    -> TCM ()
    -> (TopLevelModuleName -> [TopLevelModuleName] -> TCM ())
    -> TCM ()
    forall (m :: * -> *) a b.
    Monad m =>
    m [a] -> m b -> (a -> [a] -> m b) -> m b
    caseListM TCM [TopLevelModuleName]
    getImportPath TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ((TopLevelModuleName -> [TopLevelModuleName] -> TCM ()) -> TCM ())
    -> (TopLevelModuleName -> [TopLevelModuleName] -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ TopLevelModuleName
    m [TopLevelModuleName]
    ms -> do
        Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (TopLevelModuleName
    m TopLevelModuleName -> [TopLevelModuleName] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [TopLevelModuleName]
    ms) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TopLevelModuleName] -> TypeError
    CyclicModuleDependency
                                       ([TopLevelModuleName] -> TypeError)
    -> [TopLevelModuleName] -> TypeError
    forall a b. (a -> b) -> a -> b
    $ (TopLevelModuleName -> Bool)
    -> [TopLevelModuleName] -> [TopLevelModuleName]
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile (TopLevelModuleName -> TopLevelModuleName -> Bool
    forall a. Eq a => a -> a -> Bool
    /= TopLevelModuleName
    m) ([TopLevelModuleName] -> [TopLevelModuleName])
    -> [TopLevelModuleName] -> [TopLevelModuleName]
    forall a b. (a -> b) -> a -> b
    $ [TopLevelModuleName] -> [TopLevelModuleName]
    forall a. [a] -> [a]
    reverse (TopLevelModuleName
    mTopLevelModuleName -> [TopLevelModuleName] -> [TopLevelModuleName]
    forall a. a -> [a] -> [a]
    :[TopLevelModuleName]
    ms)