X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2FusageSP%2FUsageSPInf.lhs;h=cce3ffeda863cf2b22a85d50926cbc588f5464cc;hb=b7cc3d012a98cc49abb3441e6637d5148f57f1d1;hp=6de660962dd33d7d9510537360c12a203f0cdfbc;hpb=69e14f75a4b031e489b7774914e5a176409cea78;p=ghc-hetmet.git diff --git a/ghc/compiler/usageSP/UsageSPInf.lhs b/ghc/compiler/usageSP/UsageSPInf.lhs index 6de6609..cce3ffe 100644 --- a/ghc/compiler/usageSP/UsageSPInf.lhs +++ b/ghc/compiler/usageSP/UsageSPInf.lhs @@ -6,7 +6,7 @@ This code is (based on) PhD work of Keith Wansbrough , September 1998 .. May 1999. -Keith Wansbrough 1998-09-04..1999-05-05 +Keith Wansbrough 1998-09-04..1999-07-06 \begin{code} module UsageSPInf ( doUsageSPInf ) where @@ -18,27 +18,36 @@ import UsageSPLint import UConSet import CoreSyn -import Type ( Type(..), TyNote(..), UsageAnn(..), - applyTy, applyTys, - splitFunTy_maybe, splitFunTys, splitTyConApp_maybe, - mkUsgTy, splitUsgTy, isUsgTy, isNotUsgTy, unUsgTy, tyUsg, +import Rules ( RuleBase ) +import TypeRep ( Type(..), TyNote(..) ) -- friend +import Type ( applyTy, applyTys, + splitFunTy_maybe, splitFunTys, splitTyConApp, mkFunTy, mkForAllTy ) -import TyCon ( tyConArgVrcs_maybe ) -import DataCon ( dataConType ) -import Const ( Con(..), Literal(..), literalType ) -import Var ( IdOrTyVar, UVar, varType, mkUVar, modifyIdInfo ) +import TyCon ( tyConArgVrcs_maybe, isFunTyCon ) +import Literal ( Literal(..), literalType ) +import Var ( Var, varType, setVarType, modifyIdInfo ) import IdInfo ( setLBVarInfo, LBVarInfo(..) ) +import Id ( isExportedId ) import VarEnv +import VarSet import UniqSupply ( UniqSupply, UniqSM, initUs, splitUniqSupply ) +import Util ( lengthExceeds ) import Outputable -import CmdLineOpts ( opt_D_dump_usagesp, opt_DoUSPLinting ) -import ErrUtils ( doIfSet, dumpIfSet ) +import Maybes ( expectJust ) +import List ( unzip4 ) +import CmdLineOpts ( DynFlags, DynFlag(..), dopt, opt_UsageSPOn ) +import CoreLint ( showPass, endPass ) +import ErrUtils ( doIfSet_dyn, dumpIfSet_dyn ) import PprCore ( pprCoreBindings ) \end{code} ====================================================================== +-- **! wasn't I going to do something about not requiring annotations +-- to be correct on unpointed types and/or those without haskell pointers +-- inside? + The whole inference ~~~~~~~~~~~~~~~~~~~ @@ -46,13 +55,17 @@ For full details, see _Once Upon a Polymorphic Type_, University of Glasgow Department of Computing Science Technical Report TR-1998-19, December 1998, or the summary in POPL'99. +[** NEW VERSION NOW IMPLEMENTED; different from the papers + above. Hopefully to appear in PLDI'00, and Keith Wansbrough's + University of Cambridge PhD thesis, c. Sep 2000 **] + + Inference is performed as follows: - 1. Remove all manipulable[*] annotations and add fresh @UVar@ - annotations. + 1. Remove all manipulable[*] annotations. - 2. Walk over the resulting term applying the type rules and - collecting the constraints. + 2. Walk over the resulting term adding fresh UVar annotations, + applying the type rules and collecting the constraints. 3. Find the solution to the constraints and apply the substitution to the annotations, leaving a @UVar@-free term. @@ -64,46 +77,61 @@ not allowed to alter. As in the paper, a ``tau-type'' is a type that does *not* have an annotation on top (although it may have some inside), and a ``sigma-type'' is one that does (i.e., is a tau-type with an -annotation added). This conflicts with the totally unrelated usage of -these terms in the remainder of GHC. Caveat lector! KSW 1999-04. +annotation added). Also, a ``rho-type'' is one that may have initial +``\/u.''s. This conflicts with the totally unrelated usage of these +terms in the remainder of GHC. Caveat lector! KSW 1999-07. The inference is done over a set of @CoreBind@s, and inside the IO monad. \begin{code} -doUsageSPInf :: UniqSupply +doUsageSPInf :: DynFlags + -> UniqSupply -> [CoreBind] -> IO [CoreBind] -doUsageSPInf us binds = do - let binds1 = doUnAnnotBinds binds - - (us1,us2) = splitUniqSupply us - (binds2,_) = doAnnotBinds us1 binds1 - - dumpIfSet opt_D_dump_usagesp "UsageSPInf reannot'd" $ - pprCoreBindings binds2 - - doIfSet opt_DoUSPLinting $ - doLintUSPAnnotsBinds binds2 -- lint check 0 - - let ((ucs,_),_) = initUs us2 (uniqSMMToUs (usgInfBinds binds2)) - ms = solveUCS ucs - s = case ms of - Just s -> s - Nothing -> panic "doUsageSPInf: insol. conset!" - binds3 = appUSubstBinds s binds2 - - doIfSet opt_DoUSPLinting $ - do doLintUSPAnnotsBinds binds3 -- lint check 1 - doLintUSPConstBinds binds3 -- lint check 2 (force solution) - doCheckIfWorseUSP binds binds3 -- check for worsening of usages - - dumpIfSet opt_D_dump_usagesp "UsageSPInf" $ - pprCoreBindings binds3 - - return binds3 +doUsageSPInf dflags us binds + | not opt_UsageSPOn + = do { printDump (text "WARNING: ignoring requested -fusagesp pass; requires -fusagesp-on") ; + return binds + } + +{- ENTIRE PASS COMMENTED OUT FOR NOW -- KSW 2000-10-13 + + This monomorphic version of the analysis is outdated. I'm + currently ripping out the old one and inserting the new one. For + now, I'm simply commenting out this entire pass. + + + | otherwise + = do + let binds1 = doUnAnnotBinds binds + + showPass dflags "UsageSPInf" + + dumpIfSet_dyn dflags Opt_D_dump_usagesp "UsageSPInf unannot'd" $ + pprCoreBindings binds1 + + let ((binds2,ucs,_),_) = initUs us (uniqSMMToUs (usgInfBinds emptyVarEnv binds1)) + + dumpIfSet_dyn dflags Opt_D_dump_usagesp "UsageSPInf annot'd" $ + pprCoreBindings binds2 + + let ms = solveUCS ucs + s = case ms of + Just s -> s + Nothing -> panic "doUsageSPInf: insol. conset!" + binds3 = appUSubstBinds s binds2 + + doIfSet_dyn dflags Opt_DoUSPLinting $ + do doLintUSPAnnotsBinds binds3 -- lint check 1 + doLintUSPConstBinds binds3 -- lint check 2 (force solution) + doCheckIfWorseUSP binds binds3 -- check for worsening of usages + + endPass dflags "UsageSPInf" (dopt Opt_D_dump_usagesp dflags) binds3 + + return binds3 \end{code} ====================================================================== @@ -111,257 +139,353 @@ doUsageSPInf us binds = do Inferring an expression ~~~~~~~~~~~~~~~~~~~~~~~ -When we infer types for an expression, we expect it to be already -annotated - normally with usage variables everywhere (or possibly -constants). No context is required since variables already know their -types. +Inference takes an annotated (rho-typed) environment and an expression +unannotated except for variables not appearing in the environment. It +returns an annotated expression, a type, a constraint set, and a +multiset of free variables. It is in the unique supply monad, which +supplies fresh uvars for annotation. + +We conflate usage metavariables and usage variables; the latter are +distinguished by falling within the scope of a usage binder. \begin{code} -usgInfBinds :: [CoreBind] - -> UniqSMM (UConSet, - VarMultiset) - -usgInfBinds [] = return (emptyUConSet, - emptyMS) - -usgInfBinds (b:bs) = do { (ucs2,fv2) <- usgInfBinds bs -- careful of scoping here - ; (ucs1,fv1) <- usgInfBind b fv2 - ; return (ucs1 `unionUCS` ucs2, - fv1) - } - -usgInfBind :: CoreBind -- CoreBind to infer for - -> VarMultiset -- fvs of `body' (later CoreBinds) - -> UniqSMM (UConSet, -- constraints generated by this CoreBind - VarMultiset) -- fvs of this CoreBind and later ones - -usgInfBind (NonRec v1 e1) fv0 = do { (ty1u,ucs1,fv1) <- usgInfCE e1 - ; let ty2u = varType v1 - ucs2 = usgSubTy ty1u ty2u - ucs3 = occChkUConSet v1 fv0 - ; return (unionUCSs [ucs1,ucs2,ucs3], - fv1 `plusMS` (fv0 `delFromMS` v1)) - } - -usgInfBind (Rec ves) fv0 = do { tuf1s <- mapM (usgInfCE . snd) ves - ; let (ty1us,ucs1s,fv1s) = unzip3 tuf1s - vs = map fst ves - ucs2s = zipWith usgSubTy ty1us (map varType vs) - fv3 = foldl plusMS fv0 fv1s - ucs3 = occChksUConSet vs fv3 - ; return (unionUCSs (ucs1s ++ ucs2s ++ [ucs3]), - foldl delFromMS fv3 vs) - } - -usgInfCE :: CoreExpr - -> UniqSMM (Type,UConSet,VarMultiset) - -- ^- in the unique supply monad for new uvars - -- ^- type of the @CoreExpr@ (always a sigma type) - -- ^- set of constraints arising - -- ^- variable appearances for occur() - -usgInfCE e0@(Var v) | isTyVar v = panic "usgInfCE: unexpected TyVar" - | otherwise = return (ASSERT( isUsgTy (varType v) ) - varType v, - emptyUConSet, - unitMS v) - -usgInfCE e0@(Con (Literal lit) args) = ASSERT( null args ) - do { u1 <- newVarUSMM (Left e0) - ; return (mkUsgTy u1 (literalType lit), - emptyUConSet, - emptyMS) - } - -usgInfCE (Con DEFAULT _) = panic "usgInfCE: DEFAULT" - -usgInfCE e0@(Con con args) = -- constant or primop. guaranteed saturated. - do { let (ety1s,e1s) = span isTypeArg args - ty1s = map (\ (Type ty) -> ty) ety1s -- univ. + exist. - ; (ty3us,ty3u) <- case con of - DataCon c -> do { u4 <- newVarUSMM (Left e0) - ; return $ dataConTys c u4 ty1s - -- ty1s is exdicts + args - } - PrimOp p -> return $ primOpUsgTys p ty1s - otherwise -> panic "usgInfCE: unrecognised Con" - ; tuf4s <- mapM usgInfCE e1s - ; let (ty4us,ucs4s,fv4s) = unzip3 tuf4s - ucs5s = zipWith usgSubTy - ty4us ty3us - ; return (ty3u, - -- note ty3 is T ty1s, so it already - -- has annotations inside where they - -- should be (for datacons); for - -- primops we assume types are - -- appropriately annotated already. - unionUCSs (ucs4s ++ ucs5s), - foldl plusMS emptyMS fv4s) - } - where dataConTys c u tys = -- compute argtys of a datacon - let rawCTy = dataConType c - cTy = ASSERT( isUnAnnotated rawCTy ) - -- algebraic data types are defined entirely - -- unannotated; we place Many annotations inside - -- them to get the required tau-types (p20(fn) TR) - annotManyN rawCTy - -- we really don't want annots on top of the - -- funargs, but we can't easily avoid - -- this so we use unUsgTy later - (ty3us,ty3) = ASSERT( all isNotUsgTy tys ) - splitFunTys (applyTys cTy tys) - -- safe 'cos a DataCon always returns a - -- value of type (TyCon tys), not an - -- arrow type - ty3u = if null ty3us then mkUsgTy u ty3 else ty3 - -- if no args, ty3 is tau; else already sigma - reUsg = mkUsgTy u . unUsgTy - in (map reUsg ty3us, - reUsg ty3u) - -usgInfCE (App e1 (Type ty2)) = do { (ty1u,ucs,fv) <- usgInfCE e1 - ; let (u,ty1) = splitUsgTy ty1u - ; ASSERT( isNotUsgTy ty2 ) - return (mkUsgTy u (applyTy ty1 ty2), - ucs, - fv) - } - -usgInfCE (App e1 e2) = do { (ty1u,ucs1,fv1) <- usgInfCE e1 - ; (ty2u,ucs2,fv2) <- usgInfCE e2 - ; let (u1,ty1) = splitUsgTy ty1u - (ty3u,ty4u) = case splitFunTy_maybe ty1 of - Just tys -> tys - Nothing -> panic "usgInfCE: app of non-funty" - ucs5 = usgSubTy ty2u ty3u - ; return (ASSERT( isUsgTy ty4u ) - ty4u, - unionUCSs [ucs1,ucs2,ucs5], - fv1 `plusMS` fv2) - } - -usgInfCE (Lam v e) | isTyVar v = do { (ty1u,ucs,fv) <- usgInfCE e -- safe to ignore free v here - ; let (u,ty1) = splitUsgTy ty1u - ; return (mkUsgTy u (mkForAllTy v ty1), - ucs, - fv) - } - | otherwise = panic "usgInfCE: missing lambda usage annot" +usgInfBinds :: VarEnv Var -- incoming environment (usu. empty) + -> [CoreBind] -- CoreBinds in dependency order + -> UniqSMM ([CoreBind], -- annotated CoreBinds + UConSet, -- constraint set + VarMultiset) -- usage of environment vars + +usgInfBinds ve [] + = return ([], + emptyUConSet, + emptyMS) + +usgInfBinds ve (b0:b0s) +-- (this clause is almost the same as the Let clause) + = do (v1s,ve1,b1,h1,fb1,fa1) <- usgInfBind ve b0 + (b2s,h2,f2) <- usgInfBinds ve1 b0s + let h3 = occChksUConSet v1s (fb1 `plusMS` f2) + return (b1:b2s, + unionUCSs [h1,h2,h3], + fa1 `plusMS` (f2 `delsFromMS` v1s)) + + +usgInfBind :: VarEnv Var + -> CoreBind -- CoreBind to infer for + -> UniqSMM ([Var], -- variables bound + VarEnv Var, -- extended VarEnv + CoreBind, -- annotated CoreBind + UConSet, -- constraints generated by this CoreBind + VarMultiset, -- this bd's use of vars bound in this bd + -- (could be anything for other vars) + VarMultiset) -- this bd's use of other vars + +usgInfBind ve (NonRec v1 e1) + = do (v1',y1u) <- annotVar v1 + (e2,y2u,h2,f2) <- usgInfCE (extendVarEnv ve v1 v1') e1 + let h3 = usgSubTy y2u y1u + h4 = h2 `unionUCS` h3 + (y4r,h4') = usgClos ve y2u h4 + v1'' = setVarType v1 y4r + h5 = if isExportedId v1 then pessimise y4r else emptyUConSet + return ([v1''], + extendVarEnv ve v1 v1'', + NonRec v1'' e2, + h4' `unionUCS` h5, + emptyMS, + f2) + +usgInfBind ve (Rec ves) + = do let (v1s,e1s) = unzip ves + vy1s' <- mapM annotVar v1s + let (v1s',y1us) = unzip vy1s' + ve' = ve `plusVarEnv` (zipVarEnv v1s v1s') + eyhf2s <- mapM (usgInfCE ve') e1s + let (e2s,y2us,h2s,f2s) = unzip4 eyhf2s + h3s = zipWith usgSubTy y2us y1us + h4s = zipWith unionUCS h2s h3s + yh4s = zipWith (usgClos ve) y2us h4s + (y4rs,h4s') = unzip yh4s + v1s'' = zipWith setVarType v1s y4rs + f5 = foldl plusMS emptyMS f2s + h6s = zipWith (\ v y -> if isExportedId v then pessimise y else emptyUConSet) + v1s y4rs + return (v1s'', + ve `plusVarEnv` (zipVarEnv v1s v1s''), + Rec (zip v1s'' e2s), + unionUCSs (h4s' ++ h6s), + f5, + f5 `delsFromMS` v1s') -- we take pains that v1'==v1'' etc + + +usgInfCE :: VarEnv Var -- unannotated -> annotated vars + -> CoreExpr -- expression to annotate / infer + -> UniqSMM (CoreExpr, -- annotated expression (e) + Type, -- (sigma) type of expression (y)(u=sigma)(r=rho) + UConSet, -- set of constraints arising (h) + VarMultiset) -- variable occurrences (f) + +usgInfCE ve e0@(Var v) | isTyVar v + = panic "usgInfCE: unexpected TyVar" + | otherwise + = do v' <- instVar (lookupVar ve v) + return $ ASSERT( isUsgTy (varType v' {-'cpp-}) ) + (Var v', + varType v', + emptyUConSet, + unitMS v') + +usgInfCE ve e0@(Lit lit) + = do u1 <- newVarUSMM (Left e0) + return (e0, + mkUsgTy u1 (literalType lit), + emptyUConSet, + emptyMS) + +{- ------------------------------------ + No Con form now; we rely on usage information in the constructor itself + +usgInfCE ve e0@(Con con args) + = -- constant or primop. guaranteed saturated. + do let (ey1s,e1s) = span isTypeArg args + y1s <- mapM (\ (Type ty) -> annotTyN (Left e0) ty) ey1s -- univ. + exist. + (y2us,y2u) <- case con of + DataCon c -> do u2 <- newVarUSMM (Left e0) + return $ dataConTys c u2 y1s + -- y1s is exdicts + args + PrimOp p -> return $ primOpUsgTys p y1s + otherwise -> panic "usgInfCE: unrecognised Con" + eyhf3s <- mapM (usgInfCE ve) e1s + let (e3s,y3us,h3s,f3s) = unzip4 eyhf3s + h4s = zipWith usgSubTy y3us y2us + return $ ASSERT( isUsgTy y2u ) + (Con con (map Type y1s ++ e3s), + y2u, + unionUCSs (h3s ++ h4s), + foldl plusMS emptyMS f3s) + + whered ataConTys c u y1s + -- compute argtys of a datacon + = let cTy = annotMany (dataConType c) -- extra (sigma) annots later replaced + (y2us,y2u) = splitFunTys (applyTys cTy y1s) + -- safe 'cos a DataCon always returns a value of type (TyCon tys), + -- not an arrow type. + reUsg = mkUsgTy u . unUsgTy + in (map reUsg y2us, reUsg y2u) +-------------------------------------------- -} + + +usgInfCE ve e0@(App ea (Type yb)) + = do (ea1,ya1u,ha1,fa1) <- usgInfCE ve ea + let (u1,ya1) = splitUsgTy ya1u + yb1 <- annotTyN (Left e0) yb + return (App ea1 (Type yb1), + mkUsgTy u1 (applyTy ya1 yb1), + ha1, + fa1) + +usgInfCE ve (App ea eb) + = do (ea1,ya1u,ha1,fa1) <- usgInfCE ve ea + let ( u1,ya1) = splitUsgTy ya1u + (y2u,y3u) = expectJust "usgInfCE:App" $ splitFunTy_maybe ya1 + (eb1,yb1u,hb1,fb1) <- usgInfCE ve eb + let h4 = usgSubTy yb1u y2u + return $ ASSERT( isUsgTy y3u ) + (App ea1 eb1, + y3u, + unionUCSs [ha1,hb1,h4], + fa1 `plusMS` fb1) + +usgInfCE ve e0@(Lam v0 e) | isTyVar v0 + = do (e1,y1u,h1,f1) <- usgInfCE ve e + let (u1,y1) = splitUsgTy y1u + return (Lam v0 e1, + mkUsgTy u1 (mkForAllTy v0 y1), + h1, + f1) + + -- [OLD COMMENT:] -- if used for checking also, may need to extend this case to -- look in lbvarInfo instead. - -usgInfCE (Note (TermUsg u) (Lam v e)) - = ASSERT( not (isTyVar v) ) - do { (ty1u,ucs1,fv) <- usgInfCE e - ; let ty2u = varType v - ucs2 = occChkUConSet v fv - fv' = fv `delFromMS` v - ucs3s = foldMS (\v _ ucss -> (leqUConSet u ((tyUsg . varType) v) - : ucss)) -- in reverse order! - [] - fv' - ; return (mkUsgTy u (mkFunTy ty2u ty1u), - unionUCSs ([ucs1,ucs2] ++ ucs3s), - fv') - } - -usgInfCE (Let bind e0) = do { (ty0u,ucs0,fv0) <- usgInfCE e0 - ; (ucs1,fv1) <- usgInfBind bind fv0 - ; return (ASSERT( isUsgTy ty0u ) - ty0u, - ucs0 `unionUCS` ucs1, - fv1) - } - -usgInfCE (Case e0 v0 [(DEFAULT,[],e1)]) - = -- pure strict let, no selection (could be at polymorphic or function type) - do { (ty0u,ucs0,fv0) <- usgInfCE e0 - ; (ty1u,ucs1,fv1) <- usgInfCE e1 - ; let (u0,ty0) = splitUsgTy ty0u - ucs2 = usgEqTy ty0u (varType v0) -- messy! but OK - ; ty4u <- freshannotTy ty1u - ; let ucs5 = usgSubTy ty1u ty4u - ucs7 = occChkUConSet v0 (fv1 `plusMS` (unitMS v0)) - ; return (ASSERT( isUsgTy ty4u ) - ty4u, - unionUCSs [ucs0,ucs1,ucs2,ucs5,ucs7], - fv0 `plusMS` (fv1 `delFromMS` v0)) - } - -usgInfCE expr@(Case e0 v0 alts) - = -- general case (tycon of scrutinee must be known) - do { let (cs,vss,es) = unzip3 alts - ; (ty0u,ucs0,fv0) <- usgInfCE e0 - ; tuf2s <- mapM usgInfCE es - ; let (u0,ty0) = splitUsgTy ty0u - ucs1 = usgEqTy ty0u (varType v0) -- messy! but OK - (tc,ty0ks) = case splitTyConApp_maybe ty0 of - Just tcks -> tcks - Nothing -> pprPanic "usgInfCE: weird:" $ - vcat [text "scrutinee:" <+> ppr e0, - text "type:" <+> ppr ty0u] - ; let (ty2us,ucs2s,fv2s) = unzip3 tuf2s - ucs3ss = ASSERT2( all isNotUsgTy ty0ks, text "expression" <+> ppr e0 $$ text "has type" <+> ppr ty0u ) - zipWith (\ c vs -> zipWith (\ty v -> - usgSubTy (mkUsgTy u0 ty) - (varType v)) - (caseAltArgs ty0ks c) - vs) - cs - vss - ; ty4u <- freshannotTy (head ty2us) -- assume at least one alt - ; let ucs5s = zipWith usgSubTy ty2us (repeat ty4u) - ucs6s = zipWith occChksUConSet vss fv2s - fv7 = ASSERT( not (null fv2s) && (length fv2s == length vss) ) - foldl1 maxMS (zipWith (foldl delFromMS) fv2s vss) - ucs7 = occChkUConSet v0 (fv7 `plusMS` (unitMS v0)) - ; return (ASSERT( isUsgTy ty4u ) - ty4u, - unionUCSs ([ucs0,ucs1] ++ ucs2s - ++ (concat ucs3ss) - ++ ucs5s - ++ ucs6s - ++ [ucs7]), - fv0 `plusMS` (fv7 `delFromMS` v0)) - } - where caseAltArgs :: [Type] -> Con -> [Type] - -- compute list of tau-types required by a case-alt - caseAltArgs tys (DataCon dc) = let rawCTy = dataConType dc - cTy = ASSERT2( isUnAnnotated rawCTy, (text "caseAltArgs: rawCTy annotated!:" <+> ppr rawCTy <+> text "in" <+> ppr expr) ) - annotManyN rawCTy - in ASSERT( all isNotUsgTy tys ) - map unUsgTy (fst (splitFunTys (applyTys cTy tys))) - caseAltArgs tys (Literal _) = [] - caseAltArgs tys DEFAULT = [] - caseAltArgs tys (PrimOp _) = panic "caseAltArgs: unexpected PrimOp" - -usgInfCE (Note (SCC _) e) = usgInfCE e - -usgInfCE (Note (Coerce ty1 ty0) e) - = do { (ty2u,ucs2,fv2) <- usgInfCE e - ; let (u2,ty2) = splitUsgTy ty2u - ucs3 = usgEqTy ty0 ty2 -- messy but OK - ty0' = (annotManyN . unannotTy) ty0 -- really nasty type - ucs4 = usgEqTy ty0 ty0' - ucs5 = emptyUConSet + | otherwise + = do u1 <- newVarUSMM (Left e0) + (v1,y1u) <- annotVar v0 + (e2,y2u,h2,f2) <- usgInfCE (extendVarEnv ve v0 v1) e + let h3 = occChkUConSet v1 f2 + f2' = f2 `delFromMS` v1 + h4s = foldMS (\ v _ hs -> (leqUConSet u1 ((tyUsg . varType . lookupVar ve) v) + : hs)) -- in reverse order! + [] + f2' + return (Note (TermUsg u1) (Lam v1 e2), -- add annot for lbVarInfo computation + mkUsgTy u1 (mkFunTy y1u y2u), + unionUCSs (h2:h3:h4s), + f2') + +usgInfCE ve (Let b0s e0) + = do (v1s,ve1,b1s,h1,fb1,fa1) <- usgInfBind ve b0s + (e2,y2u,h2,f2) <- usgInfCE ve1 e0 + let h3 = occChksUConSet v1s (fb1 `plusMS` f2) + return $ ASSERT( isUsgTy y2u ) + (Let b1s e2, + y2u, + unionUCSs [h1,h2,h3], + fa1 `plusMS` (f2 `delsFromMS` v1s)) + +usgInfCE ve (Case e0 v0 [(DEFAULT,[],e1)]) +-- pure strict let, no selection (could be at polymorphic or function type) + = do (v1,y1u) <- annotVar v0 + (e2,y2u,h2,f2) <- usgInfCE ve e0 + (e3,y3u,h3,f3) <- usgInfCE (extendVarEnv ve v0 v1) e1 + let h4 = usgEqTy y2u y1u -- **! why not subty? + h5 = occChkUConSet v1 f3 + return $ ASSERT( isUsgTy y3u ) + (Case e2 v1 [(DEFAULT,[],e3)], + y3u, + unionUCSs [h2,h3,h4,h5], + f2 `plusMS` (f3 `delFromMS` v1)) + +usgInfCE ve e0@(Case e1 v1 alts) +-- general case (tycon of scrutinee must be known) +-- (assumes well-typed already; so doesn't check constructor) + = do (v2,y1u) <- annotVar v1 + (e2,y2u,h2,f2) <- usgInfCE ve e1 + let h3 = usgEqTy y2u y1u -- **! why not subty? + (u2,y2) = splitUsgTy y2u + (tc,y2s) = splitTyConApp y2 + (cs,v1ss,es) = unzip3 alts + v2ss = map (map (\ v -> setVarType v (mkUsgTy u2 (annotManyN (varType v))))) + v1ss + ve3 = extendVarEnv ve v1 v2 + eyhf4s <- mapM (\ (v1s,v2s,e) -> usgInfCE (ve3 `plusVarEnv` (zipVarEnv v1s v2s)) e) + (zip3 v1ss v2ss es) + let (e4s,y4us,h4s,f4s) = unzip4 eyhf4s + y5u <- annotTy (Left e0) (unannotTy (head y4us)) + let h5s = zipWith usgSubTy y4us (repeat y5u) + h6s = zipWith occChksUConSet v2ss f4s + f4 = foldl1 maxMS (zipWith delsFromMS f4s v2ss) + h7 = occChkUConSet v2 (f4 `plusMS` (unitMS v2)) + return $ ASSERT( isUsgTy y5u ) + (Case e2 v2 (zip3 cs v2ss e4s), + y5u, + unionUCSs (h2:h3:h7:(h4s ++ h5s ++ h6s)), + f2 `plusMS` (f4 `delFromMS` v2)) + +usgInfCE ve e0@(Note note ea) + = do (e1,y1u,h1,f1) <- usgInfCE ve ea + case note of + Coerce yb ya -> do let (u1,y1) = splitUsgTy y1u + ya3 = annotManyN ya -- really nasty type + h3 = usgEqTy y1 ya3 -- messy but OK + yb3 <- annotTyN (Left e0) yb -- What this says is that a Coerce does the most general possible -- annotation to what's inside it (nasty, nasty), because no information -- can pass through a Coerce. It of course simply ignores the info -- that filters down through into ty1, because it can do nothing with it. -- It does still pass through the topmost usage annotation, though. - ; return (mkUsgTy u2 ty1, - unionUCSs [ucs2,ucs3,ucs4,ucs5], - fv2) - } + return (Note (Coerce yb3 ya3) e1, + mkUsgTy u1 yb3, + unionUCSs [h1,h3], + f1) -usgInfCE (Note InlineCall e) = usgInfCE e + SCC _ -> return (Note note e1, y1u, h1, f1) -usgInfCE (Note (TermUsg u) e) = pprTrace "usgInfCE: ignoring extra TermUsg:" (ppr u) $ - usgInfCE e + InlineCall -> return (Note note e1, y1u, h1, f1) -usgInfCE (Type ty) = panic "usgInfCE: unexpected Type" + InlineMe -> return (Note note e1, y1u, h1, f1) + + TermUsg _ -> pprPanic "usgInfCE:Note TermUsg" $ ppr e0 + +usgInfCE ve e0@(Type _) + = pprPanic "usgInfCE:Type" $ ppr e0 \end{code} + +\begin{code} +lookupVar :: VarEnv Var -> Var -> Var +-- if variable in VarEnv then return annotated version, +-- otherwise it's imported and already annotated so leave alone. +--lookupVar ve v = error "lookupVar unimplemented" +lookupVar ve v = case lookupVarEnv ve v of + Just v' -> v' + Nothing -> ASSERT( not (mustHaveLocalBinding v) ) + ASSERT( isUsgTy (varType v) ) + v + +instVar :: Var -> UniqSMM Var +-- instantiate variable with rho-type, giving it a fresh sigma-type +instVar v = do let (uvs,ty) = splitUsForAllTys (varType v) + case uvs of + [] -> return v + _ -> do uvs' <- mapM (\_ -> newVarUSMM (Left (Var v))) uvs + let ty' = substUsTy (zipVarEnv uvs uvs') ty + return (setVarType v ty') + +annotVar :: Var -> UniqSMM (Var,Type) +-- freshly annotates a variable and returns it along with its new type +annotVar v = do y1u <- annotTy (Left (Var v)) (varType v) + return (setVarType v y1u, y1u) +\end{code} + + +The closure operation, which does the generalisation at let bindings. + +\begin{code} +usgClos :: VarEnv Var -- environment to close with respect to + -> Type -- type to close (sigma) + -> UConSet -- constraint set to reduce + -> (Type, -- closed type (rho) + UConSet) -- residual constraint set + +usgClos zz_ve ty ucs = (ty,ucs) -- dummy definition; no generalisation at all + + -- hmm! what if it sets some uvars to 1 or omega? + -- (should it do substitution here, or return a substitution, + -- or should it leave all that work to the end and just use + -- an "=" constraint here for now?) +\end{code} + +The pessimise operation, which generates constraints to pessimise an +id (applied to exported ids, to ensure that they have fully general +types, since we don't know how they will be used in other modules). + +\begin{code} +pessimise :: Type -> UConSet + +pessimise ty + = pess True emptyVarEnv ty + + where + pess :: Bool -> UVarSet -> Type -> UConSet + pess co ve (NoteTy (UsgForAll uv) ty) + = pess co (ve `extendVarSet` uv) ty + pess co ve ty0@(NoteTy (UsgNote u) ty) + = pessN co ve ty `unionUCS` + (case (co,u) of + (False,_ ) -> emptyUConSet + (True ,UsMany ) -> emptyUConSet + (True ,UsOnce ) -> pprPanic "pessimise: can't force:" (ppr ty0) + (True ,UsVar uv) -> if uv `elemVarSet` ve + then emptyUConSet -- if bound by \/u, no need to pessimise + else eqManyUConSet u) + pess _ _ ty0 + = pprPanic "pessimise: missing annot:" (ppr ty0) + + pessN :: Bool -> UVarSet -> Type -> UConSet + pessN co ve (NoteTy (UsgForAll uv) ty) = pessN co (ve `extendVarSet` uv) ty + pessN co ve ty0@(NoteTy (UsgNote _) _ ) = pprPanic "pessimise: unexpected annot:" (ppr ty0) + pessN co ve (NoteTy (SynNote sty) ty) = pessN co ve sty `unionUCS` pessN co ve ty + pessN co ve (NoteTy (FTVNote _) ty) = pessN co ve ty + pessN co ve (TyVarTy _) = emptyUConSet + pessN co ve (AppTy _ _) = emptyUConSet + pessN co ve (TyConApp tc tys) = ASSERT( not((isFunTyCon tc)&&( tys `lengthExceeds` 1)) ) + emptyUConSet + pessN co ve (FunTy ty1 ty2) = pess (not co) ve ty1 `unionUCS` pess co ve ty2 + pessN co ve (ForAllTy _ ty) = pessN co ve ty +\end{code} + + + ====================================================================== Helper functions @@ -370,15 +494,16 @@ Helper functions If a variable appears more than once in an fv set, force its usage to be Many. \begin{code} -occChkUConSet :: IdOrTyVar +occChkUConSet :: Var -> VarMultiset -> UConSet occChkUConSet v fv = if occInMS v fv > 1 - then eqManyUConSet ((tyUsg . varType) v) + then ASSERT2( isUsgTy (varType v), ppr v ) + eqManyUConSet ((tyUsg . varType) v) else emptyUConSet -occChksUConSet :: [IdOrTyVar] +occChksUConSet :: [Var] -> VarMultiset -> UConSet @@ -509,11 +634,12 @@ A @VarMultiset@ is what it says: a set of variables with counts attached to them. We build one out of a @VarEnv@. \begin{code} -type VarMultiset = VarEnv (IdOrTyVar,Int) -- I guess 536 870 911 occurrences is enough +type VarMultiset = VarEnv (Var,Int) -- I guess 536 870 911 occurrences is enough emptyMS = emptyVarEnv unitMS v = unitVarEnv v (v,1) delFromMS = delVarEnv +delsFromMS = delVarEnvList plusMS :: VarMultiset -> VarMultiset -> VarMultiset plusMS = plusVarEnv_C (\ (v,n) (_,m) -> (v,n+m)) maxMS :: VarMultiset -> VarMultiset -> VarMultiset @@ -538,6 +664,9 @@ isUnAnnotated (AppTy ty1 ty2) = isUnAnnotated ty1 && isUnAnnotated ty2 isUnAnnotated (TyConApp tc tys) = all isUnAnnotated tys isUnAnnotated (FunTy ty1 ty2) = isUnAnnotated ty1 && isUnAnnotated ty2 isUnAnnotated (ForAllTy tyv ty) = isUnAnnotated ty + + +END OF ENTIRELY-COMMENTED-OUT PASS -- KSW 2000-10-13 -} \end{code} ======================================================================