opt_D_dump_cpranal,
opt_D_dump_worker_wrapper,
opt_D_dump_tc,
+ opt_D_dump_usagesp,
opt_D_show_passes,
opt_D_show_rn_trace,
opt_D_show_rn_imports,
opt_D_verbose_stg2stg,
opt_DictsStrict,
opt_DoCoreLinting,
+ opt_DoUSPLinting,
opt_DoStgLinting,
opt_DoSemiTagging,
opt_DoEtaReduction,
opt_EnsureSplittableC,
opt_FoldrBuildOn,
opt_UnboxStrictFields,
+ opt_UsageSPOn,
opt_GlasgowExts,
opt_GranMacros,
opt_HiMap,
| CoreDoSpecialising
| CoreDoFoldrBuildWorkerWrapper
| CoreDoFoldrBuildWWAnal
+ | CoreDoUSPInf
| CoreDoCPResult
\end{code}
opt_D_dump_worker_wrapper = lookUp SLIT("-ddump-workwrap")
opt_D_dump_cpranal = lookUp SLIT("-ddump-cpranalyse")
opt_D_dump_tc = lookUp SLIT("-ddump-tc")
+opt_D_dump_usagesp = lookUp SLIT("-ddump-usagesp")
opt_D_show_passes = lookUp SLIT("-dshow-passes")
opt_D_show_rn_trace = lookUp SLIT("-dshow-rn-trace")
opt_D_show_rn_imports = lookUp SLIT("-dshow-rn-imports")
opt_DoCoreLinting = lookUp SLIT("-dcore-lint")
opt_DoStgLinting = lookUp SLIT("-dstg-lint")
opt_DoEtaReduction = lookUp SLIT("-fdo-eta-reduction")
+opt_UsageSPOn = lookUp SLIT("-fusagesp-on")
opt_DoSemiTagging = lookUp SLIT("-fsemi-tagging")
opt_DoTickyProfiling = lookUp SLIT("-fticky-ticky")
+opt_DoUSPLinting = lookUp SLIT("-dusagesp-lint")
opt_EmitCExternDecls = lookUp SLIT("-femit-extern-decls")
opt_EnsureSplittableC = lookUp SLIT("-fglobalise-toplev-names")
opt_FoldrBuildOn = lookUp SLIT("-ffoldr-build-on")
"-fworker-wrapper" -> CORE_TD(CoreDoWorkerWrapper)
"-fspecialise" -> CORE_TD(CoreDoSpecialising)
"-ffoldr-build-worker-wrapper" -> CORE_TD(CoreDoFoldrBuildWorkerWrapper)
- "-ffoldr-build-ww-anal" -> CORE_TD(CoreDoFoldrBuildWWAnal)
+ "-ffoldr-build-ww-anal" -> CORE_TD(CoreDoFoldrBuildWWAnal)
+ "-fusagesp" -> CORE_TD(CoreDoUSPInf)
"-fcpr-analyse" -> CORE_TD(CoreDoCPResult)
"-fstg-static-args" -> STG_TD(StgDoStaticArgs)
--- /dev/null
+%
+% (c) The GRASP/AQUA Project, Glasgow University, 1998
+%
+\section[UConSet]{UsageSP constraint solver}
+
+This code is (based on) PhD work of Keith Wansbrough <kw217@cl.cam.ac.uk>,
+February 1998 .. April 1999.
+
+Keith Wansbrough 1998-02-16..1999-04-29
+
+\begin{code}
+module UConSet ( UConSet,
+ emptyUConSet,
+ eqManyUConSet,
+ eqUConSet,
+ leqUConSet,
+ unionUCS,
+ unionUCSs,
+ solveUCS,
+ ) where
+
+#include "HsVersions.h"
+
+import VarEnv
+import Type ( UsageAnn(..) )
+import Var ( UVar )
+import Monad ( foldM )
+import Bag ( Bag, unitBag, emptyBag, unionBags, foldlBag, bagToList )
+import Outputable
+import PprType
+\end{code}
+
+======================================================================
+
+The data type:
+~~~~~~~~~~~~~~
+
+First, individual constraints on particular variables. This is
+private to the implementation.
+
+\begin{code}
+data UCon = UCEq UVar UVar -- j = k (equivalence)
+ | UCBound [UVar] UVar [UVar] -- {..} <= j <= {..}
+ | UCUsOnce UVar -- j = 1
+ | UCUsMany UVar -- j = omega
+\end{code}
+
+Next, the public (but abstract) data type for a usage constraint set:
+either a bag of mappings from @UVar@ to @UCon@, or an error message
+for an inconsistent constraint set.
+
+\begin{code}
+data UConSet = UConSet (Bag (VarEnv UCon))
+ | UConFail SDoc
+\end{code}
+
+The idea is that the @VarEnv@s (which will eventually be merged into a
+single @VarEnv@) are union-find data structures: a variable is either
+equal to another variable, or it is bounded or has a value. The
+equalities form a forest pointing to a root node for each equality
+class, on which is found the bound or value for that class.
+
+The @Bag@ enables two-phase operation: we merely collect constraints
+in the first phase, an donly union them at solution time. This gives
+a much more efficient algorithm, as we make only a single pass over
+the constraints.
+
+Note that the absence of a variable from the @VarEnv@ is exactly
+equivalent to it being mapped to @UCBound [] _ []@.
+
+
+The interface:
+~~~~~~~~~~~~~~
+
+@emptyUConSet@ gives an empty constraint set.
+@eqManyUConSet@ constrains an annotation to be Many.
+@eqUConSet@ constrains two annotations to be equal.
+@leqUConSet@ constrains one annotation to be less than or equal to
+another (with Once < Many).
+
+\begin{code}
+mkUCS = UConSet . unitBag -- helper function not exported
+
+emptyUConSet :: UConSet
+emptyUConSet = UConSet emptyBag
+
+eqManyUConSet :: UsageAnn -> UConSet
+
+eqManyUConSet UsOnce = UConFail (text "Once /= Many")
+eqManyUConSet UsMany = emptyUConSet
+eqManyUConSet (UsVar uv) = mkUCS $ unitVarEnv uv (UCUsMany uv)
+
+eqUConSet :: UsageAnn -> UsageAnn -> UConSet
+
+eqUConSet UsOnce UsOnce = emptyUConSet
+eqUConSet UsOnce (UsVar uv) = mkUCS $ unitVarEnv uv (UCUsOnce uv)
+eqUConSet UsMany UsMany = emptyUConSet
+eqUConSet UsMany (UsVar uv) = mkUCS $ unitVarEnv uv (UCUsMany uv)
+eqUConSet (UsVar uv) UsOnce = mkUCS $ unitVarEnv uv (UCUsOnce uv)
+eqUConSet (UsVar uv) UsMany = mkUCS $ unitVarEnv uv (UCUsMany uv)
+eqUConSet (UsVar uv) (UsVar uv') = if uv==uv'
+ then emptyUConSet
+ else mkUCS $ unitVarEnv uv (UCEq uv uv')
+eqUConSet UsMany UsOnce = UConFail (text "Many /= Once")
+eqUConSet UsOnce UsMany = UConFail (text "Once /= Many")
+
+leqUConSet :: UsageAnn -> UsageAnn -> UConSet
+
+leqUConSet UsOnce _ = emptyUConSet
+leqUConSet _ UsMany = emptyUConSet
+leqUConSet UsMany UsOnce = UConFail (text "Many /<= Once")
+leqUConSet UsMany (UsVar uv) = mkUCS $ unitVarEnv uv (UCUsMany uv)
+leqUConSet (UsVar uv) UsOnce = mkUCS $ unitVarEnv uv (UCUsOnce uv)
+leqUConSet (UsVar uv) (UsVar uv') = mkUCS $ mkVarEnv [(uv, UCBound [] uv [uv']),
+ (uv',UCBound [uv] uv' [] )]
+\end{code}
+
+@unionUCS@ forms the union of two @UConSet@s.
+@unionUCSs@ forms the `big union' of a list of @UConSet@s.
+
+\begin{code}
+unionUCS :: UConSet -> UConSet -> UConSet
+
+unionUCS (UConSet b1) (UConSet b2) = UConSet (b1 `unionBags` b2)
+unionUCS ucs@(UConFail _) _ = ucs -- favour first error
+unionUCS (UConSet _) ucs@(UConFail _) = ucs
+
+unionUCSs :: [UConSet] -> UConSet
+
+unionUCSs ucss = foldl unionUCS emptyUConSet ucss
+\end{code}
+
+
+@solveUCS@ finds the minimal solution to the constraint set, returning
+it as @Just@ a substitution function taking usage variables to usage
+annotations (@UsOnce@ or @UsMany@). If this is not possible (for an
+inconsistent constraint set), @solveUCS@ returns @Nothing@.
+
+The minimal solution is found by simply reading off the known
+variables, and for unknown ones substituting @UsOnce@.
+
+\begin{code}
+solveUCS :: UConSet -> Maybe (UVar -> UsageAnn)
+
+solveUCS (UConSet css)
+ = case foldlBag (\cs1 jcs2 -> foldVarEnv addUCS cs1 jcs2)
+ (Left emptyVarEnv)
+ css of
+ Left cs -> let cs' = mapVarEnv conToSub cs
+ sub uv = case lookupVarEnv cs' uv of
+ Just u -> u
+ Nothing -> UsOnce
+ conToSub (UCEq _ uv') = case lookupVarEnv cs uv' of
+ Nothing -> UsOnce
+ Just con' -> conToSub con'
+ conToSub (UCUsOnce _ ) = UsOnce
+ conToSub (UCUsMany _ ) = UsMany
+ conToSub (UCBound _ _ _ ) = UsOnce
+ in Just sub
+ Right err -> solveUCS (UConFail err)
+
+solveUCS (UConFail why) =
+#ifdef DEBUG
+ pprTrace "UConFail:" why $
+#endif
+ Nothing
+\end{code}
+
+======================================================================
+
+The internals:
+~~~~~~~~~~~~~~
+
+In the internals, we use the @VarEnv UCon@ explicitly, or occasionally
+@Either (VarEnv UCon) SDoc@. In other words, the @Bag@ is no longer
+used.
+
+@findUCon@ finds the root of an equivalence class.
+@changeUConUVar@ copies a constraint, but changes the variable constrained.
+
+\begin{code}
+findUCon :: VarEnv UCon -> UVar -> UVar
+
+findUCon cs uv
+ = case lookupVarEnv cs uv of
+ Just (UCEq _ uv') -> findUCon cs uv'
+ Just _ -> uv
+ Nothing -> uv
+
+changeUConUVar :: UCon -> UVar -> UCon
+
+changeUConUVar (UCEq _ v ) uv' = (UCEq uv' v )
+changeUConUVar (UCBound us _ vs) uv' = (UCBound us uv' vs)
+changeUConUVar (UCUsOnce _ ) uv' = (UCUsOnce uv' )
+changeUConUVar (UCUsMany _ ) uv' = (UCUsMany uv' )
+\end{code}
+
+@mergeUVars@ tests to see if a set of @UVar@s can be constrained. If
+they can, it returns the set of root @UVar@s represented (with no
+duplicates); if they can't, it returns @Nothing@.
+
+\begin{code}
+mergeUVars :: VarEnv UCon -- current constraint set
+ -> Bool -- True/False = try to constrain to Many/Once
+ -> [UVar] -- list of UVars to constrain
+ -> Maybe [UVar] -- Just [root uvars to force], or Nothing if conflict
+
+mergeUVars cs isMany vs = foldl muv (Just []) vs
+ where
+ muv :: Maybe [UVar] -> UVar -> Maybe [UVar]
+ muv Nothing _
+ = Nothing
+ muv jvs@(Just vs) v
+ = let rv = findUCon cs v
+ in if elem rv vs
+ then
+ jvs
+ else
+ case lookupVarEnv cs rv of -- never UCEq
+ Nothing -> Just (rv:vs)
+ Just (UCBound _ _ _) -> Just (rv:vs)
+ Just (UCUsOnce _) -> if isMany then Nothing else jvs
+ Just (UCUsMany _) -> if isMany then jvs else Nothing
+\end{code}
+
+@addUCS@ adds an individual @UCon@ on a @UVar@ to a @UConSet@. This
+is the core of the algorithm. As such, it could probably use some
+optimising.
+
+\begin{code}
+addUCS :: UCon -- constraint to add
+ -> Either (VarEnv UCon) SDoc -- old constraint set or error
+ -> Either (VarEnv UCon) SDoc -- new constraint set or error
+
+addUCS _ jcs@(Right _) = jcs -- propagate errors
+
+addUCS (UCEq uv1 uv2) jcs@(Left cs)
+ = let ruv1 = findUCon cs uv1
+ ruv2 = findUCon cs uv2
+ in if ruv1==ruv2
+ then jcs -- no change if already equal
+ else let cs' = Left $ extendVarEnv cs ruv1 (UCEq ruv1 ruv2) -- merge trees
+ in case lookupVarEnv cs ruv1 of
+ Just uc'
+ -> addUCS (changeUConUVar uc' ruv2) cs' -- merge old constraints
+ Nothing
+ -> cs'
+
+addUCS (UCBound us uv1 vs) jcs@(Left cs)
+ = let ruv1 = findUCon cs uv1
+ in case lookupWithDefaultVarEnv cs (UCBound [] ruv1 []) ruv1 of -- never UCEq
+ UCBound us' _ vs'
+ -> case (mergeUVars cs False (us'++us),
+ mergeUVars cs True (vs'++vs)) of
+ (Just us'',Just vs'') -- update
+ -> Left $ extendVarEnv cs ruv1 (UCBound us'' ruv1 vs'')
+ (Nothing, Just vs'') -- set
+ -> addUCS (UCUsMany ruv1)
+ (forceUVars UCUsMany vs'' jcs)
+ (Just us'',Nothing) -- set
+ -> addUCS (UCUsOnce ruv1)
+ (forceUVars UCUsOnce us'' jcs)
+ (Nothing, Nothing) -- fail
+ -> Right (text "union failed[B] at" <+> ppr uv1)
+ UCUsOnce _
+ -> forceUVars UCUsOnce us jcs
+ UCUsMany _
+ -> forceUVars UCUsMany vs jcs
+
+addUCS (UCUsOnce uv1) jcs@(Left cs)
+ = let ruv1 = findUCon cs uv1
+ in case lookupWithDefaultVarEnv cs (UCBound [] ruv1 []) ruv1 of -- never UCEq
+ UCBound us _ vs
+ -> forceUVars UCUsOnce us (Left $ extendVarEnv cs ruv1 (UCUsOnce ruv1))
+ UCUsOnce _
+ -> jcs
+ UCUsMany _
+ -> Right (text "union failed[O] at" <+> ppr uv1)
+
+addUCS (UCUsMany uv1) jcs@(Left cs)
+ = let ruv1 = findUCon cs uv1
+ in case lookupWithDefaultVarEnv cs (UCBound [] ruv1 []) ruv1 of -- never UCEq
+ UCBound us _ vs
+ -> forceUVars UCUsMany vs (Left $ extendVarEnv cs ruv1 (UCUsMany ruv1))
+ UCUsOnce _
+ -> Right (text "union failed[M] at" <+> ppr uv1)
+ UCUsMany _
+ -> jcs
+
+-- helper function forcing a set of UVars to either Once or Many:
+forceUVars :: (UVar -> UCon)
+ -> [UVar]
+ -> Either (VarEnv UCon) SDoc
+ -> Either (VarEnv UCon) SDoc
+forceUVars uc uvs cs0 = foldl (\cs uv -> addUCS (uc uv) cs) cs0 uvs
+\end{code}
+
+======================================================================
+
+Pretty-printing:
+~~~~~~~~~~~~~~~~
+
+\begin{code}
+-- Printing a usage constraint.
+
+pprintUCon :: VarEnv UCon -> UCon -> SDoc
+
+pprintUCon fm (UCEq uv1 uv2)
+ = ppr uv1 <+> text "=" <+> ppr uv2 <> text ":"
+ <+> let uv2' = findUCon fm uv2
+ in case lookupVarEnv fm uv2' of
+ Just uc -> pprintUCon fm uc
+ Nothing -> text "unconstrained"
+
+pprintUCon fm (UCBound us uv vs)
+ = lbrace <> hcat (punctuate comma (map ppr us)) <> rbrace
+ <+> text "<=" <+> ppr uv <+> text "<="
+ <+> lbrace <> hcat (punctuate comma (map ppr vs)) <> rbrace
+
+pprintUCon fm (UCUsOnce uv)
+ = ppr uv <+> text "=" <+> ppr UsOnce
+
+pprintUCon fm (UCUsMany uv)
+ = ppr uv <+> text "=" <+> ppr UsMany
+
+-- Printing a usage constraint set.
+
+instance Outputable UConSet where
+ ppr (UConSet bfm)
+ = text "UConSet:" <+> lbrace
+ $$ vcat (map (\fm -> nest 2 (vcat (map (pprintUCon fm) (rngVarEnv fm))))
+ (bagToList bfm))
+ $$ rbrace
+
+ ppr (UConFail d)
+ = hang (text "UConSet inconsistent:")
+ 4 d
+\end{code}
+
+======================================================================
+
+EOF
--- /dev/null
+%
+% (c) The GRASP/AQUA Project, Glasgow University, 1998
+%
+\section[UsageSPInf]{UsageSP Inference Engine}
+
+This code is (based on) PhD work of Keith Wansbrough <kw217@cl.cam.ac.uk>,
+September 1998 .. May 1999.
+
+Keith Wansbrough 1998-09-04..1999-05-05
+
+\begin{code}
+module UsageSPInf ( doUsageSPInf ) where
+
+#include "HsVersions.h"
+
+import UsageSPUtils
+import UsageSPLint
+import UConSet
+
+import CoreSyn
+import Type ( Type(..), TyNote(..), UsageAnn(..),
+ applyTy, applyTys,
+ splitFunTy_maybe, splitFunTys, splitTyConApp_maybe,
+ mkUsgTy, splitUsgTy, isUsgTy, isNotUsgTy, unUsgTy, tyUsg,
+ mkFunTy, mkForAllTy )
+import TyCon ( tyConArgVrcs_maybe )
+import DataCon ( dataConType )
+import Const ( Con(..), Literal(..), literalType )
+import Var ( IdOrTyVar, UVar, varType, mkUVar, modifyIdInfo )
+import IdInfo ( setLBVarInfo, LBVarInfo(..) )
+import VarEnv
+import UniqSupply ( UniqSupply, UniqSM,
+ initUs, splitUniqSupply )
+import Outputable
+import CmdLineOpts ( opt_D_dump_usagesp, opt_DoUSPLinting )
+import ErrUtils ( doIfSet, dumpIfSet )
+import PprCore ( pprCoreBindings )
+\end{code}
+
+======================================================================
+
+The whole inference
+~~~~~~~~~~~~~~~~~~~
+
+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.
+
+Inference is performed as follows:
+
+ 1. Remove all manipulable[*] annotations and add fresh @UVar@
+ annotations.
+
+ 2. Walk over the resulting term 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.
+
+[*] A manipulable annotation is one derived from the current source
+module, as opposed to one derived from an import, which we are clearly
+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.
+
+
+The inference is done over a set of @CoreBind@s, and inside the IO
+monad.
+
+\begin{code}
+doUsageSPInf :: 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
+\end{code}
+
+======================================================================
+
+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.
+
+\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"
+ -- 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
+ -- 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)
+ }
+
+usgInfCE (Note InlineCall e) = usgInfCE e
+
+usgInfCE (Note (TermUsg u) e) = pprTrace "usgInfCE: ignoring extra TermUsg:" (ppr u) $
+ usgInfCE e
+
+usgInfCE (Type ty) = panic "usgInfCE: unexpected Type"
+\end{code}
+
+======================================================================
+
+Helper functions
+~~~~~~~~~~~~~~~~
+
+If a variable appears more than once in an fv set, force its usage to be Many.
+
+\begin{code}
+occChkUConSet :: IdOrTyVar
+ -> VarMultiset
+ -> UConSet
+
+occChkUConSet v fv = if occInMS v fv > 1
+ then eqManyUConSet ((tyUsg . varType) v)
+ else emptyUConSet
+
+occChksUConSet :: [IdOrTyVar]
+ -> VarMultiset
+ -> UConSet
+
+occChksUConSet vs fv = unionUCSs (map (\v -> occChkUConSet v fv) vs)
+\end{code}
+
+
+Subtyping and equal-typing relations. These generate constraint sets.
+Both assume their arguments are annotated correctly, and are either
+both tau-types or both sigma-types (in fact, are both exactly the same
+shape).
+
+\begin{code}
+usgSubTy ty1 ty2 = genUsgCmpTy cmp ty1 ty2
+ where cmp u1 u2 = leqUConSet u2 u1
+
+usgEqTy ty1 ty2 = genUsgCmpTy cmp ty1 ty2 -- **NB** doesn't equate tyconargs that
+ -- don't appear (see below)
+ where cmp u1 u2 = eqUConSet u1 u2
+
+genUsgCmpTy :: (UsageAnn -> UsageAnn -> UConSet) -- constraint (u1 REL u2), respectively
+ -> Type
+ -> Type
+ -> UConSet
+
+genUsgCmpTy cmp (NoteTy (UsgNote u1) ty1) (NoteTy (UsgNote u2) ty2)
+ = cmp u1 u2 `unionUCS` genUsgCmpTy cmp ty1 ty2
+
+#ifndef USMANY
+-- deal with omitted == UsMany
+genUsgCmpTy cmp (NoteTy (UsgNote u1) ty1) ty2
+ = cmp u1 UsMany `unionUCS` genUsgCmpTy cmp ty1 ty2
+genUsgCmpTy cmp ty1 (NoteTy (UsgNote u2) ty2)
+ = cmp UsMany u2 `unionUCS` genUsgCmpTy cmp ty1 ty2
+#endif
+
+genUsgCmpTy cmp (NoteTy (SynNote sty1) ty1) (NoteTy (SynNote sty2) ty2)
+ = genUsgCmpTy cmp sty1 sty2 `unionUCS` genUsgCmpTy cmp ty1 ty2
+ -- **! is this right? or should I throw away synonyms, or sth else?
+
+-- if SynNote only on one side, throw it out
+genUsgCmpTy cmp (NoteTy (SynNote sty1) ty1) ty2
+ = genUsgCmpTy cmp ty1 ty2
+genUsgCmpTy cmp ty1 (NoteTy (SynNote sty2) ty2)
+ = genUsgCmpTy cmp ty1 ty2
+
+-- ignore FTVNotes
+genUsgCmpTy cmp (NoteTy (FTVNote _) ty1) ty2
+ = genUsgCmpTy cmp ty1 ty2
+genUsgCmpTy cmp ty1 (NoteTy (FTVNote _) ty2)
+ = genUsgCmpTy cmp ty1 ty2
+
+genUsgCmpTy cmp (TyVarTy _) (TyVarTy _)
+ = emptyUConSet
+
+genUsgCmpTy cmp (AppTy tya1 tyb1) (AppTy tya2 tyb2)
+ = unionUCSs [genUsgCmpTy cmp tya1 tya2,
+ genUsgCmpTy cmp tyb1 tyb2, -- note, *both* ways for arg, since fun (prob) unknown
+ genUsgCmpTy cmp tyb2 tyb1]
+
+genUsgCmpTy cmp (TyConApp tc1 ty1s) (TyConApp tc2 ty2s)
+ = case tyConArgVrcs_maybe tc1 of
+ Just oi -> unionUCSs (zipWith3 (\ ty1 ty2 (occPos,occNeg) ->
+ -- strictly this is wasteful (and possibly dangerous) for
+ -- usgEqTy, but I think it's OK. KSW 1999-04.
+ (if occPos then genUsgCmpTy cmp ty1 ty2 else emptyUConSet)
+ `unionUCS`
+ (if occNeg then genUsgCmpTy cmp ty2 ty1 else emptyUConSet))
+ ty1s ty2s oi)
+ Nothing -> panic ("genUsgCmpTy: variance info unavailable for " ++ showSDoc (ppr tc1))
+
+genUsgCmpTy cmp (FunTy tya1 tyb1) (FunTy tya2 tyb2)
+ = genUsgCmpTy cmp tya2 tya1 `unionUCS` genUsgCmpTy cmp tyb1 tyb2 -- contravariance of arrow
+
+genUsgCmpTy cmp (ForAllTy _ ty1) (ForAllTy _ ty2)
+ = genUsgCmpTy cmp ty1 ty2
+
+genUsgCmpTy cmp ty1 ty2
+ = pprPanic "genUsgCmpTy: type shapes don't match" $
+ vcat [ppr ty1, ppr ty2]
+\end{code}
+
+
+Applying a substitution to all @UVar@s. This also moves @TermUsg@
+notes on lambdas into the @lbvarInfo@ field of the binder. This
+latter is a hack. KSW 1999-04.
+
+\begin{code}
+appUSubstTy :: (UVar -> UsageAnn)
+ -> Type
+ -> Type
+
+appUSubstTy s (NoteTy (UsgNote (UsVar uv)) ty)
+ = mkUsgTy (s uv) (appUSubstTy s ty)
+appUSubstTy s (NoteTy note@(UsgNote _) ty) = NoteTy note (appUSubstTy s ty)
+appUSubstTy s (NoteTy note@(SynNote _) ty) = NoteTy note (appUSubstTy s ty)
+appUSubstTy s (NoteTy note@(FTVNote _) ty) = NoteTy note (appUSubstTy s ty)
+appUSubstTy s ty@(TyVarTy _) = ty
+appUSubstTy s (AppTy ty1 ty2) = AppTy (appUSubstTy s ty1) (appUSubstTy s ty2)
+appUSubstTy s (TyConApp tc tys) = TyConApp tc (map (appUSubstTy s) tys)
+appUSubstTy s (FunTy ty1 ty2) = FunTy (appUSubstTy s ty1) (appUSubstTy s ty2)
+appUSubstTy s (ForAllTy tyv ty) = ForAllTy tyv (appUSubstTy s ty)
+
+
+appUSubstBinds :: (UVar -> UsageAnn)
+ -> [CoreBind]
+ -> [CoreBind]
+
+appUSubstBinds s binds = fst $ initAnnotM () $
+ genAnnotBinds mungeType mungeTerm binds
+ where mungeType _ ty = -- simply perform substitution
+ return (appUSubstTy s ty)
+
+ mungeTerm (Note (TermUsg (UsVar uv)) (Lam v e))
+ -- perform substitution *and* munge annot on lambda into IdInfo.lbvarInfo
+ = let lb = case (s uv) of { UsOnce -> IsOneShotLambda; UsMany -> NoLBVarInfo }
+ v' = modifyIdInfo v (setLBVarInfo lb) -- HACK ALERT!
+ -- see comment in IdInfo.lhs; this is because the info is easier to
+ -- access here, by agreement SLPJ/KSW 1999-04 (as a "short-term hack").
+ in return (Lam v' e)
+ -- really should be: return (Note (TermUsg (s uv)) (Lam v e))
+ mungeTerm e@(Lam _ _) = return e
+ mungeTerm e = panic "appUSubstBinds: mungeTerm:" (ppr e)
+\end{code}
+
+
+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
+
+emptyMS = emptyVarEnv
+unitMS v = unitVarEnv v (v,1)
+delFromMS = delVarEnv
+plusMS :: VarMultiset -> VarMultiset -> VarMultiset
+plusMS = plusVarEnv_C (\ (v,n) (_,m) -> (v,n+m))
+maxMS :: VarMultiset -> VarMultiset -> VarMultiset
+maxMS = plusVarEnv_C (\ (v,n) (_,m) -> (v,max n m))
+mapMS f = mapVarEnv (\ (v,n) -> f v n)
+foldMS f = foldVarEnv (\ (v,n) a -> f v n a)
+occInMS v ms = case lookupVarEnv ms v of
+ Just (_,n) -> n
+ Nothing -> 0
+\end{code}
+
+And a function used in debugging. It may give false positives with -DUSMANY turned off.
+
+\begin{code}
+isUnAnnotated :: Type -> Bool
+
+isUnAnnotated (NoteTy (UsgNote _ ) _ ) = False
+isUnAnnotated (NoteTy (SynNote sty) ty) = isUnAnnotated sty && isUnAnnotated ty
+isUnAnnotated (NoteTy (FTVNote _ ) ty) = isUnAnnotated ty
+isUnAnnotated (TyVarTy _) = True
+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{code}
+
+======================================================================
+
+EOF
--- /dev/null
+%
+% (c) The GRASP/AQUA Project, Glasgow University, 1998
+%
+\section[UsageSPLint]{UsageSP ``lint'' pass}
+
+This code is (based on) PhD work of Keith Wansbrough <kw217@cl.cam.ac.uk>,
+September 1998 .. May 1999.
+
+Keith Wansbrough 1998-09-04..1999-05-03
+
+\begin{code}
+module UsageSPLint ( doLintUSPAnnotsBinds,
+ doLintUSPConstBinds,
+ doLintUSPBinds,
+ doCheckIfWorseUSP,
+ ) where
+
+#include "HsVersions.h"
+
+import UsageSPUtils
+import CoreSyn
+import Type ( Type(..), TyNote(..), UsageAnn(..), isUsgTy, tyUsg )
+import TyCon ( isAlgTyCon, isPrimTyCon, isSynTyCon, isFunTyCon )
+import Var ( IdOrTyVar, varType, idInfo )
+import IdInfo ( LBVarInfo(..), lbvarInfo )
+import SrcLoc ( noSrcLoc )
+import ErrUtils ( Message, ghcExit )
+import Util ( zipWithEqual )
+import PprCore
+import Bag
+import Outputable
+\end{code}
+
+======================================================================
+
+Interface
+~~~~~~~~~
+
+@doLintUSPAnnotsBinds@ checks that annotations are in the correct positions.
+@doLintUSPConstsBinds@ checks that no @UVar@s remain anywhere (i.e., all annots are constants).
+@doLintUSPBinds@ checks that the annotations are consistent. [unimplemented!]
+@doCheckIfWorseUSP@ checks that annots on binders have not changed from Once to Many.
+
+\begin{code}
+doLint :: ULintM a -> IO ()
+
+doLint m = case runULM m of
+ Nothing -> return ()
+ Just bad_news -> do { printDump (display bad_news)
+ ; ghcExit 1
+ }
+ where display bad_news = vcat [ text "*** LintUSP errors: ***"
+ , bad_news
+ , text "*** end of LintUSP errors ***"
+ ]
+
+doLintUSPAnnotsBinds, doLintUSPConstBinds :: [CoreBind] -> IO ()
+
+doLintUSPAnnotsBinds = doLint . lintUSPAnnotsBinds
+doLintUSPConstBinds = doLint . lintUSPConstBinds
+
+-- doLintUSPBinds is defined below
+
+doCheckIfWorseUSP :: [CoreBind] -> [CoreBind] -> IO ()
+
+doCheckIfWorseUSP binds binds'
+ = case checkIfWorseUSP binds binds' of
+ Nothing -> return ()
+ Just warns -> printErrs warns
+\end{code}
+
+======================================================================
+
+Verifying correct annotation positioning
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+The following functions check whether the usage annotations are
+correctly placed on a type. They sit inside the lint monad.
+@lintUSPAnnots@ assumes there should be an outermost annotation,
+@lintUSPAnnotsN@ assumes there shouldn't.
+
+The fact that no general catch-all pattern is given for @NoteTy@s is
+entirely intentional. The meaning of future extensions here is
+entirely unknown, so you'll have to decide how to check them
+explicitly.
+
+\begin{code}
+lintTyUSPAnnots :: Bool -- die on omitted annotation?
+ -> Bool -- die on extra annotation?
+ -> Type -- type to check
+ -> ULintM ()
+
+lintTyUSPAnnots fom fex = lint
+ where
+ lint (NoteTy (UsgNote _) ty) = lintTyUSPAnnotsN fom fex ty
+ lint ty0 = do { mayErrULM fom "missing UsgNote" ty0
+ ; lintTyUSPAnnotsN fom fex ty0
+ }
+
+lintTyUSPAnnotsN :: Bool -- die on omitted annotation?
+ -> Bool -- die on extra annotation?
+ -> Type -- type to check
+ -> ULintM ()
+
+lintTyUSPAnnotsN fom fex = lintN
+ where
+ lintN ty0@(NoteTy (UsgNote _) ty) = do { mayErrULM fex "unexpected UsgNote" ty0
+ ; lintN ty
+ }
+ lintN (NoteTy (SynNote sty) ty) = do { lintN sty
+ ; lintN ty
+ }
+ lintN (NoteTy (FTVNote _) ty) = do { lintN ty }
+
+ lintN (TyVarTy _) = do { return () }
+ lintN (AppTy ty1 ty2) = do { lintN ty1
+ ; lintN ty2
+ }
+ lintN (TyConApp tc tys) = ASSERT( isFunTyCon tc || isAlgTyCon tc || isPrimTyCon tc || isSynTyCon tc )
+ do { let thelint = if isFunTyCon tc
+ then lintTyUSPAnnots fom fex
+ else lintN
+ ; mapM thelint tys
+ ; return ()
+ }
+ lintN (FunTy ty1 ty2) = do { lintTyUSPAnnots fom fex ty1
+ ; lintTyUSPAnnots fom fex ty2
+ }
+ lintN (ForAllTy _ ty) = do { lintN ty }
+\end{code}
+
+
+Now the combined function that takes a @MungeFlags@ to tell it what to
+do to a particular type. This is passed to @genAnnotBinds@ to get the
+work done.
+
+\begin{code}
+lintUSPAnnotsTyM :: MungeFlags -> Type -> AnnotM (ULintM ()) Type
+
+lintUSPAnnotsTyM mf ty = AnnotM $ \ m ve ->
+ (ty, do { m
+ ; atLocULM (mfLoc mf) $
+ (if isSigma mf
+ then lintTyUSPAnnots
+ else lintTyUSPAnnotsN) checkOmitted True ty
+ },
+ ve)
+#ifndef USMANY
+ where checkOmitted = False -- OK to omit Many if !USMANY
+#else
+ where checkOmitted = True -- require all annotations
+#endif
+
+lintUSPAnnotsBinds :: [CoreBind]
+ -> ULintM ()
+
+lintUSPAnnotsBinds binds = case initAnnotM (return ()) $
+ genAnnotBinds lintUSPAnnotsTyM return binds of
+ -- **! should check with mungeTerm too!
+ (_,m) -> m
+\end{code}
+
+======================================================================
+
+Verifying correct usage typing
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+The following function verifies that all usage annotations are
+consistent. It assumes that there are no usage variables, only
+@UsOnce@ and @UsMany@ annotations.
+
+This is very similar to usage inference, however, and so we could
+simply use that, with a little work. For now, it's unimplemented.
+
+\begin{code}
+doLintUSPBinds :: [CoreBind] -> IO ()
+
+doLintUSPBinds binds = panic "doLintUSPBinds unimplemented"
+ {- case initUs us (uniqSMMToUs (usgInfBinds binds)) of
+ ((ucs,_),_) -> if isJust (solveUCS ucs)
+ then return ()
+ else do { printDump (text "*** LintUSPBinds failed ***")
+ ; ghcExit 1
+ }
+ -}
+\end{code}
+
+======================================================================
+
+Verifying usage constants only (not vars)
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+The following function checks that all usage annotations are ground,
+i.e., @UsOnce@ or @UsMany@: no @UVar@s remain.
+
+\begin{code}
+lintTyUSPConst :: Type
+ -> ULintM ()
+
+lintTyUSPConst (TyVarTy _) = do { return () }
+
+lintTyUSPConst (AppTy ty1 ty2) = do { lintTyUSPConst ty1
+ ; lintTyUSPConst ty2
+ }
+lintTyUSPConst (TyConApp tc tys) = do { mapM lintTyUSPConst tys
+ ; return ()
+ }
+lintTyUSPConst (FunTy ty1 ty2) = do { lintTyUSPConst ty1
+ ; lintTyUSPConst ty2
+ }
+lintTyUSPConst (ForAllTy _ ty) = do { lintTyUSPConst ty }
+
+lintTyUSPConst ty0@(NoteTy (UsgNote (UsVar _)) ty) = do { errULM "unexpected usage variable" ty0
+ ; lintTyUSPConst ty
+ }
+lintTyUSPConst ty0@(NoteTy (UsgNote _) ty) = do { lintTyUSPConst ty }
+lintTyUSPConst ty0@(NoteTy (SynNote sty) ty) = do { lintTyUSPConst sty
+ ; lintTyUSPConst ty
+ }
+lintTyUSPConst ty0@(NoteTy (FTVNote _) ty) = do { lintTyUSPConst ty }
+\end{code}
+
+
+Now the combined function and the invocation of @genAnnotBinds@ to do the real work.
+
+\begin{code}
+lintUSPConstTyM :: MungeFlags -> Type -> AnnotM (ULintM ()) Type
+
+lintUSPConstTyM mf ty = AnnotM $ \ m ve ->
+ (ty,
+ do { m
+ ; atLocULM (mfLoc mf) $
+ lintTyUSPConst ty
+ },
+ ve)
+
+lintUSPConstBinds :: [CoreBind]
+ -> ULintM ()
+
+lintUSPConstBinds binds = case initAnnotM (return ()) $
+ genAnnotBinds lintUSPConstTyM return binds of
+ -- **! should check with mungeTerm too!
+ (_,m) -> m
+\end{code}
+
+======================================================================
+
+Checking annotations don't get any worse
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+It is assumed that all transformations in GHC are `work-safe', that
+is, they do not cause any work to be duplicated. Thus they should
+also be safe wrt the UsageSP analysis: if an identifier has a
+used-once type at one point, the identifier should never become
+used-many after transformation. This check verifies that this is the
+case.
+
+The arguments are the CoreBinds before and after the inference. They
+must have exactly the same shape apart from usage annotations.
+
+We only bother checking binders; free variables *should* be fixed
+already since they are imported and not changeable.
+
+First, the various kinds of worsenings we can have:
+
+\begin{code}
+data WorseErr = WorseVar IdOrTyVar IdOrTyVar -- variable gets worse
+ | WorseTerm CoreExpr CoreExpr -- term gets worse
+ | WorseLam IdOrTyVar IdOrTyVar -- lambda gets worse
+
+instance Outputable WorseErr where
+ ppr (WorseVar v0 v) = ptext SLIT("Identifier:") <+> ppr v0 <+> dcolon
+ <+> ( ptext SLIT("was") <+> ppr (varType v0)
+ $$ ptext SLIT("now") <+> ppr (varType v))
+ ppr (WorseTerm e0 e) = ptext SLIT("Term:")
+ <+> ( ptext SLIT("was") <+> ppr e0
+ $$ ptext SLIT("now") <+> ppr e)
+ ppr (WorseLam v0 v) = ptext SLIT("Lambda:")
+ <+> ( ppr v0
+ $$ ptext SLIT("(lambda-bound var info for var worsened)"))
+\end{code}
+
+Now the checker.
+
+\begin{code}
+checkIfWorseUSP :: [CoreBind] -- old binds
+ -> [CoreBind] -- new binds
+ -> Maybe SDoc -- maybe warnings
+
+checkIfWorseUSP binds binds'
+ = let vvs = checkBinds binds binds'
+ in if isEmptyBag vvs then
+ Nothing
+ else
+ Just $ ptext SLIT("UsageSP warning: annotations worsen for")
+ $$ nest 4 (vcat (map ppr (bagToList vvs)))
+
+checkBinds :: [CoreBind] -> [CoreBind] -> Bag WorseErr
+checkBinds binds binds' = unionManyBags $
+ zipWithEqual "UsageSPLint.checkBinds" checkBind binds binds'
+
+checkBind :: CoreBind -> CoreBind -> Bag WorseErr
+checkBind (NonRec v e) (NonRec v' e') = (checkVar v v') `unionBags` (checkCE e e')
+checkBind (Rec ves) (Rec ves') = unionManyBags $
+ zipWithEqual "UsageSPLint.checkBind"
+ (\ (v,e) (v',e') -> (checkVar v v')
+ `unionBags` (checkCE e e'))
+ ves ves'
+checkBind _ _ = panic "UsageSPLint.checkBind"
+
+
+checkCE :: CoreExpr -> CoreExpr -> Bag WorseErr
+
+checkCE (Var _) (Var _) = emptyBag
+
+checkCE (Con _ args) (Con _ args') = unionManyBags $
+ zipWithEqual "UsageSPLint.checkCE:Con"
+ checkCE args args'
+
+checkCE (App e arg) (App e' arg') = (checkCE e e')
+ `unionBags` (checkCE arg arg')
+
+checkCE (Lam v e) (Lam v' e') = (checkVar v v')
+ `unionBags` (checkLamVar v v')
+ `unionBags` (checkCE e e')
+
+checkCE (Let bind e) (Let bind' e') = (checkBind bind bind')
+ `unionBags` (checkCE e e')
+
+checkCE (Case e v alts) (Case e' v' alts')
+ = (checkCE e e')
+ `unionBags` (checkVar v v')
+ `unionBags` (unionManyBags $
+ zipWithEqual "usageSPLint.checkCE:Case"
+ checkAlts alts alts')
+ where checkAlts (_,vs,e) (_,vs',e') = (unionManyBags $ zipWithEqual "UsageSPLint.checkCE:Alt"
+ checkVar vs vs')
+ `unionBags` (checkCE e e')
+
+checkCE (Note (SCC _) e) (Note (SCC _) e') = checkCE e e'
+
+checkCE (Note (Coerce _ _) e) (Note (Coerce _ _) e') = checkCE e e'
+
+checkCE (Note InlineCall e) (Note InlineCall e') = checkCE e e'
+
+checkCE t@(Note (TermUsg u) e) t'@(Note (TermUsg u') e')
+ = checkCE e e'
+ `unionBags` (checkUsg u u' (WorseTerm t t'))
+
+checkCE (Type _) (Type _) = emptyBag
+
+checkCE t t' = pprPanic "usageSPLint.checkCE:"
+ (ppr t $$ text "doesn't match" <+> ppr t')
+
+
+-- does binder change from Once to Many?
+-- notice we only check the top-level annotation; this is all that's necessary. KSW 1999-04.
+checkVar :: IdOrTyVar -> IdOrTyVar -> Bag WorseErr
+checkVar v v' | isTyVar v = emptyBag
+ | not (isUsgTy y) = emptyBag -- if initially no annot, definitely OK
+ | otherwise = checkUsg u u' (WorseVar v v')
+ where y = varType v
+ y' = varType v'
+ u = tyUsg y
+ u' = tyUsg y'
+
+-- does lambda change from Once to Many?
+checkLamVar :: IdOrTyVar -> IdOrTyVar -> Bag WorseErr
+checkLamVar v v' | isTyVar v = emptyBag
+ | otherwise = case ((lbvarInfo . idInfo) v, (lbvarInfo . idInfo) v') of
+ (NoLBVarInfo , _ ) -> emptyBag
+ (IsOneShotLambda, IsOneShotLambda) -> emptyBag
+ (IsOneShotLambda, NoLBVarInfo ) -> unitBag (WorseLam v v')
+
+-- does term usage annotation change from Once to Many?
+checkUsg :: UsageAnn -> UsageAnn -> WorseErr -> Bag WorseErr
+checkUsg UsMany _ _ = emptyBag
+checkUsg UsOnce UsOnce _ = emptyBag
+checkUsg UsOnce UsMany err = unitBag err
+\end{code}
+
+======================================================================
+
+Lint monad stuff
+~~~~~~~~~~~~~~~~
+
+The errors (@ULintErr@s) are collected in the @ULintM@ monad, which
+also tracks the location of the current type being checked.
+
+\begin{code}
+data ULintErr = ULintErr SDoc String Type
+
+pprULintErr :: ULintErr -> SDoc
+pprULintErr (ULintErr loc s ty) = hang (text s <+> ptext SLIT("in") <+> loc <> ptext SLIT(":"))
+ 4 (ppr ty)
+
+
+newtype ULintM a = ULintM (SDoc -> (a,Bag ULintErr))
+unULintM (ULintM f) = f
+
+instance Monad ULintM where
+ m >>= f = ULintM $ \ loc -> let (a ,errs ) = (unULintM m) loc
+ (a',errs') = (unULintM (f a)) loc
+ in (a', errs `unionBags` errs')
+ return a = ULintM $ \ _ -> (a,emptyBag)
+
+atLocULM :: SDoc -> ULintM a -> ULintM a
+atLocULM loc m = ULintM $ \ _ -> (unULintM m) loc
+
+errULM :: String -> Type -> ULintM ()
+errULM err ty
+ = ULintM $ \ loc -> ((),unitBag $ ULintErr loc err ty)
+
+mayErrULM :: Bool -> String -> Type -> ULintM ()
+mayErrULM f err ty
+ = if f then errULM err ty else return ()
+
+runULM :: ULintM a -> Maybe SDoc
+runULM m = case (unULintM m) (panic "runULM: no location") of
+ (_,errs) -> if isEmptyBag errs
+ then Nothing
+ else Just (vcat (map pprULintErr (bagToList errs)))
+\end{code}
+
+======================================================================
+
+EOF
--- /dev/null
+%
+% (c) The GRASP/AQUA Project, Glasgow University, 1998
+%
+\section[UsageSPUtils]{UsageSP Utilities}
+
+This code is (based on) PhD work of Keith Wansbrough <kw217@cl.cam.ac.uk>,
+September 1998 .. May 1999.
+
+Keith Wansbrough 1998-09-04..1999-05-07
+
+\begin{code}
+module UsageSPUtils ( AnnotM(AnnotM), initAnnotM,
+ genAnnotBinds,
+ MungeFlags(isSigma,isLocal,isExp,hasUsg,mfLoc),
+
+ doAnnotBinds, doUnAnnotBinds,
+ annotMany, annotManyN, unannotTy, freshannotTy,
+
+ newVarUs, newVarUSMM,
+ UniqSMM, usToUniqSMM, uniqSMMToUs,
+
+ primOpUsgTys,
+ ) where
+
+#include "HsVersions.h"
+
+import CoreSyn
+import Const ( Con(..), Literal(..) )
+import Var ( IdOrTyVar, varName, varType, setVarType, mkUVar )
+import Id ( idMustBeINLINEd )
+import Name ( isLocallyDefined, isExported )
+import Type ( Type(..), TyNote(..), UsageAnn(..), isUsgTy, substTy, splitFunTys )
+import TyCon ( isAlgTyCon, isPrimTyCon, isSynTyCon, isFunTyCon )
+import VarEnv
+import PrimOp ( PrimOp, primOpUsg )
+import Maybes ( expectJust )
+import UniqSupply ( UniqSupply, UniqSM, initUs, getUniqueUs, thenUs, returnUs )
+import Outputable
+import PprCore ( ) -- instances only
+\end{code}
+
+======================================================================
+
+Walking over (and altering) types
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+We often need to fiddle with (i.e., add or remove) usage annotations
+on a type. We define here a general framework to do this. Usage
+annotations come from any monad with a function @getAnnM@ which yields
+a new annotation. We use two mutually recursive functions, one for
+sigma types and one for tau types.
+
+\begin{code}
+genAnnotTy :: Monad m =>
+ (m UsageAnn) -- get new annotation
+ -> Type -- old type
+ -> m Type -- new type
+
+genAnnotTy getAnnM ty = do { u <- getAnnM
+ ; ty' <- genAnnotTyN getAnnM ty
+ ; return (NoteTy (UsgNote u) ty')
+ }
+
+genAnnotTyN :: Monad m =>
+ (m UsageAnn)
+ -> Type
+ -> m Type
+
+genAnnotTyN getAnnM
+ (NoteTy (UsgNote _) ty) = panic "genAnnotTyN: unexpected UsgNote"
+genAnnotTyN getAnnM
+ (NoteTy (SynNote sty) ty) = do { sty' <- genAnnotTyN getAnnM sty
+ -- is this right? shouldn't there be some
+ -- correlation between sty' and ty'?
+ -- But sty is a TyConApp; does this make it safer?
+ ; ty' <- genAnnotTyN getAnnM ty
+ ; return (NoteTy (SynNote sty') ty')
+ }
+genAnnotTyN getAnnM
+ (NoteTy fvn@(FTVNote _) ty) = do { ty' <- genAnnotTyN getAnnM ty
+ ; return (NoteTy fvn ty')
+ }
+
+genAnnotTyN getAnnM
+ ty0@(TyVarTy _) = do { return ty0 }
+
+genAnnotTyN getAnnM
+ (AppTy ty1 ty2) = do { ty1' <- genAnnotTyN getAnnM ty1
+ ; ty2' <- genAnnotTyN getAnnM ty2
+ ; return (AppTy ty1' ty2')
+ }
+
+genAnnotTyN getAnnM
+ (TyConApp tc tys) = ASSERT( isFunTyCon tc || isAlgTyCon tc || isPrimTyCon tc || isSynTyCon tc )
+ do { let gAT = if isFunTyCon tc
+ then genAnnotTy -- sigma for partial apps of (->)
+ else genAnnotTyN -- tau otherwise
+ ; tys' <- mapM (gAT getAnnM) tys
+ ; return (TyConApp tc tys')
+ }
+
+genAnnotTyN getAnnM
+ (FunTy ty1 ty2) = do { ty1' <- genAnnotTy getAnnM ty1
+ ; ty2' <- genAnnotTy getAnnM ty2
+ ; return (FunTy ty1' ty2')
+ }
+
+genAnnotTyN getAnnM
+ (ForAllTy v ty) = do { ty' <- genAnnotTyN getAnnM ty
+ ; return (ForAllTy v ty')
+ }
+\end{code}
+
+
+
+Walking over (and retyping) terms
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+We also often need to play with the types in a term. This is slightly
+tricky because of redundancy: we want to change binder types, and keep
+the bound types matching these; then there's a special case also with
+non-locally-defined bound variables. We generalise over all this
+here.
+
+The name `annot' is a bit of a misnomer, as the code is parameterised
+over exactly what it does to the types (and certain terms). Notice
+also that it is possible for this parameter to use
+monadically-threaded state: here called `flexi'. For genuine
+annotation, this state will be a UniqSupply.
+
+We may add annotations to the outside of a (term, not type) lambda; a
+function passed to @genAnnotBinds@ does this, taking the lambda and
+returning the annotated lambda. It is inside the @AnnotM@ monad.
+This term-munging function is applied when we see either a term lambda
+or a usage annotation; *IMPORTANT:* it is applied *before* we recurse
+down into the term, and it is expected to work only at the top level.
+Recursion will subsequently be done by genAnnotBinds. It may
+optionally remove a Note TermUsg, or optionally add one if it is not
+already present, but it may perform NO OTHER MODIFICATIONS to the
+structure of the term.
+
+We do different things to types of variables bound locally and of
+variables bound in other modules, in certain cases: the former get
+uvars and the latter keep their existing annotations when we annotate,
+for example. To control this, @MungeFlags@ describes what kind of a
+type this is that we're about to munge.
+
+\begin{code}
+data MungeFlags = MungeFlags { isSigma :: Bool, -- want annotated on top (sigma type)
+ isLocal :: Bool, -- is locally-defined type
+ hasUsg :: Bool, -- has fixed usage info, don't touch
+ isExp :: Bool, -- is exported (and must be pessimised)
+ mfLoc :: SDoc -- location info
+ }
+
+tauTyMF loc = MungeFlags { isSigma = False, isLocal = True,
+ hasUsg = False, isExp = False, mfLoc = loc }
+sigVarTyMF v = MungeFlags { isSigma = True, isLocal = hasLocalDef v,
+ hasUsg = hasUsgInfo v, isExp = isExported v,
+ mfLoc = ptext SLIT("type of binder") <+> ppr v }
+\end{code}
+
+The helper functions @tauTyMF@ and @sigVarTyMF@ create @MungeFlags@
+for us. @sigVarTyMF@ checks the variable to see how to set the flags.
+
+@hasLocalDef@ tells us if the given variable has an actual local
+definition that we can play with. This is not quite the same as
+@isLocallyDefined@, since @IMustBeINLINEd@ things (usually) don't have
+a local definition - the simplifier will inline whatever their
+unfolding is anyway. We treat these as if they were externally
+defined, since we don't have access to their definition (at least not
+easily). This doesn't hurt much, since after the simplifier has run
+the unfolding will have been inlined and we can access the unfolding
+directly.
+
+@hasUsgInfo@, on the other hand, says if the variable already has
+usage info in its type that must at all costs be preserved. This is
+assumed true (exactly) of all imported ids.
+
+\begin{code}
+hasLocalDef :: IdOrTyVar -> Bool
+hasLocalDef var = isLocallyDefined var
+ && not (idMustBeINLINEd var)
+
+hasUsgInfo :: IdOrTyVar -> Bool
+hasUsgInfo var = (not . isLocallyDefined) var
+\end{code}
+
+Here's the walk itself.
+
+\begin{code}
+genAnnotBinds :: (MungeFlags -> Type -> AnnotM flexi Type)
+ -> (CoreExpr -> AnnotM flexi CoreExpr) -- see caveats above
+ -> [CoreBind]
+ -> AnnotM flexi [CoreBind]
+
+genAnnotBinds _ _ [] = return []
+
+genAnnotBinds f g (b:bs) = do { (b',vs,vs') <- genAnnotBind f g b
+ ; bs' <- withAnnVars vs vs' $
+ genAnnotBinds f g bs
+ ; return (b':bs')
+ }
+
+genAnnotBind :: (MungeFlags -> Type -> AnnotM flexi Type) -- type-altering function
+ -> (CoreExpr -> AnnotM flexi CoreExpr) -- term-altering function
+ -> CoreBind -- original CoreBind
+ -> AnnotM flexi
+ (CoreBind, -- annotated CoreBind
+ [IdOrTyVar], -- old variables, to be mapped to...
+ [IdOrTyVar]) -- ... new variables
+
+genAnnotBind f g (NonRec v1 e1) = do { v1' <- genAnnotVar f v1
+ ; e1' <- genAnnotCE f g e1
+ ; return (NonRec v1' e1', [v1], [v1'])
+ }
+
+genAnnotBind f g (Rec ves) = do { let (vs,es) = unzip ves
+ ; vs' <- mapM (genAnnotVar f) vs
+ ; es' <- withAnnVars vs vs' $
+ mapM (genAnnotCE f g) es
+ ; return (Rec (zip vs' es'), vs, vs')
+ }
+
+genAnnotCE :: (MungeFlags -> Type -> AnnotM flexi Type) -- type-altering function
+ -> (CoreExpr -> AnnotM flexi CoreExpr) -- term-altering function
+ -> CoreExpr -- original expression
+ -> AnnotM flexi CoreExpr -- yields new expression
+
+genAnnotCE mungeType mungeTerm = go
+ where go e0@(Var v) | isTyVar v = return e0 -- arises, e.g., as tyargs of Con
+ -- (no it doesn't: (Type (TyVar tyvar))
+ | otherwise = do { mv' <- lookupAnnVar v
+ ; v' <- case mv' of
+ Just var -> return var
+ Nothing -> fixedVar v
+ ; return (Var v')
+ }
+
+ go (Con c args) = -- we know it's saturated
+ do { args' <- mapM go args
+ ; return (Con c args')
+ }
+
+ go (App e arg) = do { e' <- go e
+ ; arg' <- go arg
+ ; return (App e' arg')
+ }
+
+ go e0@(Lam v0 _) = do { e1 <- (if isTyVar v0 then return else mungeTerm) e0
+ ; let (v,e2,wrap)
+ = case e1 of -- munge may have added note
+ Note tu@(TermUsg _) (Lam v e2)
+ -> (v,e2,Note tu)
+ Lam v e2 -> (v,e2,id)
+ ; v' <- genAnnotVar mungeType v
+ ; e' <- withAnnVar v v' $ go e2
+ ; return (wrap (Lam v' e'))
+ }
+
+ go (Let bind e) = do { (bind',vs,vs') <- genAnnotBind mungeType mungeTerm bind
+ ; e' <- withAnnVars vs vs' $ go e
+ ; return (Let bind' e')
+ }
+
+ go (Case e v alts) = do { e' <- go e
+ ; v' <- genAnnotVar mungeType v
+ ; alts' <- withAnnVar v v' $ mapM genAnnotAlt alts
+ ; return (Case e' v' alts')
+ }
+
+ go (Note scc@(SCC _) e) = do { e' <- go e
+ ; return (Note scc e')
+ }
+ go e0@(Note (Coerce ty1 ty0)
+ e) = do { ty1' <- mungeType
+ (tauTyMF (ptext SLIT("coercer of")
+ <+> ppr e0)) ty1
+ ; ty0' <- mungeType
+ (tauTyMF (ptext SLIT("coercee of")
+ <+> ppr e0)) ty0
+ -- (Better to specify ty0'
+ -- identical to the type of e, including
+ -- annotations, right at the beginning, but
+ -- not possible at this point.)
+ ; e' <- go e
+ ; return (Note (Coerce ty1' ty0') e')
+ }
+ go (Note InlineCall e) = do { e' <- go e
+ ; return (Note InlineCall e')
+ }
+ go e0@(Note (TermUsg _) _) = do { e1 <- mungeTerm e0
+ ; case e1 of -- munge may have removed note
+ Note tu@(TermUsg _) e2 -> do { e3 <- go e2
+ ; return (Note tu e3)
+ }
+ e2 -> go e2
+ }
+
+ go e0@(Type ty) = -- should only occur at toplevel of Arg,
+ -- hence tau-type
+ do { ty' <- mungeType
+ (tauTyMF (ptext SLIT("tyarg")
+ <+> ppr e0)) ty
+ ; return (Type ty')
+ }
+
+ fixedVar v = ASSERT2( not (hasLocalDef v), text "genAnnotCE: locally defined var" <+> ppr v <+> text "not in varenv" )
+ genAnnotVar mungeType v
+
+ genAnnotAlt (c,vs,e) = do { vs' <- mapM (genAnnotVar mungeType) vs
+ ; e' <- withAnnVars vs vs' $ go e
+ ; return (c, vs', e')
+ }
+
+
+genAnnotVar :: (MungeFlags -> Type -> AnnotM flexi Type)
+ -> IdOrTyVar
+ -> AnnotM flexi IdOrTyVar
+
+genAnnotVar mungeType v | isTyVar v = return v
+ | otherwise = do { vty' <- mungeType (sigVarTyMF v) (varType v)
+ ; return (setVarType v vty')
+ }
+{- #ifdef DEBUG
+ ; return $
+ pprTrace "genAnnotVar" (ppr (tyUsg vty') <+> ppr v) $
+ (setVarType v vty')
+ #endif
+ -}
+\end{code}
+
+======================================================================
+
+Some specific things to do to types inside terms
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+@annotTyM@ annotates a type with fresh uvars everywhere the inference
+is allowed to go, and leaves alone annotations where it may not go.
+
+We assume there are no annotations already.
+
+\begin{code}
+annotTyM :: MungeFlags -> Type -> AnnotM UniqSupply Type
+-- general function
+annotTyM mf ty = uniqSMtoAnnotM . uniqSMMToUs $
+ case (hasUsg mf, isLocal mf, isSigma mf) of
+ (True ,_ ,_ ) -> ASSERT( isUsgTy ty )
+ return ty
+ (False,True ,True ) -> if isExp mf then
+ annotTyP (tag 'p') ty
+ else
+ annotTy (tag 's') ty
+ (False,True ,False) -> annotTyN (tag 't') ty
+ (False,False,True ) -> return $ annotMany ty -- assume worst
+ (False,False,False) -> return $ annotManyN ty
+ where tag c = Right $ "annotTyM:" ++ [c] ++ ": " ++ showSDoc (ppr ty)
+
+-- specific functions for annotating tau and sigma types
+
+-- ...with uvars
+annotTy tag = genAnnotTy (newVarUSMM tag)
+annotTyN tag = genAnnotTyN (newVarUSMM tag)
+
+-- ...with uvars and pessimal Manys (for exported ids)
+annotTyP tag ty = do { ty' <- annotTy tag ty ; return (pessimise True ty') }
+
+-- ...with Many
+annotMany, annotManyN :: Type -> Type
+#ifndef USMANY
+annotMany = id
+annotManyN = id
+#else
+annotMany ty = unId (genAnnotTy (return UsMany) ty)
+annotManyN ty = unId (genAnnotTyN (return UsMany) ty)
+#endif
+
+-- monad required for the above
+newtype Id a = Id a ; unId (Id a) = a
+instance Monad Id where { a >>= f = f (unId a) ; return a = Id a }
+
+-- lambda-annotating function for use along with the above
+annotLam e0@(Lam v e) = do { uv <- uniqSMtoAnnotM $ newVarUs (Left e0)
+ ; return (Note (TermUsg uv) (Lam v e))
+ }
+annotLam (Note (TermUsg _) _) = panic "annotLam: unexpected term usage annot"
+\end{code}
+
+The above requires a `pessimising' translation. This is applied to
+types of exported ids, and ensures that they have a fully general
+type (since we don't know how they will be used in other modules).
+
+\begin{code}
+pessimise :: Bool -> Type -> Type
+
+#ifndef USMANY
+pessimise co ty0@(NoteTy usg@(UsgNote u ) ty)
+ = if co
+ then case u of UsMany -> pty
+ UsVar _ -> pty -- force to UsMany
+ UsOnce -> pprPanic "pessimise:" (ppr ty0)
+ else NoteTy usg pty
+ where pty = pessimiseN co ty
+
+pessimise co ty0 = pessimiseN co ty0 -- assume UsMany
+#else
+pessimise co ty0@(NoteTy usg@(UsgNote u ) ty)
+ = if co
+ then case u of UsMany -> NoteTy usg pty
+ UsVar _ -> NoteTy (UsgNote UsMany) pty
+ UsOnce -> pprPanic "pessimise:" (ppr ty0)
+ else NoteTy usg pty
+ where pty = pessimiseN co ty
+
+pessimise co ty0 = pprPanic "pessimise: missing usage note:" $
+ ppr ty0
+#endif
+
+pessimiseN co ty0@(NoteTy usg@(UsgNote _ ) ty) = pprPanic "pessimiseN: unexpected usage note:" $
+ ppr ty0
+pessimiseN co (NoteTy (SynNote sty) ty) = NoteTy (SynNote (pessimiseN co sty))
+ (pessimiseN co ty )
+pessimiseN co (NoteTy note@(FTVNote _ ) ty) = NoteTy note (pessimiseN co ty)
+pessimiseN co ty0@(TyVarTy _) = ty0
+pessimiseN co ty0@(AppTy _ _) = ty0
+pessimiseN co ty0@(TyConApp tc tys) = ASSERT( not ((isFunTyCon tc) && (length tys > 1)) )
+ ty0
+pessimiseN co (FunTy ty1 ty2) = FunTy (pessimise (not co) ty1)
+ (pessimise co ty2)
+pessimiseN co (ForAllTy tyv ty) = ForAllTy tyv (pessimiseN co ty)
+\end{code}
+
+
+@unAnnotTyM@ strips annotations (that the inference is allowed to
+touch) from a term, and `fixes' those it isn't permitted to touch (by
+putting @Many@ annotations where they are missing, but leaving
+existing annotations in the type).
+
+@unTermUsg@ removes from a term any term usage annotations it finds.
+
+\begin{code}
+unAnnotTyM :: MungeFlags -> Type -> AnnotM a Type
+
+unAnnotTyM mf ty = if hasUsg mf then
+ ASSERT( isSigma mf )
+ return (fixAnnotTy ty)
+ else return (unannotTy ty)
+
+
+unTermUsg :: CoreExpr -> AnnotM a CoreExpr
+-- strip all term annotations
+unTermUsg e@(Lam _ _) = return e
+unTermUsg (Note (TermUsg _) e) = return e
+unTermUsg _ = panic "unTermUsg"
+
+unannotTy :: Type -> Type
+-- strip all annotations
+unannotTy (NoteTy (UsgNote _ ) ty) = unannotTy ty
+unannotTy (NoteTy (SynNote sty) ty) = NoteTy (SynNote (unannotTy sty)) (unannotTy ty)
+unannotTy (NoteTy note@(FTVNote _ ) ty) = NoteTy note (unannotTy ty)
+unannotTy ty@(TyVarTy _) = ty
+unannotTy (AppTy ty1 ty2) = AppTy (unannotTy ty1) (unannotTy ty2)
+unannotTy (TyConApp tc tys) = TyConApp tc (map unannotTy tys)
+unannotTy (FunTy ty1 ty2) = FunTy (unannotTy ty1) (unannotTy ty2)
+unannotTy (ForAllTy tyv ty) = ForAllTy tyv (unannotTy ty)
+
+
+fixAnnotTy :: Type -> Type
+-- put Manys where they are missing
+#ifndef USMANY
+fixAnnotTy = id
+#else
+fixAnnotTy (NoteTy note@(UsgNote _ ) ty) = NoteTy note (fixAnnotTyN ty)
+fixAnnotTy ty0 = NoteTy (UsgNote UsMany) (fixAnnotTyN ty0)
+
+fixAnnotTyN ty0@(NoteTy note@(UsgNote _ ) ty) = pprPanic "fixAnnotTyN: unexpected usage note:" $
+ ppr ty0
+fixAnnotTyN (NoteTy (SynNote sty) ty) = NoteTy (SynNote (fixAnnotTyN sty))
+ (fixAnnotTyN ty )
+fixAnnotTyN (NoteTy note@(FTVNote _ ) ty) = NoteTy note (fixAnnotTyN ty)
+fixAnnotTyN ty0@(TyVarTy _) = ty0
+fixAnnotTyN (AppTy ty1 ty2) = AppTy (fixAnnotTyN ty1) (fixAnnotTyN ty2)
+fixAnnotTyN (TyConApp tc tys) = ASSERT( isFunTyCon tc || isAlgTyCon tc || isPrimTyCon tc || isSynTyCon tc )
+ TyConApp tc (map (if isFunTyCon tc then
+ fixAnnotTy
+ else
+ fixAnnotTyN) tys)
+fixAnnotTyN (FunTy ty1 ty2) = FunTy (fixAnnotTy ty1) (fixAnnotTy ty2)
+fixAnnotTyN (ForAllTy tyv ty) = ForAllTy tyv (fixAnnotTyN ty)
+#endif
+\end{code}
+
+The composition (reannotating a type with fresh uvars but the same
+structure) is useful elsewhere:
+
+\begin{code}
+freshannotTy :: Type -> UniqSMM Type
+freshannotTy = annotTy (Right "freshannotTy") . unannotTy
+\end{code}
+
+
+Wrappers apply these functions to sets of bindings.
+
+\begin{code}
+doAnnotBinds :: UniqSupply
+ -> [CoreBind]
+ -> ([CoreBind],UniqSupply)
+
+doAnnotBinds us binds = initAnnotM us (genAnnotBinds annotTyM annotLam binds)
+
+
+doUnAnnotBinds :: [CoreBind]
+ -> [CoreBind]
+
+doUnAnnotBinds binds = fst $ initAnnotM () $
+ genAnnotBinds unAnnotTyM unTermUsg binds
+\end{code}
+
+======================================================================
+
+Monadic machinery
+~~~~~~~~~~~~~~~~~
+
+The @UniqSM@ type is not an instance of @Monad@, and cannot be made so
+since it is merely a synonym rather than a newtype. Here we define
+@UniqSMM@, which *is* an instance of @Monad@.
+
+\begin{code}
+newtype UniqSMM a = UsToUniqSMM (UniqSM a)
+uniqSMMToUs (UsToUniqSMM us) = us
+usToUniqSMM = UsToUniqSMM
+
+instance Monad UniqSMM where
+ m >>= f = UsToUniqSMM $ uniqSMMToUs m `thenUs` \ a ->
+ uniqSMMToUs (f a)
+ return = UsToUniqSMM . returnUs
+\end{code}
+
+
+For annotation, the monad @AnnotM@, we need to carry around our
+variable mapping, along with some general state.
+
+\begin{code}
+newtype AnnotM flexi a = AnnotM ( flexi -- UniqSupply etc
+ -> VarEnv IdOrTyVar -- unannotated to annotated variables
+ -> (a,flexi,VarEnv IdOrTyVar))
+unAnnotM (AnnotM f) = f
+
+instance Monad (AnnotM flexi) where
+ a >>= f = AnnotM (\ us ve -> let (r,us',ve') = unAnnotM a us ve
+ in unAnnotM (f r) us' ve')
+ return a = AnnotM (\ us ve -> (a,us,ve))
+
+initAnnotM :: fl -> AnnotM fl a -> (a,fl)
+initAnnotM fl m = case (unAnnotM m) fl emptyVarEnv of { (r,fl',_) -> (r,fl') }
+
+withAnnVar :: IdOrTyVar -> IdOrTyVar -> AnnotM fl a -> AnnotM fl a
+withAnnVar v v' m = AnnotM (\ us ve -> let ve' = extendVarEnv ve v v'
+ (r,us',_) = (unAnnotM m) us ve'
+ in (r,us',ve))
+
+withAnnVars :: [IdOrTyVar] -> [IdOrTyVar] -> AnnotM fl a -> AnnotM fl a
+withAnnVars vs vs' m = AnnotM (\ us ve -> let ve' = plusVarEnv ve (zipVarEnv vs vs')
+ (r,us',_) = (unAnnotM m) us ve'
+ in (r,us',ve))
+
+lookupAnnVar :: IdOrTyVar -> AnnotM fl (Maybe IdOrTyVar)
+lookupAnnVar var = AnnotM (\ us ve -> (lookupVarEnv ve var,
+ us,
+ ve))
+\end{code}
+
+A useful helper allows us to turn a computation in the unique supply
+monad into one in the annotation monad parameterised by a unique
+supply.
+
+\begin{code}
+uniqSMtoAnnotM :: UniqSM a -> AnnotM UniqSupply a
+
+uniqSMtoAnnotM m = AnnotM (\ us ve -> let (r,us') = initUs us m
+ in (r,us',ve))
+\end{code}
+
+@newVarUs@ and @newVarUSMM@ generate a new usage variable. They take
+an argument which is used for debugging only, describing what the
+variable is to annotate.
+
+\begin{code}
+newVarUs :: (Either CoreExpr String) -> UniqSM UsageAnn
+-- the first arg is for debugging use only
+newVarUs e = getUniqueUs `thenUs` \ u ->
+ let uv = mkUVar u in
+ returnUs (UsVar uv)
+{- #ifdef DEBUG
+ let src = case e of
+ Left (Con (Literal _) _) -> "literal"
+ Left (Con _ _) -> "primop"
+ Left (Lam v e) -> "lambda: " ++ showSDoc (ppr v)
+ Left _ -> "unknown"
+ Right s -> s
+ in pprTrace "newVarUs:" (ppr uv <+> text src) $
+ #endif
+ -}
+
+newVarUSMM :: (Either CoreExpr String) -> UniqSMM UsageAnn
+newVarUSMM = usToUniqSMM . newVarUs
+\end{code}
+
+======================================================================
+
+PrimOps and usage information.
+
+Analagously to @DataCon.dataConArgTys@, we determine the argtys and
+result ty of a primop, *after* substition (which may reveal more args,
+notably for @CCall@s).
+
+\begin{code}
+primOpUsgTys :: PrimOp -- this primop
+ -> [Type] -- instantiated at these (tau) types
+ -> ([Type],Type) -- requires args of these (sigma) types,
+ -- and returns this (sigma) type
+
+primOpUsgTys p tys = let (tyvs,ty0us,rtyu) = primOpUsg p
+ s = zipVarEnv tyvs tys
+ (ty1us,rty1u) = splitFunTys (substTy s rtyu)
+ -- substitution may reveal more args
+ in ((map (substTy s) ty0us) ++ ty1us,
+ rty1u)
+\end{code}
+
+======================================================================
+
+EOF
projects / ghc-hetmet.git / commitdiff