License | BSD-like (see LICENSE) |
---|---|
Maintainer | Brent Yorgey <byorgey@cis.upenn.edu> |
Portability | GHC only (-XKitchenSink) |
Safe Haskell | None |
Language | Haskell2010 |
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
- substBind :: Subst a b => Bind (Name a) b -> a -> b
- class Rep1 (SubstD b) a => Subst b a where
- 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
- substPatsR1 :: R1 (SubstD b) a -> Proxy b -> AlphaCtx -> [Dyn] -> a -> a
- substPatR1 :: R1 (SubstD b) a -> AlphaCtx -> b -> a -> a
Documentation
data SubstCoerce a b where Source #
See isCoerceVar
SubstCoerce :: Name b -> (b -> Maybe a) -> SubstCoerce a b |
substBind :: Subst a b => Bind (Name a) b -> a -> b Source #
Immediately substitute for a (single) bound variable in a binder, without first naming that variable.
class Rep1 (SubstD b) a => Subst b a where Source #
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
.
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 -> a Source #
substitutes subst
nm sub tmsub
for nm
in tm
. It has
a default generic implementation in terms of isvar
.
substs :: [(Name b, b)] -> a -> a Source #
Perform several simultaneous substitutions. This method also
has a default generic implementation in terms of isvar
.
substPat :: AlphaCtx -> b -> a -> a Source #
substPats :: Proxy b -> AlphaCtx -> [Dyn] -> a -> a Source #
Subst b AnyName Source # | |
Subst b Double Source # | |
Subst b Float Source # | |
Subst b Integer Source # | |
Subst b Char Source # | |
Subst b () Source # | |
Subst b Bool Source # | |
Subst b Int Source # | |
Subst c a => Subst c (Maybe a) Source # | |
Subst c a => Subst c [a] Source # | |
Rep a => Subst b (Name a) Source # | |
Rep a => Subst b (R a) Source # | |
(Alpha a, Subst b a) => Subst b (Shift a) Source # | |
(Alpha t, Subst b t) => Subst b (Embed t) Source # | |
(Alpha p, Subst b p) => Subst b (Rec p) Source # | |
(Subst c a, Subst c b) => Subst c (Either a b) Source # | |
(Subst c a, Subst c b) => Subst c (a, b) Source # | |
(Alpha p, Alpha q, Subst b p, Subst b q) => Subst b (Rebind p q) Source # | |
(Subst c a, Subst c b, Subst c d) => Subst c (a, b, d) Source # | |
(Subst c a, Subst c b, Subst c d, Subst c e) => Subst c (a, b, d, e) Source # | |
(Rep order, Rep card, Alpha p, Alpha t, Subst b p, Subst b t) => Subst b (GenBind order card p t) Source # | |
(Subst c a, Subst c b, Subst c d, Subst c e, Subst c f) => Subst c (a, b, d, e, f) Source # | |