content: {- | 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
  