content: {- | Module     : ./GMP/GMP-CoLoSS/GMP/Logics/HM.hs
   -  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.
   -}
  {-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, FlexibleContexts #-}
  module GMP.Logics.HM 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 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 = genericPGoOn
  