{-# OPTIONS -fglasgow-exts #-}

module GMP.ModalLogic where

import GMP.GMPAS

import Text.ParserCombinators.Parsec

import qualified Data.Set as Set

data PPflag = Sqr | Ang | None

deriving Eq

-------------------------------------------------------------------------------

-- Modal Logic Class

-------------------------------------------------------------------------------

class ModalLogic a b | a -> b, b -> a where

-- orderIns :: Set.Set (Formula a) -> Bool -- order insensitivity flag

flagML :: (Formula a) -> PPflag -- primary modal operator flag

parseIndex :: Parser a -- index parser

matchR :: (ModClause a) -> [b] -- Rho matching

guessClause :: b -> [PropClause] -- clause guessing

{- default instance for the (negated) contracted clause choosing

- @ param n : the pseudovaluation

- @ param ma : the modal atoms (excluding variables)

- @ return : the list of contracted clauses entailed by h -}

contrClause :: (Ord a)=>Set.Set(Formula a)->Set.Set(Formula a)->[ModClause a]

contrClause n ma =

let p = Set.difference ma n

pl = perm p

nl = perm n

in combineLit pl nl

-------------------------------------------------------------------------------

{- permute the elements of a set

- @ param s : the set

- @ return : list of permuted items (stored as list) -}

perm :: (Ord t) => Set.Set t -> [[t]]

perm s =

let perms l =

case l of

[] -> [[]]

xs -> [x : ps | (x,ys) <- selections xs, ps <- perms ys]

selections l =

case l of

[] -> []

x : xs -> (x,xs) : [(y,x:ys) | (y,ys) <- selections xs]

in perms (Set.toList s)

{- combine the positive and negative literals from the possible ones

- @ param l1 : list of modal atoms

- @ param l2 : list of modal atoms

- @ return : combined lists -}

combineLit :: [[Formula a]] -> [[Formula a]] -> [ModClause a]

combineLit l1 l2 = [Mimplies x y | x <- l1, y <- l2]

-------------------------------------------------------------------------------

-------------------------------------------------------------------------------