-- Please, see the file LICENSE for copyright and license information.

> module HFusion.Internal.RenVars (renameVariables,AlphaConvertible(..),VarsB(..))
> where

> import HFusion.Internal.Utils
> import HFusion.Internal.Parsing.HyloContext
> import Data.List((\\),intersect,nub)
> import HFusion.Internal.HyloFace
> import HFusion.Internal.HsSyn

 import Debug.Trace

 sss msg a = trace (msg++": "++show a) a

> renameVariables :: (VarsB a', VarsB ca', AlphaConvertible ca', AlphaConvertible a', VarsB a, 
>                     Vars a', Vars ca', AlphaConvertible a, Vars a,AlphaConvertible ca, Vars ca, VarsB ca, CHylo h) => 
>                  (h a ca) -> (h a' ca') -> [Variable] -> VarGenState (h a ca, h a' ca')
> renameVariables left right fvright = 
>          do right'<-if null i0 then return right
>                        else do us <- mapM (getFreshVar . varPrefix) i0
>                                return (alphaConvert' (zip i0 us) right)
>             let i1 = nub$ intersect (vars' right'++fvright) (varsB' left)
>             left'<-if null i1 then return left
>                      else do us <- mapM (getFreshVar . varPrefix) i1
>                              return (alphaConvert' (zip i1 us) left)
>             return (left',right')
>   where i0 =  nub$ intersect (vars' left) (varsB' right)
>         vars' h = getName h  : ( (\(bv,t0,c)->varsB c++vars c++vars t0++vars bv) $ getCoalgebra h) ++ vars (getAlgebra h)
>                   ++ vars (getEta h) ++ vars (getContext h) ++ (\(bvs,_,_)->vars bvs) (getCoalgebra h)
>         varsB' h = ( (\(bv,t0,c)-> varsB c++varsB t0 ++ vars bv) $ getCoalgebra h) 
>                      ++ varsB (getAlgebra h) ++ vars (getContext h)
>         alphaConvert' ss h = 
>                 let constantArgs_h = getConstantArgs (getContext h)
>                     (bv,_t0,_c) = getCoalgebra h
>                     sc' = constantArgs_h ++ vars bv
>                 in setName (getName h) $ setContext (alphaConvert constantArgs_h ss$ getContext h) $
>                                     consHylo (alphaConvert constantArgs_h ss $ getAlgebra h) 
>                                     (alphaConvert constantArgs_h ss $ getEta h) (getFunctor h)
>                                     ((\(bv,t0,c)->(alphaConvert constantArgs_h ss bv,
>                                                    alphaConvert sc' ss t0,
>                                                    alphaConvert sc' ss c)) $ getCoalgebra h)

===========================
Bounded variables
===========================

> instance (VarsB a) => VarsB (Acomponent a) where
>   varsB (Acomp (bvs, termwrapper)) = varsB termwrapper ++ vars bvs

> instance VarsB PatternS where
>   varsB (PcaseS _ pat termS) =  varsB termS ++ vars pat
>   varsB (PcaseSana _ _ pat termS) =  varsB termS ++ vars pat
>   varsB (PcaseR _ _ _ _ ts) =  concat (map (varsB.fst) ts)
>   varsB (Ppattern _ p) =  vars p
>   varsB Pdone = []


> instance VarsB Sigma where
>   varsB (Sigma (_,_,pss,_)) = concat (map varsB pss)

> instance VarsB WrappedCA where
>   varsB (WCApsi (bv, t0, psi)) = varsB t0 ++ varsB psi ++ vars bv
>   varsB (WCAoutF (bv, t0, outf)) = varsB t0 ++ varsB outf ++ vars bv
>   varsB (WCAsigma (bv, t0, sigma)) = varsB t0 ++ varsB sigma ++ vars bv

> instance VarsB InF where
>   varsB (InF (_,ts)) = varsB ts

> instance VarsB Tau where
>   varsB (Tauphi tauphii) = varsB tauphii
>   varsB (TauinF tauinf) = varsB tauinf
>   varsB (Tautau tautau) = varsB tautau

> instance VarsB a => VarsB (TermWrapper a) where
>   varsB = foldTW (\t0 pts vs -> varsB t0 ++ vars pts ++ concat vs) const varsB varsB [] 

> instance (VarsB a) => VarsB (TauTerm a) where
>   varsB _ = []

> instance VarsB OutF where
>   varsB (OutF outfis) = varsB outfis

> instance VarsB OutFi where
>   varsB (OutFc (_,vs,_)) = vs

> instance VarsB Psi where
>   varsB (Psi psis) = varsB psis

> instance VarsB Psii where
>   varsB (Psii (pat, _)) = vars pat

> instance VarsB TupleTerm where
>   varsB _ = []


======================================================================
Defino las instance de Vars
======================================================================

> instance (Vars a) => Vars (Acomponent a) where
>   vars (Acomp (bvs, termwrapper)) = vars termwrapper \\ vars bvs

> instance Vars Sigma where
>   vars (Sigma (_,listatps,_,hss)) = vars listatps ++ concat (map (maybe [] (concatMap varshs)) hss)
>     where varshs (_,apcomsInf,_,wca,_) = vars apcomsInf ++ vars wca

> instance Vars WrappedCA where
>   vars (WCApsi (bv, t0, psi)) = (vars t0 ++ vars psi) \\ vars bv
>   vars (WCAoutF (bv, t0, outf)) = (vars t0 ++ vars outf) \\ vars bv
>   vars (WCAsigma (bv, t0, sigma)) = (vars t0 ++ vars sigma) \\ vars bv

> instance Vars InF where
>   vars (InF (_,ts)) = vars ts

> instance Vars Tau where
>   vars (Tauphi tauphii) = vars tauphii
>   vars (TauinF tauinf) = vars tauinf
>   vars (Tautau tautau) = vars tautau

> instance Vars a => Vars (TermWrapper a) where
>   vars = foldTW (\t0 pts vs -> vars t0 ++ (concat vs \\ vars pts)) (\vs eta->vs++vars eta) vars vars [] 

> instance (Vars a) => Vars (TauTerm a) where
>   vars (Taucons _ tauterms a etai) = vars tauterms ++ vars a ++ vars etai
>   vars (Tausimple term) = vars term
>   vars (Taupair term tauterm) = vars term ++ vars tauterm
>   vars (Taucata _ tauterm) = vars tauterm

> instance Vars OutF where
>   vars (OutF outfis) = vars outfis

> instance Vars OutFi where
>   vars (OutFc (_,vs,tps)) = vars tps \\ vs

> instance Vars Psi where
>   vars (Psi psis) = vars psis

> instance Vars Psii where
>   vars (Psii (pat, tps)) = vars tps \\ vars pat

> instance Vars TupleTerm where
>   vars tt = vars (getTerm tt)

> instance Vars EtaOp where
>   vars EOid = []
>   vars (EOgeneral bvs ts) = vars ts \\ vars bvs
>   vars (EOsust _ ts bvs) = vars ts \\ vars bvs
>   vars (EOlet ts ps vs ts1) = (vars ts ++ (vars ts1 \\ vars ps)) \\ vs

> instance Vars Etai where
>   vars  (Etai (etaOp1,etaOp2)) = vars etaOp1 ++ vars etaOp2



> instance (AlphaConvertible a) => AlphaConvertible (Acomponent a) where
>   alphaConvert sc lvars  (Acomp (vs, termwrapper)) = Acomp (alphaConvert sc lvars vs,alphaConvert (sc++vars vs) lvars termwrapper)

> instance AlphaConvertible EtaOp where
>   alphaConvert _ _ EOid = EOid
>   alphaConvert sc lvars (EOgeneral bvs ts) = EOgeneral (alphaConvert sc lvars bvs) (alphaConvert (sc++vars bvs) lvars ts)
>   alphaConvert sc lvars (EOsust vs ts bvs) = EOsust (alphaConvert sc' lvars vs) 
>                                                   (alphaConvert sc' lvars ts) 
>                                                   (alphaConvert sc lvars bvs)
>     where sc'=sc++vars bvs
>   alphaConvert sc lvars (EOlet ts ps vs ts1) = EOlet (alphaConvert sc' lvars ts) 
>                                                    (alphaConvert sc' lvars ps)
>                                                    (alphaConvert sc lvars vs) 
>                                                    (alphaConvert (sc'++vars ps) lvars ts1)
>     where sc'=sc++vs

> instance AlphaConvertible Etai where
>   alphaConvert sc lvars  (Etai (etaOp1,etaOp2)) = Etai (alphaConvert sc lvars etaOp1, alphaConvert sc lvars etaOp2)

> instance (AlphaConvertible a) => AlphaConvertible (TermWrapper a) where
>   alphaConvert sc lvars tw = 
>         foldTW (\t0 ps ts sc -> TWcase (alphaConvert sc lvars t0)
>                                        (alphaConvert sc lvars ps) 
>                                        (zipWith ($) ts (map ((sc++).vars) ps))
>                ) 
>                (\t e sc ->TWeta (t sc) (alphaConvert sc lvars e)) (\t sc -> TWsimple (alphaConvert sc lvars t) )
>                (\t sc -> TWacomp (alphaConvert sc lvars t)) 
>                (const TWbottom) 
>                tw
>                sc


======================================================================
Coalgebra
======================================================================

> instance AlphaConvertible Psi where
>   alphaConvert sc lvars (Psi psis) = Psi (alphaConvert sc lvars psis)

> instance AlphaConvertible Psii where
>   alphaConvert sc lvars (Psii (pat, tuplets)) = Psii (alphaConvert sc lvars pat,alphaConvert (sc++vars pat) lvars tuplets)

> instance AlphaConvertible TupleTerm where
>   alphaConvert sc lvars (Tterm term position) = Tterm (alphaConvert sc lvars term) position

> instance AlphaConvertible InF where
>   alphaConvert sc lvars (InF (cons, ts)) = InF (cons,alphaConvert sc lvars ts)

> instance AlphaConvertible Sigma where
>   alphaConvert sc lvars (Sigma (casemap,listatupleterms, pss, hss)) = 
>                        Sigma (casemap,alphaConvert (sc++varsB pss) lvars listatupleterms, 
>                               map (alphaConvert sc lvars) pss, map (fmap (map ss)) hss)
>     where ss (i,compsInf, etais, wrappedCa, funcTermTerm) = 
>                 (i,alphaConvert sc lvars compsInf, alphaConvert sc lvars etais, alphaConvert sc lvars wrappedCa, funcTermTerm)

> instance AlphaConvertible WrappedCA where
>   alphaConvert sc lvars (WCApsi (bound,term,psi)) = WCApsi (alphaConvert sc lvars bound,alphaConvert sc' lvars term,alphaConvert sc' lvars psi)
>     where sc'=sc++vars bound
>   alphaConvert sc lvars (WCAoutF (bound,term,outf)) = WCAoutF (alphaConvert sc lvars bound,alphaConvert sc' lvars term,alphaConvert sc' lvars outf)
>     where sc'=sc++vars bound
>   alphaConvert sc lvars (WCAsigma (bound,term,sigma)) = WCAsigma (alphaConvert sc lvars bound,alphaConvert sc' lvars term,alphaConvert sc' lvars sigma)
>     where sc'=sc++vars bound

> instance AlphaConvertible PatternS where
>   alphaConvert sc susts (PcaseS t0 p t) = PcaseS (alphaConvert sc susts t0)
>                                                (alphaConvert sc susts p)
>                                                (alphaConvert sc' susts t) 
>     where sc'=sc++vars p
>   alphaConvert sc susts (PcaseSana i t0 p t) = PcaseSana i (alphaConvert sc susts t0)
>                                                        (alphaConvert sc susts p)
>                                                        (alphaConvert sc' susts t)
>     where sc'=sc++vars p
>   alphaConvert sc susts (PcaseR i t0 c vrs ts) = PcaseR i (alphaConvert sc susts t0) c (alphaConvert vrs susts vrs)
>                                                  (map (\ (t,pos)-> (alphaConvert (vrs++sc) susts t,pos)) ts)
>   alphaConvert sc susts (Ppattern v p) = Ppattern v (alphaConvert sc susts p)
>   alphaConvert _ _ t@Pdone = t

> instance AlphaConvertible OutFi where
>   alphaConvert sc lvars (OutFc (cons,vars,tupleterms)) = OutFc (cons,alphaConvert sc lvars vars,alphaConvert (sc++vars) lvars tupleterms)

> instance AlphaConvertible OutF where
>   alphaConvert sc lvars (OutF outfis) = OutF (alphaConvert sc lvars outfis)

> instance AlphaConvertible Tau where
>   alphaConvert sc lvars (Tauphi tau) = Tauphi (alphaConvert sc lvars tau)
>   alphaConvert sc lvars (TauinF tau) = TauinF (alphaConvert sc lvars tau)
>   alphaConvert sc lvars (Tautau tau) = Tautau (alphaConvert sc lvars tau)

> instance (AlphaConvertible a) => AlphaConvertible (TauTerm a) where
>   alphaConvert sc lvars (Taucons cons tauterms a etai) = Taucons cons (alphaConvert sc lvars tauterms) 
>                                                             (alphaConvert sc lvars a) (alphaConvert sc lvars etai)
>   alphaConvert sc lvars (Tausimple term) = Tausimple (alphaConvert sc lvars term)
>   alphaConvert sc lvars (Taupair term tauterm) = Taupair (alphaConvert sc lvars term) (alphaConvert sc lvars tauterm)
>   alphaConvert sc lvars (Taucata func tauterm) = Taucata (alphaConvert sc lvars.func) (alphaConvert sc lvars tauterm)