Logic_CoCASL.hs revision 296c6cdef9162217e9d9d1c17790dc71335b8d72
8ff8cb052a588c7a1129f7ed29de7ea2fe6dc435Till MossakowskiModule : $Header$
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
09249711700a6acbc40a2e337688b434d7aafa28Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : hausmann@tzi.de
8ff8cb052a588c7a1129f7ed29de7ea2fe6dc435Till MossakowskiStability : provisional
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederPortability : portable
8ff8cb052a588c7a1129f7ed29de7ea2fe6dc435Till MossakowskiInstance of class Logic for CoCASL.
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maederdata CoCASL = CoCASL deriving Show
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maederinstance Language CoCASL where
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder description _ =
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder "CoCASL is the coalgebraic extension of CASL."
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maedertype CoCASLMor = Morphism C_FORMULA CoCASLSign ()
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maedertype CoCASLFORMULA = FORMULA C_FORMULA
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maederinstance Category CoCASL CSign CoCASLMor
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder -- ide :: id -> object -> morphism
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder ide CoCASL = idMor dummy
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder -- comp :: id -> morphism -> morphism -> Maybe morphism
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder comp CoCASL = compose (const id)
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder -- dom, cod :: id -> morphism -> object
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder dom CoCASL = msource
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder cod CoCASL = mtarget
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder -- legal_obj :: id -> object -> Bool
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder legal_obj CoCASL = legalSign
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder -- legal_mor :: id -> morphism -> Bool
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder legal_mor CoCASL = legalMor
8ff8cb052a588c7a1129f7ed29de7ea2fe6dc435Till Mossakowski-- abstract syntax, parsing (and printing)
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederinstance Syntax CoCASL C_BASIC_SPEC
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder SYMB_ITEMS SYMB_MAP_ITEMS
8ff8cb052a588c7a1129f7ed29de7ea2fe6dc435Till Mossakowski parse_basic_spec CoCASL = Just $ basicSpec cocasl_reserved_words
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder parse_symb_items CoCASL = Just $ symbItems cocasl_reserved_words
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder parse_symb_map_items CoCASL = Just $ symbMapItems cocasl_reserved_words
d48085f765fca838c1d972d2123601997174583dChristian Maeder-- CoCASL logic
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maedermap_C_FORMULA :: MapSen C_FORMULA CoCASLSign ()
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maedermap_C_FORMULA mor frm = case frm of
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder BoxOrDiamond b m f ps -> let
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder newF = mapSen map_C_FORMULA mor f
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder newM = case m of
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder Simple_mod _ -> m
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder Term_mod t -> Term_mod $ mapTerm map_C_FORMULA mor t
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder in BoxOrDiamond b newM newF ps
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maederinstance Sentences CoCASL CoCASLFORMULA () CSign CoCASLMor Symbol where
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder map_sen CoCASL m = return . mapSen map_C_FORMULA m
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder parse_sentence CoCASL = Nothing
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder sym_of CoCASL = symOf
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder symmap_of CoCASL = morphismToSymbMap
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder sym_name CoCASL = symName
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder provers CoCASL = []
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder cons_checkers CoCASL = []
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maederinstance StaticAnalysis CoCASL C_BASIC_SPEC CoCASLFORMULA ()
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder SYMB_ITEMS SYMB_MAP_ITEMS
166d8bced941bf7d4cfab5ce4d326cb1afdc0c4eJonathan von Schroeder Symbol RawSymbol where
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder basic_analysis CoCASL = Just $ basicCoCASLAnalysis
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder stat_symb_map_items CoCASL = statSymbMapItems
54e817678f5e4b2b2a68739bdee19db4afb99b6aChristian Maeder stat_symb_items CoCASL = statSymbItems
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder ensures_amalgamability CoCASL _ =
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder fail "CoCASL: ensures_amalgamability nyi" -- ???
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder sign_to_basic_spec CoCASL _sigma _sens = Basic_spec [] -- ???
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder symbol_to_raw CoCASL = symbolToRaw
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder id_to_raw CoCASL = idToRaw
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder empty_signature CoCASL = emptySign emptyCoCASLSign
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder signature_union CoCASL sigma1 sigma2 =
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder return $ addSig addCoCASLSign sigma1 sigma2
166d8bced941bf7d4cfab5ce4d326cb1afdc0c4eJonathan von Schroeder morphism_union CoCASL = morphismUnion (const id) addCoCASLSign
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder final_union CoCASL = finalUnion addCoCASLSign
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder is_subsig CoCASL = isSubSig isSubCoCASLSign
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder inclusion CoCASL = sigInclusion dummy isSubCoCASLSign
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder cogenerated_sign CoCASL = cogeneratedSign dummy
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder generated_sign CoCASL = generatedSign dummy
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder induced_from_morphism CoCASL = inducedFromMorphism dummy
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder induced_from_to_morphism CoCASL =
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder inducedFromToMorphism dummy isSubCoCASLSign
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder-- lattices (for sublogics)
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maederinstance SemiLatticeWithTop CoCASL_Sublogics where
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maederinstance Logic CoCASL CoCASL_Sublogics
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
166d8bced941bf7d4cfab5ce4d326cb1afdc0c4eJonathan von Schroeder Symbol RawSymbol () where
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder stability _ = Unstable
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder sublogic_names CoCASL = CoCASL.Sublogic.sublogics_name
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder all_sublogics CoCASL = CoCASL.Sublogic.sublogics_all
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder data_logic CoCASL = Nothing
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder is_in_basic_spec CoCASL = CoCASL.Sublogic.in_basic_spec
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder is_in_sentence CoCASL = CoCASL.Sublogic.in_sentence
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder is_in_symb_items CoCASL = CoCASL.Sublogic.in_symb_items
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder is_in_symb_map_items CoCASL = CoCASL.Sublogic.in_symb_map_items
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder is_in_sign CoCASL = CoCASL.Sublogic.in_sign
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder is_in_morphism CoCASL = CoCASL.Sublogic.in_morphism
166d8bced941bf7d4cfab5ce4d326cb1afdc0c4eJonathan von Schroeder is_in_symbol CoCASL = CoCASL.Sublogic.in_symbol
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder min_sublogic_basic_spec CoCASL = CoCASL.Sublogic.sl_basic_spec
8ff8cb052a588c7a1129f7ed29de7ea2fe6dc435Till Mossakowski min_sublogic_sentence CoCASL = CoCASL.Sublogic.sl_sentence
7b83c5b12e33a8917807a169809e3cb922425360Christian Maeder min_sublogic_symb_items CoCASL = CoCASL.Sublogic.sl_symb_items
7b83c5b12e33a8917807a169809e3cb922425360Christian Maeder min_sublogic_symb_map_items CoCASL = CoCASL.Sublogic.sl_symb_map_items
7b83c5b12e33a8917807a169809e3cb922425360Christian Maeder min_sublogic_sign CoCASL = CoCASL.Sublogic.sl_sign
7b83c5b12e33a8917807a169809e3cb922425360Christian Maeder min_sublogic_morphism CoCASL = CoCASL.Sublogic.sl_morphism
8ff8cb052a588c7a1129f7ed29de7ea2fe6dc435Till Mossakowski min_sublogic_symbol CoCASL = CoCASL.Sublogic.sl_symbol
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder proj_sublogic_basic_spec CoCASL = CoCASL.Sublogic.pr_basic_spec
8ff8cb052a588c7a1129f7ed29de7ea2fe6dc435Till Mossakowski proj_sublogic_symb_items CoCASL = CoCASL.Sublogic.pr_symb_items
8ff8cb052a588c7a1129f7ed29de7ea2fe6dc435Till Mossakowski proj_sublogic_symb_map_items CoCASL = CoCASL.Sublogic.pr_symb_map_items
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder proj_sublogic_sign CoCASL = CoCASL.Sublogic.pr_sign
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder proj_sublogic_morphism CoCASL = CoCASL.Sublogic.pr_morphism
8ff8cb052a588c7a1129f7ed29de7ea2fe6dc435Till Mossakowski proj_sublogic_epsilon CoCASL = CoCASL.Sublogic.pr_epsilon dummy
8ff8cb052a588c7a1129f7ed29de7ea2fe6dc435Till Mossakowski proj_sublogic_symbol CoCASL = CoCASL.Sublogic.pr_symbol