    {-# LANGUAGE DeriveDataTypeable #-}
    -- | 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
      , LineNumber
      , runP
      , LibWarning'(..)
      ) where

    import Control.Exception
    import Control.Monad
    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.Except ( MonadError(throwError), ExceptT, runExceptT )
    import Agda.Utils.IO ( catchIO )
    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 = runWriter . runExceptT

    -- | Library Warnings.
    data LibWarning'
      = UnknownField String
      deriving (Show, Data)

    warningP :: LibWarning' -> P ()
    warningP = tell . pure

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

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

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

    -- | @.agda-lib@ file format with parsers and setters.
    agdaLibFields :: [Field]
    agdaLibFields =
      -- Andreas, 2017-08-23, issue #2708, field "name" is optional.
      [ Field "name"    True  parseName                      $ \ name l -> l { libName     = name }
      , Field "include" True  (pure . concatMap words)       $ \ inc  l -> l { libIncludes = inc }
      , Field "depend"  True  (pure . concatMap splitCommas) $ \ ds   l -> l { libDepends  = ds }
      ]
      where
        parseName [s] | [name] <- words s = pure name
        parseName ls = throwError $ "Bad library name: '" ++ unwords ls ++ "'"

    -- | 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 file =
      (fmap setPath . parseLib <$> readFile file) `catchIO` \e ->
        return $ throwError $ "Failed to read library file " ++ file ++ ".\nReason: " ++ show e
      where
        setPath lib = unrelativise (takeDirectory file) lib{ libFile = file }
        unrelativise dir lib = lib { libIncludes = map (dir </>) (libIncludes lib) }

    -- | Parse file contents.
    parseLib :: String -> P AgdaLibFile
    parseLib s = fromGeneric =<< parseGeneric s

    -- | Parse 'GenericFile' with 'agdaLibFields' descriptors.
    fromGeneric :: GenericFile -> P AgdaLibFile
    fromGeneric = fromGeneric' 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' fields fs = do
      checkFields fields (map geHeader fs)
      foldM upd emptyLibFile fs
      where
        upd :: AgdaLibFile -> GenericEntry -> P AgdaLibFile
        upd l (GenericEntry h cs) = do
          mf <- findField h fields
          case mf of
            Just Field{..} -> do
              x <- fParse cs
              return $ fSet x l
            Nothing -> return l

    -- | Ensure that there are no duplicate fields and no mandatory fields are missing.
    checkFields :: [Field] -> [String] -> P ()
    checkFields fields fs = do
      let mandatory = [ fName f | f <- fields, not $ fOptional f ]
          -- Missing fields.
          missing   = mandatory List.\\ fs
          -- Duplicate fields.
          dup       = fs List.\\ List.nub fs
          -- Plural s for error message.
          s xs      = if length xs > 1 then "s" else ""
          list xs   = List.intercalate ", " [ "'" ++ f ++ "'" | f <- xs ]
      when (not $ null missing) $ throwError $ "Missing field" ++ s missing ++ " " ++ list missing
      when (not $ null dup)     $ throwError $ "Duplicate field" ++ s dup ++ " " ++ list dup

    -- | Find 'Field' with given 'fName', throw error if unknown.
    findField :: String -> [Field] -> P (Maybe Field)
    findField s fs = maybe err (return . Just) $ List.find ((s ==) . fName) fs
      where err = warningP (UnknownField s) >> return 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 s =
      groupLines =<< concat <$> mapM (uncurry parseLine) (zip [1..] $ map stripComments $ lines s)

    type LineNumber = Int

    -- | 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 (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 _ "" = pure []
    parseLine l s@(c:_)
        -- Indented lines are 'Content'.
      | isSpace c   = pure [Content l $ ltrim s]
        -- Non-indented lines are 'Header'.
      | otherwise   =
        case break (==':') s of
          -- Headers are single words followed by a colon.
          -- Anything after the colon that is not whitespace is 'Content'.
          (h, ':' : r) ->
            case words h of
              [h] -> pure $ [Header l h] ++ [Content l r' | let r' = ltrim r, not (null r')]
              []  -> throwError $ show l ++ ": Missing field name"
              hs  -> throwError $ show l ++ ": Bad field name " ++ show h
          _ -> throwError $ show l ++ ": Missing ':' for field " ++ show (ltrim s)

    -- | Collect 'Header' and subsequent 'Content's into 'GenericEntry'.
    --
    --   Tailing 'Content's?  That's an error.
    --
    groupLines :: [GenericLine] -> P GenericFile
    groupLines [] = pure []
    groupLines (Content l c : _) = throwError $ show l ++ ": Missing field"
    groupLines (Header _ h : ls) = (GenericEntry h [ c | Content _ c <- cs ] :) <$> groupLines ls1
      where
        (cs, ls1) = span isContent ls
        isContent Content{} = True
        isContent Header{} = False

    -- | Remove leading whitespace and line comment.
    trimLineComment :: String -> String
    trimLineComment = stripComments . ltrim

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

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