Text.SExpression

This module provides a parseSExpr function which parses simple s-expressions represented using the SExpr type from SExpr input.

Here's a full example which uses Z3 to determine the satisfiability of a simple Boolean expression. It feeds SMT-LIB v2-format input to Z3 and then parses the output (which uses a subset of Lisp-style s-expressions) to display the satisfying assignment for the expression.

module Main (main) where

import Control.Applicative ((<|>))
import Control.Exception (evaluate)
import Control.Monad (void)
import Data.Foldable (for_)
import Data.List (sort)
import Data.Maybe (catMaybes)
import System.IO (BufferMode(..), hGetContents, hPutStrLn, hSetBuffering)
import System.Process
import Text.Megaparsec (parse)
import Text.Megaparsec.Char (char, string)
import Text.Printf (printf)
import Text.SExpression (Parser, SExpr(..), parseSExpr)

data Z3SATResult = Satisfied | Unsatisfied deriving Show

data Z3Output = Z3Output Z3SATResult SExpr deriving Show

main :: IO ()
main = do
    result <- checkSATWithZ3 "input.smt2" $
        "(push)\n\
        \(declare-const x bool)\n\
        \(declare-const y bool)\n\
        \(assert (and (not x) y))\n\
        \(check-sat)\n\
        \(get-model)\n\
        \(pop)\n\
        \(exit)\n"
    case result of
        Left e -> putStrLn $ "Error: " ++ e
        Right (satResult, funs) -> do
            for_ funs $ \(name, value) ->
                putStrLn $ printf "%s = %s" name (if value then "1" else "0")
            putStrLn $ printf "result=%s" (show satResult)

parseZ3SATResult :: Parser Z3SATResult
parseZ3SATResult = do
    s <- string "sat" <|> string "unsat"
    void $ char '\n'
    case s of
        "sat" -> pure Satisfied
        "unsat" -> pure Unsatisfied
        _ -> error "Unreachable"

parseZ3Output :: Parser Z3Output
parseZ3Output = Z3Output <$> parseZ3SATResult <*> parseSExpr

checkSATWithZ3 :: String -> String -> IO (Either String (Z3SATResult, [(String, Bool)]))
checkSATWithZ3 ctx input = do
    output <- withCreateProcess (proc "z3" ["-in"])
                        { std_in = CreatePipe
                        , std_out = CreatePipe
                        , std_err = Inherit
                        } $ \(Just hIn) (Just hOut) _ _ -> do
        hSetBuffering hIn NoBuffering
        hPutStrLn hIn input
        s <- hGetContents hOut
        void $ evaluate (length s)
        pure s
    case parse parseZ3Output ctx output of
        Left e -> pure $ Left (show e)
        Right (Z3Output satResult f) -> pure $ Right (satResult, sort (boolFuns f))

boolFuns :: SExpr -> [(String, Bool)]
boolFuns (List (Atom "model" : fs)) = catMaybes $ map p fs
    where
        p :: SExpr -> Maybe (String, Bool)
        p (List [Atom "define-fun", Atom name, List [], Atom "bool", Atom "false"]) = Just (name, False)
        p (List [Atom "define-fun", Atom name, List [], Atom "bool", Atom "true"]) = Just (name, True)
        p _ = Nothing
boolFuns _ = []

This demonstrates how to run the parser with parse and parseSExpr as well as how to compose the s-expression parser with other parsers to handle a composite format. It also shows how to pattern-match on SExpr to extract data from s-expressions.

Parser context

type Parser = Parsec Void String

Parser context

S-expression values

data SExpr

S-expression values

Constructors

Atom String

atom

List [SExpr]

list

ConsList [SExpr] SExpr

cons list

Number Integer

number literal

String String

string literal

Bool Bool

Boolean literal

Instances

Eq SExpr

Defined in Text.SExpression.Types

Methods

(==) :: SExpr -> SExpr -> Bool

(/=) :: SExpr -> SExpr -> Bool

Read SExpr

Defined in Text.SExpression.Types

Methods

readsPrec :: Int -> ReadS SExpr

readList :: ReadS [SExpr]

readPrec :: ReadPrec SExpr

readListPrec :: ReadPrec [SExpr]

Show SExpr

Defined in Text.SExpression.Types

Methods

showsPrec :: Int -> SExpr -> ShowS

show :: SExpr -> String

showList :: [SExpr] -> ShowS

S-expression parser

parseSExpr

Arguments

:: Parser SExpr

parser

S-expression parser