Unbound.LocallyNameless.Subst

The Subst type class for generic capture-avoiding substitution.

Documentation

data SubstName a b where

See isvar.

Constructors

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

data SubstCoerce a b where

See isCoerceVar

Constructors

SubstCoerce :: Name b -> (b -> Maybe a) -> SubstCoerce a b

class Rep1 (SubstD b) a => Subst b a where

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.

Minimal complete definition

Nothing

Methods

isvar :: a -> Maybe (SubstName a b)

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)

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

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 -> a

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 (Shift 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

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 -> a

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

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