CoalitionL.hs revision 3a6266ac21c1a3492d51968584d7c56043dce32b
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder{-# OPTIONS -fglasgow-exts #-}
e071fb22ea9923a2a4ff41184d80ca46b55ee932Till Mossakowskiimport qualified Data.Set as Set
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachdata CLrules = CLNR Int
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach | CLPR Int Int
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder deriving Show
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachdata Coeffs = Coeffs [Set.Set Int] [Set.Set Int]
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach deriving (Eq, Ord)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyinstance ModalLogic CL CLrules where
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder-- orderIns _ = True
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder flagML _ = Sqr
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder parseIndex = do char '{'
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let stopParser = do try(char ',')
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly <|> do try(char '}')
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return (1::Integer)
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly let xParser s = do n <- natural
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly let news = Set.insert (fromInteger n) s
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly q <- stopParser
d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian Maeder 0 -> xParser news
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly _ -> return news
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly let isEmptyParser = do try(char '}')
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder <|> do aux <- xParser Set.empty
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder res <- isEmptyParser
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return $ CL res
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly matchR r = let Coeffs q w = eccContent r
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett in if (pairDisjoint q)&&(w/=[])
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly then if (allSubsets q (head w))&&(allMaxEq (head w) (tail w))
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly then [CLPR (length q) (-1 + length w)]
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly else if (pairDisjoint w)&&(q==[])
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly then [CLNR (length w)]
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly guessClause r =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly CLNR n -> [Pimplies [] [1..n]]
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly CLPR n m -> [Pimplies [1..n] [1..(m+1)]]
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-------------------------------------------------------------------------------
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder{- extract the content of the contracted clause
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder - @ param (Mimplies n p) : contracted clause
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder - @ return : the grades of equivalentmodal applications in the input param -}
842ae753ab848a8508c4832ab64296b929167a97Christian MaedereccContent :: ModClause CL -> Coeffs
842ae753ab848a8508c4832ab64296b929167a97Christian MaedereccContent (Mimplies n p) =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly let getGrade x =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Mapp (Mop (CL i) Square) _ -> i
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly in Coeffs (map getGrade n) (map getGrade p)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly{- check if the list of sets contains pairwise disjoint sets
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder - @ param x : list of sets to be checked for containing disjoint sets
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder - @ return : True if the sets are disjoint, false otherwise -}
842ae753ab848a8508c4832ab64296b929167a97Christian MaederpairDisjoint :: [Set.Set Int] -> Bool
842ae753ab848a8508c4832ab64296b929167a97Christian MaederpairDisjoint x =
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let disjoint e l =
67e234eb781dd16dfd269486befd2b5781075079Christian Maeder r:s -> if (Set.difference e r == e) then disjoint e s
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder h:t -> if not(disjoint h t) then False
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder else pairDisjoint t
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder{- check if all the sets in a list are subsets of another set
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder - @ param l : list of supposably subsets
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly - @ param s : supposed superset
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder - @ return : True if l contains only subsets of s -}
842ae753ab848a8508c4832ab64296b929167a97Christian MaederallSubsets :: (Ord a) => [Set.Set a] -> Set.Set a -> Bool
842ae753ab848a8508c4832ab64296b929167a97Christian MaederallSubsets l s =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly h:t -> if (Set.isSubsetOf h s) then (allSubsets t s)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly{- check if all the sets in a list are equal to a superset of a given set
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly - @ param s : given set to be subset of the equal sets in the list
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly - @ param l : list of sets which should be equal
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett - @ return : True if s is a subset of the identical sets in l -}
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettallMaxEq :: (Ord a) => Set.Set a -> [Set.Set a] -> Bool
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyallMaxEq s l =
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly _ -> let aux = head l
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly in if (Set.isSubsetOf s aux)&&and(map (==aux) (tail l))
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-------------------------------------------------------------------------------