Portability | non-portable (GHC Extensions) |
---|---|
Stability | experimental |
Maintainer | Patrick Bahr <paba@diku.dk> |
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.
- data HCxt h f a i where
- data HHole
- data HNoHole
- type HContext = HCxt HHole
- data HNothing
- type HTerm f = HCxt HNoHole f HNothing
- type HConst f = f (K ())
- constHTerm :: HFunctor f => HConst f :-> HTerm f
- unHTerm :: HTerm f t -> f (HTerm f) t
- toHCxt :: HTerm f i -> HContext f a i
- simpHCxt :: HFunctor f => f a i -> HContext f a i
Documentation
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.
(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 |
(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) |
Phantom type family used to define HTerm
.
constHTerm :: HFunctor f => HConst f :-> HTerm fSource
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.