module Simplify ( simplTopBinds, simplExpr ) where

#include "HsVersions.h"

import DynFlags
import SimplMonad
import Type hiding      ( substTy, extendTvSubst, substTyVar )
import SimplEnv
import SimplUtils
import FamInstEnv	( FamInstEnv )
import Id
import MkId		( seqId, realWorldPrimId )
import MkCore		( mkImpossibleExpr )
import IdInfo
import Name		( mkSystemVarName, isExternalName )
import Coercion hiding  ( substCo, substTy, substCoVar, extendTvSubst )
import OptCoercion	( optCoercion )
import FamInstEnv       ( topNormaliseType )
import DataCon          ( DataCon, dataConWorkId, dataConRepStrictness )
import CoreMonad        ( Tick(..), SimplifierMode(..) )
import CoreSyn
import Demand           ( isStrictDmd )
import PprCore          ( pprParendExpr, pprCoreExpr )
import CoreUnfold 
import CoreUtils
import qualified CoreSubst
import CoreArity
import Rules            ( lookupRule, getRules )
import BasicTypes       ( isMarkedStrict, Arity )
import CostCentre       ( currentCCS, pushCCisNop )
import TysPrim          ( realWorldStatePrimTy )
import BasicTypes       ( TopLevelFlag(..), isTopLevel, RecFlag(..) )
import MonadUtils	( foldlM, mapAccumLM )
import Maybes           ( orElse, isNothing )
import Data.List        ( mapAccumL )
import Outputable
import FastString
import Pair

simplTopBinds :: SimplEnv -> [InBind] -> SimplM SimplEnv

simplTopBinds env0 binds0
  = do  {       -- Put all the top-level binders into scope at the start
                -- so that if a transformation rule has unexpectedly brought
                -- anything into scope, then we don't get a complaint about that.
                -- It's rather as if the top-level binders were imported.
		-- See note [Glomming] in OccurAnal.
        ; env1 <- simplRecBndrs env0 (bindersOfBinds binds0)
        ; dflags <- getDOptsSmpl
        ; let dump_flag = dopt Opt_D_verbose_core2core dflags
        ; env2 <- simpl_binds dump_flag env1 binds0
        ; freeTick SimplifierDone
        ; return env2 }
  where
        -- We need to track the zapped top-level binders, because
        -- they should have their fragile IdInfo zapped (notably occurrence info)
        -- That's why we run down binds and bndrs' simultaneously.
        --
        -- The dump-flag emits a trace for each top-level binding, which
        -- helps to locate the tracing for inlining and rule firing
    simpl_binds :: Bool -> SimplEnv -> [InBind] -> SimplM SimplEnv
    simpl_binds _    env []           = return env
    simpl_binds dump env (bind:binds) = do { env' <- trace_bind dump bind $
                                                     simpl_bind env bind
                                           ; simpl_binds dump env' binds }

    trace_bind True  bind = pprTrace "SimplBind" (ppr (bindersOf bind))
    trace_bind False _    = \x -> x

    simpl_bind env (Rec pairs)  = simplRecBind      env  TopLevel pairs
    simpl_bind env (NonRec b r) = simplRecOrTopPair env' TopLevel NonRecursive b b' r
        where
          (env', b') = addBndrRules env b (lookupRecBndr env b)

simplRecBind :: SimplEnv -> TopLevelFlag
             -> [(InId, InExpr)]
             -> SimplM SimplEnv
simplRecBind env0 top_lvl pairs0
  = do  { let (env_with_info, triples) = mapAccumL add_rules env0 pairs0
        ; env1 <- go (zapFloats env_with_info) triples
        ; return (env0 `addRecFloats` env1) }
        -- addFloats adds the floats from env1,
        -- _and_ updates env0 with the in-scope set from env1
  where
    add_rules :: SimplEnv -> (InBndr,InExpr) -> (SimplEnv, (InBndr, OutBndr, InExpr))
        -- Add the (substituted) rules to the binder
    add_rules env (bndr, rhs) = (env', (bndr, bndr', rhs))
        where
          (env', bndr') = addBndrRules env bndr (lookupRecBndr env bndr)

    go env [] = return env

    go env ((old_bndr, new_bndr, rhs) : pairs)
        = do { env' <- simplRecOrTopPair env top_lvl Recursive old_bndr new_bndr rhs
             ; go env' pairs }

simplRecOrTopPair :: SimplEnv
                  -> TopLevelFlag -> RecFlag
                  -> InId -> OutBndr -> InExpr  -- Binder and rhs
                  -> SimplM SimplEnv    -- Returns an env that includes the binding

simplRecOrTopPair env top_lvl is_rec old_bndr new_bndr rhs
  | preInlineUnconditionally env top_lvl old_bndr rhs   -- Check for unconditional inline
  = do  { tick (PreInlineUnconditionally old_bndr)
        ; return (extendIdSubst env old_bndr (mkContEx env rhs)) }

  | otherwise
  = simplLazyBind env top_lvl is_rec old_bndr new_bndr rhs env

simplLazyBind :: SimplEnv
              -> TopLevelFlag -> RecFlag
              -> InId -> OutId          -- Binder, both pre-and post simpl
                                        -- The OutId has IdInfo, except arity, unfolding
              -> InExpr -> SimplEnv     -- The RHS and its environment
              -> SimplM SimplEnv

simplLazyBind env top_lvl is_rec bndr bndr1 rhs rhs_se
  = -- pprTrace "simplLazyBind" ((ppr bndr <+> ppr bndr1) $$ ppr rhs $$ ppr (seIdSubst rhs_se)) $
    do  { let   rhs_env     = rhs_se `setInScope` env
		(tvs, body) = case collectTyBinders rhs of
			        (tvs, body) | not_lam body -> (tvs,body)
					    | otherwise	   -> ([], rhs)
		not_lam (Lam _ _) = False
		not_lam _	  = True
			-- Do not do the "abstract tyyvar" thing if there's
			-- a lambda inside, becuase it defeats eta-reduction
			--    f = /\a. \x. g a x  
			-- should eta-reduce

        ; (body_env, tvs') <- simplBinders rhs_env tvs
                -- See Note [Floating and type abstraction] in SimplUtils

        -- Simplify the RHS
        ; (body_env1, body1) <- simplExprF body_env body mkRhsStop
        -- ANF-ise a constructor or PAP rhs
        ; (body_env2, body2) <- prepareRhs top_lvl body_env1 bndr1 body1

        ; (env', rhs')
            <-  if not (doFloatFromRhs top_lvl is_rec False body2 body_env2)
                then                            -- No floating, revert to body1
                     do { rhs' <- mkLam env tvs' (wrapFloats body_env1 body1)
                        ; return (env, rhs') }

                else if null tvs then           -- Simple floating
                     do { tick LetFloatFromLet
                        ; return (addFloats env body_env2, body2) }

                else                            -- Do type-abstraction first
                     do { tick LetFloatFromLet
                        ; (poly_binds, body3) <- abstractFloats tvs' body_env2 body2
                        ; rhs' <- mkLam env tvs' body3
                        ; env' <- foldlM (addPolyBind top_lvl) env poly_binds
                        ; return (env', rhs') }

        ; completeBind env' top_lvl bndr bndr1 rhs' }

simplNonRecX :: SimplEnv
             -> InId            -- Old binder
             -> OutExpr         -- Simplified RHS
             -> SimplM SimplEnv

simplNonRecX env bndr new_rhs
  | isDeadBinder bndr	-- Not uncommon; e.g. case (a,b) of c { (p,q) -> p }
  = return env		-- 		 Here c is dead, and we avoid creating
    	   		--               the binding c = (a,b)
  | Coercion co <- new_rhs    
  = return (extendCvSubst env bndr co)
  | otherwise		--		 the binding b = (a,b)
  = do  { (env', bndr') <- simplBinder env bndr
        ; completeNonRecX NotTopLevel env' (isStrictId bndr) bndr bndr' new_rhs }
		-- simplNonRecX is only used for NotTopLevel things

completeNonRecX :: TopLevelFlag -> SimplEnv
                -> Bool
                -> InId                 -- Old binder
                -> OutId                -- New binder
                -> OutExpr              -- Simplified RHS
                -> SimplM SimplEnv

completeNonRecX top_lvl env is_strict old_bndr new_bndr new_rhs
  = do  { (env1, rhs1) <- prepareRhs top_lvl (zapFloats env) new_bndr new_rhs
        ; (env2, rhs2) <- 
                if doFloatFromRhs NotTopLevel NonRecursive is_strict rhs1 env1
                then do { tick LetFloatFromLet
                        ; return (addFloats env env1, rhs1) }   -- Add the floats to the main env
                else return (env, wrapFloats env1 rhs1)         -- Wrap the floats around the RHS
        ; completeBind env2 NotTopLevel old_bndr new_bndr rhs2 }

prepareRhs :: TopLevelFlag -> SimplEnv -> OutId -> OutExpr -> SimplM (SimplEnv, OutExpr)
-- Adds new floats to the env iff that allows us to return a good RHS
prepareRhs top_lvl env id (Cast rhs co)    -- Note [Float coercions]
  | Pair ty1 _ty2 <- coercionKind co       -- Do *not* do this if rhs has an unlifted type
  , not (isUnLiftedType ty1)            -- see Note [Float coercions (unlifted)]
  = do  { (env', rhs') <- makeTrivialWithInfo top_lvl env sanitised_info rhs
        ; return (env', Cast rhs' co) }
  where
    sanitised_info = vanillaIdInfo `setStrictnessInfo` strictnessInfo info
                                   `setDemandInfo`     demandInfo info
    info = idInfo id

prepareRhs top_lvl env0 _ rhs0
  = do  { (_is_exp, env1, rhs1) <- go 0 env0 rhs0
        ; return (env1, rhs1) }
  where
    go n_val_args env (Cast rhs co)
        = do { (is_exp, env', rhs') <- go n_val_args env rhs
             ; return (is_exp, env', Cast rhs' co) }
    go n_val_args env (App fun (Type ty))
        = do { (is_exp, env', rhs') <- go n_val_args env fun
             ; return (is_exp, env', App rhs' (Type ty)) }
    go n_val_args env (App fun arg)
        = do { (is_exp, env', fun') <- go (n_val_args+1) env fun
             ; case is_exp of
                True -> do { (env'', arg') <- makeTrivial top_lvl env' arg
                           ; return (True, env'', App fun' arg') }
                False -> return (False, env, App fun arg) }
    go n_val_args env (Var fun)
        = return (is_exp, env, Var fun)
        where
          is_exp = isExpandableApp fun n_val_args   -- The fun a constructor or PAP
		        -- See Note [CONLIKE pragma] in BasicTypes
			-- The definition of is_exp should match that in
	                -- OccurAnal.occAnalApp

    go _ env other
        = return (False, env, other)

makeTrivial :: TopLevelFlag -> SimplEnv -> OutExpr -> SimplM (SimplEnv, OutExpr)
-- Binds the expression to a variable, if it's not trivial, returning the variable
makeTrivial top_lvl env expr = makeTrivialWithInfo top_lvl env vanillaIdInfo expr

makeTrivialWithInfo :: TopLevelFlag -> SimplEnv -> IdInfo 
                    -> OutExpr -> SimplM (SimplEnv, OutExpr)
-- Propagate strictness and demand info to the new binder
-- Note [Preserve strictness when floating coercions]
-- Returned SimplEnv has same substitution as incoming one
makeTrivialWithInfo top_lvl env info expr
  | exprIsTrivial expr 				-- Already trivial
  || not (bindingOk top_lvl expr expr_ty)	-- Cannot trivialise
						--   See Note [Cannot trivialise]
  = return (env, expr)
  | otherwise           -- See Note [Take care] below
  = do  { uniq <- getUniqueM
        ; let name = mkSystemVarName uniq (fsLit "a")
              var = mkLocalIdWithInfo name expr_ty info
        ; env'  <- completeNonRecX top_lvl env False var var expr
	; expr' <- simplVar env' var
        ; return (env', expr') }
	-- The simplVar is needed becase we're constructing a new binding
	--     a = rhs
	-- And if rhs is of form (rhs1 |> co), then we might get
	--     a1 = rhs1
	--     a = a1 |> co
	-- and now a's RHS is trivial and can be substituted out, and that
	-- is what completeNonRecX will do
	-- To put it another way, it's as if we'd simplified
	--    let var = e in var
  where
    expr_ty = exprType expr

bindingOk :: TopLevelFlag -> CoreExpr -> Type -> Bool
-- True iff we can have a binding of this expression at this level
-- Precondition: the type is the type of the expression
bindingOk top_lvl _ expr_ty
  | isTopLevel top_lvl = not (isUnLiftedType expr_ty) 
  | otherwise          = True

completeBind :: SimplEnv
             -> TopLevelFlag            -- Flag stuck into unfolding
             -> InId                    -- Old binder
             -> OutId -> OutExpr        -- New binder and RHS
             -> SimplM SimplEnv
-- completeBind may choose to do its work
--      * by extending the substitution (e.g. let x = y in ...)
--      * or by adding to the floats in the envt

completeBind env top_lvl old_bndr new_bndr new_rhs
 | isCoVar old_bndr
 = case new_rhs of
     Coercion co -> return (extendCvSubst env old_bndr co)
     _           -> return (addNonRec env new_bndr new_rhs)

 | otherwise
 = ASSERT( isId new_bndr )
   do { let old_info = idInfo old_bndr
	    old_unf  = unfoldingInfo old_info
	    occ_info = occInfo old_info

	-- Do eta-expansion on the RHS of the binding
        -- See Note [Eta-expanding at let bindings] in SimplUtils
      ; (new_arity, final_rhs) <- tryEtaExpand env new_bndr new_rhs

      	-- Simplify the unfolding
      ; new_unfolding <- simplUnfolding env top_lvl old_bndr final_rhs old_unf

      ; if postInlineUnconditionally env top_lvl new_bndr occ_info final_rhs new_unfolding
	                -- Inline and discard the binding
	then do  { tick (PostInlineUnconditionally old_bndr)
	         ; return (extendIdSubst env old_bndr (DoneEx final_rhs)) }
	        -- Use the substitution to make quite, quite sure that the
	        -- substitution will happen, since we are going to discard the binding
	else
   do { let info1 = idInfo new_bndr `setArityInfo` new_arity
	
              -- Unfolding info: Note [Setting the new unfolding]
	    info2 = info1 `setUnfoldingInfo` new_unfolding

	      -- Demand info: Note [Setting the demand info]
            info3 | isEvaldUnfolding new_unfolding = zapDemandInfo info2 `orElse` info2
                  | otherwise                      = info2

            final_id = new_bndr `setIdInfo` info3

      ; -- pprTrace "Binding" (ppr final_id <+> ppr new_unfolding) $
        return (addNonRec env final_id final_rhs) } }
		-- The addNonRec adds it to the in-scope set too

------------------------------
addPolyBind :: TopLevelFlag -> SimplEnv -> OutBind -> SimplM SimplEnv
-- Add a new binding to the environment, complete with its unfolding
-- but *do not* do postInlineUnconditionally, because we have already
-- processed some of the scope of the binding
-- We still want the unfolding though.  Consider
--	let 
--	      x = /\a. let y = ... in Just y
--	in body
-- Then we float the y-binding out (via abstractFloats and addPolyBind)
-- but 'x' may well then be inlined in 'body' in which case we'd like the 
-- opportunity to inline 'y' too.

addPolyBind top_lvl env (NonRec poly_id rhs)
  = do  { unfolding <- simplUnfolding env top_lvl poly_id rhs noUnfolding
    	  		-- Assumes that poly_id did not have an INLINE prag
			-- which is perhaps wrong.  ToDo: think about this
        ; let final_id = setIdInfo poly_id $
                         idInfo poly_id `setUnfoldingInfo` unfolding
                                        `setArityInfo`     exprArity rhs

        ; return (addNonRec env final_id rhs) }

addPolyBind _ env bind@(Rec _) 
  = return (extendFloats env bind)
	-- Hack: letrecs are more awkward, so we extend "by steam"
	-- without adding unfoldings etc.  At worst this leads to
	-- more simplifier iterations

------------------------------
simplUnfolding :: SimplEnv-> TopLevelFlag
               -> InId
               -> OutExpr
	       -> Unfolding -> SimplM Unfolding
-- Note [Setting the new unfolding]
simplUnfolding env _ _ _ (DFunUnfolding ar con ops)
  = return (DFunUnfolding ar con ops')
  where
    ops' = map (substExpr (text "simplUnfolding") env) ops

simplUnfolding env top_lvl id _
    (CoreUnfolding { uf_tmpl = expr, uf_arity = arity
                   , uf_src = src, uf_guidance = guide })
  | isStableSource src
  = do { expr' <- simplExpr rule_env expr
       ; let src' = CoreSubst.substUnfoldingSource (mkCoreSubst (text "inline-unf") env) src
             is_top_lvl = isTopLevel top_lvl
       ; case guide of
           UnfWhen sat_ok _    -- Happens for INLINE things
              -> let guide' = UnfWhen sat_ok (inlineBoringOk expr')
	      	     -- Refresh the boring-ok flag, in case expr'
		     -- has got small. This happens, notably in the inlinings
		     -- for dfuns for single-method classes; see
		     -- Note [Single-method classes] in TcInstDcls.
		     -- A test case is Trac #4138
                 in return (mkCoreUnfolding src' is_top_lvl expr' arity guide')
		 -- See Note [Top-level flag on inline rules] in CoreUnfold

           _other              -- Happens for INLINABLE things
              -> let bottoming = isBottomingId id
                 in bottoming `seq` -- See Note [Force bottoming field]
                    return (mkUnfolding src' is_top_lvl bottoming expr')
                -- If the guidance is UnfIfGoodArgs, this is an INLINABLE
                -- unfolding, and we need to make sure the guidance is kept up
                -- to date with respect to any changes in the unfolding.
       }
  where
    act      = idInlineActivation id
    rule_env = updMode (updModeForInlineRules act) env
       	       -- See Note [Simplifying inside InlineRules] in SimplUtils

simplUnfolding _ top_lvl id new_rhs _
  = let bottoming = isBottomingId id
    in bottoming `seq`  -- See Note [Force bottoming field]
       return (mkUnfolding InlineRhs (isTopLevel top_lvl) bottoming new_rhs)
	  -- We make an  unfolding *even for loop-breakers*.
	  -- Reason: (a) It might be useful to know that they are WHNF
	  -- 	     (b) In TidyPgm we currently assume that, if we want to
	  --	         expose the unfolding then indeed we *have* an unfolding
	  --		 to expose.  (We could instead use the RHS, but currently
	  --		 we don't.)  The simple thing is always to have one.

simplExpr :: SimplEnv -> CoreExpr -> SimplM CoreExpr
simplExpr env expr = simplExprC env expr mkBoringStop

simplExprC :: SimplEnv -> CoreExpr -> SimplCont -> SimplM CoreExpr
        -- Simplify an expression, given a continuation
simplExprC env expr cont
  = -- pprTrace "simplExprC" (ppr expr $$ ppr cont {- $$ ppr (seIdSubst env) -} $$ ppr (seFloats env) ) $
    do  { (env', expr') <- simplExprF (zapFloats env) expr cont
        ; -- pprTrace "simplExprC ret" (ppr expr $$ ppr expr') $
          -- pprTrace "simplExprC ret3" (ppr (seInScope env')) $
          -- pprTrace "simplExprC ret4" (ppr (seFloats env')) $
          return (wrapFloats env' expr') }

--------------------------------------------------
simplExprF :: SimplEnv -> InExpr -> SimplCont
           -> SimplM (SimplEnv, OutExpr)

simplExprF env e cont
  = {- pprTrace "simplExprF" (vcat 
      [ ppr e
      , text "cont =" <+> ppr cont
      , text "inscope =" <+> ppr (seInScope env)
      , text "tvsubst =" <+> ppr (seTvSubst env)
      , text "idsubst =" <+> ppr (seIdSubst env)
      , text "cvsubst =" <+> ppr (seCvSubst env)
      {- , ppr (seFloats env) -} 
      ]) $ -}
    simplExprF1 env e cont

simplExprF1 :: SimplEnv -> InExpr -> SimplCont
            -> SimplM (SimplEnv, OutExpr)
simplExprF1 env (Var v)        cont = simplIdF env v cont
simplExprF1 env (Lit lit)      cont = rebuild env (Lit lit) cont
simplExprF1 env (Note n expr)  cont = simplNote env n expr cont
simplExprF1 env (Cast body co) cont = simplCast env body co cont
simplExprF1 env (Coercion co)  cont = simplCoercionF env co cont
simplExprF1 env (Type ty)      cont = ASSERT( contIsRhsOrArg cont )
                                      rebuild env (Type (substTy env ty)) cont
simplExprF1 env (App fun arg)  cont = simplExprF env fun $
                                      ApplyTo NoDup arg env cont

simplExprF1 env expr@(Lam {}) cont
  = simplLam env zapped_bndrs body cont
        -- The main issue here is under-saturated lambdas
        --   (\x1. \x2. e) arg1
        -- Here x1 might have "occurs-once" occ-info, because occ-info
        -- is computed assuming that a group of lambdas is applied
        -- all at once.  If there are too few args, we must zap the
        -- occ-info, UNLESS the remaining binders are one-shot
  where
    (bndrs, body) = collectBinders expr
    zapped_bndrs | need_to_zap = map zap bndrs
                 | otherwise   = bndrs

    need_to_zap = any zappable_bndr (drop n_args bndrs)
    n_args = countArgs cont
        -- NB: countArgs counts all the args (incl type args)
        -- and likewise drop counts all binders (incl type lambdas)

    zappable_bndr b = isId b && not (isOneShotBndr b)
    zap b | isTyVar b = b
          | otherwise = zapLamIdInfo b

simplExprF1 env (Case scrut bndr _ alts) cont
  | sm_case_case (getMode env)
  =     -- Simplify the scrutinee with a Select continuation
    simplExprF env scrut (Select NoDup bndr alts env cont)

  | otherwise
  =     -- If case-of-case is off, simply simplify the case expression
        -- in a vanilla Stop context, and rebuild the result around it
    do  { case_expr' <- simplExprC env scrut
                             (Select NoDup bndr alts env mkBoringStop)
        ; rebuild env case_expr' cont }

simplExprF1 env (Let (Rec pairs) body) cont
  = do  { env' <- simplRecBndrs env (map fst pairs)
                -- NB: bndrs' don't have unfoldings or rules
                -- We add them as we go down

        ; env'' <- simplRecBind env' NotTopLevel pairs
        ; simplExprF env'' body cont }

simplExprF1 env (Let (NonRec bndr rhs) body) cont
  = simplNonRecE env bndr (rhs, env) ([], body) cont

---------------------------------
simplType :: SimplEnv -> InType -> SimplM OutType
        -- Kept monadic just so we can do the seqType
simplType env ty
  = -- pprTrace "simplType" (ppr ty $$ ppr (seTvSubst env)) $
    seqType new_ty `seq` return new_ty
  where
    new_ty = substTy env ty

---------------------------------
simplCoercionF :: SimplEnv -> InCoercion -> SimplCont
               -> SimplM (SimplEnv, OutExpr)
-- We are simplifying a term of form (Coercion co)
-- Simplify the InCoercion, and then try to combine with the 
-- context, to implememt the rule
--     (Coercion co) |> g
--  =  Coercion (syn (nth 0 g) ; co ; nth 1 g) 
simplCoercionF env co cont 
  = do { co' <- simplCoercion env co
       ; simpl_co co' cont }
  where
    simpl_co co (CoerceIt g cont)
       = simpl_co new_co cont
     where
       new_co = mkSymCo g0 `mkTransCo` co `mkTransCo` g1
       [g0, g1] = decomposeCo 2 g

    simpl_co co cont
       = seqCo co `seq` rebuild env (Coercion co) cont

simplCoercion :: SimplEnv -> InCoercion -> SimplM OutCoercion
simplCoercion env co
  = let opt_co = optCoercion (getCvSubst env) co
    in opt_co `seq` return opt_co

rebuild :: SimplEnv -> OutExpr -> SimplCont -> SimplM (SimplEnv, OutExpr)
-- At this point the substitution in the SimplEnv should be irrelevant
-- only the in-scope set and floats should matter
rebuild env expr cont
  = case cont of
      Stop {}                      -> return (env, expr)
      CoerceIt co cont             -> rebuild env (Cast expr co) cont
      Select _ bndr alts se cont   -> rebuildCase (se `setFloats` env) expr bndr alts cont
      StrictArg info _ cont        -> rebuildCall env (info `addArgTo` expr) cont
      StrictBind b bs body se cont -> do { env' <- simplNonRecX (se `setFloats` env) b expr
                                         ; simplLam env' bs body cont }
      ApplyTo dup_flag arg se cont -- See Note [Avoid redundant simplification]
        | isSimplified dup_flag    -> rebuild env (App expr arg) cont
        | otherwise                -> do { arg' <- simplExpr (se `setInScope` env) arg
                                         ; rebuild env (App expr arg') cont }

simplCast :: SimplEnv -> InExpr -> Coercion -> SimplCont
          -> SimplM (SimplEnv, OutExpr)
simplCast env body co0 cont0
  = do  { co1 <- simplCoercion env co0
        ; -- pprTrace "simplCast" (ppr co1) $
          simplExprF env body (addCoerce co1 cont0) }
  where
       addCoerce co cont = add_coerce co (coercionKind co) cont

       add_coerce _co (Pair s1 k1) cont     -- co :: ty~ty
         | s1 `eqType` k1 = cont    -- is a no-op

       add_coerce co1 (Pair s1 _k2) (CoerceIt co2 cont)
         | (Pair _l1 t1) <- coercionKind co2
		-- 	e |> (g1 :: S1~L) |> (g2 :: L~T1)
                -- ==>
                --      e,                       if S1=T1
                --      e |> (g1 . g2 :: S1~T1)  otherwise
                --
                -- For example, in the initial form of a worker
                -- we may find  (coerce T (coerce S (\x.e))) y
                -- and we'd like it to simplify to e[y/x] in one round
                -- of simplification
         , s1 `eqType` t1  = cont            -- The coerces cancel out
         | otherwise       = CoerceIt (mkTransCo co1 co2) cont

       add_coerce co (Pair s1s2 _t1t2) (ApplyTo dup (Type arg_ty) arg_se cont)
                -- (f |> g) ty  --->   (f ty) |> (g @ ty)
                -- This implements the PushT rule from the paper
         | Just (tyvar,_) <- splitForAllTy_maybe s1s2
         = ASSERT( isTyVar tyvar )
           ApplyTo Simplified (Type arg_ty') (zapSubstEnv arg_se) (addCoerce new_cast cont)
         where
           new_cast = mkInstCo co arg_ty'
           arg_ty' | isSimplified dup = arg_ty
                   | otherwise        = substTy (arg_se `setInScope` env) arg_ty

{-
       add_coerce co (Pair s1s2 _t1t2) (ApplyTo dup (Coercion arg_co) arg_se cont)
                -- This implements the PushC rule from the paper
         | Just (covar,_) <- splitForAllTy_maybe s1s2
         = ASSERT( isCoVar covar )
           ApplyTo Simplified (Coercion new_arg_co) (zapSubstEnv arg_se) (addCoerce co1 cont)
         where
           [co0, co1]   = decomposeCo 2 co
           [co00, co01] = decomposeCo 2 co0

           arg_co' | isSimplified dup = arg_co
                   | otherwise        = substCo (arg_se `setInScope` env) arg_co
           new_arg_co = co00    `mkTransCo`
                        arg_co' `mkTransCo`
                        mkSymCo co01
-}

       add_coerce co (Pair s1s2 t1t2) (ApplyTo dup arg arg_se cont)
         | isFunTy s1s2   -- This implements the Push rule from the paper
         , isFunTy t1t2   -- Check t1t2 to ensure 'arg' is a value arg
                --      (e |> (g :: s1s2 ~ t1->t2)) f
                -- ===>
                --      (e (f |> (arg g :: t1~s1))
		--	|> (res g :: s2->t2)
                --
                -- t1t2 must be a function type, t1->t2, because it's applied
                -- to something but s1s2 might conceivably not be
                --
                -- When we build the ApplyTo we can't mix the out-types
                -- with the InExpr in the argument, so we simply substitute
                -- to make it all consistent.  It's a bit messy.
                -- But it isn't a common case.
                --
                -- Example of use: Trac #995
         = ApplyTo dup new_arg (zapSubstEnv arg_se) (addCoerce co2 cont)
         where
           -- we split coercion t1->t2 ~ s1->s2 into t1 ~ s1 and
           -- t2 ~ s2 with left and right on the curried form:
           --    (->) t1 t2 ~ (->) s1 s2
           [co1, co2] = decomposeCo 2 co
           new_arg    = mkCoerce (mkSymCo co1) arg'
           arg'       = substExpr (text "move-cast") arg_se' arg
           arg_se'    = arg_se `setInScope` env

       add_coerce co _ cont = CoerceIt co cont

simplLam :: SimplEnv -> [InId] -> InExpr -> SimplCont
         -> SimplM (SimplEnv, OutExpr)

simplLam env [] body cont = simplExprF env body cont

        -- Beta reduction
simplLam env (bndr:bndrs) body (ApplyTo _ arg arg_se cont)
  = do  { tick (BetaReduction bndr)
        ; simplNonRecE env (zap_unfolding bndr) (arg, arg_se) (bndrs, body) cont }
  where
    zap_unfolding bndr  -- See Note [Zap unfolding when beta-reducing]
      | isId bndr, isStableUnfolding (realIdUnfolding bndr)
      = setIdUnfolding bndr NoUnfolding
      | otherwise = bndr

        -- Not enough args, so there are real lambdas left to put in the result
simplLam env bndrs body cont
  = do  { (env', bndrs') <- simplLamBndrs env bndrs
        ; body' <- simplExpr env' body
        ; new_lam <- mkLam env' bndrs' body'
        ; rebuild env' new_lam cont }

------------------
simplNonRecE :: SimplEnv
             -> InBndr                  -- The binder
             -> (InExpr, SimplEnv)      -- Rhs of binding (or arg of lambda)
             -> ([InBndr], InExpr)      -- Body of the let/lambda
                                        --      \xs.e
             -> SimplCont
             -> SimplM (SimplEnv, OutExpr)

-- simplNonRecE is used for
--  * non-top-level non-recursive lets in expressions
--  * beta reduction
--
-- It deals with strict bindings, via the StrictBind continuation,
-- which may abort the whole process
--
-- The "body" of the binding comes as a pair of ([InId],InExpr)
-- representing a lambda; so we recurse back to simplLam
-- Why?  Because of the binder-occ-info-zapping done before
--       the call to simplLam in simplExprF (Lam ...)

	-- First deal with type applications and type lets
	--   (/\a. e) (Type ty)   and   (let a = Type ty in e)
simplNonRecE env bndr (Type ty_arg, rhs_se) (bndrs, body) cont
  = ASSERT( isTyVar bndr )
    do	{ ty_arg' <- simplType (rhs_se `setInScope` env) ty_arg
	; simplLam (extendTvSubst env bndr ty_arg') bndrs body cont }

simplNonRecE env bndr (rhs, rhs_se) (bndrs, body) cont
  | preInlineUnconditionally env NotTopLevel bndr rhs
  = do  { tick (PreInlineUnconditionally bndr)
        ; -- pprTrace "preInlineUncond" (ppr bndr <+> ppr rhs) $
          simplLam (extendIdSubst env bndr (mkContEx rhs_se rhs)) bndrs body cont }

  | isStrictId bndr		  -- Includes coercions
  = do  { simplExprF (rhs_se `setFloats` env) rhs
                     (StrictBind bndr bndrs body env cont) }

  | otherwise
  = ASSERT( not (isTyVar bndr) )
    do  { (env1, bndr1) <- simplNonRecBndr env bndr
        ; let (env2, bndr2) = addBndrRules env1 bndr bndr1
        ; env3 <- simplLazyBind env2 NotTopLevel NonRecursive bndr bndr2 rhs rhs_se
        ; simplLam env3 bndrs body cont }

-- Hack alert: we only distinguish subsumed cost centre stacks for the
-- purposes of inlining.  All other CCCSs are mapped to currentCCS.
simplNote :: SimplEnv -> Note -> CoreExpr -> SimplCont
          -> SimplM (SimplEnv, OutExpr)
simplNote env (SCC cc) e cont
  | pushCCisNop cc (getEnclosingCC env)  -- scc "f" (...(scc "f" e)...) 
  = simplExprF env e cont	         -- ==>  scc "f" (...e...)
  | otherwise
  = do  { e' <- simplExpr (setEnclosingCC env currentCCS) e
        ; rebuild env (mkSCC cc e') cont }

simplNote env (CoreNote s) e cont
  = do { e' <- simplExpr env e
       ; rebuild env (Note (CoreNote s) e') cont }

simplVar :: SimplEnv -> InVar -> SimplM OutExpr
-- Look up an InVar in the environment
simplVar env var
  | isTyVar var = return (Type (substTyVar env var))
  | isCoVar var = return (Coercion (substCoVar env var))
  | otherwise
  = case substId env var of
        DoneId var1          -> return (Var var1)
        DoneEx e             -> return e
        ContEx tvs cvs ids e -> simplExpr (setSubstEnv env tvs cvs ids) e

simplIdF :: SimplEnv -> InId -> SimplCont -> SimplM (SimplEnv, OutExpr)
simplIdF env var cont
  = case substId env var of
        DoneEx e             -> simplExprF (zapSubstEnv env) e cont
        ContEx tvs cvs ids e -> simplExprF (setSubstEnv env tvs cvs ids) e cont
        DoneId var1          -> completeCall env var1 cont
                -- Note [zapSubstEnv]
                -- The template is already simplified, so don't re-substitute.
                -- This is VITAL.  Consider
                --      let x = e in
                --      let y = \z -> ...x... in
                --      \ x -> ...y...
                -- We'll clone the inner \x, adding x->x' in the id_subst
                -- Then when we inline y, we must *not* replace x by x' in
                -- the inlined copy!!

---------------------------------------------------------
--      Dealing with a call site

completeCall :: SimplEnv -> Id -> SimplCont -> SimplM (SimplEnv, OutExpr)
completeCall env var cont
  = do  {   ------------- Try inlining ----------------
          dflags <- getDOptsSmpl
        ; let  (lone_variable, arg_infos, call_cont) = contArgs cont
                -- The args are OutExprs, obtained by *lazily* substituting
                -- in the args found in cont.  These args are only examined
                -- to limited depth (unless a rule fires).  But we must do
                -- the substitution; rule matching on un-simplified args would
                -- be bogus

               n_val_args = length arg_infos
               interesting_cont = interestingCallContext call_cont
               unfolding    = activeUnfolding env var
               maybe_inline = callSiteInline dflags var unfolding
                                             lone_variable arg_infos interesting_cont
        ; case maybe_inline of {
            Just expr      -- There is an inlining!
              ->  do { tick (UnfoldingDone var)
                     ; trace_inline dflags expr cont $
                       simplExprF (zapSubstEnv env) expr cont }

            ; Nothing -> do               -- No inlining!

        { rule_base <- getSimplRules
        ; let info = mkArgInfo var (getRules rule_base var) n_val_args call_cont
        ; rebuildCall env info cont
    }}}
  where
    trace_inline dflags unfolding cont stuff
      | not (dopt Opt_D_dump_inlinings dflags) = stuff
      | not (dopt Opt_D_verbose_core2core dflags) 
      = if isExternalName (idName var) then 
      	  pprDefiniteTrace "Inlining done:" (ppr var) stuff
        else stuff
      | otherwise
      = pprDefiniteTrace ("Inlining done: " ++ showSDoc (ppr var))
           (vcat [text "Inlined fn: " <+> nest 2 (ppr unfolding),
                  text "Cont:  " <+> ppr cont])
           stuff

rebuildCall :: SimplEnv
            -> ArgInfo
            -> SimplCont
            -> SimplM (SimplEnv, OutExpr)
rebuildCall env (ArgInfo { ai_fun = fun, ai_args = rev_args, ai_strs = [] }) cont
  -- When we run out of strictness args, it means
  -- that the call is definitely bottom; see SimplUtils.mkArgInfo
  -- Then we want to discard the entire strict continuation.  E.g.
  --    * case (error "hello") of { ... }
  --    * (error "Hello") arg
  --    * f (error "Hello") where f is strict
  --    etc
  -- Then, especially in the first of these cases, we'd like to discard
  -- the continuation, leaving just the bottoming expression.  But the
  -- type might not be right, so we may have to add a coerce.
  | not (contIsTrivial cont)     -- Only do this if there is a non-trivial
  = return (env, mk_coerce res)  -- contination to discard, else we do it
  where                          -- again and again!
    res     = mkApps (Var fun) (reverse rev_args)
    res_ty  = exprType res
    cont_ty = contResultType env res_ty cont
    co      = mkUnsafeCo res_ty cont_ty
    mk_coerce expr | cont_ty `eqType` res_ty = expr
                   | otherwise = mkCoerce co expr

rebuildCall env info (ApplyTo dup_flag (Type arg_ty) se cont)
  = do { arg_ty' <- if isSimplified dup_flag then return arg_ty
                    else simplType (se `setInScope` env) arg_ty
       ; rebuildCall env (info `addArgTo` Type arg_ty') cont }

rebuildCall env info@(ArgInfo { ai_encl = encl_rules
                              , ai_strs = str:strs, ai_discs = disc:discs })
            (ApplyTo dup_flag arg arg_se cont)
  | isSimplified dup_flag     -- See Note [Avoid redundant simplification]
  = rebuildCall env (addArgTo info' arg) cont

  | str                 -- Strict argument
  = -- pprTrace "Strict Arg" (ppr arg $$ ppr (seIdSubst env) $$ ppr (seInScope env)) $
    simplExprF (arg_se `setFloats` env) arg
               (StrictArg info' cci cont)
                -- Note [Shadowing]

  | otherwise                           -- Lazy argument
        -- DO NOT float anything outside, hence simplExprC
        -- There is no benefit (unlike in a let-binding), and we'd
        -- have to be very careful about bogus strictness through
        -- floating a demanded let.
  = do  { arg' <- simplExprC (arg_se `setInScope` env) arg
                             (mkLazyArgStop cci)
        ; rebuildCall env (addArgTo info' arg') cont }
  where
    info' = info { ai_strs = strs, ai_discs = discs }
    cci | encl_rules || disc > 0 = ArgCtxt encl_rules  -- Be keener here
        | otherwise              = BoringCtxt          -- Nothing interesting

rebuildCall env (ArgInfo { ai_fun = fun, ai_args = rev_args, ai_rules = rules }) cont
  = do {  -- We've accumulated a simplified call in <fun,rev_args> 
          -- so try rewrite rules; see Note [RULEs apply to simplified arguments]
	  -- See also Note [Rules for recursive functions]
	; let args = reverse rev_args
              env' = zapSubstEnv env
	; mb_rule <- tryRules env rules fun args cont
	; case mb_rule of {
	     Just (n_args, rule_rhs) -> simplExprF env' rule_rhs $
                                        pushSimplifiedArgs env' (drop n_args args) cont ;
                 -- n_args says how many args the rule consumed
           ; Nothing -> rebuild env (mkApps (Var fun) args) cont      -- No rules
    } }

tryRules :: SimplEnv -> [CoreRule]
         -> Id -> [OutExpr] -> SimplCont 
	 -> SimplM (Maybe (Arity, CoreExpr))	     -- The arity is the number of
	    	   	  	  		     -- args consumed by the rule
tryRules env rules fn args call_cont
  | null rules
  = return Nothing
  | otherwise
  = do { case lookupRule (activeRule env) (getUnfoldingInRuleMatch env) 
                         (getInScope env) fn args rules of {
           Nothing               -> return Nothing ;   -- No rule matches
           Just (rule, rule_rhs) ->

             do { tick (RuleFired (ru_name rule))
                ; dflags <- getDOptsSmpl
                ; trace_dump dflags rule rule_rhs $
                  return (Just (ruleArity rule, rule_rhs)) }}}
  where
    trace_dump dflags rule rule_rhs stuff
      | not (dopt Opt_D_dump_rule_firings dflags)
      , not (dopt Opt_D_dump_rule_rewrites dflags) = stuff

      | not (dopt Opt_D_dump_rule_rewrites dflags)
      = pprDefiniteTrace "Rule fired:" (ftext (ru_name rule)) stuff

      | otherwise
      = pprDefiniteTrace "Rule fired"
           (vcat [text "Rule:" <+> ftext (ru_name rule),
           	  text "Before:" <+> hang (ppr fn) 2 (sep (map pprParendExpr args)),
           	  text "After: " <+> pprCoreExpr rule_rhs,
           	  text "Cont:  " <+> ppr call_cont])
           stuff

---------------------------------------------------------
--      Eliminate the case if possible

rebuildCase, reallyRebuildCase
   :: SimplEnv
   -> OutExpr          -- Scrutinee
   -> InId             -- Case binder
   -> [InAlt]          -- Alternatives (inceasing order)
   -> SimplCont
   -> SimplM (SimplEnv, OutExpr)

--------------------------------------------------
--      1. Eliminate the case if there's a known constructor
--------------------------------------------------

rebuildCase env scrut case_bndr alts cont
  | Lit lit <- scrut    -- No need for same treatment as constructors
                        -- because literals are inlined more vigorously
  = do  { tick (KnownBranch case_bndr)
        ; case findAlt (LitAlt lit) alts of
	    Nothing           -> missingAlt env case_bndr alts cont
	    Just (_, bs, rhs) -> simple_rhs bs rhs }

  | Just (con, ty_args, other_args) <- exprIsConApp_maybe (getUnfoldingInRuleMatch env) scrut
        -- Works when the scrutinee is a variable with a known unfolding
        -- as well as when it's an explicit constructor application
  = do  { tick (KnownBranch case_bndr)
        ; case findAlt (DataAlt con) alts of
	    Nothing  -> missingAlt env case_bndr alts cont
            Just (DEFAULT, bs, rhs) -> simple_rhs bs rhs
	    Just (_, bs, rhs)       -> knownCon env scrut con ty_args other_args 
                                                case_bndr bs rhs cont
	}
  where
    simple_rhs bs rhs = ASSERT( null bs ) 
                        do { env' <- simplNonRecX env case_bndr scrut
    	                   ; simplExprF env' rhs cont }


--------------------------------------------------
--      2. Eliminate the case if scrutinee is evaluated
--------------------------------------------------

rebuildCase env scrut case_bndr [(_, bndrs, rhs)] cont
  -- See if we can get rid of the case altogether
  -- See Note [Case elimination] 
  -- mkCase made sure that if all the alternatives are equal,
  -- then there is now only one (DEFAULT) rhs
 | all isDeadBinder bndrs       -- bndrs are [InId]

 , if isUnLiftedType (idType case_bndr)
   then ok_for_spec         -- Satisfy the let-binding invariant
   else elim_lifted
  = do  { tick (CaseElim case_bndr)
        ; env' <- simplNonRecX env case_bndr scrut
          -- If case_bndr is deads, simplNonRecX will discard
        ; simplExprF env' rhs cont }
  where
    elim_lifted   -- See Note [Case elimination: lifted case]
      = exprIsHNF scrut
     || (strict_case_bndr && scrut_is_var scrut) 
              -- The case binder is going to be evaluated later,
              -- and the scrutinee is a simple variable

     || (is_plain_seq && ok_for_spec)
              -- Note: not the same as exprIsHNF

    ok_for_spec      = exprOkForSpeculation scrut
    is_plain_seq     = isDeadBinder case_bndr	-- Evaluation *only* for effect
    strict_case_bndr = isStrictDmd (idDemandInfo case_bndr)

    scrut_is_var (Cast s _) = scrut_is_var s
    scrut_is_var (Var v)    = not (isTickBoxOp v)
                                    -- ugly hack; covering this case is what
                                    -- exprOkForSpeculation was intended for.
    scrut_is_var _          = False


--------------------------------------------------
--      3. Try seq rules; see Note [User-defined RULES for seq] in MkId
--------------------------------------------------

rebuildCase env scrut case_bndr alts@[(_, bndrs, rhs)] cont
  | all isDeadBinder (case_bndr : bndrs)  -- So this is just 'seq'
  = do { let rhs' = substExpr (text "rebuild-case") env rhs
             out_args = [Type (substTy env (idType case_bndr)), 
	     	         Type (exprType rhs'), scrut, rhs']
	     	      -- Lazily evaluated, so we don't do most of this

       ; rule_base <- getSimplRules
       ; mb_rule <- tryRules env (getRules rule_base seqId) seqId out_args cont
       ; case mb_rule of 
           Just (n_args, res) -> simplExprF (zapSubstEnv env) 
	   	       		    	    (mkApps res (drop n_args out_args))
                                            cont
	   Nothing -> reallyRebuildCase env scrut case_bndr alts cont }

rebuildCase env scrut case_bndr alts cont
  = reallyRebuildCase env scrut case_bndr alts cont

--------------------------------------------------
--      3. Catch-all case
--------------------------------------------------

reallyRebuildCase env scrut case_bndr alts cont
  = do  {       -- Prepare the continuation;
                -- The new subst_env is in place
          (env', dup_cont, nodup_cont) <- prepareCaseCont env alts cont

        -- Simplify the alternatives
        ; (scrut', case_bndr', alts') <- simplAlts env' scrut case_bndr alts dup_cont

	-- Check for empty alternatives
	; if null alts' then missingAlt env case_bndr alts cont
	  else do
        { dflags <- getDOptsSmpl
        ; case_expr <- mkCase dflags scrut' case_bndr' alts'

	-- Notice that rebuild gets the in-scope set from env', not alt_env
	-- (which in any case is only build in simplAlts)
	-- The case binder *not* scope over the whole returned case-expression
	; rebuild env' case_expr nodup_cont } }

simplAlts :: SimplEnv
          -> OutExpr
          -> InId                       -- Case binder
          -> [InAlt]			-- Non-empty
	  -> SimplCont
          -> SimplM (OutExpr, OutId, [OutAlt])  -- Includes the continuation
-- Like simplExpr, this just returns the simplified alternatives;
-- it does not return an environment

simplAlts env scrut case_bndr alts cont'
  = -- pprTrace "simplAlts" (ppr alts $$ ppr (seTvSubst env)) $
    do  { let env0 = zapFloats env

        ; (env1, case_bndr1) <- simplBinder env0 case_bndr

        ; fam_envs <- getFamEnvs
	; (alt_env', scrut', case_bndr') <- improveSeq fam_envs env1 scrut 
						       case_bndr case_bndr1 alts

        ; (imposs_deflt_cons, in_alts) <- prepareAlts scrut' case_bndr' alts

	; let mb_var_scrut = case scrut' of { Var v -> Just v; _ -> Nothing }
        ; alts' <- mapM (simplAlt alt_env' mb_var_scrut
                             imposs_deflt_cons case_bndr' cont') in_alts
        ; return (scrut', case_bndr', alts') }


------------------------------------
improveSeq :: (FamInstEnv, FamInstEnv) -> SimplEnv
	   -> OutExpr -> InId -> OutId -> [InAlt]
	   -> SimplM (SimplEnv, OutExpr, OutId)
-- Note [Improving seq]
improveSeq fam_envs env scrut case_bndr case_bndr1 [(DEFAULT,_,_)]
  | not (isDeadBinder case_bndr)	-- Not a pure seq!  See Note [Improving seq]
  , Just (co, ty2) <- topNormaliseType fam_envs (idType case_bndr1)
  = do { case_bndr2 <- newId (fsLit "nt") ty2
        ; let rhs  = DoneEx (Var case_bndr2 `Cast` mkSymCo co)
              env2 = extendIdSubst env case_bndr rhs
        ; return (env2, scrut `Cast` co, case_bndr2) }

improveSeq _ env scrut _ case_bndr1 _
  = return (env, scrut, case_bndr1)


------------------------------------
simplAlt :: SimplEnv
	 -> Maybe OutId    -- Scrutinee
         -> [AltCon]       -- These constructors can't be present when
                           -- matching the DEFAULT alternative
         -> OutId          -- The case binder
         -> SimplCont
         -> InAlt
         -> SimplM OutAlt

simplAlt env scrut imposs_deflt_cons case_bndr' cont' (DEFAULT, bndrs, rhs)
  = ASSERT( null bndrs )
    do  { let env' = addBinderUnfolding env scrut case_bndr' 
                                        (mkOtherCon imposs_deflt_cons)
                -- Record the constructors that the case-binder *can't* be.
        ; rhs' <- simplExprC env' rhs cont'
        ; return (DEFAULT, [], rhs') }

simplAlt env scrut _ case_bndr' cont' (LitAlt lit, bndrs, rhs)
  = ASSERT( null bndrs )
    do  { let env' = addBinderUnfolding env scrut case_bndr' 
                                        (mkSimpleUnfolding (Lit lit))
        ; rhs' <- simplExprC env' rhs cont'
        ; return (LitAlt lit, [], rhs') }

simplAlt env scrut _ case_bndr' cont' (DataAlt con, vs, rhs)
  = do  {       -- Deal with the pattern-bound variables
                -- Mark the ones that are in ! positions in the
                -- data constructor as certainly-evaluated.
                -- NB: simplLamBinders preserves this eval info
          let vs_with_evals = add_evals (dataConRepStrictness con)
        ; (env', vs') <- simplLamBndrs env vs_with_evals

                -- Bind the case-binder to (con args)
        ; let inst_tys' = tyConAppArgs (idType case_bndr')
              con_args  = map Type inst_tys' ++ varsToCoreExprs vs'
              unf       = mkSimpleUnfolding (mkConApp con con_args)
              env''     = addBinderUnfolding env' scrut case_bndr' unf

        ; rhs' <- simplExprC env'' rhs cont'
        ; return (DataAlt con, vs', rhs') }
  where
        -- add_evals records the evaluated-ness of the bound variables of
        -- a case pattern.  This is *important*.  Consider
        --      data T = T !Int !Int
        --
        --      case x of { T a b -> T (a+1) b }
        --
        -- We really must record that b is already evaluated so that we don't
        -- go and re-evaluate it when constructing the result.
        -- See Note [Data-con worker strictness] in MkId.lhs
    add_evals the_strs
        = go vs the_strs
        where
          go [] [] = []
          go (v:vs') strs | isTyVar v = v : go vs' strs
          go (v:vs') (str:strs)
            | isMarkedStrict str = evald_v  : go vs' strs
            | otherwise          = zapped_v : go vs' strs
            where
              zapped_v = zapBndrOccInfo keep_occ_info v
              evald_v  = zapped_v `setIdUnfolding` evaldUnfolding
          go _ _ = pprPanic "cat_evals" (ppr con $$ ppr vs $$ ppr the_strs)

	-- See Note [zapOccInfo]
        -- zap_occ_info: if the case binder is alive, then we add the unfolding
        --      case_bndr = C vs
        -- to the envt; so vs are now very much alive
        -- Note [Aug06] I can't see why this actually matters, but it's neater
        --        case e of t { (a,b) -> ...(case t of (p,q) -> p)... }
        --   ==>  case e of t { (a,b) -> ...(a)... }
        -- Look, Ma, a is alive now.
    keep_occ_info = isDeadBinder case_bndr' && isNothing scrut

addBinderUnfolding :: SimplEnv -> Maybe OutId -> Id -> Unfolding -> SimplEnv
addBinderUnfolding env scrut bndr unf
  = case scrut of
       Just v -> modifyInScope env1 (v `setIdUnfolding` unf)
       _      -> env1
  where
    env1 = modifyInScope env bndr_w_unf
    bndr_w_unf = bndr `setIdUnfolding` unf

zapBndrOccInfo :: Bool -> Id -> Id
-- Consider  case e of b { (a,b) -> ... }
-- Then if we bind b to (a,b) in "...", and b is not dead,
-- then we must zap the deadness info on a,b
zapBndrOccInfo keep_occ_info pat_id
  | keep_occ_info = pat_id
  | otherwise     = zapIdOccInfo pat_id

knownCon :: SimplEnv		
         -> OutExpr				-- The scrutinee
         -> DataCon -> [OutType] -> [OutExpr]	-- The scrutinee (in pieces)
         -> InId -> [InBndr] -> InExpr		-- The alternative
         -> SimplCont
         -> SimplM (SimplEnv, OutExpr)

knownCon env scrut dc dc_ty_args dc_args bndr bs rhs cont
  = do  { env'  <- bind_args env bs dc_args
        ; env'' <- bind_case_bndr env'
        ; simplExprF env'' rhs cont }
  where
    zap_occ = zapBndrOccInfo (isDeadBinder bndr)    -- bndr is an InId

                  -- Ugh!
    bind_args env' [] _  = return env'

    bind_args env' (b:bs') (Type ty : args)
      = ASSERT( isTyVar b )
        bind_args (extendTvSubst env' b ty) bs' args

    bind_args env' (b:bs') (arg : args)
      = ASSERT( isId b )
        do { let b' = zap_occ b
             -- Note that the binder might be "dead", because it doesn't
             -- occur in the RHS; and simplNonRecX may therefore discard
             -- it via postInlineUnconditionally.
             -- Nevertheless we must keep it if the case-binder is alive,
             -- because it may be used in the con_app.  See Note [zapOccInfo]
           ; env'' <- simplNonRecX env' b' arg
           ; bind_args env'' bs' args }

    bind_args _ _ _ =
      pprPanic "bind_args" $ ppr dc $$ ppr bs $$ ppr dc_args $$
                             text "scrut:" <+> ppr scrut

       -- It's useful to bind bndr to scrut, rather than to a fresh
       -- binding      x = Con arg1 .. argn
       -- because very often the scrut is a variable, so we avoid
       -- creating, and then subsequently eliminating, a let-binding
       -- BUT, if scrut is a not a variable, we must be careful
       -- about duplicating the arg redexes; in that case, make
       -- a new con-app from the args
    bind_case_bndr env
      | isDeadBinder bndr   = return env
      | exprIsTrivial scrut = return (extendIdSubst env bndr (DoneEx scrut))
      | otherwise           = do { dc_args <- mapM (simplVar env) bs
      			      	         -- dc_ty_args are aready OutTypes, 
					 -- but bs are InBndrs
		    	         ; let con_app = Var (dataConWorkId dc) 
                          			 `mkTyApps` dc_ty_args      
                          			 `mkApps`   dc_args
      			         ; simplNonRecX env bndr con_app }
  
-------------------
missingAlt :: SimplEnv -> Id -> [InAlt] -> SimplCont -> SimplM (SimplEnv, OutExpr)
   		-- This isn't strictly an error, although it is unusual. 
		-- It's possible that the simplifer might "see" that 
		-- an inner case has no accessible alternatives before 
		-- it "sees" that the entire branch of an outer case is 
		-- inaccessible.  So we simply put an error case here instead.
missingAlt env case_bndr alts cont
  = WARN( True, ptext (sLit "missingAlt") <+> ppr case_bndr )
    return (env, mkImpossibleExpr res_ty)
  where
    res_ty = contResultType env (substTy env (coreAltsType alts)) cont

prepareCaseCont :: SimplEnv
                -> [InAlt] -> SimplCont
                -> SimplM (SimplEnv, SimplCont, SimplCont)
-- We are considering
--     K[case _ of { p1 -> r1; ...; pn -> rn }] 
-- where K is some enclosing continuation for the case
-- Goal: split K into two pieces Kdup,Knodup so that
-- 	 a) Kdup can be duplicated
--	 b) Knodup[Kdup[e]] = K[e]
-- The idea is that we'll transform thus:
--          Knodup[ (case _ of { p1 -> Kdup[r1]; ...; pn -> Kdup[rn] }
--
-- We also return some extra bindings in SimplEnv (that scope over 
-- the entire continuation)

prepareCaseCont env alts cont 
  | many_alts alts = mkDupableCont env cont 
  | otherwise      = return (env, cont, mkBoringStop)
  where
    many_alts :: [InAlt] -> Bool  -- True iff strictly > 1 non-bottom alternative
    many_alts []  = False   	  -- See Note [Bottom alternatives]
    many_alts [_] = False
    many_alts (alt:alts) 
      | is_bot_alt alt = many_alts alts   
      | otherwise      = not (all is_bot_alt alts)
  
    is_bot_alt (_,_,rhs) = exprIsBottom rhs

mkDupableCont :: SimplEnv -> SimplCont
              -> SimplM (SimplEnv, SimplCont, SimplCont)

mkDupableCont env cont
  | contIsDupable cont
  = return (env, cont, mkBoringStop)

mkDupableCont _   (Stop {}) = panic "mkDupableCont"     -- Handled by previous eqn

mkDupableCont env (CoerceIt ty cont)
  = do  { (env', dup, nodup) <- mkDupableCont env cont
        ; return (env', CoerceIt ty dup, nodup) }

mkDupableCont env cont@(StrictBind {})
  =  return (env, mkBoringStop, cont)
        -- See Note [Duplicating StrictBind]

mkDupableCont env (StrictArg info cci cont)
        -- See Note [Duplicating StrictArg]
  = do { (env', dup, nodup) <- mkDupableCont env cont
       ; (env'', args')     <- mapAccumLM (makeTrivial NotTopLevel) env' (ai_args info)
       ; return (env'', StrictArg (info { ai_args = args' }) cci dup, nodup) }

mkDupableCont env (ApplyTo _ arg se cont)
  =     -- e.g.         [...hole...] (...arg...)
        --      ==>
        --              let a = ...arg...
        --              in [...hole...] a
    do  { (env', dup_cont, nodup_cont) <- mkDupableCont env cont
        ; arg' <- simplExpr (se `setInScope` env') arg
        ; (env'', arg'') <- makeTrivial NotTopLevel env' arg'
        ; let app_cont = ApplyTo OkToDup arg'' (zapSubstEnv env'') dup_cont
        ; return (env'', app_cont, nodup_cont) }

mkDupableCont env cont@(Select _ case_bndr [(_, bs, _rhs)] _ _)
--  See Note [Single-alternative case]
--  | not (exprIsDupable rhs && contIsDupable case_cont)
--  | not (isDeadBinder case_bndr)
  | all isDeadBinder bs  -- InIds
    && not (isUnLiftedType (idType case_bndr))
    -- Note [Single-alternative-unlifted]
  = return (env, mkBoringStop, cont)

mkDupableCont env (Select _ case_bndr alts se cont)
  =     -- e.g.         (case [...hole...] of { pi -> ei })
        --      ===>
        --              let ji = \xij -> ei
        --              in case [...hole...] of { pi -> ji xij }
    do  { tick (CaseOfCase case_bndr)
        ; (env', dup_cont, nodup_cont) <- prepareCaseCont env alts cont
                -- NB: We call prepareCaseCont here.  If there is only one
		-- alternative, then dup_cont may be big, but that's ok
		-- becuase we push it into the single alternative, and then
		-- use mkDupableAlt to turn that simplified alternative into
		-- a join point if it's too big to duplicate.
		-- And this is important: see Note [Fusing case continuations]

        ; let alt_env = se `setInScope` env'
        ; (alt_env', case_bndr') <- simplBinder alt_env case_bndr
        ; alts' <- mapM (simplAlt alt_env' Nothing [] case_bndr' dup_cont) alts
        -- Safe to say that there are no handled-cons for the DEFAULT case
                -- NB: simplBinder does not zap deadness occ-info, so
                -- a dead case_bndr' will still advertise its deadness
                -- This is really important because in
                --      case e of b { (# p,q #) -> ... }
                -- b is always dead, and indeed we are not allowed to bind b to (# p,q #),
                -- which might happen if e was an explicit unboxed pair and b wasn't marked dead.
                -- In the new alts we build, we have the new case binder, so it must retain
                -- its deadness.
        -- NB: we don't use alt_env further; it has the substEnv for
        --     the alternatives, and we don't want that

        ; (env'', alts'') <- mkDupableAlts env' case_bndr' alts'
        ; return (env'',  -- Note [Duplicated env]
                  Select OkToDup case_bndr' alts'' (zapSubstEnv env'') mkBoringStop,
                  nodup_cont) }


mkDupableAlts :: SimplEnv -> OutId -> [InAlt]
              -> SimplM (SimplEnv, [InAlt])
-- Absorbs the continuation into the new alternatives

mkDupableAlts env case_bndr' the_alts
  = go env the_alts
  where
    go env0 [] = return (env0, [])
    go env0 (alt:alts)
        = do { (env1, alt') <- mkDupableAlt env0 case_bndr' alt
             ; (env2, alts') <- go env1 alts
             ; return (env2, alt' : alts' ) }

mkDupableAlt :: SimplEnv -> OutId -> (AltCon, [CoreBndr], CoreExpr)
              -> SimplM (SimplEnv, (AltCon, [CoreBndr], CoreExpr))
mkDupableAlt env case_bndr (con, bndrs', rhs')
  | exprIsDupable rhs'  -- Note [Small alternative rhs]
  = return (env, (con, bndrs', rhs'))
  | otherwise
  = do  { let rhs_ty'  = exprType rhs'
    	      scrut_ty = idType case_bndr
    	      case_bndr_w_unf	
                = case con of 
		      DEFAULT    -> case_bndr					
	      	      DataAlt dc -> setIdUnfolding case_bndr unf
		      	  where
			     	 -- See Note [Case binders and join points]
		      	     unf = mkInlineUnfolding Nothing rhs
		      	     rhs = mkConApp dc (map Type (tyConAppArgs scrut_ty)
			     	   	        ++ varsToCoreExprs bndrs')

		      LitAlt {} -> WARN( True, ptext (sLit "mkDupableAlt")
		      	     	   	        <+> ppr case_bndr <+> ppr con )
			           case_bndr
		      	   -- The case binder is alive but trivial, so why has 
		      	   -- it not been substituted away?

              used_bndrs' | isDeadBinder case_bndr = filter abstract_over bndrs'
			  | otherwise		   = bndrs' ++ [case_bndr_w_unf]
	      
              abstract_over bndr
                  | isTyVar bndr = True -- Abstract over all type variables just in case
                  | otherwise    = not (isDeadBinder bndr)
                        -- The deadness info on the new Ids is preserved by simplBinders

        ; (final_bndrs', final_args)    -- Note [Join point abstraction]
                <- if (any isId used_bndrs')
                   then return (used_bndrs', varsToCoreExprs used_bndrs')
                    else do { rw_id <- newId (fsLit "w") realWorldStatePrimTy
                            ; return ([rw_id], [Var realWorldPrimId]) }

        ; join_bndr <- newId (fsLit "$j") (mkPiTypes final_bndrs' rhs_ty')
                -- Note [Funky mkPiTypes]

        ; let   -- We make the lambdas into one-shot-lambdas.  The
                -- join point is sure to be applied at most once, and doing so
                -- prevents the body of the join point being floated out by
                -- the full laziness pass
                really_final_bndrs     = map one_shot final_bndrs'
                one_shot v | isId v    = setOneShotLambda v
                           | otherwise = v
                join_rhs  = mkLams really_final_bndrs rhs'
                join_call = mkApps (Var join_bndr) final_args

	; env' <- addPolyBind NotTopLevel env (NonRec join_bndr join_rhs)
        ; return (env', (con, bndrs', join_call)) }
                -- See Note [Duplicated env]