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
type LibName = String
data LibrariesFile = LibrariesFile
{ LibrariesFile -> String
lfPath :: FilePath
, LibrariesFile -> Bool
lfExists :: Bool
} deriving (LineNumber -> LibrariesFile -> ShowS
[LibrariesFile] -> ShowS
LibrariesFile -> String
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)
type ExeName = Text
data ExecutablesFile = ExecutablesFile
{ ExecutablesFile -> String
efPath :: FilePath
, ExecutablesFile -> Bool
efExists :: Bool
} deriving (LineNumber -> ExecutablesFile -> ShowS
[ExecutablesFile] -> ShowS
ExecutablesFile -> String
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
ExecutablesFile -> Constr
ExecutablesFile -> DataType
(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. 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)
libNameForCurrentDir :: LibName
libNameForCurrentDir :: String
libNameForCurrentDir = String
"."
data ProjectConfig
= ProjectConfig
{ ProjectConfig -> String
configRoot :: FilePath
, ProjectConfig -> [String]
configAgdaLibFiles :: [FilePath]
}
| DefaultProjectConfig
deriving 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
data AgdaLibFile = AgdaLibFile
{ AgdaLibFile -> String
_libName :: LibName
, AgdaLibFile -> String
_libFile :: FilePath
, AgdaLibFile -> [String]
_libIncludes :: [FilePath]
, AgdaLibFile -> [String]
_libDepends :: [LibName]
, AgdaLibFile -> [String]
_libPragmas :: [String]
}
deriving (LineNumber -> AgdaLibFile -> ShowS
[AgdaLibFile] -> ShowS
AgdaLibFile -> String
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. 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 = []
}
libName :: Lens' LibName AgdaLibFile
libName :: Lens' String AgdaLibFile
libName String -> f String
f AgdaLibFile
a = String -> f String
f (AgdaLibFile -> String
_libName AgdaLibFile
a) 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) 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) 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) 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) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ [String]
x -> AgdaLibFile
a { _libPragmas :: [String]
_libPragmas = [String]
x }
type LineNumber = Int
data LibPositionInfo = LibPositionInfo
{ LibPositionInfo -> Maybe String
libFilePos :: Maybe FilePath
, LibPositionInfo -> LineNumber
lineNumPos :: LineNumber
, LibPositionInfo -> String
filePos :: FilePath
}
deriving (LineNumber -> LibPositionInfo -> ShowS
[LibPositionInfo] -> ShowS
LibPositionInfo -> String
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
LibPositionInfo -> Constr
LibPositionInfo -> DataType
(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. 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
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
LibWarning -> Constr
LibWarning -> DataType
(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. 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 LibWarning'
= UnknownField String
deriving (LineNumber -> LibWarning' -> ShowS
[LibWarning'] -> ShowS
LibWarning' -> String
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'
LibWarning' -> Constr
LibWarning' -> DataType
(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. 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_
data LibError'
= LibNotFound LibrariesFile LibName
| AmbiguousLib LibName [AgdaLibFile]
| OtherError String
deriving (LineNumber -> LibError' -> ShowS
[LibError'] -> ShowS
LibError' -> String
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)
type LibState =
( Map FilePath ProjectConfig
, Map FilePath AgdaLibFile
)
type LibErrorIO = WriterT [Either LibError LibWarning] (StateT LibState IO)
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 = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map 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' = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe LibPositionInfo -> LibWarning' -> LibWarning
LibWarning forall a. Maybe a
Nothing)
raiseErrors' :: MonadWriter [Either LibError LibWarning] m => [LibError'] -> m ()
raiseErrors' :: forall (m :: * -> *).
MonadWriter [Either LibError LibWarning] m =>
[LibError'] -> m ()
raiseErrors' = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe LibPositionInfo -> LibError' -> LibError
LibError forall a. Maybe a
Nothing))
raiseErrors :: MonadWriter [Either LibError LibWarning] m => [LibError] -> m ()
raiseErrors :: forall (m :: * -> *).
MonadWriter [Either LibError LibWarning] m =>
[LibError] -> m ()
raiseErrors = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map 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 <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO String
canonicalizePath String
path
Map String ProjectConfig
cache <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a b. (a, b) -> a
fst
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO String
canonicalizePath String
path
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first forall a b. (a -> b) -> a -> b
$ 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 <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO String
canonicalizePath String
path
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
path forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO String
canonicalizePath String
path
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
path AgdaLibFile
lib
formatLibPositionInfo :: LibPositionInfo -> String -> Doc
formatLibPositionInfo :: LibPositionInfo -> String -> Doc
formatLibPositionInfo (LibPositionInfo Maybe String
libFile LineNumber
lineNum String
file) String
err = String -> Doc
text forall a b. (a -> b) -> a -> b
$
let loc :: String
loc | Just String
lf <- Maybe String
libFile = String
lf forall a. [a] -> [a] -> [a]
++ String
":" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show LineNumber
lineNum forall a. [a] -> [a] -> [a]
++ String
": "
| Bool
otherwise = String
""
in if String
"Failed to read" forall a. Eq a => [a] -> [a] -> Bool
`List.isPrefixOf` String
err
then String
loc
else String
file forall a. [a] -> [a] -> [a]
++ String
":" forall a. [a] -> [a] -> [a]
++ (if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isDigit (forall a. LineNumber -> [a] -> [a]
take LineNumber
1 String
err) then String
"" else String
" ")
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 -> forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat forall a b. (a -> b) -> a -> b
$
[ String -> Doc
text forall a b. (a -> b) -> a -> b
$ String
"Library '" forall a. [a] -> [a] -> [a]
++ String
lib forall a. [a] -> [a] -> [a]
++ String
"' not found."
, forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Doc
"Add the path to its .agda-lib file to"
, LineNumber -> Doc -> Doc
nest LineNumber
2 forall a b. (a -> b) -> a -> b
$ String -> Doc
text forall a b. (a -> b) -> a -> b
$ String
"'" forall a. [a] -> [a] -> [a]
++ LibrariesFile -> String
lfPath LibrariesFile
file forall a. [a] -> [a] -> [a]
++ String
"'"
, Doc
"to install."
]
, Doc
"Installed libraries:"
] forall a. [a] -> [a] -> [a]
++
forall a b. (a -> b) -> [a] -> [b]
map (LineNumber -> Doc -> Doc
nest LineNumber
2)
(if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [AgdaLibFile]
installed then [Doc
"(none)"]
else [ forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ String -> Doc
text forall a b. (a -> b) -> a -> b
$ AgdaLibFile -> String
_libName AgdaLibFile
l, LineNumber -> Doc -> Doc
nest LineNumber
2 forall a b. (a -> b) -> a -> b
$ Doc -> Doc
parens forall a b. (a -> b) -> a -> b
$ String -> Doc
text forall a b. (a -> b) -> a -> b
$ AgdaLibFile -> String
_libFile AgdaLibFile
l ]
| AgdaLibFile
l <- [AgdaLibFile]
installed ])
AmbiguousLib String
lib [AgdaLibFile]
tgts -> forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat forall a b. (a -> b) -> a -> b
$
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ String -> Doc
text forall a b. (a -> b) -> a -> b
$ String
"Ambiguous library '" forall a. [a] -> [a] -> [a]
++ String
lib forall a. [a] -> [a] -> [a]
++ String
"'."
, Doc
"Could refer to any one of"
]
forall a. a -> [a] -> [a]
: [ LineNumber -> Doc -> Doc
nest LineNumber
2 forall a b. (a -> b) -> a -> b
$ String -> Doc
text (AgdaLibFile -> String
_libName AgdaLibFile
l) Doc -> Doc -> Doc
<+> Doc -> Doc
parens (String -> Doc
text 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
<+> 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 forall a b. (a -> b) -> a -> b
$ String
"Unknown field '" forall a. [a] -> [a] -> [a]
++ String
s forall a. [a] -> [a] -> [a]
++ String
"'"
instance NFData ExecutablesFile
instance NFData ProjectConfig
instance NFData AgdaLibFile
instance NFData LibPositionInfo
instance NFData LibWarning
instance NFData LibWarning'