    {-# LANGUAGE OverloadedLists #-}
    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | Library management.
    --
    --   Sample use:
    --
    --   @
    --     -- Get libraries as listed in @.agda/libraries@ file.
    --     libs <- getInstalledLibraries Nothing
    --
    --     -- Get the libraries (and immediate paths) relevant for @projectRoot@.
    --     -- This involves locating and processing the @.agda-lib@ file for the project.
    --     (libNames, includePaths) <-  getDefaultLibraries projectRoot True
    --
    --     -- Get include paths of depended-on libraries.
    --     resolvedPaths <- libraryIncludePaths Nothing libs libNames
    --
    --     let allPaths = includePaths ++ resolvedPaths
    --   @
    --
    module Agda.Interaction.Library
      ( findProjectRoot
      , getDefaultLibraries
      , getInstalledLibraries
      , getTrustedExecutables
      , libraryIncludePaths
      , getAgdaLibFile
      , getPrimitiveLibDir
      , classifyBuiltinModule_
      , builtinModules
      , builtinModulesWithSafePostulates
      , builtinModulesWithUnsafePostulates
      , primitiveModules
      , LibName, parseLibName
      , OptionsPragma(..)
      , AgdaLibFile(..)
      , ExeName
      , LibM
      , mkLibM
      , LibWarning(..)
      , LibPositionInfo(..)
      , libraryWarningName
      , ProjectConfig(..)
      -- * Exported for testing
      , findLib'
      ) where

    import qualified Control.Exception as E
    import Control.Monad.Except   ( runExceptT, MonadError, throwError )
    import Control.Monad.Writer   ( Writer, runWriterT, tell )
    import Control.Monad.IO.Class ( MonadIO(..) )

    import Data.Bifunctor ( second )
    import Data.Either
    import Data.Function (on)
    import qualified Data.List as List
    import Data.Map ( Map )
    import qualified Data.Map as Map
    import Data.Set ( Set )
    import qualified Data.Set as Set
    import qualified Data.Text as T

    import System.Directory
    import System.FilePath
    import System.IO.Error ( isPermissionError )

    import Agda.Interaction.Library.Base
    import Agda.Interaction.Library.Parse

    import Agda.TypeChecking.Monad.Base.Types ( IsBuiltinModule(..) )

    import Agda.Utils.Environment
    import Agda.Utils.FileName
    import Agda.Utils.IO ( catchIO )
    import qualified Agda.Utils.IO.UTF8 as UTF8
    import Agda.Utils.Lens
    import Agda.Utils.List
    import Agda.Utils.List1             ( List1, pattern (:|) )
    import Agda.Utils.List2             ( pattern List2 )
    import qualified Agda.Utils.List1   as List1
    import qualified Agda.Utils.List2   as List2
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Singleton
    import Agda.Utils.Tuple ( mapSndM )

    import Agda.Setup ( getDataFileName, getAgdaAppDir )
    import Agda.Version

    ------------------------------------------------------------------------
    -- * Types and Monads
    ------------------------------------------------------------------------

    -- | Raise collected 'LibErrors' as exception.
    --
    mkLibM :: [AgdaLibFile] -> LibErrorIO a -> LibM a
    mkLibM :: forall a. [AgdaLibFile] -> LibErrorIO a -> LibM a
    mkLibM [AgdaLibFile]
    libs LibErrorIO a
    m = do
      (x, ews) <- WriterT [LibWarning] (StateT LibState IO) (a, LibErrWarns)
    -> ExceptT
         LibErrors
         (WriterT [LibWarning] (StateT LibState IO))
         (a, LibErrWarns)
    forall (m :: * -> *) a. Monad m => m a -> ExceptT LibErrors m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (WriterT [LibWarning] (StateT LibState IO) (a, LibErrWarns)
     -> ExceptT
          LibErrors
          (WriterT [LibWarning] (StateT LibState IO))
          (a, LibErrWarns))
    -> WriterT [LibWarning] (StateT LibState IO) (a, LibErrWarns)
    -> ExceptT
         LibErrors
         (WriterT [LibWarning] (StateT LibState IO))
         (a, LibErrWarns)
    forall a b. (a -> b) -> a -> b
    $ StateT LibState IO (a, LibErrWarns)
    -> WriterT [LibWarning] (StateT LibState IO) (a, LibErrWarns)
    forall (m :: * -> *) a. Monad m => m a -> WriterT [LibWarning] m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (StateT LibState IO (a, LibErrWarns)
     -> WriterT [LibWarning] (StateT LibState IO) (a, LibErrWarns))
    -> StateT LibState IO (a, LibErrWarns)
    -> WriterT [LibWarning] (StateT LibState IO) (a, LibErrWarns)
    forall a b. (a -> b) -> a -> b
    $ LibErrorIO a -> StateT LibState IO (a, LibErrWarns)
    forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
    runWriterT LibErrorIO a
    m
      let (errs, warns) = partitionEithers ews
      tell warns
      () <- List1.unlessNull errs \ List1 LibError
    errs -> LibErrors
    -> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) ()
    forall a.
    LibErrors
    -> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (LibErrors
     -> ExceptT
          LibErrors (WriterT [LibWarning] (StateT LibState IO)) ())
    -> LibErrors
    -> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) ()
    forall a b. (a -> b) -> a -> b
    $ [AgdaLibFile] -> List1 LibError -> LibErrors
    LibErrors [AgdaLibFile]
    libs List1 LibError
    errs
      return x

    ------------------------------------------------------------------------
    -- * Resources
    ------------------------------------------------------------------------

    -- | Returns the absolute default lib dir. This directory is used to
    -- store the Primitive.agda file.
    getPrimitiveLibDir :: IO AbsolutePath
    getPrimitiveLibDir :: IO AbsolutePath
    getPrimitiveLibDir = do
      libdir <- AbsolutePath -> FilePath
    filePath (AbsolutePath -> FilePath) -> IO AbsolutePath -> IO FilePath
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (FilePath -> IO AbsolutePath
    absolute (FilePath -> IO AbsolutePath) -> IO FilePath -> IO AbsolutePath
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< FilePath -> IO FilePath
    getDataFileName FilePath
    "lib")
      ifM (doesDirectoryExist libdir)
          (return $ AbsolutePath $ T.pack $ libdir </> "prim")
          (error $ "The lib directory " ++ libdir ++ " does not exist")

    -- | The @~/.agda/libraries@ file lists the libraries Agda should know about.
    --   The content of @libraries@ is a list of paths to @.agda-lib@ files.
    --
    --   Agda honors also version-specific @libraries@ files, e.g. @libraries-2.6.0@.
    --
    --   @defaultLibraryFiles@ gives a list of all @libraries@ files Agda should process
    --   by default.  The first file in this list that exists is actually used.
    --
    defaultLibraryFiles :: List1 FilePath
    defaultLibraryFiles :: NonEmpty FilePath
    defaultLibraryFiles = (FilePath
    "libraries-" FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    version) FilePath -> [FilePath] -> NonEmpty FilePath
    forall a. a -> [a] -> NonEmpty a
    :| FilePath
    "libraries" FilePath -> [FilePath] -> [FilePath]
    forall a. a -> [a] -> [a]
    : []

    -- | The @defaultsFile@ contains a list of library names relevant for each Agda project.
    --
    defaultsFile :: FilePath
    defaultsFile :: FilePath
    defaultsFile = FilePath
    "defaults"

    -- | The @~/.agda/executables@ file lists the executables Agda should know about.
    --   The content of @executables@ is a list of paths to executables.
    --
    --   Agda honors also version-specific @executables@ files, e.g. @executables-2.6.0@.
    --
    --   @defaultExecutablesFiles@ gives a list of all @executables@ Agda should process
    --   by default.  The first file in this list that exists is actually used.
    --
    defaultExecutableFiles :: List1 FilePath
    defaultExecutableFiles :: NonEmpty FilePath
    defaultExecutableFiles = (FilePath
    "executables-" FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    version) FilePath -> [FilePath] -> NonEmpty FilePath
    forall a. a -> [a] -> NonEmpty a
    :| FilePath
    "executables" FilePath -> [FilePath] -> [FilePath]
    forall a. a -> [a] -> [a]
    : []

    ------------------------------------------------------------------------
    -- * Agda builtin modules
    ------------------------------------------------------------------------

    -- | Prefix path with @Agda.Builtin@.

    agdaBuiltin :: FilePath -> FilePath
    agdaBuiltin :: FilePath -> FilePath
    agdaBuiltin = (FilePath
    "Agda" FilePath -> FilePath -> FilePath
    </>) (FilePath -> FilePath)
    -> (FilePath -> FilePath) -> FilePath -> FilePath
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (FilePath
    "Builtin" FilePath -> FilePath -> FilePath
    </>)

    -- | The very magical, auto-imported modules.

    primitiveModules :: Set FilePath
    primitiveModules :: Set FilePath
    primitiveModules = [FilePath] -> Set FilePath
    forall a. Ord a => [a] -> Set a
    Set.fromList
      [ FilePath
    "Agda" FilePath -> FilePath -> FilePath
    </> FilePath
    "Primitive.agda"
      , FilePath
    "Agda" FilePath -> FilePath -> FilePath
    </> FilePath
    "Primitive" FilePath -> FilePath -> FilePath
    </> FilePath
    "Cubical.agda"
      ]

    -- | These builtins may use postulates, and are still considered @--safe@.

    builtinModulesWithSafePostulates :: Set FilePath
    builtinModulesWithSafePostulates :: Set FilePath
    builtinModulesWithSafePostulates =
      (Set FilePath
    primitiveModules Set FilePath -> Set FilePath -> Set FilePath
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.union`) (Set FilePath -> Set FilePath) -> Set FilePath -> Set FilePath
    forall a b. (a -> b) -> a -> b
    $ [FilePath] -> Set FilePath
    forall a. Ord a => [a] -> Set a
    Set.fromList ([FilePath] -> Set FilePath) -> [FilePath] -> Set FilePath
    forall a b. (a -> b) -> a -> b
    $
      (FilePath -> FilePath) -> [FilePath] -> [FilePath]
    forall a b. (a -> b) -> [a] -> [b]
    map FilePath -> FilePath
    agdaBuiltin ([FilePath] -> [FilePath]) -> [FilePath] -> [FilePath]
    forall a b. (a -> b) -> a -> b
    $
        [ FilePath
    Item [FilePath]
    "Bool.agda"
        , FilePath
    Item [FilePath]
    "Char.agda"
        , FilePath
    "Char" FilePath -> FilePath -> FilePath
    </> FilePath
    "Properties.agda"
        , FilePath
    Item [FilePath]
    "Coinduction.agda"
        , FilePath
    "Cubical" FilePath -> FilePath -> FilePath
    </> FilePath
    "Equiv.agda"
        , FilePath
    "Cubical" FilePath -> FilePath -> FilePath
    </> FilePath
    "Glue.agda"
        , FilePath
    "Cubical" FilePath -> FilePath -> FilePath
    </> FilePath
    "HCompU.agda"
        , FilePath
    "Cubical" FilePath -> FilePath -> FilePath
    </> FilePath
    "Id.agda"
        , FilePath
    "Cubical" FilePath -> FilePath -> FilePath
    </> FilePath
    "Path.agda"
        , FilePath
    "Cubical" FilePath -> FilePath -> FilePath
    </> FilePath
    "Sub.agda"
        , FilePath
    "Equality" FilePath -> FilePath -> FilePath
    </> FilePath
    "Erase.agda"
        , FilePath
    Item [FilePath]
    "Equality.agda"
        , FilePath
    Item [FilePath]
    "Float.agda"
        , FilePath
    "Float" FilePath -> FilePath -> FilePath
    </> FilePath
    "Properties.agda"
        , FilePath
    Item [FilePath]
    "FromNat.agda"
        , FilePath
    Item [FilePath]
    "FromNeg.agda"
        , FilePath
    Item [FilePath]
    "FromString.agda"
        , FilePath
    Item [FilePath]
    "Int.agda"
        , FilePath
    Item [FilePath]
    "IO.agda"
        , FilePath
    Item [FilePath]
    "List.agda"
        , FilePath
    Item [FilePath]
    "Maybe.agda"
        , FilePath
    Item [FilePath]
    "Nat.agda"
        , FilePath
    Item [FilePath]
    "Reflection.agda"
        , FilePath
    "Reflection" FilePath -> FilePath -> FilePath
    </> FilePath
    "Properties.agda"
        , FilePath
    "Reflection" FilePath -> FilePath -> FilePath
    </> FilePath
    "External.agda"
        , FilePath
    Item [FilePath]
    "Sigma.agda"
        , FilePath
    Item [FilePath]
    "Size.agda"
        , FilePath
    Item [FilePath]
    "Strict.agda"
        , FilePath
    Item [FilePath]
    "String.agda"
        , FilePath
    "String" FilePath -> FilePath -> FilePath
    </> FilePath
    "Properties.agda"
        , FilePath
    Item [FilePath]
    "Unit.agda"
        , FilePath
    Item [FilePath]
    "Word.agda"
        , FilePath
    "Word" FilePath -> FilePath -> FilePath
    </> FilePath
    "Properties.agda"
        ]

    -- | These builtins may not use postulates under @--safe@. They are not
    --   automatically unsafe, but will be if they use an unsafe feature.

    builtinModulesWithUnsafePostulates :: Set FilePath
    builtinModulesWithUnsafePostulates :: Set FilePath
    builtinModulesWithUnsafePostulates = [FilePath] -> Set FilePath
    forall a. Ord a => [a] -> Set a
    Set.fromList ([FilePath] -> Set FilePath) -> [FilePath] -> Set FilePath
    forall a b. (a -> b) -> a -> b
    $
      (FilePath -> FilePath) -> [FilePath] -> [FilePath]
    forall a b. (a -> b) -> [a] -> [b]
    map FilePath -> FilePath
    agdaBuiltin ([FilePath] -> [FilePath]) -> [FilePath] -> [FilePath]
    forall a b. (a -> b) -> a -> b
    $
        [ FilePath
    Item [FilePath]
    "TrustMe.agda"
        , FilePath
    "Equality" FilePath -> FilePath -> FilePath
    </> FilePath
    "Rewrite.agda"
        ]

    -- | All builtin modules.

    builtinModules :: Set FilePath
    builtinModules :: Set FilePath
    builtinModules = Set FilePath
    builtinModulesWithSafePostulates Set FilePath -> Set FilePath -> Set FilePath
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.union`
                     Set FilePath
    builtinModulesWithUnsafePostulates

    -- | Determine whether the second absolute path refers to one of Agda's primitive modules.
    --   The first argument should be the result of 'getPrimitiveLibDir'.
    --
    classifyBuiltinModule_ :: AbsolutePath -> AbsolutePath -> Maybe IsBuiltinModule
    classifyBuiltinModule_ :: AbsolutePath -> AbsolutePath -> Maybe IsBuiltinModule
    classifyBuiltinModule_ AbsolutePath
    primLibDir AbsolutePath
    fp = do
      f <- AbsolutePath -> AbsolutePath -> Maybe FilePath
    relativizeAbsolutePath AbsolutePath
    fp AbsolutePath
    primLibDir
      guard $ f `Set.member` builtinModules
      if f `Set.member` builtinModulesWithUnsafePostulates then return IsBuiltinModule
      else if f `Set.member` primitiveModules then return IsPrimitiveModule
      else return IsBuiltinModuleWithSafePostulates

    ------------------------------------------------------------------------
    -- * Get the libraries for the current project
    ------------------------------------------------------------------------

    -- | Find project root by looking for @.agda-lib@ files.
    --
    --   If there are none, look in the parent directories until one is found.

    findProjectConfig ::
         FilePath
           -- ^ Candidate (initially: the directory Agda was called in).
      -> LibM ProjectConfig
           -- ^ Actual root and @.agda-lib@ file for this project.
    findProjectConfig :: FilePath -> LibM ProjectConfig
    findProjectConfig FilePath
    root = do
      FilePath
    -> ExceptT
         LibErrors
         (WriterT [LibWarning] (StateT LibState IO))
         (Maybe ProjectConfig)
    forall (m :: * -> *).
    (MonadState LibState m, MonadIO m) =>
    FilePath -> m (Maybe ProjectConfig)
    getCachedProjectConfig FilePath
    root ExceptT
      LibErrors
      (WriterT [LibWarning] (StateT LibState IO))
      (Maybe ProjectConfig)
    -> (Maybe ProjectConfig -> LibM ProjectConfig)
    -> LibM ProjectConfig
    forall a b.
    ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
    -> (a
        -> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) b)
    -> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Just ProjectConfig
    conf -> ProjectConfig -> LibM ProjectConfig
    forall a.
    a
    -> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ProjectConfig
    conf
        Maybe ProjectConfig
    Nothing   -> LibM ProjectConfig -> LibM ProjectConfig
    handlePermissionException do
          libFiles <- IO [FilePath]
    -> ExceptT
         LibErrors (WriterT [LibWarning] (StateT LibState IO)) [FilePath]
    forall a.
    IO a
    -> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO [FilePath]
     -> ExceptT
          LibErrors (WriterT [LibWarning] (StateT LibState IO)) [FilePath])
    -> IO [FilePath]
    -> ExceptT
         LibErrors (WriterT [LibWarning] (StateT LibState IO)) [FilePath]
    forall a b. (a -> b) -> a -> b
    $ FilePath -> IO [FilePath]
    getDirectoryContents FilePath
    root IO [FilePath] -> ([FilePath] -> IO [FilePath]) -> IO [FilePath]
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>=
            (FilePath -> IO Bool) -> [FilePath] -> IO [FilePath]
    forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m [a]
    filterM (\FilePath
    file -> IO Bool -> IO Bool -> IO Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    and2M
              (Bool -> IO Bool
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> IO Bool) -> Bool -> IO Bool
    forall a b. (a -> b) -> a -> b
    $ FilePath -> FilePath
    takeExtension FilePath
    file FilePath -> FilePath -> Bool
    forall a. Eq a => a -> a -> Bool
    == FilePath
    ".agda-lib")
              (FilePath -> IO Bool
    doesFileExist (FilePath
    root FilePath -> FilePath -> FilePath
    </> FilePath
    file)))
          case libFiles of
            []     -> IO (Maybe FilePath)
    -> ExceptT
         LibErrors
         (WriterT [LibWarning] (StateT LibState IO))
         (Maybe FilePath)
    forall a.
    IO a
    -> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (FilePath -> IO (Maybe FilePath)
    upPath FilePath
    root) ExceptT
      LibErrors
      (WriterT [LibWarning] (StateT LibState IO))
      (Maybe FilePath)
    -> (Maybe FilePath -> LibM ProjectConfig) -> LibM ProjectConfig
    forall a b.
    ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
    -> (a
        -> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) b)
    -> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
              Just FilePath
    up -> do
                conf <- Lens' ProjectConfig LineNumber -> LensMap ProjectConfig LineNumber
    forall o i. Lens' o i -> LensMap o i
    over (LineNumber -> f LineNumber) -> ProjectConfig -> f ProjectConfig
    Lens' ProjectConfig LineNumber
    lensConfigAbove (LineNumber -> LineNumber -> LineNumber
    forall a. Num a => a -> a -> a
    + LineNumber
    1) (ProjectConfig -> ProjectConfig)
    -> LibM ProjectConfig -> LibM ProjectConfig
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> FilePath -> LibM ProjectConfig
    findProjectConfig FilePath
    up
                storeCachedProjectConfig root conf
                return conf
              Maybe FilePath
    Nothing -> ProjectConfig -> LibM ProjectConfig
    forall a.
    a
    -> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ProjectConfig
    DefaultProjectConfig
            [Item [FilePath]
    file] -> do
              let conf :: ProjectConfig
    conf = FilePath -> FilePath -> LineNumber -> ProjectConfig
    ProjectConfig FilePath
    root FilePath
    Item [FilePath]
    file LineNumber
    0
              FilePath
    -> ProjectConfig
    -> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) ()
    forall (m :: * -> *).
    (MonadState LibState m, MonadIO m) =>
    FilePath -> ProjectConfig -> m ()
    storeCachedProjectConfig FilePath
    root ProjectConfig
    conf
              ProjectConfig -> LibM ProjectConfig
    forall a.
    a
    -> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ProjectConfig
    conf
            FilePath
    f1:FilePath
    f2:[FilePath]
    files -> LibErrors -> LibM ProjectConfig
    forall a.
    LibErrors
    -> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (LibErrors -> LibM ProjectConfig)
    -> LibErrors -> LibM ProjectConfig
    forall a b. (a -> b) -> a -> b
    $ [AgdaLibFile] -> List1 LibError -> LibErrors
    LibErrors [] (List1 LibError -> LibErrors) -> List1 LibError -> LibErrors
    forall a b. (a -> b) -> a -> b
    $ LibError -> List1 LibError
    forall el coll. Singleton el coll => el -> coll
    singleton (LibError -> List1 LibError) -> LibError -> List1 LibError
    forall a b. (a -> b) -> a -> b
    $ Maybe LibPositionInfo -> LibError' -> LibError
    LibError Maybe LibPositionInfo
    forall a. Maybe a
    Nothing (LibError' -> LibError) -> LibError' -> LibError
    forall a b. (a -> b) -> a -> b
    $
              FilePath -> List2 FilePath -> LibError'
    SeveralAgdaLibFiles FilePath
    root (List2 FilePath -> LibError') -> List2 FilePath -> LibError'
    forall a b. (a -> b) -> a -> b
    $ FilePath -> FilePath -> [FilePath] -> List2 FilePath
    forall a. a -> a -> [a] -> List2 a
    List2 FilePath
    f1 FilePath
    f2 [FilePath]
    files

      where
        -- Andreas, 2024-06-26, issue #7331:
        -- In case of missing permission we terminate our search for the project file
        -- with the default value.
        handlePermissionException :: LibM ProjectConfig -> LibM ProjectConfig
        handlePermissionException :: LibM ProjectConfig -> LibM ProjectConfig
    handlePermissionException = (LibM ProjectConfig
     -> (IOError -> LibM ProjectConfig) -> LibM ProjectConfig)
    -> (IOError -> LibM ProjectConfig)
    -> LibM ProjectConfig
    -> LibM ProjectConfig
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip LibM ProjectConfig
    -> (IOError -> LibM ProjectConfig) -> LibM ProjectConfig
    forall e a.
    Exception e =>
    ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
    -> (e
        -> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a)
    -> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
    forall (m :: * -> *) e a.
    (CatchIO m, Exception e) =>
    m a -> (e -> m a) -> m a
    catchIO \ IOError
    e ->
          if IOError -> Bool
    isPermissionError IOError
    e then ProjectConfig -> LibM ProjectConfig
    forall a.
    a
    -> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ProjectConfig
    DefaultProjectConfig else IO ProjectConfig -> LibM ProjectConfig
    forall a.
    IO a
    -> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO ProjectConfig -> LibM ProjectConfig)
    -> IO ProjectConfig -> LibM ProjectConfig
    forall a b. (a -> b) -> a -> b
    $ IOError -> IO ProjectConfig
    forall e a. (HasCallStack, Exception e) => e -> IO a
    E.throwIO IOError
    e

        -- Note that "going up" one directory is OS dependent
        -- if the directory is a symlink.
        --
        -- Quoting from https://hackage.haskell.org/package/directory-1.3.6.1/docs/System-Directory.html#v:canonicalizePath :
        --
        --   Note that on Windows parent directories .. are always fully
        --   expanded before the symbolic links, as consistent with the
        --   rest of the Windows API (such as GetFullPathName). In
        --   contrast, on POSIX systems parent directories .. are
        --   expanded alongside symbolic links from left to right. To
        --   put this more concretely: if L is a symbolic link for R/P,
        --   then on Windows L\.. refers to ., whereas on other
        --   operating systems L/.. refers to R.
        upPath :: FilePath -> IO (Maybe FilePath)
        upPath :: FilePath -> IO (Maybe FilePath)
    upPath FilePath
    root = do
          up <- FilePath -> IO FilePath
    canonicalizePath (FilePath -> IO FilePath) -> FilePath -> IO FilePath
    forall a b. (a -> b) -> a -> b
    $ FilePath
    root FilePath -> FilePath -> FilePath
    </> FilePath
    ".."
          if up == root then return Nothing else return $ Just up

    -- | Get project root

    findProjectRoot :: FilePath -> LibM (Maybe FilePath)
    findProjectRoot :: FilePath
    -> ExceptT
         LibErrors
         (WriterT [LibWarning] (StateT LibState IO))
         (Maybe FilePath)
    findProjectRoot FilePath
    root = FilePath -> LibM ProjectConfig
    findProjectConfig FilePath
    root LibM ProjectConfig
    -> (ProjectConfig -> Maybe FilePath)
    -> ExceptT
         LibErrors
         (WriterT [LibWarning] (StateT LibState IO))
         (Maybe FilePath)
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \case
      ProjectConfig FilePath
    p FilePath
    _ LineNumber
    _  -> FilePath -> Maybe FilePath
    forall a. a -> Maybe a
    Just FilePath
    p
      ProjectConfig
    DefaultProjectConfig -> Maybe FilePath
    forall a. Maybe a
    Nothing

    -- | Get the content of the @.agda-lib@ file in the given project root.
    getAgdaLibFile :: FilePath -> LibM [AgdaLibFile]
    getAgdaLibFile :: FilePath -> LibM [AgdaLibFile]
    getAgdaLibFile FilePath
    path = FilePath -> LibM ProjectConfig
    findProjectConfig FilePath
    path LibM ProjectConfig
    -> (ProjectConfig -> LibM [AgdaLibFile]) -> LibM [AgdaLibFile]
    forall a b.
    ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
    -> (a
        -> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) b)
    -> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
      ProjectConfig
    DefaultProjectConfig          -> [AgdaLibFile] -> LibM [AgdaLibFile]
    forall a.
    a
    -> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
      ProjectConfig FilePath
    root FilePath
    file LineNumber
    above -> [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
    $
        (AgdaLibFile -> AgdaLibFile) -> [AgdaLibFile] -> [AgdaLibFile]
    forall a b. (a -> b) -> [a] -> [b]
    map (Lens' AgdaLibFile LineNumber -> LensSet AgdaLibFile LineNumber
    forall o i. Lens' o i -> LensSet o i
    set (LineNumber -> f LineNumber) -> AgdaLibFile -> f AgdaLibFile
    Lens' AgdaLibFile LineNumber
    libAbove LineNumber
    above) ([AgdaLibFile] -> [AgdaLibFile])
    -> LibErrorIO [AgdaLibFile] -> LibErrorIO [AgdaLibFile]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
        Maybe LibrariesFile
    -> [(LineNumber, FilePath)] -> LibErrorIO [AgdaLibFile]
    parseLibFiles Maybe LibrariesFile
    forall a. Maybe a
    Nothing [(LineNumber
    0, FilePath
    root FilePath -> FilePath -> FilePath
    </> FilePath
    file)]

    -- | Get dependencies and include paths for given project root:
    --
    --   Look for @.agda-lib@ files according to 'findAgdaLibFiles'.
    --   If none are found, use default dependencies (according to @defaults@ file)
    --   and current directory (project root).
    --
    getDefaultLibraries
      :: FilePath  -- ^ Project root.
      -> Bool      -- ^ Use @defaults@ if no @.agda-lib@ file exists for this project?
      -> LibM ([LibName], [FilePath])  -- ^ The returned @LibName@s are all non-empty strings.
    getDefaultLibraries :: FilePath -> Bool -> LibM ([LibName], [FilePath])
    getDefaultLibraries FilePath
    root Bool
    optDefaultLibs = do
      libs <- FilePath -> LibM [AgdaLibFile]
    getAgdaLibFile FilePath
    root
      if null libs
        then (,[]) <$> if optDefaultLibs then mkLibM [] $ (libNameForCurrentDir :) <$> readDefaultsFile else return []
        else return $ libsAndPaths libs
      where
        libsAndPaths :: t AgdaLibFile -> ([LibName], [FilePath])
    libsAndPaths t AgdaLibFile
    ls = ( (AgdaLibFile -> [LibName]) -> t AgdaLibFile -> [LibName]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap AgdaLibFile -> [LibName]
    _libDepends t AgdaLibFile
    ls
                          , (FilePath -> FilePath) -> [FilePath] -> [FilePath]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    nubOn FilePath -> FilePath
    forall a. a -> a
    id ((AgdaLibFile -> [FilePath]) -> t AgdaLibFile -> [FilePath]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap AgdaLibFile -> [FilePath]
    _libIncludes t AgdaLibFile
    ls)
                          )

    -- | Return list of libraries to be used by default.
    --
    --   None if the @defaults@ file does not exist.
    --
    readDefaultsFile :: LibErrorIO [LibName]
    readDefaultsFile :: LibErrorIO [LibName]
    readDefaultsFile = do
        agdaDir <- IO FilePath -> WriterT LibErrWarns (StateT LibState IO) FilePath
    forall a. IO a -> WriterT LibErrWarns (StateT LibState IO) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO IO FilePath
    getAgdaAppDir
        let file = FilePath
    agdaDir FilePath -> FilePath -> FilePath
    </> FilePath
    defaultsFile
        ifNotM (liftIO $ doesFileExist file) (return []) $ {-else-} do
          ls <- liftIO $ map snd . stripCommentLines <$> UTF8.readFile file
          return $ map parseLibName $ concatMap splitCommas ls
      LibErrorIO [LibName]
    -> (IOError -> LibErrorIO [LibName]) -> LibErrorIO [LibName]
    forall e a.
    Exception e =>
    WriterT LibErrWarns (StateT LibState IO) a
    -> (e -> WriterT LibErrWarns (StateT LibState IO) a)
    -> WriterT LibErrWarns (StateT LibState IO) a
    forall (m :: * -> *) e a.
    (CatchIO m, Exception e) =>
    m a -> (e -> m a) -> m a
    `catchIO` \ IOError
    e -> do
        List1 LibError' -> WriterT LibErrWarns (StateT LibState IO) ()
    forall (m :: * -> *).
    MonadWriter LibErrWarns m =>
    List1 LibError' -> m ()
    raiseErrors' [ IOError -> FilePath -> LibError'
    ReadError IOError
    e FilePath
    "Failed to read defaults file." ]
        [LibName] -> LibErrorIO [LibName]
    forall a. a -> WriterT LibErrWarns (StateT LibState IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []

    ------------------------------------------------------------------------
    -- * Reading the installed libraries
    ------------------------------------------------------------------------

    -- | Returns the path of the @libraries@ file which lists the libraries Agda knows about.
    --
    --   Note: file may not exist.
    --
    --   If the user specified an alternative @libraries@ file which does not exist,
    --   an exception is thrown containing the name of this file.
    getLibrariesFile
      :: (MonadIO m, MonadError FilePath m)
      => Maybe FilePath -- ^ Override the default @libraries@ file?
      -> m LibrariesFile
    getLibrariesFile :: forall (m :: * -> *).
    (MonadIO m, MonadError FilePath m) =>
    Maybe FilePath -> m LibrariesFile
    getLibrariesFile (Just FilePath
    overrideLibFile) = do
      -- A user-specified override file must exist.
      m Bool -> m LibrariesFile -> m LibrariesFile -> m LibrariesFile
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (IO Bool -> m Bool
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO Bool -> m Bool) -> IO Bool -> m Bool
    forall a b. (a -> b) -> a -> b
    $ FilePath -> IO Bool
    doesFileExist FilePath
    overrideLibFile)
        {-then-} (LibrariesFile -> m LibrariesFile
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (LibrariesFile -> m LibrariesFile)
    -> LibrariesFile -> m LibrariesFile
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Bool -> LibrariesFile
    LibrariesFile FilePath
    overrideLibFile Bool
    True)
        {-else-} (FilePath -> m LibrariesFile
    forall a. FilePath -> m a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError FilePath
    overrideLibFile)
    getLibrariesFile Maybe FilePath
    Nothing = do
      agdaDir <- IO FilePath -> m FilePath
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO FilePath -> m FilePath) -> IO FilePath -> m FilePath
    forall a b. (a -> b) -> a -> b
    $ IO FilePath
    getAgdaAppDir
      let defaults = (FilePath -> FilePath) -> NonEmpty FilePath -> NonEmpty FilePath
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    List1.map (FilePath
    agdaDir FilePath -> FilePath -> FilePath
    </>) NonEmpty FilePath
    defaultLibraryFiles -- NB: very short list
      files <- liftIO $ filterM doesFileExist (List1.toList defaults)
      case files of
        FilePath
    file : [FilePath]
    _ -> LibrariesFile -> m LibrariesFile
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (LibrariesFile -> m LibrariesFile)
    -> LibrariesFile -> m LibrariesFile
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Bool -> LibrariesFile
    LibrariesFile FilePath
    file Bool
    True
        []       -> LibrariesFile -> m LibrariesFile
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (LibrariesFile -> m LibrariesFile)
    -> LibrariesFile -> m LibrariesFile
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Bool -> LibrariesFile
    LibrariesFile (NonEmpty FilePath -> FilePath
    forall a. NonEmpty a -> a
    List1.last NonEmpty FilePath
    defaults) Bool
    False -- doesn't exist, but that's ok

    -- | Parse the descriptions of the libraries Agda knows about.
    --
    --   Returns none if there is no @libraries@ file.
    --
    getInstalledLibraries
      :: Maybe FilePath     -- ^ Override the default @libraries@ file?
      -> LibM [AgdaLibFile] -- ^ Content of library files.  (Might have empty @LibName@s.)
    getInstalledLibraries :: Maybe FilePath -> LibM [AgdaLibFile]
    getInstalledLibraries Maybe FilePath
    overrideLibFile = [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
    $ do
        filem <- IO (Either FilePath LibrariesFile)
    -> WriterT
         LibErrWarns (StateT LibState IO) (Either FilePath LibrariesFile)
    forall a. IO a -> WriterT LibErrWarns (StateT LibState IO) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (Either FilePath LibrariesFile)
     -> WriterT
          LibErrWarns (StateT LibState IO) (Either FilePath LibrariesFile))
    -> IO (Either FilePath LibrariesFile)
    -> WriterT
         LibErrWarns (StateT LibState IO) (Either FilePath LibrariesFile)
    forall a b. (a -> b) -> a -> b
    $ ExceptT FilePath IO LibrariesFile
    -> IO (Either FilePath LibrariesFile)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (ExceptT FilePath IO LibrariesFile
     -> IO (Either FilePath LibrariesFile))
    -> ExceptT FilePath IO LibrariesFile
    -> IO (Either FilePath LibrariesFile)
    forall a b. (a -> b) -> a -> b
    $ Maybe FilePath -> ExceptT FilePath IO LibrariesFile
    forall (m :: * -> *).
    (MonadIO m, MonadError FilePath m) =>
    Maybe FilePath -> m LibrariesFile
    getLibrariesFile Maybe FilePath
    overrideLibFile
        userlibs <- case filem of
          Left FilePath
    theOverrideLibFile -> do
            List1 LibError' -> WriterT LibErrWarns (StateT LibState IO) ()
    forall (m :: * -> *).
    MonadWriter LibErrWarns m =>
    List1 LibError' -> m ()
    raiseErrors' [ FilePath -> LibError'
    LibrariesFileNotFound FilePath
    theOverrideLibFile ]
            [AgdaLibFile] -> LibErrorIO [AgdaLibFile]
    forall a. a -> WriterT LibErrWarns (StateT LibState IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
          Right LibrariesFile
    file -> do
            if Bool -> Bool
    not (LibrariesFile -> Bool
    lfExists LibrariesFile
    file) then [AgdaLibFile] -> LibErrorIO [AgdaLibFile]
    forall a. a -> WriterT LibErrWarns (StateT LibState IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [] else do
              ls    <- IO [(LineNumber, FilePath)]
    -> WriterT
         LibErrWarns (StateT LibState IO) [(LineNumber, FilePath)]
    forall a. IO a -> WriterT LibErrWarns (StateT LibState IO) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO [(LineNumber, FilePath)]
     -> WriterT
          LibErrWarns (StateT LibState IO) [(LineNumber, FilePath)])
    -> IO [(LineNumber, FilePath)]
    -> WriterT
         LibErrWarns (StateT LibState IO) [(LineNumber, FilePath)]
    forall a b. (a -> b) -> a -> b
    $ FilePath -> [(LineNumber, FilePath)]
    stripCommentLines (FilePath -> [(LineNumber, FilePath)])
    -> IO FilePath -> IO [(LineNumber, FilePath)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> FilePath -> IO FilePath
    UTF8.readFile (LibrariesFile -> FilePath
    lfPath LibrariesFile
    file)
              files <- liftIO $ sequence [ (i, ) <$> expandEnvironmentVariables s | (i, s) <- ls ]
              parseLibFiles (Just file) $ nubOn snd files
        systemlibs <- ifNotM (liftIO $ doesDirectoryExist systemLibDir) (return []) $ do
          files <- liftIO $ filter isLibFile <$> listDirectory systemLibDir
          parseLibFiles Nothing $ zip [1..] $ map (systemLibDir </>) files
        return $ userlibs ++ systemlibs
      LibErrorIO [AgdaLibFile]
    -> (IOError -> LibErrorIO [AgdaLibFile])
    -> LibErrorIO [AgdaLibFile]
    forall e a.
    Exception e =>
    WriterT LibErrWarns (StateT LibState IO) a
    -> (e -> WriterT LibErrWarns (StateT LibState IO) a)
    -> WriterT LibErrWarns (StateT LibState IO) a
    forall (m :: * -> *) e a.
    (CatchIO m, Exception e) =>
    m a -> (e -> m a) -> m a
    `catchIO` \ IOError
    e -> do
        List1 LibError' -> WriterT LibErrWarns (StateT LibState IO) ()
    forall (m :: * -> *).
    MonadWriter LibErrWarns m =>
    List1 LibError' -> m ()
    raiseErrors' [ IOError -> FilePath -> LibError'
    ReadError IOError
    e FilePath
    "Failed to read installed libraries." ]
        [AgdaLibFile] -> LibErrorIO [AgdaLibFile]
    forall a. a -> WriterT LibErrWarns (StateT LibState IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
      where systemLibDir :: FilePath
    systemLibDir = FilePath
    "/var/lib/agda"
            isLibFile :: FilePath -> Bool
    isLibFile FilePath
    fn = FilePath -> FilePath
    takeExtension FilePath
    fn FilePath -> FilePath -> Bool
    forall a. Eq a => a -> a -> Bool
    == FilePath
    ".agda-lib" Bool -> Bool -> Bool
    && Bool -> Bool
    not (FilePath
    "." FilePath -> FilePath -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `List.isPrefixOf` FilePath
    fn)

    -- | Parse the given library files.
    --
    parseLibFiles
      :: Maybe LibrariesFile       -- ^ Name of @libraries@ file for error reporting.
      -> [(LineNumber, FilePath)]  -- ^ Library files paired with their line number in @libraries@.
      -> LibErrorIO [AgdaLibFile]  -- ^ Content of library files.  (Might have empty @LibName@s.)
    parseLibFiles :: Maybe LibrariesFile
    -> [(LineNumber, FilePath)] -> LibErrorIO [AgdaLibFile]
    parseLibFiles Maybe LibrariesFile
    mlibFile [(LineNumber, FilePath)]
    files = do

      anns <- [(LineNumber, FilePath)]
    -> ((LineNumber, FilePath)
        -> WriterT
             LibErrWarns
             (StateT LibState IO)
             (Either (Maybe LibPositionInfo, LibParseError) AgdaLibFile,
              [LibWarning]))
    -> WriterT
         LibErrWarns
         (StateT LibState IO)
         [(Either (Maybe LibPositionInfo, LibParseError) AgdaLibFile,
           [LibWarning])]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [(LineNumber, FilePath)]
    files (((LineNumber, FilePath)
      -> WriterT
           LibErrWarns
           (StateT LibState IO)
           (Either (Maybe LibPositionInfo, LibParseError) AgdaLibFile,
            [LibWarning]))
     -> WriterT
          LibErrWarns
          (StateT LibState IO)
          [(Either (Maybe LibPositionInfo, LibParseError) AgdaLibFile,
            [LibWarning])])
    -> ((LineNumber, FilePath)
        -> WriterT
             LibErrWarns
             (StateT LibState IO)
             (Either (Maybe LibPositionInfo, LibParseError) AgdaLibFile,
              [LibWarning]))
    -> WriterT
         LibErrWarns
         (StateT LibState IO)
         [(Either (Maybe LibPositionInfo, LibParseError) AgdaLibFile,
           [LibWarning])]
    forall a b. (a -> b) -> a -> b
    $ \(LineNumber
    ln, FilePath
    file) -> do
        FilePath
    -> WriterT LibErrWarns (StateT LibState IO) (Maybe AgdaLibFile)
    forall (m :: * -> *).
    (MonadState LibState m, MonadIO m) =>
    FilePath -> m (Maybe AgdaLibFile)
    getCachedAgdaLibFile FilePath
    file WriterT LibErrWarns (StateT LibState IO) (Maybe AgdaLibFile)
    -> (Maybe AgdaLibFile
        -> WriterT
             LibErrWarns
             (StateT LibState IO)
             (Either (Maybe LibPositionInfo, LibParseError) AgdaLibFile,
              [LibWarning]))
    -> WriterT
         LibErrWarns
         (StateT LibState IO)
         (Either (Maybe LibPositionInfo, LibParseError) AgdaLibFile,
          [LibWarning])
    forall a b.
    WriterT LibErrWarns (StateT LibState IO) a
    -> (a -> WriterT LibErrWarns (StateT LibState IO) b)
    -> WriterT LibErrWarns (StateT LibState IO) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Just AgdaLibFile
    lib -> (Either (Maybe LibPositionInfo, LibParseError) AgdaLibFile,
     [LibWarning])
    -> WriterT
         LibErrWarns
         (StateT LibState IO)
         (Either (Maybe LibPositionInfo, LibParseError) AgdaLibFile,
          [LibWarning])
    forall a. a -> WriterT LibErrWarns (StateT LibState IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (AgdaLibFile
    -> Either (Maybe LibPositionInfo, LibParseError) AgdaLibFile
    forall a b. b -> Either a b
    Right AgdaLibFile
    lib, [])
          Maybe AgdaLibFile
    Nothing  -> do
            (e, ws) <- IO (Either LibParseError AgdaLibFile, [LibWarning'])
    -> WriterT
         LibErrWarns
         (StateT LibState IO)
         (Either LibParseError AgdaLibFile, [LibWarning'])
    forall a. IO a -> WriterT LibErrWarns (StateT LibState IO) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (Either LibParseError AgdaLibFile, [LibWarning'])
     -> WriterT
          LibErrWarns
          (StateT LibState IO)
          (Either LibParseError AgdaLibFile, [LibWarning']))
    -> IO (Either LibParseError AgdaLibFile, [LibWarning'])
    -> WriterT
         LibErrWarns
         (StateT LibState IO)
         (Either LibParseError AgdaLibFile, [LibWarning'])
    forall a b. (a -> b) -> a -> b
    $ P AgdaLibFile -> (Either LibParseError AgdaLibFile, [LibWarning'])
    forall a. P a -> (Either LibParseError a, [LibWarning'])
    runP (P AgdaLibFile
     -> (Either LibParseError AgdaLibFile, [LibWarning']))
    -> IO (P AgdaLibFile)
    -> IO (Either LibParseError AgdaLibFile, [LibWarning'])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> FilePath -> IO (P AgdaLibFile)
    parseLibFile FilePath
    file
            let pos = Maybe FilePath -> LineNumber -> FilePath -> LibPositionInfo
    LibPositionInfo (LibrariesFile -> FilePath
    lfPath (LibrariesFile -> FilePath)
    -> Maybe LibrariesFile -> Maybe FilePath
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe LibrariesFile
    mlibFile) LineNumber
    ln FilePath
    file
                ws' = (LibWarning' -> LibWarning) -> [LibWarning'] -> [LibWarning]
    forall a b. (a -> b) -> [a] -> [b]
    map (Maybe LibPositionInfo -> LibWarning' -> LibWarning
    LibWarning (LibPositionInfo -> Maybe LibPositionInfo
    forall a. a -> Maybe a
    Just LibPositionInfo
    pos)) [LibWarning']
    ws
            case e of
              Left LibParseError
    err -> do
                (Either (Maybe LibPositionInfo, LibParseError) AgdaLibFile,
     [LibWarning])
    -> WriterT
         LibErrWarns
         (StateT LibState IO)
         (Either (Maybe LibPositionInfo, LibParseError) AgdaLibFile,
          [LibWarning])
    forall a. a -> WriterT LibErrWarns (StateT LibState IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Maybe LibPositionInfo, LibParseError)
    -> Either (Maybe LibPositionInfo, LibParseError) AgdaLibFile
    forall a b. a -> Either a b
    Left (LibPositionInfo -> Maybe LibPositionInfo
    forall a. a -> Maybe a
    Just LibPositionInfo
    pos, LibParseError
    err), [LibWarning]
    ws')
              Right AgdaLibFile
    lib -> do
                FilePath
    -> AgdaLibFile -> WriterT LibErrWarns (StateT LibState IO) ()
    forall (m :: * -> *).
    (MonadState LibState m, MonadIO m) =>
    FilePath -> AgdaLibFile -> m ()
    storeCachedAgdaLibFile FilePath
    file AgdaLibFile
    lib
                (Either (Maybe LibPositionInfo, LibParseError) AgdaLibFile,
     [LibWarning])
    -> WriterT
         LibErrWarns
         (StateT LibState IO)
         (Either (Maybe LibPositionInfo, LibParseError) AgdaLibFile,
          [LibWarning])
    forall a. a -> WriterT LibErrWarns (StateT LibState IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (AgdaLibFile
    -> Either (Maybe LibPositionInfo, LibParseError) AgdaLibFile
    forall a b. b -> Either a b
    Right AgdaLibFile
    lib, [LibWarning]
    ws')

      let (xs, warns) = unzip anns
          (errs, als) = partitionEithers xs

      List1.unlessNull (concat warns) warnings
      List1.unlessNull errs $ \ List1 (Maybe LibPositionInfo, LibParseError)
    errs1 ->
        List1 LibError -> WriterT LibErrWarns (StateT LibState IO) ()
    forall (m :: * -> *).
    MonadWriter LibErrWarns m =>
    List1 LibError -> m ()
    raiseErrors (List1 LibError -> WriterT LibErrWarns (StateT LibState IO) ())
    -> List1 LibError -> WriterT LibErrWarns (StateT LibState IO) ()
    forall a b. (a -> b) -> a -> b
    $ ((Maybe LibPositionInfo, LibParseError) -> LibError)
    -> List1 (Maybe LibPositionInfo, LibParseError) -> List1 LibError
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\ (Maybe LibPositionInfo
    mc, LibParseError
    err) -> Maybe LibPositionInfo -> LibError' -> LibError
    LibError Maybe LibPositionInfo
    mc (LibError' -> LibError) -> LibError' -> LibError
    forall a b. (a -> b) -> a -> b
    $ LibParseError -> LibError'
    LibParseError LibParseError
    err) List1 (Maybe LibPositionInfo, LibParseError)
    errs1

      return $ nubOn _libFile als

    -- | Remove trailing white space and line comments.
    --
    stripCommentLines :: String -> [(LineNumber, String)]
    stripCommentLines :: FilePath -> [(LineNumber, FilePath)]
    stripCommentLines = ((LineNumber, FilePath) -> [(LineNumber, FilePath)])
    -> [(LineNumber, FilePath)] -> [(LineNumber, FilePath)]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (LineNumber, FilePath) -> [(LineNumber, FilePath)]
    forall {a}. (a, FilePath) -> [(a, FilePath)]
    strip ([(LineNumber, FilePath)] -> [(LineNumber, FilePath)])
    -> (FilePath -> [(LineNumber, FilePath)])
    -> FilePath
    -> [(LineNumber, FilePath)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [LineNumber] -> [FilePath] -> [(LineNumber, FilePath)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [LineNumber
    Item [LineNumber]
    1..] ([FilePath] -> [(LineNumber, FilePath)])
    -> (FilePath -> [FilePath]) -> FilePath -> [(LineNumber, FilePath)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FilePath -> [FilePath]
    lines
      where
        strip :: (a, FilePath) -> [(a, FilePath)]
    strip (a
    i, FilePath
    s) = [ (a
    i, FilePath
    s') | Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null FilePath
    s' ]
          where s' :: FilePath
    s' = FilePath -> FilePath
    trimLineComment FilePath
    s

    -- | Returns the path of the @executables@ file which lists the trusted executables Agda knows about.
    --
    --   Note: file may not exist.
    --
    getExecutablesFile
      :: IO ExecutablesFile
    getExecutablesFile :: IO ExecutablesFile
    getExecutablesFile = do
      agdaDir <- IO FilePath
    getAgdaAppDir
      let defaults = (FilePath -> FilePath) -> NonEmpty FilePath -> NonEmpty FilePath
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    List1.map (FilePath
    agdaDir FilePath -> FilePath -> FilePath
    </>) NonEmpty FilePath
    defaultExecutableFiles  -- NB: very short list
      files <- filterM doesFileExist (List1.toList defaults)
      case files of
        FilePath
    file : [FilePath]
    _ -> ExecutablesFile -> IO ExecutablesFile
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ExecutablesFile -> IO ExecutablesFile)
    -> ExecutablesFile -> IO ExecutablesFile
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Bool -> ExecutablesFile
    ExecutablesFile FilePath
    file Bool
    True
        []       -> ExecutablesFile -> IO ExecutablesFile
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ExecutablesFile -> IO ExecutablesFile)
    -> ExecutablesFile -> IO ExecutablesFile
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Bool -> ExecutablesFile
    ExecutablesFile (NonEmpty FilePath -> FilePath
    forall a. NonEmpty a -> a
    List1.last NonEmpty FilePath
    defaults) Bool
    False -- doesn't exist, but that's ok

    -- | Return the trusted executables Agda knows about.
    --
    --   Returns none if there is no @executables@ file.
    --
    getTrustedExecutables
      :: LibM (Map ExeName FilePath)  -- ^ Content of @executables@ files.
    getTrustedExecutables :: LibM (Map Text FilePath)
    getTrustedExecutables = [AgdaLibFile]
    -> LibErrorIO (Map Text FilePath) -> LibM (Map Text FilePath)
    forall a. [AgdaLibFile] -> LibErrorIO a -> LibM a
    mkLibM [] (LibErrorIO (Map Text FilePath) -> LibM (Map Text FilePath))
    -> LibErrorIO (Map Text FilePath) -> LibM (Map Text FilePath)
    forall a b. (a -> b) -> a -> b
    $ do
        file <- IO ExecutablesFile
    -> WriterT LibErrWarns (StateT LibState IO) ExecutablesFile
    forall a. IO a -> WriterT LibErrWarns (StateT LibState IO) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO IO ExecutablesFile
    getExecutablesFile
        if not (efExists file) then return Map.empty else do
          es    <- liftIO $ stripCommentLines <$> UTF8.readFile (efPath file)
          lines <- liftIO $ mapM (mapSndM expandEnvironmentVariables) es
          parseExecutablesFile file lines
      LibErrorIO (Map Text FilePath)
    -> (IOError -> LibErrorIO (Map Text FilePath))
    -> LibErrorIO (Map Text FilePath)
    forall e a.
    Exception e =>
    WriterT LibErrWarns (StateT LibState IO) a
    -> (e -> WriterT LibErrWarns (StateT LibState IO) a)
    -> WriterT LibErrWarns (StateT LibState IO) a
    forall (m :: * -> *) e a.
    (CatchIO m, Exception e) =>
    m a -> (e -> m a) -> m a
    `catchIO` \ IOError
    e -> do
        List1 LibError' -> WriterT LibErrWarns (StateT LibState IO) ()
    forall (m :: * -> *).
    MonadWriter LibErrWarns m =>
    List1 LibError' -> m ()
    raiseErrors' [ IOError -> FilePath -> LibError'
    ReadError IOError
    e FilePath
    "Failed to read trusted executables." ]
        Map Text FilePath -> LibErrorIO (Map Text FilePath)
    forall a. a -> WriterT LibErrWarns (StateT LibState IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Map Text FilePath
    forall k a. Map k a
    Map.empty

    -- | Parse the @executables@ file.
    --
    parseExecutablesFile
      :: ExecutablesFile
      -> [(LineNumber, FilePath)]
      -> LibErrorIO (Map ExeName FilePath)
    parseExecutablesFile :: ExecutablesFile
    -> [(LineNumber, FilePath)] -> LibErrorIO (Map Text FilePath)
    parseExecutablesFile ExecutablesFile
    ef [(LineNumber, FilePath)]
    files = do
      executables <- [(LineNumber, FilePath)]
    -> ((LineNumber, FilePath)
        -> WriterT
             LibErrWarns (StateT LibState IO) (Text, (LineNumber, FilePath)))
    -> WriterT
         LibErrWarns (StateT LibState IO) [(Text, (LineNumber, FilePath))]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [(LineNumber, FilePath)]
    files (((LineNumber, FilePath)
      -> WriterT
           LibErrWarns (StateT LibState IO) (Text, (LineNumber, FilePath)))
     -> WriterT
          LibErrWarns (StateT LibState IO) [(Text, (LineNumber, FilePath))])
    -> ((LineNumber, FilePath)
        -> WriterT
             LibErrWarns (StateT LibState IO) (Text, (LineNumber, FilePath)))
    -> WriterT
         LibErrWarns (StateT LibState IO) [(Text, (LineNumber, FilePath))]
    forall a b. (a -> b) -> a -> b
    $ \(LineNumber
    ln, FilePath
    fp) -> do
        -- Compute canonical executable name and absolute filepath.
        let strExeName :: FilePath
    strExeName  = FilePath -> FilePath
    takeFileName FilePath
    fp
        let strExeName' :: FilePath
    strExeName' = FilePath -> Maybe FilePath -> FilePath
    forall a. a -> Maybe a -> a
    fromMaybe FilePath
    strExeName (Maybe FilePath -> FilePath) -> Maybe FilePath -> FilePath
    forall a b. (a -> b) -> a -> b
    $ FilePath -> FilePath -> Maybe FilePath
    stripExtension FilePath
    exeExtension FilePath
    strExeName
        let txtExeName :: Text
    txtExeName  = FilePath -> Text
    T.pack FilePath
    strExeName'
        exePath <- IO FilePath -> WriterT LibErrWarns (StateT LibState IO) FilePath
    forall a. IO a -> WriterT LibErrWarns (StateT LibState IO) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO FilePath -> WriterT LibErrWarns (StateT LibState IO) FilePath)
    -> IO FilePath -> WriterT LibErrWarns (StateT LibState IO) FilePath
    forall a b. (a -> b) -> a -> b
    $ FilePath -> IO FilePath
    makeAbsolute FilePath
    fp
        return (txtExeName, (ln, exePath))

      -- Create a map from executable names to their location(s).
      let exeMap1 :: Map ExeName (List1 (LineNumber, FilePath))
          exeMap1 = (List1 (LineNumber, FilePath)
     -> List1 (LineNumber, FilePath) -> List1 (LineNumber, FilePath))
    -> [(Text, List1 (LineNumber, FilePath))]
    -> Map Text (List1 (LineNumber, FilePath))
    forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
    Map.fromListWith List1 (LineNumber, FilePath)
    -> List1 (LineNumber, FilePath) -> List1 (LineNumber, FilePath)
    forall a. Semigroup a => a -> a -> a
    (<>) ([(Text, List1 (LineNumber, FilePath))]
     -> Map Text (List1 (LineNumber, FilePath)))
    -> [(Text, List1 (LineNumber, FilePath))]
    -> Map Text (List1 (LineNumber, FilePath))
    forall a b. (a -> b) -> a -> b
    $ ((Text, (LineNumber, FilePath))
     -> (Text, List1 (LineNumber, FilePath)))
    -> [(Text, (LineNumber, FilePath))]
    -> [(Text, List1 (LineNumber, FilePath))]
    forall a b. (a -> b) -> [a] -> [b]
    map (((LineNumber, FilePath) -> List1 (LineNumber, FilePath))
    -> (Text, (LineNumber, FilePath))
    -> (Text, List1 (LineNumber, FilePath))
    forall b c a. (b -> c) -> (a, b) -> (a, c)
    forall (p :: * -> * -> *) b c a.
    Bifunctor p =>
    (b -> c) -> p a b -> p a c
    second (LineNumber, FilePath) -> List1 (LineNumber, FilePath)
    forall el coll. Singleton el coll => el -> coll
    singleton) ([(Text, (LineNumber, FilePath))]
     -> [(Text, List1 (LineNumber, FilePath))])
    -> [(Text, (LineNumber, FilePath))]
    -> [(Text, List1 (LineNumber, FilePath))]
    forall a b. (a -> b) -> a -> b
    $ [(Text, (LineNumber, FilePath))]
    -> [(Text, (LineNumber, FilePath))]
    forall a. [a] -> [a]
    reverse [(Text, (LineNumber, FilePath))]
    executables

      -- Separate non-ambiguous from ambiguous mappings.
      let (exeMap, duplicates) = Map.mapEither List2.fromList1Either exeMap1

      -- Report ambiguous mappings with line numbers.
      List1.unlessNull (Map.toList duplicates) $ \ List1 (Text, List2 (LineNumber, FilePath))
    duplicates1 ->
        List1 LibError' -> WriterT LibErrWarns (StateT LibState IO) ()
    forall (m :: * -> *).
    MonadWriter LibErrWarns m =>
    List1 LibError' -> m ()
    raiseErrors' (List1 LibError' -> WriterT LibErrWarns (StateT LibState IO) ())
    -> List1 LibError' -> WriterT LibErrWarns (StateT LibState IO) ()
    forall a b. (a -> b) -> a -> b
    $ ((Text, List2 (LineNumber, FilePath)) -> LibError')
    -> List1 (Text, List2 (LineNumber, FilePath)) -> List1 LibError'
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Text -> List2 (LineNumber, FilePath) -> LibError')
    -> (Text, List2 (LineNumber, FilePath)) -> LibError'
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry ((Text -> List2 (LineNumber, FilePath) -> LibError')
     -> (Text, List2 (LineNumber, FilePath)) -> LibError')
    -> (Text -> List2 (LineNumber, FilePath) -> LibError')
    -> (Text, List2 (LineNumber, FilePath))
    -> LibError'
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Text -> List2 (LineNumber, FilePath) -> LibError'
    DuplicateExecutable (FilePath -> Text -> List2 (LineNumber, FilePath) -> LibError')
    -> FilePath -> Text -> List2 (LineNumber, FilePath) -> LibError'
    forall a b. (a -> b) -> a -> b
    $ ExecutablesFile -> FilePath
    efPath ExecutablesFile
    ef) List1 (Text, List2 (LineNumber, FilePath))
    duplicates1

      -- Return non-ambiguous mappings without line numbers.
      return $ fmap snd exeMap

    ------------------------------------------------------------------------
    -- * Resolving library names to include pathes
    ------------------------------------------------------------------------

    -- | Get all include pathes for a list of libraries to use.
    libraryIncludePaths
      :: Maybe FilePath  -- ^ @libraries@ file (error reporting only).
      -> [AgdaLibFile]   -- ^ Libraries Agda knows about.
      -> [LibName]       -- ^ (Non-empty) library names to be resolved to (lists of) pathes.
      -> LibM [FilePath] -- ^ Resolved pathes (no duplicates).  Contains "." if @[LibName]@ does.
    libraryIncludePaths :: Maybe FilePath
    -> [AgdaLibFile]
    -> [LibName]
    -> ExceptT
         LibErrors (WriterT [LibWarning] (StateT LibState IO)) [FilePath]
    libraryIncludePaths Maybe FilePath
    overrideLibFile [AgdaLibFile]
    libs [LibName]
    xs0 = [AgdaLibFile]
    -> WriterT LibErrWarns (StateT LibState IO) [FilePath]
    -> ExceptT
         LibErrors (WriterT [LibWarning] (StateT LibState IO)) [FilePath]
    forall a. [AgdaLibFile] -> LibErrorIO a -> LibM a
    mkLibM [AgdaLibFile]
    libs (WriterT LibErrWarns (StateT LibState IO) [FilePath]
     -> ExceptT
          LibErrors (WriterT [LibWarning] (StateT LibState IO)) [FilePath])
    -> WriterT LibErrWarns (StateT LibState IO) [FilePath]
    -> ExceptT
         LibErrors (WriterT [LibWarning] (StateT LibState IO)) [FilePath]
    forall a b. (a -> b) -> a -> b
    $ do
        efile <- IO (Either FilePath LibrariesFile)
    -> WriterT
         LibErrWarns (StateT LibState IO) (Either FilePath LibrariesFile)
    forall a. IO a -> WriterT LibErrWarns (StateT LibState IO) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (Either FilePath LibrariesFile)
     -> WriterT
          LibErrWarns (StateT LibState IO) (Either FilePath LibrariesFile))
    -> IO (Either FilePath LibrariesFile)
    -> WriterT
         LibErrWarns (StateT LibState IO) (Either FilePath LibrariesFile)
    forall a b. (a -> b) -> a -> b
    $ ExceptT FilePath IO LibrariesFile
    -> IO (Either FilePath LibrariesFile)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (ExceptT FilePath IO LibrariesFile
     -> IO (Either FilePath LibrariesFile))
    -> ExceptT FilePath IO LibrariesFile
    -> IO (Either FilePath LibrariesFile)
    forall a b. (a -> b) -> a -> b
    $ Maybe FilePath -> ExceptT FilePath IO LibrariesFile
    forall (m :: * -> *).
    (MonadIO m, MonadError FilePath m) =>
    Maybe FilePath -> m LibrariesFile
    getLibrariesFile Maybe FilePath
    overrideLibFile
        case efile of
          Left FilePath
    theOverrideLibFile -> do
            List1 LibError' -> WriterT LibErrWarns (StateT LibState IO) ()
    forall (m :: * -> *).
    MonadWriter LibErrWarns m =>
    List1 LibError' -> m ()
    raiseErrors' [ FilePath -> LibError'
    LibrariesFileNotFound FilePath
    theOverrideLibFile ]
            [FilePath] -> WriterT LibErrWarns (StateT LibState IO) [FilePath]
    forall a. a -> WriterT LibErrWarns (StateT LibState IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
          Right LibrariesFile
    file -> Writer LibErrWarns [FilePath]
    -> WriterT LibErrWarns (StateT LibState IO) [FilePath]
    forall w (m :: * -> *) a.
    (Monoid w, Monad m) =>
    Writer w a -> WriterT w m a
    embedWriter (Writer LibErrWarns [FilePath]
     -> WriterT LibErrWarns (StateT LibState IO) [FilePath])
    -> Writer LibErrWarns [FilePath]
    -> WriterT LibErrWarns (StateT LibState IO) [FilePath]
    forall a b. (a -> b) -> a -> b
    $ ([FilePath]
    dot [FilePath] -> [FilePath] -> [FilePath]
    forall a. [a] -> [a] -> [a]
    ++) ([FilePath] -> [FilePath])
    -> ([AgdaLibFile] -> [FilePath]) -> [AgdaLibFile] -> [FilePath]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [AgdaLibFile] -> [FilePath]
    incs ([AgdaLibFile] -> [FilePath])
    -> WriterT LibErrWarns Identity [AgdaLibFile]
    -> Writer LibErrWarns [FilePath]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> LibrariesFile
    -> [LibName]
    -> [LibName]
    -> WriterT LibErrWarns Identity [AgdaLibFile]
    find LibrariesFile
    file [] [LibName]
    xs
      where
        ([LibName]
    dots, [LibName]
    xs) = (LibName -> Bool) -> [LibName] -> ([LibName], [LibName])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    List.partition (LibName -> LibName -> Bool
    forall a. Eq a => a -> a -> Bool
    == LibName
    libNameForCurrentDir) [LibName]
    xs0
        incs :: [AgdaLibFile] -> [FilePath]
    incs       = (FilePath -> FilePath) -> [FilePath] -> [FilePath]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    nubOn FilePath -> FilePath
    forall a. a -> a
    id ([FilePath] -> [FilePath])
    -> ([AgdaLibFile] -> [FilePath]) -> [AgdaLibFile] -> [FilePath]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (AgdaLibFile -> [FilePath]) -> [AgdaLibFile] -> [FilePath]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap AgdaLibFile -> [FilePath]
    _libIncludes
        dot :: [FilePath]
    dot        = [ FilePath
    "." | Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ [LibName] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [LibName]
    dots ]

        -- Due to library dependencies, the work list may grow temporarily.
        find
          :: LibrariesFile  -- Only for error reporting.
          -> [LibName]      -- Already resolved libraries.
          -> [LibName]      -- Work list: libraries left to be resolved.
          -> Writer LibErrWarns [AgdaLibFile]
        find :: LibrariesFile
    -> [LibName]
    -> [LibName]
    -> WriterT LibErrWarns Identity [AgdaLibFile]
    find LibrariesFile
    _ [LibName]
    _ [] = [AgdaLibFile] -> WriterT LibErrWarns Identity [AgdaLibFile]
    forall a. a -> WriterT LibErrWarns Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure []
        find LibrariesFile
    file [LibName]
    visited (LibName
    x : [LibName]
    xs)
          | LibName
    x LibName -> [LibName] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [LibName]
    visited = LibrariesFile
    -> [LibName]
    -> [LibName]
    -> WriterT LibErrWarns Identity [AgdaLibFile]
    find LibrariesFile
    file [LibName]
    visited [LibName]
    xs
          | Bool
    otherwise = do
              -- May or may not find the library
              ml <- case LibName -> [AgdaLibFile] -> [AgdaLibFile]
    findLib LibName
    x [AgdaLibFile]
    libs of
                [Item [AgdaLibFile]
    l] -> Maybe AgdaLibFile
    -> WriterT LibErrWarns Identity (Maybe AgdaLibFile)
    forall a. a -> WriterT LibErrWarns Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (AgdaLibFile -> Maybe AgdaLibFile
    forall a. a -> Maybe a
    Just Item [AgdaLibFile]
    AgdaLibFile
    l)
                []  -> Maybe AgdaLibFile
    forall a. Maybe a
    Nothing Maybe AgdaLibFile
    -> WriterT LibErrWarns Identity ()
    -> WriterT LibErrWarns Identity (Maybe AgdaLibFile)
    forall a b.
    a
    -> WriterT LibErrWarns Identity b -> WriterT LibErrWarns Identity a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ List1 LibError' -> WriterT LibErrWarns Identity ()
    forall (m :: * -> *).
    MonadWriter LibErrWarns m =>
    List1 LibError' -> m ()
    raiseErrors' [LibrariesFile -> LibName -> LibError'
    LibNotFound LibrariesFile
    file LibName
    x]
                AgdaLibFile
    l1 : AgdaLibFile
    l2 : [AgdaLibFile]
    ls  -> Maybe AgdaLibFile
    forall a. Maybe a
    Nothing Maybe AgdaLibFile
    -> WriterT LibErrWarns Identity ()
    -> WriterT LibErrWarns Identity (Maybe AgdaLibFile)
    forall a b.
    a
    -> WriterT LibErrWarns Identity b -> WriterT LibErrWarns Identity a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ List1 LibError' -> WriterT LibErrWarns Identity ()
    forall (m :: * -> *).
    MonadWriter LibErrWarns m =>
    List1 LibError' -> m ()
    raiseErrors' [LibName -> List2 AgdaLibFile -> LibError'
    AmbiguousLib LibName
    x (List2 AgdaLibFile -> LibError') -> List2 AgdaLibFile -> LibError'
    forall a b. (a -> b) -> a -> b
    $ AgdaLibFile -> AgdaLibFile -> [AgdaLibFile] -> List2 AgdaLibFile
    forall a. a -> a -> [a] -> List2 a
    List2 AgdaLibFile
    l1 AgdaLibFile
    l2 [AgdaLibFile]
    ls]
              -- If it is found, add its dependencies to work list
              let xs' = (AgdaLibFile -> [LibName]) -> Maybe AgdaLibFile -> [LibName]
    forall m a. Monoid m => (a -> m) -> Maybe a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap AgdaLibFile -> [LibName]
    _libDepends Maybe AgdaLibFile
    ml [LibName] -> [LibName] -> [LibName]
    forall a. [a] -> [a] -> [a]
    ++ [LibName]
    xs
              mcons ml <$> find file (x : visited) xs'

    -- | @findLib x libs@ retrieves the matches for @x@ from list @libs@.
    --
    --   1. Case @x@ is unversioned:
    --      If @x@ is contained in @libs@, then that match is returned.
    --      Otherwise, the matches with the highest version number are returned.
    --
    --   2. Case @x@ is versioned: the matches with the highest version number are returned.
    --
    --   Examples, see 'findLib''.
    --
    findLib :: LibName -> [AgdaLibFile] -> [AgdaLibFile]
    findLib :: LibName -> [AgdaLibFile] -> [AgdaLibFile]
    findLib = (AgdaLibFile -> LibName)
    -> LibName -> [AgdaLibFile] -> [AgdaLibFile]
    forall a. (a -> LibName) -> LibName -> [a] -> [a]
    findLib' AgdaLibFile -> LibName
    _libName

    -- | Generalized version of 'findLib' for testing.
    --
    --   > findLib' id "a"   [ "a-1", "a-02", "a-2", "b" ] == [ "a-02", "a-2" ]
    --
    --   > findLib' id "a"   [ "a", "a-1", "a-01", "a-2", "b" ] == [ "a" ]
    --   > findLib' id "a-1" [ "a", "a-1", "a-01", "a-2", "b" ] == [ "a-1", "a-01" ]
    --   > findLib' id "a-2" [ "a", "a-1", "a-01", "a-2", "b" ] == [ "a-2" ]
    --   > findLib' id "c"   [ "a", "a-1", "a-01", "a-2", "b" ] == []
    --
    findLib' :: (a -> LibName) -> LibName -> [a] -> [a]
    findLib' :: forall a. (a -> LibName) -> LibName -> [a] -> [a]
    findLib' a -> LibName
    libName LibName
    x [a]
    libs =
      case [a]
    ls of
        -- Take the first and all exact matches (modulo leading zeros in version numbers).
        a
    l : [a]
    ls' -> a
    l a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : (a -> Bool) -> [a] -> [a]
    forall a. (a -> Bool) -> [a] -> [a]
    takeWhile ((LibName -> LibName -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (LibName -> LibName -> Bool) -> (a -> LibName) -> a -> a -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` a -> LibName
    libName) a
    l) [a]
    ls'
        []      -> []
      where
        -- @LibName@s that match @x@, sorted descendingly.
        -- The unversioned LibName, if any, will come first.
        ls :: [a]
    ls = (a -> a -> Ordering) -> [a] -> [a]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    List.sortBy ((LibName -> LibName -> Ordering) -> LibName -> LibName -> Ordering
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip LibName -> LibName -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (LibName -> LibName -> Ordering)
    -> (a -> LibName) -> a -> a -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` a -> LibName
    libName) [ a
    l | a
    l <- [a]
    libs, LibName
    x LibName -> LibName -> Bool
    `hasMatch` a -> LibName
    libName a
    l ]
        -- foo > foo-2.2 > foo-2.0.1 > foo-2 > foo-1.0

    -- | @x `hasMatch` y@ if @x@ and @y@ have the same base and
    --   either @x@ has no version qualifier or the versions also match.
    hasMatch :: LibName -> LibName -> Bool
    hasMatch :: LibName -> LibName -> Bool
    hasMatch (LibName Text
    rx [Integer]
    vx) (LibName Text
    ry [Integer]
    vy) = Text
    rx Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    ry Bool -> Bool -> Bool
    && ([Integer]
    vx [Integer] -> [Integer] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Integer]
    vy Bool -> Bool -> Bool
    || [Integer] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Integer]
    vx)