-normaliseGivenDicts, normaliseWantedDicts
- :: [Inst] -- given equations
- -> [Inst] -- dictionaries
- -> TcM ([Inst],TcDictBinds)
-
-normaliseGivenDicts eqs dicts = normalise_dicts eqs dicts False
-normaliseWantedDicts eqs dicts = normalise_dicts eqs dicts True
-
-normalise_dicts
- :: [Inst] -- given equations
- -> [Inst] -- dictionaries
- -> Bool -- True <=> the dicts are wanted
- -- Fals <=> they are given
- -> TcM ([Inst],TcDictBinds)
-normalise_dicts given_eqs dicts is_wanted
- = do { traceTc $ let name | is_wanted = "normaliseWantedDicts <-"
- | otherwise = "normaliseGivenDicts <-"
- in
- text name <+> ppr dicts <+>
- text "with" <+> ppr given_eqs
- ; (dicts0, binds0) <- normaliseInsts is_wanted dicts
- ; (dicts1, binds1) <- substEqInDictInsts is_wanted given_eqs dicts0
- ; let binds01 = binds0 `unionBags` binds1
- ; if isEmptyBag binds1
- then return (dicts1, binds01)
- else do { (dicts2, binds2) <-
- normalise_dicts given_eqs dicts1 is_wanted
- ; return (dicts2, binds01 `unionBags` binds2) } }
+-- |Configuration of normalised equalities used during solving.
+--
+data EqConfig = EqConfig { eqs :: [RewriteInst] -- all equalities
+ , locals :: [Inst] -- given dicts
+ , wanteds :: [Inst] -- wanted dicts
+ , binds :: TcDictBinds -- bindings
+ , skolems :: TyVarSet -- flattening skolems
+ }
+
+addSkolems :: EqConfig -> TyVarSet -> EqConfig
+addSkolems eqCfg newSkolems
+ = eqCfg {skolems = skolems eqCfg `unionVarSet` newSkolems}
+
+addEq :: EqConfig -> RewriteInst -> EqConfig
+addEq eqCfg eq = eqCfg {eqs = eq : eqs eqCfg}
+
+unionEqConfig :: EqConfig -> EqConfig -> EqConfig
+unionEqConfig eqc1 eqc2 = EqConfig
+ { eqs = eqs eqc1 ++ eqs eqc2
+ , locals = locals eqc1 ++ locals eqc2
+ , wanteds = wanteds eqc1 ++ wanteds eqc2
+ , binds = binds eqc1 `unionBags` binds eqc2
+ , skolems = skolems eqc1 `unionVarSet` skolems eqc2
+ }
+
+emptyEqConfig :: EqConfig
+emptyEqConfig = EqConfig
+ { eqs = []
+ , locals = []
+ , wanteds = []
+ , binds = emptyBag
+ , skolems = emptyVarSet
+ }
+
+instance Outputable EqConfig where
+ ppr (EqConfig {eqs = eqs, locals = locals, wanteds = wanteds, binds = binds})
+ = vcat [ppr eqs, ppr locals, ppr wanteds, ppr binds]
+\end{code}
+
+The set of operations on an equality configuration. We obtain the initialise
+configuration by normalisation ('normaliseEqs'), solve the equalities by
+propagation ('propagateEqs'), and eventually finalise the configuration when
+no further propoagation is possible.
+
+\begin{code}
+-- |Turn a set of equalities into an equality configuration for solving.
+--
+-- Precondition: The Insts are zonked.
+--
+normaliseEqs :: [Inst] -> TcM EqConfig
+normaliseEqs eqs
+ = do { ASSERTM2( allM isValidWantedEqInst eqs, ppr eqs )
+ ; traceTc $ ptext (sLit "Entering normaliseEqs")
+
+ ; (eqss, skolemss) <- mapAndUnzipM normEqInst eqs
+ ; return $ emptyEqConfig { eqs = concat eqss
+ , skolems = unionVarSets skolemss
+ }
+ }
+
+-- |Flatten the type arguments of all dictionaries, returning the result as a
+-- equality configuration. The dictionaries go into the 'wanted' component if
+-- the second argument is 'True'.
+--
+-- Precondition: The Insts are zonked.
+--
+normaliseDicts :: Bool -> [Inst] -> TcM EqConfig
+normaliseDicts isWanted insts
+ = do { traceTc $ hang (ptext (sLit "Entering normaliseDicts") <+>
+ ptext (if isWanted then sLit "[Wanted] for"
+ else sLit "[Local] for"))
+ 4 (ppr insts)
+ ; (insts', eqss, bindss, skolemss) <- mapAndUnzip4M (normDict isWanted)
+ insts
+
+ ; traceTc $ hang (ptext (sLit "normaliseDicts returns"))
+ 4 (ppr insts' $$ ppr eqss)
+ ; return $ emptyEqConfig { eqs = concat eqss
+ , locals = if isWanted then [] else insts'
+ , wanteds = if isWanted then insts' else []
+ , binds = unionManyBags bindss
+ , skolems = unionVarSets skolemss
+ }
+ }
+
+-- |Solves the equalities as far as possible by applying propagation rules.
+--
+propagateEqs :: EqConfig -> TcM EqConfig
+propagateEqs eqCfg@(EqConfig {eqs = todoEqs})
+ = do { traceTc $ hang (ptext (sLit "Entering propagateEqs:"))
+ 4 (ppr eqCfg)
+
+ ; propagate todoEqs (eqCfg {eqs = []})
+ }
+
+-- |Finalise a set of equalities and associated dictionaries after
+-- propagation. The returned Boolean value is `True' iff any flexible
+-- variables, except those introduced by flattening (i.e., those in the
+-- `skolems' component of the argument) where instantiated. The first returned
+-- set of instances are the locals (without equalities) and the second set are
+-- all residual wanteds, including equalities.
+--
+finaliseEqsAndDicts :: EqConfig
+ -> TcM ([Inst], [Inst], TcDictBinds, Bool)
+finaliseEqsAndDicts (EqConfig { eqs = eqs
+ , locals = locals
+ , wanteds = wanteds
+ , binds = binds
+ , skolems = skolems
+ })
+ = do { traceTc $ ptext (sLit "finaliseEqsAndDicts")
+ ; (eqs', subst_binds, locals', wanteds') <- substitute eqs locals wanteds
+ ; (eqs'', improved) <- instantiateAndExtract eqs' (null locals) skolems
+ ; let final_binds = subst_binds `unionBags` binds
+
+ -- Assert that all cotvs of wanted equalities are still unfilled, and
+ -- zonk all final insts, to make any improvement visible
+ ; ASSERTM2( allM isValidWantedEqInst eqs'', ppr eqs'' )
+ ; zonked_locals <- zonkInsts locals'
+ ; zonked_wanteds <- zonkInsts (eqs'' ++ wanteds')
+ ; return (zonked_locals, zonked_wanteds, final_binds, improved)
+ }