-- | 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 -> FilePath
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 (Int -> LibrariesFile -> ShowS
[LibrariesFile] -> ShowS
LibrariesFile -> FilePath
(Int -> LibrariesFile -> ShowS)
-> (LibrariesFile -> FilePath)
-> ([LibrariesFile] -> ShowS)
-> Show LibrariesFile
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [LibrariesFile] -> ShowS
$cshowList :: [LibrariesFile] -> ShowS
show :: LibrariesFile -> FilePath
$cshow :: LibrariesFile -> FilePath
showsPrec :: Int -> LibrariesFile -> ShowS
$cshowsPrec :: Int -> LibrariesFile -> ShowS
Show)

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

data ExecutablesFile = ExecutablesFile
  { ExecutablesFile -> FilePath
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 (Int -> ExecutablesFile -> ShowS
[ExecutablesFile] -> ShowS
ExecutablesFile -> FilePath
(Int -> ExecutablesFile -> ShowS)
-> (ExecutablesFile -> FilePath)
-> ([ExecutablesFile] -> ShowS)
-> Show ExecutablesFile
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [ExecutablesFile] -> ShowS
$cshowList :: [ExecutablesFile] -> ShowS
show :: ExecutablesFile -> FilePath
$cshow :: ExecutablesFile -> FilePath
showsPrec :: Int -> ExecutablesFile -> ShowS
$cshowsPrec :: Int -> ExecutablesFile -> ShowS
Show, Typeable ExecutablesFile
DataType
Constr
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.
    Int -> (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 d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ExecutablesFile -> c ExecutablesFile
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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. Int -> (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.
Int -> (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)
$cExecutablesFile :: Constr
$tExecutablesFile :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> ExecutablesFile -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> ExecutablesFile -> u
gmapQ :: (forall d. Data d => d -> u) -> ExecutablesFile -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ExecutablesFile -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable 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 :: FilePath
libNameForCurrentDir = FilePath
"."

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

-- | Lenses for AgdaLibFile

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

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

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

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

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


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

type LineNumber = Int

data LibPositionInfo = LibPositionInfo
  { LibPositionInfo -> Maybe FilePath
libFilePos :: Maybe FilePath -- ^ Name of @libraries@ file
  , LibPositionInfo -> Int
lineNumPos :: LineNumber     -- ^ Line number in @libraries@ file.
  , LibPositionInfo -> FilePath
filePos    :: FilePath       -- ^ Library file
  }
  deriving (Int -> LibPositionInfo -> ShowS
[LibPositionInfo] -> ShowS
LibPositionInfo -> FilePath
(Int -> LibPositionInfo -> ShowS)
-> (LibPositionInfo -> FilePath)
-> ([LibPositionInfo] -> ShowS)
-> Show LibPositionInfo
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [LibPositionInfo] -> ShowS
$cshowList :: [LibPositionInfo] -> ShowS
show :: LibPositionInfo -> FilePath
$cshow :: LibPositionInfo -> FilePath
showsPrec :: Int -> LibPositionInfo -> ShowS
$cshowsPrec :: Int -> LibPositionInfo -> ShowS
Show, Typeable LibPositionInfo
DataType
Constr
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.
    Int -> (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 d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LibPositionInfo -> c LibPositionInfo
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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. Int -> (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.
Int -> (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)
$cLibPositionInfo :: Constr
$tLibPositionInfo :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> LibPositionInfo -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> LibPositionInfo -> u
gmapQ :: (forall d. Data d => d -> u) -> LibPositionInfo -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> LibPositionInfo -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable 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 (Int -> LibWarning -> ShowS
[LibWarning] -> ShowS
LibWarning -> FilePath
(Int -> LibWarning -> ShowS)
-> (LibWarning -> FilePath)
-> ([LibWarning] -> ShowS)
-> Show LibWarning
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [LibWarning] -> ShowS
$cshowList :: [LibWarning] -> ShowS
show :: LibWarning -> FilePath
$cshow :: LibWarning -> FilePath
showsPrec :: Int -> LibWarning -> ShowS
$cshowsPrec :: Int -> LibWarning -> ShowS
Show, Typeable LibWarning
DataType
Constr
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.
    Int -> (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 d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LibWarning -> c LibWarning
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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. Int -> (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. Int -> (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)
$cLibWarning :: Constr
$tLibWarning :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> LibWarning -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> LibWarning -> u
gmapQ :: (forall d. Data d => d -> u) -> LibWarning -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> LibWarning -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable 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 (Int -> LibWarning' -> ShowS
[LibWarning'] -> ShowS
LibWarning' -> FilePath
(Int -> LibWarning' -> ShowS)
-> (LibWarning' -> FilePath)
-> ([LibWarning'] -> ShowS)
-> Show LibWarning'
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [LibWarning'] -> ShowS
$cshowList :: [LibWarning'] -> ShowS
show :: LibWarning' -> FilePath
$cshow :: LibWarning' -> FilePath
showsPrec :: Int -> LibWarning' -> ShowS
$cshowsPrec :: Int -> LibWarning' -> ShowS
Show, Typeable LibWarning'
DataType
Constr
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.
    Int -> (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 d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LibWarning' -> c LibWarning'
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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. Int -> (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. Int -> (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')
$cUnknownField :: Constr
$tLibWarning' :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> LibWarning' -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> LibWarning' -> u
gmapQ :: (forall d. Data d => d -> u) -> LibWarning' -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> LibWarning' -> [u]
gmapQr :: (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 :: (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 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 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 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 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'
$cp1Data :: Typeable 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 (Int -> LibError' -> ShowS
[LibError'] -> ShowS
LibError' -> FilePath
(Int -> LibError' -> ShowS)
-> (LibError' -> FilePath)
-> ([LibError'] -> ShowS)
-> Show LibError'
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [LibError'] -> ShowS
$cshowList :: [LibError'] -> ShowS
show :: LibError' -> FilePath
$cshow :: LibError' -> FilePath
showsPrec :: Int -> LibError' -> ShowS
$cshowsPrec :: Int -> 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 :: [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' :: [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' :: [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 :: [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 :: FilePath -> m (Maybe ProjectConfig)
getCachedProjectConfig FilePath
path = do
  FilePath
path <- IO FilePath -> m FilePath
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO FilePath -> m FilePath) -> IO FilePath -> m FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> IO FilePath
canonicalizePath FilePath
path
  Map FilePath ProjectConfig
cache <- ((Map FilePath ProjectConfig, Map FilePath AgdaLibFile)
 -> Map FilePath ProjectConfig)
-> m (Map FilePath ProjectConfig)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Map FilePath ProjectConfig, Map FilePath AgdaLibFile)
-> Map FilePath 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
$ FilePath -> Map FilePath ProjectConfig -> Maybe ProjectConfig
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup FilePath
path Map FilePath ProjectConfig
cache

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

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

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

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

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

-- | 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 FilePath
err <- LibError'
e -> LibPositionInfo -> FilePath -> Doc
formatLibPositionInfo LibPositionInfo
c FilePath
err
    Maybe LibPositionInfo
_                            -> Doc
""

  body :: Doc
body = case LibError'
e of
    LibNotFound LibrariesFile
file FilePath
lib -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
      [ FilePath -> Doc
text (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
"Library '" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
lib FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
"' not found."
      , [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Doc
"Add the path to its .agda-lib file to"
            , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath -> Doc
text (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
"'" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ LibrariesFile -> FilePath
lfPath LibrariesFile
file FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
"'"
            , 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 (Int -> Doc -> Doc
nest Int
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 [ FilePath -> Doc
text (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ AgdaLibFile -> FilePath
_libName AgdaLibFile
l, Int -> Doc -> Doc
nest Int
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
$ FilePath -> Doc
text (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ AgdaLibFile -> FilePath
_libFile AgdaLibFile
l ]
               | AgdaLibFile
l <- [AgdaLibFile]
installed ])

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


    OtherError FilePath
err -> FilePath -> Doc
text FilePath
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 -> FilePath -> Doc
formatLibPositionInfo LibPositionInfo
c FilePath
""


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

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

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