diff options
Diffstat (limited to 'src/Verismith/CounterEg.hs')
-rw-r--r-- | src/Verismith/CounterEg.hs | 112 |
1 files changed, 112 insertions, 0 deletions
diff --git a/src/Verismith/CounterEg.hs b/src/Verismith/CounterEg.hs new file mode 100644 index 0000000..f5547ed --- /dev/null +++ b/src/Verismith/CounterEg.hs @@ -0,0 +1,112 @@ +{-| +Module : Verismith.CounterEg +Description : Counter example parser to load the counter example +Copyright : (c) 2019, Yann Herklotz +License : BSD-3 +Maintainer : yann [at] yannherklotz [dot] com +Stability : experimental +Portability : POSIX +-} + +module Verismith.CounterEg + ( 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 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, Int)] + , _counterEgStates :: ![[(Text, Int)]] + } + deriving (Eq, Show) + +instance Semigroup CounterEg where + CounterEg a b <> CounterEg c d = CounterEg (a <> c) (b <> d) + +instance Monoid CounterEg where + mempty = CounterEg mempty mempty + +type Parser = P.Parsec String () + +fromBytes :: ByteString -> Int +fromBytes = B.foldl' f 0 where f a b = a `shiftL` 8 .|. fromIntegral b + +convert :: String -> ByteString +convert = + L.toStrict + . (encode :: Integer -> L.ByteString) + . maybe 0 fst + . listToMaybe + . readInt 2 (`elem` ("01" :: String)) digitToInt + +convertBinary :: String -> Int +convertBinary = fromBytes . convert + +lexme :: Parser a -> Parser a +lexme f = do { a <- f; _ <- P.spaces; return a } + +nameChar :: Parser Char +nameChar = P.alphaNum + <|> P.oneOf "$.:_" + +parens :: Parser a -> Parser a +parens = lexme . P.between (P.char '(') (P.char ')') + +brackets :: Parser a -> Parser a +brackets = lexme . P.between (P.char '[') (P.char ']') + +trueOrFalse :: Parser String +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) + +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 + +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) + +parseCE :: Parser [[(String, String)]] +parseCE = lexme $ do + i <- parseInitial + other <- fmap snd <$> P.many parseState + return (i : other) + +cEtoCounterEg :: [[(String, String)]] -> CounterEg +cEtoCounterEg [] = mempty +cEtoCounterEg (i : is) = CounterEg (bimap T.pack convertBinary <$> i) + (fmap (bimap T.pack convertBinary) <$> is) + +parseCounterEg' :: Parser CounterEg +parseCounterEg' = lexme $ do + _ <- P.spaces + cEtoCounterEg <$> parseCE + +parseCounterEg :: Text -> Either String CounterEg +parseCounterEg = bimap show id . P.parse parseCounterEg' "" . T.unpack |