Types.hs

{-# 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 (Eq, Show)

instance PPrint Command where
  pprintTidy _ = ppCmd

ppCmd :: Command -> Doc
ppCmd Exit             = text "Exit"
ppCmd SetMbqi          = text "SetMbqi"
ppCmd Push             = text "Push"
ppCmd Pop              = text "Pop"
ppCmd CheckSat         = text "CheckSat"
ppCmd (DeclData d)     = text "Data" <+> pprint d
ppCmd (Declare x [] t) = text "Declare" <+> text (T.unpack x) <+> text ":" <+> pprint t
ppCmd (Declare x ts t) = text "Declare" <+> text (T.unpack x) <+> text ":" <+> parens (pprint ts) <+> pprint t
ppCmd Define {}   = text "Define ..."
ppCmd (DefineFunc name symList rsort e) =
  text "DefineFunc" <+> pprint name <+> pprint symList <+> pprint rsort <+> pprint e
ppCmd (Assert _ e)  = text "Assert" <+> pprint e
ppCmd (AssertAx _)  = text "AssertAxiom ..."
ppCmd Distinct {} = text "Distinct ..."
ppCmd GetValue {} = text "GetValue ..."
ppCmd CMany {}    = text "CMany ..."
ppCmd (Comment t) = text ("; " ++ T.unpack t)

-- | Responses received from SMT engine
data Response     = Ok
                  | Sat
                  | Unsat
                  | Unknown
                  | Values [(Symbol, T.Text)]
                  | Error !T.Text
                  deriving (Eq, Show)

-- | Additional information around the SMT solver backend
data Context = Ctx
  {
  -- | The high-level interface for interacting with the SMT solver backend.
    ctxSolver  :: SMTLIB.Backends.Solver
  , ctxElabF   :: ElabFlags
  -- | The close operation of the SMT solver backend.
  , ctxClose   :: IO ()
  , ctxLog     :: !(Maybe Handle)
  , ctxVerbose :: !Bool
  , ctxSymEnv  :: !SymEnv
  -- | The stack of sort indexes which were fresh at the corresponding level of push/pop stack.
  , ctxIxs     :: ![Int]
  , ctxDefines :: DefinedFuns
  -- | Flag which controls the generation SMT placeholders for lambda arguments
  --   See also `L.F.Smt.Theories.maxLamArg`
  , ctxLams    :: !Bool
  -- | Configuration options
  , 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 s =
  do ctx <- get
     let (a, env') = runState s (ctxSymEnv ctx)
     put (ctx {ctxSymEnv = env'})
     pure a

catchSMT :: Exception e => SmtM a -> (e -> IO a) -> SmtM a
catchSMT action handler = StateT $ \s -> catch (runStateT action s) (fmap (, s) . handler)

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

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

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

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