Copyright | (c) 2011 Patrick Bahr |
---|---|

License | BSD3 |

Maintainer | Patrick Bahr <paba@diku.dk> |

Stability | experimental |

Portability | non-portable (GHC Extensions) |

Safe Haskell | None |

Language | Haskell98 |

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

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.

HFunctor f => HFunctor (Cxt h f) | |

HFoldable f => HFoldable (Cxt h f) | |

HTraversable f => HTraversable (Cxt h f) | |

(ShowHF f, HFunctor f) => ShowHF (Cxt h f) | |

EqHF f => EqHF (Cxt h f) | |

(HFunctor f, OrdHF f) => OrdHF (Cxt h f) | From an |

(ShowHF f, HFunctor f, KShow a) => KShow (Cxt h f a) | |

(EqHF f, KEq a) => KEq (Cxt h f a) | |

(HFunctor f, OrdHF f, KOrd a) => KOrd (Cxt h f a) | |

(EqHF f, KEq a) => Eq (Cxt h f a i) | From an |

(HFunctor f, OrdHF f, KOrd a) => Ord (Cxt h f a i) | Ordering of terms. |

KShow (Cxt h f a) => Show (Cxt h f a i) |

constTerm :: HFunctor f => Const f :-> Term f Source

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.

unTerm :: Term f t -> f (Term f) t Source

This function unravels the given term at the topmost layer.