{-# LANGUAGE OverloadedStrings, Safe, DeriveDataTypeable #-}
module SMTLib1.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 Conn = Not | Implies | And | Or | Xor | Iff | IfThenElse
deriving (Eq,Ord,Show,Data,Typeable)
data Formula = FTrue
| FFalse
| FPred Ident [Term]
| FVar Name
| Conn Conn [Formula]
| Quant Quant [Binder] Formula
| Let Name Term Formula
| FLet Name Formula Formula
| FAnnot Formula [Annot]
deriving (Eq,Ord,Show,Data,Typeable)
type Sort = Ident
data Binder = Bind { bindVar :: Name, bindSort :: Sort }
deriving (Eq,Ord,Show,Data,Typeable)
data Term = Var Name
| App Ident [Term]
| Lit Literal
| ITE Formula Term Term
| TAnnot Term [Annot]
deriving (Eq,Ord,Show,Data,Typeable)
data Literal = LitNum Integer
| LitFrac Rational
| LitStr String
deriving (Eq,Ord,Show,Data,Typeable)
data Annot = Attr { attrName :: Name, attrVal :: Maybe String }
deriving (Eq,Ord,Show,Data,Typeable)
data FunDecl = FunDecl { funName :: Ident
, funArgs :: [Sort]
, funRes :: Sort
, funAnnots :: [Annot]
}
deriving (Data,Typeable)
data PredDecl = PredDecl { predName :: Ident
, predArgs :: [Sort]
, predAnnots :: [Annot]
}
deriving (Data,Typeable)
data Status = Sat | Unsat | Unknown
deriving (Data,Typeable)
data Command
= CmdLogic Ident
| CmdAssumption Formula
| CmdFormula Formula
| CmdStatus Status
| CmdExtraSorts [ Sort ]
| CmdExtraFuns [ FunDecl ]
| CmdExtraPreds [ PredDecl ]
| CmdNotes String
| CmdAnnot Annot
deriving (Data,Typeable)
data Script = Script { scrName :: Ident, scrCommands :: [Command] }
instance IsString Name where fromString x = N x
instance IsString Ident where fromString x = I (fromString x) []
instance IsString Term where fromString x = Lit (LitStr x)
instance Num Term where
fromInteger = Lit . LitNum
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 Term where
fromRational = Lit . LitFrac . fromRational
x / y = App "/" [x,y]
(===) :: Term -> Term -> Formula
x === y = FPred "=" [x,y]
(=/=) :: Term -> Term -> Formula
x =/= y = FPred "distinct" [x,y]
(.<.) :: Term -> Term -> Formula
x .<. y = FPred "<" [x,y]
(.>.) :: Term -> Term -> Formula
x .>. y = FPred ">" [x,y]
tInt :: Sort
tInt = "Int"
funDef :: Ident -> [Sort] -> Sort -> Command
funDef x as b = CmdExtraFuns [ FunDecl { funName = x
, funArgs = as
, funRes = b
, funAnnots = []
} ]
constDef :: Ident -> Sort -> Command
constDef x t = funDef x [] t
logic :: Ident -> Command
logic = CmdLogic
assume :: Formula -> Command
assume = CmdAssumption
goal :: Formula -> Command
goal = CmdFormula