Parse_AS.hs revision 2eeec5240b424984e3ee26296da1eeab6c6d739e
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder{- |
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2004
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian MaederMaintainer : hausmann@informatik.uni-bremen.de
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian MaederStability : provisional
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian MaederPortability : portable
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian MaederParser for CoCASL
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder-}
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maedermodule CoCASL.Parse_AS where
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maederimport Common.AnnoState
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maederimport Common.AS_Annotation
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maederimport Common.Id
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maederimport Common.Keywords
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maederimport Common.Lexer
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maederimport Common.Token
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maederimport CoCASL.AS_CoCASL
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maederimport Text.ParserCombinators.Parsec
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maederimport CASL.Formula
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport CASL.Parse_AS_Basic (sigItems)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport CASL.AS_Basic_CASL
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maedercocasl_reserved_words :: [String]
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maedercocasl_reserved_words = [diamondS]
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian MaedercocaslFormula :: AParser st C_FORMULA
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian MaedercocaslFormula =
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder do o <- oBracketT
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder m <- modality []
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder c <- cBracketT
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder f <- formula cocasl_reserved_words
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder return (BoxOrDiamond True m f $ toPos o [] c)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder <|>
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder do o <- asKey lessS
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder m <- modality [greaterS] -- do not consume matching ">"!
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder c <- asKey greaterS
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder f <- formula cocasl_reserved_words
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder return (BoxOrDiamond False m f $ toPos o [] c)
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maedermodality :: [String] -> AParser st MODALITY
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maedermodality ks =
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder do t <- term (prodS : ks ++ cocasl_reserved_words)
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder -- put the term in parens if you need to use "*"
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder option () (asKey prodS >> return ())
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder -- presence of "*" is not stored yet!
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder return $ case t of
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder Mixfix_token tok -> Simple_mod tok
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder _ -> Term_mod t
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maederinstance AParsable C_FORMULA where
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder aparser = cocaslFormula
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian MaedercBasic :: AParser st C_BASIC_ITEM
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian MaedercBasic = do f <- asKey cofreeS
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder ti <- coSigItems
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder return (codatatypeToCofreetype ti (tokPos f))
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder <|> do g <- asKey cogeneratedS
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder do t <- sigItems cocasl_reserved_words
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder return (CoSort_gen [Annoted t nullRange [] []] $ tokPos g)
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder <|>
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder do o <- oBraceT
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder is <- annosParser (sigItems cocasl_reserved_words)
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder c <- cBraceT
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder return (CoSort_gen is
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder (toPos g [o] c))
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian MaedercoSigItems :: AParser st C_SIG_ITEM
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian MaedercoSigItems = itemList cocasl_reserved_words cotypeS codatatype CoDatatype_items
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maedercodatatype :: [String] -> AParser st CODATATYPE_DECL
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maedercodatatype ks =
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder do s <- sortId ks
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder addAnnos
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder e <- asKey defnS
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder addAnnos
de4e22f27c1e1c6e0efbc72ffe1670f74181e49eChristian Maeder a <- getAnnos
(Annoted v _ _ b:as, ps) <- acoAlternative ks `separatedBy` barT
return $ CoDatatype_decl s (Annoted v nullRange a b:as)
$ catPos $ e:ps
acoAlternative :: [String] -> AParser st (Annoted COALTERNATIVE)
acoAlternative ks =
do a <- coalternative ks
an <- annos
return (Annoted a nullRange [] an)
coalternative :: [String] -> AParser st COALTERNATIVE
coalternative ks =
do s <- pluralKeyword sortS
(ts, cs) <- sortId ks `separatedBy` anComma
return (CoSubsorts ts $ catPos $ s:cs)
<|>
do i <- consId ks
cocomp (Just i)
<|>
do cocomp Nothing
where
cocomp i =
do o <- oParenT
(cs, ps) <- cocomponent ks `separatedBy` anSemi
c <- cParenT
let qs = toPos o ps c
do q <- quMarkT
return (Co_construct Partial i cs (qs `appRange` tokPos q))
<|> return (Co_construct Total i cs qs)
<|> return (Co_construct Total i [] nullRange)
cocomponent :: [String] -> AParser st COCOMPONENTS
cocomponent ks =
do (is, cs) <- parseId ks `separatedBy` anComma
c <- colonST
t <- opType ks
return $ CoSelect is t $ catPos $ cs ++ [c]
instance AParsable C_SIG_ITEM where
aparser = coSigItems
instance AParsable C_BASIC_ITEM where
aparser = cBasic
---- helpers ----------------------------------------------------------------
codatatypeToCofreetype :: C_SIG_ITEM -> Range -> C_BASIC_ITEM
codatatypeToCofreetype d pos =
case d of
CoDatatype_items ts ps -> CoFree_datatype ts (pos `appRange` ps)