sexpr-parser (empty) → 0.1.0.0
raw patch · 9 files changed
+774/−0 lines, 9 filesdep +basedep +bytestringdep +hspec
Dependencies added: base, bytestring, hspec, megaparsec, parsec, process, sexpr-parser
Files
- LICENSE +21/−0
- README.md +24/−0
- lib/Text/SExpression.hs +112/−0
- lib/Text/SExpression/Internal.hs +118/−0
- lib/Text/SExpression/Types.hs +34/−0
- sexpr-parser.cabal +51/−0
- spec/Spec.hs +11/−0
- spec/Text/SExpression/InternalSpec.hs +318/−0
- z3-demo/Main.hs +85/−0
+ LICENSE view
@@ -0,0 +1,21 @@+The MIT License (MIT)++Copyright (c) 2019 Richard Cook++Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in all+copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE+SOFTWARE.
+ README.md view
@@ -0,0 +1,24 @@+# sexpr-parser++S-expression parser in Haskell++## Description++This is a [Megaparsec][megaparsec]-based parser for s-expression, heavily inspired by [lispparser][lispparser]. I'm building this to parse [SMT-LIB v2][smt-lib] output, so there.++## Run Z3 demo++The [Z3 demo](z3-demo/Main.hs) parses SMT-LIB v2 output from Z3. The executable assumes that you have [Z3][z3] installed and available on your system search path:++```bash+stack build --fast --exec sexpr-parser-z3-demo+```++## Licence++[MIT License](LICENSE)++[lispparser]: http://hackage.haskell.org/package/lispparser+[megaparsec]: http://hackage.haskell.org/package/megaparsec+[smt-lib]: http://smtlib.cs.uiowa.edu/language.shtml+[z3]: https://github.com/Z3Prover/z3
+ lib/Text/SExpression.hs view
@@ -0,0 +1,112 @@+{-|+Module : Text.SExpression+Description : S-expression parser+Copyright : (C) Richard Cook, 2019+Licence : MIT+Maintainer : rcook@rcook.org+Stability : stable+Portability : portable++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 <https://github.com/Z3Prover/z3 Z3> to+determine the satisfiability of a simple Boolean expression. It feeds+<http://smtlib.cs.uiowa.edu/language.shtml 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 $ "result=" ++ 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 'Text.Megaparsec.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.++-}++{-# OPTIONS_GHC -Wall -Werror #-}++module Text.SExpression+ ( -- * Parser context+ Parser+ , -- * S-expression values+ SExpr(..)+ , -- * S-expression parser+ parseSExpr+ ) where++import Text.SExpression.Internal (parseSExpr)+import Text.SExpression.Types (Parser, SExpr(..))
+ lib/Text/SExpression/Internal.hs view
@@ -0,0 +1,118 @@+{-|+Module : Text.SExpression.Internal+Description : Internal parser functions+Copyright : (C) Richard Cook, 2019+Licence : MIT+Maintainer : rcook@rcook.org+Stability : stable+Portability : portable++This module provides internal parser functions.+-}++{-# OPTIONS_GHC -Wall -Werror #-}++module Text.SExpression.Internal+ ( -- * S-expression parser+ parseSExpr+ , -- * S-expression value parsers+ parseAtom+ , parseConsList+ , parseList+ , parseNumber+ , parseQuoted+ , parseString+ ) where++import Control.Applicative (empty)+import Control.Monad (void)+import Text.Megaparsec+ ( (<|>)+ , endBy+ , many+ , sepBy+ , some+ , try+ )+import Text.Megaparsec.Char+ ( char+ , digitChar+ , letterChar+ , noneOf+ , oneOf+ , space1+ )+import Text.Megaparsec.Char.Lexer+ ( space+ , skipLineComment+ )+import Text.SExpression.Types (Parser, SExpr(..))++sc :: Parser ()+sc = space space1 lineComment empty+ where+ lineComment = skipLineComment ";"++symbol :: Parser Char+symbol = oneOf "!$%&|*+-/:<=>?@^_~#"++-- | S-expression parser+parseSExpr ::+ Parser SExpr -- ^ parser+parseSExpr =+ parseAtom+ <|> parseString+ <|> parseNumber+ <|> parseQuoted+ <|> do+ void $ char '('+ lst <- (try parseList) <|> parseConsList+ void $ char ')' >> sc+ pure lst++-- | Parse s-expression atom+parseAtom ::+ Parser SExpr -- ^ parser+parseAtom = do+ h <- letterChar <|> symbol+ t <- many (letterChar <|> digitChar <|> symbol)+ let s = h : t+ pure $ case s of+ "#t" -> Bool True+ "#f" -> Bool False+ _ -> Atom s++-- | Parse s-expression list+parseList ::+ Parser SExpr -- ^ parser+parseList = List <$> parseSExpr `sepBy` sc++-- | Parse s-expression cons list+parseConsList ::+ Parser SExpr -- ^ parser+parseConsList = do+ h <- parseSExpr `endBy` sc+ t <- char '.' >> sc >> parseSExpr+ pure $ ConsList h t++-- | Parse s-expression number literal+parseNumber ::+ Parser SExpr -- ^ parser+parseNumber = (Number . read) <$> some digitChar++-- | Parse s-expression string literal+parseString ::+ Parser SExpr -- ^ parser+parseString = do+ void $ char '"'+ s <- many (noneOf "\"")+ void $ char '"'+ pure $ String s++-- | Parse s-expression quoted expression+parseQuoted ::+ Parser SExpr -- ^ parser+parseQuoted = do+ void $ char '\''+ e <- parseSExpr+ pure $ List [Atom "quote", e]
+ lib/Text/SExpression/Types.hs view
@@ -0,0 +1,34 @@+{-|+Module : Text.SExpression.Types+Description : Types+Copyright : (C) Richard Cook, 2019+Licence : MIT+Maintainer : rcook@rcook.org+Stability : stable+Portability : portable++This module provides parser context type 'Parser' and value type 'SExpr'.+-}++{-# OPTIONS_GHC -Wall -Werror #-}++module Text.SExpression.Types+ ( Parser+ , SExpr(..)+ ) where++import Data.Void (Void)+import Text.Megaparsec (Parsec)++-- | Parser context+type Parser = Parsec Void String++-- | S-expression values+data SExpr =+ Atom String -- ^ atom+ | List [SExpr] -- ^ list+ | ConsList [SExpr] SExpr -- ^ cons list+ | Number Integer -- ^ number literal+ | String String -- ^ string literal+ | Bool Bool -- ^ Boolean literal+ deriving (Eq, Read, Show)
+ sexpr-parser.cabal view
@@ -0,0 +1,51 @@+name: sexpr-parser+version: 0.1.0.0+synopsis: Simple s-expression parser+description:+ This package provides a simple Megaparsec-based s-expression parser.+homepage: https://github.com/rcook/sexpr-parser#readme+license: MIT+license-file: LICENSE+author: Richard Cook+maintainer: rcook@rcook.org+copyright: 2019 Richard Cook+category: Command Line+build-type: Simple+cabal-version: >= 1.10+extra-source-files: README.md++library+ default-language: Haskell2010+ hs-source-dirs: lib+ exposed-modules:+ Text.SExpression+ , Text.SExpression.Internal+ , Text.SExpression.Types+ build-depends:+ base >= 4.7 && < 5+ , megaparsec+ , parsec++test-suite sexpr-parser-spec+ type: exitcode-stdio-1.0+ default-language: Haskell2010+ hs-source-dirs: spec+ main-is: Spec.hs+ other-modules:+ Text.SExpression.InternalSpec+ build-depends:+ base >= 4.7 && < 5+ , hspec+ , megaparsec+ , sexpr-parser++executable sexpr-parser-z3-demo+ default-language: Haskell2010+ hs-source-dirs: z3-demo+ main-is: Main.hs+ build-depends:+ base >= 4.7 && < 5+ , bytestring+ , megaparsec+ , process+ , sexpr-parser
+ spec/Spec.hs view
@@ -0,0 +1,11 @@+{-|+Module : Text.SExpression.Spec+Description : Tests+Copyright : (C) Richard Cook, 2019+Licence : MIT+Maintainer : rcook@rcook.org+Stability : stable+Portability : portable+-}++{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
+ spec/Text/SExpression/InternalSpec.hs view
@@ -0,0 +1,318 @@+{-|+Module : Text.SExpression.InternalSpec+Description : Tests+Copyright : (C) Richard Cook, 2019+Licence : MIT+Maintainer : rcook@rcook.org+Stability : stable+Portability : portable+-}++{-# OPTIONS_GHC -Wall -Werror #-}++module Text.SExpression.InternalSpec (spec) where++import Test.Hspec+ ( Spec+ , describe+ , it+ , shouldBe+ )+import Text.Megaparsec (parse)+import Text.SExpression.Internal+ ( parseAtom+ , parseConsList+ , parseList+ , parseNumber+ , parseQuoted+ , parseSExpr+ , parseString+ )+import Text.SExpression.Types (SExpr(..))++spec :: Spec+spec = do+ describe "parseSExpr" $+ it "parses test expressions" $ do+ parse parseSExpr "" "assert" `shouldBe` Right (Atom "assert")+ parse parseSExpr "" "(assert)" `shouldBe` Right (List [Atom "assert"])+ parse parseSExpr "" "(assert (and))" `shouldBe` Right (List [Atom "assert", List [Atom "and"]])+ parse parseSExpr "" "(assert (and (>)))" `shouldBe` Right (List [Atom "assert", List [Atom "and", List [Atom ">"]]])+ parse parseSExpr "" "(assert (and (> (* 2 a) (+ b c)) (> (* 2 b) (+ c d))))" `shouldBe`+ Right (List+ [ Atom "assert"+ , List+ [ Atom "and"+ , List+ [ Atom ">"+ , List+ [ Atom "*"+ , Number 2+ , Atom "a"+ ]+ , List+ [ Atom "+"+ , Atom "b"+ , Atom "c"+ ]+ ]+ , List+ [ Atom ">"+ , List+ [ Atom "*"+ , Number 2+ , Atom "b"+ ]+ , List+ [ Atom "+"+ , Atom "c"+ , Atom "d"+ ]+ ]+ ]+ ])+ describe "parseAtom" $ do+ it "parses #t" $+ parse parseAtom "" "#t" `shouldBe` Right (Bool True)+ it "parses #f" $+ parse parseAtom "" "#f" `shouldBe` Right (Bool False)+ it "parses single-character atom" $+ parse parseAtom "" "x" `shouldBe` Right (Atom "x")+ it "parses other atom" $+ parse parseAtom "" "foo" `shouldBe` Right (Atom "foo")+ describe "parseList" $+ it "parses a list of different atoms" $+ parse parseList "" "#t #f x foo 123" `shouldBe` Right (List [Bool True, Bool False, Atom "x", Atom "foo", Number 123])+ describe "parseConsList" $+ it "parses a cons list" $+ parse parseConsList "" "123 . foo" `shouldBe` Right (ConsList [Number 123] (Atom "foo"))+ describe "parseNumber" $+ it "parses number literal" $+ parse parseNumber "" "123" `shouldBe` Right (Number 123)+ describe "parseString" $+ it "parses string literal" $+ parse parseString "" "\"foo\"" `shouldBe` Right (String "foo")+ describe "parseQuoted" $+ it "parses quoted expression" $+ parse parseQuoted "" "'\"foo\"" `shouldBe` Right (List [Atom "quote", String "foo"])+ describe "parseSExpr" $ do+ it "parses Z3 output" $ do+ let Right result = parse parseSExpr ""+ "(model\n\+ \(define-fun a4 () bool\n\+ \ false)\n\+ \(define-fun c3 () bool\n\+ \ true)\n\+ \(define-fun d4 () bool\n\+ \ false)\n\+ \(define-fun a2 () bool\n\+ \ true)\n\+ \(define-fun c5 () bool\n\+ \ false)\n\+ \(define-fun b4 () bool\n\+ \ true)\n\+ \(define-fun b5 () bool\n\+ \ true)\n\+ \(define-fun b2 () bool\n\+ \ false)\n\+ \(define-fun d1 () bool\n\+ \ true)\n\+ \(define-fun d2 () bool\n\+ \ false)\n\+ \(define-fun b1 () bool\n\+ \ false)\n\+ \(define-fun a5 () bool\n\+ \ true)\n\+ \(define-fun c2 () bool\n\+ \ true)\n\+ \(define-fun d3 () bool\n\+ \ true)\n\+ \(define-fun c4 () bool\n\+ \ true)\n\+ \(define-fun a1 () bool\n\+ \ false)\n\+ \(define-fun d5 () bool\n\+ \ false)\n\+ \(define-fun b3 () bool\n\+ \ true)\n\+ \(define-fun c0 () bool\n\+ \ false)\n\+ \(define-fun c1 () bool\n\+ \ true)\n\+ \(define-fun a3 () bool\n\+ \ true))"+ result `shouldBe`+ List+ [ Atom "model"+ , List+ [ Atom "define-fun"+ , Atom "a4"+ , List []+ , Atom "bool"+ , Atom "false"+ ]+ , List+ [ Atom "define-fun"+ , Atom "c3"+ , List []+ , Atom "bool"+ , Atom "true"+ ]+ , List+ [ Atom "define-fun"+ , Atom "d4"+ , List []+ , Atom "bool"+ , Atom "false"+ ]+ , List+ [ Atom "define-fun"+ , Atom "a2"+ , List []+ , Atom "bool"+ , Atom "true"+ ]+ , List+ [ Atom "define-fun"+ , Atom "c5"+ , List []+ , Atom "bool"+ , Atom "false"+ ]+ , List+ [ Atom "define-fun"+ , Atom "b4"+ , List []+ , Atom "bool"+ , Atom "true"+ ]+ , List+ [ Atom "define-fun"+ , Atom "b5"+ , List []+ , Atom "bool"+ , Atom "true"+ ]+ , List+ [ Atom "define-fun"+ , Atom "b2"+ , List []+ , Atom "bool"+ , Atom "false"+ ]+ , List+ [ Atom "define-fun"+ , Atom "d1"+ , List []+ , Atom "bool"+ , Atom "true"+ ]+ , List+ [ Atom "define-fun"+ , Atom "d2"+ , List []+ , Atom "bool"+ , Atom "false"+ ]+ , List+ [ Atom "define-fun"+ , Atom "b1"+ , List []+ , Atom "bool"+ , Atom "false"+ ]+ , List+ [ Atom "define-fun"+ , Atom "a5"+ , List []+ , Atom "bool"+ , Atom "true"+ ]+ , List+ [ Atom "define-fun"+ , Atom "c2"+ , List []+ , Atom "bool"+ , Atom "true"+ ]+ , List+ [ Atom "define-fun"+ , Atom "d3"+ , List []+ , Atom "bool"+ , Atom "true"+ ]+ , List+ [ Atom "define-fun"+ , Atom "c4"+ , List []+ , Atom "bool"+ , Atom "true"+ ]+ , List+ [ Atom "define-fun"+ , Atom "a1"+ , List []+ , Atom "bool"+ , Atom "false"+ ]+ , List+ [ Atom "define-fun"+ , Atom "d5"+ , List []+ , Atom "bool"+ , Atom "false"+ ]+ , List+ [ Atom "define-fun"+ , Atom "b3"+ , List []+ , Atom "bool"+ , Atom "true"+ ]+ , List+ [ Atom "define-fun"+ , Atom "c0"+ , List []+ , Atom "bool"+ , Atom "false"+ ]+ , List+ [ Atom "define-fun"+ , Atom "c1"+ , List []+ , Atom "bool"+ , Atom "true"+ ]+ , List+ [ Atom "define-fun"+ , Atom "a3"+ , List []+ , Atom "bool"+ , Atom "true"+ ]+ ]+ it "skips comments" $+ parse parseSExpr "" "(aaa; a comment\nbbb ccc)"+ `shouldBe` Right (List [Atom "aaa", Atom "bbb", Atom "ccc"])+ it "handles trailing whitespace" $+ parse parseSExpr "" "(model \n (define-fun y () bool\n true)\n (define-fun x () bool\n false)\n)\n"+ `shouldBe` Right+ (List+ [ Atom "model"+ , List+ [ Atom "define-fun"+ , Atom "y"+ , List []+ , Atom "bool"+ , Atom "true"+ ]+ , List+ [ Atom "define-fun"+ , Atom "x"+ , List []+ , Atom"bool"+ , Atom "false"+ ]+ ]+ )
+ z3-demo/Main.hs view
@@ -0,0 +1,85 @@+{-|+Module : Main+Description : Z3 demo+Copyright : (C) Richard Cook, 2019+Licence : MIT+Maintainer : rcook@rcook.org+Stability : stable+Portability : portable+-}++{-# OPTIONS_GHC -Wall -Werror #-}++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 $ "result=" ++ 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 _ = []