| Copyright | (c) 2011 Patrick Bahr |
|---|---|
| License | BSD3 |
| Maintainer | Patrick Bahr <paba@diku.dk> |
| Stability | experimental |
| Portability | non-portable (GHC Extensions) |
| Safe Haskell | None |
| Language | Haskell98 |
Data.Comp.Multi.Variables
Description
This module defines an abstract notion of (bound) variables in compositional data types, and scoped substitution. Capture-avoidance is not taken into account. All definitions are generalised versions of those in Data.Comp.Variables.
Synopsis
- class HasVars v (f :: (* -> *) -> * -> *) where
- type GSubst v a = Map v (A a)
- type CxtSubst h a f v = GSubst v (Cxt h f a)
- type Subst f v = CxtSubst NoHole (K ()) f v
- varsToHoles :: forall f v. (HTraversable f, HasVars v f, Ord v) => HFix f :-> Context f (K v)
- containsVar :: (Ord v, HasVars v f, HTraversable f, HFunctor f) => v -> Cxt h f a :=> Bool
- variables :: (Ord v, HasVars v f, HTraversable f, HFunctor f) => Cxt h f a :=> Set v
- variableList :: (HasVars v f, HTraversable f, HFunctor f, Ord v) => Cxt h f a :=> [v]
- variables' :: (Ord v, HasVars v f, HFoldable f, HFunctor f) => Const f :=> Set v
- appSubst :: (Ord v, SubstVars v t a) => GSubst v t -> a :-> a
- compSubst :: (Ord v, HasVars v f, HTraversable f) => CxtSubst h a f v -> CxtSubst h a f v -> CxtSubst h a f v
- getBoundVars :: forall f a v i. (HasVars v f, HTraversable f) => f a i -> f (a :*: K (Set v)) i
- (&) :: Mapping m k => m v -> m v -> m v
- (|->) :: Mapping m k => k i -> v -> m v
- empty :: Mapping m k => m v
Documentation
class HasVars v (f :: (* -> *) -> * -> *) 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.
Minimal complete definition
Nothing
Methods
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 i e = Let Var (e i) (e i) 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.
varsToHoles :: forall f v. (HTraversable f, HasVars v f, Ord v) => HFix f :-> Context f (K v) Source #
containsVar :: (Ord v, HasVars v f, HTraversable f, HFunctor f) => v -> Cxt h f a :=> Bool Source #
This function checks whether a variable is contained in a context.
variables :: (Ord v, HasVars v f, HTraversable f, HFunctor f) => Cxt h f a :=> Set v Source #
This function computes the set of variables occurring in a context.
variableList :: (HasVars v f, HTraversable f, HFunctor f, Ord v) => Cxt h f a :=> [v] Source #
This function computes the list of variables occurring in a context.
variables' :: (Ord v, HasVars v f, HFoldable f, HFunctor f) => Const f :=> Set v Source #
This function computes the set of variables occurring in a context.
compSubst :: (Ord v, HasVars v f, HTraversable 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 :: forall f a v i. (HasVars v f, HTraversable f) => f a i -> f (a :*: K (Set v)) i 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.