GMPAS.hs revision 44c6463550fe61e24668a2c79f90ce413a1ef6e2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-------------------------------------------------------------------------------
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- the Generic Model Parser Abstract Syntax
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski-- Copyright 2007, Lutz Schroeder and Georgel Calin
73dfcef93ee2ba07fedf4f3c74bace31853d1b9fChristian Maeder-------------------------------------------------------------------------------
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport qualified Data.Set as Set
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-------------------------------------------------------------------------------
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski-- Abstract Syntax
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski-------------------------------------------------------------------------------
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski-- Datatype for the clauses ---------------------------------------------------
0095c7efbddd0ffeed6aaf8ec015346be161d819Till Mossakowskidata PropClause = Pimplies [Int] [Int]
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder deriving Show
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- Datatypes for the modal index ----------------------------------------------
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederdata ModalK = ModalK () -- K modal logic index
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder deriving (Eq, Ord)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederdata ModalKD = ModalKD () -- KD modal logic index
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder deriving (Eq, Ord)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederdata GML = GML Int -- Graded modal logic index
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder deriving (Eq, Ord)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederdata CL = CL (Set.Set Int) Int -- Coalition modal logic index
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder deriving (Eq, Ord)
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederdata ML = ML Int -- Majority modal logic index
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder deriving (Eq, Ord)
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederdata Kars = Kars [Char] -- Generic modal logic index
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder deriving (Eq, Ord)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- Formula Datatype -----------------------------------------------------------
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederdata Otype = Square | Angle -- type of the Modal Operator
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder deriving (Eq, Ord)
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maederdata Junctor = And | Or | If | Fi | Iff
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder deriving (Eq, Ord)
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maederdata Mop a = Mop a Otype -- Modal Operator: index & type
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder deriving (Eq, Ord)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederdata Formula a = F -- datatype for the formulae
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder | Neg (Formula a)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder | Junctor (Formula a) Junctor (Formula a)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder | Mapp (Mop a) (Formula a) -- modal appl constr
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder | Var Char Integer -- variables
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder deriving (Eq, Ord)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- Modal Clause (Negated and Positive modal Atoms -----------------------------
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederdata ModClause a = Mimplies [Formula a] [Formula a]
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder deriving (Eq, Ord)
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski-------------------------------------------------------------------------------
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski-- Show Instances 4 Abstract Syntax
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski-------------------------------------------------------------------------------
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowskiinstance Show a => Show (Mop a) where
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski show m = case m of
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski Mop x Square -> "[" ++ show x ++ "]"
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski Mop x Angle -> "<" ++ show x ++ ">"
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowskiinstance Show Junctor where
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski show j = case j of
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowskiinstance Show a => Show (Formula a) where
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder show f = case f of
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Neg x -> "~" ++ show x
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Junctor x j y -> "(" ++ show x ++ " " ++ show j ++ " " ++ show y ++ ")"
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Mapp m x -> show m ++ show x
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Var x i -> show ([x] ++ show i)
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederinstance Show Kars where
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder show (Kars l) = show l
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederinstance Show CL where
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder show (CL i m) = let showSet s =
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder 1 -> let (aux, next) = Set.deleteFindMin s
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder in show aux ++ showSet next
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder _ -> let (aux, next) = Set.deleteFindMin s
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder in show aux ++ "," ++ showSet next
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder in "{" ++ showSet i ++ "}" ++ ":" ++ show m
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maederinstance Show ModalK where
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder show (ModalK ()) = ""
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederinstance Show ModalKD where
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder show (ModalKD ()) = ""
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederinstance Show GML where
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder show (GML n) = show n
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederinstance Show ML where
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder show x = case x of
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder ML n -> show n
b20cc520e698253354303b7bf3bc17f84240b213Klaus Luettich-------------------------------------------------------------------------------
b20cc520e698253354303b7bf3bc17f84240b213Klaus Luettich-------------------------------------------------------------------------------