| Copyright | (c) 2014 Aleksey Kliger |
|---|---|
| License | BSD3 (See LICENSE) |
| Maintainer | Aleksey Kliger |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Unbound.Generics.LocallyNameless.Subst
Contents
Description
A typeclass for types that may participate in capture-avoiding substitution
The minimal definition is empty, provided your type is an instance of Generic
type Var = Name Factor data Expr = SumOf [Summand] deriving (Show, Generic) data Summand = ProductOf [Factor] deriving (Show, Generic) instance Subst Var Expr instance Subst Var Summand
The default instance just propagates the substitution into the constituent factors.
If you identify the variable occurrences by implementing the isvar function, the derived subst function will be able to substitute a factor for a variable.
data Factor = V Var | C Int | Subexpr Expr deriving (Show, Generic) instance Subst Var Factor where isvar (V v) = Just (SubstName v) isvar _ = Nothing
Synopsis
- data SubstName a b where
- data SubstCoerce a b where
- SubstCoerce :: forall b a. Name b -> (b -> Maybe a) -> SubstCoerce a b
- class Subst b a where
- substBind :: Subst a t => Bind (Name a) t -> a -> t
- instantiate :: (Alpha a, Alpha b, Alpha p, Subst a b) => Bind p b -> [a] -> b
Documentation
data SubstCoerce a b where Source #
See isCoerceVar
Constructors
| SubstCoerce :: forall b a. Name b -> (b -> Maybe a) -> SubstCoerce a b |
class Subst b a where Source #
Instances of Subst b aa that may contain variables of type b that may participate in capture-avoiding substitution.
Minimal complete definition
Nothing
Methods
isvar :: a -> Maybe (SubstName a b) Source #
This is the only method that must be implemented
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 e tme for nm in tm. It has a default generic implementation in terms of isvar
Instances
substBind :: Subst a t => Bind (Name a) t -> a -> t Source #
Specialized version of capture-avoiding substitution for that operates on a Bind (Name a) tunbindName a and immediately subsitute a new term for its occurrences.
This is a specialization of instantiate :: Bind pat term -> [a] -> termBind pat termName aa. Unlike instantiate, this function cannot fail at runtime.
instantiate :: (Alpha a, Alpha b, Alpha p, Subst a b) => Bind p b -> [a] -> b Source #
Immediately substitute for the bound variables of a pattern in a binder, without first naming the variables. NOTE: this operation does not check that the number of terms passed in match the number of variables in the pattern. (Or that they are of appropriate type.)