Copyright | (c) 2010-2011 Patrick Bahr, Tom Hvitved |
---|---|

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 *terms* and its
generalisation to contexts.

- data Cxt :: * -> (* -> *) -> * -> * where
- data Hole
- data NoHole
- type Context = Cxt Hole
- type Term f = Cxt NoHole f ()
- type PTerm f = forall h a. Cxt h f a
- type Const f = f ()
- unTerm :: Cxt NoHole f a -> f (Cxt NoHole f a)
- simpCxt :: Functor f => f a -> Context f a
- toCxt :: Functor f => Term f -> Cxt h f a
- constTerm :: Functor f => Const f -> Term f

# Documentation

data Cxt :: * -> (* -> *) -> * -> * where Source

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 of the holes.

Functor f => Monad (Context f) | |

ArbitraryF f => Arbitrary (Term f) | This lifts instances of |

ArbitraryF f => ArbitraryF (Context f) | This lifts instances of |

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

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

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

(Functor f, ShowF f) => ShowF (Cxt h f) | |

(ArbitraryF f, Arbitrary a) => Arbitrary (Context f a) | This lifts instances of |

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

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

(EqF f, Eq a) => Eq (Cxt h f a) | From an |

(OrdF f, Ord a) => Ord (Cxt h f a) | From an |

(Functor f, ShowF f, Show a) => Show (Cxt h f a) | |

(NFDataF f, NFData a) => NFData (Cxt h f a) |

Phantom type that signals that a `Cxt`

might contain holes.

Functor f => Monad (Context f) | |

ArbitraryF f => ArbitraryF (Context f) | This lifts instances of |

(ArbitraryF f, Arbitrary a) => Arbitrary (Context f a) | This lifts instances of |

Phantom type that signals that a `Cxt`

does not contain holes.

ArbitraryF f => Arbitrary (Term f) | This lifts instances of |

type PTerm f = forall h a. Cxt h f a Source

Polymorphic definition of a term. This formulation is more
natural than `Term`

, it leads to impredicative types in some cases,
though.

unTerm :: Cxt NoHole f a -> f (Cxt NoHole f a) Source

This function unravels the given term at the topmost layer.