Cleaning up the extractUnsolved story.
authorDimitrios Vytiniotis <dimitris@microsoft.com>
Thu, 19 Jul 2012 12:32:15 +0000 (14:32 +0200)
committerDimitrios Vytiniotis <dimitris@microsoft.com>
Thu, 19 Jul 2012 12:32:15 +0000 (14:32 +0200)
compiler/typecheck/TcSMonad.lhs
compiler/typecheck/TcSimplify.lhs

index f0c69c5..4073e4e 100644 (file)
@@ -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
 
 
 
index 637aa0a..914d463 100644 (file)
@@ -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