    -- | Basic data types for library management.

    module Agda.Interaction.Library.Base where

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

    import Data.Char ( isDigit )
    import Data.Data ( Data )
    import qualified Data.List as List
    import Data.Map (Map)
    import qualified Data.Map as Map
    import Data.Text ( Text )

    import GHC.Generics (Generic)

    import System.Directory
    import System.FilePath

    import Agda.Interaction.Options.Warnings

    import Agda.Utils.FileName
    import Agda.Utils.Lens
    import Agda.Utils.Pretty

    -- | A symbolic library name.
    --
    type LibName = String

    data LibrariesFile = LibrariesFile
      { LibrariesFile -> String
    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 -> String
    (LineNumber -> LibrariesFile -> ShowS)
    -> (LibrariesFile -> String)
    -> ([LibrariesFile] -> ShowS)
    -> Show LibrariesFile
    forall a.
    (LineNumber -> a -> ShowS)
    -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [LibrariesFile] -> ShowS
    $cshowList :: [LibrariesFile] -> ShowS
    show :: LibrariesFile -> String
    $cshow :: LibrariesFile -> String
    showsPrec :: LineNumber -> LibrariesFile -> ShowS
    $cshowsPrec :: LineNumber -> LibrariesFile -> ShowS
    Show)

    -- | A symbolic executable name.
    --
    type ExeName = Text

    data ExecutablesFile = ExecutablesFile
      { ExecutablesFile -> String
    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 -> String
    (LineNumber -> ExecutablesFile -> ShowS)
    -> (ExecutablesFile -> String)
    -> ([ExecutablesFile] -> ShowS)
    -> Show ExecutablesFile
    forall a.
    (LineNumber -> a -> ShowS)
    -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [ExecutablesFile] -> ShowS
    $cshowList :: [ExecutablesFile] -> ShowS
    show :: ExecutablesFile -> String
    $cshow :: ExecutablesFile -> String
    showsPrec :: LineNumber -> ExecutablesFile -> ShowS
    $cshowsPrec :: LineNumber -> ExecutablesFile -> ShowS
    Show, Typeable ExecutablesFile
    Typeable ExecutablesFile
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> ExecutablesFile -> c ExecutablesFile)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c ExecutablesFile)
    -> (ExecutablesFile -> Constr)
    -> (ExecutablesFile -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c ExecutablesFile))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e))
        -> Maybe (c ExecutablesFile))
    -> ((forall b. Data b => b -> b)
        -> ExecutablesFile -> ExecutablesFile)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> ExecutablesFile -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> ExecutablesFile -> r)
    -> (forall u.
        (forall d. Data d => d -> u) -> ExecutablesFile -> [u])
    -> (forall u.
        LineNumber -> (forall d. Data d => d -> u) -> ExecutablesFile -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d)
        -> ExecutablesFile -> m ExecutablesFile)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d)
        -> ExecutablesFile -> m ExecutablesFile)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d)
        -> ExecutablesFile -> m ExecutablesFile)
    -> Data ExecutablesFile
    ExecutablesFile -> DataType
    ExecutablesFile -> Constr
    (forall b. Data b => b -> b) -> ExecutablesFile -> ExecutablesFile
    forall a.
    Typeable a
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. LineNumber -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u.
    LineNumber -> (forall d. Data d => d -> u) -> ExecutablesFile -> u
    forall u. (forall d. Data d => d -> u) -> ExecutablesFile -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ExecutablesFile -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ExecutablesFile -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> ExecutablesFile -> m ExecutablesFile
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> ExecutablesFile -> m ExecutablesFile
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ExecutablesFile
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> ExecutablesFile -> c ExecutablesFile
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ExecutablesFile)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c ExecutablesFile)
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> ExecutablesFile -> m ExecutablesFile
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> ExecutablesFile -> m ExecutablesFile
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> ExecutablesFile -> m ExecutablesFile
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> ExecutablesFile -> m ExecutablesFile
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> ExecutablesFile -> m ExecutablesFile
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> ExecutablesFile -> m ExecutablesFile
    gmapQi :: forall u.
    LineNumber -> (forall d. Data d => d -> u) -> ExecutablesFile -> u
    $cgmapQi :: forall u.
    LineNumber -> (forall d. Data d => d -> u) -> ExecutablesFile -> u
    gmapQ :: forall u. (forall d. Data d => d -> u) -> ExecutablesFile -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> ExecutablesFile -> [u]
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ExecutablesFile -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ExecutablesFile -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ExecutablesFile -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ExecutablesFile -> r
    gmapT :: (forall b. Data b => b -> b) -> ExecutablesFile -> ExecutablesFile
    $cgmapT :: (forall b. Data b => b -> b) -> ExecutablesFile -> ExecutablesFile
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c ExecutablesFile)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c ExecutablesFile)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ExecutablesFile)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ExecutablesFile)
    dataTypeOf :: ExecutablesFile -> DataType
    $cdataTypeOf :: ExecutablesFile -> DataType
    toConstr :: ExecutablesFile -> Constr
    $ctoConstr :: ExecutablesFile -> Constr
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ExecutablesFile
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ExecutablesFile
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> ExecutablesFile -> c ExecutablesFile
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> ExecutablesFile -> c ExecutablesFile
    Data, (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
    $cto :: forall x. Rep ExecutablesFile x -> ExecutablesFile
    $cfrom :: forall x. ExecutablesFile -> Rep ExecutablesFile x
    Generic)

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

    -- | A file can either belong to a project located at a given root
    --   containing one or more .agda-lib files, or be part of the default
    --   project.
    data ProjectConfig
      = ProjectConfig
        { ProjectConfig -> String
    configRoot         :: FilePath
        , ProjectConfig -> [String]
    configAgdaLibFiles :: [FilePath]
        }
      | 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
    $cto :: forall x. Rep ProjectConfig x -> ProjectConfig
    $cfrom :: forall x. ProjectConfig -> Rep ProjectConfig x
    Generic

    -- | Content of a @.agda-lib@ file.
    --
    data AgdaLibFile = AgdaLibFile
      { AgdaLibFile -> String
    _libName     :: LibName     -- ^ The symbolic name of the library.
      , AgdaLibFile -> String
    _libFile     :: FilePath    -- ^ Path to this @.agda-lib@ file (not content of the file).
      , AgdaLibFile -> [String]
    _libIncludes :: [FilePath]  -- ^ Roots where to look for the modules of the library.
      , AgdaLibFile -> [String]
    _libDepends  :: [LibName]   -- ^ Dependencies.
      , AgdaLibFile -> [String]
    _libPragmas  :: [String]    -- ^ Default pragma options for all files in the library.
      }
      deriving (LineNumber -> AgdaLibFile -> ShowS
    [AgdaLibFile] -> ShowS
    AgdaLibFile -> String
    (LineNumber -> AgdaLibFile -> ShowS)
    -> (AgdaLibFile -> String)
    -> ([AgdaLibFile] -> ShowS)
    -> Show AgdaLibFile
    forall a.
    (LineNumber -> a -> ShowS)
    -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [AgdaLibFile] -> ShowS
    $cshowList :: [AgdaLibFile] -> ShowS
    show :: AgdaLibFile -> String
    $cshow :: AgdaLibFile -> String
    showsPrec :: LineNumber -> AgdaLibFile -> ShowS
    $cshowsPrec :: LineNumber -> 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
    $cto :: forall x. Rep AgdaLibFile x -> AgdaLibFile
    $cfrom :: forall x. AgdaLibFile -> Rep AgdaLibFile x
    Generic)

    emptyLibFile :: AgdaLibFile
    emptyLibFile :: AgdaLibFile
    emptyLibFile = AgdaLibFile :: String -> String -> [String] -> [String] -> [String] -> AgdaLibFile
    AgdaLibFile
      { _libName :: String
    _libName     = String
    ""
      , _libFile :: String
    _libFile     = String
    ""
      , _libIncludes :: [String]
    _libIncludes = []
      , _libDepends :: [String]
    _libDepends  = []
      , _libPragmas :: [String]
    _libPragmas  = []
      }

    -- | Lenses for AgdaLibFile

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

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

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

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

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

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

    type LineNumber = Int

    data LibPositionInfo = LibPositionInfo
      { LibPositionInfo -> Maybe String
    libFilePos :: Maybe FilePath -- ^ Name of @libraries@ file
      , LibPositionInfo -> LineNumber
    lineNumPos :: LineNumber     -- ^ Line number in @libraries@ file.
      , LibPositionInfo -> String
    filePos    :: FilePath       -- ^ Library file
      }
      deriving (LineNumber -> LibPositionInfo -> ShowS
    [LibPositionInfo] -> ShowS
    LibPositionInfo -> String
    (LineNumber -> LibPositionInfo -> ShowS)
    -> (LibPositionInfo -> String)
    -> ([LibPositionInfo] -> ShowS)
    -> Show LibPositionInfo
    forall a.
    (LineNumber -> a -> ShowS)
    -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [LibPositionInfo] -> ShowS
    $cshowList :: [LibPositionInfo] -> ShowS
    show :: LibPositionInfo -> String
    $cshow :: LibPositionInfo -> String
    showsPrec :: LineNumber -> LibPositionInfo -> ShowS
    $cshowsPrec :: LineNumber -> LibPositionInfo -> ShowS
    Show, Typeable LibPositionInfo
    Typeable LibPositionInfo
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> LibPositionInfo -> c LibPositionInfo)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c LibPositionInfo)
    -> (LibPositionInfo -> Constr)
    -> (LibPositionInfo -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c LibPositionInfo))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e))
        -> Maybe (c LibPositionInfo))
    -> ((forall b. Data b => b -> b)
        -> LibPositionInfo -> LibPositionInfo)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> LibPositionInfo -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> LibPositionInfo -> r)
    -> (forall u.
        (forall d. Data d => d -> u) -> LibPositionInfo -> [u])
    -> (forall u.
        LineNumber -> (forall d. Data d => d -> u) -> LibPositionInfo -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d)
        -> LibPositionInfo -> m LibPositionInfo)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d)
        -> LibPositionInfo -> m LibPositionInfo)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d)
        -> LibPositionInfo -> m LibPositionInfo)
    -> Data LibPositionInfo
    LibPositionInfo -> DataType
    LibPositionInfo -> Constr
    (forall b. Data b => b -> b) -> LibPositionInfo -> LibPositionInfo
    forall a.
    Typeable a
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. LineNumber -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u.
    LineNumber -> (forall d. Data d => d -> u) -> LibPositionInfo -> u
    forall u. (forall d. Data d => d -> u) -> LibPositionInfo -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LibPositionInfo -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LibPositionInfo -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> LibPositionInfo -> m LibPositionInfo
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> LibPositionInfo -> m LibPositionInfo
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c LibPositionInfo
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> LibPositionInfo -> c LibPositionInfo
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c LibPositionInfo)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c LibPositionInfo)
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> LibPositionInfo -> m LibPositionInfo
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> LibPositionInfo -> m LibPositionInfo
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> LibPositionInfo -> m LibPositionInfo
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> LibPositionInfo -> m LibPositionInfo
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> LibPositionInfo -> m LibPositionInfo
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> LibPositionInfo -> m LibPositionInfo
    gmapQi :: forall u.
    LineNumber -> (forall d. Data d => d -> u) -> LibPositionInfo -> u
    $cgmapQi :: forall u.
    LineNumber -> (forall d. Data d => d -> u) -> LibPositionInfo -> u
    gmapQ :: forall u. (forall d. Data d => d -> u) -> LibPositionInfo -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> LibPositionInfo -> [u]
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LibPositionInfo -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LibPositionInfo -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LibPositionInfo -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LibPositionInfo -> r
    gmapT :: (forall b. Data b => b -> b) -> LibPositionInfo -> LibPositionInfo
    $cgmapT :: (forall b. Data b => b -> b) -> LibPositionInfo -> LibPositionInfo
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c LibPositionInfo)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c LibPositionInfo)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c LibPositionInfo)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c LibPositionInfo)
    dataTypeOf :: LibPositionInfo -> DataType
    $cdataTypeOf :: LibPositionInfo -> DataType
    toConstr :: LibPositionInfo -> Constr
    $ctoConstr :: LibPositionInfo -> Constr
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c LibPositionInfo
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c LibPositionInfo
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> LibPositionInfo -> c LibPositionInfo
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> LibPositionInfo -> c LibPositionInfo
    Data, (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
    $cto :: forall x. Rep LibPositionInfo x -> LibPositionInfo
    $cfrom :: forall x. LibPositionInfo -> Rep LibPositionInfo x
    Generic)

    data LibWarning = LibWarning (Maybe LibPositionInfo) LibWarning'
      deriving (LineNumber -> LibWarning -> ShowS
    [LibWarning] -> ShowS
    LibWarning -> String
    (LineNumber -> LibWarning -> ShowS)
    -> (LibWarning -> String)
    -> ([LibWarning] -> ShowS)
    -> Show LibWarning
    forall a.
    (LineNumber -> a -> ShowS)
    -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [LibWarning] -> ShowS
    $cshowList :: [LibWarning] -> ShowS
    show :: LibWarning -> String
    $cshow :: LibWarning -> String
    showsPrec :: LineNumber -> LibWarning -> ShowS
    $cshowsPrec :: LineNumber -> LibWarning -> ShowS
    Show, Typeable LibWarning
    Typeable LibWarning
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> LibWarning -> c LibWarning)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c LibWarning)
    -> (LibWarning -> Constr)
    -> (LibWarning -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c LibWarning))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e))
        -> Maybe (c LibWarning))
    -> ((forall b. Data b => b -> b) -> LibWarning -> LibWarning)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> LibWarning -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> LibWarning -> r)
    -> (forall u. (forall d. Data d => d -> u) -> LibWarning -> [u])
    -> (forall u.
        LineNumber -> (forall d. Data d => d -> u) -> LibWarning -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> LibWarning -> m LibWarning)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> LibWarning -> m LibWarning)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> LibWarning -> m LibWarning)
    -> Data LibWarning
    LibWarning -> DataType
    LibWarning -> Constr
    (forall b. Data b => b -> b) -> LibWarning -> LibWarning
    forall a.
    Typeable a
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. LineNumber -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u.
    LineNumber -> (forall d. Data d => d -> u) -> LibWarning -> u
    forall u. (forall d. Data d => d -> u) -> LibWarning -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LibWarning -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LibWarning -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> LibWarning -> m LibWarning
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LibWarning -> m LibWarning
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c LibWarning
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> LibWarning -> c LibWarning
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c LibWarning)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LibWarning)
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LibWarning -> m LibWarning
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LibWarning -> m LibWarning
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LibWarning -> m LibWarning
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LibWarning -> m LibWarning
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> LibWarning -> m LibWarning
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> LibWarning -> m LibWarning
    gmapQi :: forall u.
    LineNumber -> (forall d. Data d => d -> u) -> LibWarning -> u
    $cgmapQi :: forall u.
    LineNumber -> (forall d. Data d => d -> u) -> LibWarning -> u
    gmapQ :: forall u. (forall d. Data d => d -> u) -> LibWarning -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> LibWarning -> [u]
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LibWarning -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LibWarning -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LibWarning -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LibWarning -> r
    gmapT :: (forall b. Data b => b -> b) -> LibWarning -> LibWarning
    $cgmapT :: (forall b. Data b => b -> b) -> LibWarning -> LibWarning
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LibWarning)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LibWarning)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c LibWarning)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c LibWarning)
    dataTypeOf :: LibWarning -> DataType
    $cdataTypeOf :: LibWarning -> DataType
    toConstr :: LibWarning -> Constr
    $ctoConstr :: LibWarning -> Constr
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c LibWarning
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c LibWarning
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> LibWarning -> c LibWarning
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> LibWarning -> c LibWarning
    Data, (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
    $cto :: forall x. Rep LibWarning x -> LibWarning
    $cfrom :: forall x. LibWarning -> Rep LibWarning x
    Generic)

    -- | Library Warnings.
    data LibWarning'
      = UnknownField String
      deriving (LineNumber -> LibWarning' -> ShowS
    [LibWarning'] -> ShowS
    LibWarning' -> String
    (LineNumber -> LibWarning' -> ShowS)
    -> (LibWarning' -> String)
    -> ([LibWarning'] -> ShowS)
    -> Show LibWarning'
    forall a.
    (LineNumber -> a -> ShowS)
    -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [LibWarning'] -> ShowS
    $cshowList :: [LibWarning'] -> ShowS
    show :: LibWarning' -> String
    $cshow :: LibWarning' -> String
    showsPrec :: LineNumber -> LibWarning' -> ShowS
    $cshowsPrec :: LineNumber -> LibWarning' -> ShowS
    Show, Typeable LibWarning'
    Typeable LibWarning'
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> LibWarning' -> c LibWarning')
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c LibWarning')
    -> (LibWarning' -> Constr)
    -> (LibWarning' -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c LibWarning'))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e))
        -> Maybe (c LibWarning'))
    -> ((forall b. Data b => b -> b) -> LibWarning' -> LibWarning')
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> LibWarning' -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> LibWarning' -> r)
    -> (forall u. (forall d. Data d => d -> u) -> LibWarning' -> [u])
    -> (forall u.
        LineNumber -> (forall d. Data d => d -> u) -> LibWarning' -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning')
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning')
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning')
    -> Data LibWarning'
    LibWarning' -> DataType
    LibWarning' -> Constr
    (forall b. Data b => b -> b) -> LibWarning' -> LibWarning'
    forall a.
    Typeable a
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. LineNumber -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u.
    LineNumber -> (forall d. Data d => d -> u) -> LibWarning' -> u
    forall u. (forall d. Data d => d -> u) -> LibWarning' -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LibWarning' -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LibWarning' -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning'
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning'
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c LibWarning'
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> LibWarning' -> c LibWarning'
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c LibWarning')
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c LibWarning')
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning'
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning'
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning'
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning'
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning'
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning'
    gmapQi :: forall u.
    LineNumber -> (forall d. Data d => d -> u) -> LibWarning' -> u
    $cgmapQi :: forall u.
    LineNumber -> (forall d. Data d => d -> u) -> LibWarning' -> u
    gmapQ :: forall u. (forall d. Data d => d -> u) -> LibWarning' -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> LibWarning' -> [u]
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LibWarning' -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LibWarning' -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LibWarning' -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LibWarning' -> r
    gmapT :: (forall b. Data b => b -> b) -> LibWarning' -> LibWarning'
    $cgmapT :: (forall b. Data b => b -> b) -> LibWarning' -> LibWarning'
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c LibWarning')
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c LibWarning')
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c LibWarning')
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c LibWarning')
    dataTypeOf :: LibWarning' -> DataType
    $cdataTypeOf :: LibWarning' -> DataType
    toConstr :: LibWarning' -> Constr
    $ctoConstr :: LibWarning' -> Constr
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c LibWarning'
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c LibWarning'
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> LibWarning' -> c LibWarning'
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> LibWarning' -> c LibWarning'
    Data, (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
    $cto :: forall x. Rep LibWarning' x -> LibWarning'
    $cfrom :: forall x. LibWarning' -> Rep LibWarning' x
    Generic)

    data LibError = LibError (Maybe LibPositionInfo) LibError'

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

    -- | Collected errors while processing library files.
    --
    data LibError'
      = LibNotFound LibrariesFile LibName
          -- ^ Raised when a library name could not successfully be resolved
          --   to an @.agda-lib@ file.
          --
      | AmbiguousLib LibName [AgdaLibFile]
          -- ^ Raised when a library name is defined in several @.agda-lib files@.
      | OtherError String
          -- ^ Generic error.
      deriving (LineNumber -> LibError' -> ShowS
    [LibError'] -> ShowS
    LibError' -> String
    (LineNumber -> LibError' -> ShowS)
    -> (LibError' -> String)
    -> ([LibError'] -> ShowS)
    -> Show LibError'
    forall a.
    (LineNumber -> a -> ShowS)
    -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [LibError'] -> ShowS
    $cshowList :: [LibError'] -> ShowS
    show :: LibError' -> String
    $cshow :: LibError' -> String
    showsPrec :: LineNumber -> LibError' -> ShowS
    $cshowsPrec :: LineNumber -> LibError' -> ShowS
    Show)

    -- | Cache locations of project configurations and parsed .agda-lib files
    type LibState =
      ( Map FilePath ProjectConfig
      , Map FilePath AgdaLibFile
      )

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

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

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

    warnings' :: MonadWriter [Either LibError LibWarning] m => [LibWarning'] -> m ()
    warnings' :: forall (m :: * -> *).
    MonadWriter [Either LibError LibWarning] m =>
    [LibWarning'] -> m ()
    warnings' = [Either LibError LibWarning] -> m ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell ([Either LibError LibWarning] -> m ())
    -> ([LibWarning'] -> [Either LibError LibWarning])
    -> [LibWarning']
    -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (LibWarning' -> Either LibError LibWarning)
    -> [LibWarning'] -> [Either LibError LibWarning]
    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)

    -- UNUSED Liang-Ting Chen 2019-07-16
    --warning :: MonadWriter [Either LibError LibWarning] m => LibWarning -> m ()
    --warning = warnings . pure

    raiseErrors' :: MonadWriter [Either LibError LibWarning] m => [LibError'] -> m ()
    raiseErrors' :: forall (m :: * -> *).
    MonadWriter [Either LibError LibWarning] m =>
    [LibError'] -> m ()
    raiseErrors' = [Either LibError LibWarning] -> m ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell ([Either LibError LibWarning] -> m ())
    -> ([LibError'] -> [Either LibError LibWarning])
    -> [LibError']
    -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (LibError' -> Either LibError LibWarning)
    -> [LibError'] -> [Either LibError LibWarning]
    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))

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

    getCachedProjectConfig
      :: (MonadState LibState m, MonadIO m)
      => FilePath -> m (Maybe ProjectConfig)
    getCachedProjectConfig :: forall (m :: * -> *).
    (MonadState LibState m, MonadIO m) =>
    String -> m (Maybe ProjectConfig)
    getCachedProjectConfig String
    path = do
      String
    path <- IO String -> m String
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO String -> m String) -> IO String -> m String
    forall a b. (a -> b) -> a -> b
    $ String -> IO String
    canonicalizePath String
    path
      Map String ProjectConfig
    cache <- (LibState -> Map String ProjectConfig)
    -> m (Map String ProjectConfig)
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets LibState -> Map String ProjectConfig
    forall a b. (a, b) -> a
    fst
      Maybe ProjectConfig -> m (Maybe ProjectConfig)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe ProjectConfig -> m (Maybe ProjectConfig))
    -> Maybe ProjectConfig -> m (Maybe ProjectConfig)
    forall a b. (a -> b) -> a -> b
    $ String -> Map String ProjectConfig -> Maybe ProjectConfig
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup String
    path Map String ProjectConfig
    cache

    storeCachedProjectConfig
      :: (MonadState LibState m, MonadIO m)
      => FilePath -> ProjectConfig -> m ()
    storeCachedProjectConfig :: forall (m :: * -> *).
    (MonadState LibState m, MonadIO m) =>
    String -> ProjectConfig -> m ()
    storeCachedProjectConfig String
    path ProjectConfig
    conf = do
      String
    path <- IO String -> m String
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO String -> m String) -> IO String -> m String
    forall a b. (a -> b) -> a -> b
    $ String -> IO String
    canonicalizePath String
    path
      (LibState -> LibState) -> m ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((LibState -> LibState) -> m ()) -> (LibState -> LibState) -> m ()
    forall a b. (a -> b) -> a -> b
    $ (Map String ProjectConfig -> Map String ProjectConfig)
    -> LibState -> LibState
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (b, d) (c, d)
    first ((Map String ProjectConfig -> Map String ProjectConfig)
     -> LibState -> LibState)
    -> (Map String ProjectConfig -> Map String ProjectConfig)
    -> LibState
    -> LibState
    forall a b. (a -> b) -> a -> b
    $ String
    -> ProjectConfig
    -> Map String ProjectConfig
    -> Map String ProjectConfig
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert String
    path ProjectConfig
    conf

    getCachedAgdaLibFile
      :: (MonadState LibState m, MonadIO m)
      => FilePath -> m (Maybe AgdaLibFile)
    getCachedAgdaLibFile :: forall (m :: * -> *).
    (MonadState LibState m, MonadIO m) =>
    String -> m (Maybe AgdaLibFile)
    getCachedAgdaLibFile String
    path = do
      String
    path <- IO String -> m String
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO String -> m String) -> IO String -> m String
    forall a b. (a -> b) -> a -> b
    $ String -> IO String
    canonicalizePath String
    path
      (LibState -> Maybe AgdaLibFile) -> m (Maybe AgdaLibFile)
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets ((LibState -> Maybe AgdaLibFile) -> m (Maybe AgdaLibFile))
    -> (LibState -> Maybe AgdaLibFile) -> m (Maybe AgdaLibFile)
    forall a b. (a -> b) -> a -> b
    $ String -> Map String AgdaLibFile -> Maybe AgdaLibFile
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup String
    path (Map String AgdaLibFile -> Maybe AgdaLibFile)
    -> (LibState -> Map String AgdaLibFile)
    -> LibState
    -> Maybe AgdaLibFile
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LibState -> Map String AgdaLibFile
    forall a b. (a, b) -> b
    snd

    storeCachedAgdaLibFile
      :: (MonadState LibState m, MonadIO m)
      => FilePath -> AgdaLibFile -> m ()
    storeCachedAgdaLibFile :: forall (m :: * -> *).
    (MonadState LibState m, MonadIO m) =>
    String -> AgdaLibFile -> m ()
    storeCachedAgdaLibFile String
    path AgdaLibFile
    lib = do
      String
    path <- IO String -> m String
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO String -> m String) -> IO String -> m String
    forall a b. (a -> b) -> a -> b
    $ String -> IO String
    canonicalizePath String
    path
      (LibState -> LibState) -> m ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((LibState -> LibState) -> m ()) -> (LibState -> LibState) -> m ()
    forall a b. (a -> b) -> a -> b
    $ (Map String AgdaLibFile -> Map String AgdaLibFile)
    -> LibState -> LibState
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second ((Map String AgdaLibFile -> Map String AgdaLibFile)
     -> LibState -> LibState)
    -> (Map String AgdaLibFile -> Map String AgdaLibFile)
    -> LibState
    -> LibState
    forall a b. (a -> b) -> a -> b
    $ String
    -> AgdaLibFile -> Map String AgdaLibFile -> Map String AgdaLibFile
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert String
    path AgdaLibFile
    lib

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

    formatLibPositionInfo :: LibPositionInfo -> String -> Doc
    formatLibPositionInfo :: LibPositionInfo -> String -> Doc
    formatLibPositionInfo (LibPositionInfo Maybe String
    libFile LineNumber
    lineNum String
    file) String
    err = String -> Doc
    text (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $
      let loc :: String
    loc | Just String
    lf <- Maybe String
    libFile = String
    lf String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ":" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ LineNumber -> String
    forall a. Show a => a -> String
    show LineNumber
    lineNum String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ": "
              | Bool
    otherwise = String
    ""
      in if String
    "Failed to read" String -> String -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `List.isPrefixOf` String
    err
         then String
    loc
         else String
    file String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ":" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (if (Char -> Bool) -> String -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Char -> Bool
    isDigit (LineNumber -> ShowS
    forall a. LineNumber -> [a] -> [a]
    take LineNumber
    1 String
    err) then String
    "" else String
    " ")

    -- | Pretty-print 'LibError'.
    formatLibError :: [AgdaLibFile] -> LibError -> Doc
    formatLibError :: [AgdaLibFile] -> LibError -> Doc
    formatLibError [AgdaLibFile]
    installed (LibError Maybe LibPositionInfo
    mc LibError'
    e) = Doc
    prefix Doc -> Doc -> Doc
    <+> Doc
    body where
      prefix :: Doc
    prefix = case Maybe LibPositionInfo
    mc of
        Maybe LibPositionInfo
    Nothing                      -> Doc
    ""
        Just LibPositionInfo
    c | OtherError String
    err <- LibError'
    e -> LibPositionInfo -> String -> Doc
    formatLibPositionInfo LibPositionInfo
    c String
    err
        Maybe LibPositionInfo
    _                            -> Doc
    ""

      body :: Doc
    body = case LibError'
    e of
        LibNotFound LibrariesFile
    file String
    lib -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          [ String -> Doc
    text (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ String
    "Library '" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    lib String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "' 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
    nest LineNumber
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> Doc
    text (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ String
    "'" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ LibrariesFile -> String
    lfPath LibrariesFile
    file String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "'"
                , Doc
    "to install."
                ]
          , Doc
    "Installed libraries:"
          ] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++
          (Doc -> Doc) -> [Doc] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (LineNumber -> Doc -> Doc
    nest LineNumber
    2)
             (if [AgdaLibFile] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [AgdaLibFile]
    installed then [Doc
    "(none)"]
              else [ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ String -> Doc
    text (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ AgdaLibFile -> String
    _libName AgdaLibFile
    l, LineNumber -> Doc -> Doc
    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
    $ String -> Doc
    text (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ AgdaLibFile -> String
    _libFile AgdaLibFile
    l ]
                   | AgdaLibFile
    l <- [AgdaLibFile]
    installed ])

        AmbiguousLib String
    lib [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 [ String -> Doc
    text (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ String
    "Ambiguous library '" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    lib String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "'."
                , Doc
    "Could refer to any one of"
              ]
            Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : [ LineNumber -> Doc -> Doc
    nest LineNumber
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> Doc
    text (AgdaLibFile -> String
    _libName AgdaLibFile
    l) Doc -> Doc -> Doc
    <+> Doc -> Doc
    parens (String -> Doc
    text (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ AgdaLibFile -> String
    _libFile AgdaLibFile
    l) | AgdaLibFile
    l <- [AgdaLibFile]
    tgts ]

        OtherError String
    err -> String -> Doc
    text String
    err

    instance Pretty LibWarning where
      pretty :: LibWarning -> Doc
    pretty (LibWarning Maybe LibPositionInfo
    mc LibWarning'
    w) = Doc
    prefix Doc -> Doc -> Doc
    <+> LibWarning' -> Doc
    forall a. Pretty a => a -> Doc
    pretty LibWarning'
    w
        where
          prefix :: Doc
    prefix = case Maybe LibPositionInfo
    mc of
            Maybe LibPositionInfo
    Nothing -> Doc
    ""
            Just LibPositionInfo
    c  -> LibPositionInfo -> String -> Doc
    formatLibPositionInfo LibPositionInfo
    c String
    ""

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

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

    instance NFData ExecutablesFile
    instance NFData ProjectConfig
    instance NFData AgdaLibFile
    instance NFData LibPositionInfo
    instance NFData LibWarning
    instance NFData LibWarning'