Logic_CommonLogic.hs revision 551f1476dea3f969775527cb15fd512e86279307
d29201dd5328b88140ce050100693c501852657dChristian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder{- |
51846950b4b1f31342008cf17f667859a5f21949Christian MaederModule : $Header$
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl LucDescription : Instance of class Logic for common logic
6d81916b9004f8d9b6032113c5987ab07da47015Karl LucCopyright : (c) Karl Luc, DFKI Bremen 2010
b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuLicense : GPLv2 or higher
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl LucMaintainer : kluc@informatik.uni-bremen.de
51846950b4b1f31342008cf17f667859a5f21949Christian MaederStability : experimental
51846950b4b1f31342008cf17f667859a5f21949Christian MaederPortability : non-portable (imports Logic.Logic)
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl LucInstance of class Logic for the common logic
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder-}
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder
51846950b4b1f31342008cf17f667859a5f21949Christian Maedermodule CommonLogic.Logic_CommonLogic where
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Lucimport Logic.Logic
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder
51846950b4b1f31342008cf17f667859a5f21949Christian Maederimport ATC.ProofTree ()
75067b1beba1380cde707c30e7fc050d86f6927fKarl Lucimport Common.ProofTree
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Lucimport CommonLogic.ATC_CommonLogic ()
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Lucimport CommonLogic.Sign
d6ce032cac688f3698be7133d27f53d3967e6749Christian Maederimport CommonLogic.AS_CommonLogic
75067b1beba1380cde707c30e7fc050d86f6927fKarl Lucimport CommonLogic.Symbol as Symbol
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Lucimport CommonLogic.Analysis
d75d2d11170f1339ebe37d9d9c06aff148637b13Christian Maederimport CommonLogic.Parse_CLIF
66977d201b3ff7ee9c1f992c0f3f701b69eac2c9Karl Lucimport CommonLogic.Morphism
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder
75067b1beba1380cde707c30e7fc050d86f6927fKarl Lucimport qualified Data.Map as Map
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc
551f1476dea3f969775527cb15fd512e86279307Karl Luc-- import CommonLogic.OMDocExport
551f1476dea3f969775527cb15fd512e86279307Karl Luc-- import CommonLogic.OMDocImport
a35bacbc16daf5c10f9accfdfadc4971e9d6f648Iulia Ignatov
51846950b4b1f31342008cf17f667859a5f21949Christian Maederdata CommonLogic = CommonLogic deriving Show
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder
51846950b4b1f31342008cf17f667859a5f21949Christian Maederinstance Language CommonLogic where
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder description _ = "CommonLogic Logic\n"
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc ++ ""
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder
75067b1beba1380cde707c30e7fc050d86f6927fKarl Lucinstance Category Sign Morphism
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc where
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
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Lucinstance Sentences CommonLogic
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc SENTENCE
d6ce032cac688f3698be7133d27f53d3967e6749Christian Maeder Sign
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc Morphism
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Luc Symbol
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc where
551f1476dea3f969775527cb15fd512e86279307Karl Luc negation CommonLogic = Just . negForm
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc 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
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Lucinstance Syntax CommonLogic
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc BASIC_SPEC
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc NAME
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc SYMB_MAP_ITEMS
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc where
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc parse_basic_spec CommonLogic = Just basicSpec
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc parse_symb_items CommonLogic = Nothing -- Just symbItems -- TODO
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc parse_symb_map_items CommonLogic = Nothing -- Just symbMapItems -- TODO
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maederinstance Logic CommonLogic
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc () -- Sublogics
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc BASIC_SPEC -- basic_spec
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc SENTENCE -- sentence
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc NAME -- symb_items
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc SYMB_MAP_ITEMS -- symb_map_items
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc Sign -- sign
d6ce032cac688f3698be7133d27f53d3967e6749Christian Maeder Morphism -- morphism
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Luc Symbol -- symbol
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Luc Symbol -- raw_symbol
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc ProofTree -- proof_tree
551f1476dea3f969775527cb15fd512e86279307Karl Luc where
7b1111ca3b126f71cce47e60ce4b56e6f92422e9Karl Luc empty_proof_tree CommonLogic = emptyProofTree
7b1111ca3b126f71cce47e60ce4b56e6f92422e9Karl Luc provers CommonLogic = []
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc{-
a35bacbc16daf5c10f9accfdfadc4971e9d6f648Iulia Ignatov omdoc_metatheory CommonLogic = Just clMetaTheory
a35bacbc16daf5c10f9accfdfadc4971e9d6f648Iulia Ignatov export_senToOmdoc CommonLogic = exportSenToOmdoc
a35bacbc16daf5c10f9accfdfadc4971e9d6f648Iulia Ignatov export_symToOmdoc CommonLogic = exportSymToOmdoc
a35bacbc16daf5c10f9accfdfadc4971e9d6f648Iulia Ignatov omdocToSen CommonLogic = omdocToSen
a35bacbc16daf5c10f9accfdfadc4971e9d6f648Iulia Ignatov omdocToSym CommonLogic = omdocToSym
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc-}
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maederinstance StaticAnalysis CommonLogic
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc BASIC_SPEC
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc SENTENCE
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc NAME
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc SYMB_MAP_ITEMS
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Luc Sign
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc Morphism
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Luc Symbol
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Luc Symbol
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc where
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Luc basic_analysis CommonLogic = Just basicCommonLogicAnalysis
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Luc empty_signature CommonLogic = emptySig
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Luc is_subsig CommonLogic = isSubSigOf
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc signature_union CommonLogic = sigUnion
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc symbol_to_raw CommonLogic = symbolToRaw
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc id_to_raw CommonLogic = idToRaw
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc matches CommonLogic = Symbol.matches
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc induced_from_morphism CommonLogic = inducedFromMorphism -- TODO
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc induced_from_to_morphism CommonLogic = inducedFromToMorphism -- TODO
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc add_symb_to_sign CommonLogic = addSymbToSign -- TODO
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc{-
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc stat_symb_items CommonLogic = ()
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc stat_symb_map_items CommonLogic = ()
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc morphism_union CommonLogic = ()
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc signature_colimit CommonLogic = ()
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc-}