diff --git a/peregrine.cabal b/peregrine.cabal index ebeaf66f61e82554a6ae2876f71a9391a7ec8e6a..fe29c61a580d123398550d41436a9c20234a633d 100644 --- a/peregrine.cabal +++ b/peregrine.cabal @@ -22,8 +22,8 @@ executable peregrine main-is: Main.hs other-modules: -- other-extensions: - build-depends: base >=4 && <5, sbv, parsec, containers, transformers, - bytestring, mtl, stm, async, parallel-io + build-depends: base >=4 && <5, sbv, parsec >= 3.1, containers, transformers, + bytestring, mtl, stm, async, parallel-io, text, aeson hs-source-dirs: src default-language: Haskell2010 ghc-options: -fsimpl-tick-factor=1000 -threaded -rtsopts -with-rtsopts=-N diff --git a/src/Parser.hs b/src/Parser.hs index d324c274f3ff4a6938b445d248aed8681515c9bc..ccb51c9b57b5ff1d89bc31e87bd96a3cb347d901 100644 --- a/src/Parser.hs +++ b/src/Parser.hs @@ -3,6 +3,8 @@ module Parser where import Text.Parsec +import qualified Data.Text as T +import qualified Data.Text.IO as TIO type Parser a = Parsec String () a @@ -14,7 +16,7 @@ parseString p str = parseFile :: Parser a -> String -> IO a parseFile p file = do - contents <- readFile file - case parse p file contents of + contents <- T.unpack <$> TIO.readFile file + case parse p file contents of Left e -> print e >> fail "parse error" Right r -> return r diff --git a/src/Parser/PP.hs b/src/Parser/PP.hs index ef387d9b6c266618be4b634407796580e5aa8da8..67310f5991af86ea2b0d75edd69d59600dec557e 100644 --- a/src/Parser/PP.hs +++ b/src/Parser/PP.hs @@ -1,14 +1,22 @@ +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE OverloadedStrings #-} + module Parser.PP (parseContent) where +import Data.Aeson +import Data.Aeson.TH (deriveJSON, defaultOptions) import Control.Applicative ((<*),(*>),(<$>)) import Data.Functor.Identity import Text.Parsec +import qualified Data.Set as S +import qualified Data.ByteString.Lazy.Char8 as BS +import qualified Data.Text as T import Text.Parsec.Expr import Text.Parsec.Language (LanguageDef, emptyDef) import qualified Text.Parsec.Token as Token - import Parser import PopulationProtocol (PopulationProtocol,makePopulationProtocolFromStrings,State(..),Transition(..)) import Property @@ -25,7 +33,7 @@ languageDef = Token.reservedOpNames = ["->", "<", "<=", "=", "!=", ">=", ">", "+", "-", "*", "&&", "||", "!", ":"] } - + lexer :: Token.TokenParser () lexer = Token.makeTokenParser languageDef @@ -68,78 +76,6 @@ ident = (identifier <|> stringLiteral) "identifier" identList :: Parser [String] identList = singleOrList ident -states :: Parser [String] -states = reserved "states" *> identList - -transitions :: Parser [String] -transitions = reserved "transitions" *> identList - -initial :: Parser [String] -initial = reserved "initial" *> identList - -trueStates :: Parser [String] -trueStates = reserved "true" *> identList - -falseStates :: Parser [String] -falseStates = reserved "false" *> identList - -arc :: Parser [(String,String,Integer)] -arc = do - lhs <- identList - rhsList <- many1 (do - reservedOp "->" - w <- numberOption - ids <- identList - return (ids,w) - ) - return $ fst $ foldl makeArc ([],lhs) rhsList - where - makeArc (as,lhs) (rhs,w) = ([(l,r,w) | l <- lhs, r <- rhs] ++ as, rhs) - -arcs :: Parser [(String,String,Integer)] -arcs = do - reserved "arcs" - as <- singleOrList arc - return $ concat as - -data Statement = States [String] - | Transitions [String] - | Initial [String] - | TrueStatement [String] - | FalseStatement [String] - | PredicateStatement (QuantFormula String) - | Arcs [(String,String,Integer)] - -statement :: Parser Statement -statement = States <$> states <|> - Transitions <$> transitions <|> - Arcs <$> arcs <|> - Initial <$> initial <|> - TrueStatement <$> trueStates <|> - FalseStatement <$> falseStates <|> - PredicateStatement <$> predicate - -populationProtocol :: Parser PopulationProtocol -populationProtocol = do - reserved "population" - reserved "protocol" - name <- option "" ident - statements <- braces (many statement) - let (qs,ts,qinitial,qtrue,qfalse,ps,as) = foldl splitStatement ([],[],[],[],[],Nothing,[]) statements - let predicate = case ps of - Nothing -> ExQuantFormula [] FTrue - Just p -> p - return $ makePopulationProtocolFromStrings name qs ts qinitial qtrue qfalse predicate as - where - splitStatement (qs,ts,qinitial,qtrue,qfalse,ps,as) stmnt = case stmnt of - States q -> (q ++ qs,ts,qinitial,qtrue,qfalse,ps,as) - Transitions t -> (qs,t ++ ts,qinitial,qtrue,qfalse,ps,as) - Initial q -> (qs,ts,q ++ qinitial,qtrue,qfalse,ps,as) - TrueStatement q -> (qs,ts,qinitial,q ++ qtrue,qfalse,ps,as) - FalseStatement q -> (qs,ts,qinitial,qtrue,q ++ qfalse,ps,as) - PredicateStatement p -> (qs,ts,qinitial,qtrue,qfalse,Just p,as) - Arcs a -> (qs,ts,qinitial,qtrue,qfalse,ps,a ++ as) - binary :: String -> (a -> a -> a) -> Assoc -> Operator String () Identity a binary name fun = Infix ( reservedOp name *> return fun ) prefix :: String -> (a -> a) -> Operator String () Identity a @@ -205,16 +141,50 @@ quantFormula = <|> (ExQuantFormula [] <$> formula) -predicate :: Parser (QuantFormula String) -predicate = do - reserved "predicate" - form <- braces quantFormula - return form +instance FromJSON (QuantFormula String) where + parseJSON (String v) = do + let formula = parse quantFormula "" (T.unpack v) + case formula of + Left e -> fail "Predicate formula not well-formed." + Right r -> return r + parseJSON _ = fail "Expect string for predicate." + +instance ToJSON (QuantFormula String) where + toJSON x = String "" + +data RecordTransition = RecordTransition { + name :: String, + pre :: [String], + post :: [String] +} deriving (Show) + +data RecordPP = RecordPP { + title :: String, + states :: [String], + transitions :: [RecordTransition], + initialStates :: [String], + trueStates :: [String], + predicate :: Maybe (QuantFormula String) +} deriving (Show) + +$(deriveJSON defaultOptions ''RecordTransition) +$(deriveJSON defaultOptions ''RecordPP) + +recordPP2PopulationProtocol :: RecordPP -> PopulationProtocol +recordPP2PopulationProtocol r = + makePopulationProtocolFromStrings (title r) (states r) (map name (transitions r)) (initialStates r) (trueStates r) falseStates p arcs where + falseStates = [q | q <- states r, not (S.member q (S.fromList (trueStates r)))] + count = \x -> length . (filter (== x)) + arcs = [(name t, q, toInteger m) | t <- transitions r, q <- (pre t ++ post t), let m = (count q) (post t) - (count q) (pre t)] + p = case predicate r of Nothing -> ExQuantFormula [] FTrue + (Just p') -> p' parseContent :: Parser PopulationProtocol -parseContent = do - whiteSpace - pp <- populationProtocol - properties <- many predicate - eof - return pp +parseContent = do + str <- manyTill anyChar eof + let r = eitherDecode (BS.pack str) + case r of + (Left e) -> fail e + (Right pp) -> return (recordPP2PopulationProtocol pp) + +