compdata-0.5.1: Compositional Data Types

Portabilitynon-portable (GHC Extensions)
Stabilityexperimental
MaintainerPatrick Bahr <paba@diku.dk> and Tom Hvitved <hvitved@diku.dk>

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 whereSource

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 vSource

Indicates whether the f constructor is a variable.

bindsVars :: f a -> [v]Source

Indicates the set of variables bound by the f constructor.

Instances

(HasVars f v0, HasVars g v0) => HasVars (:+: f g) v0 
HasVars f v => HasVars (Cxt h f) v 

type Subst f v = CxtSubst NoHole () f vSource

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 :: (Functor f, HasVars f v, Eq v) => Term f -> Context f vSource

Convert variables to holes, except those that are bound.

containsVar :: (Eq v, HasVars f v, Foldable f, Functor f) => v -> Cxt h f a -> BoolSource

This function checks whether a variable is contained in a context.

variables :: (Ord v, HasVars f v, Foldable f, Functor f) => Cxt h f a -> Set vSource

This function computes the set of variables occurring in a context.

variableList :: (Ord v, HasVars f v, Foldable f, Functor 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 vSource

This function computes the set of variables occurring in a constant.

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

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

Apply the given substitution.

compSubst :: (Ord v, HasVars f v, Functor f) => CxtSubst h a f v -> CxtSubst h a f v -> CxtSubst h a f vSource

This function composes two substitutions s1 and s2. That is, applying the resulting substitution is equivalent to first applying s2 and then s1.