Safe Haskell | Safe-Inferred |
---|
DDC.Type.Transform.SubstituteT
Description
Capture avoiding substitution of types in types.
- substituteT :: (SubstituteT c, Ord n) => Bind n -> Type n -> c n -> c n
- substituteTs :: (SubstituteT c, Ord n) => [(Bind n, Type n)] -> c n -> c n
- substituteBoundT :: (SubstituteT c, Ord n) => Bound n -> Type n -> c n -> c n
- class SubstituteT c where
- data BindStack n = BindStack {
- stackBinds :: ![Bind n]
- stackAll :: ![Bind n]
- stackAnons :: !Int
- stackNamed :: !Int
- pushBind :: Ord n => Set n -> BindStack n -> Bind n -> (BindStack n, Bind n)
- pushBinds :: Ord n => Set n -> BindStack n -> [Bind n] -> (BindStack n, [Bind n])
- substBound :: Ord n => BindStack n -> Bound n -> Bound n -> Either (Bound n) Int
Documentation
substituteT :: (SubstituteT c, Ord n) => Bind n -> Type n -> c n -> c nSource
substituteTs :: (SubstituteT c, Ord n) => [(Bind n, Type n)] -> c n -> c nSource
Wrapper for substituteT
to substitute multiple things.
substituteBoundT :: (SubstituteT c, Ord n) => Bound n -> Type n -> c n -> c nSource
class SubstituteT c whereSource
Methods
Arguments
:: forall n . Ord n | |
=> Bound n | Bound variable that we're subsituting into. |
-> Type n | Type to substitute. |
-> Set n | Names of free varaibles in the type to substitute. |
-> BindStack n | Bind stack. |
-> c n | |
-> c n |
Substitute a type into some thing. In the target, if we find a named binder that would capture a free variable in the type to substitute, then we rewrite that binder to anonymous form, avoiding the capture.
Instances
Stack of anonymous binders that we've entered under during substitution.
Constructors
BindStack | |
Fields
|
Arguments
:: Ord n | |
=> Set n | Names that need to be rewritten. |
-> BindStack n | Current bind stack. |
-> Bind n | Bind to push. |
-> (BindStack n, Bind n) | New stack and possibly anonymised bind. |
Push a bind onto a bind stack, anonymizing it if need be to avoid variable capture.