-- | Functions for collecting together and applying rewrite rules to a module.
-- The 'CoreRule' datatype itself is declared elsewhere.
module Rules (
	-- * RuleBase
	RuleBase, 
	
	-- ** Constructing 
	emptyRuleBase, mkRuleBase, extendRuleBaseList, 
	unionRuleBase, pprRuleBase, 
	
	-- ** Checking rule applications
	ruleCheckProgram,

        -- ** Manipulating 'SpecInfo' rules
	mkSpecInfo, extendSpecInfo, addSpecInfo,
	addIdSpecialisations, 
	
	-- * Misc. CoreRule helpers
        rulesOfBinds, getRules, pprRulesForUser, 
        
        lookupRule, mkRule, roughTopNames
    ) where

#include "HsVersions.h"

import CoreSyn		-- All of it
import CoreSubst
import OccurAnal        ( occurAnalyseExpr )
import CoreFVs		( exprFreeVars, exprsFreeVars, bindFreeVars, rulesFreeVars )
import CoreUtils        ( exprType, eqExpr )
import PprCore		( pprRules )
import Type             ( Type )
import TcType		( tcSplitTyConApp_maybe )
import Coercion
import CoreTidy		( tidyRules )
import Id
import IdInfo		( SpecInfo( SpecInfo ) )
import VarEnv
import VarSet
import Name		( Name, NamedThing(..) )
import NameEnv
import Unify 		( ruleMatchTyX, MatchEnv(..) )
import BasicTypes	( Activation, CompilerPhase, isActive )
import StaticFlags	( opt_PprStyle_Debug )
import Outputable
import FastString
import Maybes
import Bag
import Util
import Data.List

mkRule :: Bool -> Bool -> RuleName -> Activation 
       -> Name -> [CoreBndr] -> [CoreExpr] -> CoreExpr -> CoreRule
-- ^ Used to make 'CoreRule' for an 'Id' defined in the module being 
-- compiled. See also 'CoreSyn.CoreRule'
mkRule is_auto is_local name act fn bndrs args rhs
  = Rule { ru_name = name, ru_fn = fn, ru_act = act,
	   ru_bndrs = bndrs, ru_args = args,
	   ru_rhs = occurAnalyseExpr rhs, 
	   ru_rough = roughTopNames args,
	   ru_auto = is_auto, ru_local = is_local }

--------------
roughTopNames :: [CoreExpr] -> [Maybe Name]
-- ^ Find the \"top\" free names of several expressions. 
-- Such names are either:
--
-- 1. The function finally being applied to in an application chain
--    (if that name is a GlobalId: see "Var#globalvslocal"), or
--
-- 2. The 'TyCon' if the expression is a 'Type'
--
-- This is used for the fast-match-check for rules; 
--	if the top names don't match, the rest can't
roughTopNames args = map roughTopName args

roughTopName :: CoreExpr -> Maybe Name
roughTopName (Type ty) = case tcSplitTyConApp_maybe ty of
                               Just (tc,_) -> Just (getName tc)
                               Nothing     -> Nothing
roughTopName (Coercion _) = Nothing 
roughTopName (App f _) = roughTopName f
roughTopName (Var f)   | isGlobalId f	-- Note [Care with roughTopName]
                       , isDataConWorkId f || idArity f > 0
                       = Just (idName f)
roughTopName _ = Nothing

ruleCantMatch :: [Maybe Name] -> [Maybe Name] -> Bool
-- ^ @ruleCantMatch tpl actual@ returns True only if @actual@
-- definitely can't match @tpl@ by instantiating @tpl@.  
-- It's only a one-way match; unlike instance matching we 
-- don't consider unification.
-- 
-- Notice that [_$_]
--	@ruleCantMatch [Nothing] [Just n2] = False@
--      Reason: a template variable can be instantiated by a constant
-- Also:
--	@ruleCantMatch [Just n1] [Nothing] = False@
--      Reason: a local variable @v@ in the actuals might [_$_]

ruleCantMatch (Just n1 : ts) (Just n2 : as) = n1 /= n2 || ruleCantMatch ts as
ruleCantMatch (_       : ts) (_       : as) = ruleCantMatch ts as
ruleCantMatch _ 	     _ 		    = False

pprRulesForUser :: [CoreRule] -> SDoc
-- (a) tidy the rules
-- (b) sort them into order based on the rule name
-- (c) suppress uniques (unless -dppr-debug is on)
-- This combination makes the output stable so we can use in testing
-- It's here rather than in PprCore because it calls tidyRules
pprRulesForUser rules
  = withPprStyle defaultUserStyle $
    pprRules $
    sortLe le_rule  $
    tidyRules emptyTidyEnv rules
  where 
    le_rule r1 r2 = ru_name r1 <= ru_name r2

-- | Make a 'SpecInfo' containing a number of 'CoreRule's, suitable
-- for putting into an 'IdInfo'
mkSpecInfo :: [CoreRule] -> SpecInfo
mkSpecInfo rules = SpecInfo rules (rulesFreeVars rules)

extendSpecInfo :: SpecInfo -> [CoreRule] -> SpecInfo
extendSpecInfo (SpecInfo rs1 fvs1) rs2
  = SpecInfo (rs2 ++ rs1) (rulesFreeVars rs2 `unionVarSet` fvs1)

addSpecInfo :: SpecInfo -> SpecInfo -> SpecInfo
addSpecInfo (SpecInfo rs1 fvs1) (SpecInfo rs2 fvs2) 
  = SpecInfo (rs1 ++ rs2) (fvs1 `unionVarSet` fvs2)

addIdSpecialisations :: Id -> [CoreRule] -> Id
addIdSpecialisations id []
  = id
addIdSpecialisations id rules
  = setIdSpecialisation id $
    extendSpecInfo (idSpecialisation id) rules

-- | Gather all the rules for locally bound identifiers from the supplied bindings
rulesOfBinds :: [CoreBind] -> [CoreRule]
rulesOfBinds binds = concatMap (concatMap idCoreRules . bindersOf) binds

getRules :: RuleBase -> Id -> [CoreRule]
-- See Note [Where rules are found]
getRules rule_base fn
  = idCoreRules fn ++ imp_rules
  where
    imp_rules = lookupNameEnv rule_base (idName fn) `orElse` []

-- | Gathers a collection of 'CoreRule's. Maps (the name of) an 'Id' to its rules
type RuleBase = NameEnv [CoreRule]
	-- The rules are are unordered; 
	-- we sort out any overlaps on lookup

emptyRuleBase :: RuleBase
emptyRuleBase = emptyNameEnv

mkRuleBase :: [CoreRule] -> RuleBase
mkRuleBase rules = extendRuleBaseList emptyRuleBase rules

extendRuleBaseList :: RuleBase -> [CoreRule] -> RuleBase
extendRuleBaseList rule_base new_guys
  = foldl extendRuleBase rule_base new_guys

unionRuleBase :: RuleBase -> RuleBase -> RuleBase
unionRuleBase rb1 rb2 = plusNameEnv_C (++) rb1 rb2

extendRuleBase :: RuleBase -> CoreRule -> RuleBase
extendRuleBase rule_base rule
  = extendNameEnv_Acc (:) singleton rule_base (ruleIdName rule) rule

pprRuleBase :: RuleBase -> SDoc
pprRuleBase rules = vcat [ pprRules (tidyRules emptyTidyEnv rs) 
			 | rs <- nameEnvElts rules ]

-- | The main rule matching function. Attempts to apply all (active)
-- supplied rules to this instance of an application in a given
-- context, returning the rule applied and the resulting expression if
-- successful.
lookupRule :: (Activation -> Bool)	-- When rule is active
	    -> IdUnfoldingFun		-- When Id can be unfolded
            -> InScopeSet
	    -> Id -> [CoreExpr]
	    -> [CoreRule] -> Maybe (CoreRule, CoreExpr)

-- See Note [Extra args in rule matching]
-- See comments on matchRule
lookupRule is_active id_unf in_scope fn args rules
  = -- pprTrace "matchRules" (ppr fn <+> ppr args $$ ppr rules ) $
    case go [] rules of
	[]     -> Nothing
	(m:ms) -> Just (findBest (fn,args) m ms)
  where
    rough_args = map roughTopName args

    go :: [(CoreRule,CoreExpr)] -> [CoreRule] -> [(CoreRule,CoreExpr)]
    go ms []	       = ms
    go ms (r:rs) = case (matchRule is_active id_unf in_scope args rough_args r) of
			Just e  -> go ((r,e):ms) rs
			Nothing -> -- pprTrace "match failed" (ppr r $$ ppr args $$ 
				   -- 	ppr [ (arg_id, unfoldingTemplate unf) 
                                   --       | Var arg_id <- args
                                   --       , let unf = idUnfolding arg_id
                                   --       , isCheapUnfolding unf] )
				   go ms rs

findBest :: (Id, [CoreExpr])
	 -> (CoreRule,CoreExpr) -> [(CoreRule,CoreExpr)] -> (CoreRule,CoreExpr)
-- All these pairs matched the expression
-- Return the pair the the most specific rule
-- The (fn,args) is just for overlap reporting

findBest _      (rule,ans)   [] = (rule,ans)
findBest target (rule1,ans1) ((rule2,ans2):prs)
  | rule1 `isMoreSpecific` rule2 = findBest target (rule1,ans1) prs
  | rule2 `isMoreSpecific` rule1 = findBest target (rule2,ans2) prs
  | debugIsOn = let pp_rule rule
			| opt_PprStyle_Debug = ppr rule
			| otherwise          = doubleQuotes (ftext (ru_name rule))
		in pprTrace "Rules.findBest: rule overlap (Rule 1 wins)"
			 (vcat [if opt_PprStyle_Debug then 
				   ptext (sLit "Expression to match:") <+> ppr fn <+> sep (map ppr args)
				else empty,
				ptext (sLit "Rule 1:") <+> pp_rule rule1, 
				ptext (sLit "Rule 2:") <+> pp_rule rule2]) $
		findBest target (rule1,ans1) prs
  | otherwise = findBest target (rule1,ans1) prs
  where
    (fn,args) = target

isMoreSpecific :: CoreRule -> CoreRule -> Bool
-- This tests if one rule is more specific than another
-- We take the view that a BuiltinRule is less specific than
-- anything else, because we want user-define rules to "win"
-- In particular, class ops have a built-in rule, but we
-- any user-specific rules to win
--   eg (Trac #4397)   
--      truncate :: (RealFrac a, Integral b) => a -> b
--      {-# RULES "truncate/Double->Int" truncate = double2Int #-}
--      double2Int :: Double -> Int
--   We want the specific RULE to beat the built-in class-op rule
isMoreSpecific (BuiltinRule {}) _                = False
isMoreSpecific (Rule {})        (BuiltinRule {}) = True
isMoreSpecific (Rule { ru_bndrs = bndrs1, ru_args = args1 })
	       (Rule { ru_bndrs = bndrs2, ru_args = args2 })
  = isJust (matchN id_unfolding_fun in_scope bndrs2 args2 args1)
  where
   id_unfolding_fun _ = NoUnfolding	-- Don't expand in templates
   in_scope = mkInScopeSet (mkVarSet bndrs1)
	-- Actually we should probably include the free vars 
	-- of rule1's args, but I can't be bothered

noBlackList :: Activation -> Bool
noBlackList _ = False		-- Nothing is black listed

------------------------------------
matchRule :: (Activation -> Bool) -> IdUnfoldingFun
          -> InScopeSet
	  -> [CoreExpr] -> [Maybe Name]
	  -> CoreRule -> Maybe CoreExpr

-- If (matchRule rule args) returns Just (name,rhs)
-- then (f args) matches the rule, and the corresponding
-- rewritten RHS is rhs
--
-- The bndrs and rhs is occurrence-analysed
--
-- 	Example
--
-- The rule
--	forall f g x. map f (map g x) ==> map (f . g) x
-- is stored
--	CoreRule "map/map" 
--		 [f,g,x]		-- tpl_vars
--		 [f,map g x]		-- tpl_args
--		 map (f.g) x)		-- rhs
--	  
-- Then the call: matchRule the_rule [e1,map e2 e3]
--	  = Just ("map/map", (\f,g,x -> rhs) e1 e2 e3)
--
-- Any 'surplus' arguments in the input are simply put on the end
-- of the output.

matchRule _is_active id_unf _in_scope args _rough_args
	  (BuiltinRule { ru_try = match_fn })
-- Built-in rules can't be switched off, it seems
  = case match_fn id_unf args of
	Just expr -> Just expr
	Nothing   -> Nothing

matchRule is_active id_unf in_scope args rough_args
          (Rule { ru_act = act, ru_rough = tpl_tops,
		  ru_bndrs = tpl_vars, ru_args = tpl_args,
		  ru_rhs = rhs })
  | not (is_active act)		      = Nothing
  | ruleCantMatch tpl_tops rough_args = Nothing
  | otherwise
  = case matchN id_unf in_scope tpl_vars tpl_args args of
	Nothing		               -> Nothing
	Just (bind_wrapper, tpl_vals) -> Just (bind_wrapper $
					       rule_fn `mkApps` tpl_vals)
  where
    rule_fn = occurAnalyseExpr (mkLams tpl_vars rhs)
	-- We could do this when putting things into the rulebase, I guess

---------------------------------------
matchN	:: IdUnfoldingFun
        -> InScopeSet           -- ^ In-scope variables
	-> [Var]		-- ^ Match template type variables
	-> [CoreExpr]		-- ^ Match template
	-> [CoreExpr]		-- ^ Target; can have more elements than the template
	-> Maybe (BindWrapper,	-- Floated bindings; see Note [Matching lets]
		  [CoreExpr])
-- For a given match template and context, find bindings to wrap around 
-- the entire result and what should be substituted for each template variable.
-- Fail if there are two few actual arguments from the target to match the template

matchN id_unf in_scope tmpl_vars tmpl_es target_es
  = do  { subst <- go init_menv emptyRuleSubst tmpl_es target_es
        ; return (rs_binds subst,
                  map (lookup_tmpl subst) tmpl_vars') }
  where
    (init_rn_env, tmpl_vars') = mapAccumL rnBndrL (mkRnEnv2 in_scope) tmpl_vars
        -- See Note [Template binders]

    init_menv = RV { rv_tmpls = mkVarSet tmpl_vars', rv_lcl = init_rn_env
                   , rv_fltR = mkEmptySubst (rnInScopeSet init_rn_env)
                   , rv_unf = id_unf }
		
    go _    subst []     _  	= Just subst
    go _    _     _      [] 	= Nothing	-- Fail if too few actual args
    go menv subst (t:ts) (e:es) = do { subst1 <- match menv subst t e
				     ; go menv subst1 ts es }

    lookup_tmpl :: RuleSubst -> Var -> CoreExpr
    lookup_tmpl (RS { rs_tv_subst = tv_subst, rs_id_subst = id_subst }) tmpl_var'
        | isId tmpl_var' = case lookupVarEnv id_subst tmpl_var' of
                             Just e -> e
                             _      -> unbound tmpl_var'
        | otherwise      = case lookupVarEnv tv_subst tmpl_var' of
                             Just ty -> Type ty
                             Nothing -> unbound tmpl_var'

    unbound var = pprPanic "Template variable unbound in rewrite rule" 
			(ppr var $$ ppr tmpl_vars $$ ppr tmpl_vars' $$ ppr tmpl_es $$ ppr target_es)

-- * The domain of the TvSubstEnv and IdSubstEnv are the template
--   variables passed into the match.
--
-- * The BindWrapper in a RuleSubst are the bindings floated out
--   from nested matches; see the Let case of match, below
--
data RuleEnv = RV { rv_tmpls :: VarSet          -- Template variables
                  , rv_lcl   :: RnEnv2          -- Renamings for *local bindings*
                                                --   (lambda/case)
                  , rv_fltR  :: Subst           -- Renamings for floated let-bindings
                                                --   domain disjoint from envR of rv_lcl
                                                -- See Note [Matching lets]
                  , rv_unf :: IdUnfoldingFun
                  }

data RuleSubst = RS { rs_tv_subst :: TvSubstEnv   -- Range is the
                    , rs_id_subst :: IdSubstEnv   --   template variables
                    , rs_binds    :: BindWrapper  -- Floated bindings
                    , rs_bndrs    :: VarSet       -- Variables bound by floated lets
                    }

type BindWrapper = CoreExpr -> CoreExpr
  -- See Notes [Matching lets] and [Matching cases]
  -- we represent the floated bindings as a core-to-core function

emptyRuleSubst :: RuleSubst
emptyRuleSubst = RS { rs_tv_subst = emptyVarEnv, rs_id_subst = emptyVarEnv
                    , rs_binds = \e -> e, rs_bndrs = emptyVarSet }

--	At one stage I tried to match even if there are more 
--	template args than real args.

--	I now think this is probably a bad idea.
--	Should the template (map f xs) match (map g)?  I think not.
--	For a start, in general eta expansion wastes work.
--	SLPJ July 99


match :: RuleEnv
      -> RuleSubst
      -> CoreExpr		-- Template
      -> CoreExpr		-- Target
      -> Maybe RuleSubst

-- See the notes with Unify.match, which matches types
-- Everything is very similar for terms

-- Interesting examples:
-- Consider matching
--	\x->f 	   against    \f->f
-- When we meet the lambdas we must remember to rename f to f' in the
-- second expresion.  The RnEnv2 does that.
--
-- Consider matching 
--	forall a. \b->b	   against   \a->3
-- We must rename the \a.  Otherwise when we meet the lambdas we 
-- might substitute [a/b] in the template, and then erroneously 
-- succeed in matching what looks like the template variable 'a' against 3.

-- The Var case follows closely what happens in Unify.match
match renv subst (Var v1)    e2 = match_var renv subst v1 e2
match renv subst (Note _ e1) e2 = match renv subst e1 e2
match renv subst e1 (Note _ e2) = match renv subst e1 e2
      -- Ignore notes in both template and thing to be matched
      -- See Note [Notes in RULE matching]

match renv subst e1 (Var v2)      -- Note [Expanding variables]
  | not (inRnEnvR rn_env v2) -- Note [Do not expand locally-bound variables]
  , Just e2' <- expandUnfolding_maybe (rv_unf renv v2')
  = match (renv { rv_lcl = nukeRnEnvR rn_env }) subst e1 e2'
  where
    v2'    = lookupRnInScope rn_env v2
    rn_env = rv_lcl renv
	-- Notice that we look up v2 in the in-scope set
	-- See Note [Lookup in-scope]
	-- No need to apply any renaming first (hence no rnOccR)
	-- because of the not-inRnEnvR

match renv subst e1 (Let bind e2)
  | okToFloat (rv_lcl renv) (bindFreeVars bind)        -- See Note [Matching lets]
  = match (renv { rv_fltR = flt_subst' })
          (subst { rs_binds = rs_binds subst . Let bind'
                 , rs_bndrs = extendVarSetList (rs_bndrs subst) new_bndrs })
	  e1 e2
  where
    flt_subst = addInScopeSet (rv_fltR renv) (rs_bndrs subst)
    (flt_subst', bind') = substBind flt_subst bind
    new_bndrs = bindersOf bind'

{- Disabled: see Note [Matching cases] below
match renv (tv_subst, id_subst, binds) e1 
      (Case scrut case_bndr ty [(con, alt_bndrs, rhs)])
  | exprOkForSpeculation scrut	-- See Note [Matching cases]
  , okToFloat rn_env bndrs (exprFreeVars scrut)
  = match (renv { me_env = rn_env' })
          (tv_subst, id_subst, binds . case_wrap)
          e1 rhs 
  where
    rn_env   = me_env renv
    rn_env'  = extendRnInScopeList rn_env bndrs
    bndrs    = case_bndr : alt_bndrs
    case_wrap rhs' = Case scrut case_bndr ty [(con, alt_bndrs, rhs')]
-}

match _ subst (Lit lit1) (Lit lit2)
  | lit1 == lit2
  = Just subst

match renv subst (App f1 a1) (App f2 a2)
  = do 	{ subst' <- match renv subst f1 f2
	; match renv subst' a1 a2 }

match renv subst (Lam x1 e1) (Lam x2 e2)
  = match renv' subst e1 e2
  where
    renv' = renv { rv_lcl = rnBndr2 (rv_lcl renv) x1 x2
                 , rv_fltR = delBndr (rv_fltR renv) x2 }

-- This rule does eta expansion
--		(\x.M)  ~  N 	iff	M  ~  N x
-- It's important that this is *after* the let rule,
-- so that 	(\x.M)  ~  (let y = e in \y.N)
-- does the let thing, and then gets the lam/lam rule above
match renv subst (Lam x1 e1) e2
  = match renv' subst e1 (App e2 (varToCoreExpr new_x))
  where
    (rn_env', new_x) = rnEtaL (rv_lcl renv) x1
    renv' = renv { rv_lcl = rn_env' }

-- Eta expansion the other way
--	M  ~  (\y.N)	iff   M	y     ~  N
match renv subst e1 (Lam x2 e2)
  = match renv' subst (App e1 (varToCoreExpr new_x)) e2
  where
    (rn_env', new_x) = rnEtaR (rv_lcl renv) x2
    renv' = renv { rv_lcl = rn_env' }

match renv subst (Case e1 x1 ty1 alts1) (Case e2 x2 ty2 alts2)
  = do	{ subst1 <- match_ty renv subst ty1 ty2
	; subst2 <- match renv subst1 e1 e2
        ; let renv' = rnMatchBndr2 renv subst x1 x2
        ; match_alts renv' subst2 alts1 alts2   -- Alts are both sorted
	}

match renv subst (Type ty1) (Type ty2)
  = match_ty renv subst ty1 ty2
match renv subst (Coercion co1) (Coercion co2)
  = match_co renv subst co1 co2

match renv subst (Cast e1 co1) (Cast e2 co2)
  = do	{ subst1 <- match_co renv subst co1 co2
	; match renv subst1 e1 e2 }

-- Everything else fails
match _ _ _e1 _e2 = -- pprTrace "Failing at" ((text "e1:" <+> ppr _e1) $$ (text "e2:" <+> ppr _e2)) $
                    Nothing

-------------
match_co :: RuleEnv
      	 -> RuleSubst
      	 -> Coercion
      	 -> Coercion
      	 -> Maybe RuleSubst
match_co renv subst (CoVarCo cv) co
  = match_var renv subst cv (Coercion co)
match_co _ _ co1 _ 
  = pprTrace "match_co baling out" (ppr co1) Nothing

-------------
rnMatchBndr2 :: RuleEnv -> RuleSubst -> Var -> Var -> RuleEnv
rnMatchBndr2 renv subst x1 x2
  = renv { rv_lcl  = rnBndr2 rn_env x1 x2
         , rv_fltR = delBndr (rv_fltR renv) x2 }
  where
    rn_env = addRnInScopeSet (rv_lcl renv) (rs_bndrs subst)
    -- Typically this is a no-op, but it may matter if
    -- there are some floated let-bindings

------------------------------------------
match_alts :: RuleEnv
      	   -> RuleSubst
      	   -> [CoreAlt]		-- Template
      	   -> [CoreAlt]		-- Target
      	   -> Maybe RuleSubst
match_alts _ subst [] []
  = return subst
match_alts renv subst ((c1,vs1,r1):alts1) ((c2,vs2,r2):alts2)
  | c1 == c2
  = do  { subst1 <- match renv' subst r1 r2
        ; match_alts renv subst1 alts1 alts2 }
  where
    renv' = foldl mb renv (vs1 `zip` vs2)
    mb renv (v1,v2) = rnMatchBndr2 renv subst v1 v2

match_alts _ _ _ _
  = Nothing

------------------------------------------
okToFloat :: RnEnv2 -> VarSet -> Bool
okToFloat rn_env bind_fvs
  = foldVarSet ((&&) . not_captured) True bind_fvs
  where
    not_captured fv = not (inRnEnvR rn_env fv)

------------------------------------------
match_var :: RuleEnv
     	  -> RuleSubst
     	  -> Var		-- Template
     	  -> CoreExpr        -- Target
     	  -> Maybe RuleSubst
match_var renv@(RV { rv_tmpls = tmpls, rv_lcl = rn_env, rv_fltR = flt_env })
          subst v1 e2
  | v1' `elemVarSet` tmpls
  = match_tmpl_var renv subst v1' e2

  | otherwise   -- v1' is not a template variable; check for an exact match with e2
  = case e2 of  -- Remember, envR of rn_env is disjoint from rv_fltR
       Var v2 | v1' == rnOccR rn_env v2
              -> Just subst

              | Var v2' <- lookupIdSubst (text "match_var") flt_env v2
              , v1' == v2'
              -> Just subst

       _ -> Nothing

  where
    v1' = rnOccL rn_env v1
	-- If the template is
	--	forall x. f x (\x -> x) = ...
	-- Then the x inside the lambda isn't the 
	-- template x, so we must rename first!

------------------------------------------
match_tmpl_var :: RuleEnv
               -> RuleSubst
	       -> Var                -- Template
	       -> CoreExpr		-- Target
	       -> Maybe RuleSubst

match_tmpl_var renv@(RV { rv_lcl = rn_env, rv_fltR = flt_env })
               subst@(RS { rs_id_subst = id_subst, rs_bndrs = let_bndrs })
               v1' e2
  | any (inRnEnvR rn_env) (varSetElems (exprFreeVars e2))
  = Nothing     -- Occurs check failure
		-- e.g. match forall a. (\x-> a x) against (\y. y y)

  | Just e1' <- lookupVarEnv id_subst v1'
  = if eqExpr (rnInScopeSet rn_env) e1' e2'
    then Just subst
    else Nothing

  | otherwise
  =             -- Note [Matching variable types]
		-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
		-- However, we must match the *types*; e.g.
		--   forall (c::Char->Int) (x::Char). 
                --      f (c x) = "RULE FIRED"
		-- We must only match on args that have the right type
		-- It's actually quite difficult to come up with an example that shows
		-- you need type matching, esp since matching is left-to-right, so type
		-- args get matched first.  But it's possible (e.g. simplrun008) and
		-- this is the Right Thing to do
    do { subst' <- match_ty renv subst (idType v1') (exprType e2)
       ; return (subst' { rs_id_subst = id_subst' }) }
  where
    -- e2' is the result of applying flt_env to e2
    e2' | isEmptyVarSet let_bndrs = e2
        | otherwise = substExpr (text "match_tmpl_var") flt_env e2

    id_subst' = extendVarEnv (rs_id_subst subst) v1' e2'
         -- No further renaming to do on e2',
         -- because no free var of e2' is in the rnEnvR of the envt

------------------------------------------
match_ty :: RuleEnv
      	 -> RuleSubst
      	 -> Type		-- Template
      	 -> Type		-- Target
      	 -> Maybe RuleSubst
-- Matching Core types: use the matcher in TcType.
-- Notice that we treat newtypes as opaque.  For example, suppose 
-- we have a specialised version of a function at a newtype, say 
--	newtype T = MkT Int
-- We only want to replace (f T) with f', not (f Int).

match_ty renv subst ty1 ty2
  = do  { tv_subst' <- Unify.ruleMatchTyX menv tv_subst ty1 ty2
        ; return (subst { rs_tv_subst = tv_subst' }) }
  where
    tv_subst = rs_tv_subst subst
    menv = ME { me_tmpls = rv_tmpls renv, me_env = rv_lcl renv }

-- | Report partial matches for rules beginning with the specified
-- string for the purposes of error reporting
ruleCheckProgram :: CompilerPhase               -- ^ Rule activation test
                 -> String                      -- ^ Rule pattern
                 -> RuleBase                    -- ^ Database of rules
                 -> [CoreBind]                  -- ^ Bindings to check in
                 -> SDoc                        -- ^ Resulting check message
ruleCheckProgram phase rule_pat rule_base binds 
  | isEmptyBag results
  = text "Rule check results: no rule application sites"
  | otherwise
  = vcat [text "Rule check results:",
	  line,
	  vcat [ p $$ line | p <- bagToList results ]
	 ]
  where
    env = RuleCheckEnv { rc_is_active = isActive phase
                       , rc_id_unf    = idUnfolding	-- Not quite right
		       	 	      			-- Should use activeUnfolding
                       , rc_pattern   = rule_pat
                       , rc_rule_base = rule_base }
    results = unionManyBags (map (ruleCheckBind env) binds)
    line = text (replicate 20 '-')
	  
data RuleCheckEnv = RuleCheckEnv {
    rc_is_active :: Activation -> Bool, 
    rc_id_unf  :: IdUnfoldingFun,
    rc_pattern :: String, 
    rc_rule_base :: RuleBase
}

ruleCheckBind :: RuleCheckEnv -> CoreBind -> Bag SDoc
   -- The Bag returned has one SDoc for each call site found
ruleCheckBind env (NonRec _ r) = ruleCheck env r
ruleCheckBind env (Rec prs)    = unionManyBags [ruleCheck env r | (_,r) <- prs]

ruleCheck :: RuleCheckEnv -> CoreExpr -> Bag SDoc
ruleCheck _   (Var _) 	    = emptyBag
ruleCheck _   (Lit _) 	    = emptyBag
ruleCheck _   (Type _)      = emptyBag
ruleCheck _   (Coercion _)  = emptyBag
ruleCheck env (App f a)     = ruleCheckApp env (App f a) []
ruleCheck env (Note _ e)    = ruleCheck env e
ruleCheck env (Cast e _)    = ruleCheck env e
ruleCheck env (Let bd e)    = ruleCheckBind env bd `unionBags` ruleCheck env e
ruleCheck env (Lam _ e)     = ruleCheck env e
ruleCheck env (Case e _ _ as) = ruleCheck env e `unionBags` 
			        unionManyBags [ruleCheck env r | (_,_,r) <- as]

ruleCheckApp :: RuleCheckEnv -> Expr CoreBndr -> [Arg CoreBndr] -> Bag SDoc
ruleCheckApp env (App f a) as = ruleCheck env a `unionBags` ruleCheckApp env f (a:as)
ruleCheckApp env (Var f) as   = ruleCheckFun env f as
ruleCheckApp env other _      = ruleCheck env other

ruleCheckFun :: RuleCheckEnv -> Id -> [CoreExpr] -> Bag SDoc
-- Produce a report for all rules matching the predicate
-- saying why it doesn't match the specified application

ruleCheckFun env fn args
  | null name_match_rules = emptyBag
  | otherwise		  = unitBag (ruleAppCheck_help env fn args name_match_rules)
  where
    name_match_rules = filter match (getRules (rc_rule_base env) fn)
    match rule = (rc_pattern env) `isPrefixOf` unpackFS (ruleName rule)

ruleAppCheck_help :: RuleCheckEnv -> Id -> [CoreExpr] -> [CoreRule] -> SDoc
ruleAppCheck_help env fn args rules
  = 	-- The rules match the pattern, so we want to print something
    vcat [text "Expression:" <+> ppr (mkApps (Var fn) args),
	  vcat (map check_rule rules)]
  where
    n_args = length args
    i_args = args `zip` [1::Int ..]
    rough_args = map roughTopName args

    check_rule rule = rule_herald rule <> colon <+> rule_info rule

    rule_herald (BuiltinRule { ru_name = name })
	= ptext (sLit "Builtin rule") <+> doubleQuotes (ftext name)
    rule_herald (Rule { ru_name = name })
	= ptext (sLit "Rule") <+> doubleQuotes (ftext name)

    rule_info rule
	| Just _ <- matchRule noBlackList (rc_id_unf env) emptyInScopeSet args rough_args rule
	= text "matches (which is very peculiar!)"

    rule_info (BuiltinRule {}) = text "does not match"

    rule_info (Rule { ru_act = act, 
		      ru_bndrs = rule_bndrs, ru_args = rule_args})
	| not (rc_is_active env act)  = text "active only in later phase"
	| n_args < n_rule_args	      = text "too few arguments"
	| n_mismatches == n_rule_args = text "no arguments match"
	| n_mismatches == 0	      = text "all arguments match (considered individually), but rule as a whole does not"
	| otherwise		      = text "arguments" <+> ppr mismatches <+> text "do not match (1-indexing)"
	where
	  n_rule_args  = length rule_args
	  n_mismatches = length mismatches
	  mismatches   = [i | (rule_arg, (arg,i)) <- rule_args `zip` i_args,
			      not (isJust (match_fn rule_arg arg))]

	  lhs_fvs = exprsFreeVars rule_args	-- Includes template tyvars
          match_fn rule_arg arg = match renv emptyRuleSubst rule_arg arg
		where
                  in_scope = mkInScopeSet (lhs_fvs `unionVarSet` exprFreeVars arg)
                  renv = RV { rv_lcl   = mkRnEnv2 in_scope
                            , rv_tmpls = mkVarSet rule_bndrs
                            , rv_fltR  = mkEmptySubst in_scope
                            , rv_unf   = rc_id_unf env }