    -- This file is based on:
    --
    -- "The SMT-LIB Standard, Version 1.2"
    -- by Silvio Ranise and Cesare Tinelli
    -- Release: 5 August 2006
    -- Appendix A
    --
    -- URL:
    -- http://goedel.cs.uiowa.edu/smtlib/papers/format-v1.2-r06.08.05.pdf

    {-# 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)

    -- aka "benchmark"
    data Script = Script { scrName :: Ident, scrCommands :: [Command] }

    --------------------------------------------------------------------------------
    -- To make it a bit simpler to write terms in the above AST
    -- we provide some instances.  They are intended to be used only
    -- for writing simple literals, and not any of the computational
    -- operations associated with the classes.

    -- Strings
    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)

    -- Integral operations
    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]

    -- Fractional numbers
    instance Fractional Term where
      fromRational  = Lit . LitFrac . fromRational
      x / y         = App "/" [x,y]

    --------------------------------------------------------------------------------
    -- XXX: move to a separate module?

    (===) :: Term -> Term -> Formula
    x === y   = FPred "=" [x,y]

    (=/=) :: Term -> Term -> Formula
    x =/= y   = FPred "distinct" [x,y]

    -- | For 'Int'
    (.<.) :: Term -> Term -> Formula
    x .<. y   = FPred "<" [x,y]

    -- | For 'Int'
    (.>.) :: 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