Commit a04583ac authored by dimitris's avatar dimitris
Browse files

Cleaning up the extractUnsolved story.

parent 79871261
......@@ -66,8 +66,8 @@ module TcSMonad (
InertSet(..), InertCans(..),
getInertEqs, getCtCoercion,
emptyInert, getTcSInerts, lookupInInerts,
extractUnsolved,
extractUnsolvedTcS, modifyInertTcS,
getInertUnsolved, getInertInsols, splitInertsForImplications,
modifyInertTcS,
updInertSetTcS, partitionCCanMap, partitionEqMap,
getRelevantCts, extractRelevantInerts,
CCanMap(..), CtTypeMap, CtFamHeadMap, CtPredMap,
......@@ -362,6 +362,13 @@ extractUnsolvedCMap cmap =
in (wntd `unionBags` derd,
cmap { cts_wanted = emptyUFM, cts_derived = emptyUFM })
extractWantedCMap :: CCanMap a -> (Cts, CCanMap a)
-- Gets the wanted /only/ constraints and returns a residual
-- CCanMap with only givens or derived
extractWantedCMap cmap =
let wntd = foldUFM unionBags emptyCts (cts_wanted cmap)
in (wntd, cmap { cts_wanted = emptyUFM })
-- Maps from PredTypes to Constraints
type CtTypeMap = TypeMap Ct
......@@ -655,64 +662,92 @@ modifyInertTcS upd
; return a }
extractUnsolvedTcS :: TcS (Cts,Cts)
-- Extracts frozen errors and remaining unsolved and sets the
-- inert set to be the remaining!
extractUnsolvedTcS = modifyInertTcS extractUnsolved
extractUnsolved :: InertSet -> ((Cts,Cts), InertSet)
-- Postcondition
-- -------------
-- When:
-- ((frozen,cts),is_solved) <- extractUnsolved inert
-- Then:
-- -----------------------------------------------------------------------------
-- cts | The unsolved (Derived or Wanted only) residual
-- | canonical constraints, that is, no CNonCanonicals.
-- -----------|-----------------------------------------------------------------
-- frozen | The CNonCanonicals of the original inert (frozen errors),
-- | of all flavors
-- -----------|-----------------------------------------------------------------
-- is_solved | Whatever remains from the inert after removing the previous two.
-- -----------------------------------------------------------------------------
extractUnsolved (IS { inert_cans = IC { inert_eqs = eqs
, inert_eq_tvs = eq_tvs
, inert_irreds = irreds
, inert_funeqs = funeqs
, inert_dicts = dicts
}
, inert_frozen = frozen
, inert_solved = solved
, inert_flat_cache = flat_cache
, inert_solved_funeqs = funeq_cache
})
= let is_solved = IS { inert_cans = IC { inert_eqs = solved_eqs
, inert_eq_tvs = eq_tvs
, inert_dicts = solved_dicts
, inert_irreds = solved_irreds
, inert_funeqs = solved_funeqs }
, inert_frozen = emptyCts -- All out
-- At some point, I used to flush all the solved, in
-- fear of evidence loops. But I think we are safe,
-- flushing is why T3064 had become slower
, inert_solved = solved -- PredMap emptyTM
, inert_flat_cache = flat_cache -- FamHeadMap emptyTM
, inert_solved_funeqs = funeq_cache -- FamHeadMap emptyTM
}
in ((frozen, unsolved), is_solved)
where solved_eqs = filterVarEnv_Directly (\_ ct -> isGivenCt ct) eqs
unsolved_eqs = foldVarEnv (\ct cts -> cts `extendCts` ct) emptyCts $
eqs `minusVarEnv` solved_eqs
(unsolved_irreds, solved_irreds) = Bag.partitionBag (not.isGivenCt) irreds
(unsolved_dicts, solved_dicts) = extractUnsolvedCMap dicts
(unsolved_funeqs, solved_funeqs) = partCtFamHeadMap (not . isGivenCt) funeqs
unsolved = unsolved_eqs `unionBags` unsolved_irreds `unionBags`
unsolved_dicts `unionBags` unsolved_funeqs
splitInertsForImplications :: InertSet -> ([Ct],InertSet)
-- Converts the Wanted of the original inert to Given and removes
-- all Wanted and Derived from the inerts.
-- DV: Is the removal of Derived essential?
splitInertsForImplications is
= let (cts,is') = extractWanted is
in (givens_from_unsolved cts,is')
where givens_from_unsolved = foldrBag get_unsolved []
get_unsolved cc rest_givens
| pushable_wanted cc
= let fl = ctEvidence cc
gfl = Given { ctev_gloc = setCtLocOrigin (ctev_wloc fl) UnkSkol
, ctev_evtm = EvId (ctev_evar fl)
, ctev_pred = ctev_pred fl }
this_given = cc { cc_ev = gfl }
in this_given : rest_givens
| otherwise = rest_givens
pushable_wanted :: Ct -> Bool
pushable_wanted cc
= isEqPred (ctPred cc) -- see Note [Preparing inert set for implications]
-- Returns Wanted constraints and a Derived/Given InertSet
extractWanted (IS { inert_cans = IC { inert_eqs = eqs
, inert_eq_tvs = eq_tvs
, inert_irreds = irreds
, inert_funeqs = funeqs
, inert_dicts = dicts
}
, inert_frozen = _frozen
, inert_solved = solved
, inert_flat_cache = flat_cache
, inert_solved_funeqs = funeq_cache
})
= let is_solved = IS { inert_cans = IC { inert_eqs = solved_eqs
, inert_eq_tvs = eq_tvs
, inert_dicts = solved_dicts
, inert_irreds = solved_irreds
, inert_funeqs = solved_funeqs }
, inert_frozen = emptyCts -- All out
-- At some point, I used to flush all the solved, in
-- fear of evidence loops. But I think we are safe,
-- flushing is why T3064 had become slower
, inert_solved = solved -- PredMap emptyTM
, inert_flat_cache = flat_cache -- FamHeadMap emptyTM
, inert_solved_funeqs = funeq_cache -- FamHeadMap emptyTM
}
in (wanted, is_solved)
where gd_eqs = filterVarEnv_Directly (\_ ct -> not (isWantedCt ct)) eqs
wanted_eqs = foldVarEnv (\ct cts -> cts `extendCts` ct) emptyCts $
eqs `minusVarEnv` gd_eqs
(wanted_irreds, gd_irreds) = Bag.partitionBag isWantedCt irreds
(wanted_dicts, gd_dicts) = extractWantedCMap dicts
(wanted_funeqs, gd_funeqs) = partCtFamHeadMap isWantedCt funeqs
-- Is this all necessary?
solved_eqs = filterVarEnv_Directly (\_ ct -> isGivenCt ct) gd_eqs
solved_irreds = Bag.filterBag isGivenCt gd_irreds
(_,solved_dicts) = extractUnsolvedCMap gd_dicts
(_,solved_funeqs) = partCtFamHeadMap (not . isGivenCt) gd_funeqs
wanted = wanted_eqs `unionBags` wanted_irreds `unionBags`
wanted_dicts `unionBags` wanted_funeqs
getInertInsols :: InertSet -> Cts
-- Insolubles only
getInertInsols is = inert_frozen is
getInertUnsolved :: InertSet -> Cts
-- Unsolved Wanted or Derived only
getInertUnsolved (IS { inert_cans = icans })
= let unsolved_eqs = foldVarEnv add_if_not_given emptyCts (inert_eqs icans)
add_if_not_given ct cts
| isGivenCt ct = cts
| otherwise = cts `extendCts` ct
(unsolved_irreds,_) = Bag.partitionBag (not . isGivenCt) (inert_irreds icans)
(unsolved_dicts,_) = extractUnsolvedCMap (inert_dicts icans)
(unsolved_funeqs,_) = partCtFamHeadMap (not . isGivenCt) (inert_funeqs icans)
in unsolved_eqs `unionBags` unsolved_irreds `unionBags`
unsolved_dicts `unionBags` unsolved_funeqs
......
......@@ -782,7 +782,9 @@ solve_wanteds wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol = insols
-- out of one or more of the implications.
; unsolved_implics <- simpl_loop 1 (implics `unionBags` impls_from_flats)
; (insoluble_flats,unsolved_flats) <- extractUnsolvedTcS
; is <- getTcSInerts
; let insoluble_flats = getInertInsols is
unsolved_flats = getInertUnsolved is
; bb <- getTcEvBindsMap
; tb <- getTcSTyBindsMap
......@@ -815,24 +817,24 @@ simpl_loop n implics
| otherwise
= do { (implic_eqs, unsolved_implics) <- solveNestedImplications implics
; inerts <- getTcSInerts
; let ((_,unsolved_flats),_) = extractUnsolved inerts
; let improve_eqs = implic_eqs
-- NB: improve_eqs used to contain defaulting equations HERE but
-- defaulting now happens only at simplifyTop and not deep inside
-- simpl_loop! See Note [Top-level Defaulting Plan]
; unsolved_flats <- getTcSInerts >>= (return . getInertUnsolved)
; traceTcS "solveWanteds: simpl_loop end" $
vcat [ text "improve_eqs =" <+> ppr improve_eqs
, text "unsolved_flats =" <+> ppr unsolved_flats
, text "unsolved_implics =" <+> ppr unsolved_implics ]
; if isEmptyBag improve_eqs then return unsolved_implics
else do { impls_from_eqs <- solveInteractCts $ bagToList improve_eqs
; simpl_loop (n+1) (unsolved_implics `unionBags`
impls_from_eqs)} }
solveNestedImplications :: Bag Implication
-> TcS (Cts, Bag Implication)
-- Precondition: the TcS inerts may contain unsolved flats which have
......@@ -842,19 +844,17 @@ solveNestedImplications implics
= return (emptyBag, emptyBag)
| otherwise
= do { inerts <- getTcSInerts
; traceTcS "solveNestedImplications starting, inerts are:" $ ppr inerts
; let ((_insoluble_flats, unsolved_flats),thinner_inerts) = extractUnsolved inerts
; traceTcS "solveNestedImplications starting, inerts are:" $ ppr inerts
; let (pushed_givens, thinner_inerts) = splitInertsForImplications inerts
; traceTcS "solveNestedImplications starting, more info:" $
vcat [ text "inerts = " <+> ppr inerts
, text "insoluble_flats = " <+> ppr _insoluble_flats
, text "unsolved_flats = " <+> ppr unsolved_flats
vcat [ text "original inerts = " <+> ppr inerts
, text "pushed_givens = " <+> ppr pushed_givens
, text "thinner_inerts = " <+> ppr thinner_inerts ]
; (implic_eqs, unsolved_implics)
<- doWithInert thinner_inerts $
do { let pushed_givens = givens_from_wanteds unsolved_flats
tcs_untouchables
do { let tcs_untouchables
= foldr (unionVarSet . tyVarsOfCt) emptyVarSet pushed_givens
-- Typically pushed_givens is very small, consists
-- only of unsolved equalities, so no inefficiency
......@@ -885,23 +885,6 @@ solveNestedImplications implics
; return (implic_eqs, unsolved_implics) }
where givens_from_wanteds = foldrBag get_wanted []
get_wanted cc rest_givens
| pushable_wanted cc
= let fl = ctEvidence cc
gfl = Given { ctev_gloc = setCtLocOrigin (ctev_wloc fl) UnkSkol
, ctev_evtm = EvId (ctev_evar fl)
, ctev_pred = ctev_pred fl }
this_given = cc { cc_ev = gfl }
in this_given : rest_givens
| otherwise = rest_givens
pushable_wanted :: Ct -> Bool
pushable_wanted cc
| isWantedCt cc
= isEqPred (ctPred cc) -- see Note [Preparing inert set for implications]
| otherwise = False
solveImplication :: TcTyVarSet -- Untouchable TcS unification variables
-> Implication -- Wanted
-> TcS (Cts, -- All wanted or derived floated equalities: var = type
......@@ -1522,7 +1505,7 @@ defaultTyVar the_tv
; implics_from_defaulting <- solveInteractCts cts
; MASSERT (isEmptyBag implics_from_defaulting)
; (_,unsolved) <- extractUnsolvedTcS
; unsolved <- getTcSInerts >>= (return . getInertUnsolved)
; if isEmptyBag (keepWanted unsolved) then return (listToBag cts)
else return emptyBag }
| otherwise = return emptyBag -- The common case
......@@ -1638,7 +1621,7 @@ disambigGroup (default_ty:default_tys) group
-- I am not certain if any implications can be generated
-- but I am letting this fail aggressively if this ever happens.
; (_,unsolved) <- extractUnsolvedTcS
; unsolved <- getTcSInerts >>= (return . getInertUnsolved)
; traceTcS "disambigGroup (solving) }" $
text "disambigGroup unsolved =" <+> ppr (keepWanted unsolved)
; if isEmptyBag (keepWanted unsolved) then -- Don't care about Derived's
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment