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 Cxt h f a i where
- data Hole
- data NoHole
- type Context = Cxt Hole
- data Nothing
- type Term f = Cxt NoHole f Nothing
- type Const f = f (K ())
- constTerm :: HFunctor f => Const f :-> Term f
- unTerm :: Term f t -> f (Term f) t
- toCxt :: HFunctor f => Term f :-> Context f a
- simpCxt :: HFunctor f => f a i -> Context 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 Hole
and NoHole
. 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 (Cxt h f a) (Cxt h f a) | |
HFunctor f => HFunctor (Cxt h f) | |
HFoldable f => HFoldable (Cxt h f) | |
HTraversable f => HTraversable (Cxt h f) | |
HEqF f => HEqF (Cxt h f) | From an |
(HShowF f, HFunctor f) => HShowF (Cxt h f) | |
HasVars f v => HasVars (Cxt h f) v | |
(HEqF f, KEq a) => KEq (Cxt h f a) | |
(HShowF f, HFunctor f, KShow a) => KShow (Cxt h f a) |
Phantom type family used to define Term
.
constTerm :: HFunctor f => Const f :-> Term 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.