{- | Module : ./GMP/GMP-CoLoSS/GMP/Logics/C.hs

- Description : Implementation of logic instance Coalition Logic

- 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 coalition logic.

-}

{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, FlexibleContexts #-}

module GMP.Logics.C 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 coalition logic

------------------------------------------------------------------------------ -}

data C a = C [Int] [Formula a] deriving (Eq, Show)

agents :: Int; agents = 10

{- For each positive modal literal, there are possibly serveral premises,

containing only one sequent each. This sequent contains the stripped positive

literal and additional stripped literals which are computed by

'c_build_matches'. Also there is one additional premise, containing the sequent

of all negated stripped negative literals.

e.g. seq = [ (M (C [0,3]) p), !(M (C [0]) q), (M (C [0,2,3]) !p), !(M (C [1]) !r)]

match seq = [ [[ p, !p, !q ]], [[ p, !p, !q]], [[!q, r]] ] -}

instance (SigFeature b c d, Eq (b (c d)), Eq (c d)) => NonEmptyFeature C b c d where

nefMatch flags seq = let neglits = [ Neg phi | Neg (Mod (C s [phi])) <- seq ]

poslits = [ phi | Mod (C s [phi]) <- seq ]

in [ [[Sequent (c_match ++ poslits)]] |

c_match <- c_build_matches (keep_poslits seq)

(keep_neglits seq)] ++ [[[Sequent neglits]]]

nefPretty d = case d of

C l [] -> "[C]" ++ show l ++ "nothing contained"

C l e -> "[C]" ++ show l ++ pretty (head e)

nefFeatureFromSignature sig = C [1]

nefFeatureFromFormula phi = C [1]

nefStripFeature (C i phis) = phis

nefDisj2Conj (Mod (C l phi)) = Mod (C l [disj2conj (head phi)])

nefNegNorm (Mod (C l phi)) = Mod (C l [negNorm (head phi)])

nefParser sig = do -- checks whether there are more numbers to be parsed

let stopParser = do char ','

return False

<|> do char '}'

return True

<?> "Parser.parseCindex.stop"

-- checks whether the index is of the form x1,..,x&

let normalParser l = do x <- natural

let n = fromInteger x

spaces

q <- stopParser

spaces

if q then normalParser (n : l)

else return (n : l)

<?> "Parser.parseCindex.normal"

char '{'

res <- try (normalParser [])

return $ C res

<|> do -- checks whether the index is of the form "n..m"

let shortParser = do x <- natural

let n = fromInteger x

spaces

string ".."

spaces

y <- natural

let m = fromInteger y

return [n .. m]

<?> "Parser.parseCindex.short"

res <- try shortParser

return $ C res

<?> "Parser.parseCindex"

{- ------------------------------------------------------------------------------

additional functions for the matching function of this logic

------------------------------------------------------------------------------ -}

-- Form negative literal parts of matching premise for positive literals

c_build_matches :: (Eq b) => [Formula (C b)] -> [Formula (C b)] -> [[Formula b]]

c_build_matches [] _ = []

c_build_matches ( Mod (C pset pphi) : pls) nls =

let relevant_neglits = filter (\ (Neg (Mod (C s _))) -> ((s `intersect` pset) == s)) nls

relevant_ncoalitions = nub $ map (\ (Neg (Mod (C s _))) -> s) relevant_neglits

maximal_pw_dis_lists = rm_sublists $ sortBy compare_length

(filter pairwise_disjunct

(powerList relevant_ncoalitions))

negmats = [ [Neg phi] | [Neg (Mod (C s [phi]))] <-

concatMap (build_lit_lists relevant_neglits) maximal_pw_dis_lists]

in map ([head pphi] ++) negmats ++ c_build_matches pls nls

{- Given a list of negative literals and a list of pairwise disjunctive lists, form pairwise

disjunctive lists of the according literals -}

build_lit_lists :: (Eq b) => [Formula (C b)] -> [[Int]] -> [[Formula (C b)]]

build_lit_lists _ [] = [[]]

build_lit_lists lits (set : sets) =

let relevant_neglits = filter (\ (Neg (Mod (C t _))) -> set == t) lits

in if null relevant_neglits then [] else

map ([head relevant_neglits] ++) (build_lit_lists lits sets)

++ build_lit_lists (lits \\ [head relevant_neglits]) (set : sets)

-- Does the list contain only pairwise disjunct lists?

pairwise_disjunct :: (Eq a) => [[a]] -> Bool

pairwise_disjunct [] = True

pairwise_disjunct (x : xs) = all (\ y -> null (x `intersect` y)) xs &&

pairwise_disjunct xs

-- Remove sublists (i.e. keep only maximal lists). Requires input to be sorted

rm_sublists :: (Eq a) => [[a]] -> [[a]]

rm_sublists [] = []

rm_sublists (x : xs) | any (\ y -> x `intersect` y == x) xs = rm_sublists xs

| otherwise = x : rm_sublists xs

-- Compare lists by size.

compare_length :: [a] -> [a] -> Ordering

compare_length s t = if length s < length t then LT else GT

{- ------------------------------------------------------------------------------

instance of sigFeature for coalition logic

------------------------------------------------------------------------------ -}

instance (SigFeature b c d, Eq (c d), Eq (b (c d))) => NonEmptySigFeature C b c d where

neGoOn = genericPGoOn