{-# LANGUAGE DeriveDataTypeable #-}
module Agda.Interaction.Library.Parse
( parseLibFile
, splitCommas
, trimLineComment
, LineNumber
, runP
, LibWarning'(..)
) where
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.Applicative
import Agda.Utils.Except ( MonadError(throwError), ExceptT, runExceptT )
import Agda.Utils.IO ( catchIO )
import Agda.Utils.Lens
import Agda.Utils.List ( duplicates )
import Agda.Utils.String ( ltrim )
type P = ExceptT String (Writer [LibWarning'])
runP :: P a -> (Either String a, [LibWarning'])
runP = runWriter . runExceptT
data LibWarning'
= UnknownField String
deriving (Show, Data)
warningP :: LibWarning' -> P ()
warningP = tell . pure
type GenericFile = [GenericEntry]
data GenericEntry = GenericEntry
{ geHeader :: String
, _geContent :: [String]
}
data Field = forall a. Field
{ fName :: String
, fOptional :: Bool
, fParse :: [String] -> P a
, fSet :: LensSet a AgdaLibFile
}
optionalField :: String -> ([String] -> P a) -> Lens' a AgdaLibFile -> Field
optionalField str p l = Field str True p (set l)
agdaLibFields :: [Field]
agdaLibFields =
[ optionalField "name" parseName libName
, optionalField "include" (pure . concatMap parsePaths) libIncludes
, optionalField "depend" (pure . concatMap splitCommas) libDepends
]
where
parseName :: [String] -> P LibName
parseName [s] | [name] <- words s = pure name
parseName ls = throwError $ "Bad library name: '" ++ unwords ls ++ "'"
parsePaths :: String -> [FilePath]
parsePaths = go id where
fixup acc = let fp = acc [] in not (null fp) ?$> fp
go acc [] = fixup acc
go acc ('\\' : ' ' :cs) = go (acc . (' ':)) cs
go acc ('\\' : '\\' :cs) = go (acc . ('\\':)) cs
go acc ( ' ' :cs) = fixup acc ++ go id cs
go acc (c :cs) = go (acc . (c:)) cs
parseLibFile :: FilePath -> IO (P AgdaLibFile)
parseLibFile file =
(fmap setPath . parseLib <$> readFile file) `catchIO` \e ->
return $ throwError $ unlines
[ "Failed to read library file " ++ file ++ "."
, "Reason: " ++ show e
]
where
setPath lib = unrelativise (takeDirectory file) (set libFile file lib)
unrelativise dir = over libIncludes (map (dir </>))
parseLib :: String -> P AgdaLibFile
parseLib s = fromGeneric =<< parseGeneric s
fromGeneric :: GenericFile -> P AgdaLibFile
fromGeneric = fromGeneric' agdaLibFields
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
checkFields :: [Field] -> [String] -> P ()
checkFields fields fs = do
let mandatory = [ fName f | f <- fields, not $ fOptional f ]
missing = mandatory List.\\ fs
dup = duplicates fs
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
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
parseGeneric :: String -> P GenericFile
parseGeneric s =
groupLines =<< concat <$> mapM (uncurry parseLine) (zip [1..] $ map stripComments $ lines s)
type LineNumber = Int
data GenericLine
= Header LineNumber String
| Content LineNumber String
deriving (Show)
parseLine :: LineNumber -> String -> P [GenericLine]
parseLine _ "" = pure []
parseLine l s@(c:_)
| isSpace c = pure [Content l $ ltrim s]
| otherwise =
case break (==':') s of
(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)
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
trimLineComment :: String -> String
trimLineComment = stripComments . ltrim
splitCommas :: String -> [String]
splitCommas s = words $ map (\c -> if c == ',' then ' ' else c) s
stripComments :: String -> String
stripComments "" = ""
stripComments ('-':'-':_) = ""
stripComments (c : s) = cons c (stripComments s)
where
cons c "" | isSpace c = ""
cons c s = c : s