Copyright	(c) 2010-2011 Patrick Bahr Tom Hvitved
License	BSD3
Maintainer	Patrick Bahr <[email protected]>
Stability	experimental
Portability	non-portable (GHC Extensions)
Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Comp.Term

Description

This module defines the central notion of terms and its generalisation to contexts.

Synopsis

data Cxt :: Type -> (Type -> Type) -> Type -> Type where
- Term :: f (Cxt h f a) -> Cxt h f a
- Hole :: a -> Cxt Hole f a
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 :: Type -> (Type -> Type) -> Type -> Type 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 Cxt and NoHole. The second parameter is the signature of the context. The third parameter is the type of the holes.

Constructors

Term :: f (Cxt h f a) -> Cxt h f a
Hole :: a -> Cxt Hole f a

Instances

Instances details

ArbitraryF f => Arbitrary (Term f) Source #	This lifts instances of `ArbitraryF` to instances of `Arbitrary` for the corresponding term type.
Instance details Defined in Data.Comp.Arbitrary Methods arbitrary :: Gen (Term f) # shrink :: Term f -> [Term f] #
Functor f => Applicative (Context f) Source #
Instance details Defined in Data.Comp.Term Methods pure :: a -> Context f a # (<>) :: Context f (a -> b) -> Context f a -> Context f b # liftA2 :: (a -> b -> c) -> Context f a -> Context f b -> Context f c # (>) :: Context f a -> Context f b -> Context f b # (<*) :: Context f a -> Context f b -> Context f a #
Functor f => Monad (Context f) Source #
Instance details Defined in Data.Comp.Term Methods (>>=) :: Context f a -> (a -> Context f b) -> Context f b # (>>) :: Context f a -> Context f b -> Context f b # return :: a -> Context f a #
ArbitraryF f => ArbitraryF (Context f) Source #	This lifts instances of `ArbitraryF` to instances of `ArbitraryF` for the corresponding context functor.
Instance details Defined in Data.Comp.Arbitrary Methods arbitraryF' :: Arbitrary v => [(Int, Gen (Context f v))] Source # arbitraryF :: Arbitrary v => Gen (Context f v) Source # shrinkF :: Arbitrary v => Context f v -> [Context f v] Source #
(ArbitraryF f, Arbitrary a) => Arbitrary (Context f a) Source #	This lifts instances of `ArbitraryF` to instances of `Arbitrary` for the corresponding context type.
Instance details Defined in Data.Comp.Arbitrary Methods arbitrary :: Gen (Context f a) # shrink :: Context f a -> [Context f a] #
Foldable f => Foldable (Cxt h f) Source #
Instance details Defined in Data.Comp.Term Methods fold :: Monoid m => Cxt h f m -> m # foldMap :: Monoid m => (a -> m) -> Cxt h f a -> 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 # toList :: Cxt h f a -> [a] # null :: Cxt h f a -> Bool # length :: Cxt h f a -> Int # 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 # sum :: Num a => Cxt h f a -> a # product :: Num a => Cxt h f a -> a #
Traversable f => Traversable (Cxt h f) Source #
Instance details Defined in Data.Comp.Term Methods traverse :: Applicative f0 => (a -> f0 b) -> Cxt h f a -> f0 (Cxt h f b) # sequenceA :: Applicative f0 => Cxt h f (f0 a) -> f0 (Cxt h f a) # mapM :: Monad m => (a -> m b) -> Cxt h f a -> m (Cxt h f b) # sequence :: Monad m => Cxt h f (m a) -> m (Cxt h f a) #
Functor f => Functor (Cxt h f) Source #
Instance details Defined in Data.Comp.Term Methods fmap :: (a -> b) -> Cxt h f a -> Cxt h f b # (<$) :: a -> Cxt h f b -> Cxt h f a #
EqF f => EqF (Cxt h f) Source #
Instance details Defined in Data.Comp.Equality Methods eqF :: Eq a => Cxt h f a -> Cxt h f a -> Bool Source #
OrdF f => OrdF (Cxt h f) Source #
Instance details Defined in Data.Comp.Ordering Methods compareF :: Ord a => Cxt h f a -> Cxt h f a -> Ordering Source #
(Functor f, ShowF f) => ShowF (Cxt h f) Source #
Instance details Defined in Data.Comp.Show Methods showF :: Cxt h f String -> String Source #
(Functor f, ShowF f, Show a) => Show (Cxt h f a) Source #
Instance details Defined in Data.Comp.Show Methods showsPrec :: Int -> Cxt h f a -> ShowS # show :: Cxt h f a -> String # showList :: [Cxt h f a] -> ShowS #
(NFDataF f, NFData a) => NFData (Cxt h f a) Source #
Instance details Defined in Data.Comp.DeepSeq Methods rnf :: Cxt h f a -> () #
(EqF f, Eq a) => Eq (Cxt h f a) Source #	From an `EqF` functor an `Eq` instance of the corresponding term type can be derived.
Instance details Defined in Data.Comp.Equality Methods (==) :: Cxt h f a -> Cxt h f a -> Bool # (/=) :: Cxt h f a -> Cxt h f a -> Bool #
(OrdF f, Ord a) => Ord (Cxt h f a) Source #	From an `OrdF` functor an `Ord` instance of the corresponding term type can be derived.
Instance details Defined in Data.Comp.Ordering Methods compare :: Cxt h f a -> Cxt h f a -> Ordering # (<) :: Cxt h f a -> Cxt h f a -> Bool # (<=) :: Cxt h f a -> Cxt h f a -> Bool # (>) :: Cxt h f a -> Cxt h f a -> Bool # (>=) :: Cxt h f a -> Cxt h f a -> Bool # max :: Cxt h f a -> Cxt h f a -> Cxt h f a # min :: Cxt h f a -> Cxt h f a -> Cxt h f a #

data Hole Source #

Phantom type that signals that a Cxt might contain holes.

Instances

Instances details

Functor f => Applicative (Context f) Source #
Instance details Defined in Data.Comp.Term Methods pure :: a -> Context f a # (<>) :: Context f (a -> b) -> Context f a -> Context f b # liftA2 :: (a -> b -> c) -> Context f a -> Context f b -> Context f c # (>) :: Context f a -> Context f b -> Context f b # (<*) :: Context f a -> Context f b -> Context f a #
Functor f => Monad (Context f) Source #
Instance details Defined in Data.Comp.Term Methods (>>=) :: Context f a -> (a -> Context f b) -> Context f b # (>>) :: Context f a -> Context f b -> Context f b # return :: a -> Context f a #
ArbitraryF f => ArbitraryF (Context f) Source #	This lifts instances of `ArbitraryF` to instances of `ArbitraryF` for the corresponding context functor.
Instance details Defined in Data.Comp.Arbitrary Methods arbitraryF' :: Arbitrary v => [(Int, Gen (Context f v))] Source # arbitraryF :: Arbitrary v => Gen (Context f v) Source # shrinkF :: Arbitrary v => Context f v -> [Context f v] Source #
(ArbitraryF f, Arbitrary a) => Arbitrary (Context f a) Source #	This lifts instances of `ArbitraryF` to instances of `Arbitrary` for the corresponding context type.
Instance details Defined in Data.Comp.Arbitrary Methods arbitrary :: Gen (Context f a) # shrink :: Context f a -> [Context f a] #

data NoHole Source #

Phantom type that signals that a Cxt does not contain holes.

Instances

Instances details

ArbitraryF f => Arbitrary (Term f) Source #	This lifts instances of `ArbitraryF` to instances of `Arbitrary` for the corresponding term type.
Instance details Defined in Data.Comp.Arbitrary Methods arbitrary :: Gen (Term f) # shrink :: Term f -> [Term f] #

type Context = Cxt Hole Source #

type Term f = Cxt NoHole f () Source #

A term is a context with no holes.

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

Polymorphic definition of a term. This formulation is more natural than Cxt, it leads to impredicative types in some cases, though.

type Const f = f () Source #

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

This function unravels the given term at the topmost layer.

simpCxt :: Functor f => f a -> Context f a Source #

Convert a functorial value into a context.

toCxt :: Functor f => Term f -> Cxt h f a Source #

Cast a term over a signature to a context over the same signature.

constTerm :: Functor 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.