Safe Haskell | Safe-Infered |
---|
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 level-1 binder 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.