diff options
| -rw-r--r-- | ghc/compiler/main/CmdLineOpts.lhs | 10 | ||||
| -rw-r--r-- | ghc/compiler/usageSP/UConSet.lhs | 342 | ||||
| -rw-r--r-- | ghc/compiler/usageSP/UsageSPInf.lhs | 545 | ||||
| -rw-r--r-- | ghc/compiler/usageSP/UsageSPLint.lhs | 427 | ||||
| -rw-r--r-- | ghc/compiler/usageSP/UsageSPUtils.lhs | 633 |
5 files changed, 1956 insertions, 1 deletions
diff --git a/ghc/compiler/main/CmdLineOpts.lhs b/ghc/compiler/main/CmdLineOpts.lhs index 711c28dbd6..97a1820287 100644 --- a/ghc/compiler/main/CmdLineOpts.lhs +++ b/ghc/compiler/main/CmdLineOpts.lhs @@ -41,6 +41,7 @@ module CmdLineOpts ( 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, @@ -50,6 +51,7 @@ module CmdLineOpts ( opt_D_verbose_stg2stg, opt_DictsStrict, opt_DoCoreLinting, + opt_DoUSPLinting, opt_DoStgLinting, opt_DoSemiTagging, opt_DoEtaReduction, @@ -58,6 +60,7 @@ module CmdLineOpts ( opt_EnsureSplittableC, opt_FoldrBuildOn, opt_UnboxStrictFields, + opt_UsageSPOn, opt_GlasgowExts, opt_GranMacros, opt_HiMap, @@ -180,6 +183,7 @@ data CoreToDo -- These are diff core-to-core passes, | CoreDoSpecialising | CoreDoFoldrBuildWorkerWrapper | CoreDoFoldrBuildWWAnal + | CoreDoUSPInf | CoreDoCPResult \end{code} @@ -315,6 +319,7 @@ opt_D_dump_stranal = lookUp SLIT("-ddump-stranal") 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") @@ -326,8 +331,10 @@ opt_DictsStrict = lookUp SLIT("-fdicts-strict") 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") @@ -425,7 +432,8 @@ classifyOpts = sep argv [] [] -- accumulators... "-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) diff --git a/ghc/compiler/usageSP/UConSet.lhs b/ghc/compiler/usageSP/UConSet.lhs new file mode 100644 index 0000000000..674bbd8b68 --- /dev/null +++ b/ghc/compiler/usageSP/UConSet.lhs @@ -0,0 +1,342 @@ +% +% (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 diff --git a/ghc/compiler/usageSP/UsageSPInf.lhs b/ghc/compiler/usageSP/UsageSPInf.lhs new file mode 100644 index 0000000000..331c3a39ac --- /dev/null +++ b/ghc/compiler/usageSP/UsageSPInf.lhs @@ -0,0 +1,545 @@ +% +% (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 diff --git a/ghc/compiler/usageSP/UsageSPLint.lhs b/ghc/compiler/usageSP/UsageSPLint.lhs new file mode 100644 index 0000000000..41d71c5ded --- /dev/null +++ b/ghc/compiler/usageSP/UsageSPLint.lhs @@ -0,0 +1,427 @@ +% +% (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 diff --git a/ghc/compiler/usageSP/UsageSPUtils.lhs b/ghc/compiler/usageSP/UsageSPUtils.lhs new file mode 100644 index 0000000000..2ec5ace5dc --- /dev/null +++ b/ghc/compiler/usageSP/UsageSPUtils.lhs @@ -0,0 +1,633 @@ +% +% (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 |