[commit: ghc] wip/tc-plugins: Improve method for running plugins. (34573cd)
git at git.haskell.org
git at git.haskell.org
Thu Oct 9 17:18:00 UTC 2014
Repository : ssh://git@git.haskell.org/ghc
On branch : wip/tc-plugins
Link : http://ghc.haskell.org/trac/ghc/changeset/34573cd5cdd910e8aef10e30b0fd6a8a21f55267/ghc
>---------------------------------------------------------------
commit 34573cd5cdd910e8aef10e30b0fd6a8a21f55267
Author: Iavor S. Diatchki <diatchki at galois.com>
Date: Thu Oct 9 10:16:49 2014 -0700
Improve method for running plugins.
Instead of trying to manually filter out known constraints,
we leave it to GHC to do its usual thing. To avoid looping,
we need to know if running the solver pipeline modified the inert set:
if the inert set was changed, then we re-run the plugins, otherwise
we are done so we stop.
>---------------------------------------------------------------
34573cd5cdd910e8aef10e30b0fd6a8a21f55267
compiler/typecheck/TcInteract.lhs | 132 ++++++++++++++++----------------------
1 file changed, 57 insertions(+), 75 deletions(-)
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index a881a40..f54e408 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -111,89 +111,70 @@ solveInteract cts
= {-# SCC "solveInteract" #-}
withWorkList cts $
do { dyn_flags <- getDynFlags
- ; solve_loop (maxSubGoalDepth dyn_flags) }
+ ; solve_loop False (maxSubGoalDepth dyn_flags) }
where
- solve_loop max_depth
+ solve_loop inertsModified max_depth
= {-# SCC "solve_loop" #-}
do { sel <- selectNextWorkItem max_depth
; case sel of
- NoWorkRemaining -- Done, successfuly (modulo frozen)
- -> do more_work <- runTcPlugins
- when more_work (solve_loop max_depth)
+
+ NoWorkRemaining
+ | inertsModified ->
+ do gblEnv <- getGblEnv
+ mapM_ runTcPlugin (tcg_tc_plugins gblEnv)
+ solve_loop False max_depth
+
+ -- Done, successfuly (modulo frozen)
+ | otherwise -> 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 } }
+ -> do { changes <- runSolverPipeline thePipeline ct
+ ; let newMod = changes || inertsModified
+ ; newMod `seq` solve_loop newMod max_depth } }
-- | Try to make progress using type-checker plugings.
--- Returns 'True' if we added some extra work to the work queue.
-runTcPlugins :: TcS Bool
-runTcPlugins =
- do gblEnv <- getGblEnv
- case tcg_tc_plugins gblEnv of
- [] -> return False
- plugins ->
- do has_new_works <- mapM runPlugin plugins
- return (or has_new_works)
- where
- runPlugin p =
- do iSet <- getTcSInerts
- let iCans = inert_cans iSet
- iEqs = concat (varEnvElts (inert_eqs iCans))
- iFunEqs = funEqsToList (inert_funeqs iCans)
- allCts = iEqs ++ iFunEqs
- (derived,other) = partition isDerivedCt allCts
- (wanted,given) = partition isWantedCt other
-
- -- We use this to remove some constraints.
- -- 'survived' should be the sub-set of constraints that
- -- remains inert.
- restoreICans survived =
- do let iCans1 = iCans { inert_eqs = emptyVarEnv
- , inert_funeqs = emptyFunEqs }
- iCans2 = foldl addInertCan iCans1 derived
- iCans3 = foldl addInertCan iCans2 survived
- setInertCans iCans3
-
- result <- tcPluginIO $ tcPluginSolve p given wanted
- case result of
-
- TcPluginContradiction bad_cts ok_cts ->
- do restoreICans ok_cts
- mapM_ emitInsoluble bad_cts
- return False
-
- TcPluginNewWork new_cts ->
- case removeKnownCts iCans new_cts of
- [] -> return False
- new_work ->
- do updWorkListTcS (extendWorkListCts new_work)
- return True
-
- TcPluginSolved solved_cts other_cts ->
- case solved_cts of
- [] -> return False -- Fast common case
- _ -> do restoreICans other_cts
- let setEv (ev,ct) = setEvBind (ctev_evar (cc_ev ct)) ev
- mapM_ setEv solved_cts
- return False
-
- removeKnownCts origIcans = filter (not . isKnownCt origIcans)
- isKnownCt origIcans ct =
- case ct of
-
- CFunEqCan { cc_fun = f, cc_tyargs = ts } ->
- case findFunEq (inert_funeqs origIcans) f ts of
- Just _ -> True
- _ -> False
-
- CTyEqCan { cc_tyvar = x, cc_rhs = t } ->
- not $ any (eqType t . cc_rhs) $ findTyEqs (inert_eqs origIcans) x
-
- _ -> panic "TcPlugin returned not a TyEq or FunEq constraint"
-
+-- The plugin is provided with only with CTyEq and CFunEq constraints.
+runTcPlugin :: TcPlugin -> TcS ()
+runTcPlugin p =
+ do iSet <- getTcSInerts
+ let iCans = inert_cans iSet
+ iEqs = concat (varEnvElts (inert_eqs iCans))
+ iFunEqs = funEqsToList (inert_funeqs iCans)
+ allCts = iEqs ++ iFunEqs
+ (derived,other) = partition isDerivedCt allCts
+ (wanted,given) = partition isWantedCt other
+
+ -- We use this to remove some constraints.
+ -- 'survived' should be the sub-set of constraints that
+ -- remains inert.
+ restoreICans survived =
+ do let iCans1 = iCans { inert_eqs = emptyVarEnv
+ , inert_funeqs = emptyFunEqs }
+ iCans2 = foldl addInertCan iCans1 derived
+ iCans3 = foldl addInertCan iCans2 survived
+ setInertCans iCans3
+
+ result <- tcPluginIO $ tcPluginSolve p given wanted
+ case result of
+
+ TcPluginContradiction bad_cts ok_cts ->
+ do restoreICans ok_cts
+ mapM_ emitInsoluble bad_cts
+
+ TcPluginNewWork new_cts ->
+ updWorkListTcS (extendWorkListCts new_cts)
+
+ TcPluginSolved solved_cts other_cts ->
+ case solved_cts of
+ [] -> return () -- Fast common case
+ _ -> do restoreICans other_cts
+ let setEv (ev,ct) = setEvBind (ctev_evar (cc_ev ct)) ev
+ mapM_ setEv solved_cts
type WorkItem = Ct
@@ -225,7 +206,7 @@ selectNextWorkItem max_depth
runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline
-> WorkItem -- The work item
- -> TcS ()
+ -> TcS Bool -- Did we modify the inert set
-- Run this item down the pipeline, leaving behind new work and inerts
runSolverPipeline pipeline workItem
= do { initial_is <- getTcSInerts
@@ -240,13 +221,14 @@ runSolverPipeline pipeline workItem
; case final_res of
Stop -> do { traceTcS "End solver pipeline (discharged) }"
(ptext (sLit "inerts = ") <+> ppr final_is)
- ; return () }
+ ; return False }
ContinueWith ct -> do { traceFireTcS ct (ptext (sLit "Kept as inert"))
; traceTcS "End solver pipeline (not discharged) }" $
vcat [ ptext (sLit "final_item = ") <+> ppr ct
, pprTvBndrs (varSetElems $ tyVarsOfCt ct)
, ptext (sLit "inerts = ") <+> ppr final_is]
- ; insertInertItemTcS ct }
+ ; insertInertItemTcS ct
+ ; return True }
}
where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue -> TcS StopOrContinue
run_pipeline [] res = return res
More information about the ghc-commits
mailing list