License	BSD-like (see LICENSE)
Maintainer	Brent Yorgey <byorgey@cis.upenn.edu>
Portability	GHC only (-XKitchenSink)
Safe Haskell	None
Language	Haskell2010

Unbound.LocallyNameless.Subst

Description

The Subst type class for generic capture-avoiding substitution.

Synopsis

Documentation

data SubstName a b where Source #

See isvar.

Constructors

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

data SubstCoerce a b where Source #

See isCoerceVar

Constructors

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.

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

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

Instances

Subst b AnyName Source #
Methods isvar :: AnyName -> Maybe (SubstName AnyName b) Source # isCoerceVar :: AnyName -> Maybe (SubstCoerce AnyName b) Source # subst :: Name b -> b -> AnyName -> AnyName Source # substs :: [(Name b, b)] -> AnyName -> AnyName Source # substPat :: AlphaCtx -> b -> AnyName -> AnyName Source # substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> AnyName -> AnyName Source #
Subst b Double Source #
Methods isvar :: Double -> Maybe (SubstName Double b) Source # isCoerceVar :: Double -> Maybe (SubstCoerce Double b) Source # subst :: Name b -> b -> Double -> Double Source # substs :: [(Name b, b)] -> Double -> Double Source # substPat :: AlphaCtx -> b -> Double -> Double Source # substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> Double -> Double Source #
Subst b Float Source #
Methods isvar :: Float -> Maybe (SubstName Float b) Source # isCoerceVar :: Float -> Maybe (SubstCoerce Float b) Source # subst :: Name b -> b -> Float -> Float Source # substs :: [(Name b, b)] -> Float -> Float Source # substPat :: AlphaCtx -> b -> Float -> Float Source # substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> Float -> Float Source #
Subst b Integer Source #
Methods isvar :: Integer -> Maybe (SubstName Integer b) Source # isCoerceVar :: Integer -> Maybe (SubstCoerce Integer b) Source # subst :: Name b -> b -> Integer -> Integer Source # substs :: [(Name b, b)] -> Integer -> Integer Source # substPat :: AlphaCtx -> b -> Integer -> Integer Source # substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> Integer -> Integer Source #
Subst b Char Source #
Methods isvar :: Char -> Maybe (SubstName Char b) Source # isCoerceVar :: Char -> Maybe (SubstCoerce Char b) Source # subst :: Name b -> b -> Char -> Char Source # substs :: [(Name b, b)] -> Char -> Char Source # substPat :: AlphaCtx -> b -> Char -> Char Source # substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> Char -> Char Source #
Subst b () Source #
Methods isvar :: () -> Maybe (SubstName () b) Source # isCoerceVar :: () -> Maybe (SubstCoerce () b) Source # subst :: Name b -> b -> () -> () Source # substs :: [(Name b, b)] -> () -> () Source # substPat :: AlphaCtx -> b -> () -> () Source # substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> () -> () Source #
Subst b Bool Source #
Methods isvar :: Bool -> Maybe (SubstName Bool b) Source # isCoerceVar :: Bool -> Maybe (SubstCoerce Bool b) Source # subst :: Name b -> b -> Bool -> Bool Source # substs :: [(Name b, b)] -> Bool -> Bool Source # substPat :: AlphaCtx -> b -> Bool -> Bool Source # substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> Bool -> Bool Source #
Subst b Int Source #
Methods isvar :: Int -> Maybe (SubstName Int b) Source # isCoerceVar :: Int -> Maybe (SubstCoerce Int b) Source # subst :: Name b -> b -> Int -> Int Source # substs :: [(Name b, b)] -> Int -> Int Source # substPat :: AlphaCtx -> b -> Int -> Int Source # substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> Int -> Int Source #
Subst c a => Subst c (Maybe a) Source #
Methods isvar :: Maybe a -> Maybe (SubstName (Maybe a) c) Source # isCoerceVar :: Maybe a -> Maybe (SubstCoerce (Maybe a) c) Source # subst :: Name c -> c -> Maybe a -> Maybe a Source # substs :: [(Name c, c)] -> Maybe a -> Maybe a Source # substPat :: AlphaCtx -> c -> Maybe a -> Maybe a Source # substPats :: Proxy * c -> AlphaCtx -> [Dyn] -> Maybe a -> Maybe a Source #
Subst c a => Subst c [a] Source #
Methods isvar :: [a] -> Maybe (SubstName [a] c) Source # isCoerceVar :: [a] -> Maybe (SubstCoerce [a] c) Source # subst :: Name c -> c -> [a] -> [a] Source # substs :: [(Name c, c)] -> [a] -> [a] Source # substPat :: AlphaCtx -> c -> [a] -> [a] Source # substPats :: Proxy * c -> AlphaCtx -> [Dyn] -> [a] -> [a] Source #
Rep a => Subst b (Name a) Source #
Methods isvar :: Name a -> Maybe (SubstName (Name a) b) Source # isCoerceVar :: Name a -> Maybe (SubstCoerce (Name a) b) Source # subst :: Name b -> b -> Name a -> Name a Source # substs :: [(Name b, b)] -> Name a -> Name a Source # substPat :: AlphaCtx -> b -> Name a -> Name a Source # substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> Name a -> Name a Source #
Rep a => Subst b (R a) Source #
Methods isvar :: R a -> Maybe (SubstName (R a) b) Source # isCoerceVar :: R a -> Maybe (SubstCoerce (R a) b) Source # subst :: Name b -> b -> R a -> R a Source # substs :: [(Name b, b)] -> R a -> R a Source # substPat :: AlphaCtx -> b -> R a -> R a Source # substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> R a -> R a Source #
(Alpha a, Subst b a) => Subst b (Shift a) Source #
Methods isvar :: Shift a -> Maybe (SubstName (Shift a) b) Source # isCoerceVar :: Shift a -> Maybe (SubstCoerce (Shift a) b) Source # subst :: Name b -> b -> Shift a -> Shift a Source # substs :: [(Name b, b)] -> Shift a -> Shift a Source # substPat :: AlphaCtx -> b -> Shift a -> Shift a Source # substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> Shift a -> Shift a Source #
(Alpha t, Subst b t) => Subst b (Embed t) Source #
Methods isvar :: Embed t -> Maybe (SubstName (Embed t) b) Source # isCoerceVar :: Embed t -> Maybe (SubstCoerce (Embed t) b) Source # subst :: Name b -> b -> Embed t -> Embed t Source # substs :: [(Name b, b)] -> Embed t -> Embed t Source # substPat :: AlphaCtx -> b -> Embed t -> Embed t Source # substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> Embed t -> Embed t Source #
(Alpha p, Subst b p) => Subst b (Rec p) Source #
Methods isvar :: Rec p -> Maybe (SubstName (Rec p) b) Source # isCoerceVar :: Rec p -> Maybe (SubstCoerce (Rec p) b) Source # subst :: Name b -> b -> Rec p -> Rec p Source # substs :: [(Name b, b)] -> Rec p -> Rec p Source # substPat :: AlphaCtx -> b -> Rec p -> Rec p Source # substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> Rec p -> Rec p Source #
(Subst c a, Subst c b) => Subst c (Either a b) Source #
Methods isvar :: Either a b -> Maybe (SubstName (Either a b) c) Source # isCoerceVar :: Either a b -> Maybe (SubstCoerce (Either a b) c) Source # subst :: Name c -> c -> Either a b -> Either a b Source # substs :: [(Name c, c)] -> Either a b -> Either a b Source # substPat :: AlphaCtx -> c -> Either a b -> Either a b Source # substPats :: Proxy * c -> AlphaCtx -> [Dyn] -> Either a b -> Either a b Source #
(Subst c a, Subst c b) => Subst c (a, b) Source #
Methods isvar :: (a, b) -> Maybe (SubstName (a, b) c) Source # isCoerceVar :: (a, b) -> Maybe (SubstCoerce (a, b) c) Source # subst :: Name c -> c -> (a, b) -> (a, b) Source # substs :: [(Name c, c)] -> (a, b) -> (a, b) Source # substPat :: AlphaCtx -> c -> (a, b) -> (a, b) Source # substPats :: Proxy * c -> AlphaCtx -> [Dyn] -> (a, b) -> (a, b) Source #
(Alpha p, Alpha q, Subst b p, Subst b q) => Subst b (Rebind p q) Source #
Methods isvar :: Rebind p q -> Maybe (SubstName (Rebind p q) b) Source # isCoerceVar :: Rebind p q -> Maybe (SubstCoerce (Rebind p q) b) Source # subst :: Name b -> b -> Rebind p q -> Rebind p q Source # substs :: [(Name b, b)] -> Rebind p q -> Rebind p q Source # substPat :: AlphaCtx -> b -> Rebind p q -> Rebind p q Source # substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> Rebind p q -> Rebind p q Source #
(Subst c a, Subst c b, Subst c d) => Subst c (a, b, d) Source #
Methods isvar :: (a, b, d) -> Maybe (SubstName (a, b, d) c) Source # isCoerceVar :: (a, b, d) -> Maybe (SubstCoerce (a, b, d) c) Source # subst :: Name c -> c -> (a, b, d) -> (a, b, d) Source # substs :: [(Name c, c)] -> (a, b, d) -> (a, b, d) Source # substPat :: AlphaCtx -> c -> (a, b, d) -> (a, b, d) Source # substPats :: Proxy * c -> AlphaCtx -> [Dyn] -> (a, b, d) -> (a, b, d) Source #
(Subst c a, Subst c b, Subst c d, Subst c e) => Subst c (a, b, d, e) Source #
Methods isvar :: (a, b, d, e) -> Maybe (SubstName (a, b, d, e) c) Source # isCoerceVar :: (a, b, d, e) -> Maybe (SubstCoerce (a, b, d, e) c) Source # subst :: Name c -> c -> (a, b, d, e) -> (a, b, d, e) Source # substs :: [(Name c, c)] -> (a, b, d, e) -> (a, b, d, e) Source # substPat :: AlphaCtx -> c -> (a, b, d, e) -> (a, b, d, e) Source # substPats :: Proxy * c -> AlphaCtx -> [Dyn] -> (a, b, d, e) -> (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 #
Methods isvar :: GenBind order card p t -> Maybe (SubstName (GenBind order card p t) b) Source # isCoerceVar :: GenBind order card p t -> Maybe (SubstCoerce (GenBind order card p t) b) Source # subst :: Name b -> b -> GenBind order card p t -> GenBind order card p t Source # substs :: [(Name b, b)] -> GenBind order card p t -> GenBind order card p t Source # substPat :: AlphaCtx -> b -> GenBind order card p t -> GenBind order card p t Source # substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> GenBind order card p t -> 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 #
Methods isvar :: (a, b, d, e, f) -> Maybe (SubstName (a, b, d, e, f) c) Source # isCoerceVar :: (a, b, d, e, f) -> Maybe (SubstCoerce (a, b, d, e, f) c) Source # subst :: Name c -> c -> (a, b, d, e, f) -> (a, b, d, e, f) Source # substs :: [(Name c, c)] -> (a, b, d, e, f) -> (a, b, d, e, f) Source # substPat :: AlphaCtx -> c -> (a, b, d, e, f) -> (a, b, d, e, f) Source # substPats :: Proxy * c -> AlphaCtx -> [Dyn] -> (a, b, d, e, f) -> (a, b, d, e, f) Source #

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 substPatD :: AlphaCtx -> b -> a -> a substPatsD :: Proxy b -> AlphaCtx -> [Dyn] -> a -> a

Instances

Subst b a => Sat (SubstD b a) Source #
Methods dict :: SubstD b a #

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

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

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

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

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