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 :: (Type -> Type) -> Type -> Type) 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.

Minimal complete definition

Nothing

Methods

isVar :: f a :=> Maybe v

Indicates whether the f constructor is a variable. The default implementation returns Nothing.

bindsVars :: Mapping m a => f a :=> m (Set v)

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.

Instances

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

Defined in Data.Comp.Multi.Variables

Methods

isVar :: forall (a :: Type -> Type). (f :+: g) a :=> Maybe v

bindsVars :: forall (m :: TYPE LiftedRep -> TYPE LiftedRep) (a :: Type -> Type). Mapping m a => (f :+: g) a :=> m (Set v)

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 f v, Ord v) => Term f :-> Context f (K v)

containsVar :: (Ord v, HasVars f v, HTraversable 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, HTraversable f, HFunctor f) => Cxt h f a :=> Set v

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

variableList :: (HasVars f v, HTraversable f, HFunctor f, Ord 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.

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

compSubst :: (Ord v, HasVars f v, HTraversable 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.

getBoundVars :: forall f a v i. (HasVars f v, HTraversable f) => f a i -> f (a :*: K (Set v)) i

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

left-biased union of two mappings.

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

This operator constructs a singleton mapping.

empty :: Mapping m k => m v

This is the empty mapping.