{-# LANGUAGE DeriveDataTypeable #-}


-- | Data structures to describe theorems generated from types.

module Language.Haskell.FreeTheorems.Theorems where



import Data.Generics (Typeable, Data)

import Language.Haskell.FreeTheorems.BasicSyntax
import Language.Haskell.FreeTheorems.LanguageSubsets



-- | A theorem which is generated from a type signature.

type Theorem = Formula



-- | Logical formula constituting automatically generated theorems.

data Formula 
  = ForallRelations RelationVariable (TypeExpression, TypeExpression)
                    [Restriction] Formula
        -- ^ Quantifies a relation variable and two type expressions.
  
  | ForallFunctions (Either TermVariable TermVariable) 
                    (TypeExpression, TypeExpression) [Restriction] Formula
        -- ^ Quantifies a function variable and two type expressions.
  
  | ForallPairs (TermVariable, TermVariable) Relation Formula
        -- ^ Quantifies two term variables taken from a relation.
  
  | ForallVariables TermVariable TypeExpression Formula
        -- ^ Quantifies a term variable of a certain type.
  
  | Equivalence Formula Formula
        -- ^ Two formulas are equivalent.
  
  | Implication Formula Formula
        -- ^ The first formula implies the second formula.
  
  | Conjunction Formula Formula
        -- ^ The first formula and the second formula.
  
  | Predicate Predicate
        -- ^ A basic formula.
  
  deriving (Typeable, Typeable Formula
Formula -> DataType
Formula -> Constr
(forall b. Data b => b -> b) -> Formula -> Formula
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Formula -> u
forall u. (forall d. Data d => d -> u) -> Formula -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Formula -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Formula -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Formula -> m Formula
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Formula -> m Formula
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Formula
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Formula -> c Formula
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Formula)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Formula)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Formula -> m Formula
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Formula -> m Formula
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Formula -> m Formula
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Formula -> m Formula
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Formula -> m Formula
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Formula -> m Formula
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Formula -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Formula -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Formula -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Formula -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Formula -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Formula -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Formula -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Formula -> r
gmapT :: (forall b. Data b => b -> b) -> Formula -> Formula
$cgmapT :: (forall b. Data b => b -> b) -> Formula -> Formula
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Formula)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Formula)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Formula)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Formula)
dataTypeOf :: Formula -> DataType
$cdataTypeOf :: Formula -> DataType
toConstr :: Formula -> Constr
$ctoConstr :: Formula -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Formula
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Formula
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Formula -> c Formula
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Formula -> c Formula
Data)



-- | Restrictions on functions and relations.

data Restriction
  = Strict
  | Continuous
  | Total
  | BottomReflecting
  | LeftClosed
  | RespectsClasses [TypeClass]
  deriving (Typeable, Typeable Restriction
Restriction -> DataType
Restriction -> Constr
(forall b. Data b => b -> b) -> Restriction -> Restriction
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Restriction -> u
forall u. (forall d. Data d => d -> u) -> Restriction -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Restriction -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Restriction -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Restriction -> m Restriction
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Restriction -> m Restriction
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Restriction
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Restriction -> c Restriction
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Restriction)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Restriction)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Restriction -> m Restriction
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Restriction -> m Restriction
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Restriction -> m Restriction
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Restriction -> m Restriction
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Restriction -> m Restriction
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Restriction -> m Restriction
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Restriction -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Restriction -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Restriction -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Restriction -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Restriction -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Restriction -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Restriction -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Restriction -> r
gmapT :: (forall b. Data b => b -> b) -> Restriction -> Restriction
$cgmapT :: (forall b. Data b => b -> b) -> Restriction -> Restriction
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Restriction)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Restriction)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Restriction)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Restriction)
dataTypeOf :: Restriction -> DataType
$cdataTypeOf :: Restriction -> DataType
toConstr :: Restriction -> Constr
$ctoConstr :: Restriction -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Restriction
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Restriction
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Restriction -> c Restriction
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Restriction -> c Restriction
Data, Restriction -> Restriction -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Restriction -> Restriction -> Bool
$c/= :: Restriction -> Restriction -> Bool
== :: Restriction -> Restriction -> Bool
$c== :: Restriction -> Restriction -> Bool
Eq)



-- | Predicates occurring in formulas.

data Predicate
  = IsMember Term Term Relation
        -- ^ The pair of two terms is contained in a relation.
  
  | IsEqual Term Term
        -- ^ Two terms are equal.
  
  | IsLessEq Term Term
        -- ^ The first term is less defined than the second one, based on the
        --   semantical approximation order.
  
  | IsNotBot Term
        -- ^ The term is not equal to @_|_@.

  | IsTrue
        -- ^ Constant True Predicate
  
  deriving (Typeable, Typeable Predicate
Predicate -> DataType
Predicate -> Constr
(forall b. Data b => b -> b) -> Predicate -> Predicate
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Predicate -> u
forall u. (forall d. Data d => d -> u) -> Predicate -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Predicate -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Predicate -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Predicate -> m Predicate
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Predicate -> m Predicate
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Predicate
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Predicate -> c Predicate
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Predicate)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Predicate)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Predicate -> m Predicate
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Predicate -> m Predicate
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Predicate -> m Predicate
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Predicate -> m Predicate
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Predicate -> m Predicate
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Predicate -> m Predicate
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Predicate -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Predicate -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Predicate -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Predicate -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Predicate -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Predicate -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Predicate -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Predicate -> r
gmapT :: (forall b. Data b => b -> b) -> Predicate -> Predicate
$cgmapT :: (forall b. Data b => b -> b) -> Predicate -> Predicate
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Predicate)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Predicate)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Predicate)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Predicate)
dataTypeOf :: Predicate -> DataType
$cdataTypeOf :: Predicate -> DataType
toConstr :: Predicate -> Constr
$ctoConstr :: Predicate -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Predicate
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Predicate
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Predicate -> c Predicate
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Predicate -> c Predicate
Data)



-- | Terms consisting of variables, applications and instantiations.

data Term
  = TermVar TermVariable            -- ^ A term variable.
  | TermIns Term TypeExpression     -- ^ Instantiation of a term.
  | TermApp Term Term               -- ^ Application of a term to a term.
  | TermComp [Term]                 -- ^ Composition of function terms
  deriving (Typeable, Typeable Term
Term -> DataType
Term -> Constr
(forall b. Data b => b -> b) -> Term -> Term
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Term -> u
forall u. (forall d. Data d => d -> u) -> Term -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Term -> m Term
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term -> m Term
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Term
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Term -> c Term
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Term)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term -> m Term
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term -> m Term
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term -> m Term
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term -> m Term
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Term -> m Term
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Term -> m Term
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Term -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Term -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Term -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Term -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
gmapT :: (forall b. Data b => b -> b) -> Term -> Term
$cgmapT :: (forall b. Data b => b -> b) -> Term -> Term
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Term)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Term)
dataTypeOf :: Term -> DataType
$cdataTypeOf :: Term -> DataType
toConstr :: Term -> Constr
$ctoConstr :: Term -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Term
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Term
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Term -> c Term
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Term -> c Term
Data, Term -> Term -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Term -> Term -> Bool
$c/= :: Term -> Term -> Bool
== :: Term -> Term -> Bool
$c== :: Term -> Term -> Bool
Eq)



-- | Variables occurring in terms.

newtype TermVariable = TVar String
  deriving (Typeable, Typeable TermVariable
TermVariable -> DataType
TermVariable -> Constr
(forall b. Data b => b -> b) -> TermVariable -> TermVariable
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> TermVariable -> u
forall u. (forall d. Data d => d -> u) -> TermVariable -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TermVariable -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TermVariable -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TermVariable -> m TermVariable
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TermVariable -> m TermVariable
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TermVariable
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TermVariable -> c TermVariable
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TermVariable)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TermVariable)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TermVariable -> m TermVariable
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TermVariable -> m TermVariable
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TermVariable -> m TermVariable
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TermVariable -> m TermVariable
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TermVariable -> m TermVariable
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TermVariable -> m TermVariable
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TermVariable -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TermVariable -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> TermVariable -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TermVariable -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TermVariable -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TermVariable -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TermVariable -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TermVariable -> r
gmapT :: (forall b. Data b => b -> b) -> TermVariable -> TermVariable
$cgmapT :: (forall b. Data b => b -> b) -> TermVariable -> TermVariable
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TermVariable)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TermVariable)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TermVariable)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TermVariable)
dataTypeOf :: TermVariable -> DataType
$cdataTypeOf :: TermVariable -> DataType
toConstr :: TermVariable -> Constr
$ctoConstr :: TermVariable -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TermVariable
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TermVariable
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TermVariable -> c TermVariable
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TermVariable -> c TermVariable
Data, TermVariable -> TermVariable -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TermVariable -> TermVariable -> Bool
$c/= :: TermVariable -> TermVariable -> Bool
== :: TermVariable -> TermVariable -> Bool
$c== :: TermVariable -> TermVariable -> Bool
Eq)



-- | Relations are the foundations of free theorems.

data Relation
  = RelVar RelationInfo RelationVariable 
        -- ^ A relation variable.
 
  | FunVar RelationInfo (Either Term Term)
        -- ^ A function variable.
        --   It might be either a function to be applied on the left side (in
        --   equational and inequational cases) or on the right side (in 
        --   inequational cases only).
        --   In inequational cases, the term is additionally composed with the
        --   semantic approximation partial order.
 
  | RelBasic RelationInfo
        -- ^ A basic relation corresponding to a nullary type constructor.
        --   Depending on the theorem type, this can be either an equivalence
        --   relation or the semantic approximation partial order.
  
  | RelLift RelationInfo TypeConstructor [Relation]
        -- ^ A lifted relation for any nonnullary type constructor.
        --   The semantics of lifted relations is differs with the language
        --   subset:
        --   In inequational subsets lifted relations explicitly require
        --   left-closedness by composition with the semantic approximation 
        --   partial order.
        --   In equational subsets with fix or seq, this relation requires
        --   strictness explicitly by relating the undefined value with itself.
  
  | RelFun RelationInfo Relation Relation
        -- ^ A relation corresponding to a function type constructor.
        --   The semantics of this relation differs with the language subset:
        --   In the equational subset with seq, this relation is explicitly
        --   requiring bottom-reflectiveness of its members.
        --   In the inequational subset with seq, this relation is explicitly
        --   requiring totality of its members.

  | RelFunLab RelationInfo Relation Relation
        -- ^ A relation corresponding to a function type constructor.
        --   The semantics of this relation differs with the language subset:
        --   Apart from the equational subset with seq, it is equal to RelFun.
        --   In the equational subset with Seq, this relation is _not_ 
        --   explicitly requiring bottom-reflectiveness of its members.
  
  | RelAbs RelationInfo RelationVariable (TypeExpression, TypeExpression)
           [Restriction] Relation
        -- ^ A relation corresponding to a type abstraction.

  | FunAbs RelationInfo (Either TermVariable TermVariable)
           (TypeExpression, TypeExpression) [Restriction] Relation
        -- ^ A quantified function.

  deriving (Typeable, Typeable Relation
Relation -> DataType
Relation -> Constr
(forall b. Data b => b -> b) -> Relation -> Relation
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Relation -> u
forall u. (forall d. Data d => d -> u) -> Relation -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Relation -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Relation -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Relation -> m Relation
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Relation -> m Relation
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Relation
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Relation -> c Relation
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Relation)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Relation)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Relation -> m Relation
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Relation -> m Relation
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Relation -> m Relation
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Relation -> m Relation
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Relation -> m Relation
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Relation -> m Relation
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Relation -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Relation -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Relation -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Relation -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Relation -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Relation -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Relation -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Relation -> r
gmapT :: (forall b. Data b => b -> b) -> Relation -> Relation
$cgmapT :: (forall b. Data b => b -> b) -> Relation -> Relation
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Relation)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Relation)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Relation)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Relation)
dataTypeOf :: Relation -> DataType
$cdataTypeOf :: Relation -> DataType
toConstr :: Relation -> Constr
$ctoConstr :: Relation -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Relation
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Relation
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Relation -> c Relation
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Relation -> c Relation
Data, Relation -> Relation -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Relation -> Relation -> Bool
$c/= :: Relation -> Relation -> Bool
== :: Relation -> Relation -> Bool
$c== :: Relation -> Relation -> Bool
Eq)



-- | Extracts the relation information from a relation.

relationInfo :: Relation -> RelationInfo
relationInfo :: Relation -> RelationInfo
relationInfo Relation
rel = case Relation
rel of
  RelVar RelationInfo
ri RelationVariable
_       -> RelationInfo
ri
  FunVar RelationInfo
ri Either Term Term
_       -> RelationInfo
ri
  RelBasic RelationInfo
ri       -> RelationInfo
ri
  RelLift RelationInfo
ri TypeConstructor
_ [Relation]
_    -> RelationInfo
ri
  RelFun RelationInfo
ri Relation
_ Relation
_     -> RelationInfo
ri
  RelFunLab RelationInfo
ri Relation
_ Relation
_  -> RelationInfo
ri
  RelAbs RelationInfo
ri RelationVariable
_ (TypeExpression, TypeExpression)
_ [Restriction]
_ Relation
_ -> RelationInfo
ri
  FunAbs RelationInfo
ri Either TermVariable TermVariable
_ (TypeExpression, TypeExpression)
_ [Restriction]
_ Relation
_ -> RelationInfo
ri



-- | The relation information stored with every relation.

data RelationInfo = RelationInfo
  { RelationInfo -> LanguageSubset
relationLanguageSubset :: LanguageSubset
        -- ^ The language subset in which a relation was generated.
  
  , RelationInfo -> TypeExpression
relationLeftType       :: TypeExpression
        -- ^ The type of the first components of pairs contained in a relation.
  
  , RelationInfo -> TypeExpression
relationRightType      :: TypeExpression
        -- ^ The type of the second components of pairs contained in a 
        --   relation.
  
  }
  deriving (Typeable, Typeable RelationInfo
RelationInfo -> DataType
RelationInfo -> Constr
(forall b. Data b => b -> b) -> RelationInfo -> RelationInfo
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> RelationInfo -> u
forall u. (forall d. Data d => d -> u) -> RelationInfo -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RelationInfo -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RelationInfo -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RelationInfo -> m RelationInfo
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RelationInfo -> m RelationInfo
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RelationInfo
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RelationInfo -> c RelationInfo
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RelationInfo)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c RelationInfo)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RelationInfo -> m RelationInfo
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RelationInfo -> m RelationInfo
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RelationInfo -> m RelationInfo
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RelationInfo -> m RelationInfo
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RelationInfo -> m RelationInfo
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RelationInfo -> m RelationInfo
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> RelationInfo -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> RelationInfo -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> RelationInfo -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> RelationInfo -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RelationInfo -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RelationInfo -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RelationInfo -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RelationInfo -> r
gmapT :: (forall b. Data b => b -> b) -> RelationInfo -> RelationInfo
$cgmapT :: (forall b. Data b => b -> b) -> RelationInfo -> RelationInfo
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c RelationInfo)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c RelationInfo)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RelationInfo)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RelationInfo)
dataTypeOf :: RelationInfo -> DataType
$cdataTypeOf :: RelationInfo -> DataType
toConstr :: RelationInfo -> Constr
$ctoConstr :: RelationInfo -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RelationInfo
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RelationInfo
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RelationInfo -> c RelationInfo
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RelationInfo -> c RelationInfo
Data, RelationInfo -> RelationInfo -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RelationInfo -> RelationInfo -> Bool
$c/= :: RelationInfo -> RelationInfo -> Bool
== :: RelationInfo -> RelationInfo -> Bool
$c== :: RelationInfo -> RelationInfo -> Bool
Eq)



-- | A relation variable.

newtype RelationVariable = RVar String
  deriving (Typeable, Typeable RelationVariable
RelationVariable -> DataType
RelationVariable -> Constr
(forall b. Data b => b -> b)
-> RelationVariable -> RelationVariable
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> RelationVariable -> u
forall u. (forall d. Data d => d -> u) -> RelationVariable -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RelationVariable -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RelationVariable -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> RelationVariable -> m RelationVariable
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> RelationVariable -> m RelationVariable
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RelationVariable
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RelationVariable -> c RelationVariable
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RelationVariable)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c RelationVariable)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> RelationVariable -> m RelationVariable
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> RelationVariable -> m RelationVariable
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> RelationVariable -> m RelationVariable
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> RelationVariable -> m RelationVariable
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> RelationVariable -> m RelationVariable
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> RelationVariable -> m RelationVariable
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> RelationVariable -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> RelationVariable -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> RelationVariable -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> RelationVariable -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RelationVariable -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RelationVariable -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RelationVariable -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RelationVariable -> r
gmapT :: (forall b. Data b => b -> b)
-> RelationVariable -> RelationVariable
$cgmapT :: (forall b. Data b => b -> b)
-> RelationVariable -> RelationVariable
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c RelationVariable)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c RelationVariable)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RelationVariable)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RelationVariable)
dataTypeOf :: RelationVariable -> DataType
$cdataTypeOf :: RelationVariable -> DataType
toConstr :: RelationVariable -> Constr
$ctoConstr :: RelationVariable -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RelationVariable
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RelationVariable
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RelationVariable -> c RelationVariable
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RelationVariable -> c RelationVariable
Data, RelationVariable -> RelationVariable -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RelationVariable -> RelationVariable -> Bool
$c/= :: RelationVariable -> RelationVariable -> Bool
== :: RelationVariable -> RelationVariable -> Bool
$c== :: RelationVariable -> RelationVariable -> Bool
Eq)



-- | Describes unfolded lift relations.

data UnfoldedLift = UnfoldedLift Relation [UnfoldedDataCon]
  deriving (Typeable, Typeable UnfoldedLift
UnfoldedLift -> DataType
UnfoldedLift -> Constr
(forall b. Data b => b -> b) -> UnfoldedLift -> UnfoldedLift
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> UnfoldedLift -> u
forall u. (forall d. Data d => d -> u) -> UnfoldedLift -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UnfoldedLift -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UnfoldedLift -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UnfoldedLift -> m UnfoldedLift
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UnfoldedLift -> m UnfoldedLift
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UnfoldedLift
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UnfoldedLift -> c UnfoldedLift
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UnfoldedLift)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UnfoldedLift)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UnfoldedLift -> m UnfoldedLift
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UnfoldedLift -> m UnfoldedLift
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UnfoldedLift -> m UnfoldedLift
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UnfoldedLift -> m UnfoldedLift
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UnfoldedLift -> m UnfoldedLift
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UnfoldedLift -> m UnfoldedLift
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> UnfoldedLift -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> UnfoldedLift -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> UnfoldedLift -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> UnfoldedLift -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UnfoldedLift -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UnfoldedLift -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UnfoldedLift -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UnfoldedLift -> r
gmapT :: (forall b. Data b => b -> b) -> UnfoldedLift -> UnfoldedLift
$cgmapT :: (forall b. Data b => b -> b) -> UnfoldedLift -> UnfoldedLift
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UnfoldedLift)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UnfoldedLift)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UnfoldedLift)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UnfoldedLift)
dataTypeOf :: UnfoldedLift -> DataType
$cdataTypeOf :: UnfoldedLift -> DataType
toConstr :: UnfoldedLift -> Constr
$ctoConstr :: UnfoldedLift -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UnfoldedLift
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UnfoldedLift
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UnfoldedLift -> c UnfoldedLift
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UnfoldedLift -> c UnfoldedLift
Data)



-- | A relational descriptions of a data constructor.

data UnfoldedDataCon
  = BotPair
  | ConPair DataConstructor
  | ConMore DataConstructor [TermVariable] [TermVariable] Formula
  deriving (Typeable, Typeable UnfoldedDataCon
UnfoldedDataCon -> DataType
UnfoldedDataCon -> Constr
(forall b. Data b => b -> b) -> UnfoldedDataCon -> UnfoldedDataCon
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> UnfoldedDataCon -> u
forall u. (forall d. Data d => d -> u) -> UnfoldedDataCon -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UnfoldedDataCon -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UnfoldedDataCon -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> UnfoldedDataCon -> m UnfoldedDataCon
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UnfoldedDataCon -> m UnfoldedDataCon
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UnfoldedDataCon
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UnfoldedDataCon -> c UnfoldedDataCon
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UnfoldedDataCon)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UnfoldedDataCon)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UnfoldedDataCon -> m UnfoldedDataCon
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UnfoldedDataCon -> m UnfoldedDataCon
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UnfoldedDataCon -> m UnfoldedDataCon
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UnfoldedDataCon -> m UnfoldedDataCon
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> UnfoldedDataCon -> m UnfoldedDataCon
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> UnfoldedDataCon -> m UnfoldedDataCon
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> UnfoldedDataCon -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> UnfoldedDataCon -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> UnfoldedDataCon -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> UnfoldedDataCon -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UnfoldedDataCon -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UnfoldedDataCon -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UnfoldedDataCon -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UnfoldedDataCon -> r
gmapT :: (forall b. Data b => b -> b) -> UnfoldedDataCon -> UnfoldedDataCon
$cgmapT :: (forall b. Data b => b -> b) -> UnfoldedDataCon -> UnfoldedDataCon
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UnfoldedDataCon)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UnfoldedDataCon)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UnfoldedDataCon)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UnfoldedDataCon)
dataTypeOf :: UnfoldedDataCon -> DataType
$cdataTypeOf :: UnfoldedDataCon -> DataType
toConstr :: UnfoldedDataCon -> Constr
$ctoConstr :: UnfoldedDataCon -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UnfoldedDataCon
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UnfoldedDataCon
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UnfoldedDataCon -> c UnfoldedDataCon
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UnfoldedDataCon -> c UnfoldedDataCon
Data)



-- | Data constructors.

data DataConstructor
  = DConEmptyList   -- ^ The nullary data constructor @[]@.
  | DConConsList    -- ^ The binary data constructor @:@.
  | DConTuple Int   -- ^ The n-ary tuple data constructor.
  | DCon String     -- ^ Any other data constructor.
  deriving (Typeable, Typeable DataConstructor
DataConstructor -> DataType
DataConstructor -> Constr
(forall b. Data b => b -> b) -> DataConstructor -> DataConstructor
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> DataConstructor -> u
forall u. (forall d. Data d => d -> u) -> DataConstructor -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataConstructor -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataConstructor -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> DataConstructor -> m DataConstructor
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DataConstructor -> m DataConstructor
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataConstructor
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataConstructor -> c DataConstructor
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataConstructor)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DataConstructor)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DataConstructor -> m DataConstructor
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DataConstructor -> m DataConstructor
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DataConstructor -> m DataConstructor
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DataConstructor -> m DataConstructor
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> DataConstructor -> m DataConstructor
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> DataConstructor -> m DataConstructor
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> DataConstructor -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> DataConstructor -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> DataConstructor -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> DataConstructor -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataConstructor -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataConstructor -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataConstructor -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataConstructor -> r
gmapT :: (forall b. Data b => b -> b) -> DataConstructor -> DataConstructor
$cgmapT :: (forall b. Data b => b -> b) -> DataConstructor -> DataConstructor
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DataConstructor)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DataConstructor)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataConstructor)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataConstructor)
dataTypeOf :: DataConstructor -> DataType
$cdataTypeOf :: DataConstructor -> DataType
toConstr :: DataConstructor -> Constr
$ctoConstr :: DataConstructor -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataConstructor
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataConstructor
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataConstructor -> c DataConstructor
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataConstructor -> c DataConstructor
Data)



-- | A relational description of a class declaration.

data UnfoldedClass 
  = UnfoldedClass [TypeClass] TypeClass (Either RelationVariable TermVariable)
                  [Formula]
  deriving (Typeable, Typeable UnfoldedClass
UnfoldedClass -> DataType
UnfoldedClass -> Constr
(forall b. Data b => b -> b) -> UnfoldedClass -> UnfoldedClass
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> UnfoldedClass -> u
forall u. (forall d. Data d => d -> u) -> UnfoldedClass -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UnfoldedClass -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UnfoldedClass -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UnfoldedClass -> m UnfoldedClass
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UnfoldedClass -> m UnfoldedClass
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UnfoldedClass
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UnfoldedClass -> c UnfoldedClass
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UnfoldedClass)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UnfoldedClass)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UnfoldedClass -> m UnfoldedClass
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UnfoldedClass -> m UnfoldedClass
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UnfoldedClass -> m UnfoldedClass
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UnfoldedClass -> m UnfoldedClass
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UnfoldedClass -> m UnfoldedClass
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UnfoldedClass -> m UnfoldedClass
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> UnfoldedClass -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> UnfoldedClass -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> UnfoldedClass -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> UnfoldedClass -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UnfoldedClass -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UnfoldedClass -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UnfoldedClass -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UnfoldedClass -> r
gmapT :: (forall b. Data b => b -> b) -> UnfoldedClass -> UnfoldedClass
$cgmapT :: (forall b. Data b => b -> b) -> UnfoldedClass -> UnfoldedClass
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UnfoldedClass)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UnfoldedClass)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UnfoldedClass)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UnfoldedClass)
dataTypeOf :: UnfoldedClass -> DataType
$cdataTypeOf :: UnfoldedClass -> DataType
toConstr :: UnfoldedClass -> Constr
$ctoConstr :: UnfoldedClass -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UnfoldedClass
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UnfoldedClass
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UnfoldedClass -> c UnfoldedClass
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UnfoldedClass -> c UnfoldedClass
Data)