sexpr-parser-0.2.0.0: spec/Text/SExpression/InternalSpec.hs
{-|
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 Data.Default (def)
import Text.SExpression.Internal
( parseAtom
, parseConsList
, parseList
, parseNumberDef
, parseQuoted
, parseSExpr
, parseStringDef
)
import Text.SExpression.Types (SExpr(..))
spec :: Spec
spec = do
describe "parseSExpr" $
it "parses test expressions" $ do
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
[ 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 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 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 def) "" "123 . foo" `shouldBe` Right (ConsList [Number 123] (Atom "foo"))
describe "parseNumberDef" $
it "parses number literal" $
parse parseNumberDef "" "123" `shouldBe` Right (Number 123)
describe "parseStringDef" $
it "parses string literal" $
parse parseStringDef "" "\"foo\"" `shouldBe` Right (String "foo")
describe "parseQuoted" $
it "parses quoted expression" $
parse (parseQuoted def) "" "'\"foo\"" `shouldBe` Right (List [Atom "quote", String "foo"])
describe "parseSExpr" $ do
it "parses Z3 output" $ do
let Right result = parse (parseSExpr def) ""
"(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 def) "" "(aaa; a comment\nbbb ccc)"
`shouldBe` Right (List [Atom "aaa", Atom "bbb", Atom "ccc"])
it "handles trailing whitespace" $
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"
, List
[ Atom "define-fun"
, Atom "y"
, List []
, Atom "bool"
, Atom "true"
]
, List
[ Atom "define-fun"
, Atom "x"
, List []
, Atom"bool"
, Atom "false"
]
]
)