Copyright | (c) 2010-2011 Patrick Bahr |
---|---|
License | BSD3 |
Maintainer | Patrick Bahr <paba@diku.dk> and Tom Hvitved <hvitved@diku.dk> |
Stability | experimental |
Portability | non-portable (GHC Extensions) |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
This module defines an abstract notion of (bound) variables in compositional data types, and scoped substitution. Capture-avoidance is not taken into account.
Synopsis
- class HasVars f v where
- type Subst f v = CxtSubst NoHole () f v
- type CxtSubst h a f v = Map v (Cxt h f a)
- varsToHoles :: (Traversable f, HasVars f v, Ord v) => Term f -> Context f v
- containsVar :: (Eq v, HasVars f v, Traversable f, Ord v) => v -> Cxt h f a -> Bool
- variables :: (Ord v, HasVars f v, Traversable f) => Cxt h f a -> Set v
- variableList :: (Ord v, HasVars f v, Traversable f) => Cxt h f a -> [v]
- variables' :: (Ord v, HasVars f v, Foldable f, Functor f) => Const f -> Set v
- substVars :: SubstVars v t a => (v -> Maybe t) -> a -> a
- appSubst :: (Ord v, SubstVars v t a) => Map v t -> a -> a
- compSubst :: (Ord v, HasVars f v, Traversable f) => CxtSubst h a f v -> CxtSubst h a f v -> CxtSubst h a f v
- getBoundVars :: (HasVars f v, Traversable f) => f a -> f (Set v, a)
- (&) :: Mapping m k => m v -> m v -> m v
- (|->) :: Mapping m k => k -> v -> m v
- empty :: Mapping m k => m v
Documentation
class HasVars f v where Source #
This multiparameter class defines functors with variables. An instance
HasVar f v
denotes that values over f
might contain and bind variables of
type v
.
Nothing
isVar :: f a -> Maybe v Source #
Indicates whether the f
constructor is a variable. The
default implementation returns Nothing
.
bindsVars :: Mapping m a => f a -> m (Set v) Source #
Indicates the set of variables bound by the f
constructor
for each argument of the constructor. For example for a
non-recursive let binding:
data Let e = Let Var e e instance HasVars Let Var where bindsVars (Let v x y) = y |-> Set.singleton v
If, instead, the let binding is recursive, the methods has to be implemented like this:
bindsVars (Let v x y) = x |-> Set.singleton v & y |-> Set.singleton v
This indicates that the scope of the bound variable also extends to the right-hand side of the variable binding.
The default implementation returns the empty map.
type Subst f v = CxtSubst NoHole () f v Source #
This type represents substitutions of terms, i.e. finite mappings from variables to terms.
type CxtSubst h a f v = Map v (Cxt h f a) Source #
This type represents substitutions of contexts, i.e. finite mappings from variables to contexts.
varsToHoles :: (Traversable f, HasVars f v, Ord v) => Term f -> Context f v Source #
Convert variables to holes, except those that are bound.
containsVar :: (Eq v, HasVars f v, Traversable f, Ord v) => v -> Cxt h f a -> Bool Source #
This function checks whether a variable is contained in a context.
variables :: (Ord v, HasVars f v, Traversable f) => Cxt h f a -> Set v Source #
This function computes the set of variables occurring in a context.
variableList :: (Ord v, HasVars f v, Traversable f) => Cxt h f a -> [v] Source #
This function computes the list of variables occurring in a context.
variables' :: (Ord v, HasVars f v, Foldable f, Functor f) => Const f -> Set v Source #
This function computes the set of variables occurring in a constant.
compSubst :: (Ord v, HasVars f v, Traversable f) => CxtSubst h a f v -> CxtSubst h a f v -> CxtSubst h a f v Source #
This function composes two substitutions s1
and s2
. That is,
applying the resulting substitution is equivalent to first applying
s2
and then s1
.
getBoundVars :: (HasVars f v, Traversable f) => f a -> f (Set v, a) Source #
This combinator pairs every argument of a given constructor with
the set of (newly) bound variables according to the corresponding
HasVars
type class instance.