| Safe Haskell | Safe |
|---|---|
| Language | Haskell98 |
DDC.Core.Transform.AnonymizeX
Description
Rewrite all binders to anonymous deBruijn form.
- anonymizeX :: (Ord n, AnonymizeX c) => c n -> c n
- class AnonymizeX c where
- anonymizeWithX :: forall n. Ord n => Set n -> [Bind n] -> [Bind n] -> c n -> c n
- pushAnonymizeBindX :: Ord n => Set n -> [Bind n] -> [Bind n] -> Bind n -> ([Bind n], Bind n)
Documentation
anonymizeX :: (Ord n, AnonymizeX c) => c n -> c n Source
Rewrite all binders in a thing to anonymous form.
class AnonymizeX c where Source
Methods
Arguments
| :: Ord n | |
| => Set n | Don't anonymize level-0 binders with these names. |
| -> [Bind n] | Stack for Spec binders (level-1). |
| -> [Bind n] | Stack for Data and Witness binders (level-0). |
| -> c n | |
| -> c n |
Rewrite all binders in a thing to be anonymous. The stacks contains existing anonymous binders that we have entered into, and named binders that we have rewritten. All bound occurrences of variables will be replaced by references into these stacks.
Instances
| AnonymizeX Bind Source | |
| AnonymizeX (Module a) Source | |
| AnonymizeX (Exp a) Source | |
| AnonymizeX (Alt a) Source | |
| AnonymizeX (Cast a) Source | |
| AnonymizeX (Witness a) Source |
Arguments
| :: Ord n | |
| => Set n | Don't anonymize binders with these names. |
| -> [Bind n] | Stack for Spec binders (level-1) |
| -> [Bind n] | Stack for Value and Witness binders (level-0) |
| -> Bind n | |
| -> ([Bind n], Bind n) |
Push a binding occurrence of a level-0 on the stack, returning the anonyized binding occurrence and the new stack.