Logic_CommonLogic.hs revision c51d1f5ff88cce030fe543e271ca6b85625b70d8
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder{- |
51846950b4b1f31342008cf17f667859a5f21949Christian MaederModule : $Header$
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl LucDescription : Instance of class Logic for common logic
6d81916b9004f8d9b6032113c5987ab07da47015Karl LucCopyright : (c) Karl Luc, DFKI Bremen 2010
51846950b4b1f31342008cf17f667859a5f21949Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.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 Common.DefaultMorphism
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Lucimport Logic.Logic
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder
51846950b4b1f31342008cf17f667859a5f21949Christian Maederimport ATC.ProofTree ()
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Lucimport CommonLogic.ATC_CommonLogic ()
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Lucimport CommonLogic.Sign
d6ce032cac688f3698be7133d27f53d3967e6749Christian Maederimport CommonLogic.AS_CommonLogic
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Lucimport CommonLogic.Symbol
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Lucimport CommonLogic.Analysis
d75d2d11170f1339ebe37d9d9c06aff148637b13Christian Maederimport CommonLogic.Parse_CLIF
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder
51846950b4b1f31342008cf17f667859a5f21949Christian Maederdata CommonLogic = CommonLogic deriving Show
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder
51846950b4b1f31342008cf17f667859a5f21949Christian Maederinstance Language CommonLogic where
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder description _ = "CommonLogic Logic\n"
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc ++ ""
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder
d6ce032cac688f3698be7133d27f53d3967e6749Christian Maedertype Morphism = DefaultMorphism Sign
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Lucinstance Sentences CommonLogic
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc SENTENCE
d6ce032cac688f3698be7133d27f53d3967e6749Christian Maeder Sign
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc Morphism
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Luc Symbol
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Lucinstance Syntax CommonLogic
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc BASIC_SPEC
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc NAME
d75d2d11170f1339ebe37d9d9c06aff148637b13Christian Maeder () where
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc parse_basic_spec CommonLogic = Just basicSpec
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc -- parse_symb_items CommonLogic = Just symbItems
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc -- parse_symb_map_items CommonLogic = Just symbMapItems
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maederinstance Logic CommonLogic
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc () -- Sublogics
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc BASIC_SPEC -- basic_spec
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc SENTENCE -- sentence
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc NAME -- symb_items
d6ce032cac688f3698be7133d27f53d3967e6749Christian Maeder () -- symb_map_items
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc Sign -- sign
d6ce032cac688f3698be7133d27f53d3967e6749Christian Maeder Morphism -- morphism
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Luc Symbol -- symbol
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Luc Symbol -- raw_symbol
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc () -- proof_tree
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maederinstance StaticAnalysis CommonLogic
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc BASIC_SPEC
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc SENTENCE
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc NAME
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder ()
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
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc