GMPAS.hs revision 4f621ec3a4e599391b6e5cbf5870d5bd90415f1c
076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian Maeder----------------------------------------------------------------
076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian Maeder-- the Generic Model Parser Abstract Syntax
81d182b21020b815887e9057959228546cf61b6bChristian Maeder-- Copyright 2007, Lutz Schroeder and Georgel Calin
076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian Maeder----------------------------------------------------------------
076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian Maedermodule GMPAS where
076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian Maeder----------------------------------------------------------------
076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian Maeder-- Abstract Syntax
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder----------------------------------------------------------------
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maederdata ModalK = ModalK () -- K modal logic
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maederdata ModalKD = ModalKD () -- KD modal logic
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maederdata BitString = BitString Integer -- for bit-string indexes
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maederdata Kars = Kars [Char] -- for string indexes
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederdata Otype = Square | Angle -- type of the Modal Operator
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder deriving (Eq, Ord)
076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian Maederdata Junctor = And | Or | If | Fi | Iff
35db0960aa2e2a13652381c756fae5fb2b27213bChristian Maeder deriving (Eq, Ord)
ac510075311023bf24175f7a76b89ec2bbda0626Christian Maederdata Mop a = Mop a Otype -- Modal Operator: index & type
ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder deriving (Eq, Ord)
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maederdata Formula a = F -- datatype for the formulae
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder | Neg (Formula a)
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder | Junctor (Formula a) Junctor (Formula a)
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder | Mapp (Mop a) (Formula a) -- modal appl constr
6e5180855658f12f9059d9041f447bf0935de344Christian Maeder deriving (Eq, Ord)
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder----------------------------------------------------------------
8a1f427564a5ae2db32332512237ef645289c34dChristian Maeder-- Print Abstract Syntax
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder----------------------------------------------------------------
76647324ed70f33b95a881b536d883daccf9568dChristian Maederinstance Show a => Show (Mop a) where
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder show m = case m of
1865083b72c1307e9040d78c2743abd5a54ee260Christian Maeder Mop x Square -> "[" ++ show x ++ "]"
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder Mop x Angle -> "<" ++ show x ++ ">"
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maederinstance Show Junctor where
76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder show j = case j of
fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederinstance Show a => Show (Formula a) where
ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder show f = case f of
b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder Neg x -> "~" ++ show x
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder Junctor x j y -> "(" ++ show x ++ " " ++ show j ++ " " ++ show y ++ ")"
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder Mapp m x -> show m ++ " " ++ show x
ac510075311023bf24175f7a76b89ec2bbda0626Christian Maederinstance Show Kars where
fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder show (Kars l) = show l
fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederinstance Show BitString where
fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder show (BitString s) = let (d,p)=divMod s 2 in
4be371b81d055e03a5946e4ec333613f313d689bChristian Maeder if (d == 0) then show p
4be371b81d055e03a5946e4ec333613f313d689bChristian Maeder else show (BitString d) ++ show p
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maederinstance Show ModalK where
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder show (ModalK ()) = show ()
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maederinstance Show ModalKD where
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder show (ModalKD ()) = show ()