Parse_AS.hs revision e071fb22ea9923a2a4ff41184d80ca46b55ee932
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederModule : $Header$
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederDescription : Parser for CoCASL
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiCopyright : (c) Till Mossakowski, Uni Bremen 2004
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederMaintainer : hausmann@informatik.uni-bremen.de
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiStability : provisional
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederParser for CoCASL
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedercocasl_reserved_words :: [String]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedercocasl_reserved_words = [diamondS]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskicocaslFormula :: AParser st C_FORMULA
0c2a90cbfb63865ff485c3fbe20a14589a5914beTill MossakowskicocaslFormula =
9744c7d9fa61d255d5e73beec7edc3499522e9e2Till Mossakowski do o <- oBracketT
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder m <- modality []
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder c <- cBracketT
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder f <- formula cocasl_reserved_words
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return (BoxOrDiamond True m f $ toPos o [] c)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder do o <- asKey lessS
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder m <- modality [greaterS] -- do not consume matching ">"!
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder c <- asKey greaterS
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski f <- formula cocasl_reserved_words
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return (BoxOrDiamond False m f $ toPos o [] c)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskimodality :: [String] -> AParser st MODALITY
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski do t <- term (prodS : ks ++ cocasl_reserved_words)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- put the term in parens if you need to use "*"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski option () (asKey prodS >> return ())
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- presence of "*" is not stored yet!
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return $ case t of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Mixfix_token tok -> Simple_mod tok
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski _ -> Term_mod t
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiinstance AParsable C_FORMULA where
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder aparser = cocaslFormula
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedercBasic :: AParser st C_BASIC_ITEM
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskicBasic = do f <- asKey cofreeS
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder ti <- coSigItems
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return (codatatypeToCofreetype ti (tokPos f))
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder <|> do g <- asKey cogeneratedS
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder do t <- sigItems cocasl_reserved_words
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return (CoSort_gen [Annoted t nullRange [] []] $ tokPos g)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder do o <- oBraceT
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski is <- annosParser (sigItems cocasl_reserved_words)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return (CoSort_gen is
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (toPos g [o] c))
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedercoSigItems :: AParser st C_SIG_ITEM
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till MossakowskicoSigItems = itemList cocasl_reserved_words cotypeS codatatype CoDatatype_items
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedercodatatype :: [String] -> AParser st CODATATYPE_DECL
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maedercodatatype ks =
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder do s <- sortId ks
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder e <- asKey defnS
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder a <- getAnnos
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (Annoted v _ _ b:as, ps) <- acoAlternative ks `separatedBy` barT
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return $ CoDatatype_decl s (Annoted v nullRange a b:as)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder $ catPos $ e:ps
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederacoAlternative :: [String] -> AParser st (Annoted COALTERNATIVE)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederacoAlternative ks =
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder do a <- coalternative ks
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder return (Annoted a nullRange [] an)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowskicoalternative :: [String] -> AParser st COALTERNATIVE
5e46b572ed576c0494768998b043d9d340594122Till Mossakowskicoalternative ks =
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder do s <- pluralKeyword sortS
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder (ts, cs) <- sortId ks `separatedBy` anComma
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder return (CoSubsorts ts $ catPos $ s:cs)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder do i <- consId ks
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder cocomp (Just i)
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder do cocomp Nothing
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski do o <- oParenT
10a2cf8d9887524acde19d4ea59f8fea3a7f3258Till Mossakowski (cs, ps) <- cocomponent ks `separatedBy` anSemi
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let qs = toPos o ps c
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski do q <- quMarkT
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder return (Co_construct Partial i cs (qs `appRange` tokPos q))
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder <|> return (Co_construct Total i cs qs)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder <|> return (Co_construct Total i [] nullRange)
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maedercocomponent :: [String] -> AParser st COCOMPONENTS
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maedercocomponent ks =
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder do (is, cs) <- parseId ks `separatedBy` anComma
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder t <- opType ks
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder return $ CoSelect is t $ catPos $ cs ++ [c]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederinstance AParsable C_SIG_ITEM where
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder aparser = coSigItems
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maederinstance AParsable C_BASIC_ITEM where
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder aparser = cBasic
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder---- helpers ----------------------------------------------------------------
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedercodatatypeToCofreetype :: C_SIG_ITEM -> Range -> C_BASIC_ITEM
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedercodatatypeToCofreetype d pos =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder CoDatatype_items ts ps -> CoFree_datatype ts (pos `appRange` ps)