Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.Interaction.Library.Parse
Description
Parser for .agda-lib
files.
Example file:
name: Main depend: standard-library include: . src more-src
Should parse as:
AgdaLib { libName = Main , libFile = path_to_this_file , libIncludes = [ "." , "src" , "more-src" ] , libDepends = [ "standard-library" ] }
Synopsis
- parseLibFile :: FilePath -> IO (P AgdaLibFile)
- splitCommas :: String -> [String]
- trimLineComment :: String -> String
- type LineNumber = Int
- runP :: P a -> (Either String a, [LibWarning'])
- data LibWarning' = UnknownField String
Documentation
parseLibFile :: FilePath -> IO (P AgdaLibFile) Source #
Parse .agda-lib
file.
Sets libFile
name and turn mentioned include directories into absolute pathes
(provided the given FilePath
is absolute).
splitCommas :: String -> [String] Source #
Break a comma-separated string. Result strings are trim
med.
trimLineComment :: String -> String Source #
Remove leading whitespace and line comment.
type LineNumber = Int Source #
runP :: P a -> (Either String a, [LibWarning']) Source #
data LibWarning' Source #
Library Warnings.
Constructors
UnknownField String |
Instances
Data LibWarning' Source # | |
Defined in Agda.Interaction.Library.Parse Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LibWarning' -> c LibWarning' gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LibWarning' toConstr :: LibWarning' -> Constr dataTypeOf :: LibWarning' -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LibWarning') dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LibWarning') gmapT :: (forall b. Data b => b -> b) -> LibWarning' -> LibWarning' gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LibWarning' -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LibWarning' -> r gmapQ :: (forall d. Data d => d -> u) -> LibWarning' -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> LibWarning' -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning' gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning' gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning' | |
Show LibWarning' Source # | |
Defined in Agda.Interaction.Library.Parse Methods showsPrec :: Int -> LibWarning' -> ShowS show :: LibWarning' -> String showList :: [LibWarning'] -> ShowS | |
Pretty LibWarning' Source # | |
Defined in Agda.Interaction.Library Methods pretty :: LibWarning' -> Doc Source # prettyPrec :: Int -> LibWarning' -> Doc Source # prettyList :: [LibWarning'] -> Doc Source # | |
EmbPrj LibWarning' Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: LibWarning' -> S Int32 Source # icod_ :: LibWarning' -> S Int32 Source # value :: Int32 -> R LibWarning' Source # |