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 level1 binder on the rewrite stack.
bind1s :: Ord n => Sub n > [Bind n] > (Sub n, [Bind n]) Source #
Push some level1 binders on the rewrite stack.
bind0 :: Ord n => Sub n > Bind n > (Sub n, Bind n) Source #
Push a level0 binder on the rewrite stack.
bind0s :: Ord n => Sub n > [Bind n] > (Sub n, [Bind n]) Source #
Push some level0 binders on the rewrite stack.