{- | Module     : ./GMP/GMP-CoLoSS/GMP/Logics/KD.hs
 -  Description : Implementation of logic instance KD
 -  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 the modal logic KD.
 -}
{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, FlexibleContexts #-}
module GMP.Logics.KD 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 KD
------------------------------------------------------------------------------ -}

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

{- For each positive modal literal, there is a premise containing only one
sequent. This sequent contains the stripped positive literal and all
negated stripped negative literals. Also there is an additional premise,
containing the sequent of all negated stripped negative literals.
e.g. seq       = [ (M KD p), !(M KD q), (M KD !p), !(M KD !r)]
match seq = [ [[ p, !q, r]], [[ !p, !q, r]], [[!q, r]] ] -}

instance (SigFeature b c d, Eq (b (c d)), Eq (c d)) => NonEmptyFeature KD b c d where
  nefMatch flags seq = let stripnlits = [ Neg (head phi) |
                                          Neg (Mod (KD phi)) <- seq]
                           striplits = [ head phi | Mod (KD phi) <- seq]
                       in (if flags !! 1 then trace ("\n  <KD-matching this:> "
                            ++ pretty_list seq) else id)
                           [ [[Sequent (pos : stripnlits)]] | pos <- striplits]
                           ++ [[[ Sequent stripnlits ]]]


  nefPretty d = genfPretty d "[KD]"
  nefFeatureFromSignature sig = KD
  nefFeatureFromFormula phi = KD
  nefStripFeature (KD phis) = phis

{- ------------------------------------------------------------------------------
instance of sigFeature for KD
------------------------------------------------------------------------------ -}

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