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


-- | 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 (..)

    -- * SMT monad
    , SmtM
    , liftSym
    , catchSMT
    , bracketSMT

    ) where
import           Control.Exception
import           Control.Monad.State
import           Data.ByteString.Builder (Builder)
import           Language.Fixpoint.Types
import           Language.Fixpoint.Types.Config (ElabFlags, Config)
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]
                  | Comment T.Text
                  deriving (Command -> Command -> Bool
(Command -> Command -> Bool)
-> (Command -> Command -> Bool) -> Eq Command
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Command -> Command -> Bool
== :: Command -> Command -> Bool
$c/= :: Command -> Command -> Bool
/= :: Command -> Command -> Bool
Eq, Int -> Command -> ShowS
[Command] -> ShowS
Command -> [Char]
(Int -> Command -> ShowS)
-> (Command -> [Char]) -> ([Command] -> ShowS) -> Show Command
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Command -> ShowS
showsPrec :: Int -> Command -> ShowS
$cshow :: Command -> [Char]
show :: Command -> [Char]
$cshowList :: [Command] -> ShowS
showList :: [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             = [Char] -> Doc
text [Char]
"Exit"
ppCmd Command
SetMbqi          = [Char] -> Doc
text [Char]
"SetMbqi"
ppCmd Command
Push             = [Char] -> Doc
text [Char]
"Push"
ppCmd Command
Pop              = [Char] -> Doc
text [Char]
"Pop"
ppCmd Command
CheckSat         = [Char] -> Doc
text [Char]
"CheckSat"
ppCmd (DeclData [DataDecl]
d)     = [Char] -> Doc
text [Char]
"Data" Doc -> Doc -> Doc
<+> [DataDecl] -> Doc
forall a. PPrint a => a -> Doc
pprint [DataDecl]
d
ppCmd (Declare Text
x [] SmtSort
t) = [Char] -> Doc
text [Char]
"Declare" Doc -> Doc -> Doc
<+> [Char] -> Doc
text (Text -> [Char]
T.unpack Text
x) Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
":" Doc -> Doc -> Doc
<+> SmtSort -> Doc
forall a. PPrint a => a -> Doc
pprint SmtSort
t
ppCmd (Declare Text
x [SmtSort]
ts SmtSort
t) = [Char] -> Doc
text [Char]
"Declare" Doc -> Doc -> Doc
<+> [Char] -> Doc
text (Text -> [Char]
T.unpack Text
x) Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
":" Doc -> Doc -> Doc
<+> Doc -> Doc
parens ([SmtSort] -> Doc
forall a. PPrint a => a -> Doc
pprint [SmtSort]
ts) Doc -> Doc -> Doc
<+> SmtSort -> Doc
forall a. PPrint a => a -> Doc
pprint SmtSort
t
ppCmd Define {}   = [Char] -> Doc
text [Char]
"Define ..."
ppCmd (DefineFunc Symbol
name [(Symbol, SmtSort)]
symList SmtSort
rsort Expr
e) =
  [Char] -> Doc
text [Char]
"DefineFunc" Doc -> Doc -> Doc
<+> Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint Symbol
name Doc -> Doc -> Doc
<+> [(Symbol, SmtSort)] -> Doc
forall a. PPrint a => a -> Doc
pprint [(Symbol, SmtSort)]
symList Doc -> Doc -> Doc
<+> SmtSort -> Doc
forall a. PPrint a => a -> Doc
pprint SmtSort
rsort Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. PPrint a => a -> Doc
pprint Expr
e
ppCmd (Assert Maybe Int
_ Expr
e)  = [Char] -> Doc
text [Char]
"Assert" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. PPrint a => a -> Doc
pprint Expr
e
ppCmd (AssertAx Triggered Expr
_)  = [Char] -> Doc
text [Char]
"AssertAxiom ..."
ppCmd Distinct {} = [Char] -> Doc
text [Char]
"Distinct ..."
ppCmd GetValue {} = [Char] -> Doc
text [Char]
"GetValue ..."
ppCmd CMany {}    = [Char] -> Doc
text [Char]
"CMany ..."
ppCmd (Comment Text
t) = [Char] -> Doc
text ([Char]
"; " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
T.unpack Text
t)

-- | Responses received from SMT engine
data Response     = Ok
                  | Sat
                  | Unsat
                  | Unknown
                  | Values [(Symbol, T.Text)]
                  | Error !T.Text
                  deriving (Response -> Response -> Bool
(Response -> Response -> Bool)
-> (Response -> Response -> Bool) -> Eq Response
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Response -> Response -> Bool
== :: Response -> Response -> Bool
$c/= :: Response -> Response -> Bool
/= :: Response -> Response -> Bool
Eq, Int -> Response -> ShowS
[Response] -> ShowS
Response -> [Char]
(Int -> Response -> ShowS)
-> (Response -> [Char]) -> ([Response] -> ShowS) -> Show Response
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Response -> ShowS
showsPrec :: Int -> Response -> ShowS
$cshow :: Response -> [Char]
show :: Response -> [Char]
$cshowList :: [Response] -> ShowS
showList :: [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
  , Context -> ElabFlags
ctxElabF   :: ElabFlags
  -- | 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
  -- | The stack of sort indexes which were fresh at the corresponding level of push/pop stack.
  , Context -> [Int]
ctxIxs     :: ![Int]
  , Context -> DefinedFuns
ctxDefines :: DefinedFuns
  -- | Flag which controls the generation SMT placeholders for lambda arguments
  --   See also `L.F.Smt.Theories.maxLamArg`
  , Context -> Bool
ctxLams    :: !Bool
  -- | Configuration options
  , Context -> Config
config     :: !Config
  }

-- | SMT monad, used to communicate with the SMT solver backend.
--   The `SymM` monad embeds into it, as the symbolic state has to be threaded
--   through for gnerating `apply`s and other function sort symbols.
type SmtM = StateT Context IO

liftSym :: SymM a -> SmtM a
liftSym :: forall a. SymM a -> SmtM a
liftSym SymM a
s =
  do Context
ctx <- StateT Context IO Context
forall s (m :: * -> *). MonadState s m => m s
get
     let (a
a, SymEnv
env') = SymM a -> SymEnv -> (a, SymEnv)
forall s a. State s a -> s -> (a, s)
runState SymM a
s (Context -> SymEnv
ctxSymEnv Context
ctx)
     Context -> StateT Context IO ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Context
ctx {ctxSymEnv = env'})
     a -> SmtM a
forall a. a -> StateT Context IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a

catchSMT :: Exception e => SmtM a -> (e -> IO a) -> SmtM a
catchSMT :: forall e a. Exception e => SmtM a -> (e -> IO a) -> SmtM a
catchSMT SmtM a
action e -> IO a
handler = (Context -> IO (a, Context)) -> SmtM a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((Context -> IO (a, Context)) -> SmtM a)
-> (Context -> IO (a, Context)) -> SmtM a
forall a b. (a -> b) -> a -> b
$ \Context
s -> IO (a, Context) -> (e -> IO (a, Context)) -> IO (a, Context)
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
catch (SmtM a -> Context -> IO (a, Context)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT SmtM a
action Context
s) ((a -> (a, Context)) -> IO a -> IO (a, Context)
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (, Context
s) (IO a -> IO (a, Context)) -> (e -> IO a) -> e -> IO (a, Context)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> IO a
handler)

bracketSMT :: SmtM a -> (a -> IO b) -> (a -> SmtM c) -> SmtM c
bracketSMT :: forall a b c. SmtM a -> (a -> IO b) -> (a -> SmtM c) -> SmtM c
bracketSMT SmtM a
acquire a -> IO b
release a -> SmtM c
use = (Context -> IO (c, Context)) -> SmtM c
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((Context -> IO (c, Context)) -> SmtM c)
-> (Context -> IO (c, Context)) -> SmtM c
forall a b. (a -> b) -> a -> b
$ \Context
s ->
  IO (a, Context)
-> ((a, Context) -> IO b)
-> ((a, Context) -> IO (c, Context))
-> IO (c, Context)
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
bracket
    (SmtM a -> Context -> IO (a, Context)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT SmtM a
acquire Context
s)
    (\(a
resource, Context
_) -> a -> IO b
release a
resource)
    (\(a
resource, Context
intermediateState) -> SmtM c -> Context -> IO (c, Context)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (a -> SmtM c
use a
resource) Context
intermediateState)

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

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

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