{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE UndecidableInstances      #-}

{-# OPTIONS_GHC -Wno-name-shadowing    #-}

-- | This module contains the types defining an SMTLIB2 interface.

module Language.Fixpoint.Smt.Types (

    -- * Serialized Representation
    --    symbolBuilder

    -- * Commands
      Command  (..)

    -- * Responses
    , Response (..)

    -- * Typeclass for SMTLIB2 conversion
    , SMTLIB2 (..)
    , runSmt2

    -- * SMTLIB2 Process Context
    , Context (..)

    ) where

import           Data.ByteString.Builder (Builder)
import           Language.Fixpoint.Types
import qualified Data.Text                as T
import           Text.PrettyPrint.HughesPJ
import qualified SMTLIB.Backends

import           System.IO                (Handle)
-- import           Language.Fixpoint.Misc   (traceShow)

--------------------------------------------------------------------------------
-- | Types ---------------------------------------------------------------------
--------------------------------------------------------------------------------

-- symbolBuilder :: Symbol -> LT.Builder
-- symbolBuilder = LT.fromText . symbolSafeText

-- | Commands issued to SMT engine
data Command      = Push
                  | Pop
                  | Exit
                  | SetMbqi
                  | CheckSat
                  | DeclData ![DataDecl]
                  | Declare  T.Text [SmtSort] !SmtSort
                  | Define   !Sort
                  | DefineFunc Symbol [(Symbol, SmtSort)] !SmtSort Expr
                  | Assert   !(Maybe Int) !Expr
                  | AssertAx !(Triggered Expr)
                  | Distinct [Expr] -- {v:[Expr] | 2 <= len v}
                  | GetValue [Symbol]
                  | CMany    [Command]
                  deriving (Command -> Command -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Command -> Command -> Bool
$c/= :: Command -> Command -> Bool
== :: Command -> Command -> Bool
$c== :: Command -> Command -> Bool
Eq, Int -> Command -> ShowS
[Command] -> ShowS
Command -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Command] -> ShowS
$cshowList :: [Command] -> ShowS
show :: Command -> String
$cshow :: Command -> String
showsPrec :: Int -> Command -> ShowS
$cshowsPrec :: Int -> Command -> ShowS
Show)

instance PPrint Command where
  pprintTidy :: Tidy -> Command -> Doc
pprintTidy Tidy
_ = Command -> Doc
ppCmd

ppCmd :: Command -> Doc
ppCmd :: Command -> Doc
ppCmd Command
Exit             = String -> Doc
text String
"Exit"
ppCmd Command
SetMbqi          = String -> Doc
text String
"SetMbqi"
ppCmd Command
Push             = String -> Doc
text String
"Push"
ppCmd Command
Pop              = String -> Doc
text String
"Pop"
ppCmd Command
CheckSat         = String -> Doc
text String
"CheckSat"
ppCmd (DeclData [DataDecl]
d)     = String -> Doc
text String
"Data" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint [DataDecl]
d
ppCmd (Declare Text
x [] SmtSort
t) = String -> Doc
text String
"Declare" Doc -> Doc -> Doc
<+> String -> Doc
text (Text -> String
T.unpack Text
x) Doc -> Doc -> Doc
<+> String -> Doc
text String
":" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint SmtSort
t
ppCmd (Declare Text
x [SmtSort]
ts SmtSort
t) = String -> Doc
text String
"Declare" Doc -> Doc -> Doc
<+> String -> Doc
text (Text -> String
T.unpack Text
x) Doc -> Doc -> Doc
<+> String -> Doc
text String
":" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (forall a. PPrint a => a -> Doc
pprint [SmtSort]
ts) Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint SmtSort
t
ppCmd Define {}   = String -> Doc
text String
"Define ..."
ppCmd (DefineFunc Symbol
name [(Symbol, SmtSort)]
params SmtSort
rsort Expr
e) =
  String -> Doc
text String
"DefineFunc" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint Symbol
name Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint [(Symbol, SmtSort)]
params Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint SmtSort
rsort Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint Expr
e
ppCmd (Assert Maybe Int
_ Expr
e)  = String -> Doc
text String
"Assert" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint Expr
e
ppCmd (AssertAx Triggered Expr
_)  = String -> Doc
text String
"AssertAxiom ..."
ppCmd Distinct {} = String -> Doc
text String
"Distinct ..."
ppCmd GetValue {} = String -> Doc
text String
"GetValue ..."
ppCmd CMany {}    = String -> Doc
text String
"CMany ..."

-- | Responses received from SMT engine
data Response     = Ok
                  | Sat
                  | Unsat
                  | Unknown
                  | Values [(Symbol, T.Text)]
                  | Error !T.Text
                  deriving (Response -> Response -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Response -> Response -> Bool
$c/= :: Response -> Response -> Bool
== :: Response -> Response -> Bool
$c== :: Response -> Response -> Bool
Eq, Int -> Response -> ShowS
[Response] -> ShowS
Response -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Response] -> ShowS
$cshowList :: [Response] -> ShowS
show :: Response -> String
$cshow :: Response -> String
showsPrec :: Int -> Response -> ShowS
$cshowsPrec :: Int -> Response -> ShowS
Show)

-- | Additional information around the SMT solver backend
data Context = Ctx
  {
  -- | The high-level interface for interacting with the SMT solver backend.
    Context -> Solver
ctxSolver  :: SMTLIB.Backends.Solver
  -- | The close operation of the SMT solver backend.
  , Context -> IO ()
ctxClose   :: IO ()
  , Context -> Maybe Handle
ctxLog     :: !(Maybe Handle)
  , Context -> Bool
ctxVerbose :: !Bool
  , Context -> SymEnv
ctxSymEnv  :: !SymEnv
  }

--------------------------------------------------------------------------------
-- | AST Conversion: Types that can be serialized ------------------------------
--------------------------------------------------------------------------------

class SMTLIB2 a where
  smt2 :: SymEnv -> a -> Builder

runSmt2 :: (SMTLIB2 a) => SymEnv -> a -> Builder
runSmt2 :: forall a. SMTLIB2 a => SymEnv -> a -> Builder
runSmt2 = forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2