Logic_CommonLogic.hs revision a35bacbc16daf5c10f9accfdfadc4971e9d6f648
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
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 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
66977d201b3ff7ee9c1f992c0f3f701b69eac2c9Karl Lucimport CommonLogic.Morphism
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder
a35bacbc16daf5c10f9accfdfadc4971e9d6f648Iulia Ignatovimport CommonLogic.OMDocExport
a35bacbc16daf5c10f9accfdfadc4971e9d6f648Iulia Ignatovimport 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
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
b696e806e85f1c07f2f5ea07f2b5babcd656e0d6Karl 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
a35bacbc16daf5c10f9accfdfadc4971e9d6f648Iulia Ignatov where
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
a35bacbc16daf5c10f9accfdfadc4971e9d6f648Iulia Ignatov
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
d29201dd5328b88140ce050100693c501852657dChristian Maeder