content: {- | Module     : ./GMP/GMP-CoLoSS/GMP/Logics/Mon.hs
   -  Description : Implementation of logic instance Mon
   -  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 monotonic modal logic.
   -}
  {-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, FlexibleContexts #-}
  module GMP.Logics.Mon 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 Monotonic logic
  ------------------------------------------------------------------------------ -}
  
  data Mon a = Mon [Formula a] deriving (Eq, Show)
  
  {- For any combination of a positive and a negative literal, there is a premise
  containing only one sequent. This sequent contains only one formula over the
  stripped positive literal and the negated stripped negative literal.
  e.g. seq       = [ (M Mon p), !(M Mon q), (M Mon !p), !(M Mon !r)]
  match seq = [ [[ p, !q]], [[p, r]], [[ !p, !q]], [[ !p, r]] ] -}
  
  instance (SigFeature b c d, Eq (b (c d)), Eq (c d)) => NonEmptyFeature Mon b c d where
    nefMatch flags seq =
      let stripnlits = [ Neg (head phi) | Neg (Mod (Mon phi)) <- seq]
          striplits = [ head phi | Mod (Mon phi) <- seq]
      in [ [[Sequent [Neg (And (Neg neg) (Neg pos))]]] |
           neg <- stripnlits, pos <- striplits]
  
    nefPretty d = genfPretty d "[Mon]"
    nefFeatureFromSignature sig = Mon
    nefFeatureFromFormula phi = Mon
    nefStripFeature (Mon phis) = phis
  
  {- ------------------------------------------------------------------------------
  instance of sigFeature for Monotonic logic
  ------------------------------------------------------------------------------ -}
  
  instance (SigFeature b c d, Eq (c d), Eq (b (c d))) => NonEmptySigFeature Mon b c d where
    neGoOn = genericPGoOn
  