sexpr-parser-0.2.2.0: Simple s-expression parser
Copyright(C) Richard Cook 2019
LicenseMIT
Maintainerrcook@rcook.org
Stabilitystable
Portabilityportable
Safe HaskellSafe-Inferred
LanguageHaskell2010

Text.SExpression

Description

This module provides a parseSExpr function which parses simple s-expressions represented using the SExpr type from String 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, def)
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 def

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.

Synopsis

Parser context

type Parser = Parsec Void String Source #

Parser context

S-expression values

data SExpr Source #

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

Instances details
Eq SExpr Source # 
Instance details

Defined in Text.SExpression.Types

Methods

(==) :: 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

Methods

showsPrec :: Int -> SExpr -> ShowS #

show :: SExpr -> String #

showList :: [SExpr] -> ShowS #

S-expression parser

parseSExpr Source #

Arguments

:: LiteralParsers 
-> Parser SExpr

parser

S-expression parser

Polymorphic default value

def :: Default a => a #

The default value for this type.