Data.Comp.Multi.Variables

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.

Documentation

class HasVars f v where

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

bindsVars :: f a :=> [v]

Instances

HasVars f v => HasVars (Cxt h f) v

(HasVars f v0, HasVars g v0) => HasVars (:+: f g) v0

type GSubst v a = NatM Maybe (K v) a

type CxtSubst h a f v = GSubst v (Cxt h f a)

type Subst f v = CxtSubst NoHole Nothing f v

varsToHoles :: forall f v. (HFunctor f, HasVars f v, Eq v) => Term f :-> Context f (K v)

containsVar :: (Eq v, HasVars f v, HFoldable f, HFunctor f) => v -> Cxt h f a :=> Bool

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

variables :: (Ord v, HasVars f v, HFoldable f, HFunctor f) => Cxt h f a :=> Set v

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

variableList :: (HasVars f v, HFoldable f, HFunctor f, Eq v) => Cxt h f a :=> [v]

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

variables' :: (Ord v, HasVars f v, HFoldable f, HFunctor f) => Const f :=> Set v

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

substVars :: SubstVars v t a => GSubst v t -> a :-> a

appSubst :: SubstVars v t a => GSubst v t -> a :-> a

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

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