    -- | 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 qualified Data.List as List
    import Data.Text (Text)
    import qualified Data.Text as T
    import System.FilePath

    import Agda.Interaction.Library.Base

    import Agda.Syntax.Position

    import Agda.Utils.Applicative
    import Agda.Utils.FileName
    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.List1             ( List1, toList )
    import qualified Agda.Utils.List1   as List1
    import qualified Agda.Utils.Maybe.Strict as Strict
    import Agda.Utils.Singleton
    import Agda.Utils.String            ( ltrim )

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

    runP :: P a -> (Either LibParseError a, [LibWarning'])
    runP :: forall a. P a -> (Either LibParseError a, [LibWarning'])
    runP = Writer [LibWarning'] (Either LibParseError a)
    -> (Either LibParseError a, [LibWarning'])
    forall w a. Writer w a -> (a, w)
    runWriter (Writer [LibWarning'] (Either LibParseError a)
     -> (Either LibParseError a, [LibWarning']))
    -> (P a -> Writer [LibWarning'] (Either LibParseError a))
    -> P a
    -> (Either LibParseError a, [LibWarning'])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . P a -> Writer [LibWarning'] (Either LibParseError 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 a. a -> [a]
    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    :: Range -> [String] -> P a
          -- ^ Content parser for this field.
          --
          -- The range points to the start of the file.
      , ()
    fSet      :: LensSet AgdaLibFile a
          -- ^ Sets parsed content in 'AgdaLibFile' structure.
      }

    optionalField ::
      String -> (Range -> [String] -> P a) -> Lens' AgdaLibFile a -> Field
    optionalField :: forall a.
    String
    -> (Range -> [String] -> P a) -> Lens' AgdaLibFile a -> Field
    optionalField String
    str Range -> [String] -> P a
    p Lens' AgdaLibFile a
    l = String
    -> Bool
    -> (Range -> [String] -> P a)
    -> LensSet AgdaLibFile a
    -> Field
    forall a.
    String
    -> Bool
    -> (Range -> [String] -> P a)
    -> LensSet AgdaLibFile a
    -> Field
    Field String
    str Bool
    True Range -> [String] -> P a
    p (Lens' AgdaLibFile a -> LensSet AgdaLibFile a
    forall o i. Lens' o i -> LensSet o i
    set (a -> f a) -> AgdaLibFile -> f AgdaLibFile
    Lens' AgdaLibFile a
    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
    -> (Range -> [String] -> P LibName)
    -> Lens' AgdaLibFile LibName
    -> Field
    forall a.
    String
    -> (Range -> [String] -> P a) -> Lens' AgdaLibFile a -> Field
    optionalField String
    "name"    (\Range
    _ -> [String] -> P LibName
    parseName)                     (LibName -> f LibName) -> AgdaLibFile -> f AgdaLibFile
    Lens' AgdaLibFile LibName
    libName
      , String
    -> (Range -> [String] -> P [String])
    -> Lens' AgdaLibFile [String]
    -> Field
    forall a.
    String
    -> (Range -> [String] -> P a) -> Lens' AgdaLibFile a -> Field
    optionalField String
    "include" (\Range
    _ -> [String] -> P [String]
    forall a. a -> ExceptT LibParseError (Writer [LibWarning']) a
    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)   ([String] -> f [String]) -> AgdaLibFile -> f AgdaLibFile
    Lens' AgdaLibFile [String]
    libIncludes
      , String
    -> (Range -> [String] -> P [LibName])
    -> Lens' AgdaLibFile [LibName]
    -> Field
    forall a.
    String
    -> (Range -> [String] -> P a) -> Lens' AgdaLibFile a -> Field
    optionalField String
    "depend"  (\Range
    _ -> [LibName] -> P [LibName]
    forall a. a -> ExceptT LibParseError (Writer [LibWarning']) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([LibName] -> P [LibName])
    -> ([String] -> [LibName]) -> [String] -> P [LibName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String -> LibName) -> [String] -> [LibName]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> LibName
    parseLibName ([String] -> [LibName])
    -> ([String] -> [String]) -> [String] -> [LibName]
    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)  ([LibName] -> f [LibName]) -> AgdaLibFile -> f AgdaLibFile
    Lens' AgdaLibFile [LibName]
    libDepends
      , String
    -> (Range -> [String] -> P OptionsPragma)
    -> Lens' AgdaLibFile OptionsPragma
    -> Field
    forall a.
    String
    -> (Range -> [String] -> P a) -> Lens' AgdaLibFile a -> Field
    optionalField String
    "flags"   (\Range
    r -> OptionsPragma -> P OptionsPragma
    forall a. a -> ExceptT LibParseError (Writer [LibWarning']) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (OptionsPragma -> P OptionsPragma)
    -> ([String] -> OptionsPragma) -> [String] -> P OptionsPragma
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String -> OptionsPragma) -> [String] -> OptionsPragma
    forall m a. Monoid m => (a -> m) -> [a] -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap (Range -> String -> OptionsPragma
    parseFlags Range
    r)) (OptionsPragma -> f OptionsPragma) -> AgdaLibFile -> f AgdaLibFile
    Lens' AgdaLibFile OptionsPragma
    libPragmas
      ]
      where
        parseName :: [String] -> P LibName
        parseName :: [String] -> P LibName
    parseName [String
    s] | [String
    name] <- String -> [String]
    words String
    s = LibName -> P LibName
    forall a. a -> ExceptT LibParseError (Writer [LibWarning']) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (LibName -> P LibName) -> LibName -> P LibName
    forall a b. (a -> b) -> a -> b
    $ String -> LibName
    parseLibName String
    name
        parseName [String]
    ls = LibParseError -> P LibName
    forall a.
    LibParseError -> ExceptT LibParseError (Writer [LibWarning']) a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (LibParseError -> P LibName) -> LibParseError -> P LibName
    forall a b. (a -> b) -> a -> b
    $ String -> LibParseError
    BadLibraryName (String -> LibParseError) -> String -> LibParseError
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unwords [String]
    ls

        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 a. 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 :: Range -> String -> OptionsPragma
        parseFlags :: Range -> String -> OptionsPragma
    parseFlags Range
    r String
    s = OptionsPragma
          { pragmaStrings :: [String]
    pragmaStrings = String -> [String]
    words String
    s
          , pragmaRange :: Range
    pragmaRange   = Range
    r
          }

    -- | 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 = do
      abs <- String -> IO AbsolutePath
    absolute String
    file
      (fmap setPath . parseLib abs <$> UTF8.readFile file) `catchIO` \IOException
    e ->
        P AgdaLibFile -> IO (P AgdaLibFile)
    forall a. a -> IO a
    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
    $ LibParseError -> P AgdaLibFile
    forall a.
    LibParseError -> ExceptT LibParseError (Writer [LibWarning']) a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (LibParseError -> P AgdaLibFile) -> LibParseError -> P AgdaLibFile
    forall a b. (a -> b) -> a -> b
    $ String -> IOException -> LibParseError
    ReadFailure String
    file IOException
    e
      where
        setPath :: AgdaLibFile -> AgdaLibFile
    setPath      AgdaLibFile
    lib = String -> AgdaLibFile -> AgdaLibFile
    unrelativise (String -> String
    takeDirectory String
    file) (Lens' AgdaLibFile String -> String -> AgdaLibFile -> AgdaLibFile
    forall o i. Lens' o i -> LensSet o i
    set (String -> f String) -> AgdaLibFile -> f AgdaLibFile
    Lens' AgdaLibFile String
    libFile String
    file AgdaLibFile
    lib)
        unrelativise :: String -> AgdaLibFile -> AgdaLibFile
    unrelativise String
    dir = Lens' AgdaLibFile [String] -> LensMap AgdaLibFile [String]
    forall o i. Lens' o i -> LensMap o i
    over ([String] -> f [String]) -> AgdaLibFile -> f AgdaLibFile
    Lens' AgdaLibFile [String]
    libIncludes ((String -> String) -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String
    dir String -> String -> String
    </>))

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

    -- | Parse 'GenericFile' with 'agdaLibFields' descriptors.
    fromGeneric
      :: AbsolutePath
         -- ^ The parsed file.
      -> GenericFile
      -> P AgdaLibFile
    fromGeneric :: AbsolutePath -> GenericFile -> P AgdaLibFile
    fromGeneric AbsolutePath
    file = AbsolutePath -> [Field] -> GenericFile -> P AgdaLibFile
    fromGeneric' AbsolutePath
    file [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'
      :: AbsolutePath
         -- ^ The parsed file.
      -> [Field]
      -> GenericFile
      -> P AgdaLibFile
    fromGeneric' :: AbsolutePath -> [Field] -> GenericFile -> P AgdaLibFile
    fromGeneric' AbsolutePath
    file [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
        -- The range points to the start of the file.
        r :: Range
    r = Maybe RangeFile -> Seq (Interval' ()) -> Range
    forall a. a -> Seq (Interval' ()) -> Range' a
    Range
              (RangeFile -> Maybe RangeFile
    forall a. a -> Maybe a
    Strict.Just (RangeFile -> Maybe RangeFile) -> RangeFile -> Maybe RangeFile
    forall a b. (a -> b) -> a -> b
    $ AbsolutePath -> Maybe (TopLevelModuleName' Range) -> RangeFile
    mkRangeFile AbsolutePath
    file Maybe (TopLevelModuleName' Range)
    forall a. Maybe a
    Nothing)
              (Interval' () -> Seq (Interval' ())
    forall el coll. Singleton el coll => el -> coll
    singleton (() -> PositionWithoutFile -> PositionWithoutFile -> Interval' ()
    forall a.
    a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a
    posToInterval () PositionWithoutFile
    p PositionWithoutFile
    p))
          where
          p :: PositionWithoutFile
    p = Pn { srcFile :: ()
    srcFile = ()
                 , posPos :: Word32
    posPos  = Word32
    1
                 , posLine :: Word32
    posLine = Word32
    1
                 , posCol :: Word32
    posCol  = Word32
    1
                 }

        upd :: AgdaLibFile -> GenericEntry -> P AgdaLibFile
        upd :: AgdaLibFile -> GenericEntry -> P AgdaLibFile
    upd AgdaLibFile
    l (GenericEntry String
    h [String]
    cs) = do
          mf <- String -> [Field] -> P (Maybe Field)
    findField String
    h [Field]
    fields
          case mf of
            Just Field{Bool
    String
    LensSet AgdaLibFile a
    Range -> [String] -> P a
    fName :: Field -> String
    fOptional :: Field -> Bool
    fParse :: ()
    fSet :: ()
    fName :: String
    fOptional :: Bool
    fParse :: Range -> [String] -> P a
    fSet :: LensSet AgdaLibFile a
    ..} -> do
              x <- Range -> [String] -> P a
    fParse Range
    r [String]
    cs
              return $ fSet x l
            Maybe Field
    Nothing -> AgdaLibFile -> P AgdaLibFile
    forall a. a -> ExceptT LibParseError (Writer [LibWarning']) a
    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
      -- Report missing mandatory fields.
      () <- [String] -> (List1 String -> P ()) -> P ()
    forall (m :: * -> *) a.
    Applicative m =>
    [a] -> (List1 a -> m ()) -> m ()
    List1.unlessNull [String]
    missing ((List1 String -> P ()) -> P ()) -> (List1 String -> P ()) -> P ()
    forall a b. (a -> b) -> a -> b
    $ LibParseError -> P ()
    forall a.
    LibParseError -> ExceptT LibParseError (Writer [LibWarning']) a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (LibParseError -> P ())
    -> (List1 String -> LibParseError) -> List1 String -> P ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 String -> LibParseError
    MissingFields
      -- Report duplicate fields.
      List1.unlessNull (duplicates fs) $ throwError . DuplicateFields
      where
      mandatory :: [String]
      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   :: [String]
      missing :: [String]
    missing   = [String]
    mandatory [String] -> [String] -> [String]
    forall a. Eq a => [a] -> [a] -> [a]
    List.\\ [String]
    fs

    -- | 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 a. a -> ExceptT LibParseError (Writer [LibWarning']) a
    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 a b.
    ExceptT LibParseError (Writer [LibWarning']) a
    -> ExceptT LibParseError (Writer [LibWarning']) b
    -> ExceptT LibParseError (Writer [LibWarning']) b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Maybe Field -> P (Maybe Field)
    forall a. a -> ExceptT LibParseError (Writer [LibWarning']) a
    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 LibParseError (Writer [LibWarning']) GenericFile
    parseGeneric String
    s =
      [GenericLine]
    -> ExceptT LibParseError (Writer [LibWarning']) GenericFile
    groupLines ([GenericLine]
     -> ExceptT LibParseError (Writer [LibWarning']) GenericFile)
    -> ExceptT LibParseError (Writer [LibWarning']) [GenericLine]
    -> ExceptT LibParseError (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 LibParseError (Writer [LibWarning']) [[GenericLine]]
    -> ExceptT LibParseError (Writer [LibWarning']) [GenericLine]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (LineNumber
     -> String
     -> ExceptT LibParseError (Writer [LibWarning']) [GenericLine])
    -> [LineNumber]
    -> [String]
    -> ExceptT LibParseError (Writer [LibWarning']) [[GenericLine]]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM LineNumber
    -> String
    -> ExceptT LibParseError (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
    $cshowsPrec :: LineNumber -> GenericLine -> String -> String
    showsPrec :: LineNumber -> GenericLine -> String -> String
    $cshow :: GenericLine -> String
    show :: GenericLine -> String
    $cshowList :: [GenericLine] -> String -> String
    showList :: [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 LibParseError (Writer [LibWarning']) [GenericLine]
    parseLine LineNumber
    _ String
    "" = [GenericLine]
    -> ExceptT LibParseError (Writer [LibWarning']) [GenericLine]
    forall a. a -> ExceptT LibParseError (Writer [LibWarning']) a
    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 LibParseError (Writer [LibWarning']) [GenericLine]
    forall a. a -> ExceptT LibParseError (Writer [LibWarning']) a
    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 LibParseError (Writer [LibWarning']) [GenericLine]
    forall a. a -> ExceptT LibParseError (Writer [LibWarning']) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([GenericLine]
     -> ExceptT LibParseError (Writer [LibWarning']) [GenericLine])
    -> [GenericLine]
    -> ExceptT LibParseError (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 a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null String
    r')]
              []  -> LibParseError
    -> ExceptT LibParseError (Writer [LibWarning']) [GenericLine]
    forall a.
    LibParseError -> ExceptT LibParseError (Writer [LibWarning']) a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (LibParseError
     -> ExceptT LibParseError (Writer [LibWarning']) [GenericLine])
    -> LibParseError
    -> ExceptT LibParseError (Writer [LibWarning']) [GenericLine]
    forall a b. (a -> b) -> a -> b
    $ LineNumber -> LibParseError
    MissingFieldName LineNumber
    l
              [String]
    hs  -> LibParseError
    -> ExceptT LibParseError (Writer [LibWarning']) [GenericLine]
    forall a.
    LibParseError -> ExceptT LibParseError (Writer [LibWarning']) a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (LibParseError
     -> ExceptT LibParseError (Writer [LibWarning']) [GenericLine])
    -> LibParseError
    -> ExceptT LibParseError (Writer [LibWarning']) [GenericLine]
    forall a b. (a -> b) -> a -> b
    $ LineNumber -> String -> LibParseError
    BadFieldName LineNumber
    l String
    h
          (String, String)
    _ -> LibParseError
    -> ExceptT LibParseError (Writer [LibWarning']) [GenericLine]
    forall a.
    LibParseError -> ExceptT LibParseError (Writer [LibWarning']) a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (LibParseError
     -> ExceptT LibParseError (Writer [LibWarning']) [GenericLine])
    -> LibParseError
    -> ExceptT LibParseError (Writer [LibWarning']) [GenericLine]
    forall a b. (a -> b) -> a -> b
    $ LineNumber -> String -> LibParseError
    MissingColonForField LineNumber
    l (String -> String
    ltrim String
    s)

    -- | Collect 'Header' and subsequent 'Content's into 'GenericEntry'.
    --
    --   Leading 'Content's?  That's an error.
    --
    groupLines :: [GenericLine] -> P GenericFile
    groupLines :: [GenericLine]
    -> ExceptT LibParseError (Writer [LibWarning']) GenericFile
    groupLines [] = GenericFile
    -> ExceptT LibParseError (Writer [LibWarning']) GenericFile
    forall a. a -> ExceptT LibParseError (Writer [LibWarning']) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure []
    groupLines (Content LineNumber
    l String
    c : [GenericLine]
    _) = LibParseError
    -> ExceptT LibParseError (Writer [LibWarning']) GenericFile
    forall a.
    LibParseError -> ExceptT LibParseError (Writer [LibWarning']) a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (LibParseError
     -> ExceptT LibParseError (Writer [LibWarning']) GenericFile)
    -> LibParseError
    -> ExceptT LibParseError (Writer [LibWarning']) GenericFile
    forall a b. (a -> b) -> a -> b
    $ LineNumber -> LibParseError
    ContentWithoutField LineNumber
    l
    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 LibParseError (Writer [LibWarning']) GenericFile
    -> ExceptT LibParseError (Writer [LibWarning']) GenericFile
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [GenericLine]
    -> ExceptT LibParseError (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 -> [String]
    words (String -> [String]) -> (String -> String) -> String -> [String]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (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)

    -- | ...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