    module Agda.TypeChecking.Monad.Options where

    import Control.Arrow          ( (&&&) )
    import Control.Monad          ( unless, when )
    import Control.Monad.IO.Class ( MonadIO(..) )
    import Control.Monad.Except
    import Control.Monad.Reader
    import Control.Monad.State
    import Control.Monad.Writer

    import qualified Data.Graph as Graph
    import Data.List (sort)
    import Data.Maybe
    import Data.Map (Map)
    import qualified Data.Map as Map

    import System.Directory
    import System.FilePath

    import Agda.Syntax.Common
    import Agda.Syntax.Concrete (TopLevelModuleName)
    import qualified Agda.Syntax.Concrete as C
    import qualified Agda.Syntax.Abstract as A
    import Agda.TypeChecking.Monad.Debug (reportSDoc)
    import Agda.TypeChecking.Warnings
    import Agda.TypeChecking.Monad.Base
    import Agda.TypeChecking.Monad.Imports
    import Agda.TypeChecking.Monad.State
    import Agda.TypeChecking.Monad.Benchmark
    import Agda.Interaction.FindFile
    import Agda.Interaction.Options
    import qualified Agda.Interaction.Options.Lenses as Lens
    import Agda.Interaction.Library
    import Agda.Utils.FileName
    import Agda.Utils.Functor
    import qualified Agda.Utils.Graph.AdjacencyMap.Unidirectional as G
    import Agda.Utils.List
    import Agda.Utils.Maybe
    import Agda.Utils.Pretty
    import Agda.Utils.Tuple
    import Agda.Utils.WithDefault

    import Agda.Utils.Impossible

    -- | Sets the pragma options.

    setPragmaOptions :: PragmaOptions -> TCM ()
    setPragmaOptions :: PragmaOptions -> TCM ()
    setPragmaOptions PragmaOptions
    opts = do
      Lens' PragmaOptions TCState
    stPragmaOptions Lens' PragmaOptions TCState
    -> (PragmaOptions -> PragmaOptions) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    `modifyTCLens` (SafeMode -> SafeMode) -> PragmaOptions -> PragmaOptions
    forall a. LensSafeMode a => (SafeMode -> SafeMode) -> a -> a
    Lens.mapSafeMode (PragmaOptions -> SafeMode
    forall a. LensSafeMode a => a -> SafeMode
    Lens.getSafeMode PragmaOptions
    opts SafeMode -> SafeMode -> SafeMode
    ||)
      CommandLineOptions
    clo <- TCMT IO CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions
      let unsafe :: [FilePath]
    unsafe = CommandLineOptions -> PragmaOptions -> [FilePath]
    unsafePragmaOptions CommandLineOptions
    clo PragmaOptions
    opts
      SafeMode -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => SafeMode -> f () -> f ()
    when (PragmaOptions -> SafeMode
    forall a. LensSafeMode a => a -> SafeMode
    Lens.getSafeMode PragmaOptions
    opts SafeMode -> SafeMode -> SafeMode
    && SafeMode -> SafeMode
    not ([FilePath] -> SafeMode
    forall (t :: * -> *) a. Foldable t => t a -> SafeMode
    null [FilePath]
    unsafe)) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCM ()) -> Warning -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [FilePath] -> Warning
    SafeFlagPragma [FilePath]
    unsafe
      OptM CommandLineOptions
    -> TCMT IO (Either FilePath CommandLineOptions)
    forall (m :: * -> *) opts.
    Monad m =>
    OptM opts -> m (Either FilePath opts)
    runOptM (Flag CommandLineOptions
    checkOpts CommandLineOptions
    clo{ optPragmaOptions :: PragmaOptions
    optPragmaOptions = PragmaOptions
    opts }) TCMT IO (Either FilePath CommandLineOptions)
    -> (Either FilePath CommandLineOptions -> TCM ()) -> TCM ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Left FilePath
    err   -> TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Right CommandLineOptions
    opts -> do
          Lens' PragmaOptions TCState
    stPragmaOptions Lens' PragmaOptions TCState -> PragmaOptions -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    `setTCLens` CommandLineOptions -> PragmaOptions
    optPragmaOptions CommandLineOptions
    opts
          TCM ()
    updateBenchmarkingStatus

    -- | Sets the command line options (both persistent and pragma options
    -- are updated).
    --
    -- Relative include directories are made absolute with respect to the
    -- current working directory. If the include directories have changed
    -- (thus, they are 'Left' now, and were previously @'Right' something@),
    -- then the state is reset (completely, see setIncludeDirs) .
    --
    -- An empty list of relative include directories (@'Left' []@) is
    -- interpreted as @["."]@.
    setCommandLineOptions :: CommandLineOptions -> TCM ()
    setCommandLineOptions :: CommandLineOptions -> TCM ()
    setCommandLineOptions CommandLineOptions
    opts = do
      AbsolutePath
    root <- IO AbsolutePath -> TCMT IO AbsolutePath
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (FilePath -> IO AbsolutePath
    absolute (FilePath -> IO AbsolutePath) -> IO FilePath -> IO AbsolutePath
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< IO FilePath
    getCurrentDirectory)
      AbsolutePath -> CommandLineOptions -> TCM ()
    setCommandLineOptions' AbsolutePath
    root CommandLineOptions
    opts

    setCommandLineOptions'
      :: AbsolutePath
         -- ^ The base directory of relative paths.
      -> CommandLineOptions
      -> TCM ()
    setCommandLineOptions' :: AbsolutePath -> CommandLineOptions -> TCM ()
    setCommandLineOptions' AbsolutePath
    root CommandLineOptions
    opts = do
      OptM CommandLineOptions
    -> TCMT IO (Either FilePath CommandLineOptions)
    forall (m :: * -> *) opts.
    Monad m =>
    OptM opts -> m (Either FilePath opts)
    runOptM (Flag CommandLineOptions
    checkOpts CommandLineOptions
    opts) TCMT IO (Either FilePath CommandLineOptions)
    -> (Either FilePath CommandLineOptions -> TCM ()) -> TCM ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Left FilePath
    err   -> TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Right CommandLineOptions
    opts -> do
          [AbsolutePath]
    incs <- case CommandLineOptions -> [AbsolutePath]
    optAbsoluteIncludePaths CommandLineOptions
    opts of
            [] -> do
              CommandLineOptions
    opts' <- AbsolutePath -> CommandLineOptions -> TCMT IO CommandLineOptions
    setLibraryPaths AbsolutePath
    root CommandLineOptions
    opts
              let incs :: [FilePath]
    incs = CommandLineOptions -> [FilePath]
    optIncludePaths CommandLineOptions
    opts'
              [FilePath] -> AbsolutePath -> TCM ()
    setIncludeDirs [FilePath]
    incs AbsolutePath
    root
              TCMT IO [AbsolutePath]
    forall (m :: * -> *). HasOptions m => m [AbsolutePath]
    getIncludeDirs
            [AbsolutePath]
    incs -> [AbsolutePath] -> TCMT IO [AbsolutePath]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [AbsolutePath]
    incs
          (TCState -> TCState) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (TCState -> TCState) -> m ()
    modifyTC ((TCState -> TCState) -> TCM ()) -> (TCState -> TCState) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions -> TCState -> TCState
    forall a. LensCommandLineOptions a => CommandLineOptions -> a -> a
    Lens.setCommandLineOptions CommandLineOptions
    opts{ optAbsoluteIncludePaths :: [AbsolutePath]
    optAbsoluteIncludePaths = [AbsolutePath]
    incs }
          PragmaOptions -> TCM ()
    setPragmaOptions (CommandLineOptions -> PragmaOptions
    optPragmaOptions CommandLineOptions
    opts)
          TCM ()
    updateBenchmarkingStatus

    libToTCM :: LibM a -> TCM a
    libToTCM :: forall a. LibM a -> TCM a
    libToTCM LibM a
    m = do
      Map FilePath ProjectConfig
    cachedConfs <- Lens' (Map FilePath ProjectConfig) TCState
    -> TCMT IO (Map FilePath ProjectConfig)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (Map FilePath ProjectConfig) TCState
    stProjectConfigs
      Map FilePath AgdaLibFile
    cachedLibs  <- Lens' (Map FilePath AgdaLibFile) TCState
    -> TCMT IO (Map FilePath AgdaLibFile)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (Map FilePath AgdaLibFile) TCState
    stAgdaLibFiles

      ((Either Doc a
    z, [LibWarning]
    warns), (Map FilePath ProjectConfig
    cachedConfs', Map FilePath AgdaLibFile
    cachedLibs')) <- IO
      ((Either Doc a, [LibWarning]),
       (Map FilePath ProjectConfig, Map FilePath AgdaLibFile))
    -> TCMT
         IO
         ((Either Doc a, [LibWarning]),
          (Map FilePath ProjectConfig, Map FilePath AgdaLibFile))
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO
       ((Either Doc a, [LibWarning]),
        (Map FilePath ProjectConfig, Map FilePath AgdaLibFile))
     -> TCMT
          IO
          ((Either Doc a, [LibWarning]),
           (Map FilePath ProjectConfig, Map FilePath AgdaLibFile)))
    -> IO
         ((Either Doc a, [LibWarning]),
          (Map FilePath ProjectConfig, Map FilePath AgdaLibFile))
    -> TCMT
         IO
         ((Either Doc a, [LibWarning]),
          (Map FilePath ProjectConfig, Map FilePath AgdaLibFile))
    forall a b. (a -> b) -> a -> b
    $
        (StateT
      (Map FilePath ProjectConfig, Map FilePath AgdaLibFile)
      IO
      (Either Doc a, [LibWarning])
    -> (Map FilePath ProjectConfig, Map FilePath AgdaLibFile)
    -> IO
         ((Either Doc a, [LibWarning]),
          (Map FilePath ProjectConfig, Map FilePath AgdaLibFile))
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    `runStateT` (Map FilePath ProjectConfig
    cachedConfs, Map FilePath AgdaLibFile
    cachedLibs)) (StateT
       (Map FilePath ProjectConfig, Map FilePath AgdaLibFile)
       IO
       (Either Doc a, [LibWarning])
     -> IO
          ((Either Doc a, [LibWarning]),
           (Map FilePath ProjectConfig, Map FilePath AgdaLibFile)))
    -> StateT
         (Map FilePath ProjectConfig, Map FilePath AgdaLibFile)
         IO
         (Either Doc a, [LibWarning])
    -> IO
         ((Either Doc a, [LibWarning]),
          (Map FilePath ProjectConfig, Map FilePath AgdaLibFile))
    forall a b. (a -> b) -> a -> b
    $ WriterT
      [LibWarning]
      (StateT (Map FilePath ProjectConfig, Map FilePath AgdaLibFile) IO)
      (Either Doc a)
    -> StateT
         (Map FilePath ProjectConfig, Map FilePath AgdaLibFile)
         IO
         (Either Doc a, [LibWarning])
    forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
    runWriterT (WriterT
       [LibWarning]
       (StateT (Map FilePath ProjectConfig, Map FilePath AgdaLibFile) IO)
       (Either Doc a)
     -> StateT
          (Map FilePath ProjectConfig, Map FilePath AgdaLibFile)
          IO
          (Either Doc a, [LibWarning]))
    -> WriterT
         [LibWarning]
         (StateT (Map FilePath ProjectConfig, Map FilePath AgdaLibFile) IO)
         (Either Doc a)
    -> StateT
         (Map FilePath ProjectConfig, Map FilePath AgdaLibFile)
         IO
         (Either Doc a, [LibWarning])
    forall a b. (a -> b) -> a -> b
    $ LibM a
    -> WriterT
         [LibWarning]
         (StateT (Map FilePath ProjectConfig, Map FilePath AgdaLibFile) IO)
         (Either Doc a)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT LibM a
    m

      Lens' (Map FilePath ProjectConfig) TCState
    -> (Map FilePath ProjectConfig -> Map FilePath ProjectConfig)
    -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    modifyTCLens Lens' (Map FilePath ProjectConfig) TCState
    stProjectConfigs ((Map FilePath ProjectConfig -> Map FilePath ProjectConfig)
     -> TCM ())
    -> (Map FilePath ProjectConfig -> Map FilePath ProjectConfig)
    -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Map FilePath ProjectConfig
    -> Map FilePath ProjectConfig -> Map FilePath ProjectConfig
    forall a b. a -> b -> a
    const Map FilePath ProjectConfig
    cachedConfs'
      Lens' (Map FilePath AgdaLibFile) TCState
    -> (Map FilePath AgdaLibFile -> Map FilePath AgdaLibFile) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    modifyTCLens Lens' (Map FilePath AgdaLibFile) TCState
    stAgdaLibFiles   ((Map FilePath AgdaLibFile -> Map FilePath AgdaLibFile) -> TCM ())
    -> (Map FilePath AgdaLibFile -> Map FilePath AgdaLibFile) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Map FilePath AgdaLibFile
    -> Map FilePath AgdaLibFile -> Map FilePath AgdaLibFile
    forall a b. a -> b -> a
    const Map FilePath AgdaLibFile
    cachedLibs'

      SafeMode -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => SafeMode -> f () -> f ()
    unless ([LibWarning] -> SafeMode
    forall (t :: * -> *) a. Foldable t => t a -> SafeMode
    null [LibWarning]
    warns) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Warning] -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    [Warning] -> m ()
    warnings ([Warning] -> TCM ()) -> [Warning] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (LibWarning -> Warning) -> [LibWarning] -> [Warning]
    forall a b. (a -> b) -> [a] -> [b]
    map LibWarning -> Warning
    LibraryWarning [LibWarning]
    warns
      case Either Doc a
    z of
        Left Doc
    s  -> TypeError -> TCM a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM a) -> TypeError -> TCM a
    forall a b. (a -> b) -> a -> b
    $ Doc -> TypeError
    GenericDocError Doc
    s
        Right a
    x -> a -> TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    x

    getAgdaLibFiles :: FilePath -> TCM [AgdaLibFile]
    getAgdaLibFiles :: FilePath -> TCM [AgdaLibFile]
    getAgdaLibFiles FilePath
    root = do
      SafeMode
    useLibs <- CommandLineOptions -> SafeMode
    optUseLibs (CommandLineOptions -> SafeMode)
    -> TCMT IO CommandLineOptions -> TCMT IO SafeMode
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions
      if | SafeMode
    useLibs   -> LibM [AgdaLibFile] -> TCM [AgdaLibFile]
    forall a. LibM a -> TCM a
    libToTCM (LibM [AgdaLibFile] -> TCM [AgdaLibFile])
    -> LibM [AgdaLibFile] -> TCM [AgdaLibFile]
    forall a b. (a -> b) -> a -> b
    $ [AgdaLibFile] -> LibErrorIO [AgdaLibFile] -> LibM [AgdaLibFile]
    forall a. [AgdaLibFile] -> LibErrorIO a -> LibM a
    mkLibM [] (LibErrorIO [AgdaLibFile] -> LibM [AgdaLibFile])
    -> LibErrorIO [AgdaLibFile] -> LibM [AgdaLibFile]
    forall a b. (a -> b) -> a -> b
    $ FilePath -> LibErrorIO [AgdaLibFile]
    getAgdaLibFiles' FilePath
    root
         | SafeMode
    otherwise -> [AgdaLibFile] -> TCM [AgdaLibFile]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []

    getLibraryOptions :: FilePath -> TCM [OptionsPragma]
    getLibraryOptions :: FilePath -> TCM [[FilePath]]
    getLibraryOptions FilePath
    root = (AgdaLibFile -> [FilePath]) -> [AgdaLibFile] -> [[FilePath]]
    forall a b. (a -> b) -> [a] -> [b]
    map AgdaLibFile -> [FilePath]
    _libPragmas ([AgdaLibFile] -> [[FilePath]])
    -> TCM [AgdaLibFile] -> TCM [[FilePath]]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> FilePath -> TCM [AgdaLibFile]
    getAgdaLibFiles FilePath
    root

    setLibraryPaths
      :: AbsolutePath
         -- ^ The base directory of relative paths.
      -> CommandLineOptions
      -> TCM CommandLineOptions
    setLibraryPaths :: AbsolutePath -> CommandLineOptions -> TCMT IO CommandLineOptions
    setLibraryPaths AbsolutePath
    root CommandLineOptions
    o =
      CommandLineOptions -> TCMT IO CommandLineOptions
    setLibraryIncludes (CommandLineOptions -> TCMT IO CommandLineOptions)
    -> TCMT IO CommandLineOptions -> TCMT IO CommandLineOptions
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< AbsolutePath -> CommandLineOptions -> TCMT IO CommandLineOptions
    addDefaultLibraries AbsolutePath
    root CommandLineOptions
    o

    setLibraryIncludes :: CommandLineOptions -> TCM CommandLineOptions
    setLibraryIncludes :: CommandLineOptions -> TCMT IO CommandLineOptions
    setLibraryIncludes CommandLineOptions
    o
      | SafeMode -> SafeMode
    not (CommandLineOptions -> SafeMode
    optUseLibs CommandLineOptions
    o) = CommandLineOptions -> TCMT IO CommandLineOptions
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CommandLineOptions
    o
      | SafeMode
    otherwise = do
        let libs :: [FilePath]
    libs = CommandLineOptions -> [FilePath]
    optLibraries CommandLineOptions
    o
        [AgdaLibFile]
    installed <- LibM [AgdaLibFile] -> TCM [AgdaLibFile]
    forall a. LibM a -> TCM a
    libToTCM (LibM [AgdaLibFile] -> TCM [AgdaLibFile])
    -> LibM [AgdaLibFile] -> TCM [AgdaLibFile]
    forall a b. (a -> b) -> a -> b
    $ Maybe FilePath -> LibM [AgdaLibFile]
    getInstalledLibraries (CommandLineOptions -> Maybe FilePath
    optOverrideLibrariesFile CommandLineOptions
    o)
        [FilePath]
    paths     <- LibM [FilePath] -> TCM [FilePath]
    forall a. LibM a -> TCM a
    libToTCM (LibM [FilePath] -> TCM [FilePath])
    -> LibM [FilePath] -> TCM [FilePath]
    forall a b. (a -> b) -> a -> b
    $ Maybe FilePath -> [AgdaLibFile] -> [FilePath] -> LibM [FilePath]
    libraryIncludePaths (CommandLineOptions -> Maybe FilePath
    optOverrideLibrariesFile CommandLineOptions
    o) [AgdaLibFile]
    installed [FilePath]
    libs
        CommandLineOptions -> TCMT IO CommandLineOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return CommandLineOptions
    o{ optIncludePaths :: [FilePath]
    optIncludePaths = [FilePath]
    paths [FilePath] -> [FilePath] -> [FilePath]
    forall a. [a] -> [a] -> [a]
    ++ CommandLineOptions -> [FilePath]
    optIncludePaths CommandLineOptions
    o }

    addDefaultLibraries
      :: AbsolutePath
         -- ^ The base directory of relative paths.
      -> CommandLineOptions
      -> TCM CommandLineOptions
    addDefaultLibraries :: AbsolutePath -> CommandLineOptions -> TCMT IO CommandLineOptions
    addDefaultLibraries AbsolutePath
    root CommandLineOptions
    o
      | SafeMode -> SafeMode
    not ([FilePath] -> SafeMode
    forall (t :: * -> *) a. Foldable t => t a -> SafeMode
    null ([FilePath] -> SafeMode) -> [FilePath] -> SafeMode
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions -> [FilePath]
    optLibraries CommandLineOptions
    o) SafeMode -> SafeMode -> SafeMode
    || SafeMode -> SafeMode
    not (CommandLineOptions -> SafeMode
    optUseLibs CommandLineOptions
    o) = CommandLineOptions -> TCMT IO CommandLineOptions
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CommandLineOptions
    o
      | SafeMode
    otherwise = do
      ([FilePath]
    libs, [FilePath]
    incs) <- LibM ([FilePath], [FilePath]) -> TCM ([FilePath], [FilePath])
    forall a. LibM a -> TCM a
    libToTCM (LibM ([FilePath], [FilePath]) -> TCM ([FilePath], [FilePath]))
    -> LibM ([FilePath], [FilePath]) -> TCM ([FilePath], [FilePath])
    forall a b. (a -> b) -> a -> b
    $ FilePath -> SafeMode -> LibM ([FilePath], [FilePath])
    getDefaultLibraries (AbsolutePath -> FilePath
    filePath AbsolutePath
    root) (CommandLineOptions -> SafeMode
    optDefaultLibs CommandLineOptions
    o)
      CommandLineOptions -> TCMT IO CommandLineOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return CommandLineOptions
    o{ optIncludePaths :: [FilePath]
    optIncludePaths = [FilePath]
    incs [FilePath] -> [FilePath] -> [FilePath]
    forall a. [a] -> [a] -> [a]
    ++ CommandLineOptions -> [FilePath]
    optIncludePaths CommandLineOptions
    o, optLibraries :: [FilePath]
    optLibraries = [FilePath]
    libs }

    -- This function is only called when an interactor exists
    -- (i.e. when Agda actually does something).
    addTrustedExecutables
      :: CommandLineOptions
      -> TCM CommandLineOptions
    addTrustedExecutables :: CommandLineOptions -> TCMT IO CommandLineOptions
    addTrustedExecutables CommandLineOptions
    o = do
      Map ExeName FilePath
    trustedExes <- LibM (Map ExeName FilePath) -> TCM (Map ExeName FilePath)
    forall a. LibM a -> TCM a
    libToTCM (LibM (Map ExeName FilePath) -> TCM (Map ExeName FilePath))
    -> LibM (Map ExeName FilePath) -> TCM (Map ExeName FilePath)
    forall a b. (a -> b) -> a -> b
    $ LibM (Map ExeName FilePath)
    getTrustedExecutables
      -- Wen, 2020-06-03
      -- Replace the map wholesale instead of computing the union because this function
      -- should never be called more than once, and doing so either has the same result
      -- or is a security risk.
      CommandLineOptions -> TCMT IO CommandLineOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return CommandLineOptions
    o{ optTrustedExecutables :: Map ExeName FilePath
    optTrustedExecutables = Map ExeName FilePath
    trustedExes }

    setOptionsFromPragma :: OptionsPragma -> TCM ()
    setOptionsFromPragma :: [FilePath] -> TCM ()
    setOptionsFromPragma [FilePath]
    ps = do
        CommandLineOptions
    opts <- TCMT IO CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions
        OptM PragmaOptions -> TCMT IO (Either FilePath PragmaOptions)
    forall (m :: * -> *) opts.
    Monad m =>
    OptM opts -> m (Either FilePath opts)
    runOptM ([FilePath] -> CommandLineOptions -> OptM PragmaOptions
    parsePragmaOptions [FilePath]
    ps CommandLineOptions
    opts) TCMT IO (Either FilePath PragmaOptions)
    -> (Either FilePath PragmaOptions -> TCM ()) -> TCM ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Left FilePath
    err    -> TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ FilePath -> TypeError
    GenericError FilePath
    err
          Right PragmaOptions
    opts' -> PragmaOptions -> TCM ()
    setPragmaOptions PragmaOptions
    opts'

    -- | Disable display forms.
    enableDisplayForms :: MonadTCEnv m => m a -> m a
    enableDisplayForms :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    enableDisplayForms =
      (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ \TCEnv
    e -> TCEnv
    e { envDisplayFormsEnabled :: SafeMode
    envDisplayFormsEnabled = SafeMode
    True }

    -- | Disable display forms.
    disableDisplayForms :: MonadTCEnv m => m a -> m a
    disableDisplayForms :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    disableDisplayForms =
      (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ \TCEnv
    e -> TCEnv
    e { envDisplayFormsEnabled :: SafeMode
    envDisplayFormsEnabled = SafeMode
    False }

    -- | Check if display forms are enabled.
    displayFormsEnabled :: MonadTCEnv m => m Bool
    displayFormsEnabled :: forall (m :: * -> *). MonadTCEnv m => m SafeMode
    displayFormsEnabled = (TCEnv -> SafeMode) -> m SafeMode
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> SafeMode
    envDisplayFormsEnabled

    -- | Gets the include directories.
    --
    -- Precondition: 'optAbsoluteIncludePaths' must be nonempty (i.e.
    -- 'setCommandLineOptions' must have run).

    getIncludeDirs :: HasOptions m => m [AbsolutePath]
    getIncludeDirs :: forall (m :: * -> *). HasOptions m => m [AbsolutePath]
    getIncludeDirs = do
      [AbsolutePath]
    incs <- CommandLineOptions -> [AbsolutePath]
    optAbsoluteIncludePaths (CommandLineOptions -> [AbsolutePath])
    -> m CommandLineOptions -> m [AbsolutePath]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions
      case [AbsolutePath]
    incs of
        [] -> m [AbsolutePath]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        [AbsolutePath]
    _  -> [AbsolutePath] -> m [AbsolutePath]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [AbsolutePath]
    incs

    -- | Makes the given directories absolute and stores them as include
    -- directories.
    --
    -- If the include directories change, then the state is reset
    -- (completely, except for the include directories and some other
    -- things).
    --
    -- An empty list is interpreted as @["."]@.

    setIncludeDirs :: [FilePath]    -- ^ New include directories.
                   -> AbsolutePath  -- ^ The base directory of relative paths.
                   -> TCM ()
    setIncludeDirs :: [FilePath] -> AbsolutePath -> TCM ()
    setIncludeDirs [FilePath]
    incs AbsolutePath
    root = do
      -- save the previous include dirs
      [AbsolutePath]
    oldIncs <- (TCState -> [AbsolutePath]) -> TCMT IO [AbsolutePath]
    forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
    getsTC TCState -> [AbsolutePath]
    forall a. LensIncludePaths a => a -> [AbsolutePath]
    Lens.getAbsoluteIncludePaths

      -- Add the current dir if no include path is given
      [FilePath]
    incs <- [FilePath] -> TCM [FilePath]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([FilePath] -> TCM [FilePath]) -> [FilePath] -> TCM [FilePath]
    forall a b. (a -> b) -> a -> b
    $ if [FilePath] -> SafeMode
    forall (t :: * -> *) a. Foldable t => t a -> SafeMode
    null [FilePath]
    incs then [FilePath
    "."] else [FilePath]
    incs
      -- Make paths absolute
      [AbsolutePath]
    incs <- [AbsolutePath] -> TCMT IO [AbsolutePath]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([AbsolutePath] -> TCMT IO [AbsolutePath])
    -> [AbsolutePath] -> TCMT IO [AbsolutePath]
    forall a b. (a -> b) -> a -> b
    $  (FilePath -> AbsolutePath) -> [FilePath] -> [AbsolutePath]
    forall a b. (a -> b) -> [a] -> [b]
    map (FilePath -> AbsolutePath
    mkAbsolute (FilePath -> AbsolutePath)
    -> (FilePath -> FilePath) -> FilePath -> AbsolutePath
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (AbsolutePath -> FilePath
    filePath AbsolutePath
    root FilePath -> FilePath -> FilePath
    </>)) [FilePath]
    incs

      -- Andreas, 2013-10-30  Add default include dir
          -- NB: This is an absolute file name, but
          -- Agda.Utils.FilePath wants to check absoluteness anyway.
      AbsolutePath
    primdir <- IO AbsolutePath -> TCMT IO AbsolutePath
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO AbsolutePath -> TCMT IO AbsolutePath)
    -> IO AbsolutePath -> TCMT IO AbsolutePath
    forall a b. (a -> b) -> a -> b
    $ FilePath -> AbsolutePath
    mkAbsolute (FilePath -> AbsolutePath) -> IO FilePath -> IO AbsolutePath
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IO FilePath
    getPrimitiveLibDir
          -- We add the default dir at the end, since it is then
          -- printed last in error messages.
          -- Might also be useful to overwrite default imports...
      [AbsolutePath]
    incs <- [AbsolutePath] -> TCMT IO [AbsolutePath]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([AbsolutePath] -> TCMT IO [AbsolutePath])
    -> [AbsolutePath] -> TCMT IO [AbsolutePath]
    forall a b. (a -> b) -> a -> b
    $ (AbsolutePath -> AbsolutePath) -> [AbsolutePath] -> [AbsolutePath]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    nubOn AbsolutePath -> AbsolutePath
    forall a. a -> a
    id ([AbsolutePath] -> [AbsolutePath])
    -> [AbsolutePath] -> [AbsolutePath]
    forall a b. (a -> b) -> a -> b
    $ [AbsolutePath]
    incs [AbsolutePath] -> [AbsolutePath] -> [AbsolutePath]
    forall a. [a] -> [a] -> [a]
    ++ [AbsolutePath
    primdir]

      FilePath -> VerboseLevel -> TCM Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    FilePath -> VerboseLevel -> TCM Doc -> m ()
    reportSDoc FilePath
    "setIncludeDirs" VerboseLevel
    10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCM Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCM Doc) -> Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat
        [ Doc
    "Old include directories:"
        , VerboseLevel -> Doc -> Doc
    nest VerboseLevel
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (AbsolutePath -> Doc) -> [AbsolutePath] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map AbsolutePath -> Doc
    forall a. Pretty a => a -> Doc
    pretty [AbsolutePath]
    oldIncs
        , Doc
    "New include directories:"
        , VerboseLevel -> Doc -> Doc
    nest VerboseLevel
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (AbsolutePath -> Doc) -> [AbsolutePath] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map AbsolutePath -> Doc
    forall a. Pretty a => a -> Doc
    pretty [AbsolutePath]
    incs
        ]

      -- Check whether the include dirs have changed.  If yes, reset state.
      -- Andreas, 2013-10-30 comments:
      -- The logic, namely using the include-dirs variable as a driver
      -- for the interaction, qualifies for a code-obfuscation contest.
      -- I guess one Boolean more in the state cost 10.000 EUR at the time
      -- of this implementation...
      --
      -- Andreas, perhaps you have misunderstood something: If the include
      -- directories have changed and we do not reset the decoded modules,
      -- then we might (depending on how the rest of the code works) end
      -- up in a situation in which we use the contents of the file
      -- "old-path/M.agda", when the user actually meant
      -- "new-path/M.agda".
      SafeMode -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => SafeMode -> f () -> f ()
    when ([AbsolutePath] -> [AbsolutePath]
    forall a. Ord a => [a] -> [a]
    sort [AbsolutePath]
    oldIncs [AbsolutePath] -> [AbsolutePath] -> SafeMode
    forall a. Eq a => a -> a -> SafeMode
    /= [AbsolutePath] -> [AbsolutePath]
    forall a. Ord a => [a] -> [a]
    sort [AbsolutePath]
    incs) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        InteractionOutputCallback
    ho <- TCMT IO InteractionOutputCallback
    forall (m :: * -> *). ReadTCState m => m InteractionOutputCallback
    getInteractionOutputCallback
        [TCWarning]
    tcWarnings <- Lens' [TCWarning] TCState -> TCMT IO [TCWarning]
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' [TCWarning] TCState
    stTCWarnings -- restore already generated warnings
        Map FilePath ProjectConfig
    projectConfs <- Lens' (Map FilePath ProjectConfig) TCState
    -> TCMT IO (Map FilePath ProjectConfig)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (Map FilePath ProjectConfig) TCState
    stProjectConfigs  -- restore cached project configs & .agda-lib
        Map FilePath AgdaLibFile
    agdaLibFiles <- Lens' (Map FilePath AgdaLibFile) TCState
    -> TCMT IO (Map FilePath AgdaLibFile)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (Map FilePath AgdaLibFile) TCState
    stAgdaLibFiles    -- files, since they use absolute paths
        DecodedModules
    decodedModules <- TCM DecodedModules
    getDecodedModules
        (DecodedModules
    keptDecodedModules, ModuleToSource
    modFile) <- [AbsolutePath]
    -> DecodedModules -> TCM (DecodedModules, ModuleToSource)
    modulesToKeep [AbsolutePath]
    incs DecodedModules
    decodedModules
        TCM ()
    resetAllState
        Lens' [TCWarning] TCState -> [TCWarning] -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    setTCLens Lens' [TCWarning] TCState
    stTCWarnings [TCWarning]
    tcWarnings
        Lens' (Map FilePath ProjectConfig) TCState
    -> Map FilePath ProjectConfig -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    setTCLens Lens' (Map FilePath ProjectConfig) TCState
    stProjectConfigs Map FilePath ProjectConfig
    projectConfs
        Lens' (Map FilePath AgdaLibFile) TCState
    -> Map FilePath AgdaLibFile -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    setTCLens Lens' (Map FilePath AgdaLibFile) TCState
    stAgdaLibFiles Map FilePath AgdaLibFile
    agdaLibFiles
        InteractionOutputCallback -> TCM ()
    setInteractionOutputCallback InteractionOutputCallback
    ho
        DecodedModules -> TCM ()
    setDecodedModules DecodedModules
    keptDecodedModules
        Lens' ModuleToSource TCState -> ModuleToSource -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    setTCLens Lens' ModuleToSource TCState
    stModuleToSource ModuleToSource
    modFile

      [AbsolutePath] -> TCM ()
    forall (m :: * -> *). MonadTCState m => [AbsolutePath] -> m ()
    Lens.putAbsoluteIncludePaths [AbsolutePath]
    incs
      where
      -- A decoded module is kept if its top-level module name is resolved
      -- to the same absolute path using the old and the new include
      -- directories, and the same applies to all dependencies.
      --
      -- File system accesses are cached using the ModuleToSource data
      -- structure: For the old include directories this should mean that
      -- the file system is not accessed, but the file system is accessed
      -- for the new include directories, and certain changes to the file
      -- system could lead to interfaces being discarded. A new
      -- ModuleToSource structure, constructed using the new include
      -- directories, is returned.
      modulesToKeep
        :: [AbsolutePath]  -- New include directories.
        -> DecodedModules  -- Old decoded modules.
        -> TCM (DecodedModules, ModuleToSource)
      modulesToKeep :: [AbsolutePath]
    -> DecodedModules -> TCM (DecodedModules, ModuleToSource)
    modulesToKeep [AbsolutePath]
    incs DecodedModules
    old = Map ModuleName ModuleInfo
    -> ModuleToSource
    -> [ModuleInfo]
    -> TCM (DecodedModules, ModuleToSource)
    process Map ModuleName ModuleInfo
    forall k a. Map k a
    Map.empty ModuleToSource
    forall k a. Map k a
    Map.empty [ModuleInfo]
    modules
        where
        -- A graph with one node per module in old, and an edge from m to
        -- n if the module corresponding to m imports the module
        -- corresponding to n.
        dependencyGraph :: G.Graph A.ModuleName ()
        dependencyGraph :: Graph ModuleName ()
    dependencyGraph =
          [ModuleName] -> Graph ModuleName ()
    forall n e. Ord n => [n] -> Graph n e
    G.fromNodes
            [ Interface -> ModuleName
    iModuleName (Interface -> ModuleName) -> Interface -> ModuleName
    forall a b. (a -> b) -> a -> b
    $ ModuleInfo -> Interface
    miInterface ModuleInfo
    m
            | ModuleInfo
    m <- DecodedModules -> [ModuleInfo]
    forall k a. Map k a -> [a]
    Map.elems DecodedModules
    old
            ]
            Graph ModuleName () -> Graph ModuleName () -> Graph ModuleName ()
    forall n e. Ord n => Graph n e -> Graph n e -> Graph n e
    `G.union`
          [Edge ModuleName ()] -> Graph ModuleName ()
    forall n e. Ord n => [Edge n e] -> Graph n e
    G.fromEdges
            [ Edge :: forall n e. n -> n -> e -> Edge n e
    G.Edge
                { source :: ModuleName
    source = Interface -> ModuleName
    iModuleName (Interface -> ModuleName) -> Interface -> ModuleName
    forall a b. (a -> b) -> a -> b
    $ ModuleInfo -> Interface
    miInterface ModuleInfo
    m
                , target :: ModuleName
    target = ModuleName
    d
                , label :: ()
    label = ()
                }
            | ModuleInfo
    m      <- DecodedModules -> [ModuleInfo]
    forall k a. Map k a -> [a]
    Map.elems DecodedModules
    old
            , (ModuleName
    d, Hash
    _) <- Interface -> [(ModuleName, Hash)]
    iImportedModules (Interface -> [(ModuleName, Hash)])
    -> Interface -> [(ModuleName, Hash)]
    forall a b. (a -> b) -> a -> b
    $ ModuleInfo -> Interface
    miInterface ModuleInfo
    m
            ]

        -- All the modules from old, sorted so that all of a module's
        -- dependencies precede it in the list.
        modules :: [ModuleInfo]
        modules :: [ModuleInfo]
    modules =
          (SCC ModuleName -> ModuleInfo) -> [SCC ModuleName] -> [ModuleInfo]
    forall a b. (a -> b) -> [a] -> [b]
    map (\case
                  Graph.CyclicSCC{} ->
                    -- Agda does not allow cycles in the dependency graph.
                    ModuleInfo
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                  Graph.AcyclicSCC ModuleName
    m ->
                    case TopLevelModuleName -> DecodedModules -> Maybe ModuleInfo
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup (ModuleName -> TopLevelModuleName
    A.toTopLevelModuleName ModuleName
    m) DecodedModules
    old of
                      Just ModuleInfo
    m  -> ModuleInfo
    m
                      Maybe ModuleInfo
    Nothing -> ModuleInfo
    forall a. HasCallStack => a
    __IMPOSSIBLE__) ([SCC ModuleName] -> [ModuleInfo])
    -> [SCC ModuleName] -> [ModuleInfo]
    forall a b. (a -> b) -> a -> b
    $
          Graph ModuleName () -> [SCC ModuleName]
    forall n e. Ord n => Graph n e -> [SCC n]
    G.sccs' Graph ModuleName ()
    dependencyGraph

        process ::
          Map A.ModuleName ModuleInfo -> ModuleToSource -> [ModuleInfo] ->
          TCM (DecodedModules, ModuleToSource)
        process :: Map ModuleName ModuleInfo
    -> ModuleToSource
    -> [ModuleInfo]
    -> TCM (DecodedModules, ModuleToSource)
    process !Map ModuleName ModuleInfo
    keep !ModuleToSource
    modFile [] = (DecodedModules, ModuleToSource)
    -> TCM (DecodedModules, ModuleToSource)
    forall (m :: * -> *) a. Monad m => a -> m a
    return
          ( [(TopLevelModuleName, ModuleInfo)] -> DecodedModules
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList ([(TopLevelModuleName, ModuleInfo)] -> DecodedModules)
    -> [(TopLevelModuleName, ModuleInfo)] -> DecodedModules
    forall a b. (a -> b) -> a -> b
    $
            ((ModuleName, ModuleInfo) -> (TopLevelModuleName, ModuleInfo))
    -> [(ModuleName, ModuleInfo)] -> [(TopLevelModuleName, ModuleInfo)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((ModuleName -> TopLevelModuleName)
    -> (ModuleName, ModuleInfo) -> (TopLevelModuleName, ModuleInfo)
    forall a c b. (a -> c) -> (a, b) -> (c, b)
    mapFst ModuleName -> TopLevelModuleName
    A.toTopLevelModuleName) ([(ModuleName, ModuleInfo)] -> [(TopLevelModuleName, ModuleInfo)])
    -> [(ModuleName, ModuleInfo)] -> [(TopLevelModuleName, ModuleInfo)]
    forall a b. (a -> b) -> a -> b
    $
            Map ModuleName ModuleInfo -> [(ModuleName, ModuleInfo)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map ModuleName ModuleInfo
    keep
          , ModuleToSource
    modFile
          )
        process Map ModuleName ModuleInfo
    keep ModuleToSource
    modFile (ModuleInfo
    m : [ModuleInfo]
    ms) = do
          let deps :: [ModuleName]
    deps     = ((ModuleName, Hash) -> ModuleName)
    -> [(ModuleName, Hash)] -> [ModuleName]
    forall a b. (a -> b) -> [a] -> [b]
    map (ModuleName, Hash) -> ModuleName
    forall a b. (a, b) -> a
    fst ([(ModuleName, Hash)] -> [ModuleName])
    -> [(ModuleName, Hash)] -> [ModuleName]
    forall a b. (a -> b) -> a -> b
    $ Interface -> [(ModuleName, Hash)]
    iImportedModules (Interface -> [(ModuleName, Hash)])
    -> Interface -> [(ModuleName, Hash)]
    forall a b. (a -> b) -> a -> b
    $ ModuleInfo -> Interface
    miInterface ModuleInfo
    m
              depsKept :: SafeMode
    depsKept = (ModuleName -> SafeMode) -> [ModuleName] -> SafeMode
    forall (t :: * -> *) a.
    Foldable t =>
    (a -> SafeMode) -> t a -> SafeMode
    all (ModuleName -> Map ModuleName ModuleInfo -> SafeMode
    forall k a. Ord k => k -> Map k a -> SafeMode
    `Map.member` Map ModuleName ModuleInfo
    keep) [ModuleName]
    deps
          (Map ModuleName ModuleInfo
    keep, ModuleToSource
    modFile) <-
            if SafeMode -> SafeMode
    not SafeMode
    depsKept then (Map ModuleName ModuleInfo, ModuleToSource)
    -> TCMT IO (Map ModuleName ModuleInfo, ModuleToSource)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Map ModuleName ModuleInfo
    keep, ModuleToSource
    modFile) else do
            let n :: ModuleName
    n = Interface -> ModuleName
    iModuleName (Interface -> ModuleName) -> Interface -> ModuleName
    forall a b. (a -> b) -> a -> b
    $ ModuleInfo -> Interface
    miInterface ModuleInfo
    m
                t :: TopLevelModuleName
    t = ModuleName -> TopLevelModuleName
    A.toTopLevelModuleName ModuleName
    n
            Either FindError SourceFile
    oldF            <- TopLevelModuleName -> TCM (Either FindError SourceFile)
    findFile' TopLevelModuleName
    t
            (Either FindError SourceFile
    newF, ModuleToSource
    modFile) <- IO (Either FindError SourceFile, ModuleToSource)
    -> TCMT IO (Either FindError SourceFile, ModuleToSource)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (Either FindError SourceFile, ModuleToSource)
     -> TCMT IO (Either FindError SourceFile, ModuleToSource))
    -> IO (Either FindError SourceFile, ModuleToSource)
    -> TCMT IO (Either FindError SourceFile, ModuleToSource)
    forall a b. (a -> b) -> a -> b
    $ [AbsolutePath]
    -> TopLevelModuleName
    -> ModuleToSource
    -> IO (Either FindError SourceFile, ModuleToSource)
    findFile'' [AbsolutePath]
    incs TopLevelModuleName
    t ModuleToSource
    modFile
            (Map ModuleName ModuleInfo, ModuleToSource)
    -> TCMT IO (Map ModuleName ModuleInfo, ModuleToSource)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Map ModuleName ModuleInfo, ModuleToSource)
     -> TCMT IO (Map ModuleName ModuleInfo, ModuleToSource))
    -> (Map ModuleName ModuleInfo, ModuleToSource)
    -> TCMT IO (Map ModuleName ModuleInfo, ModuleToSource)
    forall a b. (a -> b) -> a -> b
    $ case (Either FindError SourceFile
    oldF, Either FindError SourceFile
    newF) of
              (Right SourceFile
    f1, Right SourceFile
    f2) | SourceFile
    f1 SourceFile -> SourceFile -> SafeMode
    forall a. Eq a => a -> a -> SafeMode
    == SourceFile
    f2 ->
                (ModuleName
    -> ModuleInfo
    -> Map ModuleName ModuleInfo
    -> Map ModuleName ModuleInfo
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert ModuleName
    n ModuleInfo
    m Map ModuleName ModuleInfo
    keep, ModuleToSource
    modFile)
              (Either FindError SourceFile, Either FindError SourceFile)
    _ -> (Map ModuleName ModuleInfo
    keep, ModuleToSource
    modFile)
          Map ModuleName ModuleInfo
    -> ModuleToSource
    -> [ModuleInfo]
    -> TCM (DecodedModules, ModuleToSource)
    process Map ModuleName ModuleInfo
    keep ModuleToSource
    modFile [ModuleInfo]
    ms

    isPropEnabled :: HasOptions m => m Bool
    isPropEnabled :: forall (m :: * -> *). HasOptions m => m SafeMode
    isPropEnabled = PragmaOptions -> SafeMode
    optProp (PragmaOptions -> SafeMode) -> m PragmaOptions -> m SafeMode
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

    isTwoLevelEnabled :: HasOptions m => m Bool
    isTwoLevelEnabled :: forall (m :: * -> *). HasOptions m => m SafeMode
    isTwoLevelEnabled = WithDefault 'False -> SafeMode
    forall (b :: SafeMode). KnownBool b => WithDefault b -> SafeMode
    collapseDefault (WithDefault 'False -> SafeMode)
    -> (PragmaOptions -> WithDefault 'False)
    -> PragmaOptions
    -> SafeMode
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    optTwoLevel (PragmaOptions -> SafeMode) -> m PragmaOptions -> m SafeMode
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

    {-# SPECIALIZE hasUniversePolymorphism :: TCM Bool #-}
    hasUniversePolymorphism :: HasOptions m => m Bool
    hasUniversePolymorphism :: forall (m :: * -> *). HasOptions m => m SafeMode
    hasUniversePolymorphism = PragmaOptions -> SafeMode
    optUniversePolymorphism (PragmaOptions -> SafeMode) -> m PragmaOptions -> m SafeMode
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

    showImplicitArguments :: HasOptions m => m Bool
    showImplicitArguments :: forall (m :: * -> *). HasOptions m => m SafeMode
    showImplicitArguments = PragmaOptions -> SafeMode
    optShowImplicit (PragmaOptions -> SafeMode) -> m PragmaOptions -> m SafeMode
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

    showIrrelevantArguments :: HasOptions m => m Bool
    showIrrelevantArguments :: forall (m :: * -> *). HasOptions m => m SafeMode
    showIrrelevantArguments = PragmaOptions -> SafeMode
    optShowIrrelevant (PragmaOptions -> SafeMode) -> m PragmaOptions -> m SafeMode
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

    showIdentitySubstitutions :: HasOptions m => m Bool
    showIdentitySubstitutions :: forall (m :: * -> *). HasOptions m => m SafeMode
    showIdentitySubstitutions = PragmaOptions -> SafeMode
    optShowIdentitySubstitutions (PragmaOptions -> SafeMode) -> m PragmaOptions -> m SafeMode
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

    -- | Switch on printing of implicit and irrelevant arguments.
    --   E.g. for reification in with-function generation.
    --
    --   Restores all 'PragmaOptions' after completion.
    --   Thus, do not attempt to make persistent 'PragmaOptions'
    --   changes in a `withShowAllArguments` bracket.

    withShowAllArguments :: ReadTCState m => m a -> m a
    withShowAllArguments :: forall (m :: * -> *) a. ReadTCState m => m a -> m a
    withShowAllArguments = SafeMode -> m a -> m a
    forall (m :: * -> *) a. ReadTCState m => SafeMode -> m a -> m a
    withShowAllArguments' SafeMode
    True

    withShowAllArguments' :: ReadTCState m => Bool -> m a -> m a
    withShowAllArguments' :: forall (m :: * -> *) a. ReadTCState m => SafeMode -> m a -> m a
    withShowAllArguments' SafeMode
    yes = (PragmaOptions -> PragmaOptions) -> m a -> m a
    forall (m :: * -> *) a.
    ReadTCState m =>
    (PragmaOptions -> PragmaOptions) -> m a -> m a
    withPragmaOptions ((PragmaOptions -> PragmaOptions) -> m a -> m a)
    -> (PragmaOptions -> PragmaOptions) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ \ PragmaOptions
    opts ->
      PragmaOptions
    opts { optShowImplicit :: SafeMode
    optShowImplicit = SafeMode
    yes, optShowIrrelevant :: SafeMode
    optShowIrrelevant = SafeMode
    yes }

    -- | Change 'PragmaOptions' for a computation and restore afterwards.
    withPragmaOptions :: ReadTCState m => (PragmaOptions -> PragmaOptions) -> m a -> m a
    withPragmaOptions :: forall (m :: * -> *) a.
    ReadTCState m =>
    (PragmaOptions -> PragmaOptions) -> m a -> m a
    withPragmaOptions = Lens' PragmaOptions TCState
    -> (PragmaOptions -> PragmaOptions) -> m a -> m a
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' a TCState -> (a -> a) -> m b -> m b
    locallyTCState Lens' PragmaOptions TCState
    stPragmaOptions

    positivityCheckEnabled :: HasOptions m => m Bool
    positivityCheckEnabled :: forall (m :: * -> *). HasOptions m => m SafeMode
    positivityCheckEnabled = SafeMode -> SafeMode
    not (SafeMode -> SafeMode)
    -> (PragmaOptions -> SafeMode) -> PragmaOptions -> SafeMode
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> SafeMode
    optDisablePositivity (PragmaOptions -> SafeMode) -> m PragmaOptions -> m SafeMode
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

    {-# SPECIALIZE typeInType :: TCM Bool #-}
    typeInType :: HasOptions m => m Bool
    typeInType :: forall (m :: * -> *). HasOptions m => m SafeMode
    typeInType = SafeMode -> SafeMode
    not (SafeMode -> SafeMode)
    -> (PragmaOptions -> SafeMode) -> PragmaOptions -> SafeMode
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> SafeMode
    optUniverseCheck (PragmaOptions -> SafeMode) -> m PragmaOptions -> m SafeMode
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

    etaEnabled :: HasOptions m => m Bool
    etaEnabled :: forall (m :: * -> *). HasOptions m => m SafeMode
    etaEnabled = PragmaOptions -> SafeMode
    optEta (PragmaOptions -> SafeMode) -> m PragmaOptions -> m SafeMode
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

    maxInstanceSearchDepth :: HasOptions m => m Int
    maxInstanceSearchDepth :: forall (m :: * -> *). HasOptions m => m VerboseLevel
    maxInstanceSearchDepth = PragmaOptions -> VerboseLevel
    optInstanceSearchDepth (PragmaOptions -> VerboseLevel)
    -> m PragmaOptions -> m VerboseLevel
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

    maxInversionDepth :: HasOptions m => m Int
    maxInversionDepth :: forall (m :: * -> *). HasOptions m => m VerboseLevel
    maxInversionDepth = PragmaOptions -> VerboseLevel
    optInversionMaxDepth (PragmaOptions -> VerboseLevel)
    -> m PragmaOptions -> m VerboseLevel
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

    -- | Returns the 'Language' currently in effect.

    getLanguage :: HasOptions m => m Language
    getLanguage :: forall (m :: * -> *). HasOptions m => m Language
    getLanguage = do
      PragmaOptions
    opts <- m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions
      Language -> m Language
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Language -> m Language) -> Language -> m Language
    forall a b. (a -> b) -> a -> b
    $
        if SafeMode -> SafeMode
    not (WithDefault 'False -> SafeMode
    forall (b :: SafeMode). KnownBool b => WithDefault b -> SafeMode
    collapseDefault (PragmaOptions -> WithDefault 'False
    optWithoutK PragmaOptions
    opts)) then Language
    WithK else
        case PragmaOptions -> Maybe Cubical
    optCubical PragmaOptions
    opts of
          Just Cubical
    variant -> Cubical -> Language
    Cubical Cubical
    variant
          Maybe Cubical
    Nothing      -> Language
    WithoutK