From 4db20c6efe4213f815cabcd3d1c78529aa6490df Mon Sep 17 00:00:00 2001 From: Manuel M T Chakravarty Date: Thu, 6 Sep 2007 11:58:18 +0000 Subject: [PATCH] Cleanup of equality rewriting and no swapInsts for wanteds - Removed code duplication - Added comments - Took out swapInsts for wanteds. With the recent extension to swapInsts it does mess up error messages if applied to wanteds and i should not be necessary. NB: The code actually shrunk. Line increase is due to comments. --- compiler/typecheck/TcTyFuns.lhs | 247 +++++++++++++++++++++------------------ 1 file changed, 132 insertions(+), 115 deletions(-) diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs index 4be39c3..fc19061 100644 --- a/compiler/typecheck/TcTyFuns.lhs +++ b/compiler/typecheck/TcTyFuns.lhs @@ -41,6 +41,7 @@ import SrcLoc ( Located(..) ) import Maybes import Data.List +import Control.Monad (liftM) \end{code} @@ -227,19 +228,20 @@ normalise_dicts given_eqs dicts is_wanted %************************************************************************ %* * -\section{Normalisation of Wanteds} +\section{Normalisation of wanteds constraints} %* * %************************************************************************ \begin{code} normaliseWanteds :: [Inst] -> TcM [Inst] normaliseWanteds insts - = do { traceTc (text "normaliseWanteds" <+> ppr insts) - ; result <- eq_rewrite - [ ("(Occurs)", simple_rewrite_check $ occursCheckInsts) - , ("(ZONK)", simple_rewrite $ zonkInsts) + = do { traceTc (text "normaliseWanteds <-" <+> ppr insts) + ; result <- liftM fst $ rewriteToFixedPoint Nothing + [ ("(Occurs)", noChange $ occursCheckInsts) + , ("(ZONK)", dontRerun $ zonkInsts) , ("(TRIVIAL)", trivialInsts) - , ("(SWAP)", swapInsts) + -- no `swapInsts'; it messes up error messages and should + -- not be necessary -=chak , ("(DECOMP)", decompInsts) , ("(TOP)", topInsts) , ("(SUBST)", substInsts) @@ -250,34 +252,34 @@ normaliseWanteds insts } \end{code} + %************************************************************************ %* * -\section{Normalisation of Givens} +\section{Normalisation of givens constraints} %* * %************************************************************************ \begin{code} - -normaliseGivens :: [Inst] -> TcM ([Inst],TcM ()) -normaliseGivens givens = - do { traceTc (text "normaliseGivens <-" <+> ppr givens) - ; (result,action) <- given_eq_rewrite - ("(SkolemOccurs)", skolemOccurs) - (return ()) - [("(Occurs)", simple_rewrite_check $ occursCheckInsts), - ("(ZONK)", simple_rewrite $ zonkInsts), - ("(TRIVIAL)", trivialInsts), - ("(SWAP)", swapInsts), - ("(DECOMP)", decompInsts), - ("(TOP)", topInsts), - ("(SUBST)", substInsts)] - givens - ; traceTc (text "normaliseGivens ->" <+> ppr result) - ; return (result,action) - } - -skolemOccurs :: [Inst] -> TcM ([Inst],TcM ()) -skolemOccurs [] = return ([], return ()) +normaliseGivens :: [Inst] -> TcM ([Inst], TcM ()) +normaliseGivens givens + = do { traceTc (text "normaliseGivens <-" <+> ppr givens) + ; (result, deSkolem) <- + rewriteToFixedPoint (Just ("(SkolemOccurs)", skolemOccurs)) + [ ("(Occurs)", noChange $ occursCheckInsts) + , ("(ZONK)", dontRerun $ zonkInsts) + , ("(TRIVIAL)", trivialInsts) + , ("(SWAP)", swapInsts) + , ("(DECOMP)", decompInsts) + , ("(TOP)", topInsts) + , ("(SUBST)", substInsts) + ] givens + ; traceTc (text "normaliseGivens ->" <+> ppr result) + ; return (result, deSkolem) + } + +-- An explanation of what this does would be helpful! -=chak +skolemOccurs :: PrecondRule +skolemOccurs [] = return ([], return ()) skolemOccurs (inst@(EqInst {}):insts) = do { (insts',actions) <- skolemOccurs insts -- check whether the current inst co :: ty1 ~ ty2 suffers @@ -317,109 +319,123 @@ skolemOccurs (inst@(EqInst {}):insts) go flag ty = False \end{code} + %************************************************************************ %* * -\section{Solving of Wanteds} +\section{Solving of wanted constraints with respect to a given set} %* * %************************************************************************ \begin{code} -solveWanteds :: - [Inst] -> -- givens - [Inst] -> -- wanteds - TcM [Inst] -- irreducible wanteds -solveWanteds givens wanteds = - do { traceTc (text "solveWanteds <-" <+> ppr wanteds <+> text "with" <+> ppr givens) - ; result <- eq_rewrite - [("(Occurs)", simple_rewrite_check $ occursCheckInsts), - ("(TRIVIAL)", trivialInsts), - ("(DECOMP)", decompInsts), - ("(TOP)", topInsts), - ("(GIVEN)", givenInsts givens), - ("(UNIFY)", unifyInsts)] - wanteds - ; traceTc (text "solveWanteds ->" <+> ppr result) - ; return result +solveWanteds :: [Inst] -- givens + -> [Inst] -- wanteds + -> TcM [Inst] -- irreducible wanteds +solveWanteds givens wanteds + = do { traceTc $ text "solveWanteds <-" <+> ppr wanteds <+> text "with" <+> + ppr givens + ; result <- liftM fst $ rewriteToFixedPoint Nothing + [ ("(Occurs)", noChange $ occursCheckInsts) + , ("(TRIVIAL)", trivialInsts) + , ("(DECOMP)", decompInsts) + , ("(TOP)", topInsts) + , ("(GIVEN)", givenInsts givens) + , ("(UNIFY)", unifyInsts) + ] wanteds + ; traceTc (text "solveWanteds ->" <+> ppr result) + ; return result + } + where + -- Use `substInst' with every given on all the wanteds. + givenInsts :: [Inst] -> [Inst] -> TcM ([Inst],Bool) + givenInsts [] wanteds = return (wanteds,False) + givenInsts (g:gs) wanteds + = do { (wanteds1, changed1) <- givenInsts gs wanteds + ; (wanteds2, changed2) <- substInst g wanteds1 + ; return (wanteds2, changed1 || changed2) } +\end{code} -givenInsts :: [Inst] -> [Inst] -> TcM ([Inst],Bool) -givenInsts [] wanteds - = return (wanteds,False) -givenInsts (g:gs) wanteds - = do { (wanteds1,changed1) <- givenInsts gs wanteds - ; (wanteds2,changed2) <- substInst g wanteds1 - ; return (wanteds2,changed1 || changed2) - } +%************************************************************************ +%* * +\section{Normalisation rules and iterative rule application} +%* * +%************************************************************************ +We have four kinds of normalising rewrite rules: +(1) Normalisation rules that rewrite a set of insts and return a flag indicating + whether any changes occurred during rewriting that necessitate re-running + the current rule set. - -- fixpoint computation - -- of a number of rewrites of equalities -eq_rewrite :: - [(String,[Inst] -> TcM ([Inst],Bool))] -> -- rewrite functions and descriptions - [Inst] -> -- initial equations - TcM [Inst] -- final equations (at fixed point) -eq_rewrite rewrites insts - = go rewrites insts - where - go _ [] -- return quickly when there's nothing to be done - = return [] - go [] insts - = return insts - go ((desc,r):rs) insts - = do { (insts',changed) <- r insts - ; traceTc (text desc <+> ppr insts') - ; if changed - then loop insts' - else go rs insts' - } - loop = eq_rewrite rewrites - - -- fixpoint computation - -- of a number of rewrites of equalities -given_eq_rewrite :: - - (String,[Inst] -> TcM ([Inst],TcM ())) -> - (TcM ()) -> - [(String,[Inst] -> TcM ([Inst],Bool))] -> -- rewrite functions and descriptions - [Inst] -> -- initial equations - TcM ([Inst],TcM ()) -- final equations (at fixed point) -given_eq_rewrite p@(desc,start) acc rewrites insts - = do { (insts',acc') <- start insts - ; go (acc >> acc') rewrites insts' - } - where - go acc _ [] -- return quickly when there's nothing to be done - = return ([],acc) - go acc [] insts - = return (insts,acc) - go acc ((desc,r):rs) insts - = do { (insts',changed) <- r insts - ; traceTc (text desc <+> ppr insts') - ; if changed - then loop acc insts' - else go acc rs insts' - } - loop acc = given_eq_rewrite p acc rewrites - -simple_rewrite :: - ([Inst] -> TcM [Inst]) -> - ([Inst] -> TcM ([Inst],Bool)) -simple_rewrite r insts - = do { insts' <- r insts - ; return (insts',False) - } +(2) Precondition rules that rewrite a set of insts and return a monadic action + that reverts the effect of preconditioning. -simple_rewrite_check :: - ([Inst] -> TcM ()) -> - ([Inst] -> TcM ([Inst],Bool)) -simple_rewrite_check check insts - = check insts >> return (insts,False) - +(3) Idempotent normalisation rules that never require re-running the rule set. +(4) Checking rule that does not alter the set of insts. + +\begin{code} +type RewriteRule = [Inst] -> TcM ([Inst], Bool) -- rewrite, maybe re-run +type PrecondRule = [Inst] -> TcM ([Inst], TcM ()) -- rewrite, revertable +type IdemRewriteRule = [Inst] -> TcM [Inst] -- rewrite, don't re-run +type CheckRule = [Inst] -> TcM () -- check + +type NamedRule = (String, RewriteRule) -- rule with description +type NamedPreRule = (String, PrecondRule) -- precond with desc +\end{code} + +Templates lifting idempotent and checking rules to full rules (which can be put +into a rule set). + +\begin{code} +dontRerun :: IdemRewriteRule -> RewriteRule +dontRerun rule insts = liftM addFalse $ rule insts + where + addFalse x = (x, False) + +noChange :: CheckRule -> RewriteRule +noChange rule insts = rule insts >> return (insts, False) \end{code} +The following function applies a set of rewrite rules until a fixed point is +reached; i.e., none of the `RewriteRule's require re-running the rule set. +Optionally, there may be a pre-conditing rule that is applied before any other +rules are applied and before the rule set is re-run. + +The result is the set of rewritten (i.e., normalised) insts and, in case of a +pre-conditing rule, a monadic action that reverts the effects of +pre-conditioning - specifically, this is removing introduced skolems. + +\begin{code} +rewriteToFixedPoint :: Maybe NamedPreRule -- optional preconditioning rule + -> [NamedRule] -- rule set + -> [Inst] -- insts to rewrite + -> TcM ([Inst], TcM ()) +rewriteToFixedPoint precondRule rules insts + = completeRewrite (return ()) precondRule insts + where + completeRewrite :: TcM () -> Maybe NamedPreRule -> [Inst] + -> TcM ([Inst], TcM ()) + completeRewrite dePrecond (Just (precondName, precond)) insts + = do { (insts', dePrecond') <- precond insts + ; traceTc $ text precondName <+> ppr insts' + ; tryRules dePrecond rules insts' + } + completeRewrite dePrecond Nothing insts + = tryRules dePrecond rules insts + + tryRules dePrecond _ [] = return ([] , dePrecond) + tryRules dePrecond [] insts = return (insts, dePrecond) + tryRules dePrecond ((name, rule):rules) insts + = do { (insts', rerun) <- rule insts + ; traceTc $ text name <+> ppr insts' + ; if rerun then completeRewrite dePrecond precondRule insts' + else tryRules dePrecond rules insts' + } +\end{code} + + %************************************************************************ %* * \section{Different forms of Inst rewritings} @@ -468,6 +484,7 @@ swapInsts insts -- g2 : Fd ~ c -- g1 := sym g2 -- + -- This is not all, is it? Td ~ c is also rewritten to c ~ Td! swapInst i@(EqInst {}) = go ty1 ty2 where -- 1.7.10.4