Data.Comp.Multi.Variables

This module defines an abstraction notion of a variable in a term. All definitions are generalised versions of those in Data.Comp.Variables.

Documentation

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

type HCxtSubst h a f v = GSubst v (HCxt h f a)

type Subst f v = HCxtSubst HNoHole HNothing f v

class HasVars f v where

This multiparameter class defines functors with variables. An instance HasVar f v denotes that values over f might contain variables of type v.

Methods

isVar :: f a :=> Maybe v

Instances

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

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

varsToHHoles :: forall f v. (HFunctor f, HasVars f v) => HTerm f :-> HContext f (K v)

containsVarAlg :: (Eq v, HasVars f v, HFoldable f) => v -> HAlg f (K Bool)

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

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

variableListAlg :: (HasVars f v, HFoldable f) => HAlg f (K [v])

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

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

variablesAlg :: (Ord v, HasVars f v, HFoldable f) => HAlg f (K (Set v))

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

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

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

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

substAlg :: HasVars f v => HCxtSubst h a f v -> HAlg f (HCxt h f a)

class SubstVars v t a where

This function substitutes variables in a context according to a partial mapping from variables to contexts.

Methods

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

Instances

(SubstVars v t a, HFunctor f) => SubstVars v t (f a)

(Ord v, HasVars f v, HFunctor f) => SubstVars v (HCxt h f a) (HCxt h f a)

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

compSubst :: (Ord v, HasVars f v, HFunctor f) => HCxtSubst h a f v -> HCxtSubst h a f v -> HCxtSubst 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.