Logic_CommonLogic.hs revision de03ed90ff6efbbc4751301bcf6b50d9790c1afb
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
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Lucimport Common.Id as Id
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
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 GetRange SENTENCE
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Lucinstance Sentences CommonLogic
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc SENTENCE
d6ce032cac688f3698be7133d27f53d3967e6749Christian Maeder Sign
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc Morphism
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Luc Symbol
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Lucinstance Syntax CommonLogic
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc [SENTENCE]
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc ()
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc ()
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maederinstance Logic CommonLogic
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc () -- Sublogics
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Luc [SENTENCE] -- basic_spec
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc SENTENCE -- sentence
d6ce032cac688f3698be7133d27f53d3967e6749Christian Maeder () -- 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
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc [SENTENCE]
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc SENTENCE
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder ()
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