Data.Comp.Multi.Term

This module defines the central notion of mutual recursive (or, higher-order) terms and its generalisation to (higher-order) contexts. All definitions are generalised versions of those in Data.Comp.Term.

Documentation

data HCxt h f a i where

This data type represents contexts over a signature. Contexts are terms containing zero or more holes. The first type parameter is supposed to be one of the phantom types HHole and HNoHole. The second parameter is the signature of the context. The third parameter is the type family of the holes. The last parameter is the index/label.

Constructors

HTerm :: f (HCxt h f a) i -> HCxt h f a i

HHole :: a i -> HCxt HHole f a i

Instances

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

HFunctor f => HFunctor (HCxt h f)

HEqF f => HEqF (HCxt h f)

From an EqF functor an Eq instance of the corresponding term type can be derived.

(HShowF f, HFunctor f) => HShowF (HCxt h f)

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

(HEqF f, KEq a) => KEq (HCxt h f a)

(HShowF f, HFunctor f, KShow a) => KShow (HCxt h f a)

data HHole

Phantom type that signals that a HCxt might contain holes.

data HNoHole

Phantom type that signals that a HCxt does not contain holes.

type HContext = HCxt HHole

A context might contain holes.

data HNothing

Phantom type family used to define HTerm.

Instances

KEq HNothing

KShow HNothing

Eq (HNothing i)

Ord (HNothing i)

Show (HNothing i)

type HTerm f = HCxt HNoHole f HNothing

A (higher-order) term is a context with no holes.

type HConst f = f (K ())

constHTerm :: HFunctor f => HConst f :-> HTerm f

This function converts a constant to a term. This assumes that the argument is indeed a constant, i.e. does not have a value for the argument type of the functor f.

unHTerm :: HTerm f t -> f (HTerm f) t

This function unravels the given term at the topmost layer.

toHCxt :: HTerm f i -> HContext f a i

simpHCxt :: HFunctor f => f a i -> HContext f a i