diff options
Diffstat (limited to 'src/Verismith/CounterEg.hs')
| -rw-r--r-- | src/Verismith/CounterEg.hs | 105 |
1 files changed, 54 insertions, 51 deletions
diff --git a/src/Verismith/CounterEg.hs b/src/Verismith/CounterEg.hs index a2e1210..f378baf 100644 --- a/src/Verismith/CounterEg.hs +++ b/src/Verismith/CounterEg.hs @@ -1,44 +1,44 @@ -{-| -Module : Verismith.CounterEg -Description : Counter example parser to load the counter example -Copyright : (c) 2019, Yann Herklotz -License : GPL-3 -Maintainer : yann [at] yannherklotz [dot] com -Stability : experimental -Portability : POSIX --} - +-- | +-- Module : Verismith.CounterEg +-- Description : Counter example parser to load the counter example +-- Copyright : (c) 2019, Yann Herklotz +-- License : GPL-3 +-- Maintainer : yann [at] yannherklotz [dot] com +-- Stability : experimental +-- Portability : POSIX module Verismith.CounterEg - ( CounterEg(..) - , parseCounterEg - ) + ( CounterEg (..), + parseCounterEg, + ) where -import Control.Applicative ((<|>)) -import Data.Bifunctor (bimap) -import Data.Binary (encode) -import Data.Bits (shiftL, (.|.)) -import Data.ByteString (ByteString) -import qualified Data.ByteString as B +import Control.Applicative ((<|>)) +import Data.Bifunctor (bimap) +import Data.Binary (encode) +import Data.Bits ((.|.), shiftL) +import Data.ByteString (ByteString) +import qualified Data.ByteString as B import qualified Data.ByteString.Lazy as L -import Data.Char (digitToInt) -import Data.Functor (($>)) -import Data.Maybe (listToMaybe) -import Data.Text (Text) -import qualified Data.Text as T -import Numeric (readInt) -import qualified Text.Parsec as P - -data CounterEg = CounterEg { _counterEgInitial :: ![(Text, Text)] - , _counterEgStates :: ![[(Text, Text)]] - } - deriving (Eq, Show) +import Data.Char (digitToInt) +import Data.Functor (($>)) +import Data.Maybe (listToMaybe) +import Data.Text (Text) +import qualified Data.Text as T +import Numeric (readInt) +import qualified Text.Parsec as P + +data CounterEg + = CounterEg + { _counterEgInitial :: ![(Text, Text)], + _counterEgStates :: ![[(Text, Text)]] + } + deriving (Eq, Show) instance Semigroup CounterEg where - CounterEg a b <> CounterEg c d = CounterEg (a <> c) (b <> d) + CounterEg a b <> CounterEg c d = CounterEg (a <> c) (b <> d) instance Monoid CounterEg where - mempty = CounterEg mempty mempty + mempty = CounterEg mempty mempty type Parser = P.Parsec String () @@ -57,11 +57,12 @@ type Parser = P.Parsec String () -- convertBinary = fromBytes . convert lexme :: Parser a -> Parser a -lexme f = do { a <- f; _ <- P.spaces; return a } +lexme f = do a <- f; _ <- P.spaces; return a nameChar :: Parser Char -nameChar = P.alphaNum - <|> P.oneOf "$.:_" +nameChar = + P.alphaNum + <|> P.oneOf "$.:_" parens :: Parser a -> Parser a parens = lexme . P.between (P.char '(') (P.char ')') @@ -74,39 +75,41 @@ trueOrFalse = lexme $ (P.string "true" $> "1") <|> (P.string "false" $> "0") assumeBody :: Parser (String, String) assumeBody = lexme $ do - name <- P.char '=' *> P.spaces *> brackets (P.many1 nameChar) - num <- P.spaces *> ((P.string "#b" *> P.many1 P.digit) <|> trueOrFalse) - return (name, num) + name <- P.char '=' *> P.spaces *> brackets (P.many1 nameChar) + num <- P.spaces *> ((P.string "#b" *> P.many1 P.digit) <|> trueOrFalse) + return (name, num) parseAssume :: Parser (String, String) parseAssume = lexme $ P.string "assume" *> P.spaces *> parens assumeBody parseInitial :: Parser [(String, String)] parseInitial = lexme $ do - _ <- lexme $ P.string "initial" - P.many parseAssume + _ <- lexme $ P.string "initial" + P.many parseAssume parseState :: Parser (String, [(String, String)]) parseState = lexme $ do - n <- lexme $ P.string "state" *> P.spaces *> P.many1 P.digit - assumes <- P.many parseAssume - return (n, assumes) + n <- lexme $ P.string "state" *> P.spaces *> P.many1 P.digit + assumes <- P.many parseAssume + return (n, assumes) parseCE :: Parser [[(String, String)]] parseCE = lexme $ do - i <- parseInitial - other <- fmap snd <$> P.many parseState - return (i : other) + i <- parseInitial + other <- fmap snd <$> P.many parseState + return (i : other) cEtoCounterEg :: [[(String, String)]] -> CounterEg cEtoCounterEg [] = mempty -cEtoCounterEg (i : is) = CounterEg (bimap T.pack T.pack <$> i) - (fmap (bimap T.pack T.pack) <$> is) +cEtoCounterEg (i : is) = + CounterEg + (bimap T.pack T.pack <$> i) + (fmap (bimap T.pack T.pack) <$> is) parseCounterEg' :: Parser CounterEg parseCounterEg' = lexme $ do - _ <- P.spaces - cEtoCounterEg <$> parseCE + _ <- P.spaces + cEtoCounterEg <$> parseCE parseCounterEg :: Text -> Either String CounterEg parseCounterEg = bimap show id . P.parse parseCounterEg' "" . T.unpack |