diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,7 +1,8 @@ # sexpr-parser -[![Travis branch](https://img.shields.io/travis/rcook/sexpr-parser/master.svg)](https://travis-ci.org/rcook/sexpr-parser) +[![Travis CI](https://img.shields.io/travis/rcook/sexpr-parser/master.svg)](https://travis-ci.org/rcook/sexpr-parser) [![Hackage](https://img.shields.io/hackage/v/sexpr-parser.svg)](http://hackage.haskell.org/package/sexpr-parser) +[![Hackage dependencies](https://img.shields.io/hackage-deps/v/sexpr-parser.svg)](http://hackage.haskell.org/package/sexpr-parser) [![Licence](https://img.shields.io/badge/license-MIT-blue.svg)](https://raw.githubusercontent.com/rcook/sexpr-parser/master/LICENSE) S-expression parser in Haskell diff --git a/lib/Text/SExpression.hs b/lib/Text/SExpression.hs --- a/lib/Text/SExpression.hs +++ b/lib/Text/SExpression.hs @@ -29,8 +29,7 @@ > import Text.Megaparsec (parse) > import Text.Megaparsec.Char (char, string) > import Text.Printf (printf) -> import Text.SExpression (Parser, SExpr(..), parseSExpr) -> +> import Text.SExpression (Parser, SExpr(..), parseSExpr, def) > data Z3SATResult = Satisfied | Unsatisfied deriving Show > > data Z3Output = Z3Output Z3SATResult SExpr deriving Show @@ -63,7 +62,7 @@ > _ -> error "Unreachable" > > parseZ3Output :: Parser Z3Output -> parseZ3Output = Z3Output <$> parseZ3SATResult <*> parseSExpr +> parseZ3Output = Z3Output <$> parseZ3SATResult <*> parseSExpr def > > checkSATWithZ3 :: String -> String -> IO (Either String (Z3SATResult, [(String, Bool)])) > checkSATWithZ3 ctx input = do @@ -106,7 +105,10 @@ SExpr(..) , -- * S-expression parser parseSExpr + , -- * Polymorphic default value + def ) where +import Data.Default (def) import Text.SExpression.Internal (parseSExpr) import Text.SExpression.Types (Parser, SExpr(..)) diff --git a/lib/Text/SExpression/Default.hs b/lib/Text/SExpression/Default.hs new file mode 100644 --- /dev/null +++ b/lib/Text/SExpression/Default.hs @@ -0,0 +1,148 @@ +{-# OPTIONS_GHC -Wall -Werror #-} + +{-# LANGUAGE CPP #-} +{-# LANGUAGE RecordWildCards #-} + +#undef MEGAPARSEC_7_OR_LATER +#ifdef MIN_VERSION_GLASGOW_HASKELL +-- GHC >= 7.10.1.0 +#if MIN_VERSION_GLASGOW_HASKELL(8,0,0,0) +-- GHC >= 8.0.0.0 +#if MIN_VERSION_megaparsec(7,0,0) +#define MEGAPARSEC_7_OR_LATER +#endif +#endif +#endif + +module Text.SExpression.Default + ( LiteralParsers(..) + , LiteralParsersM + , mkLiteralParsers + , overrideStringP + , overrideNumberP + , overrideBoolP + , parseStringDef + , parseNumberDef + , parseBoolDef + ) where + +import Data.Semigroup (Last(..)) +import Data.Default +import Text.SExpression.Types (SExpr(..), Parser) +import Control.Monad (void) +import Text.Megaparsec + ( (<|>) + , many + , notFollowedBy +#ifdef MEGAPARSEC_7_OR_LATER + , noneOf +#endif + , some + ) +import Text.Megaparsec.Char + ( char + , digitChar + , string + , alphaNumChar +#ifndef MEGAPARSEC_7_OR_LATER + , noneOf +#endif + ) + +-- | Partial parser configuration +data LiteralParsersM = LiteralParsersM + { parseStringM :: Maybe (Last (Parser SExpr)) + , parseNumberM :: Maybe (Last (Parser SExpr)) + , parseBoolM :: Maybe (Last (Parser SExpr)) + } + +-- | Fully defined parser configuration +data LiteralParsers = LiteralParsers + { parseString :: Parser SExpr + , parseNumber :: Parser SExpr + , parseBool :: Parser SExpr + } + +instance Semigroup LiteralParsersM where + (<>) + (LiteralParsersM ps pn pb) + (LiteralParsersM ps' pn' pb') = + LiteralParsersM (ps <> ps') (pn <> pn') (pb <> pb') + +instance Default LiteralParsersM where + def = LiteralParsersM + { parseStringM = Just $ Last parseStringDef + , parseNumberM = Just $ Last parseNumberDef + , parseBoolM = Just $ Last parseBoolDef + } + +instance Default LiteralParsers where + def = mkLiteralParsers def + +-- | Smart constructor for parser configuration +-- that allows overriding the default literal parsers +mkLiteralParsers :: + (LiteralParsersM -> LiteralParsersM) -- ^ Cumulative override function + -> LiteralParsers +mkLiteralParsers f = + case f def of + LiteralParsersM{..} -> + let Just (Last parseString) = parseStringM + Just (Last parseNumber) = parseNumberM + Just (Last parseBool) = parseBoolM in + LiteralParsers parseString parseNumber parseBool + +-- | String parser override function +overrideStringP :: Parser SExpr -- ^ String parser + -> (LiteralParsersM -> LiteralParsersM) +overrideStringP sp lp = lp <> + LiteralParsersM + { parseStringM = Just $ Last sp + , parseNumberM = Nothing + , parseBoolM = Nothing + } + +-- | Number parser override function +overrideNumberP :: Parser SExpr -- ^ Number parser + -> (LiteralParsersM -> LiteralParsersM) +overrideNumberP np lp = lp <> + LiteralParsersM + { parseStringM = Nothing + , parseNumberM = Just $ Last np + , parseBoolM = Nothing + } + +-- | Boolean parser override function +overrideBoolP :: Parser SExpr -- ^ Bool parser + -> (LiteralParsersM -> LiteralParsersM) +overrideBoolP bp lp = lp <> + LiteralParsersM + { parseStringM = Nothing + , parseNumberM = Nothing + , parseBoolM = Just $ Last bp + } + +-- | Default parser for s-expression boolean literals +parseBoolDef :: + Parser SExpr +parseBoolDef = do + b <- string "#t" <* notFollowedBy alphaNumChar + <|> string "#f" <* notFollowedBy alphaNumChar + case b of + "#t" -> return $ Bool True + "#f" -> return $ Bool False + _ -> fail "Not a boolean" + +-- | Default parser for s-expression numeric literals +parseNumberDef :: + Parser SExpr -- ^ parser +parseNumberDef = (Number . read) <$> some digitChar + +-- | Default parser for s-expression string literals +parseStringDef :: + Parser SExpr -- ^ parser +parseStringDef = do + void $ char '"' + s <- many (noneOf "\"") + void $ char '"' + pure $ String s diff --git a/lib/Text/SExpression/Internal.hs b/lib/Text/SExpression/Internal.hs --- a/lib/Text/SExpression/Internal.hs +++ b/lib/Text/SExpression/Internal.hs @@ -13,6 +13,7 @@ {-# OPTIONS_GHC -Wall -Werror #-} {-# LANGUAGE CPP #-} +{-# LANGUAGE RecordWildCards #-} #undef MEGAPARSEC_7_OR_LATER #ifdef MIN_VERSION_GLASGOW_HASKELL @@ -32,9 +33,14 @@ parseAtom , parseConsList , parseList - , parseNumber , parseQuoted - , parseString + , parseStringDef + , parseNumberDef + , parseBoolDef + , mkLiteralParsers + , overrideBoolP + , overrideNumberP + , overrideStringP ) where import Control.Applicative (empty) @@ -44,11 +50,9 @@ , endBy , many #ifdef MEGAPARSEC_7_OR_LATER - , noneOf , oneOf #endif , sepBy - , some , try ) import Text.Megaparsec.Char @@ -56,7 +60,6 @@ , digitChar , letterChar #ifndef MEGAPARSEC_7_OR_LATER - , noneOf , oneOf #endif , space1 @@ -66,6 +69,7 @@ , skipLineComment ) import Text.SExpression.Types (Parser, SExpr(..)) +import Text.SExpression.Default sc :: Parser () sc = space space1 lineComment empty @@ -77,15 +81,17 @@ -- | S-expression parser parseSExpr :: + LiteralParsers -> Parser SExpr -- ^ parser -parseSExpr = - parseAtom +parseSExpr lp@(LiteralParsers{..}) = + try parseBool + <|> parseAtom <|> parseString <|> parseNumber - <|> parseQuoted + <|> parseQuoted lp <|> do void $ char '(' - lst <- (try parseList) <|> parseConsList + lst <- (try $ parseList lp) <|> parseConsList lp void $ char ')' >> sc pure lst @@ -95,43 +101,30 @@ 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 + return . Atom $ h : t + -- | Parse s-expression list parseList :: + LiteralParsers -> Parser SExpr -- ^ parser -parseList = List <$> parseSExpr `sepBy` sc +parseList lp = + List <$> parseSExpr lp `sepBy` sc -- | Parse s-expression cons list parseConsList :: + LiteralParsers -> Parser SExpr -- ^ parser -parseConsList = do - h <- parseSExpr `endBy` sc - t <- char '.' >> sc >> parseSExpr +parseConsList lp = do + h <- parseSExpr lp `endBy` sc + t <- char '.' >> sc >> parseSExpr lp 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 :: + LiteralParsers -> Parser SExpr -- ^ parser -parseQuoted = do +parseQuoted lp = do void $ char '\'' - e <- parseSExpr + e <- parseSExpr lp pure $ List [Atom "quote", e] diff --git a/sexpr-parser.cabal b/sexpr-parser.cabal --- a/sexpr-parser.cabal +++ b/sexpr-parser.cabal @@ -1,5 +1,5 @@ name: sexpr-parser -version: 0.1.1.2 +version: 0.2.0.0 synopsis: Simple s-expression parser description: This package provides a simple Megaparsec-based s-expression parser. @@ -21,10 +21,12 @@ Text.SExpression , Text.SExpression.Internal , Text.SExpression.Types + , Text.SExpression.Default build-depends: - base >= 4.8 && < 5 - , megaparsec >= 6.5 && < 8 - + base >= 4.9 && < 4.13 + , megaparsec >= 6.5 && < 7.1 + , data-default >= 0.6 && < 0.8 + test-suite sexpr-parser-spec type: exitcode-stdio-1.0 default-language: Haskell2010 @@ -33,18 +35,19 @@ other-modules: Text.SExpression.InternalSpec build-depends: - base >= 4.8 && < 5 - , hspec >= 2.5 && < 3 - , megaparsec >= 6.5 && < 8 + base >= 4.9 && < 4.13 + , hspec >= 2.5 && < 2.8 + , megaparsec >= 6.5 && < 7.1 + , data-default >= 0.6 && < 0.8 , sexpr-parser - + executable sexpr-parser-z3-demo default-language: Haskell2010 hs-source-dirs: z3-demo main-is: Main.hs build-depends: - base >= 4.8 && < 5 - , bytestring >= 0.10 && < 1 - , megaparsec >= 6.5 && < 8 - , process >= 1.6 && < 2 + base >= 4.9 && < 4.13 + , bytestring >= 0.10 && < 0.11 + , megaparsec >= 6.5 && < 7.1 + , process >= 1.6 && < 1.7 , sexpr-parser diff --git a/spec/Text/SExpression/InternalSpec.hs b/spec/Text/SExpression/InternalSpec.hs --- a/spec/Text/SExpression/InternalSpec.hs +++ b/spec/Text/SExpression/InternalSpec.hs @@ -19,14 +19,15 @@ , shouldBe ) import Text.Megaparsec (parse) +import Data.Default (def) import Text.SExpression.Internal ( parseAtom , parseConsList , parseList - , parseNumber + , parseNumberDef , parseQuoted , parseSExpr - , parseString + , parseStringDef ) import Text.SExpression.Types (SExpr(..)) @@ -34,11 +35,11 @@ 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` + parse (parseSExpr def) "" "assert" `shouldBe` Right (Atom "assert") + parse (parseSExpr def) "" "(assert)" `shouldBe` Right (List [Atom "assert"]) + parse (parseSExpr def) "" "(assert (and))" `shouldBe` Right (List [Atom "assert", List [Atom "and"]]) + parse (parseSExpr def) "" "(assert (and (>)))" `shouldBe` Right (List [Atom "assert", List [Atom "and", List [Atom ">"]]]) + parse (parseSExpr def) "" "(assert (and (> (* 2 a) (+ b c)) (> (* 2 b) (+ c d))))" `shouldBe` Right (List [ Atom "assert" , List @@ -72,32 +73,28 @@ ] ]) 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]) + parse (parseList def) "" "#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" $ + parse (parseConsList def) "" "123 . foo" `shouldBe` Right (ConsList [Number 123] (Atom "foo")) + describe "parseNumberDef" $ it "parses number literal" $ - parse parseNumber "" "123" `shouldBe` Right (Number 123) - describe "parseString" $ + parse parseNumberDef "" "123" `shouldBe` Right (Number 123) + describe "parseStringDef" $ it "parses string literal" $ - parse parseString "" "\"foo\"" `shouldBe` Right (String "foo") + parse parseStringDef "" "\"foo\"" `shouldBe` Right (String "foo") describe "parseQuoted" $ it "parses quoted expression" $ - parse parseQuoted "" "'\"foo\"" `shouldBe` Right (List [Atom "quote", String "foo"]) + parse (parseQuoted def) "" "'\"foo\"" `shouldBe` Right (List [Atom "quote", String "foo"]) describe "parseSExpr" $ do it "parses Z3 output" $ do - let Right result = parse parseSExpr "" + let Right result = parse (parseSExpr def) "" "(model\n\ \(define-fun a4 () bool\n\ \ false)\n\ @@ -293,10 +290,10 @@ ] ] it "skips comments" $ - parse parseSExpr "" "(aaa; a comment\nbbb ccc)" + parse (parseSExpr def) "" "(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" + parse (parseSExpr def) "" "(model \n (define-fun y () bool\n true)\n (define-fun x () bool\n false)\n)\n" `shouldBe` Right (List [ Atom "model" diff --git a/z3-demo/Main.hs b/z3-demo/Main.hs --- a/z3-demo/Main.hs +++ b/z3-demo/Main.hs @@ -23,7 +23,7 @@ import Text.Megaparsec (parse) import Text.Megaparsec.Char (char, string) import Text.Printf (printf) -import Text.SExpression (Parser, SExpr(..), parseSExpr) +import Text.SExpression (Parser, SExpr(..), parseSExpr, def) data Z3SATResult = Satisfied | Unsatisfied deriving Show @@ -57,7 +57,7 @@ _ -> error "Unreachable" parseZ3Output :: Parser Z3Output -parseZ3Output = Z3Output <$> parseZ3SATResult <*> parseSExpr +parseZ3Output = Z3Output <$> parseZ3SATResult <*> parseSExpr def checkSATWithZ3 :: String -> String -> IO (Either String (Z3SATResult, [(String, Bool)])) checkSATWithZ3 ctx input = do