GMP.GMPAS.hs revision 61b020f416f2204caf544da16d97b9955148b53e
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-------------------------------------------------------------------------------
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-- the Generic Model Parser Abstract Syntax
5d801400993c9671010d244646936d8fd435638cChristian Maeder-- Copyright 2007, Lutz Schroeder and Georgel Calin
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-------------------------------------------------------------------------------
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-------------------------------------------------------------------------------
5d801400993c9671010d244646936d8fd435638cChristian Maeder-- Abstract Syntax
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-------------------------------------------------------------------------------
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance-- Datatype for the clauses ---------------------------------------------------
aa0ca44e856c87db27e61687cbb630f270976da1Felix Gabriel Mancedata PropClause = Pimplies [Int] [Int]
5d801400993c9671010d244646936d8fd435638cChristian Maeder deriving Show
5d801400993c9671010d244646936d8fd435638cChristian Maeder-- Datatypes for the modal index ----------------------------------------------
5d801400993c9671010d244646936d8fd435638cChristian Maederdata ModalK = ModalK () -- K modal logic index
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance deriving (Eq, Ord)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancedata ModalKD = ModalKD () -- KD modal logic index
097bc9f18b722812d480df0f5c634d09cbca8e21Felix Gabriel Mance deriving (Eq, Ord)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancedata GML = GML Int -- Graded modal logic index
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder deriving (Eq, Ord)
dc8c83e9922e4746c192916565f3522418534f3aFelix Gabriel Mancedata CL = CL Integer -- Coalition modal logic index
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance deriving (Eq, Ord)
feab1106bbee4f2ea2fd48bca7106dd041e4211dFelix Gabriel Mancedata Kars = Kars [Char] -- Generic modal logic index
18ff56829e5e99383ee6106584d55bcbd8ed45e7Felix Gabriel Mance deriving (Eq, Ord)
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance-- Formula Datatype -----------------------------------------------------------
b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maederdata Otype = Square | Angle -- type of the Modal Operator
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance deriving (Eq, Ord)
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mancedata Junctor = And | Or | If | Fi | Iff
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance deriving (Eq, Ord)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancedata Mop a = Mop a Otype -- Modal Operator: index & type
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance deriving (Eq, Ord)
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mancedata Formula a = F -- datatype for the formulae
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance | Neg (Formula a)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance | Junctor (Formula a) Junctor (Formula a)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance | Mapp (Mop a) (Formula a) -- modal appl constr
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance | Var Char Integer -- variables
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance deriving (Eq, Ord)
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance-- Modal Clause (Negated and Positive modal Atoms -----------------------------
0ec1551231bc5dfdcb3f2bd68fec7457fade7bfdFelix Gabriel Mancedata ModClause a = Mimplies [Formula a] [Formula a]
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance deriving (Eq, Ord)
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder-------------------------------------------------------------------------------
968930c7674ae3b63d308bf4fa651400aa263054Christian Maeder-- Show Instances 4 Abstract Syntax
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-------------------------------------------------------------------------------
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Manceinstance Show a => Show (Mop a) where
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance show m = case m of
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance Mop x Square -> "[" ++ show x ++ "]"
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance Mop x Angle -> "<" ++ show x ++ ">"
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Manceinstance Show Junctor where
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance show j = case j of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceinstance Show a => Show (Formula a) where
3c6b4f79cea11dd2acc2060bf1502b6ba9e905f2Felix Gabriel Mance show f = case f of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Neg x -> "~" ++ show x
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder Junctor x j y -> "(" ++ show x ++ " " ++ show j ++ " " ++ show y ++ ")"
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Mapp m x -> show m ++ " " ++ show x
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Var x i -> show ([x] ++ show i)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceinstance Show Kars where
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance show (Kars l) = show l
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceinstance Show CL where
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance show (CL s) = let (d,p) = divMod s 2
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance in if (d == 0)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance else show (CL d) ++ show p
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceinstance Show ModalK where
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder show (ModalK ()) = ""
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Manceinstance Show ModalKD where
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance show (ModalKD ()) = ""
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceinstance Show GML where
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance show (GML n) = show n