```{-# LANGUAGE DeriveDataTypeable #-}

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

import Data.Generics (Typeable, Data)

-- | 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, Data)

-- | Restrictions on functions and relations.

data Restriction
= Strict
| Continuous
| Total
| BottomReflecting
| LeftClosed
| RespectsClasses [TypeClass]
deriving (Typeable, Data, 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, 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, Data, Eq)

-- | Variables occurring in terms.

newtype TermVariable = TVar String
deriving (Typeable, Data, 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, Data, Eq)

-- | Extracts the relation information from a relation.

relationInfo :: Relation -> RelationInfo
relationInfo rel = case rel of
RelVar ri _       -> ri
FunVar ri _       -> ri
RelBasic ri       -> ri
RelLift ri _ _    -> ri
RelFun ri _ _     -> ri
RelFunLab ri _ _  -> ri
RelAbs ri _ _ _ _ -> ri
FunAbs ri _ _ _ _ -> ri

-- | The relation information stored with every relation.

data RelationInfo = RelationInfo
{ relationLanguageSubset :: LanguageSubset
-- ^ The language subset in which a relation was generated.

, relationLeftType       :: TypeExpression
-- ^ The type of the first components of pairs contained in a relation.

, relationRightType      :: TypeExpression
-- ^ The type of the second components of pairs contained in a
--   relation.

}
deriving (Typeable, Data, Eq)

-- | A relation variable.

newtype RelationVariable = RVar String
deriving (Typeable, Data, Eq)

-- | Describes unfolded lift relations.

data UnfoldedLift = UnfoldedLift Relation [UnfoldedDataCon]
deriving (Typeable, Data)

-- | A relational descriptions of a data constructor.

data UnfoldedDataCon
= BotPair
| ConPair DataConstructor
| ConMore DataConstructor [TermVariable] [TermVariable] Formula
deriving (Typeable, 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, Data)

-- | A relational description of a class declaration.

data UnfoldedClass
= UnfoldedClass [TypeClass] TypeClass (Either RelationVariable TermVariable)
[Formula]
deriving (Typeable, Data)

```