7a8401ce858002b67e8f4198fde45a1562696ccbChristian Maeder{- HetCATS/CASL/Parse_AS_Basic.hs

2b4130336e941b7d01c78a6da55449a4c6eca609Till Mossakowski $Id$

53d399c20374a99bd95db1f9b5b93980cbf6a984Christian Maeder Authors: Wiebke Herding

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder Year: 2003

2b4130336e941b7d01c78a6da55449a4c6eca609Till Mossakowski

b4fbc96e05117839ca409f5f20f97b3ac872d1edTill Mossakowski parse Modal Logic Items

2b4130336e941b7d01c78a6da55449a4c6eca609Till Mossakowski-}

2b4130336e941b7d01c78a6da55449a4c6eca609Till Mossakowski

2b4130336e941b7d01c78a6da55449a4c6eca609Till Mossakowskimodule Modal.Parse_AS where

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederimport Common.AnnoState

59d823de481014f68b8b024474bffac150b56e1eWiebke Herdingimport Common.Id

cc6df32dd55910aac7de12b30cc5049d96b8f770Wiebke Herdingimport Common.Token

e4e1509ff358e739fddf1483ad39467e0e1becc2Christian Maederimport Common.Keywords

53d399c20374a99bd95db1f9b5b93980cbf6a984Christian Maederimport Common.Lexer

e4e1509ff358e739fddf1483ad39467e0e1becc2Christian Maederimport Modal.AS_Modal

310532f8a7a1a1f1b6c25c67b7c340abc0889335Christian Maederimport Common.AS_Annotation

e4e1509ff358e739fddf1483ad39467e0e1becc2Christian Maederimport Common.Lib.Parsec

e4e1509ff358e739fddf1483ad39467e0e1becc2Christian Maeder

e4e1509ff358e739fddf1483ad39467e0e1becc2Christian Maeder-- aus CASL, kann bleiben

53d399c20374a99bd95db1f9b5b93980cbf6a984Christian MaederbasicSpec :: AParser BASIC_SPEC

e4e1509ff358e739fddf1483ad39467e0e1becc2Christian MaederbasicSpec = (fmap Basic_spec $ annosParser basicItems)

35db0960aa2e2a13652381c756fae5fb2b27213bChristian Maeder <|> (oBraceT >> cBraceT >> return (Basic_spec []))

53d399c20374a99bd95db1f9b5b93980cbf6a984Christian Maeder

53d399c20374a99bd95db1f9b5b93980cbf6a984Christian MaederbasicItems :: AParser BASIC_ITEMS

cc6df32dd55910aac7de12b30cc5049d96b8f770Wiebke HerdingbasicItems = fmap Sig_items sigItems

414ffa281d82f05a2d742c702f8e06b0cb05b229Christian Maeder <|> dotFormulae -- sp�ter!

53d399c20374a99bd95db1f9b5b93980cbf6a984Christian Maeder

856bdbffc895793cc5739dbb862323944cb76fdbChristian MaedersigItems :: AParser SIG_ITEMS

856bdbffc895793cc5739dbb862323944cb76fdbChristian MaedersigItems = propItems

856bdbffc895793cc5739dbb862323944cb76fdbChristian Maeder

856bdbffc895793cc5739dbb862323944cb76fdbChristian MaederpropItem :: AParser PROP_ITEM

f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian MaederpropItem = do s <- sortId ; -- Props are the same as sorts (in declaration)

856bdbffc895793cc5739dbb862323944cb76fdbChristian Maeder commaPropDecl s

856bdbffc895793cc5739dbb862323944cb76fdbChristian Maeder <|>

856bdbffc895793cc5739dbb862323944cb76fdbChristian Maeder return (Prop_decl [s] [])

856bdbffc895793cc5739dbb862323944cb76fdbChristian Maeder

856bdbffc895793cc5739dbb862323944cb76fdbChristian MaederpropItems :: AParser SIG_ITEMS

f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian MaederpropItems = itemList propS propItem Prop_items

856bdbffc895793cc5739dbb862323944cb76fdbChristian Maeder

856bdbffc895793cc5739dbb862323944cb76fdbChristian MaedercommaPropDecl :: Id -> AParser PROP_ITEM

856bdbffc895793cc5739dbb862323944cb76fdbChristian MaedercommaPropDecl s = do c <- anComma

856bdbffc895793cc5739dbb862323944cb76fdbChristian Maeder (is, cs) <- sortId `separatedBy` anComma

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder let l = s : is

b1f52a36d45c5031c462291e263cec114975add1Wiebke Herding p = tokPos c : map tokPos cs in return (Prop_decl l p)

414ffa281d82f05a2d742c702f8e06b0cb05b229Christian Maeder

d297778800daa7ceba73ad9b19884c883487dee7Christian Maeder

d297778800daa7ceba73ad9b19884c883487dee7Christian MaederdotFormulae :: AParser BASIC_ITEMS

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederdotFormulae = do d <- dotT

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder (fs, ds) <- aFormula `separatedBy` dotT

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder (m, an) <- optSemi

53d399c20374a99bd95db1f9b5b93980cbf6a984Christian Maeder let ps = map tokPos (d:ds)

2b4130336e941b7d01c78a6da55449a4c6eca609Till Mossakowski ns = init fs ++ [appendAnno (last fs) an]

b1f52a36d45c5031c462291e263cec114975add1Wiebke Herding in case m of

414ffa281d82f05a2d742c702f8e06b0cb05b229Christian Maeder Nothing -> return (Axiom_items ns ps)

53d399c20374a99bd95db1f9b5b93980cbf6a984Christian Maeder Just t -> return (Axiom_items ns

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder (ps ++ [tokPos t]))

b1f52a36d45c5031c462291e263cec114975add1Wiebke Herding

414ffa281d82f05a2d742c702f8e06b0cb05b229Christian MaederaFormula :: AParser (Annoted FORMULA)

53d399c20374a99bd95db1f9b5b93980cbf6a984Christian MaederaFormula = bind appendAnno (annoParser formula) lineAnnos

53d399c20374a99bd95db1f9b5b93980cbf6a984Christian Maeder

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maederformula :: AParser FORMULA

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maederformula = impFormula []

b1f52a36d45c5031c462291e263cec114975add1Wiebke Herding

53d399c20374a99bd95db1f9b5b93980cbf6a984Christian MaederimpFormula :: [String] -> AParser FORMULA

53d399c20374a99bd95db1f9b5b93980cbf6a984Christian MaederimpFormula k =

b1f52a36d45c5031c462291e263cec114975add1Wiebke Herding do f <- andOrFormula k

414ffa281d82f05a2d742c702f8e06b0cb05b229Christian Maeder do c <- implKey

5bc645bae86e7cc7714ab73934b77bb98ecbd078Christian Maeder (fs, ps) <- andOrFormula k `separatedBy` implKey

b1f52a36d45c5031c462291e263cec114975add1Wiebke Herding return (makeImpl (f:fs) (map tokPos (c:ps)))

414ffa281d82f05a2d742c702f8e06b0cb05b229Christian Maeder <|>

53d399c20374a99bd95db1f9b5b93980cbf6a984Christian Maeder do c <- ifKey

310532f8a7a1a1f1b6c25c67b7c340abc0889335Christian Maeder (fs, ps) <- andOrFormula k `separatedBy` ifKey

310532f8a7a1a1f1b6c25c67b7c340abc0889335Christian Maeder return (makeIf (f:fs) (map tokPos (c:ps)))

53d399c20374a99bd95db1f9b5b93980cbf6a984Christian Maeder <|>

53d399c20374a99bd95db1f9b5b93980cbf6a984Christian Maeder do c <- asKey equivS

310532f8a7a1a1f1b6c25c67b7c340abc0889335Christian Maeder g <- andOrFormula k

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski return (Equivalence f g [tokPos c])

310532f8a7a1a1f1b6c25c67b7c340abc0889335Christian Maeder <|> return f

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski where makeImpl [f,g] p = Implication f g p

310532f8a7a1a1f1b6c25c67b7c340abc0889335Christian Maeder makeImpl (f:r) (c:p) =

53d399c20374a99bd95db1f9b5b93980cbf6a984Christian Maeder Implication f (makeImpl r p) [c]

310532f8a7a1a1f1b6c25c67b7c340abc0889335Christian Maeder makeImpl _ _ = error "makeImpl got illegal argument"

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder makeIf l p = makeImpl (reverse l) (reverse p)

310532f8a7a1a1f1b6c25c67b7c340abc0889335Christian Maeder

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian MaederandOrFormula :: [String] -> AParser FORMULA

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian MaederandOrFormula k =

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder do f <- primFormula k

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski do c <- andKey

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder (fs, ps) <- primFormula k `separatedBy` andKey

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder return (Conjunction (f:fs) (map tokPos (c:ps)))

53d399c20374a99bd95db1f9b5b93980cbf6a984Christian Maeder <|>

53d399c20374a99bd95db1f9b5b93980cbf6a984Christian Maeder do c <- orKey

(fs, ps) <- primFormula k `separatedBy` orKey

return (Disjunction (f:fs) (map tokPos (c:ps)))

<|> return f

implKey, ifKey :: AParser Token

implKey = asKey implS

ifKey = asKey ifS

instance PosItem FORMULA where

-- don't know if up_pos_l must be further defined. Now it's 'id'

updFormulaPos :: Pos -> Pos -> FORMULA -> FORMULA

updFormulaPos o c = up_pos_l (\l-> o:l++[c])

parenFormula :: [String] -> AParser FORMULA

parenFormula k =

do o <- oParenT

f <- impFormula k

c <- cParenT

return (updFormulaPos (tokPos o) (tokPos c) f)

boxKey, diamondKey :: AParser Token

boxKey = asKey boxS

diamondKey = asKey diamondS

primFormula :: [String] -> AParser FORMULA

primFormula k =

-- Does Modal logic operate on truth values?

-- No definedness

-- No quantification

-- No when...else

-- Diamond and Box operator

do c <- try(asKey notS <|> asKey negS) <?> "\"not\""

f <- primFormula k

return (Negation f [tokPos c])

<|>

do c <- boxKey

f <- primFormula k

return (Box f [tokPos c])

<|>

do c <- diamondKey

f <- primFormula k

return (Diamond f [tokPos c])

<|> parenFormula k

andKey, orKey :: AParser Token

andKey = asKey lAnd

orKey = asKey lOr