+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}
+
+