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

substBind :: Subst a b => Bind (Name a) b -> a -> b

Immediately substitute for a (single) bound variable in a binder, without first naming that variable.

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)

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.

substPat :: AlphaCtx -> b -> a -> a

substPats :: Proxy b -> AlphaCtx -> [Dyn] -> a -> a

Instances

Subst b AnyName

Defined in Unbound.LocallyNameless.Subst

Methods

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

isCoerceVar :: AnyName -> Maybe (SubstCoerce AnyName b)

subst :: Name b -> b -> AnyName -> AnyName

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

substPat :: AlphaCtx -> b -> AnyName -> AnyName

substPats :: Proxy b -> AlphaCtx -> [Dyn] -> AnyName -> AnyName

Subst b Double

Defined in Unbound.LocallyNameless.Subst

Methods

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

isCoerceVar :: Double -> Maybe (SubstCoerce Double b)

subst :: Name b -> b -> Double -> Double

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

substPat :: AlphaCtx -> b -> Double -> Double

substPats :: Proxy b -> AlphaCtx -> [Dyn] -> Double -> Double

Subst b Float

Defined in Unbound.LocallyNameless.Subst

Methods

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

isCoerceVar :: Float -> Maybe (SubstCoerce Float b)

subst :: Name b -> b -> Float -> Float

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

substPat :: AlphaCtx -> b -> Float -> Float

substPats :: Proxy b -> AlphaCtx -> [Dyn] -> Float -> Float

Subst b Integer

Defined in Unbound.LocallyNameless.Subst

Methods

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

isCoerceVar :: Integer -> Maybe (SubstCoerce Integer b)

subst :: Name b -> b -> Integer -> Integer

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

substPat :: AlphaCtx -> b -> Integer -> Integer

substPats :: Proxy b -> AlphaCtx -> [Dyn] -> Integer -> Integer

Subst b Char

Defined in Unbound.LocallyNameless.Subst

Methods

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

isCoerceVar :: Char -> Maybe (SubstCoerce Char b)

subst :: Name b -> b -> Char -> Char

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

substPat :: AlphaCtx -> b -> Char -> Char

substPats :: Proxy b -> AlphaCtx -> [Dyn] -> Char -> Char

Subst b ()

Defined in Unbound.LocallyNameless.Subst

Methods

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

isCoerceVar :: () -> Maybe (SubstCoerce () b)

subst :: Name b -> b -> () -> ()

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

substPat :: AlphaCtx -> b -> () -> ()

substPats :: Proxy b -> AlphaCtx -> [Dyn] -> () -> ()

Subst b Bool

Defined in Unbound.LocallyNameless.Subst

Methods

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

isCoerceVar :: Bool -> Maybe (SubstCoerce Bool b)

subst :: Name b -> b -> Bool -> Bool

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

substPat :: AlphaCtx -> b -> Bool -> Bool

substPats :: Proxy b -> AlphaCtx -> [Dyn] -> Bool -> Bool

Subst b Int

Defined in Unbound.LocallyNameless.Subst

Methods

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

isCoerceVar :: Int -> Maybe (SubstCoerce Int b)

subst :: Name b -> b -> Int -> Int

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

substPat :: AlphaCtx -> b -> Int -> Int

substPats :: Proxy b -> AlphaCtx -> [Dyn] -> Int -> Int

Subst c a => Subst c (Maybe a)

Defined in Unbound.LocallyNameless.Subst

Methods

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

isCoerceVar :: Maybe a -> Maybe (SubstCoerce (Maybe a) c)

subst :: Name c -> c -> Maybe a -> Maybe a

substs :: [(Name c, c)] -> Maybe a -> Maybe a

substPat :: AlphaCtx -> c -> Maybe a -> Maybe a

substPats :: Proxy c -> AlphaCtx -> [Dyn] -> Maybe a -> Maybe a

Subst c a => Subst c [a]

Defined in Unbound.LocallyNameless.Subst

Methods

isvar :: [a] -> Maybe (SubstName [a] c)

isCoerceVar :: [a] -> Maybe (SubstCoerce [a] c)

subst :: Name c -> c -> [a] -> [a]

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

substPat :: AlphaCtx -> c -> [a] -> [a]

substPats :: Proxy c -> AlphaCtx -> [Dyn] -> [a] -> [a]

Rep a => Subst b (Name a)

Defined in Unbound.LocallyNameless.Subst

Methods

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

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

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

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

substPat :: AlphaCtx -> b -> Name a -> Name a

substPats :: Proxy b -> AlphaCtx -> [Dyn] -> Name a -> Name a

Rep a => Subst b (R a)

Defined in Unbound.LocallyNameless.Subst

Methods

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

isCoerceVar :: R a -> Maybe (SubstCoerce (R a) b)

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

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

substPat :: AlphaCtx -> b -> R a -> R a

substPats :: Proxy b -> AlphaCtx -> [Dyn] -> R a -> R a

(Alpha a, Subst b a) => Subst b (Shift a)

Defined in Unbound.LocallyNameless.Subst

Methods

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

isCoerceVar :: Shift a -> Maybe (SubstCoerce (Shift a) b)

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

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

substPat :: AlphaCtx -> b -> Shift a -> Shift a

substPats :: Proxy b -> AlphaCtx -> [Dyn] -> Shift a -> Shift a

(Alpha t, Subst b t) => Subst b (Embed t)

Defined in Unbound.LocallyNameless.Subst

Methods

isvar :: Embed t -> Maybe (SubstName (Embed t) b)

isCoerceVar :: Embed t -> Maybe (SubstCoerce (Embed t) b)

subst :: Name b -> b -> Embed t -> Embed t

substs :: [(Name b, b)] -> Embed t -> Embed t

substPat :: AlphaCtx -> b -> Embed t -> Embed t

substPats :: Proxy b -> AlphaCtx -> [Dyn] -> Embed t -> Embed t

(Alpha p, Subst b p) => Subst b (Rec p)

Defined in Unbound.LocallyNameless.Subst

Methods

isvar :: Rec p -> Maybe (SubstName (Rec p) b)

isCoerceVar :: Rec p -> Maybe (SubstCoerce (Rec p) b)

subst :: Name b -> b -> Rec p -> Rec p

substs :: [(Name b, b)] -> Rec p -> Rec p

substPat :: AlphaCtx -> b -> Rec p -> Rec p

substPats :: Proxy b -> AlphaCtx -> [Dyn] -> Rec p -> Rec p

(Subst c a, Subst c b) => Subst c (Either a b)

Defined in Unbound.LocallyNameless.Subst

Methods

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

isCoerceVar :: Either a b -> Maybe (SubstCoerce (Either a b) c)

subst :: Name c -> c -> Either a b -> Either a b

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

substPat :: AlphaCtx -> c -> Either a b -> Either a b

substPats :: Proxy c -> AlphaCtx -> [Dyn] -> Either a b -> Either a b

(Subst c a, Subst c b) => Subst c (a, b)

Defined in Unbound.LocallyNameless.Subst

Methods

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

isCoerceVar :: (a, b) -> Maybe (SubstCoerce (a, b) c)

subst :: Name c -> c -> (a, b) -> (a, b)

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

substPat :: AlphaCtx -> c -> (a, b) -> (a, b)

substPats :: Proxy c -> AlphaCtx -> [Dyn] -> (a, b) -> (a, b)

(Alpha p, Alpha q, Subst b p, Subst b q) => Subst b (Rebind p q)

Defined in Unbound.LocallyNameless.Subst

Methods

isvar :: Rebind p q -> Maybe (SubstName (Rebind p q) b)

isCoerceVar :: Rebind p q -> Maybe (SubstCoerce (Rebind p q) b)

subst :: Name b -> b -> Rebind p q -> Rebind p q

substs :: [(Name b, b)] -> Rebind p q -> Rebind p q

substPat :: AlphaCtx -> b -> Rebind p q -> Rebind p q

substPats :: Proxy b -> AlphaCtx -> [Dyn] -> Rebind p q -> Rebind p q

(Subst c a, Subst c b, Subst c d) => Subst c (a, b, d)

Defined in Unbound.LocallyNameless.Subst

Methods

isvar :: (a, b, d) -> Maybe (SubstName (a, b, d) c)

isCoerceVar :: (a, b, d) -> Maybe (SubstCoerce (a, b, d) c)

subst :: Name c -> c -> (a, b, d) -> (a, b, d)

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

substPat :: AlphaCtx -> c -> (a, b, d) -> (a, b, d)

substPats :: Proxy c -> AlphaCtx -> [Dyn] -> (a, b, d) -> (a, b, d)

(Subst c a, Subst c b, Subst c d, Subst c e) => Subst c (a, b, d, e)

Defined in Unbound.LocallyNameless.Subst

Methods

isvar :: (a, b, d, e) -> Maybe (SubstName (a, b, d, e) c)

isCoerceVar :: (a, b, d, e) -> Maybe (SubstCoerce (a, b, d, e) c)

subst :: Name c -> c -> (a, b, d, e) -> (a, b, d, e)

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

substPat :: AlphaCtx -> c -> (a, b, d, e) -> (a, b, d, e)

substPats :: Proxy c -> AlphaCtx -> [Dyn] -> (a, b, d, e) -> (a, b, d, e)

(Rep order, Rep card, Alpha p, Alpha t, Subst b p, Subst b t) => Subst b (GenBind order card p t)

Defined in Unbound.LocallyNameless.Subst

Methods

isvar :: GenBind order card p t -> Maybe (SubstName (GenBind order card p t) b)

isCoerceVar :: GenBind order card p t -> Maybe (SubstCoerce (GenBind order card p t) b)

subst :: Name b -> b -> GenBind order card p t -> GenBind order card p t

substs :: [(Name b, b)] -> GenBind order card p t -> GenBind order card p t

substPat :: AlphaCtx -> b -> GenBind order card p t -> GenBind order card p t

substPats :: Proxy b -> AlphaCtx -> [Dyn] -> GenBind order card p t -> GenBind order card p t

(Subst c a, Subst c b, Subst c d, Subst c e, Subst c f) => Subst c (a, b, d, e, f)

Defined in Unbound.LocallyNameless.Subst

Methods

isvar :: (a, b, d, e, f) -> Maybe (SubstName (a, b, d, e, f) c)

isCoerceVar :: (a, b, d, e, f) -> Maybe (SubstCoerce (a, b, d, e, f) c)

subst :: Name c -> c -> (a, b, d, e, f) -> (a, b, d, e, f)

substs :: [(Name c, c)] -> (a, b, d, e, f) -> (a, b, d, e, f)

substPat :: AlphaCtx -> c -> (a, b, d, e, f) -> (a, b, d, e, f)

substPats :: Proxy c -> AlphaCtx -> [Dyn] -> (a, b, d, e, f) -> (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
• substPatD :: AlphaCtx -> b -> a -> a
• substPatsD :: Proxy b -> AlphaCtx -> [Dyn] -> a -> a

Instances

Subst b a => Sat (SubstD b a)

Defined in Unbound.LocallyNameless.Subst

Methods

dict :: 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

substPatsR1 :: R1 (SubstD b) a -> Proxy b -> AlphaCtx -> [Dyn] -> a -> a

substPatR1 :: R1 (SubstD b) a -> AlphaCtx -> b -> a -> a