content: {-# 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)
  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 (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 ..."
  
  -- | 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
    }
  
  -- | 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
  