hfusion-0.0.6: HFusion/Internal/RenVars.lhs
-- 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 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)