d29201dd5328b88140ce050100693c501852657dChristian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl LucDescription : Instance of class Logic for common logic
cacbb5e3100fb85d23d1614cace3a8662801f2e6Eugen KuksaCopyright : (c) Karl Luc, DFKI Bremen 2010, Eugen Kuksa and Uni Bremen 2011
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
cacbb5e3100fb85d23d1614cace3a8662801f2e6Eugen KuksaMaintainer : eugenk@informatik.uni-bremen.de
51846950b4b1f31342008cf17f667859a5f21949Christian MaederStability : experimental
51846950b4b1f31342008cf17f667859a5f21949Christian MaederPortability : non-portable (imports Logic.Logic)
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl LucInstance of class Logic for the common logic
75067b1beba1380cde707c30e7fc050d86f6927fKarl Lucimport CommonLogic.Symbol as Symbol
52c81e62d4a3797b926fb3392369b45a9fef336cSoeren D. Schulzeimport qualified CommonLogic.Parse_CLIF as CLIF
52c81e62d4a3797b926fb3392369b45a9fef336cSoeren D. Schulzeimport qualified CommonLogic.Parse_KIF as KIF
d386b61802c70e3d220d4520d9fcdefbd9c469f4Soeren D. Schulzeimport qualified CommonLogic.Print_KIF as Print_KIF
0ac66bed6456d7900a657269e36107ca7bec4756Iulia Ignatovimport CommonLogic.OMDocImport as OMDocImport
e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maederimport qualified Data.Map as Map
51846950b4b1f31342008cf17f667859a5f21949Christian Maederdata CommonLogic = CommonLogic deriving Show
51846950b4b1f31342008cf17f667859a5f21949Christian Maederinstance Language CommonLogic where
602041e384342ea908c976a298e8b47774d3500cTill Mossakowski description _ = "CommonLogic (an ISO standard)\n"
75067b1beba1380cde707c30e7fc050d86f6927fKarl Lucinstance Category Sign Morphism
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc ide = idMor
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc dom = source
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc cod = target
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc isInclusion = Map.null . propMap
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc legal_mor = isLegalMorphism
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc composeMorphisms = composeMor
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Lucinstance Sentences CommonLogic
551f1476dea3f969775527cb15fd512e86279307Karl Luc negation CommonLogic = Just . negForm
9e5811a3323b00d6ff8d3fe91a185de1ab31150bChristian Maeder sym_of CommonLogic = singletonList . symOf
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc symmap_of CommonLogic = getSymbolMap -- returns the symbol map
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc sym_name CommonLogic = getSymbolName -- returns the name of a symbol
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc map_sen CommonLogic = mapSentence -- TODO
a7338b15cbc9b513aaded07198c8666f0fa9d612Till Mossakowski symsOfSen CommonLogic _ = symsOfTextMeta
59ec6aa4da4c93d0d4ef53ed74fdf866d0654539Eugen Kuksa symKind CommonLogic = Symbol.symKind
e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maederinstance Monoid BASIC_SPEC where
e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder mempty = Basic_spec []
e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder mappend (Basic_spec l1) (Basic_spec l2) = Basic_spec $ l1 ++ l2
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Lucinstance Syntax CommonLogic
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc SYMB_MAP_ITEMS
0b282d1269b8f9a658f7ce9090575ba1b00e8d66Christian Maeder parsersAndPrinters CommonLogic =
d386b61802c70e3d220d4520d9fcdefbd9c469f4Soeren D. Schulze addSyntax "KIF" (KIF.basicSpec, Print_KIF.printBasicSpec)
0b282d1269b8f9a658f7ce9090575ba1b00e8d66Christian Maeder $ addSyntax "CLIF" (CLIF.basicSpec, pretty)
0b282d1269b8f9a658f7ce9090575ba1b00e8d66Christian Maeder $ makeDefault (CLIF.basicSpec, pretty)
52c81e62d4a3797b926fb3392369b45a9fef336cSoeren D. Schulze parse_symb_items CommonLogic = Just CLIF.symbItems
52c81e62d4a3797b926fb3392369b45a9fef336cSoeren D. Schulze parse_symb_map_items CommonLogic = Just CLIF.symbMapItems
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maederinstance Logic CommonLogic
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksa CommonLogicSL -- Sublogics
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc BASIC_SPEC -- basic_spec
1ea7fb6b0f66210bc0d3cb995f1b655277b33884Eugen Kuksa TEXT_META -- sentence
037be4e5b0e867dd148db2ea89640d8edf009053Eugen Kuksa SYMB_ITEMS -- symb_items
2c10bceb28a74fc291959697e023f22a66753655Eugen Kuksa SYMB_MAP_ITEMS -- symb_map_items
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc Sign -- sign
d6ce032cac688f3698be7133d27f53d3967e6749Christian Maeder Morphism -- morphism
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Luc Symbol -- symbol
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Luc Symbol -- raw_symbol
cacbb5e3100fb85d23d1614cace3a8662801f2e6Eugen Kuksa ProofTree -- proof_tree
cdcf5d3f1e79d8798d77efa29e6193af94ea0604Till Mossakowski stability CommonLogic = Stable
5e6915f767bd46767306abbfbb39ebcbc10a2a33Christian Maeder all_sublogics CommonLogic = sublogics_all
7b1111ca3b126f71cce47e60ce4b56e6f92422e9Karl Luc empty_proof_tree CommonLogic = emptyProofTree
7b1111ca3b126f71cce47e60ce4b56e6f92422e9Karl Luc provers CommonLogic = []
0ac66bed6456d7900a657269e36107ca7bec4756Iulia Ignatov omdoc_metatheory CommonLogic = Just clMetaTheory
0ac66bed6456d7900a657269e36107ca7bec4756Iulia Ignatov export_senToOmdoc CommonLogic = exportSenToOmdoc
0ac66bed6456d7900a657269e36107ca7bec4756Iulia Ignatov export_symToOmdoc CommonLogic = exportSymToOmdoc
0ac66bed6456d7900a657269e36107ca7bec4756Iulia Ignatov omdocToSen CommonLogic = OMDocImport.omdocToSen
0ac66bed6456d7900a657269e36107ca7bec4756Iulia Ignatov omdocToSym CommonLogic = OMDocImport.omdocToSym
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maederinstance StaticAnalysis CommonLogic
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc SYMB_MAP_ITEMS
9e5811a3323b00d6ff8d3fe91a185de1ab31150bChristian Maeder basic_analysis CommonLogic = Just basicCommonLogicAnalysis
9e5811a3323b00d6ff8d3fe91a185de1ab31150bChristian Maeder empty_signature CommonLogic = emptySig
9e5811a3323b00d6ff8d3fe91a185de1ab31150bChristian Maeder is_subsig CommonLogic = isSubSigOf
9e5811a3323b00d6ff8d3fe91a185de1ab31150bChristian Maeder subsig_inclusion CommonLogic s = return . inclusionMap s
9e5811a3323b00d6ff8d3fe91a185de1ab31150bChristian Maeder signature_union CommonLogic = sigUnion
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc symbol_to_raw CommonLogic = symbolToRaw
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc id_to_raw CommonLogic = idToRaw
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc matches CommonLogic = Symbol.matches
c96c73387a0c41614ba325f737edad6abbf07e79Eugen Kuksa stat_symb_items CommonLogic _ = mkStatSymbItems
c96c73387a0c41614ba325f737edad6abbf07e79Eugen Kuksa stat_symb_map_items CommonLogic _ _ = mkStatSymbMapItem
9e5811a3323b00d6ff8d3fe91a185de1ab31150bChristian Maeder induced_from_morphism CommonLogic = inducedFromMorphism
1da120eb84c9d3ed16f64d6defd9bc30569dc45bChristian Maeder induced_from_to_morphism CommonLogic = inducedFromToMorphism
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc add_symb_to_sign CommonLogic = addSymbToSign -- TODO
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc stat_symb_items CommonLogic = ()
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc stat_symb_map_items CommonLogic = ()
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc morphism_union CommonLogic = ()
40988f50f3e378a38ab97702f6cc69fc7f43be6fmcodescu signature_colimit CommonLogic = signColimit
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksa-- | Sublogics
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksainstance SemiLatticeWithTop CommonLogicSL where
8c7aa750542dcadb94b971be712564a9a8f1d189Christian Maeder lub = sublogics_max
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksainstance MinSublogic CommonLogicSL BASIC_SPEC where
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksa minSublogic = sl_basic_spec bottom
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksainstance MinSublogic CommonLogicSL Sign where
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksa minSublogic = sl_sig bottom
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksainstance SublogicName CommonLogicSL where
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksa sublogicName = sublogics_name
1ea7fb6b0f66210bc0d3cb995f1b655277b33884Eugen Kuksainstance MinSublogic CommonLogicSL TEXT_META where
1ea7fb6b0f66210bc0d3cb995f1b655277b33884Eugen Kuksa minSublogic tm = sublogic_text bottom $ getText tm
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksainstance MinSublogic CommonLogicSL NAME where
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksa minSublogic = sublogic_name bottom
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksainstance MinSublogic CommonLogicSL Symbol where
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksa minSublogic = sl_sym bottom
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksainstance MinSublogic CommonLogicSL Morphism where
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksa minSublogic = sl_mor bottom
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksainstance MinSublogic CommonLogicSL SYMB_MAP_ITEMS where
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksa minSublogic = sl_symmap bottom
037be4e5b0e867dd148db2ea89640d8edf009053Eugen Kuksainstance MinSublogic CommonLogicSL SYMB_ITEMS where
037be4e5b0e867dd148db2ea89640d8edf009053Eugen Kuksa minSublogic = sl_symitems bottom
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksainstance ProjectSublogic CommonLogicSL BASIC_SPEC where
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksa projectSublogic = prBasicSpec
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksainstance ProjectSublogicM CommonLogicSL NAME where
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksa projectSublogicM = prName
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksainstance ProjectSublogicM CommonLogicSL SYMB_MAP_ITEMS where
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksa projectSublogicM = prSymMapM
037be4e5b0e867dd148db2ea89640d8edf009053Eugen Kuksainstance ProjectSublogicM CommonLogicSL SYMB_ITEMS where
037be4e5b0e867dd148db2ea89640d8edf009053Eugen Kuksa projectSublogicM = prSymItemsM
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksainstance ProjectSublogic CommonLogicSL Sign where
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksa projectSublogic = prSig
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksainstance ProjectSublogic CommonLogicSL Morphism where
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksa projectSublogic = prMor
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksainstance ProjectSublogicM CommonLogicSL Symbol where
5e6915f767bd46767306abbfbb39ebcbc10a2a33Christian Maeder projectSublogicM = prSymbolM