Safe Haskell  SafeInferred 

Rewriting of variable binders to anonymous form to avoid capture.
 class Rewrite c where
 rewriteWith :: Ord n => Sub n > c n > c n
 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)
 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
rewriteWith :: Ord n => Sub n > c n > c nSource
Rewrite names in some thing to anonymous form if they conflict with
any names in the Sub
state.
Substitution state. Keeps track of the binders in the environment that have been rewrittten to avoid variable capture or spec binder shadowing.
Sub  

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.
bind1 :: Ord n => Sub n > Bind n > (Sub n, Bind n)Source
Push a level1 binder on the rewrite stack.
bind0 :: Ord n => Sub n > Bind n > (Sub n, Bind n)Source
Push a level0 binder on the rewrite stack.