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.

## Synopsis

- 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.

## Instances

Functor f => Monad (Context f) Source # | |

Functor f => Applicative (Context f) Source # | |

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

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

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

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

Defined in Data.Comp.Term fold :: Monoid m => Cxt h f m -> m # foldMap :: Monoid m => (a -> m) -> Cxt h f a -> m # foldr :: (a -> b -> b) -> b -> Cxt h f a -> b # foldr' :: (a -> b -> b) -> b -> Cxt h f a -> b # foldl :: (b -> a -> b) -> b -> Cxt h f a -> b # foldl' :: (b -> a -> b) -> b -> Cxt h f a -> b # foldr1 :: (a -> a -> a) -> Cxt h f a -> a # foldl1 :: (a -> a -> a) -> Cxt h f a -> a # elem :: Eq a => a -> Cxt h f a -> Bool # maximum :: Ord a => Cxt h f a -> a # minimum :: Ord a => Cxt h f a -> a # | |

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

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

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

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

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

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

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

Defined in Data.Comp.Ordering | |

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

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

Defined in Data.Comp.DeepSeq |

Phantom type that signals that a `Cxt`

might contain holes.

## Instances

Functor f => Monad (Context f) Source # | |

Functor f => Applicative (Context f) Source # | |

ArbitraryF f => ArbitraryF (Context f) Source # | 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.

## Instances

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.