-- | 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
  { _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'