module SMTLib2.AST where
import Data.Typeable
import Data.Data
import Data.String(IsString(..))
newtype Name = N String
deriving (Eq,Ord,Show,Data,Typeable)
data Ident = I Name [Integer]
deriving (Eq,Ord,Show,Data,Typeable)
data Quant = Exists | Forall
deriving (Eq,Ord,Show,Data,Typeable)
data Binder = Bind { bindVar :: Name, bindType :: Type }
deriving (Eq,Ord,Show,Data,Typeable)
data Defn = Defn { defVar :: Name, defExpr :: Expr }
deriving (Eq,Ord,Show,Data,Typeable)
data Literal = LitBV Integer Integer
| LitNum Integer
| LitFrac Rational
| LitStr String
deriving (Eq,Ord,Show,Data,Typeable)
data Type = TApp Ident [Type]
| TVar Name
deriving (Eq,Ord,Show,Data,Typeable)
data Expr = Lit Literal
| App Ident (Maybe Type) [Expr]
| Quant Quant [Binder] Expr
| Let [Defn] Expr
| Annot Expr [Attr]
deriving (Eq,Ord,Show,Data,Typeable)
data Attr = Attr { attrName :: Name , attrVal :: Maybe AttrVal }
deriving (Eq,Ord,Show,Data,Typeable)
type AttrVal = Expr
data Option
= OptPrintSuccess Bool
| OptExpandDefinitions Bool
| OptInteractiveMode Bool
| OptProduceProofs Bool
| OptProduceUnsatCores Bool
| OptProduceModels Bool
| OptProduceAssignments Bool
| OptRegularOutputChannel String
| OptDiagnosticOutputChannel String
| OptRandomSeed Integer
| OptVerbosity Integer
| OptAttr Attr
deriving (Data,Typeable)
data InfoFlag
= InfoAllStatistics
| InfoErrorBehavior
| InfoName
| InfoAuthors
| InfoVersion
| InfoStatus
| InfoReasonUnknown
| InfoAttr Attr
deriving (Data,Typeable)
data Command
= CmdSetLogic Name
| CmdSetOption Option
| CmdSetInfo Attr
| CmdDeclareType Name Integer
| CmdDefineType Name [Name] Type
| CmdDeclareFun Name [Type] Type
| CmdDefineFun Name [Binder] Type Expr
| CmdPush Integer
| CmdPop Integer
| CmdAssert Expr
| CmdCheckSat
| CmdGetAssertions
| CmdGetValue [Expr]
| CmdGetProof
| CmdGetUnsatCore
| CmdGetInfo InfoFlag
| CmdGetOption Name
| CmdComment String
| CmdExit
deriving (Data,Typeable)
newtype Script = Script [Command]
instance IsString Name where fromString = N
instance IsString Ident where fromString x = I (fromString x) []
instance IsString Type where fromString x = TApp (fromString x) []
instance IsString Expr where fromString = Lit . LitStr . fromString
instance Num Expr where
fromInteger x = Lit (LitNum x)
x + y = app "+" [x,y]
x y = app "-" [x,y]
x * y = app "*" [x,y]
signum x = app "signum" [x]
abs x = app "abs" [x]
instance Fractional Expr where
fromRational x = Lit (LitFrac x)
x / y = app "/" [x,y]
app :: Ident -> [Expr] -> Expr
app f es = App f Nothing es