Logic_CommonLogic.hs revision 9e5811a3323b00d6ff8d3fe91a185de1ab31150b
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
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
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
0ac66bed6456d7900a657269e36107ca7bec4756Iulia Ignatovimport CommonLogic.OMDocExport
0ac66bed6456d7900a657269e36107ca7bec4756Iulia Ignatovimport CommonLogic.OMDocImport as OMDocImport
0ac66bed6456d7900a657269e36107ca7bec4756Iulia Ignatovimport CommonLogic.OMDoc
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
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
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
0ac66bed6456d7900a657269e36107ca7bec4756Iulia Ignatov 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 = []
0ac66bed6456d7900a657269e36107ca7bec4756Iulia Ignatov
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
0ac66bed6456d7900a657269e36107ca7bec4756Iulia Ignatov
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
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
9e5811a3323b00d6ff8d3fe91a185de1ab31150bChristian Maeder induced_from_morphism CommonLogic = inducedFromMorphism
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc add_symb_to_sign CommonLogic = addSymbToSign -- TODO
9e5811a3323b00d6ff8d3fe91a185de1ab31150bChristian Maeder
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-}