| Portability | GHC only (-XKitchenSink) |
|---|---|
| Maintainer | Brent Yorgey <byorgey@cis.upenn.edu> |
| Safe Haskell | None |
Unbound.LocallyNameless.Subst
Description
The Subst type class for generic capture-avoiding substitution.
- data SubstName a b where
- data SubstCoerce a b where
- SubstCoerce :: Name b -> (b -> Maybe a) -> SubstCoerce a b
- class Rep1 (SubstD b) a => Subst b a where
- isvar :: a -> Maybe (SubstName a b)
- isCoerceVar :: a -> Maybe (SubstCoerce a b)
- subst :: Name b -> b -> a -> a
- substs :: [(Name b, b)] -> a -> a
- data SubstD b a = SubstD {}
- substDefault :: Rep1 (SubstD b) a => Name b -> b -> a -> a
- substR1 :: R1 (SubstD b) a -> Name b -> b -> a -> a
- substsR1 :: R1 (SubstD b) a -> [(Name b, b)] -> a -> a
Documentation
data SubstCoerce a b whereSource
See isCoerceVar
Constructors
| SubstCoerce :: Name b -> (b -> Maybe a) -> SubstCoerce a b |
class Rep1 (SubstD b) a => Subst b a whereSource
The Subst class governs capture-avoiding substitution. To
derive this class, you only need to indicate where the variables
are in the data type, by overriding the method isvar.
Methods
isvar :: a -> Maybe (SubstName a b)Source
This is the only method which normally needs to be implemented
explicitly. If the argument is a variable, return its name
wrapped in the SubstName constructor. Return Nothing for
non-variable arguments. The default implementation always
returns Nothing.
isCoerceVar :: a -> Maybe (SubstCoerce a b)Source
This is an alternative version to isvar, useable in the case
that the substituted argument doesn't have *exactly* the same type
as the term it should be substituted into.
The default implementation always returns Nothing.
subst :: Name b -> b -> a -> aSource
subst nm sub tmsub for nm in tm. It has
a default generic implementation in terms of isvar.
substs :: [(Name b, b)] -> a -> aSource
Perform several simultaneous substitutions. This method also
has a default generic implementation in terms of isvar.
Instances
| Subst b AnyName | |
| Subst b Double | |
| Subst b Float | |
| Subst b Integer | |
| Subst b Char | |
| Subst b () | |
| Subst b Bool | |
| Subst b Int | |
| (Alpha a, Subst c a) => Subst c (Rec a) | |
| Subst c a => Subst c (Embed a) | |
| Subst c a => Subst c (Maybe a) | |
| Subst c a => Subst c [a] | |
| Rep a => Subst b (Name a) | |
| Rep a => Subst b (R a) | |
| (Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Rebind a b) | |
| (Subst c a, Subst c b) => Subst c (Either a b) | |
| (Subst c a, Subst c b) => Subst c (a, b) | |
| (Subst c a, Subst c b, Subst c d) => Subst c (a, b, d) | |
| (Rep order, Rep card, Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (GenBind order card a b) | |
| (Subst c a, Subst c b, Subst c d, Subst c e) => Subst c (a, b, d, e) | |
| (Subst c a, Subst c b, Subst c d, Subst c e, Subst c f) => Subst c (a, b, d, e, f) |
substDefault :: Rep1 (SubstD b) a => Name b -> b -> a -> aSource