[commit: ghc] wip/ext-solver: Connect with GHC's solver + debugging. (b8693a4)

[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/b8693a426cd66cc7b470a32e7595d85e11d47efe/ghc

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

commit b8693a426cd66cc7b470a32e7595d85e11d47efe
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date:   Sat May 10 19:35:37 2014 -0700

    Connect with GHC's solver + debugging.


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

b8693a426cd66cc7b470a32e7595d85e11d47efe
 compiler/typecheck/TcInteract.lhs | 21 ++++++++++++++-------
 compiler/typecheck/TcTypeNats.hs  | 39 +++++++++++++++++++++++++++++++--------
 2 files changed, 45 insertions(+), 15 deletions(-)

diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 808c108..bad7bf5 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -85,9 +85,9 @@ solveInteractGiven loc old_fsks givens
   | null givens  -- Shortcut for common case
   = return (True, old_fsks)
   | otherwise
-  = do { implics1 <- solveInteract fsk_bag
+  = do { implics1 <- solveInteractWithExtern True fsk_bag
 
-       ; (no_eqs, more_fsks, implics2) <- getGivenInfo (solveInteract given_bag)
+       ; (no_eqs, more_fsks, implics2) <- getGivenInfo (solveInteractWithExtern True given_bag)
        ; MASSERT( isEmptyBag implics1 && isEmptyBag implics2 )
            -- empty implics because we discard Given equalities between
            -- foralls (see Note [Do not decompose given polytype equalities]
@@ -112,11 +112,16 @@ solveInteractGiven loc old_fsks givens
 
 -- The main solver loop implements Note [Basic Simplifier Plan]
 ---------------------------------------------------------------
+
 solveInteract :: Cts -> TcS (Bag Implication)
+solveInteract = solveInteractWithExtern False
+
+solveInteractWithExtern :: Bool -- ^ Are we in the given stage?
+                        -> Cts -> TcS (Bag Implication)
 -- Returns the final InertSet in TcS
 -- Has no effect on work-list or residual-iplications
-solveInteract cts
-  = {-# SCC "solveInteract" #-}
+solveInteractWithExtern inGivenStage cts
+  = {-# SCC "solveInteractWithExtern" #-}
     withWorkList cts $
     do { dyn_flags <- getDynFlags
        ; solve_loop (maxSubGoalDepth dyn_flags) }
@@ -126,15 +131,17 @@ solveInteract cts
         do { sel <- selectNextWorkItem max_depth
            ; case sel of
               NoWorkRemaining     -- Done, successfuly (modulo frozen)
-                -> return ()
+                -> do moreWork <- interactExternSolver inGivenStage
+                      if moreWork then solve_loop max_depth
+                                  else return ()
               MaxDepthExceeded cnt ct -- Failure, depth exceeded
                 -> wrapErrTcS $ solverDepthErrorTcS cnt (ctEvidence ct)
               NextWorkItem ct     -- More work, loop around!
                 -> do { runSolverPipeline thePipeline ct; solve_loop max_depth } }
 
-inertactExternSolver :: Bool      -- ^ Are we in given stage?
+interactExternSolver :: Bool      -- ^ Are we in given stage?
                      -> TcS Bool  -- ^ Did we generatew new work.
-inertactExternSolver inGivenStage =
+interactExternSolver inGivenStage =
   do iSet <- getTcSInerts
      let iCans  = inert_cans iSet
          feqs   = funEqsToList (inert_funeqs iCans)
diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs
index 043cb11..0a1757e 100644
--- a/compiler/typecheck/TcTypeNats.hs
+++ b/compiler/typecheck/TcTypeNats.hs
@@ -54,7 +54,8 @@ import           Control.Monad (forever)
 import           Control.Concurrent ( forkIO )
 import qualified Control.Exception as X
 import           System.Process ( runInteractiveProcess, waitForProcess )
-import           System.IO ( hPutStrLn, hFlush, hGetContents, hGetLine )
+import           System.IO ( hPutStrLn, hFlush, hGetContents, hGetLine,
+                             stderr )
 
 {-------------------------------------------------------------------------------
 Built-in type constructors for functions on type-lelve nats
@@ -772,22 +773,28 @@ newExternalSolver exe opts =
      -- See Note [Variable Scopes] for an explanation of this.
      viRef <- newIORef emptyVarInfo
 
+     let dbg = solverDebug proc
+
      return ExternalSolver
-       { extSolPush   = do solverDebug proc "=== PUSH ==="
+       { extSolPush   = do dbg "=== PUSH ==="
                            solverDebugNext proc
                            solverPush proc viRef
 
        , extSolPop    = do solverDebugPrev proc
-                           solverDebug proc "=== POP ==="
+                           dbg "=== POP ==="
                            solverPop proc viRef
 
        , extSolAssert = \cts ->
-          do (_,ours) <- solverPrepare proc viRef cts
+          do dbg "=== ASSERT ==="
+             (_,ours) <- solverPrepare proc viRef cts
              mapM_ (solverAssume proc . snd) ours
+             mapM_ (solverDebug proc . show . snd) ours
 
-       , extSolImprove = solverImprove proc viRef
+       , extSolImprove = \b cts -> do dbg "=== IMPROVE ==="
+                                      solverImprove proc viRef b cts
 
-       , extSolSolve = solverSimplify proc viRef
+       , extSolSolve = \cts -> do dbg "=== SOLVE ==="
+                                  solverSimplify proc viRef cts
 
        , extSolStop = solverStop proc
        }
@@ -871,6 +878,7 @@ solverCheck proc =
 -- Prove something by concluding that a counter-example is impossible.
 solverProve :: SolverProcess -> IORef VarInfo -> SExpr -> IO Bool
 solverProve proc viRef e =
+  debug $
   do solverPush proc viRef
      solverAssume proc $ SList [ SAtom "not", e ]
      res <- solverCheck proc
@@ -879,6 +887,14 @@ solverProve proc viRef e =
        Unsat -> return True
        _     -> return False
 
+  where
+  debug m = do solverDebug proc ("Prove: " ++ show e)
+               solverDebugNext proc
+               res <- m
+               solverDebug proc (show res)
+               solverDebugPrev proc
+               return res
+
 -- Get values for the variables that are in scope.
 solverGetModel :: SolverProcess -> VarInfo -> IO [(String,SExpr)]
 solverGetModel proc vi =
@@ -1091,7 +1107,11 @@ solverSimplify proc viRef cts =
 
   go unsolved solved ((ct,e) : more) =
     do push   -- Temporarily assume everything else.
+       solverDebug proc "Temporary assuming:"
+       solverDebugNext proc
        mapM_ (assume . snd) more
+       mapM_ (solverDebug proc . show . snd) more
+       solverDebugPrev proc
        proved <- solverProve proc viRef e
        pop
        if proved
@@ -1295,6 +1315,9 @@ declareVar tv vi
 data SExpr = SAtom String | SList [SExpr]
              deriving Eq
 
+instance Show SExpr where
+  showsPrec _ = renderSExpr
+
 data SolverProcess = SolverProcess
   { solverDo   :: SExpr -> IO SExpr
   , solverStop :: IO ()
@@ -1310,8 +1333,8 @@ startSolverProcess exe opts =
   do (hIn, hOut, hErr, h) <- runInteractiveProcess exe opts Nothing Nothing
 
      dbgNest <- newIORef (0 :: Int)
-     let dbgMsg x = return () {- do n <- readIORef dbgNest 
-                       putStrLn (replicate n ' ' ++ x) -}
+     let dbgMsg x = do n <- readIORef dbgNest
+                       hPutStrLn stderr (replicate n ' ' ++ x)
          dbgNext  = modifyIORef' dbgNest (+2)
          dbgPrev  = modifyIORef' dbgNest (subtract 2)