Copyright : (c) Till Mossakowski, Uni Bremen 2004
Maintainer : hausmann@tzi.de
cocaslFormula :: AParser st C_FORMULA
f <- formula cocasl_reserved_words
return (BoxOrDiamond True m f $ toPos o [] c)
m <- modality [greaterS] -- do not consume matching ">"!
f <- formula cocasl_reserved_words
return (BoxOrDiamond False m f $ toPos o [] c)
modality :: [String] -> AParser st MODALITY
do t <- term (prodS : ks ++ cocasl_reserved_words)
-- put the term in parens if you need to use "*"
option () (asKey prodS >> return ())
-- presence of "*" is not stored yet!
Mixfix_token tok -> Simple_mod tok
instance AParsable C_FORMULA where
cBasic :: AParser st C_BASIC_ITEM
cBasic = do f <- asKey cofreeS
return (codatatypeToCofreetype ti (tokPos f))
<|> do g <- asKey cogeneratedS
do t <- sigItems cocasl_reserved_words
return (CoSort_gen [Annoted t [] [] []] $ tokPos g)
is <- annosParser (sigItems cocasl_reserved_words)
coSigItems :: AParser st C_SIG_ITEM
coSigItems = itemList cocasl_reserved_words cotypeS codatatype CoDatatype_items
codatatype :: [String] -> AParser st CODATATYPE_DECL
(Annoted v _ _ b:as, ps) <- acoAlternative ks `separatedBy` barT
return $ CoDatatype_decl s (Annoted v [] a b:as)
acoAlternative :: [String] -> AParser st (Annoted COALTERNATIVE)
return (Annoted a [] [] an)
coalternative :: [String] -> AParser st COALTERNATIVE
do s <- pluralKeyword sortS
(ts, cs) <- sortId ks `separatedBy` anComma
return (CoSubsorts ts $ catPos $ s:cs)
(cs, ps) <- cocomponent ks `separatedBy` anSemi
return (Co_construct Partial i cs $ qs ++ tokPos q)
<|> return (Co_construct Total i cs qs)
<|> return (Co_construct Total i [] [])
cocomponent :: [String] -> AParser st COCOMPONENTS
do (is, cs) <- parseId ks `separatedBy` anComma
return $ CoSelect is t $ catPos $ cs++[c]
instance AParsable C_SIG_ITEM where
instance AParsable C_BASIC_ITEM where
---- helpers ----------------------------------------------------------------
codatatypeToCofreetype :: C_SIG_ITEM -> [Pos] -> C_BASIC_ITEM
codatatypeToCofreetype d pos =
CoDatatype_items ts ps -> CoFree_datatype ts $ pos ++ ps