module Math.SMT.Yices.Syntax ( TypY(..) , ExpY(..) , CmdY(..) ) where
import Char
import List
import Ratio
data TypY
= VarT String
| SUBTYPE (String,TypY) ExpY
| SUBRANGE ExpY ExpY
| ARR [TypY]
| TUP [TypY]
| REC [(String,TypY)]
| DEP (String,TypY)
| DATATYPE [(String,[(String,TypY)])]
| SCALAR [String]
data ExpY
= VarE String
| LitB Bool
| LitI Integer
| LitR Rational
| AND [ExpY]
| OR [ExpY]
| NOT ExpY
| ExpY :=> ExpY
| ExpY := ExpY
| ExpY :/= ExpY
| ExpY :< ExpY
| ExpY :<= ExpY
| ExpY :> ExpY
| ExpY :>= ExpY
| ExpY :+: ExpY
| ExpY :-: ExpY
| ExpY :*: ExpY
| ExpY :/: ExpY
| DIV ExpY ExpY
| MOD ExpY ExpY
| IF ExpY ExpY ExpY
| ITE ExpY ExpY ExpY
| LET [((String,Maybe TypY),ExpY)] ExpY
| FORALL [(String,TypY)] ExpY
| EXISTS [(String,TypY)] ExpY
| APP ExpY [ExpY]
| UPDATE_F ExpY [ExpY] ExpY
| LAMBDA [(String,TypY)] ExpY
| MKTUP [ExpY]
| SELECT_T ExpY Integer
| UPDATE_T ExpY Integer ExpY
| MKREC [(String,ExpY)]
| SELECT_R ExpY String
| UPDATE_R ExpY String ExpY
data CmdY
= DEFTYP String (Maybe TypY)
| DEFINE (String,TypY) (Maybe ExpY)
| ASSERT ExpY
| ASSERT_P ExpY (Maybe Integer)
| RETRACT Integer
| CHECK
| MAXSAT
| SETE Bool
| SETV Integer
| SETAO Bool
| PUSH
| POP
| ECHO String
| INCLUDE String
| RESET
| STATUS
| DUMP
| EXIT
paren s = "("++s++")"
showListSepByWith showFun sep = concat . intersperse sep . map showFun
showListSepBy :: (Show a) => String -> [a] -> String
showListSepBy = showListSepByWith show
showStringsSepBy = showListSepByWith id
showIdTyp (tname,t) = tname++"::"++show t
showIdVal (fname,e) = fname++"::"++show e
showCtorDef (c,[]) = c
showCtorDef (c,idtyps) = paren $ c++" "++showListSepByWith showIdTyp " " idtyps
showBinding ((x,Just t),e) = paren $ showIdTyp(x,t) ++ " " ++ show e
showBinding ((x,Nothing),e) = paren $ x ++ " " ++ show e
instance Show TypY where
show (VarT tname) = tname
show (SUBTYPE idty e) = paren $ "subtype " ++ showIdTyp idty ++ " " ++ show e
show (SUBRANGE e1 e2) = paren $ "subrange " ++ show e1 ++ " " ++ show e2
show (ARR ts) = paren $ "-> " ++ showListSepBy " " ts
show (TUP ts) = paren $ "tuple " ++ showListSepBy " " ts
show (REC idtyps) = paren $ "record " ++ showListSepByWith showIdTyp " " idtyps
show (DEP idty) = showIdTyp idty
show (DATATYPE ctordefs) =
paren $ "datatype " ++ showListSepByWith showCtorDef " " ctordefs
show (SCALAR tnames) = paren $ "scalar " ++ showStringsSepBy " " tnames
instance Show ExpY where
show (VarE x) = x
show (LitB True) = "true"
show (LitB False) = "false"
show (LitI n) = show n
show (LitR r) = show (numerator r) ++ "/" ++ show (denominator r)
show (AND es) = paren $ "and " ++ showListSepBy " " es
show (OR es) = paren $ "or " ++ showListSepBy " " es
show (NOT e) = paren $ "not " ++ show e
show (e1 :=> e2) = paren $ "=> " ++ show e1 ++ " " ++ show e2
show (e1 := e2) = paren $ "= " ++ show e1 ++ " " ++ show e2
show (e1 :/= e2) = paren $ "/= " ++ show e1 ++ " " ++ show e2
show (e1 :< e2) = paren $ "< " ++ show e1 ++ " " ++ show e2
show (e1 :<= e2) = paren $ "<= " ++ show e1 ++ " " ++ show e2
show (e1 :> e2) = paren $ "> " ++ show e1 ++ " " ++ show e2
show (e1 :>= e2) = paren $ ">= " ++ show e1 ++ " " ++ show e2
show (e1 :+: e2) = paren $ "+ " ++ show e1 ++ " " ++ show e2
show (e1 :-: e2) = paren $ "- " ++ show e1 ++ " " ++ show e2
show (e1 :*: e2) = paren $ "* " ++ show e1 ++ " " ++ show e2
show (e1 :/: e2) = paren $ "/ " ++ show e1 ++ " " ++ show e2
show (DIV e1 e2) = paren $ "div " ++ show e1 ++ " " ++ show e2
show (MOD e1 e2) = paren $ "mod " ++ show e1 ++ " " ++ show e2
show (IF eb et ef) = paren $ "if " ++ showListSepBy " " [eb,et,ef]
show (ITE eb et ef) = paren $ "ite " ++ showListSepBy " " [eb,et,ef]
show (LET bindings e) = paren $ "let " ++ (paren $ showListSepByWith showBinding " " bindings) ++ " "++ show e
show (FORALL idtyps e) = paren $ "forall "
++ (paren $ showListSepByWith showIdTyp " " idtyps) ++ " " ++ show e
show (EXISTS idtyps e) = paren $ "exists "
++ (paren $ showListSepByWith showIdTyp " " idtyps) ++ " " ++ show e
show (APP e es) = paren $ showListSepBy " " (e:es)
show (UPDATE_F e es v) = paren $ "update "
++ show e ++ " " ++ (paren $ showListSepBy " " es) ++ show v
show (LAMBDA idtyps e) = paren $ "lambda "
++ (paren $ showListSepByWith showIdTyp " " idtyps) ++ show e
show (MKTUP es) = paren $ "mk-tuple " ++ showListSepBy " " es
show (SELECT_T e i) = paren $ "select " ++ show e ++ " " ++ show i
show (UPDATE_T e i v) = paren $ "update "
++ show e ++ " " ++ show i ++ " " ++ show v
show (MKREC idvals) = paren $ "mk-record "
++ showListSepByWith showIdVal " " idvals
show (SELECT_R e s) = paren $ "select " ++ show e ++ " " ++ s
show (UPDATE_R e s v) = paren $ "update "
++ show e ++ " " ++ s ++ " " ++ show v
instance Show CmdY where
show (DEFTYP tname Nothing) = paren $ "define-type " ++ tname
show (DEFTYP tname (Just t)) = paren $ "define-type "++ tname ++ " " ++ show t
show (DEFINE idty Nothing) = paren $ "define " ++ showIdTyp idty
show (DEFINE idty (Just e)) = paren $ "define " ++ showIdTyp idty ++ show e
show (ASSERT e) = paren $ "assert " ++ show e
show (ASSERT_P e Nothing) = paren $ "assert+ " ++ show e
show (ASSERT_P e (Just w)) = paren $ "assert+ " ++ show e ++ " " ++ show w
show (RETRACT i) = paren $ "retract " ++ show i
show (CHECK) = paren "check"
show (MAXSAT) = paren "max-sat"
show (SETE b) = paren $ "set-evidence! " ++ show (LitB b)
show (SETV k) = paren $ "set-verbosity! " ++ show k
show (SETAO b) = paren $ "set-arith-only! " ++ show (LitB b)
show (PUSH) = paren "push"
show (POP) = paren "pop"
show (ECHO s) = paren $ "echo " ++ show s
show (INCLUDE s) = paren $ "include " ++ show s
show (RESET) = paren "reset"
show (STATUS) = paren "status"
show (DUMP) = paren "dump-context"
show (EXIT) = paren "exit"