-- |
-- 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,
  )
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
  { CounterEg -> [(Text, Text)]
_counterEgInitial :: ![(Text, Text)],
    CounterEg -> [[(Text, Text)]]
_counterEgStates :: ![[(Text, Text)]]
  }
  deriving (CounterEg -> CounterEg -> Bool
(CounterEg -> CounterEg -> Bool)
-> (CounterEg -> CounterEg -> Bool) -> Eq CounterEg
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CounterEg -> CounterEg -> Bool
== :: CounterEg -> CounterEg -> Bool
$c/= :: CounterEg -> CounterEg -> Bool
/= :: CounterEg -> CounterEg -> Bool
Eq, Int -> CounterEg -> ShowS
[CounterEg] -> ShowS
CounterEg -> String
(Int -> CounterEg -> ShowS)
-> (CounterEg -> String)
-> ([CounterEg] -> ShowS)
-> Show CounterEg
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CounterEg -> ShowS
showsPrec :: Int -> CounterEg -> ShowS
$cshow :: CounterEg -> String
show :: CounterEg -> String
$cshowList :: [CounterEg] -> ShowS
showList :: [CounterEg] -> ShowS
Show)

instance Semigroup CounterEg where
  CounterEg [(Text, Text)]
a [[(Text, Text)]]
b <> :: CounterEg -> CounterEg -> CounterEg
<> CounterEg [(Text, Text)]
c [[(Text, Text)]]
d = [(Text, Text)] -> [[(Text, Text)]] -> CounterEg
CounterEg ([(Text, Text)]
a [(Text, Text)] -> [(Text, Text)] -> [(Text, Text)]
forall a. Semigroup a => a -> a -> a
<> [(Text, Text)]
c) ([[(Text, Text)]]
b [[(Text, Text)]] -> [[(Text, Text)]] -> [[(Text, Text)]]
forall a. Semigroup a => a -> a -> a
<> [[(Text, Text)]]
d)

instance Monoid CounterEg where
  mempty :: CounterEg
mempty = [(Text, Text)] -> [[(Text, Text)]] -> CounterEg
CounterEg [(Text, Text)]
forall a. Monoid a => a
mempty [[(Text, Text)]]
forall a. Monoid a => a
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 :: forall a. Parser a -> Parser a
lexme Parser a
f = do a
a <- Parser a
f; ()
_ <- ParsecT String () Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
P.spaces; a -> Parser a
forall a. a -> ParsecT String () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

nameChar :: Parser Char
nameChar :: Parser Char
nameChar =
  Parser Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
P.alphaNum
    Parser Char -> Parser Char -> Parser Char
forall a.
ParsecT String () Identity a
-> ParsecT String () Identity a -> ParsecT String () Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> Parser Char
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m Char
P.oneOf String
"$.:_"

parens :: Parser a -> Parser a
parens :: forall a. Parser a -> Parser a
parens = Parser a -> Parser a
forall a. Parser a -> Parser a
lexme (Parser a -> Parser a)
-> (Parser a -> Parser a) -> Parser a -> Parser a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parser Char -> Parser Char -> Parser a -> Parser a
forall s (m :: * -> *) t u open close a.
Stream s m t =>
ParsecT s u m open
-> ParsecT s u m close -> ParsecT s u m a -> ParsecT s u m a
P.between (Char -> Parser Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
P.char Char
'(') (Char -> Parser Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
P.char Char
')')

brackets :: Parser a -> Parser a
brackets :: forall a. Parser a -> Parser a
brackets = Parser a -> Parser a
forall a. Parser a -> Parser a
lexme (Parser a -> Parser a)
-> (Parser a -> Parser a) -> Parser a -> Parser a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parser Char -> Parser Char -> Parser a -> Parser a
forall s (m :: * -> *) t u open close a.
Stream s m t =>
ParsecT s u m open
-> ParsecT s u m close -> ParsecT s u m a -> ParsecT s u m a
P.between (Char -> Parser Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
P.char Char
'[') (Char -> Parser Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
P.char Char
']')

trueOrFalse :: Parser String
trueOrFalse :: Parser String
trueOrFalse = Parser String -> Parser String
forall a. Parser a -> Parser a
lexme (Parser String -> Parser String) -> Parser String -> Parser String
forall a b. (a -> b) -> a -> b
$ (String -> Parser String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
P.string String
"true" Parser String -> String -> Parser String
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> String
"1") Parser String -> Parser String -> Parser String
forall a.
ParsecT String () Identity a
-> ParsecT String () Identity a -> ParsecT String () Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
P.string String
"false" Parser String -> String -> Parser String
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> String
"0")

assumeBody :: Parser (String, String)
assumeBody :: Parser (String, String)
assumeBody = Parser (String, String) -> Parser (String, String)
forall a. Parser a -> Parser a
lexme (Parser (String, String) -> Parser (String, String))
-> Parser (String, String) -> Parser (String, String)
forall a b. (a -> b) -> a -> b
$ do
  String
name <- Char -> Parser Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
P.char Char
'=' Parser Char
-> ParsecT String () Identity () -> ParsecT String () Identity ()
forall a b.
ParsecT String () Identity a
-> ParsecT String () Identity b -> ParsecT String () Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT String () Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
P.spaces ParsecT String () Identity () -> Parser String -> Parser String
forall a b.
ParsecT String () Identity a
-> ParsecT String () Identity b -> ParsecT String () Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser String -> Parser String
forall a. Parser a -> Parser a
brackets (Parser Char -> Parser String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
P.many1 Parser Char
nameChar)
  String
num <- ParsecT String () Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
P.spaces ParsecT String () Identity () -> Parser String -> Parser String
forall a b.
ParsecT String () Identity a
-> ParsecT String () Identity b -> ParsecT String () Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ((String -> Parser String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
P.string String
"#b" Parser String -> Parser String -> Parser String
forall a b.
ParsecT String () Identity a
-> ParsecT String () Identity b -> ParsecT String () Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Char -> Parser String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
P.many1 Parser Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
P.digit) Parser String -> Parser String -> Parser String
forall a.
ParsecT String () Identity a
-> ParsecT String () Identity a -> ParsecT String () Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser String
trueOrFalse)
  (String, String) -> Parser (String, String)
forall a. a -> ParsecT String () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (String
name, String
num)

parseAssume :: Parser (String, String)
parseAssume :: Parser (String, String)
parseAssume = Parser (String, String) -> Parser (String, String)
forall a. Parser a -> Parser a
lexme (Parser (String, String) -> Parser (String, String))
-> Parser (String, String) -> Parser (String, String)
forall a b. (a -> b) -> a -> b
$ String -> Parser String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
P.string String
"assume" Parser String
-> ParsecT String () Identity () -> ParsecT String () Identity ()
forall a b.
ParsecT String () Identity a
-> ParsecT String () Identity b -> ParsecT String () Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT String () Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
P.spaces ParsecT String () Identity ()
-> Parser (String, String) -> Parser (String, String)
forall a b.
ParsecT String () Identity a
-> ParsecT String () Identity b -> ParsecT String () Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser (String, String) -> Parser (String, String)
forall a. Parser a -> Parser a
parens Parser (String, String)
assumeBody

parseInitial :: Parser [(String, String)]
parseInitial :: Parser [(String, String)]
parseInitial = Parser [(String, String)] -> Parser [(String, String)]
forall a. Parser a -> Parser a
lexme (Parser [(String, String)] -> Parser [(String, String)])
-> Parser [(String, String)] -> Parser [(String, String)]
forall a b. (a -> b) -> a -> b
$ do
  String
_ <- Parser String -> Parser String
forall a. Parser a -> Parser a
lexme (Parser String -> Parser String) -> Parser String -> Parser String
forall a b. (a -> b) -> a -> b
$ String -> Parser String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
P.string String
"initial"
  Parser (String, String) -> Parser [(String, String)]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
P.many Parser (String, String)
parseAssume

parseState :: Parser (String, [(String, String)])
parseState :: Parser (String, [(String, String)])
parseState = Parser (String, [(String, String)])
-> Parser (String, [(String, String)])
forall a. Parser a -> Parser a
lexme (Parser (String, [(String, String)])
 -> Parser (String, [(String, String)]))
-> Parser (String, [(String, String)])
-> Parser (String, [(String, String)])
forall a b. (a -> b) -> a -> b
$ do
  String
n <- Parser String -> Parser String
forall a. Parser a -> Parser a
lexme (Parser String -> Parser String) -> Parser String -> Parser String
forall a b. (a -> b) -> a -> b
$ String -> Parser String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
P.string String
"state" Parser String
-> ParsecT String () Identity () -> ParsecT String () Identity ()
forall a b.
ParsecT String () Identity a
-> ParsecT String () Identity b -> ParsecT String () Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT String () Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
P.spaces ParsecT String () Identity () -> Parser String -> Parser String
forall a b.
ParsecT String () Identity a
-> ParsecT String () Identity b -> ParsecT String () Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Char -> Parser String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
P.many1 Parser Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
P.digit
  [(String, String)]
assumes <- Parser (String, String) -> Parser [(String, String)]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
P.many Parser (String, String)
parseAssume
  (String, [(String, String)]) -> Parser (String, [(String, String)])
forall a. a -> ParsecT String () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (String
n, [(String, String)]
assumes)

parseCE :: Parser [[(String, String)]]
parseCE :: Parser [[(String, String)]]
parseCE = Parser [[(String, String)]] -> Parser [[(String, String)]]
forall a. Parser a -> Parser a
lexme (Parser [[(String, String)]] -> Parser [[(String, String)]])
-> Parser [[(String, String)]] -> Parser [[(String, String)]]
forall a b. (a -> b) -> a -> b
$ do
  [(String, String)]
i <- Parser [(String, String)]
parseInitial
  [[(String, String)]]
other <- ((String, [(String, String)]) -> [(String, String)])
-> [(String, [(String, String)])] -> [[(String, String)]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String, [(String, String)]) -> [(String, String)]
forall a b. (a, b) -> b
snd ([(String, [(String, String)])] -> [[(String, String)]])
-> ParsecT String () Identity [(String, [(String, String)])]
-> Parser [[(String, String)]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (String, [(String, String)])
-> ParsecT String () Identity [(String, [(String, String)])]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
P.many Parser (String, [(String, String)])
parseState
  [[(String, String)]] -> Parser [[(String, String)]]
forall a. a -> ParsecT String () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(String, String)]
i [(String, String)] -> [[(String, String)]] -> [[(String, String)]]
forall a. a -> [a] -> [a]
: [[(String, String)]]
other)

cEtoCounterEg :: [[(String, String)]] -> CounterEg
cEtoCounterEg :: [[(String, String)]] -> CounterEg
cEtoCounterEg [] = CounterEg
forall a. Monoid a => a
mempty
cEtoCounterEg ([(String, String)]
i : [[(String, String)]]
is) =
  [(Text, Text)] -> [[(Text, Text)]] -> CounterEg
CounterEg
    ((String -> Text)
-> (String -> Text) -> (String, String) -> (Text, Text)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap String -> Text
T.pack String -> Text
T.pack ((String, String) -> (Text, Text))
-> [(String, String)] -> [(Text, Text)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(String, String)]
i)
    (((String, String) -> (Text, Text))
-> [(String, String)] -> [(Text, Text)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((String -> Text)
-> (String -> Text) -> (String, String) -> (Text, Text)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap String -> Text
T.pack String -> Text
T.pack) ([(String, String)] -> [(Text, Text)])
-> [[(String, String)]] -> [[(Text, Text)]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[(String, String)]]
is)

parseCounterEg' :: Parser CounterEg
parseCounterEg' :: Parser CounterEg
parseCounterEg' = Parser CounterEg -> Parser CounterEg
forall a. Parser a -> Parser a
lexme (Parser CounterEg -> Parser CounterEg)
-> Parser CounterEg -> Parser CounterEg
forall a b. (a -> b) -> a -> b
$ do
  ()
_ <- ParsecT String () Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
P.spaces
  [[(String, String)]] -> CounterEg
cEtoCounterEg ([[(String, String)]] -> CounterEg)
-> Parser [[(String, String)]] -> Parser CounterEg
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser [[(String, String)]]
parseCE

parseCounterEg :: Text -> Either String CounterEg
parseCounterEg :: Text -> Either String CounterEg
parseCounterEg = (ParseError -> String)
-> (CounterEg -> CounterEg)
-> Either ParseError CounterEg
-> Either String CounterEg
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ParseError -> String
forall a. Show a => a -> String
show CounterEg -> CounterEg
forall a. a -> a
id (Either ParseError CounterEg -> Either String CounterEg)
-> (Text -> Either ParseError CounterEg)
-> Text
-> Either String CounterEg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parser CounterEg -> String -> String -> Either ParseError CounterEg
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
P.parse Parser CounterEg
parseCounterEg' String
"" (String -> Either ParseError CounterEg)
-> (Text -> String) -> Text -> Either ParseError CounterEg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack