a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-------------------------------------------------------------------------------

08ea5f703d2e034f347a7e30ee3cca8a127d9c0eChristian Maeder-- the Generic Model Parser Abstract Syntax

e071fb22ea9923a2a4ff41184d80ca46b55ee932Till Mossakowski-- Copyright 2007, Lutz Schroeder and Georgel Calin

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-------------------------------------------------------------------------------

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachmodule GMP.GMPAS where

b4fbc96e05117839ca409f5f20f97b3ac872d1edTill Mossakowski

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport qualified Data.Set as Set

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-------------------------------------------------------------------------------

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-- Abstract Syntax

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder-------------------------------------------------------------------------------

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-- Datatype for the clauses ---------------------------------------------------

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachdata PropClause = Pimplies [Int] [Int]

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly deriving Show

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly-- Datatypes for the modal index ----------------------------------------------

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reillydata ModalK = ModalK () -- K modal logic index

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly deriving (Eq, Ord)

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reillydata ModalKD = ModalKD () -- KD modal logic index

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly deriving (Eq, Ord)

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reillydata GML = GML Int -- Graded modal logic index

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly deriving (Eq, Ord)

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reillydata CL = CL (Set.Set Int) -- Coalition modal logic index

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly deriving (Eq, Ord)

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reillydata ML = ML Int -- Majority modal logic index

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly | W

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly deriving (Eq, Ord)

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reillydata Kars = Kars [Char] -- Generic modal logic index

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly deriving (Eq, Ord)

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly-- Formula Datatype -----------------------------------------------------------

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reillydata Otype = Square | Angle -- type of the Modal Operator

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly deriving (Eq, Ord)

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reillydata Junctor = And | Or | If | Fi | Iff

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly deriving (Eq, Ord)

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reillydata Mop a = Mop a Otype -- Modal Operator: index & type

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly deriving (Eq, Ord)

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reillydata Formula a = F -- datatype for the formulae

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly | T

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly | Neg (Formula a)

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly | Junctor (Formula a) Junctor (Formula a)

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly | Mapp (Mop a) (Formula a) -- modal appl constr

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach | Var Char Integer -- variables

bcd914850de931848b86d7728192a149f9c0108bChristian Maeder deriving (Eq, Ord)

de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder-- Modal Clause (Negated and Positive modal Atoms -----------------------------

842ae753ab848a8508c4832ab64296b929167a97Christian Maederdata ModClause a = Mimplies [Formula a] [Formula a]

842ae753ab848a8508c4832ab64296b929167a97Christian Maeder deriving (Eq, Ord)

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder-------------------------------------------------------------------------------

842ae753ab848a8508c4832ab64296b929167a97Christian Maeder-- Show Instances 4 Abstract Syntax

2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly-------------------------------------------------------------------------------

816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reillyinstance Show a => Show (Mop a) where

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly show m = case m of

fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly Mop x Square -> "[" ++ show x ++ "]"

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder Mop x Angle -> "<" ++ show x ++ ">"

bcd914850de931848b86d7728192a149f9c0108bChristian Maederinstance Show Junctor where

2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly show j = case j of

2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly And -> "/\\"

d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian Maeder Or -> "\\/"

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly If -> "->"

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly Fi -> "<-"

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder Iff -> "<->"

096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reillyinstance Show a => Show (Formula a) where

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder show f = case f of

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder F -> "F"

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder T -> "T"

f284db6f4dffd7bf60b82319648efb7bcb9378c9Christian Maeder Neg x -> "~" ++ show x

f284db6f4dffd7bf60b82319648efb7bcb9378c9Christian Maeder Junctor x j y -> "(" ++ show x ++ " " ++ show j ++ " " ++ show y ++ ")"

90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett Mapp m x -> show m ++ " " ++ show x

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder Var x i -> show ([x] ++ show i)

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederinstance Show Kars where

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett show (Kars l) = show l

2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyinstance Show CL where

90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett show (CL i) = let showSet s =

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly case (Set.size s) of

2650e8a56cc2381719bd2390fdf82402e0c696d8Christian Maeder 0 -> ""

2650e8a56cc2381719bd2390fdf82402e0c696d8Christian Maeder 1 -> let (aux, next) = Set.deleteFindMin s

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder in show aux ++ showSet next

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly _ -> let (aux, next) = Set.deleteFindMin s

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly in show aux ++ "," ++ showSet next

4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder in "{"++ showSet i ++"}"

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederinstance Show ModalK where

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly show (ModalK ()) = ""

842ae753ab848a8508c4832ab64296b929167a97Christian Maederinstance Show ModalKD where

842ae753ab848a8508c4832ab64296b929167a97Christian Maeder show (ModalKD ()) = ""

842ae753ab848a8508c4832ab64296b929167a97Christian Maederinstance Show GML where

842ae753ab848a8508c4832ab64296b929167a97Christian Maeder show (GML n) = show n

842ae753ab848a8508c4832ab64296b929167a97Christian Maederinstance Show ML where

4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder show x = case x of

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ML n -> show n

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly W -> "W"

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder -- this is not really correct since W is actually the modal application

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly