sexpr-parser- Simple s-expression parser

Copyright(C) Richard Cook 2019
Safe HaskellNone




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" $
        \(declare-const x bool)\n\
        \(declare-const y bool)\n\
        \(assert (and (not x) y))\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
        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 Source #

Parser context

S-expression values

data SExpr Source #

S-expression values


Atom String


List [SExpr]


ConsList [SExpr] SExpr

cons list

Number Integer

number literal

String String

string literal

Bool Bool

Boolean literal

Eq SExpr Source # 
Instance details

Defined in Text.SExpression.Types


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

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

Read SExpr Source # 
Instance details

Defined in Text.SExpression.Types

Show SExpr Source # 
Instance details

Defined in Text.SExpression.Types


showsPrec :: Int -> SExpr -> ShowS #

show :: SExpr -> String #

showList :: [SExpr] -> ShowS #

S-expression parser

parseSExpr Source #


:: Parser SExpr


S-expression parser