| 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
- substituteWithT :: forall n. Ord n => Bound n -> Type n -> Set n -> BindStack n -> c n -> c n
- 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.