Safe Haskell | Safe |
---|---|
Language | Haskell98 |
Renaming of variable binders to anonymous form to avoid capture.
- class Rename c where
- data Sub n = Sub {
- subBound :: !(Bound n)
- subShadow0 :: !Bool
- subConflict1 :: !(Set n)
- subConflict0 :: !(Set n)
- subStack1 :: !(BindStack n)
- subStack0 :: !(BindStack 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
- bind1 :: Ord n => Sub n -> Bind n -> (Sub n, Bind n)
- bind1s :: Ord n => Sub n -> [Bind n] -> (Sub n, [Bind n])
- bind0 :: Ord n => Sub n -> Bind n -> (Sub n, Bind n)
- bind0s :: Ord n => Sub n -> [Bind n] -> (Sub n, [Bind n])
- use1 :: Ord n => Sub n -> Bound n -> Bound n
- use0 :: Ord n => Sub n -> Bound n -> Bound n
Documentation
Substitution states
Substitution state. Keeps track of the binders in the environment that have been rewrittten to avoid variable capture or spec binder shadowing.
Sub | |
|
Binding stacks
Stack of anonymous binders that we've entered under during substitution.
BindStack | |
|
:: 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.
pushBinds :: Ord n => Set n -> BindStack n -> [Bind n] -> (BindStack n, [Bind n]) Source #
Push several binds onto the bind stack, anonymyzing them if need be to avoid variable capture.
:: Ord n | |
=> BindStack n | Current Bind stack during substitution. |
-> Bound n | Bound we're substituting for. |
-> Bound n | Bound we're looking at now. |
-> Either (Bound n) Int |
Compare a Bound
against the one we're substituting for.
Rewriting binding occurences
bind1 :: Ord n => Sub n -> Bind n -> (Sub n, Bind n) Source #
Push a level-1 binder on the rewrite stack.
bind1s :: Ord n => Sub n -> [Bind n] -> (Sub n, [Bind n]) Source #
Push some level-1 binders on the rewrite stack.
bind0 :: Ord n => Sub n -> Bind n -> (Sub n, Bind n) Source #
Push a level-0 binder on the rewrite stack.
bind0s :: Ord n => Sub n -> [Bind n] -> (Sub n, [Bind n]) Source #
Push some level-0 binders on the rewrite stack.