    {-
    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
      , parseSExpBody
      , stringToSExp
      , parseNextWord
      , asAtomList
      , asNegAtomList
      , skipSpaceOrNewline
      , sExpToString
      ) 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 Text
    parseNextWord = do
      Parser ()
    skipSpaceOrNewline
      Parser Text Text -> Parser Text Text -> Parser Text Text
    forall a. Monoid a => a -> a -> a
    mappend ((Char -> Bool) -> Parser Text Text
    takeWhile1 Char -> Bool
    isAlphaNum) (String -> Parser Text Text
    forall a. String -> Parser Text a
    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
    $c== :: SExp -> SExp -> Bool
    == :: SExp -> SExp -> Bool
    $c/= :: SExp -> SExp -> Bool
    /= :: 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
    $ccompare :: SExp -> SExp -> Ordering
    compare :: SExp -> SExp -> Ordering
    $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
    >= :: SExp -> SExp -> Bool
    $cmax :: SExp -> SExp -> SExp
    max :: SExp -> SExp -> SExp
    $cmin :: SExp -> SExp -> SExp
    min :: SExp -> SExp -> 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
    $cshowsPrec :: Int -> SExp -> ShowS
    showsPrec :: Int -> SExp -> ShowS
    $cshow :: SExp -> String
    show :: SExp -> String
    $cshowList :: [SExp] -> ShowS
    showList :: [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 Text
    readToken = (Char -> Bool) -> Parser Text Text
    takeWhile1 Char -> Bool
    isTokenChar

    -- | Parses an SExp.  If the input is a string (recognized by the
    -- 'readString' argument), return that as an 'SString'; if the input
    -- is a single token, return that as an 'SAtom'.

    parseSExp ::
      Parser Text {- ^ A parser for string literals -} ->
      Parser SExp
    parseSExp :: Parser Text Text -> Parser SExp
    parseSExp Parser Text 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 SExp -> Parser SExp
    forall a b. Parser Text a -> Parser Text b -> Parser Text b
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
    *> Parser Text Text -> Parser SExp
    parseSExpBody Parser Text Text
    readString
           , Text -> SExp
    SString (Text -> SExp) -> Parser Text Text -> Parser SExp
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser Text Text
    readString
           , Text -> SExp
    SAtom (Text -> SExp) -> Parser Text Text -> Parser SExp
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser Text Text
    readToken
           ]

    -- | Parses the body of an SExp after the opening '(' has already been
    -- parsed.

    parseSExpBody ::
      Parser Text {- ^ A parser for string literals -} ->
      Parser SExp
    parseSExpBody :: Parser Text Text -> Parser SExp
    parseSExpBody Parser Text Text
    readString =
      Parser ()
    skipSpaceOrNewline Parser () -> Parser SExp -> Parser SExp
    forall a b. Parser Text a -> Parser Text b -> Parser Text b
    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 a. Parser Text a -> Parser Text [a]
    forall (f :: Type -> Type) a. Alternative f => f a -> f [a]
    many (Parser Text Text -> Parser SExp
    parseSExp Parser Text Text
    readString)) Parser SExp -> Parser () -> Parser SExp
    forall a b. Parser Text a -> Parser Text b -> Parser Text a
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f a
    <* Parser ()
    skipSpaceOrNewline Parser SExp -> Parser Char -> Parser SExp
    forall a b. Parser Text a -> Parser Text b -> Parser Text a
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f a
    <* Char -> Parser Char
    char Char
    ')'

    stringToSExp :: MonadFail m =>
      Parser Text {- ^ A parser for string literals -} ->
      String ->
      m [SExp]
    stringToSExp :: forall (m :: Type -> Type).
    MonadFail m =>
    Parser Text Text -> String -> m [SExp]
    stringToSExp Parser Text Text
    readString String
    s = do
      let parseSExpList :: Parser Text [SExp]
    parseSExpList = Parser SExp -> Parser Text [SExp]
    forall a. Parser Text a -> Parser Text [a]
    forall (f :: Type -> Type) a. Alternative f => f a -> f [a]
    many (Parser Text Text -> Parser SExp
    parseSExp Parser Text Text
    readString) Parser Text [SExp] -> Parser () -> Parser Text [SExp]
    forall a b. Parser Text a -> Parser Text b -> Parser Text a
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f a
    <* Parser ()
    skipSpace Parser Text [SExp] -> Parser () -> Parser Text [SExp]
    forall a b. Parser Text a -> Parser Text b -> Parser Text a
    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 a. String -> m a
    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 a. a -> m a
    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

    sExpToString :: SExp -> String
    sExpToString :: SExp -> String
    sExpToString (SAtom Text
    t) = Text -> String
    Text.unpack Text
    t
    sExpToString (SString Text
    t) = (Char
    '"' Char -> ShowS
    forall a. a -> [a] -> [a]
    : Text -> String
    Text.unpack Text
    t) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char
    '"']
    sExpToString (SApp [SExp]
    ss) = (Char
    '(' Char -> ShowS
    forall a. a -> [a] -> [a]
    : [String] -> String
    Data.String.unwords ((SExp -> String) -> [SExp] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SExp -> String
    sExpToString [SExp]
    ss)) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char
    ')']