    -- | Basic data types for library management.

    module Agda.Interaction.Library.Base where

    import Prelude hiding (null)

    import Control.DeepSeq
    import qualified Control.Exception as E

    import Control.Monad.Except
    import Control.Monad.State
    import Control.Monad.Writer        ( WriterT, runWriterT, MonadWriter, tell )
    import Control.Monad.IO.Class      ( MonadIO(..) )

    import Data.Bifunctor              ( first , second )
    import Data.Char                   ( isDigit )
    import Data.Function               ( (&), on )
    import Data.Hashable               ( Hashable )
    import qualified Data.List         as List
    import Data.Map                    ( Map )
    import qualified Data.Map          as Map
    import Data.Semigroup              ( Semigroup(..) )
    import Data.Text                   ( Text, unpack )
    import qualified Data.Text         as T

    import GHC.Generics                ( Generic )

    import System.Directory

    import Agda.Interaction.Options.Warnings

    import Agda.Syntax.Common.Pretty
    import Agda.Syntax.Position

    import Agda.Utils.IO               ( showIOException )
    import Agda.Utils.Lens
    import Agda.Utils.List             ( chopWhen )
    import Agda.Utils.List1            ( List1, toList )
    import Agda.Utils.List2            ( List2, toList )
    import qualified Agda.Utils.List1  as List1
    import Agda.Utils.Null

    -- | A symbolic library name.
    --
    --   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 LibName = LibName
      { LibName -> Text
    libNameBase    :: Text
          -- ^ Actual library name.
      , LibName -> [Integer]
    libNameVersion :: [Integer]
          -- ^ Major version, minor version, subminor version, etc., all non-negative.
      } deriving (LibName -> LibName -> Bool
    (LibName -> LibName -> Bool)
    -> (LibName -> LibName -> Bool) -> Eq LibName
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: LibName -> LibName -> Bool
    == :: LibName -> LibName -> Bool
    $c/= :: LibName -> LibName -> Bool
    /= :: LibName -> LibName -> Bool
    Eq, LineNumber -> LibName -> ShowS
    [LibName] -> ShowS
    LibName -> [Char]
    (LineNumber -> LibName -> ShowS)
    -> (LibName -> [Char]) -> ([LibName] -> ShowS) -> Show LibName
    forall a.
    (LineNumber -> a -> ShowS)
    -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: LineNumber -> LibName -> ShowS
    showsPrec :: LineNumber -> LibName -> ShowS
    $cshow :: LibName -> [Char]
    show :: LibName -> [Char]
    $cshowList :: [LibName] -> ShowS
    showList :: [LibName] -> ShowS
    Show, (forall x. LibName -> Rep LibName x)
    -> (forall x. Rep LibName x -> LibName) -> Generic LibName
    forall x. Rep LibName x -> LibName
    forall x. LibName -> Rep LibName x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. LibName -> Rep LibName x
    from :: forall x. LibName -> Rep LibName x
    $cto :: forall x. Rep LibName x -> LibName
    to :: forall x. Rep LibName x -> LibName
    Generic)

    -- | In comparisons, a missing version number is assumed to be infinity.
    --   E.g. @foo > foo-2.2 > foo-2.0.1 > foo-2 > foo-1.0@.
    instance Ord LibName where
      compare :: LibName -> LibName -> Ordering
    compare = (Text, Bool, [Integer]) -> (Text, Bool, [Integer]) -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare ((Text, Bool, [Integer]) -> (Text, Bool, [Integer]) -> Ordering)
    -> (LibName -> (Text, Bool, [Integer]))
    -> LibName
    -> LibName
    -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` LibName -> (Text, Bool, [Integer])
    versionMeasure
        where
          versionMeasure :: LibName -> (Text, Bool, [Integer])
          versionMeasure :: LibName -> (Text, Bool, [Integer])
    versionMeasure (LibName Text
    rx [Integer]
    vs) = (Text
    rx, [Integer] -> Bool
    forall a. Null a => a -> Bool
    null [Integer]
    vs, [Integer]
    vs)

    instance Pretty LibName where
      pretty :: LibName -> Doc
    pretty = \case
        LibName Text
    base [] -> Text -> Doc
    forall a. Pretty a => a -> Doc
    pretty Text
    base
        LibName Text
    base [Integer]
    vs -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hcat [ Text -> Doc
    forall a. Pretty a => a -> Doc
    pretty Text
    base, Doc
    "-", [Char] -> Doc
    forall a. [Char] -> Doc a
    text ([Char] -> Doc) -> [Char] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    List.intercalate [Char]
    "." ([[Char]] -> [Char]) -> [[Char]] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ (Integer -> [Char]) -> [Integer] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map Integer -> [Char]
    forall a. Show a => a -> [Char]
    show [Integer]
    vs ]

    -- | Split a library name into basename and a list of version numbers.
    --
    --   > parseLibName "foo-1.2.3"    == LibName "foo" [1, 2, 3]
    --   > parseLibName "foo-01.002.3" == LibName "foo" [1, 2, 3]
    --
    --   Note that because of leading zeros, @parseLibName@ is not injective.
    --   (@prettyShow . parseLibName@ would produce a normal form.)
    parseLibName :: String -> LibName
    parseLibName :: [Char] -> LibName
    parseLibName [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 {a}. Null a => [a] -> Bool
    valid [[Char]]
    vs ->
          Text -> [Integer] -> LibName
    LibName ([Char] -> Text
    T.pack ([Char] -> Text) -> [Char] -> Text
    forall a b. (a -> b) -> a -> b
    $ ShowS
    forall a. [a] -> [a]
    reverse [Char]
    x) ([Integer] -> LibName) -> [Integer] -> LibName
    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 :: [a] -> Bool
    valid [] = Bool
    False
            valid [a]
    vs = Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ (a -> Bool) -> [a] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any a -> Bool
    forall a. Null a => a -> Bool
    null [a]
    vs
        ([Char], [Char])
    _ -> Text -> [Integer] -> LibName
    LibName ([Char] -> Text
    T.pack [Char]
    s) []

    data LibrariesFile = LibrariesFile
      { LibrariesFile -> [Char]
    lfPath   :: FilePath
          -- ^ E.g. @~/.agda/libraries@.
      , LibrariesFile -> Bool
    lfExists :: Bool
           -- ^ The libraries file might not exist,
           --   but we may print its assumed location in error messages.
      } deriving (LineNumber -> LibrariesFile -> ShowS
    [LibrariesFile] -> ShowS
    LibrariesFile -> [Char]
    (LineNumber -> LibrariesFile -> ShowS)
    -> (LibrariesFile -> [Char])
    -> ([LibrariesFile] -> ShowS)
    -> Show LibrariesFile
    forall a.
    (LineNumber -> a -> ShowS)
    -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: LineNumber -> LibrariesFile -> ShowS
    showsPrec :: LineNumber -> LibrariesFile -> ShowS
    $cshow :: LibrariesFile -> [Char]
    show :: LibrariesFile -> [Char]
    $cshowList :: [LibrariesFile] -> ShowS
    showList :: [LibrariesFile] -> ShowS
    Show, (forall x. LibrariesFile -> Rep LibrariesFile x)
    -> (forall x. Rep LibrariesFile x -> LibrariesFile)
    -> Generic LibrariesFile
    forall x. Rep LibrariesFile x -> LibrariesFile
    forall x. LibrariesFile -> Rep LibrariesFile x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. LibrariesFile -> Rep LibrariesFile x
    from :: forall x. LibrariesFile -> Rep LibrariesFile x
    $cto :: forall x. Rep LibrariesFile x -> LibrariesFile
    to :: forall x. Rep LibrariesFile x -> LibrariesFile
    Generic)

    -- | A symbolic executable name.
    --
    type ExeName = Text
    type ExeMap  = Map ExeName FilePath

    data ExecutablesFile = ExecutablesFile
      { ExecutablesFile -> [Char]
    efPath   :: FilePath
          -- ^ E.g. @~/.agda/executables@.
      , ExecutablesFile -> Bool
    efExists :: Bool
           -- ^ The executables file might not exist,
           --   but we may print its assumed location in error messages.
      } deriving (LineNumber -> ExecutablesFile -> ShowS
    [ExecutablesFile] -> ShowS
    ExecutablesFile -> [Char]
    (LineNumber -> ExecutablesFile -> ShowS)
    -> (ExecutablesFile -> [Char])
    -> ([ExecutablesFile] -> ShowS)
    -> Show ExecutablesFile
    forall a.
    (LineNumber -> a -> ShowS)
    -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: LineNumber -> ExecutablesFile -> ShowS
    showsPrec :: LineNumber -> ExecutablesFile -> ShowS
    $cshow :: ExecutablesFile -> [Char]
    show :: ExecutablesFile -> [Char]
    $cshowList :: [ExecutablesFile] -> ShowS
    showList :: [ExecutablesFile] -> ShowS
    Show, (forall x. ExecutablesFile -> Rep ExecutablesFile x)
    -> (forall x. Rep ExecutablesFile x -> ExecutablesFile)
    -> Generic ExecutablesFile
    forall x. Rep ExecutablesFile x -> ExecutablesFile
    forall x. ExecutablesFile -> Rep ExecutablesFile x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. ExecutablesFile -> Rep ExecutablesFile x
    from :: forall x. ExecutablesFile -> Rep ExecutablesFile x
    $cto :: forall x. Rep ExecutablesFile x -> ExecutablesFile
    to :: forall x. Rep ExecutablesFile x -> ExecutablesFile
    Generic)

    -- | The special name @\".\"@ is used to indicated that the current directory
    --   should count as a project root.
    --
    libNameForCurrentDir :: LibName
    libNameForCurrentDir :: LibName
    libNameForCurrentDir = Text -> [Integer] -> LibName
    LibName Text
    "." []

    -- | A file can either belong to a project located at a given root
    --   containing an .agda-lib file, or be part of the default project.
    data ProjectConfig
      = ProjectConfig
        { ProjectConfig -> [Char]
    configRoot         :: FilePath
            -- ^ Directory which contains the @.agda-lib@ file for the current project.
        , ProjectConfig -> [Char]
    configAgdaLibFile  :: FilePath
            -- ^ @.agda-lib@ file relative to 'configRoot' (filename only, no directory).
        , ProjectConfig -> LineNumber
    configAbove        :: !Int
            -- ^ How many directories above the Agda file is the @.agda-lib@ file located?
        }
      | DefaultProjectConfig
      deriving (forall x. ProjectConfig -> Rep ProjectConfig x)
    -> (forall x. Rep ProjectConfig x -> ProjectConfig)
    -> Generic ProjectConfig
    forall x. Rep ProjectConfig x -> ProjectConfig
    forall x. ProjectConfig -> Rep ProjectConfig x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. ProjectConfig -> Rep ProjectConfig x
    from :: forall x. ProjectConfig -> Rep ProjectConfig x
    $cto :: forall x. Rep ProjectConfig x -> ProjectConfig
    to :: forall x. Rep ProjectConfig x -> ProjectConfig
    Generic

    -- | The options from an @OPTIONS@ pragma (or a @.agda-lib@ file).
    --
    -- In the future it might be nice to switch to a more structured
    -- representation. Note that, currently, there is not a one-to-one
    -- correspondence between list elements and options.
    data OptionsPragma = OptionsPragma
      { OptionsPragma -> [[Char]]
    pragmaStrings :: [String]
        -- ^ The options.
      , OptionsPragma -> Range
    pragmaRange :: Range
        -- ^ The range of the options in the pragma (not including things
        -- like an @OPTIONS@ keyword).
      }
      deriving LineNumber -> OptionsPragma -> ShowS
    [OptionsPragma] -> ShowS
    OptionsPragma -> [Char]
    (LineNumber -> OptionsPragma -> ShowS)
    -> (OptionsPragma -> [Char])
    -> ([OptionsPragma] -> ShowS)
    -> Show OptionsPragma
    forall a.
    (LineNumber -> a -> ShowS)
    -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: LineNumber -> OptionsPragma -> ShowS
    showsPrec :: LineNumber -> OptionsPragma -> ShowS
    $cshow :: OptionsPragma -> [Char]
    show :: OptionsPragma -> [Char]
    $cshowList :: [OptionsPragma] -> ShowS
    showList :: [OptionsPragma] -> ShowS
    Show

    instance Semigroup OptionsPragma where
      OptionsPragma { pragmaStrings :: OptionsPragma -> [[Char]]
    pragmaStrings = [[Char]]
    ss1, pragmaRange :: OptionsPragma -> Range
    pragmaRange = Range
    r1 } <> :: OptionsPragma -> OptionsPragma -> OptionsPragma
    <>
        OptionsPragma { pragmaStrings :: OptionsPragma -> [[Char]]
    pragmaStrings = [[Char]]
    ss2, pragmaRange :: OptionsPragma -> Range
    pragmaRange = Range
    r2 } =
        OptionsPragma
          { pragmaStrings :: [[Char]]
    pragmaStrings = [[Char]]
    ss1 [[Char]] -> [[Char]] -> [[Char]]
    forall a. [a] -> [a] -> [a]
    ++ [[Char]]
    ss2
          , pragmaRange :: Range
    pragmaRange   = Range -> Range -> Range
    forall a. Ord a => Range' a -> Range' a -> Range' a
    fuseRanges Range
    r1 Range
    r2
          }

    instance Monoid OptionsPragma where
      mempty :: OptionsPragma
    mempty  = OptionsPragma { pragmaStrings :: [[Char]]
    pragmaStrings = [], pragmaRange :: Range
    pragmaRange = Range
    forall a. Range' a
    noRange }
      mappend :: OptionsPragma -> OptionsPragma -> OptionsPragma
    mappend = OptionsPragma -> OptionsPragma -> OptionsPragma
    forall a. Semigroup a => a -> a -> a
    (<>)

    -- | Ranges are not forced.

    instance NFData OptionsPragma where
      rnf :: OptionsPragma -> ()
    rnf (OptionsPragma [[Char]]
    a Range
    _) = [[Char]] -> ()
    forall a. NFData a => a -> ()
    rnf [[Char]]
    a

    -- | Content of a @.agda-lib@ file.
    --
    data AgdaLibFile = AgdaLibFile
      { AgdaLibFile -> LibName
    _libName     :: LibName     -- ^ The symbolic name of the library.
      , AgdaLibFile -> [Char]
    _libFile     :: FilePath    -- ^ Path to this @.agda-lib@ file (not content of the file).
      , AgdaLibFile -> LineNumber
    _libAbove    :: !Int        -- ^ How many directories above the
                                    --   Agda file is the @.agda-lib@ file
                                    --   located?
      , AgdaLibFile -> [[Char]]
    _libIncludes :: [FilePath]  -- ^ Roots where to look for the modules of the library.
      , AgdaLibFile -> [LibName]
    _libDepends  :: [LibName]   -- ^ Dependencies.
      , AgdaLibFile -> OptionsPragma
    _libPragmas  :: OptionsPragma
                                    -- ^ Default pragma options for all files in the library.
      }
      deriving (LineNumber -> AgdaLibFile -> ShowS
    [AgdaLibFile] -> ShowS
    AgdaLibFile -> [Char]
    (LineNumber -> AgdaLibFile -> ShowS)
    -> (AgdaLibFile -> [Char])
    -> ([AgdaLibFile] -> ShowS)
    -> Show AgdaLibFile
    forall a.
    (LineNumber -> a -> ShowS)
    -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: LineNumber -> AgdaLibFile -> ShowS
    showsPrec :: LineNumber -> AgdaLibFile -> ShowS
    $cshow :: AgdaLibFile -> [Char]
    show :: AgdaLibFile -> [Char]
    $cshowList :: [AgdaLibFile] -> ShowS
    showList :: [AgdaLibFile] -> ShowS
    Show, (forall x. AgdaLibFile -> Rep AgdaLibFile x)
    -> (forall x. Rep AgdaLibFile x -> AgdaLibFile)
    -> Generic AgdaLibFile
    forall x. Rep AgdaLibFile x -> AgdaLibFile
    forall x. AgdaLibFile -> Rep AgdaLibFile x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. AgdaLibFile -> Rep AgdaLibFile x
    from :: forall x. AgdaLibFile -> Rep AgdaLibFile x
    $cto :: forall x. Rep AgdaLibFile x -> AgdaLibFile
    to :: forall x. Rep AgdaLibFile x -> AgdaLibFile
    Generic)

    emptyLibFile :: AgdaLibFile
    emptyLibFile :: AgdaLibFile
    emptyLibFile = AgdaLibFile
      { _libName :: LibName
    _libName     = LibName
    forall a. Null a => a
    empty
      , _libFile :: [Char]
    _libFile     = [Char]
    ""
      , _libAbove :: LineNumber
    _libAbove    = LineNumber
    0
      , _libIncludes :: [[Char]]
    _libIncludes = []
      , _libDepends :: [LibName]
    _libDepends  = []
      , _libPragmas :: OptionsPragma
    _libPragmas  = OptionsPragma
    forall a. Monoid a => a
    mempty
      }

    ---------------------------------------------------------------------------
    -- * Lenses
    ---------------------------------------------------------------------------

    -- ** Lenses for 'ProjectConfig'

    lensConfigAbove :: Lens' ProjectConfig Int
    lensConfigAbove :: Lens' ProjectConfig LineNumber
    lensConfigAbove LineNumber -> f LineNumber
    f = \case
      ProjectConfig
    DefaultProjectConfig -> ProjectConfig
    DefaultProjectConfig ProjectConfig -> f LineNumber -> f ProjectConfig
    forall a b. a -> f b -> f a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ LineNumber -> f LineNumber
    f LineNumber
    0
      c :: ProjectConfig
    c@ProjectConfig{} -> LineNumber -> f LineNumber
    f (ProjectConfig -> LineNumber
    configAbove ProjectConfig
    c) f LineNumber -> (LineNumber -> ProjectConfig) -> f ProjectConfig
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ !LineNumber
    i -> ProjectConfig
    c{ configAbove = i }

    -- ** Lenses for 'AgdaLibFile'

    libName :: Lens' AgdaLibFile LibName
    libName :: Lens' AgdaLibFile LibName
    libName LibName -> f LibName
    f AgdaLibFile
    a = LibName -> f LibName
    f (AgdaLibFile -> LibName
    _libName AgdaLibFile
    a) f LibName -> (LibName -> AgdaLibFile) -> f AgdaLibFile
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ LibName
    x -> AgdaLibFile
    a { _libName = x }

    libFile :: Lens' AgdaLibFile FilePath
    libFile :: Lens' AgdaLibFile [Char]
    libFile [Char] -> f [Char]
    f AgdaLibFile
    a = [Char] -> f [Char]
    f (AgdaLibFile -> [Char]
    _libFile AgdaLibFile
    a) f [Char] -> ([Char] -> AgdaLibFile) -> f AgdaLibFile
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ [Char]
    x -> AgdaLibFile
    a { _libFile = x }

    libAbove :: Lens' AgdaLibFile Int
    libAbove :: Lens' AgdaLibFile LineNumber
    libAbove LineNumber -> f LineNumber
    f AgdaLibFile
    a = LineNumber -> f LineNumber
    f (AgdaLibFile -> LineNumber
    _libAbove AgdaLibFile
    a) f LineNumber -> (LineNumber -> AgdaLibFile) -> f AgdaLibFile
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ LineNumber
    x -> AgdaLibFile
    a { _libAbove = x }

    libIncludes :: Lens' AgdaLibFile [FilePath]
    libIncludes :: Lens' AgdaLibFile [[Char]]
    libIncludes [[Char]] -> f [[Char]]
    f AgdaLibFile
    a = [[Char]] -> f [[Char]]
    f (AgdaLibFile -> [[Char]]
    _libIncludes AgdaLibFile
    a) f [[Char]] -> ([[Char]] -> AgdaLibFile) -> f AgdaLibFile
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ [[Char]]
    x -> AgdaLibFile
    a { _libIncludes = x }

    libDepends :: Lens' AgdaLibFile [LibName]
    libDepends :: Lens' AgdaLibFile [LibName]
    libDepends [LibName] -> f [LibName]
    f AgdaLibFile
    a = [LibName] -> f [LibName]
    f (AgdaLibFile -> [LibName]
    _libDepends AgdaLibFile
    a) f [LibName] -> ([LibName] -> AgdaLibFile) -> f AgdaLibFile
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ [LibName]
    x -> AgdaLibFile
    a { _libDepends = x }

    libPragmas :: Lens' AgdaLibFile OptionsPragma
    libPragmas :: Lens' AgdaLibFile OptionsPragma
    libPragmas OptionsPragma -> f OptionsPragma
    f AgdaLibFile
    a = OptionsPragma -> f OptionsPragma
    f (AgdaLibFile -> OptionsPragma
    _libPragmas AgdaLibFile
    a) f OptionsPragma -> (OptionsPragma -> AgdaLibFile) -> f AgdaLibFile
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ OptionsPragma
    x -> AgdaLibFile
    a { _libPragmas = x }

    ------------------------------------------------------------------------
    -- * Library warnings and errors
    ------------------------------------------------------------------------

    -- ** Position information

    type LineNumber = Int

    -- | Information about which @.agda-lib@ file we are reading
    --   and from where in the @libraries@ file it came from.

    data LibPositionInfo = LibPositionInfo
      { LibPositionInfo -> Maybe [Char]
    libFilePos :: Maybe FilePath -- ^ Name of @libraries@ file.
      , LibPositionInfo -> LineNumber
    lineNumPos :: LineNumber     -- ^ Line number in @libraries@ file.
      , LibPositionInfo -> [Char]
    filePos    :: FilePath       -- ^ Library file.
      }
      deriving (LineNumber -> LibPositionInfo -> ShowS
    [LibPositionInfo] -> ShowS
    LibPositionInfo -> [Char]
    (LineNumber -> LibPositionInfo -> ShowS)
    -> (LibPositionInfo -> [Char])
    -> ([LibPositionInfo] -> ShowS)
    -> Show LibPositionInfo
    forall a.
    (LineNumber -> a -> ShowS)
    -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: LineNumber -> LibPositionInfo -> ShowS
    showsPrec :: LineNumber -> LibPositionInfo -> ShowS
    $cshow :: LibPositionInfo -> [Char]
    show :: LibPositionInfo -> [Char]
    $cshowList :: [LibPositionInfo] -> ShowS
    showList :: [LibPositionInfo] -> ShowS
    Show, (forall x. LibPositionInfo -> Rep LibPositionInfo x)
    -> (forall x. Rep LibPositionInfo x -> LibPositionInfo)
    -> Generic LibPositionInfo
    forall x. Rep LibPositionInfo x -> LibPositionInfo
    forall x. LibPositionInfo -> Rep LibPositionInfo x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. LibPositionInfo -> Rep LibPositionInfo x
    from :: forall x. LibPositionInfo -> Rep LibPositionInfo x
    $cto :: forall x. Rep LibPositionInfo x -> LibPositionInfo
    to :: forall x. Rep LibPositionInfo x -> LibPositionInfo
    Generic)

    -- ** Warnings

    data LibWarning = LibWarning (Maybe LibPositionInfo) LibWarning'
      deriving (LineNumber -> LibWarning -> ShowS
    [LibWarning] -> ShowS
    LibWarning -> [Char]
    (LineNumber -> LibWarning -> ShowS)
    -> (LibWarning -> [Char])
    -> ([LibWarning] -> ShowS)
    -> Show LibWarning
    forall a.
    (LineNumber -> a -> ShowS)
    -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: LineNumber -> LibWarning -> ShowS
    showsPrec :: LineNumber -> LibWarning -> ShowS
    $cshow :: LibWarning -> [Char]
    show :: LibWarning -> [Char]
    $cshowList :: [LibWarning] -> ShowS
    showList :: [LibWarning] -> ShowS
    Show, (forall x. LibWarning -> Rep LibWarning x)
    -> (forall x. Rep LibWarning x -> LibWarning) -> Generic LibWarning
    forall x. Rep LibWarning x -> LibWarning
    forall x. LibWarning -> Rep LibWarning x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. LibWarning -> Rep LibWarning x
    from :: forall x. LibWarning -> Rep LibWarning x
    $cto :: forall x. Rep LibWarning x -> LibWarning
    to :: forall x. Rep LibWarning x -> LibWarning
    Generic)

    -- | Library Warnings.
    data LibWarning'
      = UnknownField String
      deriving (LineNumber -> LibWarning' -> ShowS
    [LibWarning'] -> ShowS
    LibWarning' -> [Char]
    (LineNumber -> LibWarning' -> ShowS)
    -> (LibWarning' -> [Char])
    -> ([LibWarning'] -> ShowS)
    -> Show LibWarning'
    forall a.
    (LineNumber -> a -> ShowS)
    -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: LineNumber -> LibWarning' -> ShowS
    showsPrec :: LineNumber -> LibWarning' -> ShowS
    $cshow :: LibWarning' -> [Char]
    show :: LibWarning' -> [Char]
    $cshowList :: [LibWarning'] -> ShowS
    showList :: [LibWarning'] -> ShowS
    Show, (forall x. LibWarning' -> Rep LibWarning' x)
    -> (forall x. Rep LibWarning' x -> LibWarning')
    -> Generic LibWarning'
    forall x. Rep LibWarning' x -> LibWarning'
    forall x. LibWarning' -> Rep LibWarning' x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. LibWarning' -> Rep LibWarning' x
    from :: forall x. LibWarning' -> Rep LibWarning' x
    $cto :: forall x. Rep LibWarning' x -> LibWarning'
    to :: forall x. Rep LibWarning' x -> LibWarning'
    Generic)

    libraryWarningName :: LibWarning -> WarningName
    libraryWarningName :: LibWarning -> WarningName
    libraryWarningName (LibWarning Maybe LibPositionInfo
    c (UnknownField{})) = WarningName
    LibUnknownField_

    -- * Errors

    data LibError = LibError (Maybe LibPositionInfo) LibError'
      deriving (LineNumber -> LibError -> ShowS
    [LibError] -> ShowS
    LibError -> [Char]
    (LineNumber -> LibError -> ShowS)
    -> (LibError -> [Char]) -> ([LibError] -> ShowS) -> Show LibError
    forall a.
    (LineNumber -> a -> ShowS)
    -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: LineNumber -> LibError -> ShowS
    showsPrec :: LineNumber -> LibError -> ShowS
    $cshow :: LibError -> [Char]
    show :: LibError -> [Char]
    $cshowList :: [LibError] -> ShowS
    showList :: [LibError] -> ShowS
    Show, (forall x. LibError -> Rep LibError x)
    -> (forall x. Rep LibError x -> LibError) -> Generic LibError
    forall x. Rep LibError x -> LibError
    forall x. LibError -> Rep LibError x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. LibError -> Rep LibError x
    from :: forall x. LibError -> Rep LibError x
    $cto :: forall x. Rep LibError x -> LibError
    to :: forall x. Rep LibError x -> LibError
    Generic)

    -- | Collected errors while processing library files.
    --
    data LibError'
      = LibrariesFileNotFound FilePath
          -- ^ The user specified replacement for the default @libraries@ file does not exist.
      | LibNotFound LibrariesFile LibName
          -- ^ Raised when a library name could not successfully be resolved
          --   to an @.agda-lib@ file.
          --
      | AmbiguousLib LibName (List2 AgdaLibFile)
          -- ^ Raised when a library name is defined in several @.agda-lib files@.
      | SeveralAgdaLibFiles FilePath (List2 FilePath)
          -- ^ The given project root contains more than one @.agda-lib@ file.
      | LibParseError LibParseError
          -- ^ The @.agda-lib@ file could not be parsed.
      | ReadError
          -- ^ An I/O Error occurred when reading a file.
          E.IOException
            -- ^ The caught exception
          String
            -- ^ Explanation when this error occurred.
      | DuplicateExecutable
          -- ^ The @executables@ file contains duplicate entries.
          FilePath
            -- ^ Name of the @executables@ file.
          Text
            -- ^ Name of the executable that is defined twice.
          (List2 (LineNumber, FilePath))
            -- ^ The resolutions of the executable.
      deriving (LineNumber -> LibError' -> ShowS
    [LibError'] -> ShowS
    LibError' -> [Char]
    (LineNumber -> LibError' -> ShowS)
    -> (LibError' -> [Char])
    -> ([LibError'] -> ShowS)
    -> Show LibError'
    forall a.
    (LineNumber -> a -> ShowS)
    -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: LineNumber -> LibError' -> ShowS
    showsPrec :: LineNumber -> LibError' -> ShowS
    $cshow :: LibError' -> [Char]
    show :: LibError' -> [Char]
    $cshowList :: [LibError'] -> ShowS
    showList :: [LibError'] -> ShowS
    Show, (forall x. LibError' -> Rep LibError' x)
    -> (forall x. Rep LibError' x -> LibError') -> Generic LibError'
    forall x. Rep LibError' x -> LibError'
    forall x. LibError' -> Rep LibError' x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. LibError' -> Rep LibError' x
    from :: forall x. LibError' -> Rep LibError' x
    $cto :: forall x. Rep LibError' x -> LibError'
    to :: forall x. Rep LibError' x -> LibError'
    Generic)

    -- | Exceptions thrown by the @.agda-lib@ parser.
    --
    data LibParseError
      = BadLibraryName String
          -- ^ An invalid library name, e.g., containing spaces.
      | ReadFailure FilePath E.IOException
          -- ^ I/O error while reading file.
      | MissingFields (List1 String)
          -- ^ Missing these mandatory fields.
      | DuplicateFields (List1 String)
          -- ^ These fields occur each more than once.
      | MissingFieldName LineNumber
          -- ^ At the given line number, a field name is missing before the @:@.
      | BadFieldName LineNumber String
          -- ^ At the given line number, an invalid field name is encountered before the @:@.
          --   (E.g., containing spaces.)
      | MissingColonForField LineNumber String
          -- ^ At the given line number, the given field is not followed by @:@.
      | ContentWithoutField LineNumber
          -- ^ At the given line number, indented text (content) is not preceded by a field.
      deriving (LineNumber -> LibParseError -> ShowS
    [LibParseError] -> ShowS
    LibParseError -> [Char]
    (LineNumber -> LibParseError -> ShowS)
    -> (LibParseError -> [Char])
    -> ([LibParseError] -> ShowS)
    -> Show LibParseError
    forall a.
    (LineNumber -> a -> ShowS)
    -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: LineNumber -> LibParseError -> ShowS
    showsPrec :: LineNumber -> LibParseError -> ShowS
    $cshow :: LibParseError -> [Char]
    show :: LibParseError -> [Char]
    $cshowList :: [LibParseError] -> ShowS
    showList :: [LibParseError] -> ShowS
    Show, (forall x. LibParseError -> Rep LibParseError x)
    -> (forall x. Rep LibParseError x -> LibParseError)
    -> Generic LibParseError
    forall x. Rep LibParseError x -> LibParseError
    forall x. LibParseError -> Rep LibParseError x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. LibParseError -> Rep LibParseError x
    from :: forall x. LibParseError -> Rep LibParseError x
    $cto :: forall x. Rep LibParseError x -> LibParseError
    to :: forall x. Rep LibParseError x -> LibParseError
    Generic)

    -- ** Raising warnings and errors

    -- | Collection of 'LibError's and 'LibWarning's.
    --
    type LibErrWarns = [Either LibError LibWarning]

    warnings :: MonadWriter LibErrWarns m => List1 LibWarning -> m ()
    warnings :: forall (m :: * -> *).
    MonadWriter LibErrWarns m =>
    List1 LibWarning -> m ()
    warnings = LibErrWarns -> m ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell (LibErrWarns -> m ())
    -> (List1 LibWarning -> LibErrWarns) -> List1 LibWarning -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (LibWarning -> Either LibError LibWarning)
    -> [LibWarning] -> LibErrWarns
    forall a b. (a -> b) -> [a] -> [b]
    map LibWarning -> Either LibError LibWarning
    forall a b. b -> Either a b
    Right ([LibWarning] -> LibErrWarns)
    -> (List1 LibWarning -> [LibWarning])
    -> List1 LibWarning
    -> LibErrWarns
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 LibWarning -> [Item (List1 LibWarning)]
    List1 LibWarning -> [LibWarning]
    forall l. IsList l => l -> [Item l]
    toList

    warnings' :: MonadWriter LibErrWarns m => List1 LibWarning' -> m ()
    warnings' :: forall (m :: * -> *).
    MonadWriter LibErrWarns m =>
    List1 LibWarning' -> m ()
    warnings' = LibErrWarns -> m ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell (LibErrWarns -> m ())
    -> (List1 LibWarning' -> LibErrWarns) -> List1 LibWarning' -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (LibWarning' -> Either LibError LibWarning)
    -> [LibWarning'] -> LibErrWarns
    forall a b. (a -> b) -> [a] -> [b]
    map (LibWarning -> Either LibError LibWarning
    forall a b. b -> Either a b
    Right (LibWarning -> Either LibError LibWarning)
    -> (LibWarning' -> LibWarning)
    -> LibWarning'
    -> Either LibError LibWarning
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe LibPositionInfo -> LibWarning' -> LibWarning
    LibWarning Maybe LibPositionInfo
    forall a. Maybe a
    Nothing) ([LibWarning'] -> LibErrWarns)
    -> (List1 LibWarning' -> [LibWarning'])
    -> List1 LibWarning'
    -> LibErrWarns
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 LibWarning' -> [Item (List1 LibWarning')]
    List1 LibWarning' -> [LibWarning']
    forall l. IsList l => l -> [Item l]
    toList

    raiseErrors' :: MonadWriter LibErrWarns m => List1 LibError' -> m ()
    raiseErrors' :: forall (m :: * -> *).
    MonadWriter LibErrWarns m =>
    List1 LibError' -> m ()
    raiseErrors' = LibErrWarns -> m ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell (LibErrWarns -> m ())
    -> (List1 LibError' -> LibErrWarns) -> List1 LibError' -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (LibError' -> Either LibError LibWarning)
    -> [LibError'] -> LibErrWarns
    forall a b. (a -> b) -> [a] -> [b]
    map (LibError -> Either LibError LibWarning
    forall a b. a -> Either a b
    Left (LibError -> Either LibError LibWarning)
    -> (LibError' -> LibError)
    -> LibError'
    -> Either LibError LibWarning
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Maybe LibPositionInfo -> LibError' -> LibError
    LibError Maybe LibPositionInfo
    forall a. Maybe a
    Nothing)) ([LibError'] -> LibErrWarns)
    -> (List1 LibError' -> [LibError'])
    -> List1 LibError'
    -> LibErrWarns
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 LibError' -> [Item (List1 LibError')]
    List1 LibError' -> [LibError']
    forall l. IsList l => l -> [Item l]
    toList

    raiseErrors :: MonadWriter LibErrWarns m => List1 LibError -> m ()
    raiseErrors :: forall (m :: * -> *).
    MonadWriter LibErrWarns m =>
    List1 LibError -> m ()
    raiseErrors = LibErrWarns -> m ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell (LibErrWarns -> m ())
    -> (List1 LibError -> LibErrWarns) -> List1 LibError -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (LibError -> Either LibError LibWarning)
    -> [LibError] -> LibErrWarns
    forall a b. (a -> b) -> [a] -> [b]
    map LibError -> Either LibError LibWarning
    forall a b. a -> Either a b
    Left ([LibError] -> LibErrWarns)
    -> (List1 LibError -> [LibError]) -> List1 LibError -> LibErrWarns
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 LibError -> [Item (List1 LibError)]
    List1 LibError -> [LibError]
    forall l. IsList l => l -> [Item l]
    toList

    ------------------------------------------------------------------------
    -- * Library Monad
    ------------------------------------------------------------------------

    -- | Collects 'LibError's and 'LibWarning's.
    --
    type LibErrorIO = WriterT LibErrWarns (StateT LibState IO)

    -- | Throws 'LibErrors' exceptions, still collects 'LibWarning's.
    type LibM = ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO))

    type LibState = LibCache

    -- | Cache locations of project configurations and parsed @.agda-lib@ files.
    data LibCache = LibCache
      { LibCache -> Map [Char] ProjectConfig
    projectConfigs :: !(Map FilePath ProjectConfig)
          -- ^ Map from directories to paths of closest enclosing @.agda-lib@
          --   files (or 'DefaultProjectConfig' if there are none).
      , LibCache -> Map [Char] AgdaLibFile
    agdaLibFiles   :: !(Map FilePath AgdaLibFile)
          -- ^ Contents of @.agda-lib@ files that have already been parsed.
      }
      deriving ((forall x. LibCache -> Rep LibCache x)
    -> (forall x. Rep LibCache x -> LibCache) -> Generic LibCache
    forall x. Rep LibCache x -> LibCache
    forall x. LibCache -> Rep LibCache x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. LibCache -> Rep LibCache x
    from :: forall x. LibCache -> Rep LibCache x
    $cto :: forall x. Rep LibCache x -> LibCache
    to :: forall x. Rep LibCache x -> LibCache
    Generic)

    -- | Collected errors when processing an @.agda-lib@ file.
    --
    data LibErrors = LibErrors
      { LibErrors -> [AgdaLibFile]
    libErrorsInstalledLibraries :: [AgdaLibFile]
      , LibErrors -> List1 LibError
    libErrors                   :: List1 LibError
      } deriving (LineNumber -> LibErrors -> ShowS
    [LibErrors] -> ShowS
    LibErrors -> [Char]
    (LineNumber -> LibErrors -> ShowS)
    -> (LibErrors -> [Char])
    -> ([LibErrors] -> ShowS)
    -> Show LibErrors
    forall a.
    (LineNumber -> a -> ShowS)
    -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: LineNumber -> LibErrors -> ShowS
    showsPrec :: LineNumber -> LibErrors -> ShowS
    $cshow :: LibErrors -> [Char]
    show :: LibErrors -> [Char]
    $cshowList :: [LibErrors] -> ShowS
    showList :: [LibErrors] -> ShowS
    Show, (forall x. LibErrors -> Rep LibErrors x)
    -> (forall x. Rep LibErrors x -> LibErrors) -> Generic LibErrors
    forall x. Rep LibErrors x -> LibErrors
    forall x. LibErrors -> Rep LibErrors x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. LibErrors -> Rep LibErrors x
    from :: forall x. LibErrors -> Rep LibErrors x
    $cto :: forall x. Rep LibErrors x -> LibErrors
    to :: forall x. Rep LibErrors x -> LibErrors
    Generic)

    runLibM :: LibM a -> LibState -> IO ((Either LibErrors a, [LibWarning]), LibState)
    runLibM :: forall a.
    LibM a
    -> LibCache -> IO ((Either LibErrors a, [LibWarning]), LibCache)
    runLibM LibM a
    m LibCache
    s = LibM a
    m LibM a
    -> (LibM a
        -> WriterT [LibWarning] (StateT LibCache IO) (Either LibErrors a))
    -> WriterT [LibWarning] (StateT LibCache IO) (Either LibErrors a)
    forall a b. a -> (a -> b) -> b
    & LibM a
    -> WriterT [LibWarning] (StateT LibCache IO) (Either LibErrors a)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT WriterT [LibWarning] (StateT LibCache IO) (Either LibErrors a)
    -> (WriterT [LibWarning] (StateT LibCache IO) (Either LibErrors a)
        -> StateT LibCache IO (Either LibErrors a, [LibWarning]))
    -> StateT LibCache IO (Either LibErrors a, [LibWarning])
    forall a b. a -> (a -> b) -> b
    & WriterT [LibWarning] (StateT LibCache IO) (Either LibErrors a)
    -> StateT LibCache IO (Either LibErrors a, [LibWarning])
    forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
    runWriterT StateT LibCache IO (Either LibErrors a, [LibWarning])
    -> (StateT LibCache IO (Either LibErrors a, [LibWarning])
        -> IO ((Either LibErrors a, [LibWarning]), LibCache))
    -> IO ((Either LibErrors a, [LibWarning]), LibCache)
    forall a b. a -> (a -> b) -> b
    & (StateT LibCache IO (Either LibErrors a, [LibWarning])
    -> LibCache -> IO ((Either LibErrors a, [LibWarning]), LibCache)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    `runStateT` LibCache
    s)

    getCachedProjectConfig
      :: (MonadState LibState m, MonadIO m)
      => FilePath -> m (Maybe ProjectConfig)
    getCachedProjectConfig :: forall (m :: * -> *).
    (MonadState LibCache m, MonadIO m) =>
    [Char] -> m (Maybe ProjectConfig)
    getCachedProjectConfig [Char]
    path = do
      path <- IO [Char] -> m [Char]
    forall a. IO a -> m a
    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 [Char]
    canonicalizePath [Char]
    path
      Map.lookup path <$> gets projectConfigs

    storeCachedProjectConfig
      :: (MonadState LibState m, MonadIO m)
      => FilePath -> ProjectConfig -> m ()
    storeCachedProjectConfig :: forall (m :: * -> *).
    (MonadState LibCache m, MonadIO m) =>
    [Char] -> ProjectConfig -> m ()
    storeCachedProjectConfig [Char]
    path ProjectConfig
    conf = do
      path <- IO [Char] -> m [Char]
    forall a. IO a -> m a
    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 [Char]
    canonicalizePath [Char]
    path
      modify \ LibCache
    s -> LibCache
    s { projectConfigs = Map.insert path conf $ projectConfigs s }

    getCachedAgdaLibFile
      :: (MonadState LibState m, MonadIO m)
      => FilePath -> m (Maybe AgdaLibFile)
    getCachedAgdaLibFile :: forall (m :: * -> *).
    (MonadState LibCache m, MonadIO m) =>
    [Char] -> m (Maybe AgdaLibFile)
    getCachedAgdaLibFile [Char]
    path = do
      path <- IO [Char] -> m [Char]
    forall a. IO a -> m a
    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 [Char]
    canonicalizePath [Char]
    path
      Map.lookup path <$> gets agdaLibFiles

    storeCachedAgdaLibFile
      :: (MonadState LibState m, MonadIO m)
      => FilePath -> AgdaLibFile -> m ()
    storeCachedAgdaLibFile :: forall (m :: * -> *).
    (MonadState LibCache m, MonadIO m) =>
    [Char] -> AgdaLibFile -> m ()
    storeCachedAgdaLibFile [Char]
    path AgdaLibFile
    lib = do
      path <- IO [Char] -> m [Char]
    forall a. IO a -> m a
    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 [Char]
    canonicalizePath [Char]
    path
      modify \ LibCache
    s -> LibCache
    s { agdaLibFiles = Map.insert path lib $ agdaLibFiles s }

    ------------------------------------------------------------------------
    -- * Prettyprinting errors and warnings
    ------------------------------------------------------------------------

    -- | Pretty-print 'LibError'.
    formatLibError :: [AgdaLibFile] -> LibError -> Doc
    formatLibError :: [AgdaLibFile] -> LibError -> Doc
    formatLibError [AgdaLibFile]
    installed (LibError Maybe LibPositionInfo
    mc LibError'
    e) =
      case (Maybe LibPositionInfo
    mc, LibError'
    e) of
        (Just LibPositionInfo
    c, LibParseError LibParseError
    err) -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep  [ LibPositionInfo -> LibParseError -> Doc
    formatLibPositionInfo LibPositionInfo
    c LibParseError
    err, LibError' -> Doc
    forall a. Pretty a => a -> Doc
    pretty LibError'
    e ]
        (Maybe LibPositionInfo
    _     , LibNotFound{}    ) -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat [ LibError' -> Doc
    forall a. Pretty a => a -> Doc
    pretty LibError'
    e, [AgdaLibFile] -> Doc
    prettyInstalledLibraries [AgdaLibFile]
    installed ]
        (Maybe LibPositionInfo, LibError')
    _ -> LibError' -> Doc
    forall a. Pretty a => a -> Doc
    pretty LibError'
    e

    -- | Pretty-print 'LibErrors'.
    formatLibErrors :: LibErrors -> Doc
    formatLibErrors :: LibErrors -> Doc
    formatLibErrors (LibErrors [AgdaLibFile]
    libs List1 LibError
    errs) =
      [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] -> [Doc]) -> [LibError] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ List1 LibError -> [Item (List1 LibError)]
    forall l. IsList l => l -> [Item l]
    List1.toList List1 LibError
    errs

    -- | Does a parse error contain a line number?
    hasLineNumber :: LibParseError -> Maybe LineNumber
    hasLineNumber :: LibParseError -> Maybe LineNumber
    hasLineNumber = \case
      BadLibraryName       [Char]
    _   -> Maybe LineNumber
    forall a. Maybe a
    Nothing
      ReadFailure          [Char]
    _ IOException
    _ -> Maybe LineNumber
    forall a. Maybe a
    Nothing
      MissingFields        List1 [Char]
    _   -> Maybe LineNumber
    forall a. Maybe a
    Nothing
      DuplicateFields      List1 [Char]
    _   -> Maybe LineNumber
    forall a. Maybe a
    Nothing
      MissingFieldName     LineNumber
    l   -> LineNumber -> Maybe LineNumber
    forall a. a -> Maybe a
    Just LineNumber
    l
      BadFieldName         LineNumber
    l [Char]
    _ -> LineNumber -> Maybe LineNumber
    forall a. a -> Maybe a
    Just LineNumber
    l
      MissingColonForField LineNumber
    l [Char]
    _ -> LineNumber -> Maybe LineNumber
    forall a. a -> Maybe a
    Just LineNumber
    l
      ContentWithoutField  LineNumber
    l   -> LineNumber -> Maybe LineNumber
    forall a. a -> Maybe a
    Just LineNumber
    l

    -- UNUSED:
    -- -- | Does a parse error contain the name of the parsed file?
    -- hasFilePath :: LibParseError -> Maybe FilePath
    -- hasFilePath = \case
    --   BadLibraryName       _   -> Nothing
    --   ReadFailure          f _ -> Just f
    --   MissingFields        _   -> Nothing
    --   DuplicateFields      _   -> Nothing
    --   MissingFieldName     _   -> Nothing
    --   BadFieldName         _ _ -> Nothing
    --   MissingColonForField _ _ -> Nothing
    --   ContentWithoutField  _   -> Nothing

    -- | Compute a position position prefix.
    --
    --   Depending on the error to be printed, it will
    --
    --   - either give the name of the @libraries@ file and a line inside it,
    --
    --   - or give the name of the @.agda-lib@ file.
    --
    formatLibPositionInfo :: LibPositionInfo -> LibParseError -> Doc
    formatLibPositionInfo :: LibPositionInfo -> LibParseError -> Doc
    formatLibPositionInfo (LibPositionInfo Maybe [Char]
    libFile LineNumber
    lineNum [Char]
    file) = \case

      -- If we couldn't even read the @.agda-lib@ file, report error in the @libraries@ file.
      ReadFailure [Char]
    _ IOException
    _
        | Just [Char]
    lf <- Maybe [Char]
    libFile
          -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hcat [ [Char] -> Doc
    forall a. [Char] -> Doc a
    text [Char]
    lf, Doc
    ":", LineNumber -> Doc
    forall a. Pretty a => a -> Doc
    pretty LineNumber
    lineNum, Doc
    ":" ]
        | Bool
    otherwise
          -> Doc
    forall a. Null a => a
    empty

      -- If the parse error comes with a line number, print it here.
      LibParseError
    e | Just LineNumber
    l <- LibParseError -> Maybe LineNumber
    hasLineNumber LibParseError
    e
          -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hcat [ [Char] -> Doc
    forall a. [Char] -> Doc a
    text [Char]
    file, Doc
    ":", LineNumber -> Doc
    forall a. Pretty a => a -> Doc
    pretty LineNumber
    l, Doc
    ":" ]
        | Bool
    otherwise
          -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hcat [ [Char] -> Doc
    forall a. [Char] -> Doc a
    text [Char]
    file, Doc
    ":" ]

    prettyInstalledLibraries :: [AgdaLibFile] -> Doc
    prettyInstalledLibraries :: [AgdaLibFile] -> Doc
    prettyInstalledLibraries [AgdaLibFile]
    installed =
      [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Doc
    "Installed libraries:" Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    :) ([Doc] -> [Doc]) -> [Doc] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $
        (Doc -> Doc) -> [Doc] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (LineNumber -> Doc -> Doc
    forall a. LineNumber -> Doc a -> Doc a
    nest LineNumber
    2) ([Doc] -> [Doc]) -> [Doc] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $
        if [AgdaLibFile] -> Bool
    forall a. Null a => a -> Bool
    null [AgdaLibFile]
    installed then [Doc
    "(none)"]
        else [ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ LibName -> Doc
    forall a. Pretty a => a -> Doc
    pretty (LibName -> Doc) -> LibName -> Doc
    forall a b. (a -> b) -> a -> b
    $ AgdaLibFile -> LibName
    _libName AgdaLibFile
    l, LineNumber -> Doc -> Doc
    forall a. LineNumber -> Doc a -> Doc a
    nest LineNumber
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> Doc
    parens (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Doc
    forall a. [Char] -> Doc a
    text ([Char] -> Doc) -> [Char] -> Doc
    forall a b. (a -> b) -> a -> b
    $ AgdaLibFile -> [Char]
    _libFile AgdaLibFile
    l ]
             | AgdaLibFile
    l <- [AgdaLibFile]
    installed
             ]

    -- | Pretty-print library management error without position info.

    instance Pretty LibError' where
      pretty :: LibError' -> Doc
    pretty = \case

        LibrariesFileNotFound [Char]
    path -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep
          [ [Char] -> Doc
    forall a. [Char] -> Doc a
    text [Char]
    "Libraries file not found:"
          , [Char] -> Doc
    forall a. [Char] -> Doc a
    text [Char]
    path
          ]

        LibNotFound LibrariesFile
    file LibName
    lib -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          [ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hcat [ Doc
    "Library '", LibName -> Doc
    forall a. Pretty a => a -> Doc
    pretty LibName
    lib, Doc
    "' not found." ]
          , [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Doc
    "Add the path to its .agda-lib file to"
                , LineNumber -> Doc -> Doc
    forall a. LineNumber -> Doc a -> Doc a
    nest LineNumber
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Doc
    forall a. [Char] -> Doc a
    text ([Char] -> Doc) -> [Char] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "'" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ LibrariesFile -> [Char]
    lfPath LibrariesFile
    file [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "'"
                , Doc
    "to install."
                ]
          ]

        AmbiguousLib LibName
    lib List2 AgdaLibFile
    tgts -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hcat [ Doc
    "Ambiguous library '", LibName -> Doc
    forall a. Pretty a => a -> Doc
    pretty LibName
    lib, Doc
    "'." ]
                , Doc
    "Could refer to any one of"
              ]
            Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : [ LineNumber -> Doc -> Doc
    forall a. LineNumber -> Doc a -> Doc a
    nest LineNumber
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ LibName -> Doc
    forall a. Pretty a => a -> Doc
    pretty (AgdaLibFile -> LibName
    _libName AgdaLibFile
    l) Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc -> Doc
    parens ([Char] -> Doc
    forall a. [Char] -> Doc a
    text ([Char] -> Doc) -> [Char] -> Doc
    forall a b. (a -> b) -> a -> b
    $ AgdaLibFile -> [Char]
    _libFile AgdaLibFile
    l) | AgdaLibFile
    l <- List2 AgdaLibFile -> [Item (List2 AgdaLibFile)]
    forall l. IsList l => l -> [Item l]
    toList List2 AgdaLibFile
    tgts ]

        SeveralAgdaLibFiles [Char]
    root List2 [Char]
    files -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Doc
    "The project root", [Char] -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Char]
    root ]
            Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : Doc
    "may contain only one .agda-lib file, but I found several:"
            Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : ([Char] -> Doc) -> [[Char]] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Doc
    "-" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+>) (Doc -> Doc) -> ([Char] -> Doc) -> [Char] -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> Doc
    forall a. Pretty a => a -> Doc
    pretty) ([[Char]] -> [[Char]]
    forall a. Ord a => [a] -> [a]
    List.sort ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
    forall a b. (a -> b) -> a -> b
    $ List2 [Char] -> [Item (List2 [Char])]
    forall l. IsList l => l -> [Item l]
    toList List2 [Char]
    files)

        LibParseError LibParseError
    err -> LibParseError -> Doc
    forall a. Pretty a => a -> Doc
    pretty LibParseError
    err

        ReadError IOException
    e [Char]
    msg -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat
          [ [Char] -> Doc
    forall a. [Char] -> Doc a
    text ([Char] -> Doc) -> [Char] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    msg
          , [Char] -> Doc
    forall a. [Char] -> Doc a
    text ([Char] -> Doc) -> [Char] -> Doc
    forall a b. (a -> b) -> a -> b
    $ IOException -> [Char]
    forall e. Exception e => e -> [Char]
    showIOException IOException
    e
          ]

        DuplicateExecutable [Char]
    exeFile Text
    exe List2 (LineNumber, [Char])
    paths -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hcat [ Doc
    "Duplicate entries for executable '", ([Char] -> Doc
    forall a. [Char] -> Doc a
    text ([Char] -> Doc) -> (Text -> [Char]) -> Text -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Text -> [Char]
    unpack) Text
    exe, Doc
    "' in ", [Char] -> Doc
    forall a. [Char] -> Doc a
    text [Char]
    exeFile, Doc
    ":" ] Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    :
          ((LineNumber, [Char]) -> Doc) -> [(LineNumber, [Char])] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (\ (LineNumber
    ln, [Char]
    fp) -> LineNumber -> Doc -> Doc
    forall a. LineNumber -> Doc a -> Doc a
    nest LineNumber
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ (LineNumber -> Doc
    forall a. Pretty a => a -> Doc
    pretty LineNumber
    ln Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    colon) Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> [Char] -> Doc
    forall a. [Char] -> Doc a
    text [Char]
    fp) (List2 (LineNumber, [Char]) -> [Item (List2 (LineNumber, [Char]))]
    forall l. IsList l => l -> [Item l]
    toList List2 (LineNumber, [Char])
    paths)

    -- | Print library file parse error without position info.
    --
    instance Pretty LibParseError where
      pretty :: LibParseError -> Doc
    pretty = \case

        BadLibraryName [Char]
    s -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep
          [ Doc
    "Bad library name:", Doc -> Doc
    quotes ([Char] -> Doc
    forall a. [Char] -> Doc a
    text [Char]
    s) ]
        ReadFailure [Char]
    file IOException
    e -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat
          [ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep [ Doc
    "Failed to read library file", [Char] -> Doc
    forall a. [Char] -> Doc a
    text [Char]
    file Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    "." ]
          , Doc
    "Reason:" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> [Char] -> Doc
    forall a. [Char] -> Doc a
    text (IOException -> [Char]
    forall e. Exception e => e -> [Char]
    showIOException IOException
    e)
          ]

        MissingFields   List1 [Char]
    xs -> Doc
    "Missing"   Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> List1 [Char] -> Doc
    listFields List1 [Char]
    xs
        DuplicateFields List1 [Char]
    xs -> Doc
    "Duplicate" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> List1 [Char] -> Doc
    listFields List1 [Char]
    xs

        MissingFieldName     LineNumber
    l   -> LineNumber -> Doc -> Doc
    forall {p} {a}. p -> a -> a
    atLine LineNumber
    l (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "Missing field name"
        BadFieldName         LineNumber
    l [Char]
    s -> LineNumber -> Doc -> Doc
    forall {p} {a}. p -> a -> a
    atLine LineNumber
    l (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "Bad field name" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> [Char] -> Doc
    forall a. [Char] -> Doc a
    text (ShowS
    forall a. Show a => a -> [Char]
    show [Char]
    s)
        MissingColonForField LineNumber
    l [Char]
    s -> LineNumber -> Doc -> Doc
    forall {p} {a}. p -> a -> a
    atLine LineNumber
    l (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "Missing ':' for field " Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> [Char] -> Doc
    forall a. [Char] -> Doc a
    text (ShowS
    forall a. Show a => a -> [Char]
    show [Char]
    s)
        ContentWithoutField  LineNumber
    l   -> LineNumber -> Doc -> Doc
    forall {p} {a}. p -> a -> a
    atLine LineNumber
    l (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "Missing field"

        where
        listFields :: List1 [Char] -> Doc
    listFields List1 [Char]
    xs = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ List1 [Char] -> Doc
    forall {a} {c}. (Sized a, IsString c) => a -> c
    fieldS List1 [Char]
    xs Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : List1 [Char] -> [Doc]
    list List1 [Char]
    xs
        fieldS :: a -> c
    fieldS a
    xs     = a -> c -> c -> c
    forall a c. Sized a => a -> c -> c -> c
    singPlural a
    xs c
    "field:" c
    "fields:"
        list :: List1 [Char] -> [Doc]
    list          = Doc -> [Doc] -> [Doc]
    forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
    punctuate Doc
    comma ([Doc] -> [Doc])
    -> (List1 [Char] -> [Doc]) -> List1 [Char] -> [Doc]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([Char] -> Doc) -> [[Char]] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Doc -> Doc
    quotes (Doc -> Doc) -> ([Char] -> Doc) -> [Char] -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> Doc
    forall a. [Char] -> Doc a
    text) ([[Char]] -> [Doc])
    -> (List1 [Char] -> [[Char]]) -> List1 [Char] -> [Doc]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 [Char] -> [[Char]]
    List1 [Char] -> [Item (List1 [Char])]
    forall l. IsList l => l -> [Item l]
    toList
        atLine :: p -> a -> a
    atLine p
    l      = a -> a
    forall a. a -> a
    id
        -- The line number will be printed by 'formatLibPositionInfo'!
        -- atLine l doc  = hsep [ text (show l) <> ":", doc ]

    instance Pretty LibWarning where
      pretty :: LibWarning -> Doc
    pretty (LibWarning Maybe LibPositionInfo
    mc LibWarning'
    w) =
        case Maybe LibPositionInfo
    mc of
          Maybe LibPositionInfo
    Nothing -> LibWarning' -> Doc
    forall a. Pretty a => a -> Doc
    pretty LibWarning'
    w
          Just (LibPositionInfo Maybe [Char]
    _ LineNumber
    _ [Char]
    file) -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hcat [ [Char] -> Doc
    forall a. [Char] -> Doc a
    text [Char]
    file, Doc
    ":"] Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> LibWarning' -> Doc
    forall a. Pretty a => a -> Doc
    pretty LibWarning'
    w

    instance Pretty LibWarning' where
      pretty :: LibWarning' -> Doc
    pretty (UnknownField [Char]
    s) = [Char] -> Doc
    forall a. [Char] -> Doc a
    text ([Char] -> Doc) -> [Char] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Unknown field '" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    s [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "'"

    ------------------------------------------------------------------------
    -- Hashable instances
    ------------------------------------------------------------------------

    instance Hashable LibName

    ------------------------------------------------------------------------
    -- Null instances
    ------------------------------------------------------------------------

    instance Null LibName where
      empty :: LibName
    empty = Text -> [Integer] -> LibName
    LibName Text
    forall a. Null a => a
    empty [Integer]
    forall a. Null a => a
    empty
      null :: LibName -> Bool
    null (LibName Text
    a [Integer]
    b) = Text -> Bool
    forall a. Null a => a -> Bool
    null Text
    a Bool -> Bool -> Bool
    && [Integer] -> Bool
    forall a. Null a => a -> Bool
    null [Integer]
    b

    instance Null LibCache where
      empty :: LibCache
    empty = Map [Char] ProjectConfig -> Map [Char] AgdaLibFile -> LibCache
    LibCache Map [Char] ProjectConfig
    forall a. Null a => a
    empty Map [Char] AgdaLibFile
    forall a. Null a => a
    empty
      null :: LibCache -> Bool
    null (LibCache Map [Char] ProjectConfig
    a Map [Char] AgdaLibFile
    b) = Map [Char] ProjectConfig -> Bool
    forall a. Null a => a -> Bool
    null Map [Char] ProjectConfig
    a Bool -> Bool -> Bool
    && Map [Char] AgdaLibFile -> Bool
    forall a. Null a => a -> Bool
    null Map [Char] AgdaLibFile
    b

    ------------------------------------------------------------------------
    -- NFData instances
    ------------------------------------------------------------------------

    instance NFData ExecutablesFile
    instance NFData LibrariesFile
    instance NFData ProjectConfig
    instance NFData AgdaLibFile
    instance NFData LibName
    instance NFData LibCache
    instance NFData LibPositionInfo
    instance NFData LibWarning
    instance NFData LibWarning'
    instance NFData LibError
    instance NFData LibError'
    instance NFData LibErrors
    instance NFData LibParseError
    instance NFData E.IOException where rnf :: IOException -> ()
    rnf IOException
    _ = ()