compdata-0.12: Compositional Data Types

Copyright (c) 2010-2011 Patrick Bahr BSD3 Patrick Bahr and Tom Hvitved experimental non-portable (GHC Extensions) None Haskell98

Data.Comp.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.

Synopsis

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

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

Instances
 HasVars f v => HasVars (f :&: a) v Source # Instance detailsDefined in Data.Comp.Variables MethodsisVar :: (f :&: a) a0 -> Maybe v Source #bindsVars :: Mapping m a0 => (f :&: a) a0 -> m (Set v) Source # (HasVars f v, HasVars g v) => HasVars (f :+: g) v Source # Instance detailsDefined in Data.Comp.Variables MethodsisVar :: (f :+: g) a -> Maybe v Source #bindsVars :: Mapping m a => (f :+: g) a -> m (Set v) Source #

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.

substVars :: SubstVars v t a => (v -> Maybe t) -> a -> a Source #

appSubst :: (Ord v, SubstVars v t a) => Map v t -> a -> a Source #

Apply the given substitution.

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.

(&) :: Mapping m k => m v -> m v -> m v infixr 0 Source #

left-biased union of two mappings.

(|->) :: Mapping m k => k -> v -> m v infix 1 Source #

This operator constructs a singleton mapping.

empty :: Mapping m k => m v Source #

This is the empty mapping.