module Math.SMT.Yices.Parser (
typY, expY, cmdY, parseTypY, parseExpY, parseExpYs, parseCmdY
) where
import Math.SMT.Yices.Syntax
import Control.Monad
import Data.Maybe
import Data.Ratio
import Text.ParserCombinators.Parsec
import Text.ParserCombinators.Parsec.Language
import qualified Text.ParserCombinators.Parsec.Token as T
parseTypY :: String -> TypY
parseTypY s = case parse typY "parseTypY" s of Right r -> r
Left msg -> error $ show msg
parseExpY :: String -> ExpY
parseExpY s = case parse expY "parseExpY" s of Right r -> r
Left msg -> error $ show msg
parseExpYs :: String -> [ExpY]
parseExpYs s = case parse expYs "parseExpYs" s of Right r -> r
Left msg -> error $ show msg
parseCmdY :: String -> CmdY
parseCmdY s = case parse cmdY "parseCmdY" s of Right r -> r
Left msg -> error $ show msg
tp = T.makeTokenParser emptyDef
stringLiteral = T.stringLiteral tp
lexme p = do spaces
r <- p
spaces
return r
paren = between (lexme $ char '(') (lexme $ char ')')
many2 p = liftM2 (:) p (many1 p)
idStart = identStart emptyDef
idLetter = identLetter emptyDef
ident = liftM2 (:) idStart (many idLetter)
identifier = lexme ident <?> "identifier"
neg = char '-' >> return negate
nat = liftM (read :: String -> Integer) (many1 digit)
int = option id neg `ap` nat
integer = lexme int <?> "integer"
rat = do n <- nat
char '/'
d <- nat
return (n % d)
ratio = option id neg `ap` rat
rational = lexme ratio <?> "rational"
true = string "true" >> return True
false = string "false" >> return False
bool = true <|> false
boolean = lexme bool <?> "boolean"
tok = try . lexme . string
typY :: GenParser Char st TypY
typY = typYsimple <|> paren typYinParen
typYinParen = subtype <|> subrange <|> arr <|> tup <|> rec
<|> datatype <|> scalar
vart = liftM VarT identifier
typYsimple = do x <- identifier
mt <- optionMaybe $ tok "::" >> (vart <|> paren typYinParen)
return $ case mt of Nothing -> VarT x
Just t -> DEP (x,t)
subtype = tok "subtype" >> liftM2 SUBTYPE (paren idty) expY
subrange = tok "subrange" >> liftM2 SUBRANGE expY expY
arr = tok "->" >> liftM ARR (many2 typY)
tup = tok "tuple" >> liftM TUP (many2 typY)
rec = tok "record" >> liftM REC (many1 idty)
datatype = tok "datatype" >> liftM DATATYPE (many1 $ paren ctordef)
scalar = tok "scalar" >> liftM SCALAR (many1 identifier)
ctordef = liftM2 (,) identifier (many idty)
idty = do x <- identifier
tok "::"
t <- typY
return (x,t)
idex = do x <- identifier
tok "::"
e <- expY
return (x,e)
expY :: GenParser Char st ExpY
expY = try litb <|> try litr <|> liti <|> vare <|> paren expYinParen
expYs :: GenParser Char st [ExpY]
expYs = many expY
expYinParen = and_ <|> or_ <|> not_ <|> try (=>:) <|> (=:) <|> (/=:)
<|> try (<:) <|> (<=:) <|> try (>:) <|> (>=:)
<|> (+:) <|> (-:) <|> (*:) <|> (/:) <|> div_ <|> mod_
<|> if_ <|> ite <|> let_ <|> forall <|> exists
<|> lambda <|> mktup <|> mkrec <|> update <|> select
<|> app
vare = liftM VarE identifier
litb = liftM LitB boolean
liti = liftM LitI integer
litr = liftM LitR rational
and_ = tok "and" >> liftM AND (many1 expY)
or_ = tok "or" >> liftM OR (many1 expY)
not_ = tok "not" >> liftM NOT expY
(=:) = tok "=" >> liftM2 (:=) expY expY
(/=:) = tok "/=" >> liftM2 (:/=) expY expY
(=>:) = tok "=>" >> liftM2 (:=>) expY expY
(<:) = tok "<" >> liftM2 (:<) expY expY
(<=:) = tok "<=" >> liftM2 (:<=) expY expY
(>:) = tok ">" >> liftM2 (:>) expY expY
(>=:) = tok ">=" >> liftM2 (:>=) expY expY
(+:) = tok "+" >> liftM2 (:+:) expY expY
(-:) = tok "-" >> liftM2 (:-:) expY expY
(*:) = tok "*" >> liftM2 (:*:) expY expY
(/:) = tok "/" >> liftM2 (:/:) expY expY
div_ = tok "div" >> liftM2 DIV expY expY
mod_ = tok "mod" >> liftM2 MOD expY expY
if_ = tok "if" >> liftM3 IF expY expY expY
ite = do tok "ite" >> liftM3 ITE expY expY expY
let_ = tok "let" >> liftM2 LET (paren $ many1 binding) expY
forall = tok "forall" >> liftM2 FORALL (paren $ many1 idty) expY
exists = tok "exists" >> liftM2 EXISTS (paren $ many1 idty) expY
lambda = tok "lambda" >> liftM2 LAMBDA (paren $ many1 idty) expY
mktup = tok "mk-tuple" >> liftM MKTUP (many2 expY)
mkrec = tok "mk-record" >> liftM MKREC (many1 idex)
update = do tok "update"
e <- expY
ix <- liftM FunIx (paren $ many expY) <|>
liftM TupIx integer <|>
liftM RecIx identifier
v <- expY
return $ case ix of FunIx es -> UPDATE_F e es v
TupIx i -> UPDATE_T e i v
RecIx f -> UPDATE_R e f v
select = do tok "select"
e <- expY
ix <- liftM TupIx integer <|>
liftM RecIx identifier
return $ case ix of TupIx i -> SELECT_T e i
RecIx f -> SELECT_R e f
app = liftM2 APP expY (many1 expY)
binding = do x <- identifier
mt <- optionMaybe $ tok "::" >> (vart <|> paren typYinParen)
e <- expY
return ((x,mt),e)
data IndexType = FunIx [ExpY] | TupIx Integer | RecIx String
cmdY :: GenParser Char st CmdY
cmdY = paren $ try deftyp <|> define <|> try assert <|> assertp <|> retract <|>
check <|> maxsat <|> sete <|> setv <|> setao <|> push <|> pop <|>
echo <|> include <|> status <|> dump <|> exit
deftyp = tok "define-type" >> liftM2 DEFTYP identifier (optionMaybe typY)
define = tok "define" >> liftM2 DEFINE idty (optionMaybe expY)
assert = tok "assert" >> liftM ASSERT expY
assertp = tok "assert+" >> liftM2 ASSERT_P expY (optionMaybe integer)
retract = tok "retract" >> liftM RETRACT integer
check = tok "check" >> return CHECK
maxsat = tok "max-sat" >> return MAXSAT
sete = tok "set-evidence!" >> liftM SETE boolean
setv = tok "set-verbosity!" >> liftM SETV integer
setao = tok "set-arith-only!" >> liftM SETAO boolean
push = tok "push" >> return PUSH
pop = tok "pop" >> return POP
echo = tok "echo" >> liftM ECHO stringLiteral
include = tok "include" >> liftM ECHO stringLiteral
reset = tok "reset" >> return RESET
status = tok "status" >> return DUMP
dump = tok "dump-context" >> return DUMP
exit = tok "exit" >> return EXIT