[project @ 2006-01-06 16:30:17 by simonmar]
[ghc-hetmet.git] / ghc / compiler / simplCore / SetLevels.lhs
index ca79733..f8ab29d 100644 (file)
@@ -1,57 +1,81 @@
 %
-% (c) The GRASP/AQUA Project, Glasgow University, 1992-1996
+% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %
 \section{SetLevels}
 
-We attach binding levels to Core bindings, in preparation for floating
-outwards (@FloatOut@).
+               ***************************
+                       Overview
+               ***************************
 
-We also let-ify many applications (notably case scrutinees), so they
-will have a fighting chance of being floated sensible.
+1. We attach binding levels to Core bindings, in preparation for floating
+   outwards (@FloatOut@).
 
-\begin{code}
-#include "HsVersions.h"
+2. We also let-ify many expressions (notably case scrutinees), so they
+   will have a fighting chance of being floated sensible.
+
+3. We clone the binders of any floatable let-binding, so that when it is
+   floated out it will be unique.  (This used to be done by the simplifier
+   but the latter now only ensures that there's no shadowing; indeed, even 
+   that may not be true.)
+
+   NOTE: this can't be done using the uniqAway idea, because the variable
+        must be unique in the whole program, not just its current scope,
+        because two variables in different scopes may float out to the
+        same top level place
+
+   NOTE: Very tiresomely, we must apply this substitution to
+        the rules stored inside a variable too.
 
+   We do *not* clone top-level bindings, because some of them must not change,
+   but we *do* clone bindings that are heading for the top level
+
+4. In the expression
+       case x of wild { p -> ...wild... }
+   we substitute x for wild in the RHS of the case alternatives:
+       case x of wild { p -> ...x... }
+   This means that a sub-expression involving x is not "trapped" inside the RHS.
+   And it's not inconvenient because we already have a substitution.
+
+  Note that this is EXACTLY BACKWARDS from the what the simplifier does.
+  The simplifier tries to get rid of occurrences of x, in favour of wild,
+  in the hope that there will only be one remaining occurrence of x, namely
+  the scrutinee of the case, and we can inline it.  
+
+\begin{code}
 module SetLevels (
-       setLevels,
+       setLevels, 
 
        Level(..), tOP_LEVEL,
+       LevelledBind, LevelledExpr,
 
-       incMinorLvl, ltMajLvl, ltLvl, isTopLvl
--- not exported: , incMajorLvl, isTopMajLvl, unTopify
+       incMinorLvl, ltMajLvl, ltLvl, isTopLvl, isInlineCtxt
     ) where
 
-IMP_Ubiq(){-uitous-}
+#include "HsVersions.h"
 
-import AnnCoreSyn
 import CoreSyn
 
-import CoreUtils       ( coreExprType )
-import CoreUnfold      ( whnfOrBottom )
-import FreeVars                -- all of it
-import Id              ( idType, mkSysLocal, toplevelishId,
-                         nullIdEnv, addOneToIdEnv, growIdEnvList,
-                         unionManyIdSets, minusIdSet, mkIdSet,
-                         idSetToList,
-                         lookupIdEnv, SYN_IE(IdEnv)
-                       )
-import Pretty          ( ppStr, ppBesides, ppChar, ppInt )
-import SrcLoc          ( mkUnknownSrcLoc )
-import Type            ( isPrimType, mkTyVarTys, mkForAllTys )
-import TyVar           ( nullTyVarEnv, addOneToTyVarEnv,
-                         growTyVarEnvList, lookupTyVarEnv,
-                         tyVarSetToList,
-                         SYN_IE(TyVarEnv),
-                         unionManyTyVarSets
-                       )
-import UniqSupply      ( thenUs, returnUs, mapUs, mapAndUnzipUs,
-                         mapAndUnzip3Us, getUnique, SYN_IE(UniqSM),
-                         UniqSupply
+import DynFlags        ( FloatOutSwitches(..) )
+import CoreUtils       ( exprType, exprIsTrivial, exprIsCheap, mkPiTypes )
+import CoreFVs         -- all of it
+import CoreSubst       ( Subst, emptySubst, extendInScope, extendIdSubst,
+                         cloneIdBndr, cloneRecIdBndrs )
+import Id              ( Id, idType, mkSysLocal, isOneShotLambda,
+                         zapDemandIdInfo,
+                         idSpecialisation, idWorkerInfo, setIdInfo
                        )
-import Usage           ( SYN_IE(UVar) )
-import Util            ( mapAccumL, zipWithEqual, zipEqual, panic, assertPanic )
-
-isLeakFreeType x y = False -- safe option; ToDo
+import IdInfo          ( workerExists, vanillaIdInfo, isEmptySpecInfo )
+import Var             ( Var )
+import VarSet
+import VarEnv
+import Name            ( getOccName )
+import OccName         ( occNameString )
+import Type            ( isUnLiftedType, Type )
+import BasicTypes      ( TopLevelFlag(..) )
+import UniqSupply
+import Util            ( sortLe, isSingleton, count )
+import Outputable
+import FastString
 \end{code}
 
 %************************************************************************
@@ -61,18 +85,20 @@ isLeakFreeType x y = False -- safe option; ToDo
 %************************************************************************
 
 \begin{code}
-data Level
-  = Top                -- Means *really* the top level.
-  | Level   Int        -- Level number of enclosing lambdas
-           Int -- Number of big-lambda and/or case expressions between
-               -- here and the nearest enclosing lambda
+data Level = InlineCtxt        -- A level that's used only for
+                       -- the context parameter ctxt_lvl
+          | Level Int  -- Level number of enclosing lambdas
+                  Int  -- Number of big-lambda and/or case expressions between
+                       -- here and the nearest enclosing lambda
 \end{code}
 
 The {\em level number} on a (type-)lambda-bound variable is the
-nesting depth of the (type-)lambda which binds it.  On an expression,
-it's the maximum level number of its free (type-)variables.  On a
-let(rec)-bound variable, it's the level of its RHS.  On a case-bound
-variable, it's the number of enclosing lambdas.
+nesting depth of the (type-)lambda which binds it.  The outermost lambda
+has level 1, so (Level 0 0) means that the variable is bound outside any lambda.
+
+On an expression, it's the maximum level number of its free
+(type-)variables.  On a let(rec)-bound variable, it's the level of its
+RHS.  On a case-bound variable, it's the number of enclosing lambdas.
 
 Top-level variables: level~0.  Those bound on the RHS of a top-level
 definition but ``before'' a lambda; e.g., the \tr{x} in (levels shown
@@ -82,71 +108,99 @@ a_0 = let  b_? = ...  in
           x_1 = ... b ... in ...
 \end{verbatim}
 
-Level 0 0 will make something get floated to a top-level "equals",
-@Top@ makes it go right to the top.
-
 The main function @lvlExpr@ carries a ``context level'' (@ctxt_lvl@).
 That's meant to be the level number of the enclosing binder in the
 final (floated) program.  If the level number of a sub-expression is
 less than that of the context, then it might be worth let-binding the
-sub-expression so that it will indeed float. This context level starts
-at @Level 0 0@; it is never @Top@.
+sub-expression so that it will indeed float.  
 
-\begin{code}
-type LevelledExpr  = GenCoreExpr    (Id, Level) Id TyVar UVar
-type LevelledArg   = GenCoreArg                        Id TyVar UVar
-type LevelledBind  = GenCoreBinding (Id, Level) Id TyVar UVar
+If you can float to level @Level 0 0@ worth doing so because then your
+allocation becomes static instead of dynamic.  We always start with
+context @Level 0 0@.  
+
+
+InlineCtxt
+~~~~~~~~~~
+@InlineCtxt@ very similar to @Level 0 0@, but is used for one purpose:
+to say "don't float anything out of here".  That's exactly what we
+want for the body of an INLINE, where we don't want to float anything
+out at all.  See notes with lvlMFE below.
 
-type LevelEnvs = (IdEnv    Level, -- bind Ids to levels
-                 TyVarEnv Level) -- bind type variables to levels
+But, check this out:
 
-tOP_LEVEL = Top
+-- At one time I tried the effect of not float anything out of an InlineMe,
+-- but it sometimes works badly.  For example, consider PrelArr.done.  It
+-- has the form        __inline (\d. e)
+-- where e doesn't mention d.  If we float this to 
+--     __inline (let x = e in \d. x)
+-- things are bad.  The inliner doesn't even inline it because it doesn't look
+-- like a head-normal form.  So it seems a lesser evil to let things float.
+-- In SetLevels we do set the context to (Level 0 0) when we get to an InlineMe
+-- which discourages floating out.
+
+So the conclusion is: don't do any floating at all inside an InlineMe.
+(In the above example, don't float the {x=e} out of the \d.)
+
+One particular case is that of workers: we don't want to float the
+call to the worker outside the wrapper, otherwise the worker might get
+inlined into the floated expression, and an importing module won't see
+the worker at all.
+
+\begin{code}
+type LevelledExpr  = TaggedExpr Level
+type LevelledBind  = TaggedBind Level
+
+tOP_LEVEL   = Level 0 0
+iNLINE_CTXT = InlineCtxt
 
 incMajorLvl :: Level -> Level
-incMajorLvl Top                        = Level 1 0
+-- For InlineCtxt we ignore any inc's; we don't want
+-- to do any floating at all; see notes above
+incMajorLvl InlineCtxt         = InlineCtxt
 incMajorLvl (Level major minor) = Level (major+1) 0
 
 incMinorLvl :: Level -> Level
-incMinorLvl Top                        = Level 0 1
+incMinorLvl InlineCtxt         = InlineCtxt
 incMinorLvl (Level major minor) = Level major (minor+1)
 
 maxLvl :: Level -> Level -> Level
-maxLvl Top l2 = l2
-maxLvl l1 Top = l1
+maxLvl InlineCtxt l2  = l2
+maxLvl l1  InlineCtxt = l1
 maxLvl l1@(Level maj1 min1) l2@(Level maj2 min2)
   | (maj1 > maj2) || (maj1 == maj2 && min1 > min2) = l1
   | otherwise                                     = l2
 
 ltLvl :: Level -> Level -> Bool
-ltLvl l1               Top               = False
-ltLvl Top              (Level _ _)       = True
+ltLvl any_lvl   InlineCtxt  = False
+ltLvl InlineCtxt (Level _ _) = True
 ltLvl (Level maj1 min1) (Level maj2 min2)
   = (maj1 < maj2) || (maj1 == maj2 && min1 < min2)
 
 ltMajLvl :: Level -> Level -> Bool
     -- Tells if one level belongs to a difft *lambda* level to another
-ltMajLvl l1            Top            = False
-ltMajLvl Top           (Level 0 _)    = False
-ltMajLvl Top           (Level _ _)    = True
+ltMajLvl any_lvl       InlineCtxt     = False
+ltMajLvl InlineCtxt    (Level maj2 _) = 0 < maj2
 ltMajLvl (Level maj1 _) (Level maj2 _) = maj1 < maj2
 
 isTopLvl :: Level -> Bool
-isTopLvl Top   = True
-isTopLvl other = False
+isTopLvl (Level 0 0) = True
+isTopLvl other      = False
 
-isTopMajLvl :: Level -> Bool -- Tells if it's the top *lambda* level
-isTopMajLvl Top                  = True
-isTopMajLvl (Level maj _) = maj == 0
-
-unTopify :: Level -> Level
-unTopify Top = Level 0 0
-unTopify lvl = lvl
+isInlineCtxt :: Level -> Bool
+isInlineCtxt InlineCtxt = True
+isInlineCtxt other     = False
 
 instance Outputable Level where
-  ppr sty Top            = ppStr "<Top>"
-  ppr sty (Level maj min) = ppBesides [ ppChar '<', ppInt maj, ppChar ',', ppInt min, ppChar '>' ]
+  ppr InlineCtxt      = text "<INLINE>"
+  ppr (Level maj min) = hcat [ char '<', int maj, char ',', int min, char '>' ]
+
+instance Eq Level where
+  InlineCtxt       == InlineCtxt        = True
+  (Level maj1 min1) == (Level maj2 min2) = maj1==maj2 && min1==min2
+  l1               == l2                = False
 \end{code}
 
+
 %************************************************************************
 %*                                                                     *
 \subsection{Main level-setting code}
@@ -154,71 +208,33 @@ instance Outputable Level where
 %************************************************************************
 
 \begin{code}
-setLevels :: [CoreBinding]
+setLevels :: FloatOutSwitches
+         -> [CoreBind]
          -> UniqSupply
          -> [LevelledBind]
 
-setLevels binds us
-  = do_them binds us
+setLevels float_lams binds us
+  = initLvl us (do_them binds)
   where
     -- "do_them"'s main business is to thread the monad along
     -- It gives each top binding the same empty envt, because
     -- things unbound in the envt have level number zero implicitly
-    do_them :: [CoreBinding] -> LvlM [LevelledBind]
+    do_them :: [CoreBind] -> LvlM [LevelledBind]
 
     do_them [] = returnLvl []
     do_them (b:bs)
-      = lvlTopBind b   `thenLvl` \ (lvld_bind, _) ->
-       do_them bs       `thenLvl` \ lvld_binds ->
-       returnLvl (lvld_bind ++ lvld_binds)
+      = lvlTopBind init_env b  `thenLvl` \ (lvld_bind, _) ->
+       do_them bs              `thenLvl` \ lvld_binds ->
+       returnLvl (lvld_bind : lvld_binds)
 
-initial_envs = (nullIdEnv, nullTyVarEnv)
+    init_env = initialEnv float_lams
 
-lvlTopBind (NonRec binder rhs)
-  = lvlBind (Level 0 0) initial_envs (AnnNonRec binder (freeVars rhs))
+lvlTopBind env (NonRec binder rhs)
+  = lvlBind TopLevel tOP_LEVEL env (AnnNonRec binder (freeVars rhs))
                                        -- Rhs can have no free vars!
 
-lvlTopBind (Rec pairs)
-  = lvlBind (Level 0 0) initial_envs (AnnRec [(b,freeVars rhs) | (b,rhs) <- pairs])
-\end{code}
-
-%************************************************************************
-%*                                                                     *
-\subsection{Bindings}
-%*                                                                     *
-%************************************************************************
-
-The binding stuff works for top level too.
-
-\begin{code}
-type CoreBindingWithFVs = AnnCoreBinding Id Id TyVar UVar FVInfo
-
-lvlBind :: Level
-       -> LevelEnvs
-       -> CoreBindingWithFVs
-       -> LvlM ([LevelledBind], LevelEnvs)
-
-lvlBind ctxt_lvl envs@(venv, tenv) (AnnNonRec name rhs)
-  = setFloatLevel True {- Already let-bound -}
-       ctxt_lvl envs rhs ty    `thenLvl` \ (final_lvl, rhs') ->
-    let
-       new_envs = (addOneToIdEnv venv name final_lvl, tenv)
-    in
-    returnLvl ([NonRec (name, final_lvl) rhs'], new_envs)
-  where
-    ty = idType name
-
-
-lvlBind ctxt_lvl envs@(venv, tenv) (AnnRec pairs)
-  = decideRecFloatLevel ctxt_lvl envs binders rhss
-                               `thenLvl` \ (final_lvl, extra_binds, rhss') ->
-    let
-       binders_w_lvls = binders `zip` repeat final_lvl
-       new_envs       = (growIdEnvList venv binders_w_lvls, tenv)
-    in
-    returnLvl (extra_binds ++ [Rec (zipEqual "lvlBind" binders_w_lvls rhss')], new_envs)
-  where
-    (binders,rhss) = unzip pairs
+lvlTopBind env (Rec pairs)
+  = lvlBind TopLevel tOP_LEVEL env (AnnRec [(b,freeVars rhs) | (b,rhs) <- pairs])
 \end{code}
 
 %************************************************************************
@@ -229,15 +245,13 @@ lvlBind ctxt_lvl envs@(venv, tenv) (AnnRec pairs)
 
 \begin{code}
 lvlExpr :: Level               -- ctxt_lvl: Level of enclosing expression
-       -> LevelEnvs            -- Level of in-scope names/tyvars
+       -> LevelEnv             -- Level of in-scope names/tyvars
        -> CoreExprWithFVs      -- input expression
        -> LvlM LevelledExpr    -- Result expression
 \end{code}
 
 The @ctxt_lvl@ is, roughly, the level of the innermost enclosing
-binder.
-
-Here's an example
+binder.  Here's an example
 
        v = \x -> ...\y -> let r = case (..x..) of
                                        ..x..
@@ -252,493 +266,582 @@ don't want @lvlExpr@ to turn the scrutinee of the @case@ into an MFE
 If there were another lambda in @r@'s rhs, it would get level-2 as well.
 
 \begin{code}
-lvlExpr _ _ (_, AnnVar v)       = returnLvl (Var v)
-lvlExpr _ _ (_, AnnLit l)       = returnLvl (Lit l)
-lvlExpr _ _ (_, AnnCon con args) = returnLvl (Con con args)
-lvlExpr _ _ (_, AnnPrim op args) = returnLvl (Prim op args)
-
-lvlExpr ctxt_lvl envs@(venv, tenv) (_, AnnApp fun arg)
-  = lvlExpr ctxt_lvl envs fun          `thenLvl` \ fun' ->
-    returnLvl (App fun' arg)
-
-lvlExpr ctxt_lvl envs (_, AnnSCC cc expr)
-  = lvlExpr ctxt_lvl envs expr                 `thenLvl` \ expr' ->
-    returnLvl (SCC cc expr')
-
-lvlExpr ctxt_lvl envs (_, AnnCoerce c ty expr)
-  = lvlExpr ctxt_lvl envs expr                 `thenLvl` \ expr' ->
-    returnLvl (Coerce c ty expr')
-
-lvlExpr ctxt_lvl envs@(venv, tenv) (_, AnnLam (ValBinder arg) rhs)
-  = lvlMFE incd_lvl (new_venv, tenv) rhs `thenLvl` \ rhs' ->
-    returnLvl (Lam (ValBinder (arg,incd_lvl)) rhs')
+lvlExpr _ _ (_, AnnType ty)   = returnLvl (Type ty)
+lvlExpr _ env (_, AnnVar v)   = returnLvl (lookupVar env v)
+lvlExpr _ env (_, AnnLit lit) = returnLvl (Lit lit)
+
+lvlExpr ctxt_lvl env (_, AnnApp fun arg)
+  = lvl_fun fun                                `thenLvl` \ fun' ->
+    lvlMFE  False ctxt_lvl env arg     `thenLvl` \ arg' ->
+    returnLvl (App fun' arg')
+  where
+-- gaw 2004
+    lvl_fun (_, AnnCase _ _ _ _) = lvlMFE True ctxt_lvl env fun
+    lvl_fun other             = lvlExpr ctxt_lvl env fun
+       -- We don't do MFE on partial applications generally,
+       -- but we do if the function is big and hairy, like a case
+
+lvlExpr ctxt_lvl env (_, AnnNote InlineMe expr)
+-- Don't float anything out of an InlineMe; hence the iNLINE_CTXT
+  = lvlExpr iNLINE_CTXT env expr       `thenLvl` \ expr' ->
+    returnLvl (Note InlineMe expr')
+
+lvlExpr ctxt_lvl env (_, AnnNote note expr)
+  = lvlExpr ctxt_lvl env expr          `thenLvl` \ expr' ->
+    returnLvl (Note note expr')
+
+-- We don't split adjacent lambdas.  That is, given
+--     \x y -> (x+1,y)
+-- we don't float to give 
+--     \x -> let v = x+y in \y -> (v,y)
+-- Why not?  Because partial applications are fairly rare, and splitting
+-- lambdas makes them more expensive.
+
+lvlExpr ctxt_lvl env expr@(_, AnnLam bndr rhs)
+  = lvlMFE True new_lvl new_env body   `thenLvl` \ new_body ->
+    returnLvl (mkLams new_bndrs new_body)
+  where 
+    (bndrs, body)       = collectAnnBndrs expr
+    (new_lvl, new_bndrs) = lvlLamBndrs ctxt_lvl bndrs
+    new_env             = extendLvlEnv env new_bndrs
+       -- At one time we called a special verion of collectBinders,
+       -- which ignored coercions, because we don't want to split
+       -- a lambda like this (\x -> coerce t (\s -> ...))
+       -- This used to happen quite a bit in state-transformer programs,
+       -- but not nearly so much now non-recursive newtypes are transparent.
+       -- [See SetLevels rev 1.50 for a version with this approach.]
+
+lvlExpr ctxt_lvl env (_, AnnLet (AnnNonRec bndr rhs) body)
+  | isUnLiftedType (idType bndr)
+       -- Treat unlifted let-bindings (let x = b in e) just like (case b of x -> e)
+       -- That is, leave it exactly where it is
+       -- We used to float unlifted bindings too (e.g. to get a cheap primop
+       -- outside a lambda (to see how, look at lvlBind in rev 1.58)
+       -- but an unrelated change meant that these unlifed bindings
+       -- could get to the top level which is bad.  And there's not much point;
+       -- unlifted bindings are always cheap, and so hardly worth floating.
+  = lvlExpr ctxt_lvl env rhs           `thenLvl` \ rhs' ->
+    lvlExpr incd_lvl env' body         `thenLvl` \ body' ->
+    returnLvl (Let (NonRec bndr' rhs') body')
   where
-    incd_lvl = incMajorLvl ctxt_lvl
-    new_venv = growIdEnvList venv [(arg,incd_lvl)]
+    incd_lvl = incMinorLvl ctxt_lvl
+    bndr' = TB bndr incd_lvl
+    env'  = extendLvlEnv env [bndr']
 
-lvlExpr ctxt_lvl (venv, tenv) (_, AnnLam (TyBinder tyvar) e)
-  = lvlExpr incd_lvl (venv, new_tenv) e        `thenLvl` \ e' ->
-    returnLvl (Lam (TyBinder tyvar) e')
+lvlExpr ctxt_lvl env (_, AnnLet bind body)
+  = lvlBind NotTopLevel ctxt_lvl env bind      `thenLvl` \ (bind', new_env) ->
+    lvlExpr ctxt_lvl new_env body              `thenLvl` \ body' ->
+    returnLvl (Let bind' body')
+
+lvlExpr ctxt_lvl env (_, AnnCase expr case_bndr ty alts)
+  = lvlMFE True ctxt_lvl env expr      `thenLvl` \ expr' ->
+    let
+       alts_env = extendCaseBndrLvlEnv env expr' case_bndr incd_lvl
+    in
+    mapLvl (lvl_alt alts_env) alts     `thenLvl` \ alts' ->
+    returnLvl (Case expr' (TB case_bndr incd_lvl) ty alts')
   where
-    incd_lvl   = incMinorLvl ctxt_lvl
-    new_tenv   = addOneToTyVarEnv tenv tyvar incd_lvl
-
-lvlExpr ctxt_lvl (venv, tenv) (_, AnnLam (UsageBinder u) e)
-  = panic "SetLevels.lvlExpr:AnnLam UsageBinder"
-
-lvlExpr ctxt_lvl envs (_, AnnLet bind body)
-  = lvlBind ctxt_lvl envs bind         `thenLvl` \ (binds', new_envs) ->
-    lvlExpr ctxt_lvl new_envs body     `thenLvl` \ body' ->
-    returnLvl (foldr Let body' binds') -- mkCoLet* requires Core...
-
-lvlExpr ctxt_lvl envs@(venv, tenv) (_, AnnCase expr alts)
-  = lvlMFE ctxt_lvl envs expr  `thenLvl` \ expr' ->
-    lvl_alts alts              `thenLvl` \ alts' ->
-    returnLvl (Case expr' alts')
-    where
-      expr_type = coreExprType (deAnnotate expr)
       incd_lvl  = incMinorLvl ctxt_lvl
 
-      lvl_alts (AnnAlgAlts alts deflt)
-       = mapLvl lvl_alt alts   `thenLvl` \ alts' ->
-         lvl_deflt deflt       `thenLvl` \ deflt' ->
-         returnLvl (AlgAlts alts' deflt')
-       where
-         lvl_alt (con, bs, e)
-           = let
-                 bs'  = [ (b, incd_lvl) | b <- bs ]
-                 new_envs = (growIdEnvList venv bs', tenv)
-             in
-             lvlMFE incd_lvl new_envs e        `thenLvl` \ e' ->
-             returnLvl (con, bs', e')
-
-      lvl_alts (AnnPrimAlts alts deflt)
-       = mapLvl lvl_alt alts   `thenLvl` \ alts' ->
-         lvl_deflt deflt       `thenLvl` \ deflt' ->
-         returnLvl (PrimAlts alts' deflt')
+      lvl_alt alts_env (con, bs, rhs)
+       = lvlMFE True incd_lvl new_env rhs      `thenLvl` \ rhs' ->
+         returnLvl (con, bs', rhs')
        where
-         lvl_alt (lit, e)
-           = lvlMFE incd_lvl envs e `thenLvl` \ e' ->
-             returnLvl (lit, e')
-
-      lvl_deflt AnnNoDefault = returnLvl NoDefault
-
-      lvl_deflt (AnnBindDefault b expr)
-       = let
-             new_envs = (addOneToIdEnv venv b incd_lvl, tenv)
-         in
-         lvlMFE incd_lvl new_envs expr `thenLvl` \ expr' ->
-         returnLvl (BindDefault (b, incd_lvl) expr')
+         bs'     = [ TB b incd_lvl | b <- bs ]
+         new_env = extendLvlEnv alts_env bs'
 \end{code}
 
 @lvlMFE@ is just like @lvlExpr@, except that it might let-bind
 the expression, so that it can itself be floated.
 
+[NOTE: unlifted MFEs]
+We don't float unlifted MFEs, which potentially loses big opportunites.
+For example:
+       \x -> f (h y)
+where h :: Int -> Int# is expensive. We'd like to float the (h y) outside
+the \x, but we don't because it's unboxed.  Possible solution: box it.
+
 \begin{code}
-lvlMFE ::  Level               -- Level of innermost enclosing lambda/tylam
-       -> LevelEnvs            -- Level of in-scope names/tyvars
+lvlMFE ::  Bool                        -- True <=> strict context [body of case or let]
+       -> Level                -- Level of innermost enclosing lambda/tylam
+       -> LevelEnv             -- Level of in-scope names/tyvars
        -> CoreExprWithFVs      -- input expression
        -> LvlM LevelledExpr    -- Result expression
 
-lvlMFE ctxt_lvl envs@(venv,_) ann_expr
-  | isPrimType ty      -- Can't let-bind it
-  = lvlExpr ctxt_lvl envs ann_expr
+lvlMFE strict_ctxt ctxt_lvl env (_, AnnType ty)
+  = returnLvl (Type ty)
+
+
+lvlMFE strict_ctxt ctxt_lvl env ann_expr@(fvs, _)
+  |  isUnLiftedType ty                 -- Can't let-bind it; see [NOTE: unlifted MFEs]
+  || isInlineCtxt ctxt_lvl             -- Don't float out of an __inline__ context
+  || exprIsTrivial expr                        -- Never float if it's trivial
+  || not good_destination
+  =    -- Don't float it out
+    lvlExpr ctxt_lvl env ann_expr
 
-  | otherwise          -- Not primitive type so could be let-bound
-  = setFloatLevel False {- Not already let-bound -}
-       ctxt_lvl envs ann_expr ty       `thenLvl` \ (final_lvl, expr') ->
-    returnLvl expr'
+  | otherwise  -- Float it out!
+  = lvlFloatRhs abs_vars dest_lvl env ann_expr `thenLvl` \ expr' ->
+    newLvlVar "lvl" abs_vars ty                        `thenLvl` \ var ->
+    returnLvl (Let (NonRec (TB var dest_lvl) expr') 
+                  (mkVarApps (Var var) abs_vars))
   where
-    ty = coreExprType (deAnnotate ann_expr)
+    expr     = deAnnotate ann_expr
+    ty       = exprType expr
+    dest_lvl = destLevel env fvs (isFunction ann_expr)
+    abs_vars = abstractVars dest_lvl env fvs
+
+       -- A decision to float entails let-binding this thing, and we only do 
+       -- that if we'll escape a value lambda, or will go to the top level.
+    good_destination 
+       | dest_lvl `ltMajLvl` ctxt_lvl          -- Escapes a value lambda
+       = not (exprIsCheap expr) || isTopLvl dest_lvl
+         -- Even if it escapes a value lambda, we only
+         -- float if it's not cheap (unless it'll get all the
+         -- way to the top).  I've seen cases where we
+         -- float dozens of tiny free expressions, which cost
+         -- more to allocate than to evaluate.
+         -- NB: exprIsCheap is also true of bottom expressions, which
+         --     is good; we don't want to share them
+         --
+         -- It's only Really Bad to float a cheap expression out of a
+         -- strict context, because that builds a thunk that otherwise
+         -- would never be built.  So another alternative would be to
+         -- add 
+         --    || (strict_ctxt && not (exprIsBottom expr))
+         -- to the condition above. We should really try this out.
+
+       | otherwise             -- Does not escape a value lambda
+       = isTopLvl dest_lvl     -- Only float if we are going to the top level
+       && floatConsts env      --   and the floatConsts flag is on
+       && not strict_ctxt      -- Don't float from a strict context    
+         -- We are keen to float something to the top level, even if it does not
+         -- escape a lambda, because then it needs no allocation.  But it's controlled
+         -- by a flag, because doing this too early loses opportunities for RULES
+         -- which (needless to say) are important in some nofib programs
+         -- (gcd is an example).
+         --
+         -- Beware:
+         --    concat = /\ a -> foldr ..a.. (++) []
+         -- was getting turned into
+         --    concat = /\ a -> lvl a
+         --    lvl    = /\ a -> foldr ..a.. (++) []
+         -- which is pretty stupid.  Hence the strict_ctxt test
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
-\subsection{Deciding floatability}
+\subsection{Bindings}
 %*                                                                     *
 %************************************************************************
 
-@setFloatLevel@ is used for let-bound right-hand-sides, or for MFEs which
-are being created as let-bindings
-
-Decision tree:
-Let Bound?
-  YES. -> (a) try abstracting type variables.
-       If we abstract type variables it will go further, that is, past more
-       lambdas. same as asking if the level number given by the free
-       variables is less than the level number given by free variables
-       and type variables together.
-       Abstract offending type variables, e.g.
-       change f ty a b
-       to let v = /\ty' -> f ty' a b
-         in v ty
-       so that v' is not stopped by the level number of ty
-       tag the original let with its level number
-       (from its variables and type variables)
-  NO.  is a WHNF?
-        YES. -> No point in let binding to float a WHNF.
-                Pin (leave) expression here.
-        NO. -> Will float past a lambda?
-               (check using free variables only, not type variables)
-                 YES. -> do the same as (a) above.
-                 NO. -> No point in let binding if it is not going anywhere
-                        Pin (leave) expression here.
+The binding stuff works for top level too.
 
 \begin{code}
-setFloatLevel :: Bool                  -- True <=> the expression is already let-bound
-                                       -- False <=> it's a possible MFE
-             -> Level                  -- of context
-             -> LevelEnvs
-
-             -> CoreExprWithFVs        -- Original rhs
-             -> Type           -- Type of rhs
-
-             -> LvlM (Level,           -- Level to attribute to this let-binding
-                      LevelledExpr)    -- Final rhs
-
-setFloatLevel alreadyLetBound ctxt_lvl envs@(venv, tenv)
-             expr@(FVInfo fvs tfvs might_leak, _) ty
--- Invariant: ctxt_lvl is never = Top
--- Beautiful ASSERT, dudes (WDP 95/04)...
-
--- Now deal with (by not floating) trivial non-let-bound expressions
--- which just aren't worth let-binding in order to float.  We always
--- choose to float even trivial let-bound things because it doesn't do
--- any harm, and not floating it may pin something important.  For
--- example
---
---     x = let v = []
---             w = 1:v
---         in ...
---
--- Here, if we don't float v we won't float w, which is Bad News.
--- If this gives any problems we could restrict the idea to things destined
--- for top level.
-
-  | not alreadyLetBound
-    && (manifestly_whnf || not will_float_past_lambda)
-  =   -- Pin whnf non-let-bound expressions,
-      -- or ones which aren't going anywhere useful
-    lvlExpr ctxt_lvl envs expr        `thenLvl` \ expr' ->
-    returnLvl (ctxt_lvl, expr')
-
-  | alreadyLetBound && not worth_type_abstraction
-  =   -- Process the expression with a new ctxt_lvl, obtained from
-      -- the free vars of the expression itself
-    lvlExpr (unTopify expr_lvl) envs expr `thenLvl` \ expr' ->
-    returnLvl (maybe_unTopify expr_lvl, expr')
-
-  | otherwise -- This will create a let anyway, even if there is no
-             -- type variable to abstract, so we try to abstract anyway
-  = abstractWrtTyVars offending_tyvars ty envs lvl_after_ty_abstr expr
-                                             `thenLvl` \ final_expr ->
-    returnLvl (expr_lvl, final_expr)
-      -- OLD LIE: The body of the let, just a type application, isn't worth floating
-      --          so pin it with ctxt_lvl
-      -- The truth: better to give it expr_lvl in case it is pinning
-      -- something non-trivial which depends on it.
-  where
-    fv_list = idSetToList    fvs
-    tv_list = tyVarSetToList tfvs
-    expr_lvl = ids_only_lvl `maxLvl` tyvars_only_lvl
-    ids_only_lvl    = foldr (maxLvl . idLevel venv)    tOP_LEVEL fv_list
-    tyvars_only_lvl = foldr (maxLvl . tyvarLevel tenv) tOP_LEVEL tv_list
-    lvl_after_ty_abstr = ids_only_lvl --`maxLvl` non_offending_tyvars_lvl
-
-    will_float_past_lambda =   -- Will escape lambda if let-bound
-                           ids_only_lvl `ltMajLvl` ctxt_lvl
-
-    worth_type_abstraction = -- Will escape (more) lambda(s)/type lambda(s)
-                            -- if type abstracted
-      (ids_only_lvl `ltLvl` tyvars_only_lvl)
-      && not (is_trivial de_ann_expr) -- avoids abstracting trivial type applications
-
-    de_ann_expr = deAnnotate expr
-
-    is_trivial (App e a)
-      | notValArg a    = is_trivial e
-    is_trivial (Var _)  = True
-    is_trivial _        = False
-
-    offending_tyvars = filter offending tv_list
-    --non_offending_tyvars = filter (not . offending) tv_list
-    --non_offending_tyvars_lvl = foldr (maxLvl . tyvarLevel tenv) tOP_LEVEL non_offending_tyvars
-
-    offending tyvar = ids_only_lvl `ltLvl` tyvarLevel tenv tyvar
-
-    manifestly_whnf = whnfOrBottom de_ann_expr
-
-    maybe_unTopify Top | not (canFloatToTop (ty, expr)) = Level 0 0
-    maybe_unTopify lvl                                  = lvl
-       {- ToDo [Andre]: the line above (maybe) should be Level 1 0,
-       -- so that the let will not go past the *last* lambda if it can
-       -- generate a space leak. If it is already in major level 0
-       -- It won't do any harm to give it a Level 1 0.
-       -- we should do the same test not only for things with level Top,
-       -- but also for anything that gets a major level 0.
-          the problem is that
-          f = \a -> let x = [1..1000]
-                    in zip a x
-          ==>
-          f = let x = [1..1000]
-              in \a -> zip a x
-          is just as bad as floating x to the top level.
-          Notice it would be OK in cases like
-          f = \a -> let x = [1..1000]
-                        y = length x
-                    in a + y
-          ==>
-          f = let x = [1..1000]
-                  y = length x
-              in \a -> a + y
-          as x will be gc'd after y is updated.
-          [We did not hit any problems with the above (Level 0 0) code
-           in nofib benchmark]
-       -}
-\end{code}
-
-Abstract wrt tyvars, by making it just as if we had seen
+lvlBind :: TopLevelFlag                -- Used solely to decide whether to clone
+       -> Level                -- Context level; might be Top even for bindings nested in the RHS
+                               -- of a top level binding
+       -> LevelEnv
+       -> CoreBindWithFVs
+       -> LvlM (LevelledBind, LevelEnv)
+
+lvlBind top_lvl ctxt_lvl env (AnnNonRec bndr rhs@(rhs_fvs,_))
+  | isInlineCtxt ctxt_lvl              -- Don't do anything inside InlineMe
+  = lvlExpr ctxt_lvl env rhs                   `thenLvl` \ rhs' ->
+    returnLvl (NonRec (TB bndr ctxt_lvl) rhs', env)
+
+  | null abs_vars
+  =    -- No type abstraction; clone existing binder
+    lvlExpr dest_lvl env rhs                   `thenLvl` \ rhs' ->
+    cloneVar top_lvl env bndr ctxt_lvl dest_lvl        `thenLvl` \ (env', bndr') ->
+    returnLvl (NonRec (TB bndr' dest_lvl) rhs', env') 
 
-     let v = /\a1..an. E
-     in v a1 ... an
-
-instead of simply E. The idea is that v can be freely floated, since it
-has no free type variables. Of course, if E has no free type
-variables, then we just return E.
+  | otherwise
+  = -- Yes, type abstraction; create a new binder, extend substitution, etc
+    lvlFloatRhs abs_vars dest_lvl env rhs      `thenLvl` \ rhs' ->
+    newPolyBndrs dest_lvl env abs_vars [bndr]  `thenLvl` \ (env', [bndr']) ->
+    returnLvl (NonRec (TB bndr' dest_lvl) rhs', env')
 
-\begin{code}
-abstractWrtTyVars offending_tyvars ty (venv,tenv) lvl expr
-  = lvlExpr incd_lvl new_envs expr     `thenLvl` \ expr' ->
-    newLvlVar poly_ty                  `thenLvl` \ poly_var ->
-    let
-       poly_var_rhs     = mkTyLam offending_tyvars expr'
-       poly_var_binding = NonRec (poly_var, lvl) poly_var_rhs
-       poly_var_app     = mkTyApp (Var poly_var) (mkTyVarTys offending_tyvars)
-       final_expr       = Let poly_var_binding poly_var_app -- mkCoLet* requires Core
-    in
-    returnLvl final_expr
   where
-    poly_ty = mkForAllTys offending_tyvars ty
-
-       -- These defns are just like those in the TyLam case of lvlExpr
-    (incd_lvl, tyvar_lvls) = mapAccumL next (unTopify lvl) offending_tyvars
-
-    next lvl tyvar = (lvl1, (tyvar,lvl1))
-                    where lvl1 = incMinorLvl lvl
-
-    new_tenv = growTyVarEnvList tenv tyvar_lvls
-    new_envs = (venv, new_tenv)
+    bind_fvs = rhs_fvs `unionVarSet` idFreeVars bndr
+    abs_vars = abstractVars dest_lvl env bind_fvs
+    dest_lvl = destLevel env bind_fvs (isFunction rhs)
 \end{code}
 
-Recursive definitions.  We want to transform
-
-       letrec
-          x1 = e1
-          ...
-          xn = en
-       in
-       body
-
-to
-
-       letrec
-          x1' = /\ ab -> let D' in e1
-          ...
-          xn' = /\ ab -> let D' in en
-       in
-       let D in body
-
-where ab are the tyvars pinning the defn further in than it
-need be, and D  is a bunch of simple type applications:
-
-               x1_cl = x1' ab
-               ...
-               xn_cl = xn' ab
-
-The "_cl" indicates that in D, the level numbers on the xi are the context level
-number; type applications aren't worth floating.  The D' decls are
-similar:
-
-               x1_ll = x1' ab
-               ...
-               xn_ll = xn' ab
-
-but differ in their level numbers; here the ab are the newly-introduced
-type lambdas.
 
 \begin{code}
-decideRecFloatLevel ctxt_lvl envs@(venv, tenv) ids rhss
-  | isTopMajLvl ids_only_lvl   &&              -- Destination = top
-    not (all canFloatToTop (zipEqual "decideRec" tys rhss)) -- Some can't float to top
-  =    -- Pin it here
+lvlBind top_lvl ctxt_lvl env (AnnRec pairs)
+  | isInlineCtxt ctxt_lvl      -- Don't do anything inside InlineMe
+  = mapLvl (lvlExpr ctxt_lvl env) rhss                 `thenLvl` \ rhss' ->
+    returnLvl (Rec ([TB b ctxt_lvl | b <- bndrs] `zip` rhss'), env)
+
+  | null abs_vars
+  = cloneRecVars top_lvl env bndrs ctxt_lvl dest_lvl   `thenLvl` \ (new_env, new_bndrs) ->
+    mapLvl (lvlExpr ctxt_lvl new_env) rhss             `thenLvl` \ new_rhss ->
+    returnLvl (Rec ([TB b dest_lvl | b <- new_bndrs] `zip` new_rhss), new_env)
+
+  | isSingleton pairs && count isId abs_vars > 1
+  =    -- Special case for self recursion where there are
+       -- several variables carried around: build a local loop:        
+       --      poly_f = \abs_vars. \lam_vars . letrec f = \lam_vars. rhs in f lam_vars
+       -- This just makes the closures a bit smaller.  If we don't do
+       -- this, allocation rises significantly on some programs
+       --
+       -- We could elaborate it for the case where there are several
+       -- mutually functions, but it's quite a bit more complicated
+       -- 
+       -- This all seems a bit ad hoc -- sigh
     let
-       ids_w_lvls = ids `zip` repeat ctxt_lvl
-       new_envs   = (growIdEnvList venv ids_w_lvls, tenv)
+       (bndr,rhs) = head pairs
+       (rhs_lvl, abs_vars_w_lvls) = lvlLamBndrs dest_lvl abs_vars
+       rhs_env = extendLvlEnv env abs_vars_w_lvls
     in
-    mapLvl (lvlExpr ctxt_lvl new_envs) rhss    `thenLvl` \ rhss' ->
-    returnLvl (ctxt_lvl, [], rhss')
-
-{- OMITTED; see comments above near isWorthFloatingExpr
-
-  | not (any (isWorthFloating True . deAnnotate) rhss)
-  =    -- Pin it here
-    mapLvl (lvlExpr ctxt_lvl envs) rhss        `thenLvl` \ rhss' ->
-    returnLvl (ctxt_lvl, [], rhss')
-
--}
-
-  | ids_only_lvl `ltLvl` tyvars_only_lvl
-  =    -- Abstract wrt tyvars;
-       -- offending_tyvars is definitely non-empty
-       -- (I love the ASSERT to check this...  WDP 95/02)
+    cloneVar NotTopLevel rhs_env bndr rhs_lvl rhs_lvl  `thenLvl` \ (rhs_env', new_bndr) ->
     let
-       -- These defns are just like those in the TyLam case of lvlExpr
-       (incd_lvl, tyvar_lvls) = mapAccumL next (unTopify ids_only_lvl) offending_tyvars
-
-       next lvl tyvar = (lvl1, (tyvar,lvl1))
-                    where lvl1 = incMinorLvl lvl
-
-       ids_w_incd_lvl = [(id,incd_lvl) | id <- ids]
-       new_tenv              = growTyVarEnvList tenv tyvar_lvls
-       new_venv              = growIdEnvList    venv ids_w_incd_lvl
-       new_envs              = (new_venv, new_tenv)
+       (lam_bndrs, rhs_body)     = collectAnnBndrs rhs
+        (body_lvl, new_lam_bndrs) = lvlLamBndrs rhs_lvl lam_bndrs
+       body_env                  = extendLvlEnv rhs_env' new_lam_bndrs
     in
-    mapLvl (lvlExpr incd_lvl new_envs) rhss    `thenLvl` \ rhss' ->
-    mapLvl newLvlVar poly_tys                  `thenLvl` \ poly_vars ->
-    let
-       ids_w_poly_vars = zipEqual "decideRec2" ids poly_vars
-
-               -- The "d_rhss" are the right-hand sides of "D" and "D'"
-               -- in the documentation above
-       d_rhss = [ mkTyApp (Var poly_var) offending_tyvar_tys | poly_var <- poly_vars]
-
-               -- "local_binds" are "D'" in the documentation above
-       local_binds = zipWithEqual "SetLevels" NonRec ids_w_incd_lvl d_rhss
-
-       poly_var_rhss = [ mkTyLam offending_tyvars (foldr Let rhs' local_binds)
-                       | rhs' <- rhss' -- mkCoLet* requires Core...
-                       ]
-
-       poly_binds  = zipEqual "poly_binds" [(poly_var, ids_only_lvl) | poly_var <- poly_vars] poly_var_rhss
-
-    in
-    returnLvl (ctxt_lvl, [Rec poly_binds], d_rhss)
-       -- The new right-hand sides, just a type application, aren't worth floating
-       -- so pin it with ctxt_lvl
-
-  | otherwise
-  =    -- Let it float freely
-    let
-       ids_w_lvls = ids `zip` repeat expr_lvl
-       new_envs   = (growIdEnvList venv ids_w_lvls, tenv)
-    in
-    mapLvl (lvlExpr (unTopify expr_lvl) new_envs) rhss `thenLvl` \ rhss' ->
-    returnLvl (expr_lvl, [], rhss')
+    lvlExpr body_lvl body_env rhs_body         `thenLvl` \ new_rhs_body ->
+    newPolyBndrs dest_lvl env abs_vars [bndr]  `thenLvl` \ (poly_env, [poly_bndr]) ->
+    returnLvl (Rec [(TB poly_bndr dest_lvl, 
+              mkLams abs_vars_w_lvls $
+              mkLams new_lam_bndrs $
+              Let (Rec [(TB new_bndr rhs_lvl, mkLams new_lam_bndrs new_rhs_body)]) 
+                  (mkVarApps (Var new_bndr) lam_bndrs))],
+              poly_env)
+
+  | otherwise  -- Non-null abs_vars
+  = newPolyBndrs dest_lvl env abs_vars bndrs           `thenLvl` \ (new_env, new_bndrs) ->
+    mapLvl (lvlFloatRhs abs_vars dest_lvl new_env) rhss `thenLvl` \ new_rhss ->
+    returnLvl (Rec ([TB b dest_lvl | b <- new_bndrs] `zip` new_rhss), new_env)
 
   where
-    tys  = map idType ids
+    (bndrs,rhss) = unzip pairs
 
-    fvs  = unionManyIdSets [freeVarsOf   rhs | rhs <- rhss] `minusIdSet` mkIdSet ids
-    tfvs = unionManyTyVarSets [freeTyVarsOf rhs | rhs <- rhss]
-    fv_list = idSetToList fvs
-    tv_list = tyVarSetToList tfvs
+       -- Finding the free vars of the binding group is annoying
+    bind_fvs       = (unionVarSets [ idFreeVars bndr `unionVarSet` rhs_fvs
+                                   | (bndr, (rhs_fvs,_)) <- pairs])
+                     `minusVarSet`
+                     mkVarSet bndrs
 
-    ids_only_lvl    = foldr (maxLvl . idLevel venv)    tOP_LEVEL fv_list
-    tyvars_only_lvl = foldr (maxLvl . tyvarLevel tenv) tOP_LEVEL tv_list
-    expr_lvl       = ids_only_lvl `maxLvl` tyvars_only_lvl
+    dest_lvl = destLevel env bind_fvs (all isFunction rhss)
+    abs_vars = abstractVars dest_lvl env bind_fvs
 
-    offending_tyvars
-       | ids_only_lvl `ltLvl` tyvars_only_lvl = filter offending tv_list
-       | otherwise                            = []
+----------------------------------------------------
+-- Three help functons for the type-abstraction case
 
-    offending_tyvar_tys = mkTyVarTys offending_tyvars
-    poly_tys = map (mkForAllTys offending_tyvars) tys
-
-    offending tyvar = ids_only_lvl `ltLvl` tyvarLevel tenv tyvar
+lvlFloatRhs abs_vars dest_lvl env rhs
+  = lvlExpr rhs_lvl rhs_env rhs        `thenLvl` \ rhs' ->
+    returnLvl (mkLams abs_vars_w_lvls rhs')
+  where
+    (rhs_lvl, abs_vars_w_lvls) = lvlLamBndrs dest_lvl abs_vars
+    rhs_env = extendLvlEnv env abs_vars_w_lvls
 \end{code}
 
 
-\begin{code}
-{- ******** OMITTED NOW
-
-isWorthFloating :: Bool                -- True <=> already let-bound
-               -> CoreExpr     -- The expression
-               -> Bool
-
-isWorthFloating alreadyLetBound expr
-
-  | alreadyLetBound = isWorthFloatingExpr expr
-
-  | otherwise       =  -- No point in adding a fresh let-binding for a WHNF, because
-                       -- floating it isn't beneficial enough.
-                     isWorthFloatingExpr expr &&
-                     not (whnfOrBottom expr)
-********** -}
-
-isWorthFloatingExpr :: CoreExpr -> Bool
+%************************************************************************
+%*                                                                     *
+\subsection{Deciding floatability}
+%*                                                                     *
+%************************************************************************
 
-isWorthFloatingExpr (Var v)    = False
-isWorthFloatingExpr (Lit lit)  = False
-isWorthFloatingExpr (App e arg)
-  | notValArg arg              = isWorthFloatingExpr e
-isWorthFloatingExpr (Con con as)
-  | all notValArg as           = False -- Just a type application
-isWorthFloatingExpr _          = True
+\begin{code}
+lvlLamBndrs :: Level -> [CoreBndr] -> (Level, [TaggedBndr Level])
+-- Compute the levels for the binders of a lambda group
+-- The binders returned are exactly the same as the ones passed,
+-- but they are now paired with a level
+lvlLamBndrs lvl [] 
+  = (lvl, [])
+
+lvlLamBndrs lvl bndrs
+  = go  (incMinorLvl lvl)
+       False   -- Havn't bumped major level in this group
+       [] bndrs
+  where
+    go old_lvl bumped_major rev_lvld_bndrs (bndr:bndrs)
+       | isId bndr &&                  -- Go to the next major level if this is a value binder,
+         not bumped_major &&           -- and we havn't already gone to the next level (one jump per group)
+         not (isOneShotLambda bndr)    -- and it isn't a one-shot lambda
+       = go new_lvl True (TB bndr new_lvl : rev_lvld_bndrs) bndrs
 
-canFloatToTop :: (Type, CoreExprWithFVs) -> Bool
+       | otherwise
+       = go old_lvl bumped_major (TB bndr old_lvl : rev_lvld_bndrs) bndrs
 
-canFloatToTop (ty, (FVInfo _ _ (LeakFree _), expr)) = True
-canFloatToTop (ty, (FVInfo _ _ MightLeak,    expr)) = isLeakFreeType [] ty
+       where
+         new_lvl = incMajorLvl old_lvl
 
-valSuggestsLeakFree expr = whnfOrBottom expr
+    go old_lvl _ rev_lvld_bndrs []
+       = (old_lvl, reverse rev_lvld_bndrs)
+       -- a lambda like this (\x -> coerce t (\s -> ...))
+       -- This happens quite a bit in state-transformer programs
 \end{code}
 
+\begin{code}
+  -- Destintion level is the max Id level of the expression
+  -- (We'll abstract the type variables, if any.)
+destLevel :: LevelEnv -> VarSet -> Bool -> Level
+destLevel env fvs is_function
+  |  floatLams env
+  && is_function = tOP_LEVEL           -- Send functions to top level; see
+                                       -- the comments with isFunction
+  | otherwise    = maxIdLevel env fvs
+
+isFunction :: CoreExprWithFVs -> Bool
+-- The idea here is that we want to float *functions* to
+-- the top level.  This saves no work, but 
+--     (a) it can make the host function body a lot smaller, 
+--             and hence inlinable.  
+--     (b) it can also save allocation when the function is recursive:
+--         h = \x -> letrec f = \y -> ...f...y...x...
+--                   in f x
+--     becomes
+--         f = \x y -> ...(f x)...y...x...
+--         h = \x -> f x x
+--     No allocation for f now.
+-- We may only want to do this if there are sufficiently few free 
+-- variables.  We certainly only want to do it for values, and not for
+-- constructors.  So the simple thing is just to look for lambdas
+isFunction (_, AnnLam b e) | isId b    = True
+                          | otherwise = isFunction e
+isFunction (_, AnnNote n e)            = isFunction e
+isFunction other                      = False
+\end{code}
 
 
 %************************************************************************
 %*                                                                     *
-\subsection{Help functions}
+\subsection{Free-To-Level Monad}
 %*                                                                     *
 %************************************************************************
 
 \begin{code}
-idLevel :: IdEnv Level -> Id -> Level
-idLevel venv v
-  = case lookupIdEnv venv v of
-      Just level -> level
-      Nothing    -> ASSERT(toplevelishId v)
-                   tOP_LEVEL
-
-tyvarLevel :: TyVarEnv Level -> TyVar -> Level
-tyvarLevel tenv tyvar
-  = case lookupTyVarEnv tenv tyvar of
-      Just level -> level
-      Nothing    -> tOP_LEVEL
-\end{code}
+type LevelEnv = (FloatOutSwitches,
+                VarEnv Level,                  -- Domain is *post-cloned* TyVars and Ids
+                Subst,                         -- Domain is pre-cloned Ids; tracks the in-scope set
+                                               --      so that subtitution is capture-avoiding
+                IdEnv ([Var], LevelledExpr))   -- Domain is pre-cloned Ids
+       -- We clone let-bound variables so that they are still
+       -- distinct when floated out; hence the SubstEnv/IdEnv.
+        -- (see point 3 of the module overview comment).
+       -- We also use these envs when making a variable polymorphic
+       -- because we want to float it out past a big lambda.
+       --
+       -- The SubstEnv and IdEnv always implement the same mapping, but the
+       -- SubstEnv maps to CoreExpr and the IdEnv to LevelledExpr
+       -- Since the range is always a variable or type application,
+       -- there is never any difference between the two, but sadly
+       -- the types differ.  The SubstEnv is used when substituting in
+       -- a variable's IdInfo; the IdEnv when we find a Var.
+       --
+       -- In addition the IdEnv records a list of tyvars free in the
+       -- type application, just so we don't have to call freeVars on
+       -- the type application repeatedly.
+       --
+       -- The domain of the both envs is *pre-cloned* Ids, though
+       --
+       -- The domain of the VarEnv Level is the *post-cloned* Ids
+
+initialEnv :: FloatOutSwitches -> LevelEnv
+initialEnv float_lams = (float_lams, emptyVarEnv, emptySubst, emptyVarEnv)
+
+floatLams :: LevelEnv -> Bool
+floatLams (FloatOutSw float_lams _, _, _, _) = float_lams
+
+floatConsts :: LevelEnv -> Bool
+floatConsts (FloatOutSw _ float_consts, _, _, _) = float_consts
+
+extendLvlEnv :: LevelEnv -> [TaggedBndr Level] -> LevelEnv
+-- Used when *not* cloning
+extendLvlEnv (float_lams, lvl_env, subst, id_env) prs
+  = (float_lams,
+     foldl add_lvl lvl_env prs,
+     foldl del_subst subst prs,
+     foldl del_id id_env prs)
+  where
+    add_lvl   env (TB v l) = extendVarEnv env v l
+    del_subst env (TB v _) = extendInScope env v
+    del_id    env (TB v _) = delVarEnv env v
+  -- We must remove any clone for this variable name in case of
+  -- shadowing.  This bit me in the following case
+  -- (in nofib/real/gg/Spark.hs):
+  -- 
+  --   case ds of wild {
+  --     ... -> case e of wild {
+  --              ... -> ... wild ...
+  --            }
+  --   }
+  -- 
+  -- The inside occurrence of @wild@ was being replaced with @ds@,
+  -- incorrectly, because the SubstEnv was still lying around.  Ouch!
+  -- KSW 2000-07.
+
+-- extendCaseBndrLvlEnv adds the mapping case-bndr->scrut-var if it can
+-- (see point 4 of the module overview comment)
+extendCaseBndrLvlEnv (float_lams, lvl_env, subst, id_env) (Var scrut_var) case_bndr lvl
+  = (float_lams,
+     extendVarEnv lvl_env case_bndr lvl,
+     extendIdSubst subst case_bndr (Var scrut_var),
+     extendVarEnv id_env case_bndr ([scrut_var], Var scrut_var))
+     
+extendCaseBndrLvlEnv env scrut case_bndr lvl
+  = extendLvlEnv          env [TB case_bndr lvl]
+
+extendPolyLvlEnv dest_lvl (float_lams, lvl_env, subst, id_env) abs_vars bndr_pairs
+  = (float_lams,
+     foldl add_lvl   lvl_env bndr_pairs,
+     foldl add_subst subst   bndr_pairs,
+     foldl add_id    id_env  bndr_pairs)
+  where
+     add_lvl   env (v,v') = extendVarEnv env v' dest_lvl
+     add_subst env (v,v') = extendIdSubst env v (mkVarApps (Var v') abs_vars)
+     add_id    env (v,v') = extendVarEnv env v ((v':abs_vars), mkVarApps (Var v') abs_vars)
+
+extendCloneLvlEnv lvl (float_lams, lvl_env, _, id_env) new_subst bndr_pairs
+  = (float_lams,
+     foldl add_lvl   lvl_env bndr_pairs,
+     new_subst,
+     foldl add_id    id_env  bndr_pairs)
+  where
+     add_lvl   env (v,v') = extendVarEnv env v' lvl
+     add_id    env (v,v') = extendVarEnv env v ([v'], Var v')
 
-%************************************************************************
-%*                                                                     *
-\subsection{Free-To-Level Monad}
-%*                                                                     *
-%************************************************************************
+
+maxIdLevel :: LevelEnv -> VarSet -> Level
+maxIdLevel (_, lvl_env,_,id_env) var_set
+  = foldVarSet max_in tOP_LEVEL var_set
+  where
+    max_in in_var lvl = foldr max_out lvl (case lookupVarEnv id_env in_var of
+                                               Just (abs_vars, _) -> abs_vars
+                                               Nothing            -> [in_var])
+
+    max_out out_var lvl 
+       | isId out_var = case lookupVarEnv lvl_env out_var of
+                               Just lvl' -> maxLvl lvl' lvl
+                               Nothing   -> lvl 
+       | otherwise    = lvl    -- Ignore tyvars in *maxIdLevel*
+
+lookupVar :: LevelEnv -> Id -> LevelledExpr
+lookupVar (_, _, _, id_env) v = case lookupVarEnv id_env v of
+                                      Just (_, expr) -> expr
+                                      other          -> Var v
+
+abstractVars :: Level -> LevelEnv -> VarSet -> [Var]
+       -- Find the variables in fvs, free vars of the target expresion,
+       -- whose level is greater than the destination level
+       -- These are the ones we are going to abstract out
+abstractVars dest_lvl env fvs
+  = uniq (sortLe le [var | fv <- varSetElems fvs, var <- absVarsOf dest_lvl env fv])
+  where
+       -- Sort the variables so we don't get 
+       -- mixed-up tyvars and Ids; it's just messy
+    v1 `le` v2 = case (isId v1, isId v2) of
+                  (True, False) -> False
+                  (False, True) -> True
+                  other         -> v1 <= v2    -- Same family
+
+    uniq :: [Var] -> [Var]
+       -- Remove adjacent duplicates; the sort will have brought them together
+    uniq (v1:v2:vs) | v1 == v2  = uniq (v2:vs)
+                   | otherwise = v1 : uniq (v2:vs)
+    uniq vs = vs
+
+absVarsOf :: Level -> LevelEnv -> Var -> [Var]
+       -- If f is free in the expression, and f maps to poly_f a b c in the
+       -- current substitution, then we must report a b c as candidate type
+       -- variables
+absVarsOf dest_lvl (_, lvl_env, _, id_env) v 
+  | isId v
+  = [zap av2 | av1 <- lookup_avs v, av2 <- add_tyvars av1, abstract_me av2]
+
+  | otherwise
+  = if abstract_me v then [v] else []
+
+  where
+    abstract_me v = case lookupVarEnv lvl_env v of
+                       Just lvl -> dest_lvl `ltLvl` lvl
+                       Nothing  -> False
+
+    lookup_avs v = case lookupVarEnv id_env v of
+                       Just (abs_vars, _) -> abs_vars
+                       Nothing            -> [v]
+
+    add_tyvars v | isId v    = v : varSetElems (idFreeTyVars v)
+                | otherwise = [v]
+
+       -- We are going to lambda-abstract, so nuke any IdInfo,
+       -- and add the tyvars of the Id (if necessary)
+    zap v | isId v = WARN( workerExists (idWorkerInfo v) ||
+                          not (isEmptySpecInfo (idSpecialisation v)),
+                          text "absVarsOf: discarding info on" <+> ppr v )
+                    setIdInfo v vanillaIdInfo
+         | otherwise = v
+\end{code}
 
 \begin{code}
 type LvlM result = UniqSM result
 
+initLvl                = initUs_
 thenLvl                = thenUs
 returnLvl      = returnUs
 mapLvl         = mapUs
-mapAndUnzipLvl  = mapAndUnzipUs
-mapAndUnzip3Lvl = mapAndUnzip3Us
 \end{code}
 
-We create a let-binding for `interesting' (non-utterly-trivial)
-applications, to give them a fighting chance of being floated.
-
 \begin{code}
-newLvlVar :: Type -> LvlM Id
+newPolyBndrs dest_lvl env abs_vars bndrs
+  = getUniquesUs               `thenLvl` \ uniqs ->
+    let
+       new_bndrs = zipWith mk_poly_bndr bndrs uniqs
+    in
+    returnLvl (extendPolyLvlEnv dest_lvl env abs_vars (bndrs `zip` new_bndrs), new_bndrs)
+  where
+    mk_poly_bndr bndr uniq = mkSysLocal (mkFastString str) uniq poly_ty
+                          where
+                            str     = "poly_" ++ occNameString (getOccName bndr)
+                            poly_ty = mkPiTypes abs_vars (idType bndr)
+       
+
+newLvlVar :: String 
+         -> [CoreBndr] -> Type         -- Abstract wrt these bndrs
+         -> LvlM Id
+newLvlVar str vars body_ty     
+  = getUniqueUs        `thenLvl` \ uniq ->
+    returnUs (mkSysLocal (mkFastString str) uniq (mkPiTypes vars body_ty))
+    
+-- The deeply tiresome thing is that we have to apply the substitution
+-- to the rules inside each Id.  Grr.  But it matters.
+
+cloneVar :: TopLevelFlag -> LevelEnv -> Id -> Level -> Level -> LvlM (LevelEnv, Id)
+cloneVar TopLevel env v ctxt_lvl dest_lvl
+  = returnUs (env, v)  -- Don't clone top level things
+cloneVar NotTopLevel env@(_,_,subst,_) v ctxt_lvl dest_lvl
+  = ASSERT( isId v )
+    getUs      `thenLvl` \ us ->
+    let
+      (subst', v1) = cloneIdBndr subst us v
+      v2          = zap_demand ctxt_lvl dest_lvl v1
+      env'        = extendCloneLvlEnv dest_lvl env subst' [(v,v2)]
+    in
+    returnUs (env', v2)
+
+cloneRecVars :: TopLevelFlag -> LevelEnv -> [Id] -> Level -> Level -> LvlM (LevelEnv, [Id])
+cloneRecVars TopLevel env vs ctxt_lvl dest_lvl 
+  = returnUs (env, vs) -- Don't clone top level things
+cloneRecVars NotTopLevel env@(_,_,subst,_) vs ctxt_lvl dest_lvl
+  = ASSERT( all isId vs )
+    getUs                      `thenLvl` \ us ->
+    let
+      (subst', vs1) = cloneRecIdBndrs subst us vs
+      vs2          = map (zap_demand ctxt_lvl dest_lvl) vs1
+      env'         = extendCloneLvlEnv dest_lvl env subst' (vs `zip` vs2)
+    in
+    returnUs (env', vs2)
 
-newLvlVar ty us
-  = mkSysLocal SLIT("lvl") (getUnique us) ty mkUnknownSrcLoc
+       -- VERY IMPORTANT: we must zap the demand info 
+       -- if the thing is going to float out past a lambda
+zap_demand dest_lvl ctxt_lvl id
+  | ctxt_lvl == dest_lvl = id                  -- Stays put
+  | otherwise           = zapDemandIdInfo id   -- Floats out
 \end{code}
+