{-# OPTIONS -fno-warn-incomplete-patterns #-}
-- The above warning supression flag is a temporary kludge.
-- While working on this module you are encouraged to remove it and fix
-- any warnings in the module. See
--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
-- for details

-- | Commonly useful utilites for manipulating the Core language
module CoreUtils (
	-- * Constructing expressions
	mkSCC, mkCoerce, mkCoerceI,
	bindNonRec, needsCaseBinding,
	mkAltExpr, mkPiType, mkPiTypes,

	-- * Taking expressions apart
	findDefault, findAlt, isDefaultAlt, mergeAlts, trimConArgs,

	-- * Properties of expressions
	exprType, coreAltType, coreAltsType,
	exprIsDupable, exprIsTrivial, 
        exprIsCheap, exprIsExpandable, exprIsCheap', CheapAppFun,
	exprIsHNF, exprOkForSpeculation, exprIsBig, exprIsConLike,
	rhsIsStatic, isCheapApp, isExpandableApp,

	-- * Expression and bindings size
	coreBindsSize, exprSize,

	-- * Hashing
	hashExpr,

	-- * Equality
	cheapEqExpr, eqExpr, eqExprX,

	-- * Eta reduction
	tryEtaReduce,

	-- * Manipulating data constructors and types
	applyTypeToArgs, applyTypeToArg,
        dataConOrigInstPat, dataConRepInstPat, dataConRepFSInstPat
    ) where

#include "HsVersions.h"

import CoreSyn
import PprCore
import Var
import SrcLoc
import VarEnv
import VarSet
import Name
#if mingw32_TARGET_OS
import Packages
#endif
import Literal
import DataCon
import PrimOp
import Id
import IdInfo
import TcType	( isPredTy )
import Type
import Coercion
import TyCon
import CostCentre
import Unique
import Outputable
import TysPrim
import PrelNames( absentErrorIdKey )
import FastString
import Maybes
import Util
import Data.Word
import Data.Bits

exprType :: CoreExpr -> Type
-- ^ Recover the type of a well-typed Core expression. Fails when
-- applied to the actual 'CoreSyn.Type' expression as it cannot
-- really be said to have a type
exprType (Var var)	     = idType var
exprType (Lit lit)	     = literalType lit
exprType (Let _ body)	     = exprType body
exprType (Case _ _ ty _)     = ty
exprType (Cast _ co)         = snd (coercionKind co)
exprType (Note _ e)          = exprType e
exprType (Lam binder expr)   = mkPiType binder (exprType expr)
exprType e@(App _ _)
  = case collectArgs e of
	(fun, args) -> applyTypeToArgs e (exprType fun) args

exprType other = pprTrace "exprType" (pprCoreExpr other) alphaTy

coreAltType :: CoreAlt -> Type
-- ^ Returns the type of the alternatives right hand side
coreAltType (_,bs,rhs) 
  | any bad_binder bs = expandTypeSynonyms ty
  | otherwise         = ty    -- Note [Existential variables and silly type synonyms]
  where
    ty           = exprType rhs
    free_tvs     = tyVarsOfType ty
    bad_binder b = isTyCoVar b && b `elemVarSet` free_tvs

coreAltsType :: [CoreAlt] -> Type
-- ^ Returns the type of the first alternative, which should be the same as for all alternatives
coreAltsType (alt:_) = coreAltType alt
coreAltsType []	     = panic "corAltsType"

mkPiType  :: EvVar -> Type -> Type
-- ^ Makes a @(->)@ type or a forall type, depending
-- on whether it is given a type variable or a term variable.
mkPiTypes :: [EvVar] -> Type -> Type
-- ^ 'mkPiType' for multiple type or value arguments

mkPiType v ty
   | isId v    = mkFunTy (idType v) ty
   | otherwise = mkForAllTy v ty

mkPiTypes vs ty = foldr mkPiType ty vs

applyTypeToArg :: Type -> CoreExpr -> Type
-- ^ Determines the type resulting from applying an expression to a function with the given type
applyTypeToArg fun_ty (Type arg_ty) = applyTy fun_ty arg_ty
applyTypeToArg fun_ty _             = funResultTy fun_ty

applyTypeToArgs :: CoreExpr -> Type -> [CoreExpr] -> Type
-- ^ A more efficient version of 'applyTypeToArg' when we have several arguments.
-- The first argument is just for debugging, and gives some context
applyTypeToArgs _ op_ty [] = op_ty

applyTypeToArgs e op_ty (Type ty : args)
  =	-- Accumulate type arguments so we can instantiate all at once
    go [ty] args
  where
    go rev_tys (Type ty : args) = go (ty:rev_tys) args
    go rev_tys rest_args        = applyTypeToArgs e op_ty' rest_args
			 	where
				  op_ty' = applyTysD msg op_ty (reverse rev_tys)
				  msg = ptext (sLit "applyTypeToArgs") <+> 
		    			panic_msg e op_ty

applyTypeToArgs e op_ty (_ : args)
  = case (splitFunTy_maybe op_ty) of
	Just (_, res_ty) -> applyTypeToArgs e res_ty args
	Nothing -> pprPanic "applyTypeToArgs" (panic_msg e op_ty)

panic_msg :: CoreExpr -> Type -> SDoc
panic_msg e op_ty = pprCoreExpr e $$ ppr op_ty

-- | Wrap the given expression in the coercion, dropping identity coercions and coalescing nested coercions
mkCoerceI :: CoercionI -> CoreExpr -> CoreExpr
mkCoerceI (IdCo _) e = e
mkCoerceI (ACo co) e = mkCoerce co e

-- | Wrap the given expression in the coercion safely, coalescing nested coercions
mkCoerce :: Coercion -> CoreExpr -> CoreExpr
mkCoerce co (Cast expr co2)
  = ASSERT(let { (from_ty, _to_ty) = coercionKind co; 
                 (_from_ty2, to_ty2) = coercionKind co2} in
           from_ty `coreEqType` to_ty2 )
    mkCoerce (mkTransCoercion co2 co) expr

mkCoerce co expr 
  = let (from_ty, _to_ty) = coercionKind co in
--    if to_ty `coreEqType` from_ty
--    then expr
--    else 
        WARN(not (from_ty `coreEqType` exprType expr), text "Trying to coerce" <+> text "(" <> ppr expr $$ text "::" <+> ppr (exprType expr) <> text ")" $$ ppr co $$ pprEqPred (coercionKind co))
         (Cast expr co)

-- | Wraps the given expression in the cost centre unless
-- in a way that maximises their utility to the user
mkSCC :: CostCentre -> Expr b -> Expr b
	-- Note: Nested SCC's *are* preserved for the benefit of
	--       cost centre stack profiling
mkSCC _  (Lit lit)          = Lit lit
mkSCC cc (Lam x e)  	    = Lam x (mkSCC cc e)  -- Move _scc_ inside lambda
mkSCC cc (Note (SCC cc') e) = Note (SCC cc) (Note (SCC cc') e)
mkSCC cc (Note n e) 	    = Note n (mkSCC cc e) -- Move _scc_ inside notes
mkSCC cc (Cast e co)        = Cast (mkSCC cc e) co -- Move _scc_ inside cast
mkSCC cc expr	    	    = Note (SCC cc) expr

bindNonRec :: Id -> CoreExpr -> CoreExpr -> CoreExpr
-- ^ @bindNonRec x r b@ produces either:
--
-- > let x = r in b
--
-- or:
--
-- > case r of x { _DEFAULT_ -> b }
--
-- depending on whether we have to use a @case@ or @let@
-- binding for the expression (see 'needsCaseBinding').
-- It's used by the desugarer to avoid building bindings
-- that give Core Lint a heart attack, although actually
-- the simplifier deals with them perfectly well. See
-- also 'MkCore.mkCoreLet'
bindNonRec bndr rhs body 
  | needsCaseBinding (idType bndr) rhs = Case rhs bndr (exprType body) [(DEFAULT, [], body)]
  | otherwise			       = Let (NonRec bndr rhs) body

-- | Tests whether we have to use a @case@ rather than @let@ binding for this expression
-- as per the invariants of 'CoreExpr': see "CoreSyn#let_app_invariant"
needsCaseBinding :: Type -> CoreExpr -> Bool
needsCaseBinding ty rhs = isUnLiftedType ty && not (exprOkForSpeculation rhs)
	-- Make a case expression instead of a let
	-- These can arise either from the desugarer,
	-- or from beta reductions: (\x.e) (x +# y)

mkAltExpr :: AltCon     -- ^ Case alternative constructor
          -> [CoreBndr] -- ^ Things bound by the pattern match
          -> [Type]     -- ^ The type arguments to the case alternative
          -> CoreExpr
-- ^ This guy constructs the value that the scrutinee must have
-- given that you are in one particular branch of a case
mkAltExpr (DataAlt con) args inst_tys
  = mkConApp con (map Type inst_tys ++ varsToCoreExprs args)
mkAltExpr (LitAlt lit) [] []
  = Lit lit
mkAltExpr (LitAlt _) _ _ = panic "mkAltExpr LitAlt"
mkAltExpr DEFAULT _ _ = panic "mkAltExpr DEFAULT"

-- | Extract the default case alternative
findDefault :: [CoreAlt] -> ([CoreAlt], Maybe CoreExpr)
findDefault ((DEFAULT,args,rhs) : alts) = ASSERT( null args ) (alts, Just rhs)
findDefault alts			= 		      (alts, Nothing)

isDefaultAlt :: CoreAlt -> Bool
isDefaultAlt (DEFAULT, _, _) = True
isDefaultAlt _               = False


-- | Find the case alternative corresponding to a particular 
-- constructor: panics if no such constructor exists
findAlt :: AltCon -> [CoreAlt] -> Maybe CoreAlt
    -- A "Nothing" result *is* legitmiate
    -- See Note [Unreachable code]
findAlt con alts
  = case alts of
	(deflt@(DEFAULT,_,_):alts) -> go alts (Just deflt)
        _                          -> go alts Nothing
  where
    go []	 	      deflt = deflt
    go (alt@(con1,_,_) : alts) deflt
      =	case con `cmpAltCon` con1 of
	  LT -> deflt	-- Missed it already; the alts are in increasing order
	  EQ -> Just alt
	  GT -> ASSERT( not (con1 == DEFAULT) ) go alts deflt

---------------------------------
mergeAlts :: [CoreAlt] -> [CoreAlt] -> [CoreAlt]
-- ^ Merge alternatives preserving order; alternatives in
-- the first argument shadow ones in the second
mergeAlts [] as2 = as2
mergeAlts as1 [] = as1
mergeAlts (a1:as1) (a2:as2)
  = case a1 `cmpAlt` a2 of
	LT -> a1 : mergeAlts as1      (a2:as2)
	EQ -> a1 : mergeAlts as1      as2	-- Discard a2
	GT -> a2 : mergeAlts (a1:as1) as2


---------------------------------
trimConArgs :: AltCon -> [CoreArg] -> [CoreArg]
-- ^ Given:
--
-- > case (C a b x y) of
-- >        C b x y -> ...
--
-- We want to drop the leading type argument of the scrutinee
-- leaving the arguments to match agains the pattern

trimConArgs DEFAULT      args = ASSERT( null args ) []
trimConArgs (LitAlt _)   args = ASSERT( null args ) []
trimConArgs (DataAlt dc) args = dropList (dataConUnivTyVars dc) args

exprIsTrivial :: CoreExpr -> Bool
exprIsTrivial (Var _)          = True        -- See Note [Variables are trivial]
exprIsTrivial (Type _)         = True
exprIsTrivial (Lit lit)        = litIsTrivial lit
exprIsTrivial (App e arg)      = not (isRuntimeArg arg) && exprIsTrivial e
exprIsTrivial (Note _       e) = exprIsTrivial e  -- See Note [SCCs are trivial]
exprIsTrivial (Cast e _)       = exprIsTrivial e
exprIsTrivial (Lam b body)     = not (isRuntimeVar b) && exprIsTrivial body
exprIsTrivial _                = False

exprIsDupable :: CoreExpr -> Bool
exprIsDupable (Type _)   = True
exprIsDupable (Var _)    = True
exprIsDupable (Lit lit)  = litIsDupable lit
exprIsDupable (Note _ e) = exprIsDupable e
exprIsDupable (Cast e _) = exprIsDupable e
exprIsDupable expr
  = go expr 0
  where
    go (Var _)   _      = True
    go (App f a) n_args =  n_args < dupAppSize
			&& exprIsDupable a
			&& go f (n_args+1)
    go _         _      = False

dupAppSize :: Int
dupAppSize = 4		-- Size of application we are prepared to duplicate

exprIsCheap :: CoreExpr -> Bool
exprIsCheap = exprIsCheap' isCheapApp

exprIsExpandable :: CoreExpr -> Bool
exprIsExpandable = exprIsCheap' isExpandableApp	-- See Note [CONLIKE pragma] in BasicTypes

type CheapAppFun = Id -> Int -> Bool
exprIsCheap' :: CheapAppFun -> CoreExpr -> Bool
exprIsCheap' _          (Lit _)   = True
exprIsCheap' _          (Type _)  = True
exprIsCheap' _          (Var _)   = True
exprIsCheap' good_app (Note _ e)  = exprIsCheap' good_app e
exprIsCheap' good_app (Cast e _)  = exprIsCheap' good_app e
exprIsCheap' good_app (Lam x e)   = isRuntimeVar x
                                 || exprIsCheap' good_app e

exprIsCheap' good_app (Case e _ _ alts) = exprIsCheap' good_app e && 
				          and [exprIsCheap' good_app rhs | (_,_,rhs) <- alts]
	-- Experimentally, treat (case x of ...) as cheap
	-- (and case __coerce x etc.)
	-- This improves arities of overloaded functions where
	-- there is only dictionary selection (no construction) involved

exprIsCheap' good_app (Let (NonRec x _) e)  
  | isUnLiftedType (idType x) = exprIsCheap' good_app e
  | otherwise		      = False
	-- Strict lets always have cheap right hand sides,
	-- and do no allocation, so just look at the body
	-- Non-strict lets do allocation so we don't treat them as cheap
	-- See also 

exprIsCheap' good_app other_expr 	-- Applications and variables
  = go other_expr []
  where
	-- Accumulate value arguments, then decide
    go (Cast e _) val_args                 = go e val_args
    go (App f a) val_args | isRuntimeArg a = go f (a:val_args)
			  | otherwise      = go f val_args

    go (Var _) [] = True	-- Just a type application of a variable
				-- (f t1 t2 t3) counts as WHNF
    go (Var f) args
 	= case idDetails f of
		RecSelId {}  	    	     -> go_sel args
		ClassOpId {} 	    	     -> go_sel args
		PrimOpId op  	    	     -> go_primop op args
		_ | good_app f (length args) -> go_pap args
                  | isBottomingId f 	     -> True
                  | otherwise       	     -> False
			-- Application of a function which
			-- always gives bottom; we treat this as cheap
			-- because it certainly doesn't need to be shared!
	
    go _ _ = False
 
    --------------
    go_pap args = all exprIsTrivial args
 	-- For constructor applications and primops, check that all
 	-- the args are trivial.  We don't want to treat as cheap, say,
 	-- 	(1:2:3:4:5:[])
 	-- We'll put up with one constructor application, but not dozens
 	
    --------------
    go_primop op args = primOpIsCheap op && all (exprIsCheap' good_app) args
 	-- In principle we should worry about primops
 	-- that return a type variable, since the result
 	-- might be applied to something, but I'm not going
 	-- to bother to check the number of args
 
    --------------
    go_sel [arg] = exprIsCheap' good_app arg	-- I'm experimenting with making record selection
    go_sel _     = False		-- look cheap, so we will substitute it inside a
 					-- lambda.  Particularly for dictionary field selection.
  		-- BUT: Take care with (sel d x)!  The (sel d) might be cheap, but
  		--	there's no guarantee that (sel d x) will be too.  Hence (n_val_args == 1)

isCheapApp :: CheapAppFun
isCheapApp fn n_val_args
  = isDataConWorkId fn 
  || n_val_args < idArity fn

isExpandableApp :: CheapAppFun
isExpandableApp fn n_val_args
  =  isConLikeId fn
  || n_val_args < idArity fn
  || go n_val_args (idType fn)
  where
  -- See if all the arguments are PredTys (implicit params or classes)
  -- If so we'll regard it as expandable; see Note [Expandable overloadings]
     go 0 _ = True
     go n_val_args ty 
       | Just (_, ty) <- splitForAllTy_maybe ty   = go n_val_args ty
       | Just (arg, ty) <- splitFunTy_maybe ty
       , isPredTy arg                             = go (n_val_args-1) ty
       | otherwise                                = False

-- | 'exprOkForSpeculation' returns True of an expression that is:
--
--  * Safe to evaluate even if normal order eval might not 
--    evaluate the expression at all, or
--
--  * Safe /not/ to evaluate even if normal order would do so
--
-- Precisely, it returns @True@ iff:
--
--  * The expression guarantees to terminate, 
--  * soon, 
--  * without raising an exception,
--  * without causing a side effect (e.g. writing a mutable variable)
--
-- Note that if @exprIsHNF e@, then @exprOkForSpecuation e@.
-- As an example of the considerations in this test, consider:
--
-- > let x = case y# +# 1# of { r# -> I# r# }
-- > in E
--
-- being translated to:
--
-- > case y# +# 1# of { r# -> 
-- >    let x = I# r#
-- >    in E 
-- > }
-- 
-- We can only do this if the @y + 1@ is ok for speculation: it has no
-- side effects, and can't diverge or raise an exception.
exprOkForSpeculation :: CoreExpr -> Bool
exprOkForSpeculation (Lit _)     = True
exprOkForSpeculation (Type _)    = True
    -- Tick boxes are *not* suitable for speculation
exprOkForSpeculation (Var v)     = isUnLiftedType (idType v)
				 && not (isTickBoxOp v)
exprOkForSpeculation (Note _ e)  = exprOkForSpeculation e
exprOkForSpeculation (Cast e _)  = exprOkForSpeculation e

exprOkForSpeculation (Case e _ _ alts) 
  =  exprOkForSpeculation e  -- Note [exprOkForSpeculation: case expressions]
  && all (\(_,_,rhs) -> exprOkForSpeculation rhs) alts

exprOkForSpeculation other_expr
  = case collectArgs other_expr of
	(Var f, args) | f `hasKey` absentErrorIdKey	-- Note [Absent error Id]
                      -> all exprOkForSpeculation args  --    in WwLib
                      | otherwise 
                      -> spec_ok (idDetails f) args
        _             -> False
 
  where
    spec_ok (DataConWorkId _) _
      = True	-- The strictness of the constructor has already
		-- been expressed by its "wrapper", so we don't need
		-- to take the arguments into account

    spec_ok (PrimOpId op) args
      | isDivOp op,		-- Special case for dividing operations that fail
	[arg1, Lit lit] <- args	-- only if the divisor is zero
      = not (isZeroLit lit) && exprOkForSpeculation arg1
		-- Often there is a literal divisor, and this 
		-- can get rid of a thunk in an inner looop

      | otherwise
      = primOpOkForSpeculation op && 
	all exprOkForSpeculation args
				-- A bit conservative: we don't really need
				-- to care about lazy arguments, but this is easy

    spec_ok (DFunId _ new_type) _ = not new_type
         -- DFuns terminate, unless the dict is implemented with a newtype
	 -- in which case they may not

    spec_ok _ _ = False

-- | True of dyadic operators that can fail only if the second arg is zero!
isDivOp :: PrimOp -> Bool
-- This function probably belongs in PrimOp, or even in 
-- an automagically generated file.. but it's such a 
-- special case I thought I'd leave it here for now.
isDivOp IntQuotOp	 = True
isDivOp IntRemOp	 = True
isDivOp WordQuotOp	 = True
isDivOp WordRemOp	 = True
isDivOp FloatDivOp       = True
isDivOp DoubleDivOp      = True
isDivOp _                = False

-- Note [exprIsHNF]		See also Note [exprIsCheap and exprIsHNF]
-- ~~~~~~~~~~~~~~~~
-- | exprIsHNF returns true for expressions that are certainly /already/ 
-- evaluated to /head/ normal form.  This is used to decide whether it's ok 
-- to change:
--
-- > case x of _ -> e
--
--    into:
--
-- > e
--
-- and to decide whether it's safe to discard a 'seq'.
-- 
-- So, it does /not/ treat variables as evaluated, unless they say they are.
-- However, it /does/ treat partial applications and constructor applications
-- as values, even if their arguments are non-trivial, provided the argument
-- type is lifted. For example, both of these are values:
--
-- > (:) (f x) (map f xs)
-- > map (...redex...)
--
-- because 'seq' on such things completes immediately.
--
-- For unlifted argument types, we have to be careful:
--
-- > C (f x :: Int#)
--
-- Suppose @f x@ diverges; then @C (f x)@ is not a value. However this can't 
-- happen: see "CoreSyn#let_app_invariant". This invariant states that arguments of
-- unboxed type must be ok-for-speculation (or trivial).
exprIsHNF :: CoreExpr -> Bool		-- True => Value-lambda, constructor, PAP
exprIsHNF = exprIsHNFlike isDataConWorkId isEvaldUnfolding

-- | Similar to 'exprIsHNF' but includes CONLIKE functions as well as
-- data constructors. Conlike arguments are considered interesting by the
-- inliner.
exprIsConLike :: CoreExpr -> Bool	-- True => lambda, conlike, PAP
exprIsConLike = exprIsHNFlike isConLikeId isConLikeUnfolding

-- | Returns true for values or value-like expressions. These are lambdas,
-- constructors / CONLIKE functions (as determined by the function argument)
-- or PAPs.
--
exprIsHNFlike :: (Var -> Bool) -> (Unfolding -> Bool) -> CoreExpr -> Bool
exprIsHNFlike is_con is_con_unf = is_hnf_like
  where
    is_hnf_like (Var v) -- NB: There are no value args at this point
      =  is_con v   	-- Catches nullary constructors, 
			--	so that [] and () are values, for example
      || idArity v > 0 	-- Catches (e.g.) primops that don't have unfoldings
      || is_con_unf (idUnfolding v)
	-- Check the thing's unfolding; it might be bound to a value
	-- We don't look through loop breakers here, which is a bit conservative
	-- but otherwise I worry that if an Id's unfolding is just itself, 
	-- we could get an infinite loop

    is_hnf_like (Lit _)          = True
    is_hnf_like (Type _)         = True       -- Types are honorary Values;
                                              -- we don't mind copying them
    is_hnf_like (Lam b e)        = isRuntimeVar b || is_hnf_like e
    is_hnf_like (Note _ e)       = is_hnf_like e
    is_hnf_like (Cast e _)       = is_hnf_like e
    is_hnf_like (App e (Type _)) = is_hnf_like e
    is_hnf_like (App e a)        = app_is_value e [a]
    is_hnf_like (Let _ e)        = is_hnf_like e  -- Lazy let(rec)s don't affect us
    is_hnf_like _                = False

    -- There is at least one value argument
    app_is_value :: CoreExpr -> [CoreArg] -> Bool
    app_is_value (Var fun) args
      = idArity fun > valArgCount args	  -- Under-applied function
        || is_con fun    		  --  or constructor-like
    app_is_value (Note _ f) as = app_is_value f as
    app_is_value (Cast f _) as = app_is_value f as
    app_is_value (App f a)  as = app_is_value f (a:as)
    app_is_value _          _  = False

dataConRepInstPat, dataConOrigInstPat :: [Unique] -> DataCon -> [Type] -> ([TyVar], [CoVar], [Id])
dataConRepFSInstPat :: [FastString] -> [Unique] -> DataCon -> [Type] -> ([TyVar], [CoVar], [Id])

dataConRepInstPat   = dataConInstPat dataConRepArgTys (repeat ((fsLit "ipv")))
dataConRepFSInstPat = dataConInstPat dataConRepArgTys
dataConOrigInstPat  = dataConInstPat dc_arg_tys       (repeat ((fsLit "ipv")))
  where 
    dc_arg_tys dc = map mkPredTy (dataConEqTheta dc) ++ map mkPredTy (dataConDictTheta dc) ++ dataConOrigArgTys dc
	-- Remember to include the existential dictionaries

dataConInstPat :: (DataCon -> [Type])      -- function used to find arg tys
                  -> [FastString]          -- A long enough list of FSs to use for names
                  -> [Unique]              -- An equally long list of uniques, at least one for each binder
                  -> DataCon
	          -> [Type]                -- Types to instantiate the universally quantified tyvars
	       -> ([TyVar], [CoVar], [Id]) -- Return instantiated variables
-- dataConInstPat arg_fun fss us con inst_tys returns a triple 
-- (ex_tvs, co_tvs, arg_ids),
--
--   ex_tvs are intended to be used as binders for existential type args
--
--   co_tvs are intended to be used as binders for coercion args and the kinds
--     of these vars have been instantiated by the inst_tys and the ex_tys
--     The co_tvs include both GADT equalities (dcEqSpec) and 
--     programmer-specified equalities (dcEqTheta)
--
--   arg_ids are indended to be used as binders for value arguments, 
--     and their types have been instantiated with inst_tys and ex_tys
--     The arg_ids include both dicts (dcDictTheta) and
--     programmer-specified arguments (after rep-ing) (deRepArgTys)
--
-- Example.
--  The following constructor T1
--
--  data T a where
--    T1 :: forall b. Int -> b -> T(a,b)
--    ...
--
--  has representation type 
--   forall a. forall a1. forall b. (a ~ (a1,b)) => 
--     Int -> b -> T a
--
--  dataConInstPat fss us T1 (a1',b') will return
--
--  ([a1'', b''], [c :: (a1', b')~(a1'', b'')], [x :: Int, y :: b''])
--
--  where the double-primed variables are created with the FastStrings and
--  Uniques given as fss and us
dataConInstPat arg_fun fss uniqs con inst_tys 
  = (ex_bndrs, co_bndrs, arg_ids)
  where 
    univ_tvs = dataConUnivTyVars con
    ex_tvs   = dataConExTyVars con
    arg_tys  = arg_fun con
    eq_spec  = dataConEqSpec con
    eq_theta = dataConEqTheta con
    eq_preds = eqSpecPreds eq_spec ++ eq_theta

    n_ex = length ex_tvs
    n_co = length eq_preds

      -- split the Uniques and FastStrings
    (ex_uniqs, uniqs')   = splitAt n_ex uniqs
    (co_uniqs, id_uniqs) = splitAt n_co uniqs'

    (ex_fss, fss')     = splitAt n_ex fss
    (co_fss, id_fss)   = splitAt n_co fss'

      -- Make existential type variables
    ex_bndrs = zipWith3 mk_ex_var ex_uniqs ex_fss ex_tvs
    mk_ex_var uniq fs var = mkTyVar new_name kind
      where
        new_name = mkSysTvName uniq fs
        kind     = tyVarKind var

      -- Make the instantiating substitution
    subst = zipOpenTvSubst (univ_tvs ++ ex_tvs) (inst_tys ++ map mkTyVarTy ex_bndrs)

      -- Make new coercion vars, instantiating kind
    co_bndrs = zipWith3 mk_co_var co_uniqs co_fss eq_preds
    mk_co_var uniq fs eq_pred = mkCoVar new_name co_kind
       where
         new_name = mkSysTvName uniq fs
         co_kind  = substTy subst (mkPredTy eq_pred)

      -- make value vars, instantiating types
    mk_id_var uniq fs ty = mkUserLocal (mkVarOccFS fs) uniq (substTy subst ty) noSrcSpan
    arg_ids = zipWith3 mk_id_var id_uniqs id_fss arg_tys

-- | A cheap equality test which bales out fast!
--      If it returns @True@ the arguments are definitely equal,
--      otherwise, they may or may not be equal.
--
-- See also 'exprIsBig'
cheapEqExpr :: Expr b -> Expr b -> Bool

cheapEqExpr (Var v1)   (Var v2)   = v1==v2
cheapEqExpr (Lit lit1) (Lit lit2) = lit1 == lit2
cheapEqExpr (Type t1)  (Type t2)  = t1 `coreEqType` t2

cheapEqExpr (App f1 a1) (App f2 a2)
  = f1 `cheapEqExpr` f2 && a1 `cheapEqExpr` a2

cheapEqExpr (Cast e1 t1) (Cast e2 t2)
  = e1 `cheapEqExpr` e2 && t1 `coreEqCoercion` t2

cheapEqExpr _ _ = False

exprIsBig :: Expr b -> Bool
-- ^ Returns @True@ of expressions that are too big to be compared by 'cheapEqExpr'
exprIsBig (Lit _)      = False
exprIsBig (Var _)      = False
exprIsBig (Type _)     = False
exprIsBig (Lam _ e)    = exprIsBig e
exprIsBig (App f a)    = exprIsBig f || exprIsBig a
exprIsBig (Cast e _)   = exprIsBig e	-- Hopefully coercions are not too big!
exprIsBig _            = True

eqExpr :: InScopeSet -> CoreExpr -> CoreExpr -> Bool
-- Compares for equality, modulo alpha
eqExpr in_scope e1 e2
  = eqExprX id_unf (mkRnEnv2 in_scope) e1 e2
  where
    id_unf _ = noUnfolding	-- Don't expand

eqExprX :: IdUnfoldingFun -> RnEnv2 -> CoreExpr -> CoreExpr -> Bool
-- ^ Compares expressions for equality, modulo alpha.
-- Does /not/ look through newtypes or predicate types
-- Used in rule matching, and also CSE

eqExprX id_unfolding_fun env e1 e2
  = go env e1 e2
  where
    go env (Var v1) (Var v2)
      | rnOccL env v1 == rnOccR env v2
      = True

    -- The next two rules expand non-local variables
    -- C.f. Note [Expanding variables] in Rules.lhs
    -- and  Note [Do not expand locally-bound variables] in Rules.lhs
    go env (Var v1) e2
      | not (locallyBoundL env v1)
      , Just e1' <- expandUnfolding_maybe (id_unfolding_fun (lookupRnInScope env v1))
      = go (nukeRnEnvL env) e1' e2

    go env e1 (Var v2)
      | not (locallyBoundR env v2)
      , Just e2' <- expandUnfolding_maybe (id_unfolding_fun (lookupRnInScope env v2))
      = go (nukeRnEnvR env) e1 e2'

    go _   (Lit lit1)    (Lit lit2)    = lit1 == lit2
    go env (Type t1)     (Type t2)     = tcEqTypeX env t1 t2
    go env (Cast e1 co1) (Cast e2 co2) = tcEqTypeX env co1 co2 && go env e1 e2
    go env (App f1 a1)   (App f2 a2)   = go env f1 f2 && go env a1 a2
    go env (Note n1 e1)  (Note n2 e2)  = go_note n1 n2 && go env e1 e2

    go env (Lam b1 e1)  (Lam b2 e2)  
      =  tcEqTypeX env (varType b1) (varType b2)   -- False for Id/TyVar combination
      && go (rnBndr2 env b1 b2) e1 e2

    go env (Let (NonRec v1 r1) e1) (Let (NonRec v2 r2) e2) 
      =  go env r1 r2  -- No need to check binder types, since RHSs match
      && go (rnBndr2 env v1 v2) e1 e2

    go env (Let (Rec ps1) e1) (Let (Rec ps2) e2) 
      = all2 (go env') rs1 rs2 && go env' e1 e2
      where
        (bs1,rs1) = unzip ps1	   
        (bs2,rs2) = unzip ps2
        env' = rnBndrs2 env bs1 bs2

    go env (Case e1 b1 _ a1) (Case e2 b2 _ a2)
      =  go env e1 e2
      && tcEqTypeX env (idType b1) (idType b2)
      && all2 (go_alt (rnBndr2 env b1 b2)) a1 a2

    go _ _ _ = False

    -----------
    go_alt env (c1, bs1, e1) (c2, bs2, e2)
      = c1 == c2 && go (rnBndrs2 env bs1 bs2) e1 e2

    -----------
    go_note (SCC cc1)     (SCC cc2)      = cc1 == cc2
    go_note (CoreNote s1) (CoreNote s2)  = s1 == s2
    go_note _             _              = False

locallyBoundL, locallyBoundR :: RnEnv2 -> Var -> Bool
locallyBoundL rn_env v = inRnEnvL rn_env v
locallyBoundR rn_env v = inRnEnvR rn_env v

coreBindsSize :: [CoreBind] -> Int
coreBindsSize bs = foldr ((+) . bindSize) 0 bs

exprSize :: CoreExpr -> Int
-- ^ A measure of the size of the expressions, strictly greater than 0
-- It also forces the expression pretty drastically as a side effect
exprSize (Var v)         = v `seq` 1
exprSize (Lit lit)       = lit `seq` 1
exprSize (App f a)       = exprSize f + exprSize a
exprSize (Lam b e)       = varSize b + exprSize e
exprSize (Let b e)       = bindSize b + exprSize e
exprSize (Case e b t as) = seqType t `seq` exprSize e + varSize b + 1 + foldr ((+) . altSize) 0 as
exprSize (Cast e co)     = (seqType co `seq` 1) + exprSize e
exprSize (Note n e)      = noteSize n + exprSize e
exprSize (Type t)        = seqType t `seq` 1

noteSize :: Note -> Int
noteSize (SCC cc)       = cc `seq` 1
noteSize (CoreNote s)   = s `seq` 1  -- hdaume: core annotations
 
varSize :: Var -> Int
varSize b  | isTyCoVar b = 1
	   | otherwise = seqType (idType b)		`seq`
			 megaSeqIdInfo (idInfo b) 	`seq`
			 1

varsSize :: [Var] -> Int
varsSize = sum . map varSize

bindSize :: CoreBind -> Int
bindSize (NonRec b e) = varSize b + exprSize e
bindSize (Rec prs)    = foldr ((+) . pairSize) 0 prs

pairSize :: (Var, CoreExpr) -> Int
pairSize (b,e) = varSize b + exprSize e

altSize :: CoreAlt -> Int
altSize (c,bs,e) = c `seq` varsSize bs + exprSize e

hashExpr :: CoreExpr -> Int
-- ^ Two expressions that hash to the same @Int@ may be equal (but may not be)
-- Two expressions that hash to the different Ints are definitely unequal.
--
-- The emphasis is on a crude, fast hash, rather than on high precision.
-- 
-- But unequal here means \"not identical\"; two alpha-equivalent 
-- expressions may hash to the different Ints.
--
-- We must be careful that @\\x.x@ and @\\y.y@ map to the same hash code,
-- (at least if we want the above invariant to be true).

hashExpr e = fromIntegral (hash_expr (1,emptyVarEnv) e .&. 0x7fffffff)
             -- UniqFM doesn't like negative Ints

type HashEnv = (Int, VarEnv Int)  -- Hash code for bound variables

hash_expr :: HashEnv -> CoreExpr -> Word32
-- Word32, because we're expecting overflows here, and overflowing
-- signed types just isn't cool.  In C it's even undefined.
hash_expr env (Note _ e)   	      = hash_expr env e
hash_expr env (Cast e _)              = hash_expr env e
hash_expr env (Var v)     	      = hashVar env v
hash_expr _   (Lit lit)               = fromIntegral (hashLiteral lit)
hash_expr env (App f e)   	      = hash_expr env f * fast_hash_expr env e
hash_expr env (Let (NonRec b r) e)    = hash_expr (extend_env env b) e * fast_hash_expr env r
hash_expr env (Let (Rec ((b,_):_)) e) = hash_expr (extend_env env b) e
hash_expr env (Case e _ _ _)	      = hash_expr env e
hash_expr env (Lam b e)	              = hash_expr (extend_env env b) e
hash_expr _   (Type _)                = WARN(True, text "hash_expr: type") 1
-- Shouldn't happen.  Better to use WARN than trace, because trace
-- prevents the CPR optimisation kicking in for hash_expr.

fast_hash_expr :: HashEnv -> CoreExpr -> Word32
fast_hash_expr env (Var v)     	= hashVar env v
fast_hash_expr env (Type t)	= fast_hash_type env t
fast_hash_expr _   (Lit lit)    = fromIntegral (hashLiteral lit)
fast_hash_expr env (Cast e _)   = fast_hash_expr env e
fast_hash_expr env (Note _ e)   = fast_hash_expr env e
fast_hash_expr env (App _ a)    = fast_hash_expr env a	-- A bit idiosyncratic ('a' not 'f')!
fast_hash_expr _   _            = 1

fast_hash_type :: HashEnv -> Type -> Word32
fast_hash_type env ty 
  | Just tv <- getTyVar_maybe ty            = hashVar env tv
  | Just (tc,tys) <- splitTyConApp_maybe ty = let hash_tc = fromIntegral (hashName (tyConName tc))
					      in foldr (\t n -> fast_hash_type env t + n) hash_tc tys
  | otherwise				    = 1

extend_env :: HashEnv -> Var -> (Int, VarEnv Int)
extend_env (n,env) b = (n+1, extendVarEnv env b n)

hashVar :: HashEnv -> Var -> Word32
hashVar (_,env) v
 = fromIntegral (lookupVarEnv env v `orElse` hashName (idName v))

tryEtaReduce :: [Var] -> CoreExpr -> Maybe CoreExpr
tryEtaReduce bndrs body 
  = go (reverse bndrs) body (IdCo (exprType body))
  where
    incoming_arity = count isId bndrs

    go :: [Var]	           -- Binders, innermost first, types [a3,a2,a1]
       -> CoreExpr         -- Of type tr
       -> CoercionI        -- Of type tr ~ ts
       -> Maybe CoreExpr   -- Of type a1 -> a2 -> a3 -> ts
    -- See Note [Eta reduction with casted arguments]
    -- for why we have an accumulating coercion
    go [] fun co
      | ok_fun fun = Just (mkCoerceI co fun)

    go (b : bs) (App fun arg) co
      | Just co' <- ok_arg b arg co
      = go bs fun co'

    go _ _ _  = Nothing		-- Failure!

    ---------------
    -- Note [Eta reduction conditions]
    ok_fun (App fun (Type ty)) 
	| not (any (`elemVarSet` tyVarsOfType ty) bndrs)
	=  ok_fun fun
    ok_fun (Var fun_id)
	=  not (fun_id `elem` bndrs)
	&& (ok_fun_id fun_id || all ok_lam bndrs)
    ok_fun _fun = False

    ---------------
    ok_fun_id fun = fun_arity fun >= incoming_arity

    ---------------
    fun_arity fun 	      -- See Note [Arity care]
       | isLocalId fun && isLoopBreaker (idOccInfo fun) = 0
       | otherwise = idArity fun   	      

    ---------------
    ok_lam v = isTyCoVar v || isDictId v

    ---------------
    ok_arg :: Var 	        -- Of type bndr_t
           -> CoreExpr          -- Of type arg_t
           -> CoercionI         -- Of kind (t1~t2)
           -> Maybe CoercionI   -- Of type (arg_t -> t1 ~  bndr_t -> t2)
	      	    		--   (and similarly for tyvars, coercion args)
    -- See Note [Eta reduction with casted arguments]
    ok_arg bndr (Type ty) co
       | Just tv <- getTyVar_maybe ty
       , bndr == tv  = Just (mkForAllTyCoI tv co)
    ok_arg bndr (Var v) co
       | bndr == v   = Just (mkFunTyCoI (IdCo (idType bndr)) co)
    ok_arg bndr (Cast (Var v) co_arg) co
       | bndr == v  = Just (mkFunTyCoI (ACo (mkSymCoercion co_arg)) co)
       -- The simplifier combines multiple casts into one, 
       -- so we can have a simple-minded pattern match here
    ok_arg _ _ _ = Nothing

-- | This function is called only on *top-level* right-hand sides.
-- Returns @True@ if the RHS can be allocated statically in the output,
-- with no thunks involved at all.
rhsIsStatic :: (Name -> Bool) -> CoreExpr -> Bool
-- It's called (i) in TidyPgm.hasCafRefs to decide if the rhs is, or
-- refers to, CAFs; (ii) in CoreToStg to decide whether to put an
-- update flag on it and (iii) in DsExpr to decide how to expand
-- list literals
--
-- The basic idea is that rhsIsStatic returns True only if the RHS is
--	(a) a value lambda
--	(b) a saturated constructor application with static args
--
-- BUT watch out for
--  (i)	Any cross-DLL references kill static-ness completely
--	because they must be 'executed' not statically allocated
--      ("DLL" here really only refers to Windows DLLs, on other platforms,
--      this is not necessary)
--
-- (ii) We treat partial applications as redexes, because in fact we 
--	make a thunk for them that runs and builds a PAP
-- 	at run-time.  The only appliations that are treated as 
--	static are *saturated* applications of constructors.

-- We used to try to be clever with nested structures like this:
--		ys = (:) w ((:) w [])
-- on the grounds that CorePrep will flatten ANF-ise it later.
-- But supporting this special case made the function much more 
-- complicated, because the special case only applies if there are no 
-- enclosing type lambdas:
--		ys = /\ a -> Foo (Baz ([] a))
-- Here the nested (Baz []) won't float out to top level in CorePrep.
--
-- But in fact, even without -O, nested structures at top level are 
-- flattened by the simplifier, so we don't need to be super-clever here.
--
-- Examples
--
--	f = \x::Int. x+7	TRUE
--	p = (True,False)	TRUE
--
--	d = (fst p, False)	FALSE because there's a redex inside
--				(this particular one doesn't happen but...)
--
--	h = D# (1.0## /## 2.0##)	FALSE (redex again)
--	n = /\a. Nil a			TRUE
--
--	t = /\a. (:) (case w a of ...) (Nil a)	FALSE (redex)
--
--
-- This is a bit like CoreUtils.exprIsHNF, with the following differences:
--    a) scc "foo" (\x -> ...) is updatable (so we catch the right SCC)
--
--    b) (C x xs), where C is a contructor is updatable if the application is
--	   dynamic
-- 
--    c) don't look through unfolding of f in (f x).

rhsIsStatic _is_dynamic_name rhs = is_static False rhs
  where
  is_static :: Bool	-- True <=> in a constructor argument; must be atomic
  	  -> CoreExpr -> Bool
  
  is_static False (Lam b e)   = isRuntimeVar b || is_static False e
  is_static in_arg (Note n e) = notSccNote n && is_static in_arg e
  is_static in_arg (Cast e _) = is_static in_arg e
  
  is_static _      (Lit lit)
    = case lit of
  	MachLabel _ _ _ -> False
        _             -> True
  	-- A MachLabel (foreign import "&foo") in an argument
  	-- prevents a constructor application from being static.  The
  	-- reason is that it might give rise to unresolvable symbols
  	-- in the object file: under Linux, references to "weak"
  	-- symbols from the data segment give rise to "unresolvable
  	-- relocation" errors at link time This might be due to a bug
  	-- in the linker, but we'll work around it here anyway. 
  	-- SDM 24/2/2004
  
  is_static in_arg other_expr = go other_expr 0
   where
    go (Var f) n_val_args
#if mingw32_TARGET_OS
        | not (_is_dynamic_name (idName f))
#endif
	=  saturated_data_con f n_val_args
	|| (in_arg && n_val_args == 0)	
		-- A naked un-applied variable is *not* deemed a static RHS
		-- E.g.		f = g
		-- Reason: better to update so that the indirection gets shorted
		-- 	   out, and the true value will be seen
		-- NB: if you change this, you'll break the invariant that THUNK_STATICs
		--     are always updatable.  If you do so, make sure that non-updatable
		--     ones have enough space for their static link field!

    go (App f a) n_val_args
	| isTypeArg a 			 = go f n_val_args
	| not in_arg && is_static True a = go f (n_val_args + 1)
	-- The (not in_arg) checks that we aren't in a constructor argument;
	-- if we are, we don't allow (value) applications of any sort
	-- 
        -- NB. In case you wonder, args are sometimes not atomic.  eg.
        --   x = D# (1.0## /## 2.0##)
        -- can't float because /## can fail.

    go (Note n f) n_val_args = notSccNote n && go f n_val_args
    go (Cast e _) n_val_args = go e n_val_args
    go _          _          = False

    saturated_data_con f n_val_args
	= case isDataConWorkId_maybe f of
	    Just dc -> n_val_args == dataConRepArity dc
	    Nothing -> False