Logic_CommonLogic.hs revision 1da120eb84c9d3ed16f64d6defd9bc30569dc45b
d29201dd5328b88140ce050100693c501852657dChristian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
51846950b4b1f31342008cf17f667859a5f21949Christian MaederModule : $Header$
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
75067b1beba1380cde707c30e7fc050d86f6927fKarl Lucimport qualified Data.Map as Map
0ac66bed6456d7900a657269e36107ca7bec4756Iulia Ignatovimport CommonLogic.OMDocImport as OMDocImport
51846950b4b1f31342008cf17f667859a5f21949Christian Maederdata CommonLogic = CommonLogic deriving Show
51846950b4b1f31342008cf17f667859a5f21949Christian Maederinstance Language CommonLogic where
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder description _ = "CommonLogic Logic\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
59ec6aa4da4c93d0d4ef53ed74fdf866d0654539Eugen Kuksa symsOfSen CommonLogic = symsOfTextMeta
59ec6aa4da4c93d0d4ef53ed74fdf866d0654539Eugen Kuksa symKind CommonLogic = Symbol.symKind
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Lucinstance Syntax CommonLogic
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc SYMB_MAP_ITEMS
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc parse_basic_spec CommonLogic = Just basicSpec
037be4e5b0e867dd148db2ea89640d8edf009053Eugen Kuksa parse_symb_items CommonLogic = Just symbItems
037be4e5b0e867dd148db2ea89640d8edf009053Eugen Kuksa parse_symb_map_items CommonLogic = Just 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
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 = ()
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc signature_colimit CommonLogic = ()
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksa-- | Sublogics
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksainstance SemiLatticeWithTop CommonLogicSL where
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksa join = 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