Unbound.LocallyNameless.Subst

Documentation

data SubstName a b where

See isvar.

Constructors

SubstName :: a ~ b => Name a -> SubstName 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.

Methods

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

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.

subst :: Name b -> b -> a -> a

subst nm sub tm substitutes sub for nm in tm.

substs :: [(Name b, b)] -> a -> a

Perform several simultaneous substitutions.

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 b, Subst c a, Alpha a, Alpha b) => Subst c (Bind 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)

(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