2 % (c) The GRASP/AQUA Project, Glasgow University, 1998
4 \section[UsageSPUtils]{UsageSP Utilities}
6 This code is (based on) PhD work of Keith Wansbrough <kw217@cl.cam.ac.uk>,
7 September 1998 .. May 1999.
9 Keith Wansbrough 1998-09-04..1999-07-07
12 module UsageSPUtils ( {- SEE BELOW: -- KSW 2000-10-13
13 AnnotM(AnnotM), initAnnotM,
15 MungeFlags(isSigma,isLocal,isExp,hasUsg,mfLoc),
17 doAnnotBinds, doUnAnnotBinds,
18 annotTy, annotTyN, annotMany, annotManyN, unannotTy, freshannotTy,
21 UniqSMM, usToUniqSMM, uniqSMMToUs,
26 #include "HsVersions.h"
28 {- ENTIRE FILE COMMENTED OUT FOR NOW -- KSW 2000-10-13
30 import Var ( Var, varType, setVarType, mkUVar )
31 import Id ( isExportedId )
32 import Name ( isLocallyDefined )
33 import TypeRep ( Type(..), TyNote(..) ) -- friend
34 import Type ( splitFunTys )
35 import Subst ( substTy, mkTyVarSubst )
36 import TyCon ( isAlgTyCon, isPrimTyCon, isSynTyCon, isFunTyCon )
38 import PrimOp ( PrimOp, primOpUsg )
39 import UniqSupply ( UniqSupply, UniqSM, initUs, getUniqueUs, thenUs, returnUs )
43 This monomorphic version of the analysis is outdated. I'm
44 currently ripping out the old one and inserting the new one. For
45 now, I'm simply commenting out this entire file.
50 ======================================================================
52 Walking over (and altering) types
53 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
55 We often need to fiddle with (i.e., add or remove) usage annotations
56 on a type. We define here a general framework to do this. Usage
57 annotations come from any monad with a function @getAnnM@ which yields
58 a new annotation. We use two mutually recursive functions, one for
59 sigma types and one for tau types.
62 genAnnotTy :: Monad m =>
63 (m UsageAnn) -- get new annotation
67 genAnnotTy getAnnM ty = do { u <- getAnnM
68 ; ty' <- genAnnotTyN getAnnM ty
69 ; return (NoteTy (UsgNote u) ty')
72 genAnnotTyN :: Monad m =>
78 (NoteTy (UsgNote _) ty) = panic "genAnnotTyN: unexpected UsgNote"
80 (NoteTy (SynNote sty) ty) = do { sty' <- genAnnotTyN getAnnM sty
81 -- is this right? shouldn't there be some
82 -- correlation between sty' and ty'?
83 -- But sty is a TyConApp; does this make it safer?
84 ; ty' <- genAnnotTyN getAnnM ty
85 ; return (NoteTy (SynNote sty') ty')
88 (NoteTy fvn@(FTVNote _) ty) = do { ty' <- genAnnotTyN getAnnM ty
89 ; return (NoteTy fvn ty')
93 ty0@(TyVarTy _) = do { return ty0 }
96 (AppTy ty1 ty2) = do { ty1' <- genAnnotTyN getAnnM ty1
97 ; ty2' <- genAnnotTyN getAnnM ty2
98 ; return (AppTy ty1' ty2')
102 (TyConApp tc tys) = ASSERT( isFunTyCon tc || isAlgTyCon tc || isPrimTyCon tc || isSynTyCon tc )
103 do { let gAT = if isFunTyCon tc
104 then genAnnotTy -- sigma for partial apps of (->)
105 else genAnnotTyN -- tau otherwise
106 ; tys' <- mapM (gAT getAnnM) tys
107 ; return (TyConApp tc tys')
111 (FunTy ty1 ty2) = do { ty1' <- genAnnotTy getAnnM ty1
112 ; ty2' <- genAnnotTy getAnnM ty2
113 ; return (FunTy ty1' ty2')
117 (ForAllTy v ty) = do { ty' <- genAnnotTyN getAnnM ty
118 ; return (ForAllTy v ty')
124 Walking over (and retyping) terms
125 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
127 We also often need to play with the types in a term. This is slightly
128 tricky because of redundancy: we want to change binder types, and keep
129 the bound types matching these; then there's a special case also with
130 non-locally-defined bound variables. We generalise over all this
133 The name `annot' is a bit of a misnomer, as the code is parameterised
134 over exactly what it does to the types (and certain terms). Notice
135 also that it is possible for this parameter to use
136 monadically-threaded state: here called `flexi'. For genuine
137 annotation, this state will be a UniqSupply.
139 We may add annotations to the outside of a (term, not type) lambda; a
140 function passed to @genAnnotBinds@ does this, taking the lambda and
141 returning the annotated lambda. It is inside the @AnnotM@ monad.
142 This term-munging function is applied when we see either a term lambda
143 or a usage annotation; *IMPORTANT:* it is applied *before* we recurse
144 down into the term, and it is expected to work only at the top level.
145 Recursion will subsequently be done by genAnnotBinds. It may
146 optionally remove a Note TermUsg, or optionally add one if it is not
147 already present, but it may perform NO OTHER MODIFICATIONS to the
148 structure of the term.
150 We do different things to types of variables bound locally and of
151 variables bound in other modules, in certain cases: the former get
152 uvars and the latter keep their existing annotations when we annotate,
153 for example. To control this, @MungeFlags@ describes what kind of a
154 type this is that we're about to munge.
157 data MungeFlags = MungeFlags { isSigma :: Bool, -- want annotated on top (sigma type)
158 isLocal :: Bool, -- is locally-defined type
159 hasUsg :: Bool, -- has fixed usage info, don't touch
160 isExp :: Bool, -- is exported (and must be pessimised)
161 mfLoc :: SDoc -- location info
164 tauTyMF loc = MungeFlags { isSigma = False, isLocal = True,
165 hasUsg = False, isExp = False, mfLoc = loc }
166 sigVarTyMF v = MungeFlags { isSigma = True, isLocal = hasLocalDef v,
167 hasUsg = hasUsgInfo v, isExp = isExportedId v,
168 mfLoc = ptext SLIT("type of binder") <+> ppr v }
171 The helper functions @tauTyMF@ and @sigVarTyMF@ create @MungeFlags@
172 for us. @sigVarTyMF@ checks the variable to see how to set the flags.
174 @hasLocalDef@ tells us if the given variable has an actual local
175 definition that we can play with. This is not quite the same as
176 @isLocallyDefined@, since @hasNoBindingId@ things (usually) don't have
177 a local definition - the simplifier will inline whatever their
178 unfolding is anyway. We treat these as if they were externally
179 defined, since we don't have access to their definition (at least not
180 easily). This doesn't hurt much, since after the simplifier has run
181 the unfolding will have been inlined and we can access the unfolding
184 @hasUsgInfo@, on the other hand, says if the variable already has
185 usage info in its type that must at all costs be preserved. This is
186 assumed true (exactly) of all imported ids.
189 hasLocalDef :: Var -> Bool
190 hasLocalDef var = mustHaveLocalBinding var
192 hasUsgInfo :: Var -> Bool
193 hasUsgInfo var = (not . isLocallyDefined) var
196 Here's the walk itself.
199 genAnnotBinds :: (MungeFlags -> Type -> AnnotM flexi Type)
200 -> (CoreExpr -> AnnotM flexi CoreExpr) -- see caveats above
202 -> AnnotM flexi [CoreBind]
204 genAnnotBinds _ _ [] = return []
206 genAnnotBinds f g (b:bs) = do { (b',vs,vs') <- genAnnotBind f g b
207 ; bs' <- withAnnVars vs vs' $
212 genAnnotBind :: (MungeFlags -> Type -> AnnotM flexi Type) -- type-altering function
213 -> (CoreExpr -> AnnotM flexi CoreExpr) -- term-altering function
214 -> CoreBind -- original CoreBind
216 (CoreBind, -- annotated CoreBind
217 [Var], -- old variables, to be mapped to...
218 [Var]) -- ... new variables
220 genAnnotBind f g (NonRec v1 e1) = do { v1' <- genAnnotVar f v1
221 ; e1' <- genAnnotCE f g e1
222 ; return (NonRec v1' e1', [v1], [v1'])
225 genAnnotBind f g (Rec ves) = do { let (vs,es) = unzip ves
226 ; vs' <- mapM (genAnnotVar f) vs
227 ; es' <- withAnnVars vs vs' $
228 mapM (genAnnotCE f g) es
229 ; return (Rec (zip vs' es'), vs, vs')
232 genAnnotCE :: (MungeFlags -> Type -> AnnotM flexi Type) -- type-altering function
233 -> (CoreExpr -> AnnotM flexi CoreExpr) -- term-altering function
234 -> CoreExpr -- original expression
235 -> AnnotM flexi CoreExpr -- yields new expression
237 genAnnotCE mungeType mungeTerm = go
238 where go e0@(Var v) | isTyVar v = return e0 -- arises, e.g., as tyargs of constructor
239 -- (no it doesn't: (Type (TyVar tyvar))
240 | otherwise = do { mv' <- lookupAnnVar v
242 Just var -> return var
243 Nothing -> fixedVar v
247 go (Lit l) = -- we know it's saturated
250 go (App e arg) = do { e' <- go e
252 ; return (App e' arg')
255 go e0@(Lam v0 _) = do { e1 <- (if isTyVar v0 then return else mungeTerm) e0
257 = case e1 of -- munge may have added note
258 Note tu@(TermUsg _) (Lam v e2)
260 Lam v e2 -> (v,e2,id)
261 ; v' <- genAnnotVar mungeType v
262 ; e' <- withAnnVar v v' $ go e2
263 ; return (wrap (Lam v' e'))
266 go (Let bind e) = do { (bind',vs,vs') <- genAnnotBind mungeType mungeTerm bind
267 ; e' <- withAnnVars vs vs' $ go e
268 ; return (Let bind' e')
271 go (Case e v alts) = do { e' <- go e
272 ; v' <- genAnnotVar mungeType v
273 ; alts' <- withAnnVar v v' $ mapM genAnnotAlt alts
274 ; return (Case e' v' alts')
277 go (Note scc@(SCC _) e) = do { e' <- go e
278 ; return (Note scc e')
280 go e0@(Note (Coerce ty1 ty0)
281 e) = do { ty1' <- mungeType
282 (tauTyMF (ptext SLIT("coercer of")
285 (tauTyMF (ptext SLIT("coercee of")
287 -- (Better to specify ty0'
288 -- identical to the type of e, including
289 -- annotations, right at the beginning, but
290 -- not possible at this point.)
292 ; return (Note (Coerce ty1' ty0') e')
294 go (Note InlineCall e) = do { e' <- go e
295 ; return (Note InlineCall e')
297 go (Note InlineMe e) = do { e' <- go e
298 ; return (Note InlineMe e')
300 go e0@(Note (TermUsg _) _) = do { e1 <- mungeTerm e0
301 ; case e1 of -- munge may have removed note
302 Note tu@(TermUsg _) e2 -> do { e3 <- go e2
303 ; return (Note tu e3)
308 go e0@(Type ty) = -- should only occur at toplevel of Arg,
310 do { ty' <- mungeType
311 (tauTyMF (ptext SLIT("tyarg")
316 fixedVar v = ASSERT2( not (hasLocalDef v), text "genAnnotCE: locally defined var" <+> ppr v <+> text "not in varenv" )
317 genAnnotVar mungeType v
319 genAnnotAlt (c,vs,e) = do { vs' <- mapM (genAnnotVar mungeType) vs
320 ; e' <- withAnnVars vs vs' $ go e
321 ; return (c, vs', e')
325 genAnnotVar :: (MungeFlags -> Type -> AnnotM flexi Type)
329 genAnnotVar mungeType v | isTyVar v = return v
330 | otherwise = do { vty' <- mungeType (sigVarTyMF v) (varType v)
331 ; return (setVarType v vty')
335 pprTrace "genAnnotVar" (ppr (tyUsg vty') <+> ppr v) $
341 ======================================================================
343 Some specific things to do to types inside terms
344 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
346 @annotTyM@ annotates a type with fresh uvars everywhere the inference
347 is allowed to go, and leaves alone annotations where it may not go.
349 We assume there are no annotations already.
352 annotTyM :: MungeFlags -> Type -> AnnotM UniqSupply Type
354 annotTyM mf ty = uniqSMtoAnnotM . uniqSMMToUs $
355 case (hasUsg mf, isLocal mf, isSigma mf) of
356 (True ,_ ,_ ) -> ASSERT( isUsgTy ty )
358 (False,True ,True ) -> if isExp mf then
359 annotTyP (tag 'p') ty
362 (False,True ,False) -> annotTyN (tag 't') ty
363 (False,False,True ) -> return $ annotMany ty -- assume worst
364 (False,False,False) -> return $ annotManyN ty
365 where tag c = Right $ "annotTyM:" ++ [c] ++ ": " ++ showSDoc (ppr ty)
367 -- specific functions for annotating tau and sigma types
370 annotTy tag = genAnnotTy (newVarUSMM tag)
371 annotTyN tag = genAnnotTyN (newVarUSMM tag)
373 -- ...with uvars and pessimal Manys (for exported ids)
374 annotTyP tag ty = do { ty' <- annotTy tag ty ; return (pessimise True ty') }
377 annotMany, annotManyN :: Type -> Type
382 annotMany ty = unId (genAnnotTy (return UsMany) ty)
383 annotManyN ty = unId (genAnnotTyN (return UsMany) ty)
386 -- monad required for the above
387 newtype Id a = Id a ; unId (Id a) = a
388 instance Monad Id where { a >>= f = f (unId a) ; return a = Id a }
390 -- lambda-annotating function for use along with the above
391 annotLam e0@(Lam v e) = do { uv <- uniqSMtoAnnotM $ newVarUs (Left e0)
392 ; return (Note (TermUsg uv) (Lam v e))
394 annotLam (Note (TermUsg _) _) = panic "annotLam: unexpected term usage annot"
397 The above requires a `pessimising' translation. This is applied to
398 types of exported ids, and ensures that they have a fully general
399 type (since we don't know how they will be used in other modules).
402 pessimise :: Bool -> Type -> Type
405 pessimise co ty0@(NoteTy usg@(UsgNote u ) ty)
407 then case u of UsMany -> pty
408 UsVar _ -> pty -- force to UsMany
409 UsOnce -> pprPanic "pessimise:" (ppr ty0)
411 where pty = pessimiseN co ty
413 pessimise co ty0 = pessimiseN co ty0 -- assume UsMany
415 pessimise co ty0@(NoteTy usg@(UsgNote u ) ty)
417 then case u of UsMany -> NoteTy usg pty
418 UsVar _ -> NoteTy (UsgNote UsMany) pty
419 UsOnce -> pprPanic "pessimise:" (ppr ty0)
421 where pty = pessimiseN co ty
423 pessimise co ty0 = pprPanic "pessimise: missing usage note:" $
427 pessimiseN co ty0@(NoteTy usg@(UsgNote _ ) ty) = pprPanic "pessimiseN: unexpected usage note:" $
429 pessimiseN co (NoteTy (SynNote sty) ty) = NoteTy (SynNote (pessimiseN co sty))
431 pessimiseN co (NoteTy note@(FTVNote _ ) ty) = NoteTy note (pessimiseN co ty)
432 pessimiseN co ty0@(TyVarTy _) = ty0
433 pessimiseN co ty0@(AppTy _ _) = ty0
434 pessimiseN co ty0@(TyConApp tc tys) = ASSERT( not ((isFunTyCon tc) && (length tys > 1)) )
436 pessimiseN co (FunTy ty1 ty2) = FunTy (pessimise (not co) ty1)
438 pessimiseN co (ForAllTy tyv ty) = ForAllTy tyv (pessimiseN co ty)
442 @unAnnotTyM@ strips annotations (that the inference is allowed to
443 touch) from a term, and `fixes' those it isn't permitted to touch (by
444 putting @Many@ annotations where they are missing, but leaving
445 existing annotations in the type).
447 @unTermUsg@ removes from a term any term usage annotations it finds.
450 unAnnotTyM :: MungeFlags -> Type -> AnnotM a Type
452 unAnnotTyM mf ty = if hasUsg mf then
454 return (fixAnnotTy ty)
455 else return (unannotTy ty)
458 unTermUsg :: CoreExpr -> AnnotM a CoreExpr
459 -- strip all term annotations
460 unTermUsg e@(Lam _ _) = return e
461 unTermUsg (Note (TermUsg _) e) = return e
462 unTermUsg _ = panic "unTermUsg"
464 unannotTy :: Type -> Type
465 -- strip all annotations
466 unannotTy (NoteTy (UsgForAll uv) ty) = unannotTy ty
467 unannotTy (NoteTy (UsgNote _ ) ty) = unannotTy ty
468 unannotTy (NoteTy (SynNote sty) ty) = NoteTy (SynNote (unannotTy sty)) (unannotTy ty)
469 unannotTy (NoteTy note@(FTVNote _ ) ty) = NoteTy note (unannotTy ty)
470 unannotTy ty@(PredTy _) = ty -- PredTys need to be preserved
471 unannotTy ty@(TyVarTy _) = ty
472 unannotTy (AppTy ty1 ty2) = AppTy (unannotTy ty1) (unannotTy ty2)
473 unannotTy (TyConApp tc tys) = TyConApp tc (map unannotTy tys)
474 unannotTy (FunTy ty1 ty2) = FunTy (unannotTy ty1) (unannotTy ty2)
475 unannotTy (ForAllTy tyv ty) = ForAllTy tyv (unannotTy ty)
478 fixAnnotTy :: Type -> Type
479 -- put Manys where they are missing
483 fixAnnotTy (NoteTy note@(UsgForAll uv) ty) = NoteTy note (fixAnnotTy ty)
484 fixAnnotTy (NoteTy note@(UsgNote _ ) ty) = NoteTy note (fixAnnotTyN ty)
485 fixAnnotTy ty0 = NoteTy (UsgNote UsMany) (fixAnnotTyN ty0)
487 fixAnnotTyN ty0@(NoteTy note@(UsgNote _ ) ty) = pprPanic "fixAnnotTyN: unexpected usage note:" $
489 fixAnnotTyN (NoteTy (SynNote sty) ty) = NoteTy (SynNote (fixAnnotTyN sty))
491 fixAnnotTyN (NoteTy note@(FTVNote _ ) ty) = NoteTy note (fixAnnotTyN ty)
492 fixAnnotTyN ty0@(TyVarTy _) = ty0
493 fixAnnotTyN (AppTy ty1 ty2) = AppTy (fixAnnotTyN ty1) (fixAnnotTyN ty2)
494 fixAnnotTyN (TyConApp tc tys) = ASSERT( isFunTyCon tc || isAlgTyCon tc || isPrimTyCon tc || isSynTyCon tc )
495 TyConApp tc (map (if isFunTyCon tc then
499 fixAnnotTyN (FunTy ty1 ty2) = FunTy (fixAnnotTy ty1) (fixAnnotTy ty2)
500 fixAnnotTyN (ForAllTy tyv ty) = ForAllTy tyv (fixAnnotTyN ty)
504 The composition (reannotating a type with fresh uvars but the same
505 structure) is useful elsewhere:
508 freshannotTy :: Type -> UniqSMM Type
509 freshannotTy = annotTy (Right "freshannotTy") . unannotTy
513 Wrappers apply these functions to sets of bindings.
516 doAnnotBinds :: UniqSupply
518 -> ([CoreBind],UniqSupply)
520 doAnnotBinds us binds = initAnnotM us (genAnnotBinds annotTyM annotLam binds)
523 doUnAnnotBinds :: [CoreBind]
526 doUnAnnotBinds binds = fst $ initAnnotM () $
527 genAnnotBinds unAnnotTyM unTermUsg binds
530 ======================================================================
535 The @UniqSM@ type is not an instance of @Monad@, and cannot be made so
536 since it is merely a synonym rather than a newtype. Here we define
537 @UniqSMM@, which *is* an instance of @Monad@.
540 newtype UniqSMM a = UsToUniqSMM (UniqSM a)
541 uniqSMMToUs (UsToUniqSMM us) = us
542 usToUniqSMM = UsToUniqSMM
544 instance Monad UniqSMM where
545 m >>= f = UsToUniqSMM $ uniqSMMToUs m `thenUs` \ a ->
547 return = UsToUniqSMM . returnUs
551 For annotation, the monad @AnnotM@, we need to carry around our
552 variable mapping, along with some general state.
555 newtype AnnotM flexi a = AnnotM ( flexi -- UniqSupply etc
556 -> VarEnv Var -- unannotated to annotated variables
557 -> (a,flexi,VarEnv Var))
558 unAnnotM (AnnotM f) = f
560 instance Monad (AnnotM flexi) where
561 a >>= f = AnnotM (\ us ve -> let (r,us',ve') = unAnnotM a us ve
562 in unAnnotM (f r) us' ve')
563 return a = AnnotM (\ us ve -> (a,us,ve))
565 initAnnotM :: fl -> AnnotM fl a -> (a,fl)
566 initAnnotM fl m = case (unAnnotM m) fl emptyVarEnv of { (r,fl',_) -> (r,fl') }
568 withAnnVar :: Var -> Var -> AnnotM fl a -> AnnotM fl a
569 withAnnVar v v' m = AnnotM (\ us ve -> let ve' = extendVarEnv ve v v'
570 (r,us',_) = (unAnnotM m) us ve'
573 withAnnVars :: [Var] -> [Var] -> AnnotM fl a -> AnnotM fl a
574 withAnnVars vs vs' m = AnnotM (\ us ve -> let ve' = plusVarEnv ve (zipVarEnv vs vs')
575 (r,us',_) = (unAnnotM m) us ve'
578 lookupAnnVar :: Var -> AnnotM fl (Maybe Var)
579 lookupAnnVar var = AnnotM (\ us ve -> (lookupVarEnv ve var,
584 A useful helper allows us to turn a computation in the unique supply
585 monad into one in the annotation monad parameterised by a unique
589 uniqSMtoAnnotM :: UniqSM a -> AnnotM UniqSupply a
591 uniqSMtoAnnotM m = AnnotM (\ us ve -> let (r,us') = initUs us m
595 @newVarUs@ and @newVarUSMM@ generate a new usage variable. They take
596 an argument which is used for debugging only, describing what the
597 variable is to annotate.
600 newVarUs :: (Either CoreExpr String) -> UniqSM UsageAnn
601 -- the first arg is for debugging use only
602 newVarUs e = getUniqueUs `thenUs` \ u ->
607 Left (Lit _) -> "literal"
608 Left (Lam v e) -> "lambda: " ++ showSDoc (ppr v)
611 in pprTrace "newVarUs:" (ppr uv <+> text src) $
615 newVarUSMM :: (Either CoreExpr String) -> UniqSMM UsageAnn
616 newVarUSMM = usToUniqSMM . newVarUs
619 ======================================================================
621 PrimOps and usage information.
623 Analagously to @DataCon.dataConArgTys@, we determine the argtys and
624 result ty of a primop, *after* substition (which may reveal more args,
625 notably for @CCall@s).
628 primOpUsgTys :: PrimOp -- this primop
629 -> [Type] -- instantiated at these (tau) types
630 -> ([Type],Type) -- requires args of these (sigma) types,
631 -- and returns this (sigma) type
633 primOpUsgTys p tys = let (tyvs,ty0us,rtyu) = primOpUsg p
634 s = mkTyVarSubst tyvs tys
635 (ty1us,rty1u) = splitFunTys (substTy s rtyu)
636 -- substitution may reveal more args
637 in ((map (substTy s) ty0us) ++ ty1us,
641 END OF ENTIRELY-COMMENTED-OUT FILE -- KSW 2000-10-13 -}
644 ======================================================================