-- Copyright 2006, Sascha Boehme.




-- | This module defines a function to unfold relations generated from types to
--   theorems.

module FreeTheorems.Unfolding (
    unfold,
    unfoldFunction,
    unfoldForall,
    getTypesOf,

    -- testing interface
    -- testUnfolding
) where



import FreeTheorems.Simplification
import FreeTheorems.TheoremData
import FreeTheorems.Types
import Control.Monad (liftM)

import FreeTheorems.Delta
import FreeTheorems.Preparation
-- import FreeTheorems.Test.ArbitraryTypes
-- import Test.QuickCheck (quickCheck)





-- | Unfolds a relation to a theorem.
--   It replaces all functional relations and relation abstractions by logical
--   statements and conditions while the other relations are transformed in
--   is-element-of predicates using relations on their right-hand side.
--
--   The returned theorem is simplified using 'simplifyTheorem'.

unfold :: TermVariable
                -- ^ The name of the type from which the theorem is to be
                --   generated.
          -> Relation
                -- ^ Relation which was generated from the type.
          -> TheoremState Theorem
                -- ^ Returns the generated theorem in the corresponding theorem
                --   state.

unfold tv rel =
  liftM simplifyTheorem (unfoldRelation rel (TermVar tv, TermVar tv))





-- | Unfolds the given relation to a theorem. This is a helper function for
--   'unfold'.
--
--   Basic relations are transformed into is-element-of predicates while
--   functional relations and relation abstractions are replaced by logical
--   expressions. See also 'unfoldFunction' and 'unfoldForall'.

unfoldRelation :: Relation -> (Term, Term) -> TheoremState Theorem
unfoldRelation rel (t1, t2) =
  case rel of
    RelTerm _ _             -> return $ IsElementOf (t1,t2) rel
    RelVar _                -> return $ IsElementOf (t1,t2) rel
    RelLift _ _ _           -> return $ IsElementOf (t1,t2) rel
    RelLiftList _ _         -> return $ IsElementOf (t1,t2) rel
    RelLiftTuple _ _        -> return $ IsElementOf (t1,t2) rel
    RelFun model rel1 rel2  -> unfoldFunction model rel1 rel2 (t1,t2)
    RelForall model rv rel1 -> unfoldForall model rv rel1 (t1,t2)



-- | Unfolds a functional relation to a logical expression.

unfoldFunction :: LanguageModel
                  -> Relation
                  -> Relation
                  -> (Term, Term)
                  -> TheoremState Theorem

unfoldFunction model rel1 rel2 (t1,t2) = do
  (x,y) <- newVariablesFor rel1
  let (tx,ty) = (TermVar x, TermVar y)
  theorem <- unfoldRelation rel2 (TermApp t1 tx, TermApp t2 ty)
  case rel1 of
    RelTerm t (t1,t2) -> return $ ForallElements x t1
                                $ ForallElements y t2
                                $ Implication (IsElementOf (tx,ty) rel1) theorem

    RelVar _          -> return $ ForallPairs (x,y) rel1 theorem
    RelLift _ _ _     -> return $ ForallPairs (x,y) rel1 theorem
    RelLiftList _ _   -> return $ ForallPairs (x,y) rel1 theorem
    RelLiftTuple _ _  -> return $ ForallPairs (x,y) rel1 theorem

    RelFun _ rel3 rel4  -> do let (t1, t2) = getTypesOf rel3
                              let (t3, t4) = getTypesOf rel4
                              theorem1 <- unfoldFunction model rel3 rel4 (tx,ty)
                              return $ ForallElements x (TypeFun t1 t3)
                                     $ ForallElements y (TypeFun t2 t4)
                                     $ Implication theorem1 theorem

    RelForall _ rv rel3 -> do let (t1, t2) = getTypesOf rel1
                              theorem1 <- unfoldForall model rv rel3 (tx,ty)
                              return $ ForallElements x t1
                                     $ ForallElements y t2
                                     $ Implication theorem1 theorem



-- | Unfolds a relation abstraction to a logical expression.
--   Depending on the language model used, the expression may contain certain
--   restriction annotations.

unfoldForall :: LanguageModel
                -> RelationVariable
                -> Relation
                -> (Term, Term)
                -> TheoremState Theorem

unfoldForall model rv rel (t1,t2) = do
  let R _ _ (ttv1, ttv2) = rv
  let pair = (TermIns t1 (TypeTermVar ttv1), TermIns t2 (TypeTermVar ttv2))

  let res = case model of
              BasicModel -> []
              FixModel   -> [IsStrictAndContinuous rv]

  liftM (ForallRelations rv res) (unfoldRelation rel pair)



--------------------------------------------------------------------------------



-- | Every relation is defined over a pair of closed types. This function
--   returns exactly that pair of types for an arbitrary relation. Thus, it acts
--   like an inverse delta function, although this is not fully true.

getTypesOf :: Relation -> (Type, Type)
getTypesOf rel = getTypes [] rel



-- | Computes the pair of types for a relation. This function is a helper
--   function for 'getTypesOf'.
--
--   The second argument contains a list of relation variables which should
--   be replaced by corresponding type variables (used to process abstractions).
--   Otherwise, relation variables are replaced by the according type term
--   variables.

getTypes :: [RelationVariable] -> Relation -> (Type, Type)
getTypes rvs rel =
  case rel of
    RelTerm _ typepair      -> typepair

    RelVar rv               -> let R _ v (ttv1, ttv2) = rv
                               in  if rv `elem` rvs
                                     then (TypeVar v, TypeVar v)
                                     else (TypeTermVar ttv1, TypeTermVar ttv2)

    RelLift model c rels    -> let (ts1, ts2) = unzip $ map (getTypes rvs) rels
                               in  (TypeCon c ts1, TypeCon c ts2)

    RelLiftList model rel'  -> let (t1, t2) = getTypes rvs rel'
                               in  (TypeList t1, TypeList t2)

    RelLiftTuple model rels -> let (ts1, ts2) = unzip $ map (getTypes rvs) rels
                               in  (TypeTuple ts1, TypeTuple ts2)

    RelFun model rel1 rel2  -> let (t1, t2) = getTypes rvs rel1
                                   (t3, t4) = getTypes rvs rel2
                               in  (TypeFun t1 t3, TypeFun t2 t4)

    RelForall model rv rel' -> let (t1, t2) = getTypes (rv:rvs) rel'
                                   R _ v _ = rv
                               in  (TypeForall v t1, TypeForall v t2)



--------------------------------------------------------------------------------



-- A list of tests for this module.

{-
testUnfolding = do
  putStr "unfold replaces functions and abstractions ... "
  quickCheck prop_unfold
  putStr "every variable is quantified ... "
  quickCheck prop_variables_are_quantified
-}



-- Check that after expansion, there are no function type relations and
-- type abstraction relations anymore.

prop_unfold model t =
  let tv = PV "t"
      theorem = fst $ execute tv (applyDelta model (prepare t) >>= unfold tv)
  in  hasNoFunAndForall theorem


hasNoFunAndForall theorem =
  case theorem of
    IsElementOf _ rel     -> isNotFunOrForall rel
    ForallPairs _ rel t   -> isNotFunOrForall rel && hasNoFunAndForall t
    ForallRelations _ _ t -> hasNoFunAndForall t
    ForallElements _ _ t  -> hasNoFunAndForall t
    Conjunction t1 t2     -> hasNoFunAndForall t1 && hasNoFunAndForall t2
    Implication t1 t2     -> hasNoFunAndForall t1 && hasNoFunAndForall t2

isNotFunOrForall rel =
  case rel of
    RelTerm _ _      -> True
    RelVar _         -> True
    RelLift _ _ _    -> True
    RelLiftList _ _  -> True
    RelLiftTuple _ _ -> True
    RelFun _ _ _     -> False
    RelForall _ _ _  -> False



-- Check that every variable is quantified after expansion.

prop_variables_are_quantified model t =
  let tv = PV "t"
      theorem = fst $ execute tv (applyDelta model (prepare t) >>= unfold tv)
  in  cqTheorem [PV "t", PV "id"] [] [] theorem


cqTheorem tvs ttvs rvs theorem =
  case theorem of
    IsElementOf (t1,t2) rel     -> cqTerm tvs ttvs t1 && cqTerm tvs ttvs t2
                                   && cqRelation tvs ttvs rvs rel

    ForallPairs (tv1,tv2) rel t -> cqRelation tvs ttvs rvs rel
                                   && cqTheorem (tv1:tv2:tvs) ttvs rvs t

    ForallRelations rv res t    -> let R _ _ (ttv1,ttv2) = rv
                                       ttvs' = ttv1:ttv2:ttvs
                                   in cqRestriction tvs (rv:rvs) res
                                      && cqTheorem tvs ttvs' (rv:rvs) t

    ForallElements tv ty t      -> cqType [] ttvs ty
                                   && cqTheorem (tv:tvs) ttvs rvs t

    Conjunction t1 t2           -> cqTheorem tvs ttvs rvs t1
                                   && cqTheorem tvs ttvs rvs t2

    Implication t1 t2           -> cqTheorem tvs ttvs rvs t1
                                   && cqTheorem tvs ttvs rvs t2


cqRestriction tvs rvs [] = True
cqRestriction tvs rvs (res:ress) = cqRestriction tvs rvs ress &&
  case res of
    IsStrict tv              -> tv `elem` tvs
    IsStrictAndContinuous rv -> rv `elem` rvs


cqTerm tvs ttvs t =
  case t of
    TermVar tv    -> tv `elem` tvs
    TermApp t1 t2 -> cqTerm tvs ttvs t1 && cqTerm tvs ttvs t2
    TermIns t' ty -> cqTerm tvs ttvs t' && cqType [] ttvs ty

cqRelation tvs ttvs rvs rel =
  case rel of
    RelTerm t (ty1, ty2) -> cqTerm tvs ttvs t
                            && cqType [] ttvs ty1 && cqType [] ttvs ty2
    RelVar rv            -> rv `elem` rvs
    RelLift _ _ rels     -> and $ map (cqRelation tvs ttvs rvs) rels
    RelLiftList _ rel'   -> cqRelation tvs ttvs rvs rel'
    RelLiftTuple _ rels  -> and $ map (cqRelation tvs ttvs rvs) rels
    RelFun _ rel1 rel2   -> cqRelation tvs ttvs rvs rel1
                            && cqRelation tvs ttvs rvs rel2
    RelForall _ rv rel'  -> cqRelation tvs ttvs (rv:rvs) rel'

cqType vs ttvs t =
  case t of
    TypeBasic _     -> True
    TypeVar v       -> v `elem` vs
    TypeTermVar ttv -> ttv `elem` ttvs
    TypeCon _ ts    -> and $ map (cqType vs ttvs) ts
    TypeList t'     -> cqType vs ttvs t'
    TypeUnit        -> True
    TypeTuple ts    -> and $ map (cqType vs ttvs) ts
    TypeFun t1 t2   -> cqType vs ttvs t1 && cqType vs ttvs t2
    TypeForall v t' -> cqType (v:vs) ttvs t'





zz = TypeForall "a" (TypeFun (TypeBasic Char) (TypeTuple [TypeBasic Float,TypeVar "b"
  ,TypeBasic Char,TypeCon "String" [],TypeCon "String" [],TypeVar "b",TypeBasic
  Double,TypeVar "c",TypeVar "b",TypeCon "String" [],TypeBasic Int]))

zzz = fst $ execute (PV "t") (applyDelta BasicModel (prepare zz) >>= unfold (PV "t"))