[commit: ghc] wip/ext-solver: Interaction with external solver (not connected to GHC's solver) (9be9110)

[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/9be9110e9643d8c3d99ed5219015e07ce2c34b72/ghc

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

commit 9be9110e9643d8c3d99ed5219015e07ce2c34b72
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date:   Sat May 10 16:41:56 2014 -0700

    Interaction with external solver (not connected to GHC's solver)


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

9be9110e9643d8c3d99ed5219015e07ce2c34b72
 compiler/typecheck/TcInteract.lhs | 63 +++++++++++++++++++++++++++++++++++++++
 compiler/typecheck/TcSMonad.lhs   |  5 ++--
 compiler/typecheck/TcTypeNats.hs  | 20 +++++--------
 3 files changed, 74 insertions(+), 14 deletions(-)

diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index b8c4c81..808c108 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -132,6 +132,69 @@ solveInteract cts
               NextWorkItem ct     -- More work, loop around!
                 -> do { runSolverPipeline thePipeline ct; solve_loop max_depth } }
 
+inertactExternSolver :: Bool      -- ^ Are we in given stage?
+                     -> TcS Bool  -- ^ Did we generatew new work.
+inertactExternSolver inGivenStage =
+  do iSet <- getTcSInerts
+     let iCans  = inert_cans iSet
+         feqs   = funEqsToList (inert_funeqs iCans)
+
+         {- `survived` should be a sub-set of the inert funeqs.
+         This function rebuilds the inert set, when we need to
+         kick-out some constraint (e.g., because they were solved, or
+         caused a contradiciton. -}
+
+         rebuildInerts survived =
+            do let new_feqs  = foldr addCt emptyFunEqs survived
+                   new_iCans = iCans { inert_funeqs = new_feqs }
+               setTcSInerts iSet { inert_cans = new_iCans }
+
+     res <- extSolImprove inGivenStage feqs
+     case res of
+
+       -- Kick-out constraints that lead to a contradiciton
+       -- and add them as insoluable.
+       ExtSolContradiction bad_feqs ok_feqs ->
+         do rebuildInerts ok_feqs
+            mapM_ emitInsoluble bad_feqs
+            return False
+
+       -- Consistent, and no more work.
+       ExtSolOk []
+
+         -- Assert the givens in the solver, so that they will be used
+         -- when we solve the wanteds (and nested implications).
+         | inGivenStage ->
+            do extSolAssert feqs
+               return False
+
+         -- During the wanted stage, we try to solve the constraints
+         -- once there is no more additional work for re-writing.
+         | otherwise ->
+             do (solved, unsolved) <- extSolSolve feqs
+                case solved of
+                  [] -> return False  -- Shortcut for common case.
+                  _  -> do rebuildInerts unsolved
+                           let setEv (ev,ct)
+                                 | isWantedCt ct =
+                                    setEvBind (ctev_evar (cc_ev ct)) ev
+                                 | otherwise = return ()
+                           mapM_ setEv solved
+                           return False
+
+       -- We added some new work, so we should keep going.
+       ExtSolOk newWork ->
+         do updWorkListTcS (extendWorkListEqs newWork)
+            return True
+
+  where
+  addCt ct mp =
+    case ct of
+      CFunEqCan { cc_fun = tc, cc_tyargs = tys } -> addFunEq mp tc tys ct
+      _ -> mp   -- Should not happend
+
+
+
 type WorkItem = Ct
 type SimplifierStage = WorkItem -> TcS StopOrContinue
 
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 903a906..259ce2d 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -75,6 +75,7 @@ module TcSMonad (
     findFunEq, findTyEqs,
     findDict, findDictsByClass, addDict, addDictsByClass, delDict, partitionDicts,
     findFunEqsByTyCon, findFunEqs, addFunEq, replaceFunEqs, partitionFunEqs,
+    emptyFunEqs, funEqsToList,
 
     instDFunType,                              -- Instantiation
     newFlexiTcSTy, instFlexiTcS, instFlexiTcSHelperTcS,
@@ -1927,8 +1928,8 @@ Interaction with an External SMT Solver
 extSolAssert :: [Ct] -> TcS ()
 extSolAssert ct = withExtSol (`TN.extSolAssert` ct)
 
-extSolImprove :: [Ct] -> TcS TN.ExtSolRes
-extSolImprove ct = withExtSol (`TN.extSolImprove` ct)
+extSolImprove :: Bool -> [Ct] -> TcS TN.ExtSolRes
+extSolImprove withEv ct = withExtSol (\s -> TN.extSolImprove s withEv ct)
 
 extSolSolve :: [Ct] -> TcS ([(EvTerm,Ct)], [Ct])
 extSolSolve ct = withExtSol (`TN.extSolSolve` ct)
diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs
index 1468bba..9d498ba 100644
--- a/compiler/typecheck/TcTypeNats.hs
+++ b/compiler/typecheck/TcTypeNats.hs
@@ -12,7 +12,7 @@ import TcEvidence ( mkTcAxiomRuleCo, EvTerm(..) )
 import TyCon      ( TyCon, SynTyConRhs(..), mkSynTyCon, TyConParent(..)  )
 import Coercion   ( Role(..) )
 import TcRnTypes  ( Xi, Ct(..), ctPred, CtEvidence(..), mkNonCanonical
-                  , isGivenCt, CtLoc, ctLoc )
+                  , CtLoc, ctLoc )
 import CoAxiom    ( CoAxiomRule(..), BuiltInSynFamily(..) )
 import Name       ( Name, BuiltInSyntax(..), nameOccName, nameUnique )
 import OccName    ( occNameString )
@@ -736,7 +736,7 @@ data ExternalSolver = ExternalSolver
     -- ^ Add some assertions.
     -- Changes assertions.
 
-  , extSolImprove :: [Ct] -> IO ExtSolRes
+  , extSolImprove :: Bool -> [Ct] -> IO ExtSolRes
     -- ^ Check for consistency and new work.
     -- Does not change assertions.
 
@@ -952,12 +952,13 @@ solverPrepare proc viRef = go [] []
 {-
 Check a list of constraints for consistency, and computer derived work.
 Does not affect set off assertions in the solver.
-Assumes that either:
-  * all constraints are given, or
-  * all are not given.
 -}
-solverImprove :: SolverProcess -> IORef VarInfo -> [Ct] -> IO ExtSolRes
-solverImprove proc viRef cts =
+solverImprove :: SolverProcess -> IORef VarInfo
+              -> Bool -- ^ Should we generate given constraints?
+                      -- If not, we generate derived ones.
+              -> [Ct]
+              -> IO ExtSolRes
+solverImprove proc viRef withEv cts =
   do push   -- declare variables
      (others,ours) <- solverPrepare proc viRef cts
      case ours of
@@ -992,7 +993,6 @@ solverImprove proc viRef cts =
                      vi   <- readIORef viRef
 
                      let loc    = ctLoc oneOfOurs -- XXX: Better location?
-                         withEv = isGivenCt oneOfOurs
                          toCt (x,e) =
                            do tv <- Map.lookup x (smtDeclaredVars vi)
                               ty <- sExprToType vi e
@@ -1140,10 +1140,6 @@ type VarTypes = UniqFM (TyVar,String,Ty)
 knownCt :: Ct -> Maybe (VarTypes, SExpr)
 knownCt ct =
   case ct of
-    CTyEqCan _ x xi ->
-      do (vs1,e1) <- knownVar x
-         (vs2,e2) <- knownXi xi
-         return (plusUFM vs1 vs2, smtEq e1 e2)
     CFunEqCan _ f args rhs ->
       do (vs1,e1) <- knownTerm f args
          (vs2,e2) <- knownXi rhs