diff options
| -rw-r--r-- | compiler/GHC/Tc/Solver/Interact.hs | 19 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Types.hs | 60 | ||||
| -rw-r--r-- | docs/users_guide/extending_ghc.rst | 24 |
3 files changed, 68 insertions, 35 deletions
diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs index 98824022cd..72f4a509c4 100644 --- a/compiler/GHC/Tc/Solver/Interact.hs +++ b/compiler/GHC/Tc/Solver/Interact.hs @@ -287,15 +287,18 @@ runTcPluginSolvers solvers all_cts return $ progress p result progress :: TcPluginProgress -> TcPluginSolveResult -> TcPluginProgress - progress p (TcPluginContradiction bad_cts) = - p { pluginInputCts = discard bad_cts (pluginInputCts p) - , pluginBadCts = bad_cts ++ pluginBadCts p - } - progress p (TcPluginOk solved_cts new_cts) = - p { pluginInputCts = discard (map snd solved_cts) (pluginInputCts p) - , pluginSolvedCts = add solved_cts (pluginSolvedCts p) - , pluginNewCts = new_cts ++ pluginNewCts p + progress p + (TcPluginSolveResult + { tcPluginInsolubleCts = bad_cts + , tcPluginSolvedCts = solved_cts + , tcPluginNewCts = new_cts } + ) = + p { pluginInputCts = discard (bad_cts ++ map snd solved_cts) (pluginInputCts p) + , pluginSolvedCts = add solved_cts (pluginSolvedCts p) + , pluginNewCts = new_cts ++ pluginNewCts p + , pluginBadCts = bad_cts ++ pluginBadCts p + } initialProgress = TcPluginProgress all_cts ([], [], []) [] [] diff --git a/compiler/GHC/Tc/Types.hs b/compiler/GHC/Tc/Types.hs index 2894321546..34d2c2e578 100644 --- a/compiler/GHC/Tc/Types.hs +++ b/compiler/GHC/Tc/Types.hs @@ -3,6 +3,7 @@ {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE PatternSynonyms #-} {- (c) The University of Glasgow 2006-2012 @@ -74,7 +75,9 @@ module GHC.Tc.Types( getPlatform, -- Constraint solver plugins - TcPlugin(..), TcPluginSolveResult(..), TcPluginRewriteResult(..), + TcPlugin(..), + TcPluginSolveResult(TcPluginContradiction, TcPluginOk, ..), + TcPluginRewriteResult(..), TcPluginSolver, TcPluginRewriter, TcPluginM(runTcPluginM), unsafeTcPluginTcM, @@ -1774,23 +1777,48 @@ data TcPlugin = forall s. TcPlugin -- ^ Clean up after the plugin, when exiting the type-checker. } +-- | The plugin found a contradiction. +-- The returned constraints are removed from the inert set, +-- and recorded as insoluble. +-- +-- The returned list of constraints should never be empty. +pattern TcPluginContradiction :: [Ct] -> TcPluginSolveResult +pattern TcPluginContradiction insols + = TcPluginSolveResult + { tcPluginInsolubleCts = insols + , tcPluginSolvedCts = [] + , tcPluginNewCts = [] } + +-- | The plugin has not found any contradictions, +-- +-- The first field is for constraints that were solved. +-- The second field contains new work, that should be processed by +-- the constraint solver. +pattern TcPluginOk :: [(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult +pattern TcPluginOk solved new + = TcPluginSolveResult + { tcPluginInsolubleCts = [] + , tcPluginSolvedCts = solved + , tcPluginNewCts = new } + +-- | Result of running a solver plugin. data TcPluginSolveResult - = TcPluginContradiction [Ct] - -- ^ The plugin found a contradiction. - -- The returned constraints are removed from the inert set, - -- and recorded as insoluble. + = TcPluginSolveResult + { -- | Insoluble constraints found by the plugin. -- - -- The returned list of constraints should never be empty. - - | TcPluginOk - { tcPluginSolvedCts :: [(EvTerm,Ct)] - , tcPluginNewCts :: [Ct] } - -- ^ The first field is for constraints that were solved. - -- These are removed from the inert set, - -- and the evidence for them is recorded. - -- The second field contains new work, that should be processed by - -- the constraint solver. - + -- These constraints will be added to the inert set, + -- and reported as insoluble to the user. + tcPluginInsolubleCts :: [Ct] + -- | Solved constraints, together with their evidence. + -- + -- These are removed from the inert set, and the + -- evidence for them is recorded. + , tcPluginSolvedCts :: [(EvTerm, Ct)] + -- | New constraints that the plugin wishes to emit. + -- + -- These will be added to the work list. + , tcPluginNewCts :: [Ct] + } data TcPluginRewriteResult = diff --git a/docs/users_guide/extending_ghc.rst b/docs/users_guide/extending_ghc.rst index 0020c0213f..7b3f7f0a78 100644 --- a/docs/users_guide/extending_ghc.rst +++ b/docs/users_guide/extending_ghc.rst @@ -555,11 +555,12 @@ is defined thus: type TcPluginRewriter = RewriteEnv -> [Ct] -> [Type] -> TcPluginM TcPluginRewriteResult - data TcPluginResult - = TcPluginContradiction [Ct] - | TcPluginOk - { tcPluginSolvedCts :: [(EvTerm,Ct)] - , tcPluginNewCts :: [Ct] } + data TcPluginSolveResult + = TcPluginSolveResult + { tcPluginInsolubleCts :: [Ct] + , tcPluginSolvedCts :: [(EvTerm, Ct)] + , tcPluginNewCts :: [Ct] + } data TcPluginRewriteResult = TcPluginNoRewrite @@ -634,19 +635,20 @@ The two ways can be distinguished by checking the Wanted constraints: in the first case (and the first case only), the plugin will be passed an empty list of Wanted constraints. -The plugin is then expected to respond in either of the following ways: +The plugin can then respond with: -* return ``TcPluginOk`` with lists of solved and new constraints, or +* solved constraints, which will be removed from the inert set, -* return ``TcPluginContradiction`` with a list of impossible - constraints, so they can be turned into errors. +* new constraints, which will be added to the work list, -In both cases, the plugin must respond with constraints of the same flavour, +* insoluble constraints, which will be reported as errors. + +The plugin must respond with constraints of the same flavour, i.e. in (1) it should return only Givens, and for (2) it should return only Wanteds (or Deriveds); all other constraints will be ignored. If the plugin cannot make any progress, it should return -``TcPluginOk [] []``. Otherwise, if there were any new constraints, the +``TcPluginSolveResult [] [] []``. Otherwise, if there were any new constraints, the main constraint solver will be re-invoked to simplify them, then the plugin will be invoked again. The plugin is responsible for making sure that this process eventually terminates. |