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.