{- | Module     : ./GMP/GMP-CoLoSS/GMP/Logics/Cond.hs
 -  Description : Implementation of logic instance CK+CEM
 -  Copyright   : (c) Daniel Hausmann & Georgel Calin & Lutz Schroeder, DFKI Lab Bremen,
 -                Rob Myers & Dirk Pattinson, Department of Computing, ICL
 -  License     : GPLv2 or higher, see LICENSE.txt
 -  Maintainer  : hausmann@dfki.de
 -  Stability   : provisional
 -  Portability : portable
 -
 - Provides the implementation of the matching functions of conditional logic plus
 - conditional excluded middle.
 -}
{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, FlexibleContexts #-}
module GMP.Logics.Cond where
import Data.List
import Data.Ratio
import Data.Maybe

import Debug.Trace
import Text.ParserCombinators.Parsec

import GMP.Logics.Generic
import GMP.Parser

{- ------------------------------------------------------------------------------
instance of feature for CK+CEM
------------------------------------------------------------------------------ -}

data Con a = Con [Formula a] deriving (Eq, Show)

instance (SigFeature b c d, Eq (b (c d)), Eq (c d)) => NonEmptyFeature Con b c d where
{- For any set of logically equivalent premises A1,...,An, there are two premises:
The first premise contains the (negated) stripped conclusions of (negative)
literals with a premise from A1,...,An.
The second premise contains just the statement that all A1,...,An are
logically equivalent. -}
  nefMatch flags seq =
    let neglits premises = [ Neg phi |
         Neg (Mod (Con (psi : phi : _))) <- seq, psi `elem` premises]
        poslits premises = [ phi |
         Mod (Con (psi : phi : _)) <- seq, psi `elem` premises]
    in if flags !! 1
       then [ trace ("  <Trying to match... Current antecedents:>     ["
               ++ pretty_list prems ++ "]") $
            [Sequent prems] :
            [[Sequent (neglits prems ++ poslits prems)]]
              | prems <- power_premises seq]
        else [ [Sequent (are_equiv prems)] :
             [[Sequent (neglits prems ++ poslits prems)]]
               | prems <- power_premises seq]

  nefPretty d = genfPretty d "[Con]"
  nefFeatureFromSignature sig = Con
  nefFeatureFromFormula phi = Con
  nefStripFeature (Con phis) = phis
  nefSeparator sig = "=>"

{- ------------------------------------------------------------------------------
additional functions for the matching function of this logic
------------------------------------------------------------------------------ -}

{- create sequent which states that all elements of the input list are equivalent
to the input formula. -}
are_equiv :: (Feature a b) => [Formula (a b)] -> [Formula (a b)]
are_equiv [] = []
are_equiv (psi : []) = {- trace ("  <Identity not needed to prove:>               "
                     ++ (pretty psi) ++ " = " ++ (pretty psi)) $ -}
                     []
are_equiv (psi : phi : xs) =  {- trace ("  <One pair to prove:>                          "
                          ++ (pretty phi) ++ " = " ++ (pretty psi)) $ -}
  And (Neg (And (Neg psi) phi)) (Neg (And (Neg phi) psi)) : are_equiv (psi : xs)

-- return the premises of each positive or negative literal in the input sequent
con_premises :: (Feature Con b) => [Formula (Con b)] -> [Formula b]
con_premises seq = [psi | (Mod (Con (psi : phi : _))) <- seq] ++
                   [psi | (Neg (Mod (Con (psi : phi : _)))) <- seq]

{- return the list of all combinations of premises that appear in the input
sequent -}
power_premises :: (Feature Con b) => [Formula (Con b)] -> [[Formula b]]
power_premises xs = powerList (con_premises xs)

{- ------------------------------------------------------------------------------
instance of sigFeature for Conditional logic with conditional excluded middle
------------------------------------------------------------------------------ -}

instance (SigFeature b c d, Eq (c d), Eq (b (c d))) => NonEmptySigFeature Con b c d where
  neGoOn = genericPGoOn
