    -- | 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" ]
    --       }
    --   @
    --
    module Agda.Interaction.Library.Parse
      ( parseLibFile
      , splitCommas
      , trimLineComment
      , runP
      ) where

    import Control.Monad
    import Control.Monad.Except
    import Control.Monad.Writer
    import Data.Char
    import Data.Data
    import qualified Data.List as List
    import System.FilePath

    import Agda.Interaction.Library.Base

    import Agda.Utils.Applicative
    import Agda.Utils.IO ( catchIO )
    import qualified Agda.Utils.IO.UTF8 as UTF8
    import Agda.Utils.Lens
    import Agda.Utils.List   ( duplicates )
    import Agda.Utils.String ( ltrim )

    -- | Parser monad: Can throw @String@ error messages, and collects
    -- @LibWarning'@s library warnings.
    type P = ExceptT String (Writer [LibWarning'])

    runP :: P a -> (Either String a, [LibWarning'])
    runP :: forall a. P a -> (Either String a, [LibWarning'])
    runP = Writer [LibWarning'] (Either String a)
    -> (Either String a, [LibWarning'])
    forall w a. Writer w a -> (a, w)
    runWriter (Writer [LibWarning'] (Either String a)
     -> (Either String a, [LibWarning']))
    -> (ExceptT String (Writer [LibWarning']) a
        -> Writer [LibWarning'] (Either String a))
    -> ExceptT String (Writer [LibWarning']) a
    -> (Either String a, [LibWarning'])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ExceptT String (Writer [LibWarning']) a
    -> Writer [LibWarning'] (Either String a)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT

    warningP :: LibWarning' -> P ()
    warningP :: LibWarning' -> P ()
    warningP = [LibWarning'] -> P ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell ([LibWarning'] -> P ())
    -> (LibWarning' -> [LibWarning']) -> LibWarning' -> P ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LibWarning' -> [LibWarning']
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure

    -- | The config files we parse have the generic structure of a sequence
    --   of @field : content@ entries.
    type GenericFile = [GenericEntry]

    data GenericEntry = GenericEntry
      { GenericEntry -> String
    geHeader   :: String   -- ^ E.g. field name.    @trim@med.
      , GenericEntry -> [String]
    _geContent :: [String] -- ^ E.g. field content. @trim@med.
      }

    -- | Library file field format format [sic!].
    data Field = forall a. Field
      { Field -> String
    fName     :: String            -- ^ Name of the field.
      , Field -> Bool
    fOptional :: Bool              -- ^ Is it optional?
      , ()
    fParse    :: [String] -> P a   -- ^ Content parser for this field.
      , ()
    fSet      :: LensSet a AgdaLibFile
        -- ^ Sets parsed content in 'AgdaLibFile' structure.
      }

    optionalField :: String -> ([String] -> P a) -> Lens' a AgdaLibFile -> Field
    optionalField :: forall a.
    String -> ([String] -> P a) -> Lens' a AgdaLibFile -> Field
    optionalField String
    str [String] -> P a
    p Lens' a AgdaLibFile
    l = String
    -> Bool -> ([String] -> P a) -> LensSet a AgdaLibFile -> Field
    forall a.
    String
    -> Bool -> ([String] -> P a) -> LensSet a AgdaLibFile -> Field
    Field String
    str Bool
    True [String] -> P a
    p (Lens' a AgdaLibFile -> LensSet a AgdaLibFile
    forall i o. Lens' i o -> LensSet i o
    set Lens' a AgdaLibFile
    l)

    -- | @.agda-lib@ file format with parsers and setters.
    agdaLibFields :: [Field]
    agdaLibFields :: [Field]
    agdaLibFields =
      -- Andreas, 2017-08-23, issue #2708, field "name" is optional.
      [ String
    -> ([String] -> P String) -> Lens' String AgdaLibFile -> Field
    forall a.
    String -> ([String] -> P a) -> Lens' a AgdaLibFile -> Field
    optionalField String
    "name"    [String] -> P String
    parseName                      Lens' String AgdaLibFile
    libName
      , String
    -> ([String] -> P [String]) -> Lens' [String] AgdaLibFile -> Field
    forall a.
    String -> ([String] -> P a) -> Lens' a AgdaLibFile -> Field
    optionalField String
    "include" ([String] -> P [String]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([String] -> P [String])
    -> ([String] -> [String]) -> [String] -> P [String]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String -> [String]) -> [String] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap String -> [String]
    parsePaths)  Lens' [String] AgdaLibFile
    libIncludes
      , String
    -> ([String] -> P [String]) -> Lens' [String] AgdaLibFile -> Field
    forall a.
    String -> ([String] -> P a) -> Lens' a AgdaLibFile -> Field
    optionalField String
    "depend"  ([String] -> P [String]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([String] -> P [String])
    -> ([String] -> [String]) -> [String] -> P [String]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String -> [String]) -> [String] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap String -> [String]
    splitCommas) Lens' [String] AgdaLibFile
    libDepends
      , String
    -> ([String] -> P [String]) -> Lens' [String] AgdaLibFile -> Field
    forall a.
    String -> ([String] -> P a) -> Lens' a AgdaLibFile -> Field
    optionalField String
    "flags"   ([String] -> P [String]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([String] -> P [String])
    -> ([String] -> [String]) -> [String] -> P [String]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String -> [String]) -> [String] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap String -> [String]
    parseFlags)  Lens' [String] AgdaLibFile
    libPragmas
      ]
      where
        parseName :: [String] -> P LibName
        parseName :: [String] -> P String
    parseName [String
    s] | [String
    name] <- String -> [String]
    words String
    s = String -> P String
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure String
    name
        parseName [String]
    ls = String -> P String
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> P String) -> String -> P String
    forall a b. (a -> b) -> a -> b
    $ String
    "Bad library name: '" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [String]
    ls String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "'"

        parsePaths :: String -> [FilePath]
        parsePaths :: String -> [String]
    parsePaths = (String -> String) -> String -> [String]
    go String -> String
    forall a. a -> a
    id where
          fixup :: ([a] -> t a) -> f (t a)
    fixup [a] -> t a
    acc = let fp :: t a
    fp = [a] -> t a
    acc [] in Bool -> Bool
    not (t a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null t a
    fp) Bool -> t a -> f (t a)
    forall (f :: * -> *) a. Alternative f => Bool -> a -> f a
    ?$> t a
    fp
          go :: (String -> String) -> String -> [String]
    go String -> String
    acc []           = (String -> String) -> [String]
    forall {f :: * -> *} {t :: * -> *} {a} {a}.
    (Alternative f, Foldable t) =>
    ([a] -> t a) -> f (t a)
    fixup String -> String
    acc
          go String -> String
    acc (Char
    '\\' : Char
    ' '  :String
    cs) = (String -> String) -> String -> [String]
    go (String -> String
    acc (String -> String) -> (String -> String) -> String -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Char
    ' 'Char -> String -> String
    forall a. a -> [a] -> [a]
    :)) String
    cs
          go String -> String
    acc (Char
    '\\' : Char
    '\\' :String
    cs) = (String -> String) -> String -> [String]
    go (String -> String
    acc (String -> String) -> (String -> String) -> String -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Char
    '\\'Char -> String -> String
    forall a. a -> [a] -> [a]
    :)) String
    cs
          go String -> String
    acc (       Char
    ' '  :String
    cs) = (String -> String) -> [String]
    forall {f :: * -> *} {t :: * -> *} {a} {a}.
    (Alternative f, Foldable t) =>
    ([a] -> t a) -> f (t a)
    fixup String -> String
    acc [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ (String -> String) -> String -> [String]
    go String -> String
    forall a. a -> a
    id String
    cs
          go String -> String
    acc (Char
    c           :String
    cs) = (String -> String) -> String -> [String]
    go (String -> String
    acc (String -> String) -> (String -> String) -> String -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Char
    cChar -> String -> String
    forall a. a -> [a] -> [a]
    :)) String
    cs

        parseFlags :: String -> [String]
        parseFlags :: String -> [String]
    parseFlags = String -> [String]
    words

    -- | Parse @.agda-lib@ file.
    --
    -- Sets 'libFile' name and turn mentioned include directories into absolute
    -- pathes (provided the given 'FilePath' is absolute).
    --
    parseLibFile :: FilePath -> IO (P AgdaLibFile)
    parseLibFile :: String -> IO (P AgdaLibFile)
    parseLibFile String
    file =
      ((AgdaLibFile -> AgdaLibFile) -> P AgdaLibFile -> P AgdaLibFile
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap AgdaLibFile -> AgdaLibFile
    setPath (P AgdaLibFile -> P AgdaLibFile)
    -> (String -> P AgdaLibFile) -> String -> P AgdaLibFile
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> P AgdaLibFile
    parseLib (String -> P AgdaLibFile) -> IO String -> IO (P AgdaLibFile)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> IO String
    UTF8.readFile String
    file) IO (P AgdaLibFile)
    -> (IOException -> IO (P AgdaLibFile)) -> IO (P AgdaLibFile)
    forall (m :: * -> *) a.
    CatchIO m =>
    m a -> (IOException -> m a) -> m a
    `catchIO` \IOException
    e ->
        P AgdaLibFile -> IO (P AgdaLibFile)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (P AgdaLibFile -> IO (P AgdaLibFile))
    -> P AgdaLibFile -> IO (P AgdaLibFile)
    forall a b. (a -> b) -> a -> b
    $ String -> P AgdaLibFile
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> P AgdaLibFile) -> String -> P AgdaLibFile
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines
          [ String
    "Failed to read library file " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    file String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "."
          , String
    "Reason: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ IOException -> String
    forall a. Show a => a -> String
    show IOException
    e
          ]
      where
        setPath :: AgdaLibFile -> AgdaLibFile
    setPath      AgdaLibFile
    lib = String -> AgdaLibFile -> AgdaLibFile
    unrelativise (String -> String
    takeDirectory String
    file) (Lens' String AgdaLibFile -> String -> AgdaLibFile -> AgdaLibFile
    forall i o. Lens' i o -> LensSet i o
    set Lens' String AgdaLibFile
    libFile String
    file AgdaLibFile
    lib)
        unrelativise :: String -> AgdaLibFile -> AgdaLibFile
    unrelativise String
    dir = Lens' [String] AgdaLibFile -> LensMap [String] AgdaLibFile
    forall i o. Lens' i o -> LensMap i o
    over Lens' [String] AgdaLibFile
    libIncludes ((String -> String) -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String
    dir String -> String -> String
    </>))

    -- | Parse file contents.
    parseLib :: String -> P AgdaLibFile
    parseLib :: String -> P AgdaLibFile
    parseLib String
    s = GenericFile -> P AgdaLibFile
    fromGeneric (GenericFile -> P AgdaLibFile)
    -> ExceptT String (Writer [LibWarning']) GenericFile
    -> P AgdaLibFile
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< String -> ExceptT String (Writer [LibWarning']) GenericFile
    parseGeneric String
    s

    -- | Parse 'GenericFile' with 'agdaLibFields' descriptors.
    fromGeneric :: GenericFile -> P AgdaLibFile
    fromGeneric :: GenericFile -> P AgdaLibFile
    fromGeneric = [Field] -> GenericFile -> P AgdaLibFile
    fromGeneric' [Field]
    agdaLibFields

    -- | Given a list of 'Field' descriptors (with their custom parsers),
    --   parse a 'GenericFile' into the 'AgdaLibFile' structure.
    --
    --   Checks mandatory fields are present;
    --   no duplicate fields, no unknown fields.

    fromGeneric' :: [Field] -> GenericFile -> P AgdaLibFile
    fromGeneric' :: [Field] -> GenericFile -> P AgdaLibFile
    fromGeneric' [Field]
    fields GenericFile
    fs = do
      [Field] -> [String] -> P ()
    checkFields [Field]
    fields ((GenericEntry -> String) -> GenericFile -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map GenericEntry -> String
    geHeader GenericFile
    fs)
      (AgdaLibFile -> GenericEntry -> P AgdaLibFile)
    -> AgdaLibFile -> GenericFile -> P AgdaLibFile
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM AgdaLibFile -> GenericEntry -> P AgdaLibFile
    upd AgdaLibFile
    emptyLibFile GenericFile
    fs
      where
        upd :: AgdaLibFile -> GenericEntry -> P AgdaLibFile
        upd :: AgdaLibFile -> GenericEntry -> P AgdaLibFile
    upd AgdaLibFile
    l (GenericEntry String
    h [String]
    cs) = do
          Maybe Field
    mf <- String -> [Field] -> P (Maybe Field)
    findField String
    h [Field]
    fields
          case Maybe Field
    mf of
            Just Field{Bool
    String
    LensSet a AgdaLibFile
    [String] -> P a
    fSet :: LensSet a AgdaLibFile
    fParse :: [String] -> P a
    fOptional :: Bool
    fName :: String
    fSet :: ()
    fParse :: ()
    fOptional :: Field -> Bool
    fName :: Field -> String
    ..} -> do
              a
    x <- [String] -> P a
    fParse [String]
    cs
              AgdaLibFile -> P AgdaLibFile
    forall (m :: * -> *) a. Monad m => a -> m a
    return (AgdaLibFile -> P AgdaLibFile) -> AgdaLibFile -> P AgdaLibFile
    forall a b. (a -> b) -> a -> b
    $ LensSet a AgdaLibFile
    fSet a
    x AgdaLibFile
    l
            Maybe Field
    Nothing -> AgdaLibFile -> P AgdaLibFile
    forall (m :: * -> *) a. Monad m => a -> m a
    return AgdaLibFile
    l

    -- | Ensure that there are no duplicate fields and no mandatory fields are missing.
    checkFields :: [Field] -> [String] -> P ()
    checkFields :: [Field] -> [String] -> P ()
    checkFields [Field]
    fields [String]
    fs = do
      let mandatory :: [String]
    mandatory = [ Field -> String
    fName Field
    f | Field
    f <- [Field]
    fields, Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Field -> Bool
    fOptional Field
    f ]
          -- Missing fields.
          missing :: [String]
    missing   = [String]
    mandatory [String] -> [String] -> [String]
    forall a. Eq a => [a] -> [a] -> [a]
    List.\\ [String]
    fs
          -- Duplicate fields.
          dup :: [String]
    dup       = [String] -> [String]
    forall a. Ord a => [a] -> [a]
    duplicates [String]
    fs
          -- Plural s for error message.
          s :: t a -> p
    s t a
    xs      = if t a -> LineNumber
    forall (t :: * -> *) a. Foldable t => t a -> LineNumber
    length t a
    xs LineNumber -> LineNumber -> Bool
    forall a. Ord a => a -> a -> Bool
    > LineNumber
    1 then p
    "s" else p
    ""
          list :: [String] -> String
    list [String]
    xs   = String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    List.intercalate String
    ", " [ String
    "'" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    f String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "'" | String
    f <- [String]
    xs ]
      Bool -> P () -> P ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([String] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    missing) (P () -> P ()) -> P () -> P ()
    forall a b. (a -> b) -> a -> b
    $ String -> P ()
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> P ()) -> String -> P ()
    forall a b. (a -> b) -> a -> b
    $ String
    "Missing field" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    forall {t :: * -> *} {p} {a}. (Foldable t, IsString p) => t a -> p
    s [String]
    missing String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    list [String]
    missing
      Bool -> P () -> P ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([String] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    dup)     (P () -> P ()) -> P () -> P ()
    forall a b. (a -> b) -> a -> b
    $ String -> P ()
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> P ()) -> String -> P ()
    forall a b. (a -> b) -> a -> b
    $ String
    "Duplicate field" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    forall {t :: * -> *} {p} {a}. (Foldable t, IsString p) => t a -> p
    s [String]
    dup String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    list [String]
    dup

    -- | Find 'Field' with given 'fName', throw error if unknown.
    findField :: String -> [Field] -> P (Maybe Field)
    findField :: String -> [Field] -> P (Maybe Field)
    findField String
    s [Field]
    fs = P (Maybe Field)
    -> (Field -> P (Maybe Field)) -> Maybe Field -> P (Maybe Field)
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe P (Maybe Field)
    err (Maybe Field -> P (Maybe Field)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Field -> P (Maybe Field))
    -> (Field -> Maybe Field) -> Field -> P (Maybe Field)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Field -> Maybe Field
    forall a. a -> Maybe a
    Just) (Maybe Field -> P (Maybe Field)) -> Maybe Field -> P (Maybe Field)
    forall a b. (a -> b) -> a -> b
    $ (Field -> Bool) -> [Field] -> Maybe Field
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    List.find ((String
    s String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (String -> Bool) -> (Field -> String) -> Field -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Field -> String
    fName) [Field]
    fs
      where err :: P (Maybe Field)
    err = LibWarning' -> P ()
    warningP (String -> LibWarning'
    UnknownField String
    s) P () -> P (Maybe Field) -> P (Maybe Field)
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Maybe Field -> P (Maybe Field)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Field
    forall a. Maybe a
    Nothing

    -- Generic file parser ----------------------------------------------------

    -- | Example:
    --
    -- @
    --     parseGeneric "name:Main--BLA\ndepend:--BLA\n  standard-library--BLA\ninclude : . --BLA\n  src more-src   \n"
    --     == Right [("name",["Main"]),("depend",["standard-library"]),("include",[".","src more-src"])]
    -- @
    parseGeneric :: String -> P GenericFile
    parseGeneric :: String -> ExceptT String (Writer [LibWarning']) GenericFile
    parseGeneric String
    s =
      [GenericLine] -> ExceptT String (Writer [LibWarning']) GenericFile
    groupLines ([GenericLine]
     -> ExceptT String (Writer [LibWarning']) GenericFile)
    -> ExceptT String (Writer [LibWarning']) [GenericLine]
    -> ExceptT String (Writer [LibWarning']) GenericFile
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [[GenericLine]] -> [GenericLine]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[GenericLine]] -> [GenericLine])
    -> ExceptT String (Writer [LibWarning']) [[GenericLine]]
    -> ExceptT String (Writer [LibWarning']) [GenericLine]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (LineNumber
     -> String -> ExceptT String (Writer [LibWarning']) [GenericLine])
    -> [LineNumber]
    -> [String]
    -> ExceptT String (Writer [LibWarning']) [[GenericLine]]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM LineNumber
    -> String -> ExceptT String (Writer [LibWarning']) [GenericLine]
    parseLine [LineNumber
    1..] ((String -> String) -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> String
    stripComments ([String] -> [String]) -> [String] -> [String]
    forall a b. (a -> b) -> a -> b
    $ String -> [String]
    lines String
    s)

    -- | Lines with line numbers.
    data GenericLine
      = Header  LineNumber String
          -- ^ Header line, like a field name, e.g. "include :".  Cannot be indented.
          --   @String@ is 'trim'med.
      | Content LineNumber String
          -- ^ Other line.  Must be indented.
          --   @String@ is 'trim'med.
      deriving (LineNumber -> GenericLine -> String -> String
    [GenericLine] -> String -> String
    GenericLine -> String
    (LineNumber -> GenericLine -> String -> String)
    -> (GenericLine -> String)
    -> ([GenericLine] -> String -> String)
    -> Show GenericLine
    forall a.
    (LineNumber -> a -> String -> String)
    -> (a -> String) -> ([a] -> String -> String) -> Show a
    showList :: [GenericLine] -> String -> String
    $cshowList :: [GenericLine] -> String -> String
    show :: GenericLine -> String
    $cshow :: GenericLine -> String
    showsPrec :: LineNumber -> GenericLine -> String -> String
    $cshowsPrec :: LineNumber -> GenericLine -> String -> String
    Show)

    -- | Parse line into 'Header' and 'Content' components.
    --
    --   Precondition: line comments and trailing whitespace have been stripped away.
    --
    --   Example file:
    --
    --   @
    --     name: Main
    --     depend:
    --       standard-library
    --     include: .
    --       src more-src
    --   @
    --
    --   This should give
    --
    --   @
    --     [ Header  1 "name"
    --     , Content 1 "Main"
    --     , Header  2 "depend"
    --     , Content 3 "standard-library"
    --     , Header  4 "include"
    --     , Content 4 "."
    --     , Content 5 "src more-src"
    --     ]
    --   @
    parseLine :: LineNumber -> String -> P [GenericLine]
    parseLine :: LineNumber
    -> String -> ExceptT String (Writer [LibWarning']) [GenericLine]
    parseLine LineNumber
    _ String
    "" = [GenericLine]
    -> ExceptT String (Writer [LibWarning']) [GenericLine]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure []
    parseLine LineNumber
    l s :: String
    s@(Char
    c:String
    _)
        -- Indented lines are 'Content'.
      | Char -> Bool
    isSpace Char
    c   = [GenericLine]
    -> ExceptT String (Writer [LibWarning']) [GenericLine]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [LineNumber -> String -> GenericLine
    Content LineNumber
    l (String -> GenericLine) -> String -> GenericLine
    forall a b. (a -> b) -> a -> b
    $ String -> String
    ltrim String
    s]
        -- Non-indented lines are 'Header'.
      | Bool
    otherwise   =
        case (Char -> Bool) -> String -> (String, String)
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    break (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    ==Char
    ':') String
    s of
          -- Headers are single words followed by a colon.
          -- Anything after the colon that is not whitespace is 'Content'.
          (String
    h, Char
    ':' : String
    r) ->
            case String -> [String]
    words String
    h of
              [String
    h] -> [GenericLine]
    -> ExceptT String (Writer [LibWarning']) [GenericLine]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([GenericLine]
     -> ExceptT String (Writer [LibWarning']) [GenericLine])
    -> [GenericLine]
    -> ExceptT String (Writer [LibWarning']) [GenericLine]
    forall a b. (a -> b) -> a -> b
    $ LineNumber -> String -> GenericLine
    Header LineNumber
    l String
    h GenericLine -> [GenericLine] -> [GenericLine]
    forall a. a -> [a] -> [a]
    : [LineNumber -> String -> GenericLine
    Content LineNumber
    l String
    r' | let r' :: String
    r' = String -> String
    ltrim String
    r, Bool -> Bool
    not (String -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null String
    r')]
              []  -> String -> ExceptT String (Writer [LibWarning']) [GenericLine]
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> ExceptT String (Writer [LibWarning']) [GenericLine])
    -> String -> ExceptT String (Writer [LibWarning']) [GenericLine]
    forall a b. (a -> b) -> a -> b
    $ LineNumber -> String
    forall a. Show a => a -> String
    show LineNumber
    l String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ": Missing field name"
              [String]
    hs  -> String -> ExceptT String (Writer [LibWarning']) [GenericLine]
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> ExceptT String (Writer [LibWarning']) [GenericLine])
    -> String -> ExceptT String (Writer [LibWarning']) [GenericLine]
    forall a b. (a -> b) -> a -> b
    $ LineNumber -> String
    forall a. Show a => a -> String
    show LineNumber
    l String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ": Bad field name " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    h
          (String, String)
    _ -> String -> ExceptT String (Writer [LibWarning']) [GenericLine]
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> ExceptT String (Writer [LibWarning']) [GenericLine])
    -> String -> ExceptT String (Writer [LibWarning']) [GenericLine]
    forall a b. (a -> b) -> a -> b
    $ LineNumber -> String
    forall a. Show a => a -> String
    show LineNumber
    l String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ": Missing ':' for field " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show (String -> String
    ltrim String
    s)

    -- | Collect 'Header' and subsequent 'Content's into 'GenericEntry'.
    --
    --   Tailing 'Content's?  That's an error.
    --
    groupLines :: [GenericLine] -> P GenericFile
    groupLines :: [GenericLine] -> ExceptT String (Writer [LibWarning']) GenericFile
    groupLines [] = GenericFile -> ExceptT String (Writer [LibWarning']) GenericFile
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure []
    groupLines (Content LineNumber
    l String
    c : [GenericLine]
    _) = String -> ExceptT String (Writer [LibWarning']) GenericFile
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> ExceptT String (Writer [LibWarning']) GenericFile)
    -> String -> ExceptT String (Writer [LibWarning']) GenericFile
    forall a b. (a -> b) -> a -> b
    $ LineNumber -> String
    forall a. Show a => a -> String
    show LineNumber
    l String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ": Missing field"
    groupLines (Header LineNumber
    _ String
    h : [GenericLine]
    ls) = (String -> [String] -> GenericEntry
    GenericEntry String
    h [ String
    c | Content LineNumber
    _ String
    c <- [GenericLine]
    cs ] GenericEntry -> GenericFile -> GenericFile
    forall a. a -> [a] -> [a]
    :) (GenericFile -> GenericFile)
    -> ExceptT String (Writer [LibWarning']) GenericFile
    -> ExceptT String (Writer [LibWarning']) GenericFile
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [GenericLine] -> ExceptT String (Writer [LibWarning']) GenericFile
    groupLines [GenericLine]
    ls1
      where
        ([GenericLine]
    cs, [GenericLine]
    ls1) = (GenericLine -> Bool)
    -> [GenericLine] -> ([GenericLine], [GenericLine])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    span GenericLine -> Bool
    isContent [GenericLine]
    ls
        isContent :: GenericLine -> Bool
    isContent Content{} = Bool
    True
        isContent Header{} = Bool
    False

    -- | Remove leading whitespace and line comment.
    trimLineComment :: String -> String
    trimLineComment :: String -> String
    trimLineComment = String -> String
    stripComments (String -> String) -> (String -> String) -> String -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> String
    ltrim

    -- | Break a comma-separated string.  Result strings are @trim@med.
    splitCommas :: String -> [String]
    splitCommas :: String -> [String]
    splitCommas String
    s = String -> [String]
    words (String -> [String]) -> String -> [String]
    forall a b. (a -> b) -> a -> b
    $ (Char -> Char) -> String -> String
    forall a b. (a -> b) -> [a] -> [b]
    map (\Char
    c -> if Char
    c Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    ',' then Char
    ' ' else Char
    c) String
    s

    -- | ...and trailing, but not leading, whitespace.
    stripComments :: String -> String
    stripComments :: String -> String
    stripComments String
    "" = String
    ""
    stripComments (Char
    '-':Char
    '-':Char
    c:String
    _) | Char -> Bool
    isSpace Char
    c = String
    ""
    stripComments (Char
    c : String
    s) = Char -> String -> String
    cons Char
    c (String -> String
    stripComments String
    s)
      where
        cons :: Char -> String -> String
    cons Char
    c String
    "" | Char -> Bool
    isSpace Char
    c = String
    ""
        cons Char
    c String
    s = Char
    c Char -> String -> String
    forall a. a -> [a] -> [a]
    : String
    s