[commit: ghc] wip/ext-solver: Add an instance of the external solver to the TcSMonad (e55edee)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : wip/ext-solver
Link       : http://ghc.haskell.org/trac/ghc/changeset/e55edee2c924ef7735faad8166ef555063e76825/ghc

>---------------------------------------------------------------

commit e55edee2c924ef7735faad8166ef555063e76825
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date:   Mon Apr 28 21:23:42 2014 -0700

    Add an instance of the external solver to the TcSMonad


>---------------------------------------------------------------

e55edee2c924ef7735faad8166ef555063e76825
 compiler/typecheck/TcSMonad.lhs |   39 ++++++++++++++++++++++++++++++++++++++-
 1 file changed, 38 insertions(+), 1 deletion(-)

diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 51f4945..6a43511 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -83,6 +83,8 @@ module TcSMonad (
     Untouchables, isTouchableMetaTyVarTcS, isFilledMetaTyVar_maybe,
     zonkTyVarsAndFV,
 
+    TN.ExtSolRes(..), extSolSend, extSolPush, extSolPop, extSolCheck,
+
     getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
 
     matchFam, matchOpenFam,
@@ -112,6 +114,7 @@ import TcType
 import DynFlags
 import Type
 import CoAxiom(sfMatchFam)
+import qualified TcTypeNats as TN
 
 import TcEvidence
 import Class
@@ -976,7 +979,9 @@ data TcSEnv
       -- while solving or canonicalising the current worklist.
       -- Specifically, when canonicalising (forall a. t1 ~ forall a. t2)
       -- from which we get the implication (forall a. t1 ~ t2)
-      tcs_implics  :: IORef (Bag Implication)
+      tcs_implics  :: IORef (Bag Implication),
+
+      tcs_ext_solver :: TN.ExternalSolver
     }
 \end{code}
 
@@ -1064,10 +1069,15 @@ runTcSWithEvBinds ev_binds_var tcs
        ; step_count <- TcM.newTcRef 0
        ; inert_var <- TcM.newTcRef is
 
+       ; extSol <- liftIO $
+                   TN.newExternalSolver "cvc4" [ "--incremental"
+                                               , "--lang=smtlib2" ]
+
        ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
                           , tcs_ty_binds = ty_binds_var
                           , tcs_count    = step_count
                           , tcs_inerts   = inert_var
+                          , tcs_ext_solver = extSol
                           , tcs_worklist    = panic "runTcS: worklist"
                           , tcs_implics     = panic "runTcS: implics" }
                                -- NB: Both these are initialised by withWorkList
@@ -1087,6 +1097,7 @@ runTcSWithEvBinds ev_binds_var tcs
        ; ev_binds <- TcM.getTcEvBinds ev_binds_var
        ; checkForCyclicBinds ev_binds
 #endif
+       ; liftIO $ TN.extSolStop extSol
 
        ; return res }
   where
@@ -1116,11 +1127,14 @@ checkForCyclicBinds ev_binds
 nestImplicTcS :: EvBindsVar -> Untouchables -> InertSet -> TcS a -> TcS a
 nestImplicTcS ref inner_untch inerts (TcS thing_inside)
   = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds
+                   , tcs_ext_solver = outer_solver
                    , tcs_count = count } ->
     do { new_inert_var <- TcM.newTcRef inerts
+       ; liftIO (TN.extSolPush outer_solver)
        ; let nest_env = TcSEnv { tcs_ev_binds    = ref
                                , tcs_ty_binds    = ty_binds
                                , tcs_count       = count
+                               , tcs_ext_solver  = outer_solver
                                , tcs_inerts      = new_inert_var
                                , tcs_worklist    = panic "nextImplicTcS: worklist"
                                , tcs_implics     = panic "nextImplicTcS: implics"
@@ -1128,6 +1142,7 @@ nestImplicTcS ref inner_untch inerts (TcS thing_inside)
                                }
        ; res <- TcM.setUntouchables inner_untch $
                 thing_inside nest_env
+       ; liftIO (TN.extSolPop outer_solver)
 
 #ifdef DEBUG
        -- Perform a check that the thing_inside did not cause cycles
@@ -1905,3 +1920,25 @@ deferTcSForAllEq role loc (tvs1,body1) (tvs2,body2)
         }
 \end{code}
 
+Interaction with an External SMT Solver
+---------------------------------------
+
+\begin{code}
+extSolSend  :: Ct -> TcS Bool
+extSolSend ct = withExtSol (\s -> TN.extSolSend s ct)
+
+extSolPush  :: TcS ()
+extSolPush = withExtSol TN.extSolPop
+
+extSolPop   :: TcS ()
+extSolPop = withExtSol TN.extSolPop
+
+extSolCheck :: TcS TN.ExtSolRes
+extSolCheck = withExtSol TN.extSolCheck
+
+withExtSol :: (TN.ExternalSolver -> IO a) -> TcS a
+withExtSol m = TcS (liftIO . m . tcs_ext_solver)
+
+
+
+\end{code}