    -- | 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
      , getAgdaLibFiles'
      , getPrimitiveLibDir
      , LibName
      , AgdaLibFile(..)
      , ExeName
      , LibM
      , mkLibM
      , LibWarning(..)
      , LibPositionInfo(..)
      , libraryWarningName
      , ProjectConfig(..)
      -- * Exported for testing
      , VersionView(..), versionView, unVersionView
      , findLib'
      ) where

    import Control.Arrow          ( first , second )
    import Control.Monad          ( filterM, forM )
    import Control.Monad.Except
    import Control.Monad.State
    import Control.Monad.Writer
    import Control.Monad.IO.Class ( MonadIO(..) )

    import Data.Char
    import Data.Data ( Data )
    import Data.Either
    import Data.Function
    import Data.Map ( Map )
    import qualified Data.Map as Map
    import Data.Maybe ( catMaybes, fromMaybe )
    import qualified Data.List as List
    import qualified Data.Text as T

    import System.Directory
    import System.FilePath
    import System.Environment

    import Agda.Interaction.Library.Base
    import Agda.Interaction.Library.Parse
    import Agda.Interaction.Options.Warnings

    import Agda.Utils.Environment
    import Agda.Utils.FileName
    import Agda.Utils.Functor ( (<&>) )
    import Agda.Utils.IO ( catchIO )
    import qualified Agda.Utils.IO.UTF8 as UTF8
    import Agda.Utils.List
    import Agda.Utils.List1 ( List1 )
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Pretty
    import Agda.Utils.String ( trim )

    import Agda.Version

    -- Paths_Agda.hs is in $(BUILD_DIR)/build/autogen/.
    import Paths_Agda ( getDataFileName )

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

    -- | Library names are structured into the base name and a suffix of version
    --   numbers, e.g. @mylib-1.2.3@.  The version suffix is optional.
    data VersionView = VersionView
      { VersionView -> [Char]
    vvBase    :: LibName
          -- ^ Actual library name.
      , VersionView -> [Integer]
    vvNumbers :: [Integer]
          -- ^ Major version, minor version, subminor version, etc., all non-negative.
          --   Note: a priori, there is no reason why the version numbers should be @Int@s.
      } deriving (VersionView -> VersionView -> Bool
    (VersionView -> VersionView -> Bool)
    -> (VersionView -> VersionView -> Bool) -> Eq VersionView
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: VersionView -> VersionView -> Bool
    $c/= :: VersionView -> VersionView -> Bool
    == :: VersionView -> VersionView -> Bool
    $c== :: VersionView -> VersionView -> Bool
    Eq, LineNumber -> VersionView -> ShowS
    [VersionView] -> ShowS
    VersionView -> [Char]
    (LineNumber -> VersionView -> ShowS)
    -> (VersionView -> [Char])
    -> ([VersionView] -> ShowS)
    -> Show VersionView
    forall a.
    (LineNumber -> a -> ShowS)
    -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    showList :: [VersionView] -> ShowS
    $cshowList :: [VersionView] -> ShowS
    show :: VersionView -> [Char]
    $cshow :: VersionView -> [Char]
    showsPrec :: LineNumber -> VersionView -> ShowS
    $cshowsPrec :: LineNumber -> VersionView -> ShowS
    Show)

    -- | 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
      (a
    x, [Either LibError LibWarning]
    ews) <- WriterT
      [LibWarning] (StateT LibState IO) (a, [Either LibError LibWarning])
    -> ExceptT
         Doc
         (WriterT [LibWarning] (StateT LibState IO))
         (a, [Either LibError LibWarning])
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (WriterT
       [LibWarning] (StateT LibState IO) (a, [Either LibError LibWarning])
     -> ExceptT
          Doc
          (WriterT [LibWarning] (StateT LibState IO))
          (a, [Either LibError LibWarning]))
    -> WriterT
         [LibWarning] (StateT LibState IO) (a, [Either LibError LibWarning])
    -> ExceptT
         Doc
         (WriterT [LibWarning] (StateT LibState IO))
         (a, [Either LibError LibWarning])
    forall a b. (a -> b) -> a -> b
    $ StateT LibState IO (a, [Either LibError LibWarning])
    -> WriterT
         [LibWarning] (StateT LibState IO) (a, [Either LibError LibWarning])
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (StateT LibState IO (a, [Either LibError LibWarning])
     -> WriterT
          [LibWarning]
          (StateT LibState IO)
          (a, [Either LibError LibWarning]))
    -> StateT LibState IO (a, [Either LibError LibWarning])
    -> WriterT
         [LibWarning] (StateT LibState IO) (a, [Either LibError LibWarning])
    forall a b. (a -> b) -> a -> b
    $ LibErrorIO a
    -> StateT LibState IO (a, [Either LibError LibWarning])
    forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
    runWriterT LibErrorIO a
    m
      let ([LibError]
    errs, [LibWarning]
    warns) = [Either LibError LibWarning] -> ([LibError], [LibWarning])
    forall a b. [Either a b] -> ([a], [b])
    partitionEithers [Either LibError LibWarning]
    ews
      [LibWarning]
    -> ExceptT Doc (WriterT [LibWarning] (StateT LibState IO)) ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell [LibWarning]
    warns
      Bool
    -> ExceptT Doc (WriterT [LibWarning] (StateT LibState IO)) ()
    -> ExceptT Doc (WriterT [LibWarning] (StateT LibState IO)) ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([LibError] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [LibError]
    errs) (ExceptT Doc (WriterT [LibWarning] (StateT LibState IO)) ()
     -> ExceptT Doc (WriterT [LibWarning] (StateT LibState IO)) ())
    -> ExceptT Doc (WriterT [LibWarning] (StateT LibState IO)) ()
    -> ExceptT Doc (WriterT [LibWarning] (StateT LibState IO)) ()
    forall a b. (a -> b) -> a -> b
    $ do
        let doc :: Doc
    doc = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (LibError -> Doc) -> [LibError] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ([AgdaLibFile] -> LibError -> Doc
    formatLibError [AgdaLibFile]
    libs) [LibError]
    errs
        Doc -> ExceptT Doc (WriterT [LibWarning] (StateT LibState IO)) ()
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError Doc
    doc
      a -> LibM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    x

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

    -- | Get the path to @~/.agda@ (system-specific).
    --   Can be overwritten by the @AGDA_DIR@ environment variable.
    --
    --   (This is not to be confused with the directory for the data files
    --   that Agda needs (e.g. the primitive modules).)
    --
    getAgdaAppDir :: IO FilePath
    getAgdaAppDir :: IO [Char]
    getAgdaAppDir = do
      -- System-specific command to build the path to ~/.agda (Unix) or %APPDATA%\agda (Win)
      let agdaDir :: IO [Char]
    agdaDir = [Char] -> IO [Char]
    getAppUserDataDirectory [Char]
    "agda"
      -- The default can be overwritten by setting the AGDA_DIR environment variable
      IO (Maybe [Char])
    -> IO [Char] -> ([Char] -> IO [Char]) -> IO [Char]
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM ([Char] -> IO (Maybe [Char])
    lookupEnv [Char]
    "AGDA_DIR") IO [Char]
    agdaDir (([Char] -> IO [Char]) -> IO [Char])
    -> ([Char] -> IO [Char]) -> IO [Char]
    forall a b. (a -> b) -> a -> b
    $ \ [Char]
    dir ->
          IO Bool -> IO [Char] -> IO [Char] -> IO [Char]
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM ([Char] -> IO Bool
    doesDirectoryExist [Char]
    dir) ([Char] -> IO [Char]
    canonicalizePath [Char]
    dir) (IO [Char] -> IO [Char]) -> IO [Char] -> IO [Char]
    forall a b. (a -> b) -> a -> b
    $ do
            [Char]
    d <- IO [Char]
    agdaDir
            [Char] -> IO ()
    putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Warning: Environment variable AGDA_DIR points to non-existing directory " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> [Char]
    show [Char]
    dir [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ", using " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> [Char]
    show [Char]
    d [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " instead."
            [Char] -> IO [Char]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Char]
    d

    -- | Returns the absolute default lib dir. This directory is used to
    -- store the Primitive.agda file.
    getPrimitiveLibDir :: IO FilePath
    getPrimitiveLibDir :: IO [Char]
    getPrimitiveLibDir = do
      [Char]
    libdir <- AbsolutePath -> [Char]
    filePath (AbsolutePath -> [Char]) -> IO AbsolutePath -> IO [Char]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ([Char] -> IO AbsolutePath
    absolute ([Char] -> IO AbsolutePath) -> IO [Char] -> IO AbsolutePath
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [Char] -> IO [Char]
    getDataFileName [Char]
    "lib")
      IO Bool -> IO [Char] -> IO [Char] -> IO [Char]
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM ([Char] -> IO Bool
    doesDirectoryExist [Char]
    libdir)
          ([Char] -> IO [Char]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Char] -> IO [Char]) -> [Char] -> IO [Char]
    forall a b. (a -> b) -> a -> b
    $ [Char]
    libdir [Char] -> ShowS
    </> [Char]
    "prim")
          ([Char] -> IO [Char]
    forall a. HasCallStack => [Char] -> a
    error ([Char] -> IO [Char]) -> [Char] -> IO [Char]
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "The lib directory " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    libdir [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " 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.
    --
    defaultLibraryFiles :: List1 FilePath
    defaultLibraryFiles :: List1 [Char]
    defaultLibraryFiles = [[Char]] -> List1 [Char]
    forall a. [a] -> NonEmpty a
    List1.fromList [[Char]
    "libraries-" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    version, [Char]
    "libraries"]

    -- | The @defaultsFile@ contains a list of library names relevant for each Agda project.
    --
    defaultsFile :: FilePath
    defaultsFile :: [Char]
    defaultsFile = [Char]
    "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.
    --
    defaultExecutableFiles :: List1 FilePath
    defaultExecutableFiles :: List1 [Char]
    defaultExecutableFiles = [[Char]] -> List1 [Char]
    forall a. [a] -> NonEmpty a
    List1.fromList [[Char]
    "executables-" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    version, [Char]
    "executables"]

    ------------------------------------------------------------------------
    -- * 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 (init: the directory Agda was called in)
      -> LibM ProjectConfig                -- ^ Actual root and @.agda-lib@ files for this project
    findProjectConfig :: [Char] -> LibM ProjectConfig
    findProjectConfig [Char]
    root = [AgdaLibFile] -> LibErrorIO ProjectConfig -> LibM ProjectConfig
    forall a. [AgdaLibFile] -> LibErrorIO a -> LibM a
    mkLibM [] (LibErrorIO ProjectConfig -> LibM ProjectConfig)
    -> LibErrorIO ProjectConfig -> LibM ProjectConfig
    forall a b. (a -> b) -> a -> b
    $ [Char] -> LibErrorIO ProjectConfig
    findProjectConfig' [Char]
    root

    findProjectConfig'
      :: FilePath                          -- ^ Candidate (init: the directory Agda was called in)
      -> LibErrorIO ProjectConfig          -- ^ Actual root and @.agda-lib@ files for this project
    findProjectConfig' :: [Char] -> LibErrorIO ProjectConfig
    findProjectConfig' [Char]
    root = do
      [Char]
    -> WriterT
         [Either LibError LibWarning]
         (StateT LibState IO)
         (Maybe ProjectConfig)
    forall (m :: * -> *).
    (MonadState LibState m, MonadIO m) =>
    [Char] -> m (Maybe ProjectConfig)
    getCachedProjectConfig [Char]
    root WriterT
      [Either LibError LibWarning]
      (StateT LibState IO)
      (Maybe ProjectConfig)
    -> (Maybe ProjectConfig -> LibErrorIO ProjectConfig)
    -> LibErrorIO ProjectConfig
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Just ProjectConfig
    conf -> ProjectConfig -> LibErrorIO ProjectConfig
    forall (m :: * -> *) a. Monad m => a -> m a
    return ProjectConfig
    conf
        Maybe ProjectConfig
    Nothing   -> do
          [[Char]]
    libFiles <- IO [[Char]]
    -> WriterT
         [Either LibError LibWarning] (StateT LibState IO) [[Char]]
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO [[Char]]
     -> WriterT
          [Either LibError LibWarning] (StateT LibState IO) [[Char]])
    -> IO [[Char]]
    -> WriterT
         [Either LibError LibWarning] (StateT LibState IO) [[Char]]
    forall a b. (a -> b) -> a -> b
    $ ([Char] -> Bool) -> [[Char]] -> [[Char]]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (([Char] -> [Char] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Char]
    ".agda-lib") ([Char] -> Bool) -> ShowS -> [Char] -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ShowS
    takeExtension) ([[Char]] -> [[Char]]) -> IO [[Char]] -> IO [[Char]]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Char] -> IO [[Char]]
    getDirectoryContents [Char]
    root
          case [[Char]]
    libFiles of
            []     -> IO (Maybe [Char])
    -> WriterT
         [Either LibError LibWarning] (StateT LibState IO) (Maybe [Char])
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO ([Char] -> IO (Maybe [Char])
    upPath [Char]
    root) WriterT
      [Either LibError LibWarning] (StateT LibState IO) (Maybe [Char])
    -> (Maybe [Char] -> LibErrorIO ProjectConfig)
    -> LibErrorIO ProjectConfig
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
              Just [Char]
    up -> do
                ProjectConfig
    conf <- [Char] -> LibErrorIO ProjectConfig
    findProjectConfig' [Char]
    up
                [Char]
    -> ProjectConfig
    -> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
    forall (m :: * -> *).
    (MonadState LibState m, MonadIO m) =>
    [Char] -> ProjectConfig -> m ()
    storeCachedProjectConfig [Char]
    root ProjectConfig
    conf
                ProjectConfig -> LibErrorIO ProjectConfig
    forall (m :: * -> *) a. Monad m => a -> m a
    return ProjectConfig
    conf
              Maybe [Char]
    Nothing -> ProjectConfig -> LibErrorIO ProjectConfig
    forall (m :: * -> *) a. Monad m => a -> m a
    return ProjectConfig
    DefaultProjectConfig
            [[Char]]
    files -> do
              let conf :: ProjectConfig
    conf = [Char] -> [[Char]] -> ProjectConfig
    ProjectConfig [Char]
    root [[Char]]
    files
              [Char]
    -> ProjectConfig
    -> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
    forall (m :: * -> *).
    (MonadState LibState m, MonadIO m) =>
    [Char] -> ProjectConfig -> m ()
    storeCachedProjectConfig [Char]
    root ProjectConfig
    conf
              ProjectConfig -> LibErrorIO ProjectConfig
    forall (m :: * -> *) a. Monad m => a -> m a
    return ProjectConfig
    conf

      where
        -- 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 :: [Char] -> IO (Maybe [Char])
    upPath [Char]
    root = do
          [Char]
    up <- [Char] -> IO [Char]
    canonicalizePath ([Char] -> IO [Char]) -> [Char] -> IO [Char]
    forall a b. (a -> b) -> a -> b
    $ [Char]
    root [Char] -> ShowS
    </> [Char]
    ".."
          if [Char]
    up [Char] -> [Char] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Char]
    root then Maybe [Char] -> IO (Maybe [Char])
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe [Char]
    forall a. Maybe a
    Nothing else Maybe [Char] -> IO (Maybe [Char])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe [Char] -> IO (Maybe [Char]))
    -> Maybe [Char] -> IO (Maybe [Char])
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    up

    -- | Get project root

    findProjectRoot :: FilePath -> LibM (Maybe FilePath)
    findProjectRoot :: [Char] -> LibM (Maybe [Char])
    findProjectRoot [Char]
    root = [Char] -> LibM ProjectConfig
    findProjectConfig [Char]
    root LibM ProjectConfig
    -> (ProjectConfig -> Maybe [Char]) -> LibM (Maybe [Char])
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \case
      ProjectConfig [Char]
    p [[Char]]
    _    -> [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    p
      ProjectConfig
    DefaultProjectConfig -> Maybe [Char]
    forall a. Maybe a
    Nothing

    -- | Get the contents of @.agda-lib@ files in the given project root.
    getAgdaLibFiles' :: FilePath -> LibErrorIO [AgdaLibFile]
    getAgdaLibFiles' :: [Char] -> LibErrorIO [AgdaLibFile]
    getAgdaLibFiles' [Char]
    path = [Char] -> LibErrorIO ProjectConfig
    findProjectConfig' [Char]
    path LibErrorIO ProjectConfig
    -> (ProjectConfig -> LibErrorIO [AgdaLibFile])
    -> LibErrorIO [AgdaLibFile]
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
      ProjectConfig
    DefaultProjectConfig    -> [AgdaLibFile] -> LibErrorIO [AgdaLibFile]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
      ProjectConfig [Char]
    root [[Char]]
    libs -> Maybe LibrariesFile
    -> [(LineNumber, [Char])] -> LibErrorIO [AgdaLibFile]
    parseLibFiles Maybe LibrariesFile
    forall a. Maybe a
    Nothing ([(LineNumber, [Char])] -> LibErrorIO [AgdaLibFile])
    -> [(LineNumber, [Char])] -> LibErrorIO [AgdaLibFile]
    forall a b. (a -> b) -> a -> b
    $ ([Char] -> (LineNumber, [Char]))
    -> [[Char]] -> [(LineNumber, [Char])]
    forall a b. (a -> b) -> [a] -> [b]
    map ((LineNumber
    0,) ([Char] -> (LineNumber, [Char]))
    -> ShowS -> [Char] -> (LineNumber, [Char])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([Char]
    root [Char] -> ShowS
    </>)) [[Char]]
    libs

    -- | 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 :: [Char] -> Bool -> LibM ([[Char]], [[Char]])
    getDefaultLibraries [Char]
    root Bool
    optDefaultLibs = [AgdaLibFile]
    -> LibErrorIO ([[Char]], [[Char]]) -> LibM ([[Char]], [[Char]])
    forall a. [AgdaLibFile] -> LibErrorIO a -> LibM a
    mkLibM [] (LibErrorIO ([[Char]], [[Char]]) -> LibM ([[Char]], [[Char]]))
    -> LibErrorIO ([[Char]], [[Char]]) -> LibM ([[Char]], [[Char]])
    forall a b. (a -> b) -> a -> b
    $ do
      [AgdaLibFile]
    libs <- [Char] -> LibErrorIO [AgdaLibFile]
    getAgdaLibFiles' [Char]
    root
      if [AgdaLibFile] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [AgdaLibFile]
    libs
        then (,[]) ([[Char]] -> ([[Char]], [[Char]]))
    -> WriterT
         [Either LibError LibWarning] (StateT LibState IO) [[Char]]
    -> LibErrorIO ([[Char]], [[Char]])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> if Bool
    optDefaultLibs then ([Char]
    libNameForCurrentDir [Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    :) ([[Char]] -> [[Char]])
    -> WriterT
         [Either LibError LibWarning] (StateT LibState IO) [[Char]]
    -> WriterT
         [Either LibError LibWarning] (StateT LibState IO) [[Char]]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> WriterT [Either LibError LibWarning] (StateT LibState IO) [[Char]]
    readDefaultsFile else [[Char]]
    -> WriterT
         [Either LibError LibWarning] (StateT LibState IO) [[Char]]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        else ([[Char]], [[Char]]) -> LibErrorIO ([[Char]], [[Char]])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (([[Char]], [[Char]]) -> LibErrorIO ([[Char]], [[Char]]))
    -> ([[Char]], [[Char]]) -> LibErrorIO ([[Char]], [[Char]])
    forall a b. (a -> b) -> a -> b
    $ [AgdaLibFile] -> ([[Char]], [[Char]])
    forall {t :: * -> *}.
    Foldable t =>
    t AgdaLibFile -> ([[Char]], [[Char]])
    libsAndPaths [AgdaLibFile]
    libs
      where
        libsAndPaths :: t AgdaLibFile -> ([[Char]], [[Char]])
    libsAndPaths t AgdaLibFile
    ls = ( (AgdaLibFile -> [[Char]]) -> t AgdaLibFile -> [[Char]]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap AgdaLibFile -> [[Char]]
    _libDepends t AgdaLibFile
    ls
                          , ShowS -> [[Char]] -> [[Char]]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    nubOn ShowS
    forall a. a -> a
    id ((AgdaLibFile -> [[Char]]) -> t AgdaLibFile -> [[Char]]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap AgdaLibFile -> [[Char]]
    _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 :: WriterT [Either LibError LibWarning] (StateT LibState IO) [[Char]]
    readDefaultsFile = do
        [Char]
    agdaDir <- IO [Char]
    -> WriterT [Either LibError LibWarning] (StateT LibState IO) [Char]
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO IO [Char]
    getAgdaAppDir
        let file :: [Char]
    file = [Char]
    agdaDir [Char] -> ShowS
    </> [Char]
    defaultsFile
        WriterT [Either LibError LibWarning] (StateT LibState IO) Bool
    -> WriterT
         [Either LibError LibWarning] (StateT LibState IO) [[Char]]
    -> WriterT
         [Either LibError LibWarning] (StateT LibState IO) [[Char]]
    -> WriterT
         [Either LibError LibWarning] (StateT LibState IO) [[Char]]
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifNotM (IO Bool
    -> WriterT [Either LibError LibWarning] (StateT LibState IO) Bool
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO Bool
     -> WriterT [Either LibError LibWarning] (StateT LibState IO) Bool)
    -> IO Bool
    -> WriterT [Either LibError LibWarning] (StateT LibState IO) Bool
    forall a b. (a -> b) -> a -> b
    $ [Char] -> IO Bool
    doesFileExist [Char]
    file) ([[Char]]
    -> WriterT
         [Either LibError LibWarning] (StateT LibState IO) [[Char]]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []) (WriterT [Either LibError LibWarning] (StateT LibState IO) [[Char]]
     -> WriterT
          [Either LibError LibWarning] (StateT LibState IO) [[Char]])
    -> WriterT
         [Either LibError LibWarning] (StateT LibState IO) [[Char]]
    -> WriterT
         [Either LibError LibWarning] (StateT LibState IO) [[Char]]
    forall a b. (a -> b) -> a -> b
    $ {-else-} do
          [[Char]]
    ls <- IO [[Char]]
    -> WriterT
         [Either LibError LibWarning] (StateT LibState IO) [[Char]]
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO [[Char]]
     -> WriterT
          [Either LibError LibWarning] (StateT LibState IO) [[Char]])
    -> IO [[Char]]
    -> WriterT
         [Either LibError LibWarning] (StateT LibState IO) [[Char]]
    forall a b. (a -> b) -> a -> b
    $ ((LineNumber, [Char]) -> [Char])
    -> [(LineNumber, [Char])] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map (LineNumber, [Char]) -> [Char]
    forall a b. (a, b) -> b
    snd ([(LineNumber, [Char])] -> [[Char]])
    -> ([Char] -> [(LineNumber, [Char])]) -> [Char] -> [[Char]]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> [(LineNumber, [Char])]
    stripCommentLines ([Char] -> [[Char]]) -> IO [Char] -> IO [[Char]]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Char] -> IO [Char]
    UTF8.readFile [Char]
    file
          [[Char]]
    -> WriterT
         [Either LibError LibWarning] (StateT LibState IO) [[Char]]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([[Char]]
     -> WriterT
          [Either LibError LibWarning] (StateT LibState IO) [[Char]])
    -> [[Char]]
    -> WriterT
         [Either LibError LibWarning] (StateT LibState IO) [[Char]]
    forall a b. (a -> b) -> a -> b
    $ ([Char] -> [[Char]]) -> [[Char]] -> [[Char]]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap [Char] -> [[Char]]
    splitCommas [[Char]]
    ls
      WriterT [Either LibError LibWarning] (StateT LibState IO) [[Char]]
    -> (IOException
        -> WriterT
             [Either LibError LibWarning] (StateT LibState IO) [[Char]])
    -> WriterT
         [Either LibError LibWarning] (StateT LibState IO) [[Char]]
    forall (m :: * -> *) a.
    CatchIO m =>
    m a -> (IOException -> m a) -> m a
    `catchIO` \ IOException
    e -> do
        [LibError']
    -> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
    forall (m :: * -> *).
    MonadWriter [Either LibError LibWarning] m =>
    [LibError'] -> m ()
    raiseErrors' [ [Char] -> LibError'
    OtherError ([Char] -> LibError') -> [Char] -> LibError'
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines [[Char]
    "Failed to read defaults file.", IOException -> [Char]
    forall a. Show a => a -> [Char]
    show IOException
    e] ]
        [[Char]]
    -> WriterT
         [Either LibError LibWarning] (StateT LibState IO) [[Char]]
    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.
    --
    getLibrariesFile
      :: (MonadIO m, MonadError String m)
      => Maybe FilePath -- ^ Override the default @libraries@ file?
      -> m LibrariesFile
    getLibrariesFile :: forall (m :: * -> *).
    (MonadIO m, MonadError [Char] m) =>
    Maybe [Char] -> m LibrariesFile
    getLibrariesFile (Just [Char]
    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 (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO Bool -> m Bool) -> IO Bool -> m Bool
    forall a b. (a -> b) -> a -> b
    $ [Char] -> IO Bool
    doesFileExist [Char]
    overrideLibFile)
        {-then-} (LibrariesFile -> m LibrariesFile
    forall (m :: * -> *) a. Monad m => a -> m a
    return (LibrariesFile -> m LibrariesFile)
    -> LibrariesFile -> m LibrariesFile
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Bool -> LibrariesFile
    LibrariesFile [Char]
    overrideLibFile Bool
    True)
        {-else-} ([Char] -> m LibrariesFile
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError ([Char] -> m LibrariesFile) -> [Char] -> m LibrariesFile
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Libraries file not found: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    overrideLibFile)
    getLibrariesFile Maybe [Char]
    Nothing = do
      [Char]
    agdaDir <- IO [Char] -> m [Char]
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO [Char] -> m [Char]) -> IO [Char] -> m [Char]
    forall a b. (a -> b) -> a -> b
    $ IO [Char]
    getAgdaAppDir
      let defaults :: List1 [Char]
    defaults = ShowS -> List1 [Char] -> List1 [Char]
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    List1.map ([Char]
    agdaDir [Char] -> ShowS
    </>) List1 [Char]
    defaultLibraryFiles -- NB: very short list
      [[Char]]
    files <- IO [[Char]] -> m [[Char]]
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO [[Char]] -> m [[Char]]) -> IO [[Char]] -> m [[Char]]
    forall a b. (a -> b) -> a -> b
    $ ([Char] -> IO Bool) -> [[Char]] -> IO [[Char]]
    forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m [a]
    filterM [Char] -> IO Bool
    doesFileExist (List1 [Char] -> [[Char]]
    forall a. NonEmpty a -> [a]
    List1.toList List1 [Char]
    defaults)
      case [[Char]]
    files of
        [Char]
    file : [[Char]]
    _ -> LibrariesFile -> m LibrariesFile
    forall (m :: * -> *) a. Monad m => a -> m a
    return (LibrariesFile -> m LibrariesFile)
    -> LibrariesFile -> m LibrariesFile
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Bool -> LibrariesFile
    LibrariesFile [Char]
    file Bool
    True
        []       -> LibrariesFile -> m LibrariesFile
    forall (m :: * -> *) a. Monad m => a -> m a
    return (LibrariesFile -> m LibrariesFile)
    -> LibrariesFile -> m LibrariesFile
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Bool -> LibrariesFile
    LibrariesFile (List1 [Char] -> [Char]
    forall a. NonEmpty a -> a
    List1.last List1 [Char]
    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 [Char] -> LibM [AgdaLibFile]
    getInstalledLibraries Maybe [Char]
    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
        Either [Char] LibrariesFile
    filem <- IO (Either [Char] LibrariesFile)
    -> WriterT
         [Either LibError LibWarning]
         (StateT LibState IO)
         (Either [Char] LibrariesFile)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (Either [Char] LibrariesFile)
     -> WriterT
          [Either LibError LibWarning]
          (StateT LibState IO)
          (Either [Char] LibrariesFile))
    -> IO (Either [Char] LibrariesFile)
    -> WriterT
         [Either LibError LibWarning]
         (StateT LibState IO)
         (Either [Char] LibrariesFile)
    forall a b. (a -> b) -> a -> b
    $ ExceptT [Char] IO LibrariesFile -> IO (Either [Char] LibrariesFile)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (ExceptT [Char] IO LibrariesFile
     -> IO (Either [Char] LibrariesFile))
    -> ExceptT [Char] IO LibrariesFile
    -> IO (Either [Char] LibrariesFile)
    forall a b. (a -> b) -> a -> b
    $ Maybe [Char] -> ExceptT [Char] IO LibrariesFile
    forall (m :: * -> *).
    (MonadIO m, MonadError [Char] m) =>
    Maybe [Char] -> m LibrariesFile
    getLibrariesFile Maybe [Char]
    overrideLibFile
        [AgdaLibFile]
    userlibs <- case Either [Char] LibrariesFile
    filem of
          Left [Char]
    err -> [LibError']
    -> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
    forall (m :: * -> *).
    MonadWriter [Either LibError LibWarning] m =>
    [LibError'] -> m ()
    raiseErrors' [[Char] -> LibError'
    OtherError [Char]
    err] WriterT [Either LibError LibWarning] (StateT LibState IO) ()
    -> LibErrorIO [AgdaLibFile] -> LibErrorIO [AgdaLibFile]
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> [AgdaLibFile] -> LibErrorIO [AgdaLibFile]
    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 (m :: * -> *) a. Monad m => a -> m a
    return [] else do
              [(LineNumber, [Char])]
    ls    <- IO [(LineNumber, [Char])]
    -> WriterT
         [Either LibError LibWarning]
         (StateT LibState IO)
         [(LineNumber, [Char])]
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO [(LineNumber, [Char])]
     -> WriterT
          [Either LibError LibWarning]
          (StateT LibState IO)
          [(LineNumber, [Char])])
    -> IO [(LineNumber, [Char])]
    -> WriterT
         [Either LibError LibWarning]
         (StateT LibState IO)
         [(LineNumber, [Char])]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [(LineNumber, [Char])]
    stripCommentLines ([Char] -> [(LineNumber, [Char])])
    -> IO [Char] -> IO [(LineNumber, [Char])]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Char] -> IO [Char]
    UTF8.readFile (LibrariesFile -> [Char]
    lfPath LibrariesFile
    file)
              [(LineNumber, [Char])]
    files <- IO [(LineNumber, [Char])]
    -> WriterT
         [Either LibError LibWarning]
         (StateT LibState IO)
         [(LineNumber, [Char])]
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO [(LineNumber, [Char])]
     -> WriterT
          [Either LibError LibWarning]
          (StateT LibState IO)
          [(LineNumber, [Char])])
    -> IO [(LineNumber, [Char])]
    -> WriterT
         [Either LibError LibWarning]
         (StateT LibState IO)
         [(LineNumber, [Char])]
    forall a b. (a -> b) -> a -> b
    $ [IO (LineNumber, [Char])] -> IO [(LineNumber, [Char])]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    sequence [ (LineNumber
    i, ) ([Char] -> (LineNumber, [Char]))
    -> IO [Char] -> IO (LineNumber, [Char])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Char] -> IO [Char]
    expandEnvironmentVariables [Char]
    s | (LineNumber
    i, [Char]
    s) <- [(LineNumber, [Char])]
    ls ]
              Maybe LibrariesFile
    -> [(LineNumber, [Char])] -> LibErrorIO [AgdaLibFile]
    parseLibFiles (LibrariesFile -> Maybe LibrariesFile
    forall a. a -> Maybe a
    Just LibrariesFile
    file) ([(LineNumber, [Char])] -> LibErrorIO [AgdaLibFile])
    -> [(LineNumber, [Char])] -> LibErrorIO [AgdaLibFile]
    forall a b. (a -> b) -> a -> b
    $ ((LineNumber, [Char]) -> [Char])
    -> [(LineNumber, [Char])] -> [(LineNumber, [Char])]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    nubOn (LineNumber, [Char]) -> [Char]
    forall a b. (a, b) -> b
    snd [(LineNumber, [Char])]
    files
        [AgdaLibFile]
    systemlibs <- WriterT [Either LibError LibWarning] (StateT LibState IO) Bool
    -> LibErrorIO [AgdaLibFile]
    -> LibErrorIO [AgdaLibFile]
    -> LibErrorIO [AgdaLibFile]
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifNotM (IO Bool
    -> WriterT [Either LibError LibWarning] (StateT LibState IO) Bool
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO Bool
     -> WriterT [Either LibError LibWarning] (StateT LibState IO) Bool)
    -> IO Bool
    -> WriterT [Either LibError LibWarning] (StateT LibState IO) Bool
    forall a b. (a -> b) -> a -> b
    $ [Char] -> IO Bool
    doesDirectoryExist [Char]
    systemLibDir) ([AgdaLibFile] -> LibErrorIO [AgdaLibFile]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []) (LibErrorIO [AgdaLibFile] -> LibErrorIO [AgdaLibFile])
    -> LibErrorIO [AgdaLibFile] -> LibErrorIO [AgdaLibFile]
    forall a b. (a -> b) -> a -> b
    $ do
          [[Char]]
    files <- IO [[Char]]
    -> WriterT
         [Either LibError LibWarning] (StateT LibState IO) [[Char]]
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO [[Char]]
     -> WriterT
          [Either LibError LibWarning] (StateT LibState IO) [[Char]])
    -> IO [[Char]]
    -> WriterT
         [Either LibError LibWarning] (StateT LibState IO) [[Char]]
    forall a b. (a -> b) -> a -> b
    $ ([Char] -> Bool) -> [[Char]] -> [[Char]]
    forall a. (a -> Bool) -> [a] -> [a]
    filter [Char] -> Bool
    isLibFile ([[Char]] -> [[Char]]) -> IO [[Char]] -> IO [[Char]]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Char] -> IO [[Char]]
    listDirectory [Char]
    systemLibDir
          Maybe LibrariesFile
    -> [(LineNumber, [Char])] -> LibErrorIO [AgdaLibFile]
    parseLibFiles Maybe LibrariesFile
    forall a. Maybe a
    Nothing ([(LineNumber, [Char])] -> LibErrorIO [AgdaLibFile])
    -> [(LineNumber, [Char])] -> LibErrorIO [AgdaLibFile]
    forall a b. (a -> b) -> a -> b
    $ [LineNumber] -> [[Char]] -> [(LineNumber, [Char])]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [LineNumber
    1..] ([[Char]] -> [(LineNumber, [Char])])
    -> [[Char]] -> [(LineNumber, [Char])]
    forall a b. (a -> b) -> a -> b
    $ ShowS -> [[Char]] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char]
    systemLibDir [Char] -> ShowS
    </>) [[Char]]
    files
        [AgdaLibFile] -> LibErrorIO [AgdaLibFile]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([AgdaLibFile] -> LibErrorIO [AgdaLibFile])
    -> [AgdaLibFile] -> LibErrorIO [AgdaLibFile]
    forall a b. (a -> b) -> a -> b
    $ [AgdaLibFile]
    userlibs [AgdaLibFile] -> [AgdaLibFile] -> [AgdaLibFile]
    forall a. [a] -> [a] -> [a]
    ++ [AgdaLibFile]
    systemlibs
      LibErrorIO [AgdaLibFile]
    -> (IOException -> LibErrorIO [AgdaLibFile])
    -> LibErrorIO [AgdaLibFile]
    forall (m :: * -> *) a.
    CatchIO m =>
    m a -> (IOException -> m a) -> m a
    `catchIO` \ IOException
    e -> do
        [LibError']
    -> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
    forall (m :: * -> *).
    MonadWriter [Either LibError LibWarning] m =>
    [LibError'] -> m ()
    raiseErrors' [ [Char] -> LibError'
    OtherError ([Char] -> LibError') -> [Char] -> LibError'
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines [[Char]
    "Failed to read installed libraries.", IOException -> [Char]
    forall a. Show a => a -> [Char]
    show IOException
    e] ]
        [AgdaLibFile] -> LibErrorIO [AgdaLibFile]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
      where systemLibDir :: [Char]
    systemLibDir = [Char]
    "/var/lib/agda"
            isLibFile :: [Char] -> Bool
    isLibFile [Char]
    fn = ShowS
    takeExtension [Char]
    fn [Char] -> [Char] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Char]
    ".agda-lib" Bool -> Bool -> Bool
    && Bool -> Bool
    not ([Char]
    "." [Char] -> [Char] -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `List.isPrefixOf` [Char]
    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, [Char])] -> LibErrorIO [AgdaLibFile]
    parseLibFiles Maybe LibrariesFile
    mlibFile [(LineNumber, [Char])]
    files = do

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

      let ([Either (Maybe LibPositionInfo, [Char]) AgdaLibFile]
    xs, [[LibWarning]]
    warns) = [(Either (Maybe LibPositionInfo, [Char]) AgdaLibFile,
      [LibWarning])]
    -> ([Either (Maybe LibPositionInfo, [Char]) AgdaLibFile],
        [[LibWarning]])
    forall a b. [(a, b)] -> ([a], [b])
    unzip [(Either (Maybe LibPositionInfo, [Char]) AgdaLibFile,
      [LibWarning])]
    anns
          ([(Maybe LibPositionInfo, [Char])]
    errs, [AgdaLibFile]
    als) = [Either (Maybe LibPositionInfo, [Char]) AgdaLibFile]
    -> ([(Maybe LibPositionInfo, [Char])], [AgdaLibFile])
    forall a b. [Either a b] -> ([a], [b])
    partitionEithers [Either (Maybe LibPositionInfo, [Char]) AgdaLibFile]
    xs

      Bool
    -> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
    -> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([[LibWarning]] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [[LibWarning]]
    warns) (WriterT [Either LibError LibWarning] (StateT LibState IO) ()
     -> WriterT [Either LibError LibWarning] (StateT LibState IO) ())
    -> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
    -> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
    forall a b. (a -> b) -> a -> b
    $ [LibWarning]
    -> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
    forall (m :: * -> *).
    MonadWriter [Either LibError LibWarning] m =>
    [LibWarning] -> m ()
    warnings ([LibWarning]
     -> WriterT [Either LibError LibWarning] (StateT LibState IO) ())
    -> [LibWarning]
    -> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
    forall a b. (a -> b) -> a -> b
    $ [[LibWarning]] -> [LibWarning]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[LibWarning]]
    warns
      Bool
    -> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
    -> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([(Maybe LibPositionInfo, [Char])] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(Maybe LibPositionInfo, [Char])]
    errs)  (WriterT [Either LibError LibWarning] (StateT LibState IO) ()
     -> WriterT [Either LibError LibWarning] (StateT LibState IO) ())
    -> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
    -> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
    forall a b. (a -> b) -> a -> b
    $
        [LibError]
    -> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
    forall (m :: * -> *).
    MonadWriter [Either LibError LibWarning] m =>
    [LibError] -> m ()
    raiseErrors ([LibError]
     -> WriterT [Either LibError LibWarning] (StateT LibState IO) ())
    -> [LibError]
    -> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
    forall a b. (a -> b) -> a -> b
    $ ((Maybe LibPositionInfo, [Char]) -> LibError)
    -> [(Maybe LibPositionInfo, [Char])] -> [LibError]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(Maybe LibPositionInfo
    mc,[Char]
    s) -> Maybe LibPositionInfo -> LibError' -> LibError
    LibError Maybe LibPositionInfo
    mc (LibError' -> LibError) -> LibError' -> LibError
    forall a b. (a -> b) -> a -> b
    $ [Char] -> LibError'
    OtherError [Char]
    s) [(Maybe LibPositionInfo, [Char])]
    errs

      [AgdaLibFile] -> LibErrorIO [AgdaLibFile]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([AgdaLibFile] -> LibErrorIO [AgdaLibFile])
    -> [AgdaLibFile] -> LibErrorIO [AgdaLibFile]
    forall a b. (a -> b) -> a -> b
    $ (AgdaLibFile -> [Char]) -> [AgdaLibFile] -> [AgdaLibFile]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    nubOn AgdaLibFile -> [Char]
    _libFile [AgdaLibFile]
    als

    -- | Remove trailing white space and line comments.
    --
    stripCommentLines :: String -> [(LineNumber, String)]
    stripCommentLines :: [Char] -> [(LineNumber, [Char])]
    stripCommentLines = ((LineNumber, [Char]) -> [(LineNumber, [Char])])
    -> [(LineNumber, [Char])] -> [(LineNumber, [Char])]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (LineNumber, [Char]) -> [(LineNumber, [Char])]
    forall {a}. (a, [Char]) -> [(a, [Char])]
    strip ([(LineNumber, [Char])] -> [(LineNumber, [Char])])
    -> ([Char] -> [(LineNumber, [Char])])
    -> [Char]
    -> [(LineNumber, [Char])]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [LineNumber] -> [[Char]] -> [(LineNumber, [Char])]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [LineNumber
    1..] ([[Char]] -> [(LineNumber, [Char])])
    -> ([Char] -> [[Char]]) -> [Char] -> [(LineNumber, [Char])]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> [[Char]]
    lines
      where
        strip :: (a, [Char]) -> [(a, [Char])]
    strip (a
    i, [Char]
    s) = [ (a
    i, [Char]
    s') | Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Char]
    s' ]
          where s' :: [Char]
    s' = ShowS
    trimLineComment [Char]
    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
      [Char]
    agdaDir <- IO [Char]
    getAgdaAppDir
      let defaults :: List1 [Char]
    defaults = ShowS -> List1 [Char] -> List1 [Char]
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    List1.map ([Char]
    agdaDir [Char] -> ShowS
    </>) List1 [Char]
    defaultExecutableFiles  -- NB: very short list
      [[Char]]
    files <- ([Char] -> IO Bool) -> [[Char]] -> IO [[Char]]
    forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m [a]
    filterM [Char] -> IO Bool
    doesFileExist (List1 [Char] -> [[Char]]
    forall a. NonEmpty a -> [a]
    List1.toList List1 [Char]
    defaults)
      case [[Char]]
    files of
        [Char]
    file : [[Char]]
    _ -> ExecutablesFile -> IO ExecutablesFile
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ExecutablesFile -> IO ExecutablesFile)
    -> ExecutablesFile -> IO ExecutablesFile
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Bool -> ExecutablesFile
    ExecutablesFile [Char]
    file Bool
    True
        []       -> ExecutablesFile -> IO ExecutablesFile
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ExecutablesFile -> IO ExecutablesFile)
    -> ExecutablesFile -> IO ExecutablesFile
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Bool -> ExecutablesFile
    ExecutablesFile (List1 [Char] -> [Char]
    forall a. NonEmpty a -> a
    List1.last List1 [Char]
    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 [Char])
    getTrustedExecutables = [AgdaLibFile]
    -> LibErrorIO (Map Text [Char]) -> LibM (Map Text [Char])
    forall a. [AgdaLibFile] -> LibErrorIO a -> LibM a
    mkLibM [] (LibErrorIO (Map Text [Char]) -> LibM (Map Text [Char]))
    -> LibErrorIO (Map Text [Char]) -> LibM (Map Text [Char])
    forall a b. (a -> b) -> a -> b
    $ do
        ExecutablesFile
    file <- IO ExecutablesFile
    -> WriterT
         [Either LibError LibWarning] (StateT LibState IO) ExecutablesFile
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO IO ExecutablesFile
    getExecutablesFile
        if Bool -> Bool
    not (ExecutablesFile -> Bool
    efExists ExecutablesFile
    file) then Map Text [Char] -> LibErrorIO (Map Text [Char])
    forall (m :: * -> *) a. Monad m => a -> m a
    return Map Text [Char]
    forall k a. Map k a
    Map.empty else do
          [(LineNumber, [Char])]
    es    <- IO [(LineNumber, [Char])]
    -> WriterT
         [Either LibError LibWarning]
         (StateT LibState IO)
         [(LineNumber, [Char])]
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO [(LineNumber, [Char])]
     -> WriterT
          [Either LibError LibWarning]
          (StateT LibState IO)
          [(LineNumber, [Char])])
    -> IO [(LineNumber, [Char])]
    -> WriterT
         [Either LibError LibWarning]
         (StateT LibState IO)
         [(LineNumber, [Char])]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [(LineNumber, [Char])]
    stripCommentLines ([Char] -> [(LineNumber, [Char])])
    -> IO [Char] -> IO [(LineNumber, [Char])]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Char] -> IO [Char]
    UTF8.readFile (ExecutablesFile -> [Char]
    efPath ExecutablesFile
    file)
          [(LineNumber, [Char])]
    files <- IO [(LineNumber, [Char])]
    -> WriterT
         [Either LibError LibWarning]
         (StateT LibState IO)
         [(LineNumber, [Char])]
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO [(LineNumber, [Char])]
     -> WriterT
          [Either LibError LibWarning]
          (StateT LibState IO)
          [(LineNumber, [Char])])
    -> IO [(LineNumber, [Char])]
    -> WriterT
         [Either LibError LibWarning]
         (StateT LibState IO)
         [(LineNumber, [Char])]
    forall a b. (a -> b) -> a -> b
    $ [IO (LineNumber, [Char])] -> IO [(LineNumber, [Char])]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    sequence [ (LineNumber
    i, ) ([Char] -> (LineNumber, [Char]))
    -> IO [Char] -> IO (LineNumber, [Char])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Char] -> IO [Char]
    expandEnvironmentVariables [Char]
    s | (LineNumber
    i, [Char]
    s) <- [(LineNumber, [Char])]
    es ]
          Map Text [Char]
    tmp   <- ExecutablesFile
    -> [(LineNumber, [Char])] -> LibErrorIO (Map Text [Char])
    parseExecutablesFile ExecutablesFile
    file ([(LineNumber, [Char])] -> LibErrorIO (Map Text [Char]))
    -> [(LineNumber, [Char])] -> LibErrorIO (Map Text [Char])
    forall a b. (a -> b) -> a -> b
    $ ((LineNumber, [Char]) -> [Char])
    -> [(LineNumber, [Char])] -> [(LineNumber, [Char])]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    nubOn (LineNumber, [Char]) -> [Char]
    forall a b. (a, b) -> b
    snd [(LineNumber, [Char])]
    files
          Map Text [Char] -> LibErrorIO (Map Text [Char])
    forall (m :: * -> *) a. Monad m => a -> m a
    return Map Text [Char]
    tmp
      LibErrorIO (Map Text [Char])
    -> (IOException -> LibErrorIO (Map Text [Char]))
    -> LibErrorIO (Map Text [Char])
    forall (m :: * -> *) a.
    CatchIO m =>
    m a -> (IOException -> m a) -> m a
    `catchIO` \ IOException
    e -> do
        [LibError']
    -> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
    forall (m :: * -> *).
    MonadWriter [Either LibError LibWarning] m =>
    [LibError'] -> m ()
    raiseErrors' [ [Char] -> LibError'
    OtherError ([Char] -> LibError') -> [Char] -> LibError'
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines [[Char]
    "Failed to read trusted executables.", IOException -> [Char]
    forall a. Show a => a -> [Char]
    show IOException
    e] ]
        Map Text [Char] -> LibErrorIO (Map Text [Char])
    forall (m :: * -> *) a. Monad m => a -> m a
    return Map Text [Char]
    forall k a. Map k a
    Map.empty

    -- | Parse the @executables@ file.
    --
    parseExecutablesFile
      :: ExecutablesFile
      -> [(LineNumber, FilePath)]
      -> LibErrorIO (Map ExeName FilePath)
    parseExecutablesFile :: ExecutablesFile
    -> [(LineNumber, [Char])] -> LibErrorIO (Map Text [Char])
    parseExecutablesFile ExecutablesFile
    ef [(LineNumber, [Char])]
    files =
      ([Maybe (Text, [Char])] -> Map Text [Char])
    -> WriterT
         [Either LibError LibWarning]
         (StateT LibState IO)
         [Maybe (Text, [Char])]
    -> LibErrorIO (Map Text [Char])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ([(Text, [Char])] -> Map Text [Char]
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList ([(Text, [Char])] -> Map Text [Char])
    -> ([Maybe (Text, [Char])] -> [(Text, [Char])])
    -> [Maybe (Text, [Char])]
    -> Map Text [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Maybe (Text, [Char])] -> [(Text, [Char])]
    forall a. [Maybe a] -> [a]
    catMaybes) (WriterT
       [Either LibError LibWarning]
       (StateT LibState IO)
       [Maybe (Text, [Char])]
     -> LibErrorIO (Map Text [Char]))
    -> (((LineNumber, [Char])
         -> WriterT
              [Either LibError LibWarning]
              (StateT LibState IO)
              (Maybe (Text, [Char])))
        -> WriterT
             [Either LibError LibWarning]
             (StateT LibState IO)
             [Maybe (Text, [Char])])
    -> ((LineNumber, [Char])
        -> WriterT
             [Either LibError LibWarning]
             (StateT LibState IO)
             (Maybe (Text, [Char])))
    -> LibErrorIO (Map Text [Char])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [(LineNumber, [Char])]
    -> ((LineNumber, [Char])
        -> WriterT
             [Either LibError LibWarning]
             (StateT LibState IO)
             (Maybe (Text, [Char])))
    -> WriterT
         [Either LibError LibWarning]
         (StateT LibState IO)
         [Maybe (Text, [Char])]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [(LineNumber, [Char])]
    files (((LineNumber, [Char])
      -> WriterT
           [Either LibError LibWarning]
           (StateT LibState IO)
           (Maybe (Text, [Char])))
     -> LibErrorIO (Map Text [Char]))
    -> ((LineNumber, [Char])
        -> WriterT
             [Either LibError LibWarning]
             (StateT LibState IO)
             (Maybe (Text, [Char])))
    -> LibErrorIO (Map Text [Char])
    forall a b. (a -> b) -> a -> b
    $ \(LineNumber
    ln, [Char]
    fp) -> do

        -- Compute canonical executable name and absolute filepath.
        let strExeName :: [Char]
    strExeName  = ShowS
    takeFileName [Char]
    fp
        let strExeName' :: [Char]
    strExeName' = [Char] -> Maybe [Char] -> [Char]
    forall a. a -> Maybe a -> a
    fromMaybe [Char]
    strExeName (Maybe [Char] -> [Char]) -> Maybe [Char] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Char] -> Maybe [Char]
    stripExtension [Char]
    exeExtension [Char]
    strExeName
        let txtExeName :: Text
    txtExeName  = [Char] -> Text
    T.pack [Char]
    strExeName'
        [Char]
    exePath <- IO [Char]
    -> WriterT [Either LibError LibWarning] (StateT LibState IO) [Char]
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO [Char]
     -> WriterT
          [Either LibError LibWarning] (StateT LibState IO) [Char])
    -> IO [Char]
    -> WriterT [Either LibError LibWarning] (StateT LibState IO) [Char]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> IO [Char]
    makeAbsolute [Char]
    fp
        Maybe (Text, [Char])
    -> WriterT
         [Either LibError LibWarning]
         (StateT LibState IO)
         (Maybe (Text, [Char]))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (Text, [Char])
     -> WriterT
          [Either LibError LibWarning]
          (StateT LibState IO)
          (Maybe (Text, [Char])))
    -> Maybe (Text, [Char])
    -> WriterT
         [Either LibError LibWarning]
         (StateT LibState IO)
         (Maybe (Text, [Char]))
    forall a b. (a -> b) -> a -> b
    $ (Text, [Char]) -> Maybe (Text, [Char])
    forall a. a -> Maybe a
    Just (Text
    txtExeName, [Char]
    exePath)

    ------------------------------------------------------------------------
    -- * 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 [Char] -> [AgdaLibFile] -> [[Char]] -> LibM [[Char]]
    libraryIncludePaths Maybe [Char]
    overrideLibFile [AgdaLibFile]
    libs [[Char]]
    xs0 = [AgdaLibFile]
    -> WriterT
         [Either LibError LibWarning] (StateT LibState IO) [[Char]]
    -> LibM [[Char]]
    forall a. [AgdaLibFile] -> LibErrorIO a -> LibM a
    mkLibM [AgdaLibFile]
    libs (WriterT [Either LibError LibWarning] (StateT LibState IO) [[Char]]
     -> LibM [[Char]])
    -> WriterT
         [Either LibError LibWarning] (StateT LibState IO) [[Char]]
    -> LibM [[Char]]
    forall a b. (a -> b) -> a -> b
    $ StateT LibState IO ([[Char]], [Either LibError LibWarning])
    -> WriterT
         [Either LibError LibWarning] (StateT LibState IO) [[Char]]
    forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
    WriterT (StateT LibState IO ([[Char]], [Either LibError LibWarning])
     -> WriterT
          [Either LibError LibWarning] (StateT LibState IO) [[Char]])
    -> StateT LibState IO ([[Char]], [Either LibError LibWarning])
    -> WriterT
         [Either LibError LibWarning] (StateT LibState IO) [[Char]]
    forall a b. (a -> b) -> a -> b
    $ do
        Either [Char] LibrariesFile
    efile <- IO (Either [Char] LibrariesFile)
    -> StateT LibState IO (Either [Char] LibrariesFile)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (Either [Char] LibrariesFile)
     -> StateT LibState IO (Either [Char] LibrariesFile))
    -> IO (Either [Char] LibrariesFile)
    -> StateT LibState IO (Either [Char] LibrariesFile)
    forall a b. (a -> b) -> a -> b
    $ ExceptT [Char] IO LibrariesFile -> IO (Either [Char] LibrariesFile)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (ExceptT [Char] IO LibrariesFile
     -> IO (Either [Char] LibrariesFile))
    -> ExceptT [Char] IO LibrariesFile
    -> IO (Either [Char] LibrariesFile)
    forall a b. (a -> b) -> a -> b
    $ Maybe [Char] -> ExceptT [Char] IO LibrariesFile
    forall (m :: * -> *).
    (MonadIO m, MonadError [Char] m) =>
    Maybe [Char] -> m LibrariesFile
    getLibrariesFile Maybe [Char]
    overrideLibFile
        case Either [Char] LibrariesFile
    efile of
          Left [Char]
    err -> ([[Char]], [Either LibError LibWarning])
    -> StateT LibState IO ([[Char]], [Either LibError LibWarning])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([], [LibError -> Either LibError LibWarning
    forall a b. a -> Either a b
    Left (LibError -> Either LibError LibWarning)
    -> LibError -> Either LibError LibWarning
    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
    $ [Char] -> LibError'
    OtherError [Char]
    err])
          Right LibrariesFile
    file -> ([[Char]], [Either LibError LibWarning])
    -> StateT LibState IO ([[Char]], [Either LibError LibWarning])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (([[Char]], [Either LibError LibWarning])
     -> StateT LibState IO ([[Char]], [Either LibError LibWarning]))
    -> ([[Char]], [Either LibError LibWarning])
    -> StateT LibState IO ([[Char]], [Either LibError LibWarning])
    forall a b. (a -> b) -> a -> b
    $ Writer [Either LibError LibWarning] [[Char]]
    -> ([[Char]], [Either LibError LibWarning])
    forall w a. Writer w a -> (a, w)
    runWriter (Writer [Either LibError LibWarning] [[Char]]
     -> ([[Char]], [Either LibError LibWarning]))
    -> Writer [Either LibError LibWarning] [[Char]]
    -> ([[Char]], [Either LibError LibWarning])
    forall a b. (a -> b) -> a -> b
    $ ([[Char]]
    dot [[Char]] -> [[Char]] -> [[Char]]
    forall a. [a] -> [a] -> [a]
    ++) ([[Char]] -> [[Char]])
    -> ([AgdaLibFile] -> [[Char]]) -> [AgdaLibFile] -> [[Char]]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [AgdaLibFile] -> [[Char]]
    incs ([AgdaLibFile] -> [[Char]])
    -> WriterT [Either LibError LibWarning] Identity [AgdaLibFile]
    -> Writer [Either LibError LibWarning] [[Char]]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> LibrariesFile
    -> [[Char]]
    -> [[Char]]
    -> WriterT [Either LibError LibWarning] Identity [AgdaLibFile]
    find LibrariesFile
    file [] [[Char]]
    xs
      where
        ([[Char]]
    dots, [[Char]]
    xs) = ([Char] -> Bool) -> [[Char]] -> ([[Char]], [[Char]])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    List.partition ([Char] -> [Char] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Char]
    libNameForCurrentDir) ([[Char]] -> ([[Char]], [[Char]]))
    -> [[Char]] -> ([[Char]], [[Char]])
    forall a b. (a -> b) -> a -> b
    $ ShowS -> [[Char]] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map ShowS
    trim [[Char]]
    xs0
        incs :: [AgdaLibFile] -> [[Char]]
    incs       = ShowS -> [[Char]] -> [[Char]]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    nubOn ShowS
    forall a. a -> a
    id ([[Char]] -> [[Char]])
    -> ([AgdaLibFile] -> [[Char]]) -> [AgdaLibFile] -> [[Char]]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (AgdaLibFile -> [[Char]]) -> [AgdaLibFile] -> [[Char]]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap AgdaLibFile -> [[Char]]
    _libIncludes
        dot :: [[Char]]
    dot        = [ [Char]
    "." | Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [[Char]]
    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 [Either LibError LibWarning] [AgdaLibFile]
        find :: LibrariesFile
    -> [[Char]]
    -> [[Char]]
    -> WriterT [Either LibError LibWarning] Identity [AgdaLibFile]
    find LibrariesFile
    _ [[Char]]
    _ [] = [AgdaLibFile]
    -> WriterT [Either LibError LibWarning] Identity [AgdaLibFile]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure []
        find LibrariesFile
    file [[Char]]
    visited ([Char]
    x : [[Char]]
    xs)
          | [Char]
    x [Char] -> [[Char]] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [[Char]]
    visited = LibrariesFile
    -> [[Char]]
    -> [[Char]]
    -> WriterT [Either LibError LibWarning] Identity [AgdaLibFile]
    find LibrariesFile
    file [[Char]]
    visited [[Char]]
    xs
          | Bool
    otherwise = do
              -- May or may not find the library
              Maybe AgdaLibFile
    ml <- case [Char] -> [AgdaLibFile] -> [AgdaLibFile]
    findLib [Char]
    x [AgdaLibFile]
    libs of
                [AgdaLibFile
    l] -> Maybe AgdaLibFile
    -> WriterT
         [Either LibError LibWarning] Identity (Maybe AgdaLibFile)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (AgdaLibFile -> Maybe AgdaLibFile
    forall a. a -> Maybe a
    Just AgdaLibFile
    l)
                []  -> Maybe AgdaLibFile
    forall a. Maybe a
    Nothing Maybe AgdaLibFile
    -> WriterT [Either LibError LibWarning] Identity ()
    -> WriterT
         [Either LibError LibWarning] Identity (Maybe AgdaLibFile)
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ [LibError'] -> WriterT [Either LibError LibWarning] Identity ()
    forall (m :: * -> *).
    MonadWriter [Either LibError LibWarning] m =>
    [LibError'] -> m ()
    raiseErrors' [LibrariesFile -> [Char] -> LibError'
    LibNotFound LibrariesFile
    file [Char]
    x]
                [AgdaLibFile]
    ls  -> Maybe AgdaLibFile
    forall a. Maybe a
    Nothing Maybe AgdaLibFile
    -> WriterT [Either LibError LibWarning] Identity ()
    -> WriterT
         [Either LibError LibWarning] Identity (Maybe AgdaLibFile)
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ [LibError'] -> WriterT [Either LibError LibWarning] Identity ()
    forall (m :: * -> *).
    MonadWriter [Either LibError LibWarning] m =>
    [LibError'] -> m ()
    raiseErrors' [[Char] -> [AgdaLibFile] -> LibError'
    AmbiguousLib [Char]
    x [AgdaLibFile]
    ls]
              -- If it is found, add its dependencies to work list
              let xs' :: [[Char]]
    xs' = (AgdaLibFile -> [[Char]]) -> Maybe AgdaLibFile -> [[Char]]
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap AgdaLibFile -> [[Char]]
    _libDepends Maybe AgdaLibFile
    ml [[Char]] -> [[Char]] -> [[Char]]
    forall a. [a] -> [a] -> [a]
    ++ [[Char]]
    xs
              Maybe AgdaLibFile -> [AgdaLibFile] -> [AgdaLibFile]
    forall a. Maybe a -> [a] -> [a]
    mcons Maybe AgdaLibFile
    ml ([AgdaLibFile] -> [AgdaLibFile])
    -> WriterT [Either LibError LibWarning] Identity [AgdaLibFile]
    -> WriterT [Either LibError LibWarning] Identity [AgdaLibFile]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> LibrariesFile
    -> [[Char]]
    -> [[Char]]
    -> WriterT [Either LibError LibWarning] Identity [AgdaLibFile]
    find LibrariesFile
    file ([Char]
    x [Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    : [[Char]]
    visited) [[Char]]
    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 :: [Char] -> [AgdaLibFile] -> [AgdaLibFile]
    findLib = (AgdaLibFile -> [Char]) -> [Char] -> [AgdaLibFile] -> [AgdaLibFile]
    forall a. (a -> [Char]) -> [Char] -> [a] -> [a]
    findLib' AgdaLibFile -> [Char]
    _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 -> [Char]) -> [Char] -> [a] -> [a]
    findLib' a -> [Char]
    libName [Char]
    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 ((([Char], Bool, [Integer]) -> ([Char], Bool, [Integer]) -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (([Char], Bool, [Integer]) -> ([Char], Bool, [Integer]) -> Bool)
    -> (a -> ([Char], Bool, [Integer])) -> a -> a -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` a -> ([Char], Bool, [Integer])
    versionMeasure) 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 ((([Char], Bool, [Integer])
     -> ([Char], Bool, [Integer]) -> Ordering)
    -> ([Char], Bool, [Integer])
    -> ([Char], Bool, [Integer])
    -> Ordering
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip ([Char], Bool, [Integer]) -> ([Char], Bool, [Integer]) -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (([Char], Bool, [Integer])
     -> ([Char], Bool, [Integer]) -> Ordering)
    -> (a -> ([Char], Bool, [Integer])) -> a -> a -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` a -> ([Char], Bool, [Integer])
    versionMeasure)
                         [ a
    l | a
    l <- [a]
    libs, [Char]
    x [Char] -> [Char] -> Bool
    `hasMatch` a -> [Char]
    libName a
    l ]

        -- foo > foo-2.2 > foo-2.0.1 > foo-2 > foo-1.0
        versionMeasure :: a -> ([Char], Bool, [Integer])
    versionMeasure a
    l = ([Char]
    rx, [Integer] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Integer]
    vs, [Integer]
    vs)
          where
            VersionView [Char]
    rx [Integer]
    vs = [Char] -> VersionView
    versionView (a -> [Char]
    libName a
    l)

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

    -- | Split a library name into basename and a list of version numbers.
    --
    --   > versionView "foo-1.2.3"    == VersionView "foo" [1, 2, 3]
    --   > versionView "foo-01.002.3" == VersionView "foo" [1, 2, 3]
    --
    --   Note that because of leading zeros, @versionView@ is not injective.
    --   (@unVersionView . versionView@ would produce a normal form.)
    versionView :: LibName -> VersionView
    versionView :: [Char] -> VersionView
    versionView [Char]
    s =
      case (Char -> Bool) -> [Char] -> ([Char], [Char])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    span (\ Char
    c -> Char -> Bool
    isDigit Char
    c Bool -> Bool -> Bool
    || Char
    c Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '.') (ShowS
    forall a. [a] -> [a]
    reverse [Char]
    s) of
        ([Char]
    v, Char
    '-' : [Char]
    x) | [[Char]] -> Bool
    forall {t :: * -> *} {a}. Foldable t => [t a] -> Bool
    valid [[Char]]
    vs ->
          [Char] -> [Integer] -> VersionView
    VersionView (ShowS
    forall a. [a] -> [a]
    reverse [Char]
    x) ([Integer] -> VersionView) -> [Integer] -> VersionView
    forall a b. (a -> b) -> a -> b
    $ [Integer] -> [Integer]
    forall a. [a] -> [a]
    reverse ([Integer] -> [Integer]) -> [Integer] -> [Integer]
    forall a b. (a -> b) -> a -> b
    $ ([Char] -> Integer) -> [[Char]] -> [Integer]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char] -> Integer
    forall a. Read a => [Char] -> a
    read ([Char] -> Integer) -> ShowS -> [Char] -> Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ShowS
    forall a. [a] -> [a]
    reverse) [[Char]]
    vs
          where vs :: [[Char]]
    vs = (Char -> Bool) -> [Char] -> [[Char]]
    forall a. (a -> Bool) -> [a] -> [[a]]
    chopWhen (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '.') [Char]
    v
                valid :: [t a] -> Bool
    valid [] = Bool
    False
                valid [t a]
    vs = Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ (t a -> Bool) -> [t a] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any t a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [t a]
    vs
        ([Char], [Char])
    _ -> [Char] -> [Integer] -> VersionView
    VersionView [Char]
    s []

    -- | Print a @VersionView@, inverse of @versionView@ (modulo leading zeros).
    unVersionView :: VersionView -> LibName
    unVersionView :: VersionView -> [Char]
    unVersionView = \case
      VersionView [Char]
    base [] -> [Char]
    base
      VersionView [Char]
    base [Integer]
    vs -> [Char]
    base [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "-" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    List.intercalate [Char]
    "." ((Integer -> [Char]) -> [Integer] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map Integer -> [Char]
    forall a. Show a => a -> [Char]
    show [Integer]
    vs)