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.