Parser.hs revision 3b7554a51bef04cbbb8c8ecd4642772fd8a9ca3f
967e5f3c25249c779575864692935627004d3f9eChristian Maeder{- | Module : $Header$
967e5f3c25249c779575864692935627004d3f9eChristian Maeder - Description : Implementation of logic formula parser
81d182b21020b815887e9057959228546cf61b6bChristian Maeder - Copyright : (c) Georgel Calin & Lutz Schroeder, DFKI Lab Bremen
f11f713bebd8e1e623a0a4361065df256033de47Christian Maeder - License : Similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder - Maintainer : g.calin@jacobs-university.de
967e5f3c25249c779575864692935627004d3f9eChristian Maeder - Stability : provisional
3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder - Portability : portable
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maeder - Provides the implementation of the generic parser for the L formula datatype
967e5f3c25249c779575864692935627004d3f9eChristian Maederdata ModalOperator = Sqr | Ang | None
650bafe7709533bc5f82bb9daf8fa06f431cd963Christian Maeder-- | Main parser
9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maederpar5er :: ModalOperator -> GenParser Char st a -> GenParser Char st (L a)
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maederpar5er flag pa = implFormula flag pa
8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maeder-- | Parser which translates all implications in disjunctions & conjunctions
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaederimplFormula :: ModalOperator -> GenParser Char st a -> GenParser Char st (L a)
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian MaederimplFormula flag pa = do
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder f <- orFormula flag pa
967e5f3c25249c779575864692935627004d3f9eChristian Maeder option f (do string "->"
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder i <- implFormula flag pa
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder return $ Or (Neg f) i
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder <|> do string "<->"
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder i <- implFormula flag pa
967e5f3c25249c779575864692935627004d3f9eChristian Maeder return $ And (Or (Neg f) i) (Or f (Neg i))
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder <|> do string "<-"
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder i <- implFormula flag pa
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder return $ Or f (Neg i)
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder <|> do return f
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder-- | Parser for disjunction - used for handling binding order
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaederorFormula :: ModalOperator -> GenParser Char st a -> GenParser Char st (L a)
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaederorFormula flag pa = do
a89389521ddf76109168a0b339031575aafbd512Christian Maeder f <- andFormula flag pa
a89389521ddf76109168a0b339031575aafbd512Christian Maeder option f $ do
a89389521ddf76109168a0b339031575aafbd512Christian Maeder g <- orFormula flag pa
a89389521ddf76109168a0b339031575aafbd512Christian Maeder return $ Or f g
a89389521ddf76109168a0b339031575aafbd512Christian Maeder-- | Parser for conjunction - used for handling the binding order
a89389521ddf76109168a0b339031575aafbd512Christian MaederandFormula :: ModalOperator -> GenParser Char st a -> GenParser Char st (L a)
a89389521ddf76109168a0b339031575aafbd512Christian MaederandFormula flag pa = do
a89389521ddf76109168a0b339031575aafbd512Christian Maeder f <- primFormula flag pa
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder option f $ do
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder g <- andFormula flag pa
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder return $ And f g
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder{- | Parse a primitive formula: T, F, ~f, <i>f, [i]f, p*,
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder - where i stands for an index, f for a formula and
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder - * for a series of digits i.e. and integer -}
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian MaederprimFormula :: ModalOperator -> GenParser Char st a -> GenParser Char st (L a)
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian MaederprimFormula flag pa =
67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder do string "T"
67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder <|> do string "F"
67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder <|> do f <- parenFormula flag pa
67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder <|> do string "~"
67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder f <- primFormula flag pa
67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder return $ nneg f
67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder <|> do char '<'
d48085f765fca838c1d972d2123601997174583dChristian Maeder f <- primFormula flag pa
d48085f765fca838c1d972d2123601997174583dChristian Maeder -- restrict to the default modal operator
d48085f765fca838c1d972d2123601997174583dChristian Maeder Ang -> return $ M i f
d48085f765fca838c1d972d2123601997174583dChristian Maeder Sqr -> return $ Neg (M i (nneg f))
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder _ -> return $ M i f
d48085f765fca838c1d972d2123601997174583dChristian Maeder <|> do char '['
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder f <- primFormula flag pa
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder -- restrict to the default modal operator
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder Sqr -> return $ M i f
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder Ang -> return $ Neg (M i (nneg f))
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder _ -> return $ M i f
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder <|> do char 'p'
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder i <- atomIndex
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder return $ Atom (fromInteger i)
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder-- | Parser for un-parenthesizing a formula
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaederparenFormula :: ModalOperator -> GenParser Char st a -> GenParser Char st (L a)
f11f713bebd8e1e623a0a4361065df256033de47Christian MaederparenFormula flag pa =
a578ec30cded5e396a7ce9a3b469e8cd3a88246aChristian Maeder f <- par5er flag pa
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder-- | Parse integer number
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maedernatural :: GenParser Char st Integer
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maedernatural = fmap read $ many1 digit
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder-- | Parse the possible integer index of a variable
99f1a09ee1847410faf46527f5465bd2070800c2Christian MaederatomIndex :: GenParser Char st Integer
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian MaederatomIndex = do i <- try natural
242397ba0f1cc490e892130bf0df239deeecf5daChristian Maeder-- | Parsers for the different modal logic indexes
242397ba0f1cc490e892130bf0df239deeecf5daChristian MaederparseCindex :: Parser C
2e9985cd67e4f2414becb670ef33b8f16513e41dChristian MaederparseCindex = do -- checks whether there are more numbers to be parsed
2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder let stopParser = do char ','
2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder <|> do char '}'
2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder -- checks whether the index is of the for x1,..,x&
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder let normalParser l = do x <- natural
2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder let n = fromInteger x
2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder q <- stopParser
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder False -> normalParser (n:l)
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski _ -> return (n:l)
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder res <- try(normalParser [])
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder return $ C res
842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder <|> do -- checks whether the index is of the form "n..m"
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski let shortParser = do x <- natural
842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder let n = fromInteger x
842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder let m = fromInteger y
967e5f3c25249c779575864692935627004d3f9eChristian Maeder res <- try(shortParser)
f2ee9fc53048ea92bad79e3f5d292d83efd7f8beMihai Codescu return $ C res
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederparseGindex :: Parser G
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederparseGindex = do n <- natural
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder return $ G (fromInteger n)
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederparseHMindex :: Parser HM
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederparseHMindex = do c <- letter
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder return $ HM c
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederparseKindex :: Parser K
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederparseKindex = return K
967e5f3c25249c779575864692935627004d3f9eChristian MaederparseKDindex ::Parser KD
ad187062b0009820118c1b773a232e29b879a2faChristian MaederparseKDindex = return KD
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederparsePindex :: Parser P
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder do x <- natural
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder let auxP n = do char '/'
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder return $ toRational (fromInteger n/fromInteger m)
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder <|> do char '.'
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder | n>=10 = 1 + noDig (div n 10)
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder let rat n = toRational(fromInteger n /
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder fromInteger (10^(noDig n)))
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder let res = toRational n + rat m
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder <|> do return $ toRational n
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder aux <- auxP x
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder return $ P aux
ad187062b0009820118c1b773a232e29b879a2faChristian MaederparseMindex :: Parser Mon
ad187062b0009820118c1b773a232e29b879a2faChristian MaederparseMindex = return Mon