module DDC.Type.Transform.SubstituteT
( substituteT
, substituteTs
, substituteBoundT
, SubstituteT(..)
, BindStack(..)
, pushBind
, pushBinds
, substBound)
where
import DDC.Type.Collect
import DDC.Type.Compounds
import DDC.Type.Transform.BoundT
import DDC.Type.Transform.Rename
import DDC.Type.Exp
import Data.Maybe
import qualified DDC.Type.Sum as Sum
import qualified DDC.Type.Env as Env
import qualified Data.Set as Set
import Data.Set (Set)
substituteT :: (SubstituteT c, Ord n) => Bind n -> Type n -> c n -> c n
substituteT b t x
= case takeSubstBoundOfBind b of
Just u -> substituteBoundT u t x
_ -> x
substituteTs :: (SubstituteT c, Ord n) => [(Bind n, Type n)] -> c n -> c n
substituteTs bts x
= foldr (uncurry substituteT) x bts
substituteBoundT :: (SubstituteT c, Ord n) => Bound n -> Type n -> c n -> c n
substituteBoundT u t x
= let
freeNames = Set.fromList
$ mapMaybe takeNameOfBound
$ Set.toList
$ freeT Env.empty t
stack = BindStack [] [] 0 0
in substituteWithT u t freeNames stack x
class SubstituteT (c :: * -> *) where
substituteWithT
:: forall n. Ord n
=> Bound n
-> Type n
-> Set n
-> BindStack n
-> c n -> c n
instance SubstituteT Bind where
substituteWithT u fvs t stack bb
= let k' = substituteWithT u fvs t stack $ typeOfBind bb
in replaceTypeOfBind k' bb
instance SubstituteT Type where
substituteWithT u t fns stack tt
= let down = substituteWithT u t fns stack
in case tt of
TCon{} -> tt
TApp t1 t2 -> TApp (down t1) (down t2)
TSum ss -> TSum (down ss)
TForall b tBody
| namedBoundMatchesBind u b -> tt
| otherwise
-> let
bSub = down b
(stack', b') = pushBind fns stack bSub
tBody' = substituteWithT u t fns stack' tBody
in TForall b' tBody'
TVar u'
-> case substBound stack u u' of
Left u'' -> TVar u''
Right n -> liftT n t
instance SubstituteT TypeSum where
substituteWithT u n fns stack ss
= let k = substituteWithT u n fns stack
$ Sum.kindOfSum ss
in Sum.fromList k
$ map (substituteWithT u n fns stack)
$ Sum.toList ss