{- | Module     : $Header$
 -  Description : Implementation of logic instance HML
 -  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 Henessy-Milner logic.
 -}

module GMP.Logics.HM where
import List
import Ratio
import Maybe

import Debug.Trace
import Text.ParserCombinators.Parsec

import GMP.Logics.Generic
import GMP.Parser

--------------------------------------------------------------------------------
-- instance of feature for Hennessy-Milner logic
--------------------------------------------------------------------------------

data HM a = HM Char [Formula a] deriving (Eq,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 with the same index.
-- e.g. seq       = [ (M (HM a) p), !(M (HM b) q), (M (HM b) !p), !(M (HM a) !r)]
--      match seq = [ [[ p, r]], [[ !p, r]] ]

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

  nefPretty d = case d of 
                  HM c [] -> "[HM]" ++ (show c) ++ "nothing contained"
                  HM c e -> "[HM]" ++ (show c) ++ (pretty (head e))
  nefFeatureFromSignature sig = HM 'a'
  nefFeatureFromFormula phi = HM 'a'
  nefStripFeature (HM a phis) = phis

  nefDisj2Conj (Mod (HM c phi)) = Mod ((HM c ([disj2conj (head phi)])))
  nefNegNorm (Mod (HM c phi)) = Mod ((HM c ([negNorm (head phi)])))

  nefParser sig = do c <- letter
                     return $ HM c
                <?> "Parser.parseHMindex"

--------------------------------------------------------------------------------
-- instance of sigFeature for Hennessy-Milner logic
--------------------------------------------------------------------------------

instance (SigFeature b c d, Eq (c d), Eq (b (c d))) => NonEmptySigFeature HM b c d where
  neGoOn sig flag = genericPGoOn sig flag

