{-
Module           : What4.Protocol.SExp
Description      : Simple datatypes for representing S-Expressions
Copyright        : (c) Galois, Inc 2014-2020
License          : BSD3
Maintainer       : Joe Hendrix <jhendrix@galois.com>

Provides an interface for parsing simple SExpressions
returned by SMT solvers.
-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE OverloadedStrings #-}
module What4.Protocol.SExp
  ( SExp(..)
  , parseSExp
  , stringToSExp
  , parseNextWord
  , asAtomList
  , asNegAtomList
  , skipSpaceOrNewline
  ) where

#if !MIN_VERSION_base(4,13,0)
import Control.Monad.Fail( MonadFail )
#endif

import           Control.Applicative
import           Control.Monad (msum)
import           Data.Attoparsec.Text
import           Data.Char
import           Data.Monoid
import           Data.String
import           Data.Text (Text)
import qualified Data.Text as Text
import           Prelude hiding (takeWhile)

skipSpaceOrNewline :: Parser ()
skipSpaceOrNewline :: Parser ()
skipSpaceOrNewline = (Char -> Bool) -> Parser ()
skipWhile Char -> Bool
f
  where f :: Char -> Bool
f Char
c = Char -> Bool
isSpace Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\r' Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\n'

-- | Read next contiguous sequence of numbers or letters.
parseNextWord :: Parser Text
parseNextWord :: Parser Text
parseNextWord = do
  Parser ()
skipSpaceOrNewline
  Parser Text -> Parser Text -> Parser Text
forall a. Monoid a => a -> a -> a
mappend ((Char -> Bool) -> Parser Text
takeWhile1 Char -> Bool
isAlphaNum) (String -> Parser Text
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"Unexpected end of stream.")

data SExp = SAtom Text
          | SString Text
          | SApp [SExp]
  deriving (SExp -> SExp -> Bool
(SExp -> SExp -> Bool) -> (SExp -> SExp -> Bool) -> Eq SExp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SExp -> SExp -> Bool
$c/= :: SExp -> SExp -> Bool
== :: SExp -> SExp -> Bool
$c== :: SExp -> SExp -> Bool
Eq, Eq SExp
Eq SExp
-> (SExp -> SExp -> Ordering)
-> (SExp -> SExp -> Bool)
-> (SExp -> SExp -> Bool)
-> (SExp -> SExp -> Bool)
-> (SExp -> SExp -> Bool)
-> (SExp -> SExp -> SExp)
-> (SExp -> SExp -> SExp)
-> Ord SExp
SExp -> SExp -> Bool
SExp -> SExp -> Ordering
SExp -> SExp -> SExp
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SExp -> SExp -> SExp
$cmin :: SExp -> SExp -> SExp
max :: SExp -> SExp -> SExp
$cmax :: SExp -> SExp -> SExp
>= :: SExp -> SExp -> Bool
$c>= :: SExp -> SExp -> Bool
> :: SExp -> SExp -> Bool
$c> :: SExp -> SExp -> Bool
<= :: SExp -> SExp -> Bool
$c<= :: SExp -> SExp -> Bool
< :: SExp -> SExp -> Bool
$c< :: SExp -> SExp -> Bool
compare :: SExp -> SExp -> Ordering
$ccompare :: SExp -> SExp -> Ordering
$cp1Ord :: Eq SExp
Ord, Int -> SExp -> ShowS
[SExp] -> ShowS
SExp -> String
(Int -> SExp -> ShowS)
-> (SExp -> String) -> ([SExp] -> ShowS) -> Show SExp
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SExp] -> ShowS
$cshowList :: [SExp] -> ShowS
show :: SExp -> String
$cshow :: SExp -> String
showsPrec :: Int -> SExp -> ShowS
$cshowsPrec :: Int -> SExp -> ShowS
Show)

instance IsString SExp where
  fromString :: String -> SExp
fromString = Text -> SExp
SAtom (Text -> SExp) -> (String -> Text) -> String -> SExp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
Text.pack

isTokenChar :: Char -> Bool
isTokenChar :: Char -> Bool
isTokenChar Char
'(' = Bool
False
isTokenChar Char
')' = Bool
False
isTokenChar Char
'"' = Bool
False
isTokenChar Char
c = Bool -> Bool
not (Char -> Bool
isSpace Char
c)

readToken :: Parser Text
readToken :: Parser Text
readToken = (Char -> Bool) -> Parser Text
takeWhile1 Char -> Bool
isTokenChar

parseSExp ::
  Parser Text {- ^ A parser for string literals -} ->
  Parser SExp
parseSExp :: Parser Text -> Parser SExp
parseSExp Parser Text
readString = do
  Parser ()
skipSpaceOrNewline
  [Parser SExp] -> Parser SExp
forall (t :: Type -> Type) (m :: Type -> Type) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [ Char -> Parser Char
char Char
'(' Parser Char -> Parser () -> Parser ()
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Parser ()
skipSpaceOrNewline Parser () -> Parser SExp -> Parser SExp
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> ([SExp] -> SExp
SApp ([SExp] -> SExp) -> Parser Text [SExp] -> Parser SExp
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser SExp -> Parser Text [SExp]
forall (f :: Type -> Type) a. Alternative f => f a -> f [a]
many (Parser Text -> Parser SExp
parseSExp Parser Text
readString)) Parser SExp -> Parser () -> Parser SExp
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f a
<* Parser ()
skipSpaceOrNewline Parser SExp -> Parser Char -> Parser SExp
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f a
<* Char -> Parser Char
char Char
')'
       , Text -> SExp
SString (Text -> SExp) -> Parser Text -> Parser SExp
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text
readString
       , Text -> SExp
SAtom (Text -> SExp) -> Parser Text -> Parser SExp
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text
readToken
       ]

stringToSExp :: MonadFail m =>
  Parser Text {- ^ A parser for string literals -} ->
  String ->
  m [SExp]
stringToSExp :: Parser Text -> String -> m [SExp]
stringToSExp Parser Text
readString String
s = do
  let parseSExpList :: Parser Text [SExp]
parseSExpList = Parser SExp -> Parser Text [SExp]
forall (f :: Type -> Type) a. Alternative f => f a -> f [a]
many (Parser Text -> Parser SExp
parseSExp Parser Text
readString) Parser Text [SExp] -> Parser () -> Parser Text [SExp]
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f a
<* Parser ()
skipSpace Parser Text [SExp] -> Parser () -> Parser Text [SExp]
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f a
<* Parser ()
forall t. Chunk t => Parser t ()
endOfInput
  case Parser Text [SExp] -> Text -> Either String [SExp]
forall a. Parser a -> Text -> Either String a
parseOnly Parser Text [SExp]
parseSExpList (String -> Text
Text.pack String
s) of
    Left String
e -> String -> m [SExp]
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> m [SExp]) -> String -> m [SExp]
forall a b. (a -> b) -> a -> b
$ String
"stringToSExpr error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
e
    Right [SExp]
v -> [SExp] -> m [SExp]
forall (m :: Type -> Type) a. Monad m => a -> m a
return [SExp]
v

asNegAtomList :: SExp -> Maybe [(Bool,Text)]
asNegAtomList :: SExp -> Maybe [(Bool, Text)]
asNegAtomList (SApp [SExp]
xs) = [SExp] -> Maybe [(Bool, Text)]
go [SExp]
xs
  where
  go :: [SExp] -> Maybe [(Bool, Text)]
go [] = [(Bool, Text)] -> Maybe [(Bool, Text)]
forall a. a -> Maybe a
Just []
  go (SAtom Text
a : [SExp]
ys) = ((Bool
True,Text
a)(Bool, Text) -> [(Bool, Text)] -> [(Bool, Text)]
forall a. a -> [a] -> [a]
:) ([(Bool, Text)] -> [(Bool, Text)])
-> Maybe [(Bool, Text)] -> Maybe [(Bool, Text)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [SExp] -> Maybe [(Bool, Text)]
go [SExp]
ys
  go (SApp [SAtom Text
"not", SAtom Text
a] : [SExp]
ys) = ((Bool
False,Text
a)(Bool, Text) -> [(Bool, Text)] -> [(Bool, Text)]
forall a. a -> [a] -> [a]
:) ([(Bool, Text)] -> [(Bool, Text)])
-> Maybe [(Bool, Text)] -> Maybe [(Bool, Text)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [SExp] -> Maybe [(Bool, Text)]
go [SExp]
ys
  go [SExp]
_ = Maybe [(Bool, Text)]
forall a. Maybe a
Nothing
asNegAtomList SExp
_ = Maybe [(Bool, Text)]
forall a. Maybe a
Nothing

asAtomList :: SExp -> Maybe [Text]
asAtomList :: SExp -> Maybe [Text]
asAtomList (SApp [SExp]
xs) = [SExp] -> Maybe [Text]
go [SExp]
xs
  where
  go :: [SExp] -> Maybe [Text]
go [] = [Text] -> Maybe [Text]
forall a. a -> Maybe a
Just []
  go (SAtom Text
a:[SExp]
ys) = (Text
aText -> [Text] -> [Text]
forall a. a -> [a] -> [a]
:) ([Text] -> [Text]) -> Maybe [Text] -> Maybe [Text]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [SExp] -> Maybe [Text]
go [SExp]
ys
  go [SExp]
_ = Maybe [Text]
forall a. Maybe a
Nothing
asAtomList SExp
_ = Maybe [Text]
forall a. Maybe a
Nothing