fd9abdda70912b99b24e3bf1a38f26fde908a74cndCopyright : (c) Till Mossakowski, Wiebke Herding, C. Maeder, Uni Bremen 2004
fd9abdda70912b99b24e3bf1a38f26fde908a74cndLicense : GPLv2 or higher, see LICENSE.txt
f43ed9051a7f4db461d67ed4f7ece175b3dbca7cjerenkrantzMaintainer : luecke@informatik.uni-bremen.de
f43ed9051a7f4db461d67ed4f7ece175b3dbca7cjerenkrantzStability : provisional
f43ed9051a7f4db461d67ed4f7ece175b3dbca7cjerenkrantzPortability : portable
96ad5d81ee4a2cc66a4ae19893efc8aa6d06fae7jailletcParser for modal logic extension of CASL
3b3b7fc78d1f5bfc2769903375050048ff41ff26ndhybrid_reserved_words :: [String]
ad74a0524a06bfe11b7de9e3b4ce7233ab3bd3f7ndhybrid_reserved_words = [
3b3b7fc78d1f5bfc2769903375050048ff41ff26nd flexibleS,
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd modalitiesS,
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndhybridFormula :: AParser st H_FORMULA
f43ed9051a7f4db461d67ed4f7ece175b3dbca7cjerenkrantzhybridFormula =
f43ed9051a7f4db461d67ed4f7ece175b3dbca7cjerenkrantz a <- asKey hereP
e4ca72aa494fed7b6948012734b9c9c098fbba07nd n <- nominal
e4ca72aa494fed7b6948012734b9c9c098fbba07nd return (Here n $ toRange a [] a)
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd a <- asKey asP
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd n <- nominal
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd f <- primFormula hybrid_reserved_words
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd return (At n f $ toRange a [] a)
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd a <- asKey exMark
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd n <- nominal
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd f <- primFormula hybrid_reserved_words
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd return (Univ n f $ toRange a [] a)
99ca75ffd7b9d0e6573ba8858c6e59d4a6d2fa15nd a <- asKey "?"
b12f74e1aaac71d21e4b9a376b31d7307a8d87d8nd n <- nominal
30471a4650391f57975f60bbb6e4a90be7b284bfhumbedooh f <- primFormula hybrid_reserved_words
1f1b6bf13313fdd14a45e52e553d3ff28689b717coar return (Exist n f $ toRange a [] a)
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd o <- oBracketT
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd m <- modality []
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd c <- cBracketT
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd f <- primFormula hybrid_reserved_words
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd return (BoxOrDiamond True m f $ toRange o [] c)
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd o <- asKey lessS
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd m <- modality [greaterS] -- do not consume matching ">"!
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd c <- asKey greaterS
e4ca72aa494fed7b6948012734b9c9c098fbba07nd f <- primFormula hybrid_reserved_words
e4ca72aa494fed7b6948012734b9c9c098fbba07nd return (BoxOrDiamond False m f $ toRange o [] c)
e4ca72aa494fed7b6948012734b9c9c098fbba07ndnominal :: AParser st NOMINAL
e4ca72aa494fed7b6948012734b9c9c098fbba07nd n <- simpleId
e4ca72aa494fed7b6948012734b9c9c098fbba07nd return (Simple_nom n)
e4ca72aa494fed7b6948012734b9c9c098fbba07ndmodality :: [String] -> AParser st MODALITY
e4ca72aa494fed7b6948012734b9c9c098fbba07ndmodality ks =
e4ca72aa494fed7b6948012734b9c9c098fbba07nd do t <- term (ks ++ hybrid_reserved_words)
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd return $ Term_mod t
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrininstance TermParser H_FORMULA where
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin termParser = aToTermParser hybridFormula
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrinrigor :: AParser st RIGOR
7e9d90004f580231e0376880710dc25408950ab9rbowenrigor = (asKey rigidS >> return Rigid)
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin <|> (asKey flexibleS >> return Flexible)
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrinrigidSigItems :: AParser st H_SIG_ITEM
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrinrigidSigItems =
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin do r <- rigor
9da97ff0bac3a0ff56a9cdebe6e5ab563636aa86jailletc itemList hybrid_reserved_words opS opItem (Rigid_op_items r)
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin <|> itemList hybrid_reserved_words predS predItem (Rigid_pred_items r)
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrininstance AParsable H_SIG_ITEM where
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin aparser = rigidSigItems
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrinhKey :: AParser st Token
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrinhKey = asKey modalityS <|> asKey modalitiesS
7e9d90004f580231e0376880710dc25408950ab9rbowenhKey' :: AParser st Token
7e9d90004f580231e0376880710dc25408950ab9rbowenhKey' = asKey nominalS <|> asKey nominalsS
7e9d90004f580231e0376880710dc25408950ab9rbowenhBasic :: AParser st H_BASIC_ITEM
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin do (as, fs, ps) <- hItem'' hKey simpleId
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin return (Simple_mod_decl as fs ps)
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin do (as, fs, ps) <- hItem'' hKey' simpleId
4aa603e6448b99f9371397d439795c91a93637eand return (Simple_nom_decl as fs ps)
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrinhItem'' :: AParser st Token -> AParser st a ->
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin AParser st ([Annoted a], [AnHybFORM], Range)
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrinhItem'' k pr = do
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin (as, cs) <- separatedBy (annoParser pr) anSemiOrComma
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin let ps = catRange $ c : cs
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin return (as, [], ps)
3658293f56f1683ca41e3bc5b70d98b203d8004bcoarinstance AParsable H_BASIC_ITEM where
4aa603e6448b99f9371397d439795c91a93637eand aparser = hBasic