hets/CoCASL/Logic_CoCASL.hs

	Logic_CoCASL.hs revision 86d6f1795b6f7fc170de133766ac7a68a5a6b7ab
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina{- |
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel BřezinaModule      :  $Header$
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel BřezinaCopyright   :  (c) Till Mossakowski, Uni Bremen 2002-2004
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel BřezinaLicense     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel BřezinaMaintainer  :  hausmann@tzi.de
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel BřezinaStability   :  provisional
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel BřezinaPortability :  portable
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel BřezinaInstance of class Logic for CoCASL.
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina-}
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina{- todo:
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina-}
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinamodule CoCASL.Logic_CoCASL where
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinaimport CoCASL.AS_CoCASL
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinaimport CoCASL.CoCASLSign
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinaimport CoCASL.ATC_CoCASL()
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinaimport CoCASL.Parse_AS
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinaimport CoCASL.StatAna
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinaimport CoCASL.Sublogic
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinaimport CASL.Sign
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinaimport CASL.Morphism
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinaimport CASL.SymbolMapAnalysis
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinaimport CASL.Logic_CASL
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinaimport CASL.AS_Basic_CASL
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinaimport CASL.Parse_AS_Basic
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinaimport CASL.MapSentence
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinaimport CASL.SymbolParser
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinaimport Logic.Logic
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinadata CoCASL = CoCASL deriving Show
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinainstance Language CoCASL  where
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina description _ =
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina  "CoCASL is the coalgebraic extension of CASL."
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinatype CoCASLMor = Morphism C_FORMULA CoCASLSign ()
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinatype CoCASLFORMULA = FORMULA C_FORMULA
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinainstance Category CoCASL CSign CoCASLMor
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina    where
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         -- ide :: id -> object -> morphism
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         ide CoCASL = idMor dummy
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         -- comp :: id -> morphism -> morphism -> Maybe morphism
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         comp CoCASL = compose (const id)
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         -- dom, cod :: id -> morphism -> object
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         dom CoCASL = msource
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         cod CoCASL = mtarget
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         -- legal_obj :: id -> object -> Bool
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         legal_obj CoCASL = legalSign
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         -- legal_mor :: id -> morphism -> Bool
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         legal_mor CoCASL = legalMor
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina-- abstract syntax, parsing (and printing)
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinainstance Syntax CoCASL C_BASIC_SPEC
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina                SYMB_ITEMS SYMB_MAP_ITEMS
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina      where
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         parse_basic_spec CoCASL = Just $ basicSpec cocasl_reserved_words
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         parse_symb_items CoCASL = Just $ symbItems cocasl_reserved_words
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         parse_symb_map_items CoCASL = Just $ symbMapItems cocasl_reserved_words
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina-- CoCASL logic
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinamap_C_FORMULA :: MapSen C_FORMULA CoCASLSign ()
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinamap_C_FORMULA mor frm = case frm of
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina           BoxOrDiamond b m f ps -> let
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina              newF = mapSen map_C_FORMULA mor f
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina              newM = case m of
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina                   Simple_mod _ ->  m
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina                   Term_mod t -> Term_mod $ mapTerm map_C_FORMULA mor t
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina              in BoxOrDiamond b newM newF ps
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina           phi -> phi
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinainstance Sentences CoCASL CoCASLFORMULA () CSign CoCASLMor Symbol where
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina      map_sen CoCASL m = return . mapSen map_C_FORMULA m
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina      parse_sentence CoCASL = Nothing
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina      sym_of CoCASL = symOf
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina      symmap_of CoCASL = morphismToSymbMap
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina      sym_name CoCASL = symName
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina      provers CoCASL = []
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina      cons_checkers CoCASL = []
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinainstance StaticAnalysis CoCASL C_BASIC_SPEC CoCASLFORMULA ()
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina               SYMB_ITEMS SYMB_MAP_ITEMS
15f3e53e7ab9285afbebc8e2ec4d6d4577fef3daPavel Březina               CSign
15f3e53e7ab9285afbebc8e2ec4d6d4577fef3daPavel Březina               CoCASLMor
15f3e53e7ab9285afbebc8e2ec4d6d4577fef3daPavel Březina               Symbol RawSymbol where
15f3e53e7ab9285afbebc8e2ec4d6d4577fef3daPavel Březina         basic_analysis CoCASL = Just $ basicCoCASLAnalysis
15f3e53e7ab9285afbebc8e2ec4d6d4577fef3daPavel Březina         stat_symb_map_items CoCASL = statSymbMapItems
15f3e53e7ab9285afbebc8e2ec4d6d4577fef3daPavel Březina         stat_symb_items CoCASL = statSymbItems
15f3e53e7ab9285afbebc8e2ec4d6d4577fef3daPavel Březina         ensures_amalgamability CoCASL _ =
15f3e53e7ab9285afbebc8e2ec4d6d4577fef3daPavel Březina             fail "CoCASL: ensures_amalgamability nyi" -- ???
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         sign_to_basic_spec CoCASL _sigma _sens = Basic_spec [] -- ???
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         symbol_to_raw CoCASL = symbolToRaw
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         id_to_raw CoCASL = idToRaw
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         matches CoCASL = CASL.Morphism.matches
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         empty_signature CoCASL = emptySign emptyCoCASLSign
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         signature_union CoCASL sigma1 sigma2 =
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina           return $ addSig addCoCASLSign sigma1 sigma2
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         morphism_union CoCASL = morphismUnion (const id) addCoCASLSign
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         final_union CoCASL = finalUnion addCoCASLSign
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         is_subsig CoCASL = isSubSig isSubCoCASLSign
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         inclusion CoCASL = sigInclusion dummy isSubCoCASLSign
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         cogenerated_sign CoCASL = cogeneratedSign dummy
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         generated_sign CoCASL = generatedSign dummy
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         induced_from_morphism CoCASL = inducedFromMorphism dummy
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         induced_from_to_morphism CoCASL =
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina             inducedFromToMorphism dummy isSubCoCASLSign
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina-- lattices (for sublogics)
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinainstance SemiLatticeWithTop CoCASL_Sublogics where
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina    join = CoCASL.Sublogic.sublogics_max
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina    top = CoCASL.Sublogic.top
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březinainstance Logic CoCASL CoCASL_Sublogics
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina               C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina               CSign
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina               CoCASLMor
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina               Symbol RawSymbol () where
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         stability _ = Unstable
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         sublogic_names CoCASL = CoCASL.Sublogic.sublogics_name
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         all_sublogics CoCASL = CoCASL.Sublogic.sublogics_all
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         data_logic CoCASL = Nothing
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         is_in_basic_spec CoCASL = CoCASL.Sublogic.in_basic_spec
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         is_in_sentence CoCASL = CoCASL.Sublogic.in_sentence
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         is_in_symb_items CoCASL = CoCASL.Sublogic.in_symb_items
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         is_in_symb_map_items CoCASL = CoCASL.Sublogic.in_symb_map_items
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         is_in_sign CoCASL = CoCASL.Sublogic.in_sign
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         is_in_morphism CoCASL = CoCASL.Sublogic.in_morphism
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         is_in_symbol CoCASL = CoCASL.Sublogic.in_symbol
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         min_sublogic_basic_spec CoCASL = CoCASL.Sublogic.sl_basic_spec
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         min_sublogic_sentence CoCASL = CoCASL.Sublogic.sl_sentence
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         min_sublogic_symb_items CoCASL = CoCASL.Sublogic.sl_symb_items
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         min_sublogic_symb_map_items CoCASL = CoCASL.Sublogic.sl_symb_map_items
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         min_sublogic_sign CoCASL = CoCASL.Sublogic.sl_sign
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         min_sublogic_morphism CoCASL = CoCASL.Sublogic.sl_morphism
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         min_sublogic_symbol CoCASL = CoCASL.Sublogic.sl_symbol
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         proj_sublogic_basic_spec CoCASL = CoCASL.Sublogic.pr_basic_spec
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         proj_sublogic_symb_items CoCASL = CoCASL.Sublogic.pr_symb_items
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         proj_sublogic_symb_map_items CoCASL = CoCASL.Sublogic.pr_symb_map_items
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         proj_sublogic_sign CoCASL = CoCASL.Sublogic.pr_sign
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         proj_sublogic_morphism CoCASL = CoCASL.Sublogic.pr_morphism
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         proj_sublogic_epsilon CoCASL = CoCASL.Sublogic.pr_epsilon dummy
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina         proj_sublogic_symbol CoCASL = CoCASL.Sublogic.pr_symbol
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina
d0599eaa9369fd867953e3c58b8d7bb445525ff5Pavel Březina