{-# OPTIONS -fno-warn-tabs #-}
-- The above warning supression flag is a temporary kludge.
-- While working on this module you are encouraged to remove it and
-- detab the module (please do the detabbing in a separate patch). See
--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
-- for details

module TcRules ( tcRules ) where

import HsSyn
import TcRnMonad
import TcSimplify
import TcMType
import TcType
import TcHsType
import TcExpr
import TcEnv
import TcEvidence( TcEvBinds(..) )
import Type
import Id
import NameEnv( emptyNameEnv )
import Name
import Var
import VarSet
import SrcLoc
import Outputable
import FastString
import Data.List( partition )

tcRules :: [LRuleDecl Name] -> TcM [LRuleDecl TcId]
tcRules decls = mapM (wrapLocM tcRule) decls

tcRule :: RuleDecl Name -> TcM (RuleDecl TcId)
tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
  = addErrCtxt (ruleCtxt name)	$
    do { traceTc "---- Rule ------" (ppr name)

    	-- Note [Typechecking rules]
       ; vars <- tcRuleBndrs hs_bndrs
       ; let (id_bndrs, tv_bndrs) = partition (isId . snd) vars
       ; (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty)
            <- tcExtendTyVarEnv2 tv_bndrs $
               tcExtendIdEnv2    id_bndrs $
               do { ((lhs', rule_ty), lhs_wanted) <- captureConstraints (tcInferRho lhs)
                  ; (rhs', rhs_wanted) <- captureConstraints (tcMonoExpr rhs rule_ty)
                  ; return (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty) }

       ; (lhs_evs, other_lhs_wanted) <- simplifyRule name lhs_wanted rhs_wanted

	-- Now figure out what to quantify over
	-- c.f. TcSimplify.simplifyInfer
	-- We quantify over any tyvars free in *either* the rule
	--  *or* the bound variables.  The latter is important.  Consider
	--	ss (x,(y,z)) = (x,z)
	--	RULE:  forall v. fst (ss v) = fst v
	-- The type of the rhs of the rule is just a, but v::(a,(b,c))
	--
	-- We also need to get the completely-uconstrained tyvars of
	-- the LHS, lest they otherwise get defaulted to Any; but we do that
	-- during zonking (see TcHsSyn.zonkRule)

       ; let tpl_ids    = lhs_evs ++ map snd id_bndrs
             forall_tvs = tyVarsOfTypes (rule_ty : map idType tpl_ids)
       ; zonked_forall_tvs <- zonkTyVarsAndFV forall_tvs
       ; gbl_tvs           <- tcGetGlobalTyVars	     -- Already zonked
       ; let tvs_to_quantify = varSetElems (zonked_forall_tvs `minusVarSet` gbl_tvs)
       ; qkvs <- kindGeneralize (tyVarsOfTypes (map tyVarKind tvs_to_quantify))
                                (map getName tvs_to_quantify)
       ; qtvs <- zonkQuantifiedTyVars tvs_to_quantify
       ; let qtkvs = qkvs ++ qtvs
       ; traceTc "tcRule" (vcat [ doubleQuotes (ftext name)
                                , ppr forall_tvs
                                , ppr qtvs
                                , ppr rule_ty
                                , vcat [ ppr id <+> dcolon <+> ppr (idType id) | id <- tpl_ids ] 
                  ])

           -- Simplify the RHS constraints
       ; loc           <- getCtLoc (RuleSkol name)
       ; rhs_binds_var <- newTcEvBinds
       ; emitImplication $ Implic { ic_untch  = NoUntouchables
                                  , ic_env    = emptyNameEnv
                                  , ic_skols  = qtkvs
                                  , ic_given  = lhs_evs
                                  , ic_wanted = rhs_wanted
                                  , ic_insol  = insolubleWC rhs_wanted
                                  , ic_binds  = rhs_binds_var
                                  , ic_loc    = loc } 

           -- For the LHS constraints we must solve the remaining constraints
           -- (a) so that we report insoluble ones
           -- (b) so that we bind any soluble ones
       ; lhs_binds_var <- newTcEvBinds
       ; emitImplication $ Implic { ic_untch  = NoUntouchables
                                  , ic_env    = emptyNameEnv
                                  , ic_skols  = qtkvs
                                  , ic_given  = lhs_evs
                                  , ic_wanted = other_lhs_wanted
                                  , ic_insol  = insolubleWC other_lhs_wanted
                                  , ic_binds  = lhs_binds_var
                                  , ic_loc    = loc } 

       ; return (HsRule name act
		    (map (RuleBndr . noLoc) (qtkvs ++ tpl_ids))
		    (mkHsDictLet (TcEvBinds lhs_binds_var) lhs') fv_lhs
		    (mkHsDictLet (TcEvBinds rhs_binds_var) rhs') fv_rhs) }

tcRuleBndrs :: [RuleBndr Name] -> TcM [(Name, Var)]
tcRuleBndrs [] 
  = return []
tcRuleBndrs (RuleBndr (L _ name) : rule_bndrs)
  = do 	{ ty <- newFlexiTyVarTy openTypeKind
        ; vars <- tcRuleBndrs rule_bndrs
	; return ((name, mkLocalId name ty) : vars) }
tcRuleBndrs (RuleBndrSig (L _ name) rn_ty : rule_bndrs)
--  e.g 	x :: a->a
--  The tyvar 'a' is brought into scope first, just as if you'd written
--		a::*, x :: a->a
  = do	{ let ctxt = RuleSigCtxt name
	; (id_ty, skol_tvs) <- tcHsPatSigType ctxt rn_ty
        ; let id = mkLocalId name id_ty

	      -- The type variables scope over subsequent bindings; yuk
        ; vars <- tcExtendTyVarEnv2 skol_tvs $ 
                  tcRuleBndrs rule_bndrs 
	; return (skol_tvs ++ (name, id) : vars) }

ruleCtxt :: FastString -> SDoc
ruleCtxt name = ptext (sLit "When checking the transformation rule") <+> 
		doubleQuotes (ftext name)