Logic_CoCASL.hs revision 03136b84a0c70d877e227444f0875e209506b9e4
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder{- |
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian MaederModule : $Header$
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian MaederDescription : Instance of class Logic for CoCASL
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian MaederMaintainer : hausmann@informatik.uni-bremen.de
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian MaederStability : provisional
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian MaederPortability : portable
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian MaederInstance of class Logic for CoCASL.
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder-}
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maedermodule CoCASL.Logic_CoCASL where
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maederimport CoCASL.AS_CoCASL
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maederimport CoCASL.CoCASLSign
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maederimport CoCASL.ATC_CoCASL()
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maederimport CoCASL.Parse_AS
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maederimport CoCASL.StatAna
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maederimport CoCASL.Sublogic
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maederimport CASL.Sign
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maederimport CASL.Morphism
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maederimport CASL.SymbolMapAnalysis
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maederimport CASL.Logic_CASL
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maederimport CASL.AS_Basic_CASL
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maederimport CASL.Parse_AS_Basic
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maederimport CASL.MapSentence
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maederimport CASL.SymbolParser
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maederimport CASL.Sublogic
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maederimport Logic.Logic
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maederdata CoCASL = CoCASL deriving Show
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maederinstance Language CoCASL where
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder description _ =
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder "CoCASL is the coalgebraic extension of CASL."
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maedertype CoCASLMor = Morphism C_FORMULA CoCASLSign ()
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maedertype CoCASLFORMULA = FORMULA C_FORMULA
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maederinstance Category CoCASL CSign CoCASLMor
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder where
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder -- ide :: id -> object -> morphism
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maeder ide CoCASL = idMor ()
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maeder -- comp :: id -> morphism -> morphism -> Maybe morphism
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maeder comp CoCASL = compose (const id)
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder -- dom, cod :: id -> morphism -> object
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder dom CoCASL = msource
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder cod CoCASL = mtarget
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maeder -- legal_obj :: id -> object -> Bool
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder legal_obj CoCASL = legalSign
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder -- legal_mor :: id -> morphism -> Bool
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder legal_mor CoCASL = legalMor
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder-- abstract syntax, parsing (and printing)
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maederinstance Syntax CoCASL C_BASIC_SPEC
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder SYMB_ITEMS SYMB_MAP_ITEMS
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maeder where
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maeder parse_basic_spec CoCASL = Just $ basicSpec cocasl_reserved_words
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder parse_symb_items CoCASL = Just $ symbItems cocasl_reserved_words
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder parse_symb_map_items CoCASL =
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder Just $ symbMapItems cocasl_reserved_words
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder-- CoCASL logic
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maedermap_C_FORMULA :: MapSen C_FORMULA CoCASLSign ()
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maedermap_C_FORMULA mor frm = case frm of
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder BoxOrDiamond b m f ps -> let
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder newF = mapSen map_C_FORMULA mor f
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder newM = case m of
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maeder Simple_mod _ -> m
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder Term_mod t -> Term_mod $ mapTerm map_C_FORMULA mor t
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder in BoxOrDiamond b newM newF ps
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder phi -> phi
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maederinstance Sentences CoCASL CoCASLFORMULA CSign CoCASLMor Symbol where
9a6861ccf8fce8d034ef0810a09e7abdf8d2fc94Christian Maeder map_sen CoCASL m = return . mapSen map_C_FORMULA m
9a6861ccf8fce8d034ef0810a09e7abdf8d2fc94Christian Maeder parse_sentence CoCASL = Nothing
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maeder sym_of CoCASL = symOf
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder symmap_of CoCASL = morphismToSymbMap
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder sym_name CoCASL = symName
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maederinstance StaticAnalysis CoCASL C_BASIC_SPEC CoCASLFORMULA
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maeder SYMB_ITEMS SYMB_MAP_ITEMS
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder CSign
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder CoCASLMor
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maeder Symbol RawSymbol where
9a6861ccf8fce8d034ef0810a09e7abdf8d2fc94Christian Maeder basic_analysis CoCASL = Just $ basicCoCASLAnalysis
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maeder stat_symb_map_items CoCASL = statSymbMapItems
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maeder stat_symb_items CoCASL = statSymbItems
9a6861ccf8fce8d034ef0810a09e7abdf8d2fc94Christian Maeder ensures_amalgamability CoCASL _ =
9a6861ccf8fce8d034ef0810a09e7abdf8d2fc94Christian Maeder fail "CoCASL: ensures_amalgamability nyi" -- ???
9a6861ccf8fce8d034ef0810a09e7abdf8d2fc94Christian Maeder
9a6861ccf8fce8d034ef0810a09e7abdf8d2fc94Christian Maeder sign_to_basic_spec CoCASL _sigma _sens = Basic_spec [] -- ???
9a6861ccf8fce8d034ef0810a09e7abdf8d2fc94Christian Maeder
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder symbol_to_raw CoCASL = symbolToRaw
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder id_to_raw CoCASL = idToRaw
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder matches CoCASL = CASL.Morphism.matches
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder empty_signature CoCASL = emptySign emptyCoCASLSign
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder signature_union CoCASL sigma1 sigma2 =
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder return $ addSig addCoCASLSign sigma1 sigma2
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder morphism_union CoCASL = morphismUnion (const id) addCoCASLSign
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder final_union CoCASL = finalUnion addCoCASLSign
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maeder is_subsig CoCASL = isSubSig isSubCoCASLSign
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder inclusion CoCASL = sigInclusion () isSubCoCASLSign
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder cogenerated_sign CoCASL = cogeneratedSign ()
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder generated_sign CoCASL = generatedSign ()
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder induced_from_morphism CoCASL = inducedFromMorphism ()
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder induced_from_to_morphism CoCASL =
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder inducedFromToMorphism () isSubCoCASLSign
7346dce678f0786a8faed1d83bdea2bd79dcc65eChristian Maeder
7346dce678f0786a8faed1d83bdea2bd79dcc65eChristian Maederinstance NameSL Bool where
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder nameSL b = if b then "Co" else ""
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maederinstance MinSL Bool C_FORMULA where
minSL = minFormSublogic
instance MinSL Bool C_SIG_ITEM where
minSL = minCSigItem
instance MinSL Bool C_BASIC_ITEM where
minSL = minCBaseItem
instance ProjForm Bool C_FORMULA where
projForm _ f = Just $ ExtFORMULA f
instance ProjSigItem Bool C_SIG_ITEM C_FORMULA where
projSigItems _ s = (Just $ Ext_SIG_ITEMS s, [])
instance ProjBasic Bool C_BASIC_ITEM C_SIG_ITEM C_FORMULA where
projBasicItems _ b = (Just $ Ext_BASIC_ITEMS b, [])
instance Logic CoCASL CoCASL_Sublogics
C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
CSign
CoCASLMor
Symbol RawSymbol () where
stability _ = Unstable
proj_sublogic_epsilon CoCASL = pr_epsilon ()
all_sublogics _ = sublogics_all [False, True]
empty_proof_tree _ = ()