GMPAS.hs revision 376c60e08a6dbaa1f15247789eae7872d340bbdb
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin-------------------------------------------------------------------------------
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin-- the Generic Model Parser Abstract Syntax
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin-- Copyright 2007, Lutz Schroeder and Georgel Calin
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin-------------------------------------------------------------------------------
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calinmodule GMPAS where
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin-------------------------------------------------------------------------------
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin-- Abstract Syntax
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin-------------------------------------------------------------------------------
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin-- Datatype for the clauses ---------------------------------------------------
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calindata PropClause = Pimplies [Int] [Int]
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin deriving Show
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin-- Datatypes for the modal index ----------------------------------------------
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calindata ModalK = ModalK () -- K modal logic index
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin deriving (Eq, Ord)
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calindata ModalKD = ModalKD () -- KD modal logic index
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin deriving (Eq, Ord)
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calindata GML = GML Int -- Graded modal logic index
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin deriving (Eq, Ord)
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calindata CL = CL Integer -- Coalition modal logic index
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin deriving (Eq, Ord)
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calindata Kars = Kars [Char] -- Generic modal logic index
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin deriving (Eq, Ord)
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin-- Formula Datatype -----------------------------------------------------------
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calindata Otype = Square | Angle -- type of the Modal Operator
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin deriving (Eq, Ord)
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calindata Junctor = And | Or | If | Fi | Iff
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin deriving (Eq, Ord)
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calindata Mop a = Mop a Otype -- Modal Operator: index & type
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin deriving (Eq, Ord)
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calindata Formula a = F -- datatype for the formulae
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin | Neg (Formula a)
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin | Junctor (Formula a) Junctor (Formula a)
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin | Mapp (Mop a) (Formula a) -- modal appl constr
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin | Var Char Integer -- variables
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin deriving (Eq, Ord)
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin-- Truth Value & Modal Atom type ----------------------------------------------
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calindata ModClause a = Mimplies [Formula a] [Formula a]
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin deriving (Eq, Ord)
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin-------------------------------------------------------------------------------
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin-- Show Instances 4 Abstract Syntax
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin-------------------------------------------------------------------------------
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calininstance Show a => Show (Mop a) where
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin show m = case m of
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin Mop x Square -> "[" ++ show x ++ "]"
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin Mop x Angle -> "<" ++ show x ++ ">"
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calininstance Show Junctor where
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin show j = case j of
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calininstance Show a => Show (Formula a) where
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin show f = case f of
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin Neg x -> "~" ++ show x
f00edd94c598adc73dc4f6005d79d2295e463da5Georgel Calin Junctor x j y -> "(" ++ show x ++ " " ++ show j ++ " " ++ show y ++ ")"
f00edd94c598adc73dc4f6005d79d2295e463da5Georgel Calin Mapp m x -> show m ++ " " ++ show x
f00edd94c598adc73dc4f6005d79d2295e463da5Georgel Calin Var x i -> show ([x] ++ show i)
f00edd94c598adc73dc4f6005d79d2295e463da5Georgel Calininstance Show Kars where
f00edd94c598adc73dc4f6005d79d2295e463da5Georgel Calin show (Kars l) = show l
f00edd94c598adc73dc4f6005d79d2295e463da5Georgel Calininstance Show CL where
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin show (CL s) = let (d,p) = divMod s 2
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin in if (d == 0)
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin else show (CL d) ++ show p
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calininstance Show ModalK where
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin show (ModalK ()) = ""
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calininstance Show ModalKD where
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin show (ModalKD ()) = ""
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calininstance Show GML where
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin show (GML n) = show n