unbound-0.4.2: Generic support for programming with names and binders

PortabilityGHC only (-XKitchenSink)
MaintainerBrent Yorgey <byorgey@cis.upenn.edu>
Safe HaskellNone

Unbound.LocallyNameless.Subst

Description

The Subst type class for generic capture-avoiding substitution.

Synopsis

Documentation

data SubstName a b whereSource

See isvar.

Constructors

SubstName :: a ~ b => Name a -> SubstName a b 

data SubstCoerce a b whereSource

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 tm substitutes sub 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) 

data SubstD b a Source

Reified class dictionary for Subst.

Constructors

SubstD 

Fields

isvarD :: a -> Maybe (SubstName a b)
 
substD :: Name b -> b -> a -> a
 
substsD :: [(Name b, b)] -> a -> a
 

Instances

Subst b a => Sat (SubstD b a) 

substDefault :: Rep1 (SubstD b) a => Name b -> b -> a -> aSource

substR1 :: R1 (SubstD b) a -> Name b -> b -> a -> aSource

substsR1 :: R1 (SubstD b) a -> [(Name b, b)] -> a -> aSource