{-# LANGUAGE OverloadedStrings #-}

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

module Language.Fixpoint.Solver.Common (askSMT, toSMT) where

import Language.Fixpoint.Types.Config (Config)
import Language.Fixpoint.Smt.Interface (Context(..), checkValidWithContext)
import Language.Fixpoint.Types
import Language.Fixpoint.Types.Visitor (kvarsExpr)
import Language.Fixpoint.Defunctionalize (defuncAny)
import Language.Fixpoint.SortCheck (elaborate)

mytracepp :: (PPrint a) => String -> a -> a
mytracepp :: forall a. PPrint a => [Char] -> a -> a
mytracepp = forall a. PPrint a => [Char] -> a -> a
notracepp

askSMT :: Config -> Context -> [(Symbol, Sort)] -> Expr -> IO Bool
askSMT :: Config -> Context -> [(Symbol, Sort)] -> Pred -> IO Bool
askSMT Config
cfg Context
ctx [(Symbol, Sort)]
bs Pred
e
--   | isContraPred e  = return False
  | Pred -> Bool
isTautoPred  Pred
e     = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  | forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Pred -> [KVar]
kvarsExpr Pred
e) = Context -> [(Symbol, Sort)] -> Pred -> Pred -> IO Bool
checkValidWithContext Context
ctx [] Pred
PTrue Pred
e'
  | Bool
otherwise          = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  where
    e' :: Pred
e' = [Char] -> Config -> Context -> [(Symbol, Sort)] -> Pred -> Pred
toSMT [Char]
"askSMT" Config
cfg Context
ctx [(Symbol, Sort)]
bs Pred
e

toSMT :: String -> Config -> Context -> [(Symbol, Sort)] -> Expr -> Pred
toSMT :: [Char] -> Config -> Context -> [(Symbol, Sort)] -> Pred -> Pred
toSMT [Char]
msg Config
cfg Context
ctx [(Symbol, Sort)]
bs Pred
e =
    forall a. Defunc a => Config -> SymEnv -> a -> a
defuncAny Config
cfg SymEnv
senv forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        forall a. Elaborate a => Located [Char] -> SymEnv -> a -> a
elaborate (forall a. a -> Located a
dummyLoc [Char]
msg) ([(Symbol, Sort)] -> SymEnv
elabEnv [(Symbol, Sort)]
bs) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            forall a. PPrint a => [Char] -> a -> a
mytracepp ([Char]
"toSMT from " forall a. [a] -> [a] -> [a]
++ [Char]
msg forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp Pred
e) forall a b. (a -> b) -> a -> b
$
                Pred
e
  where
    elabEnv :: [(Symbol, Sort)] -> SymEnv
elabEnv = SymEnv -> [(Symbol, Sort)] -> SymEnv
insertsSymEnv SymEnv
senv
    senv :: SymEnv
senv    = Context -> SymEnv
ctxSymEnv Context
ctx