{-# 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, 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)