Logic_CommonLogic.hs revision 40988f50f3e378a38ab97702f6cc69fc7f43be6f
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersen{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersen{- |
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom GundersenModule : $Header$
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom GundersenDescription : Instance of class Logic for common logic
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom GundersenCopyright : (c) Karl Luc, DFKI Bremen 2010, Eugen Kuksa and Uni Bremen 2011
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom GundersenLicense : GPLv2 or higher, see LICENSE.txt
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersen
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom GundersenMaintainer : eugenk@informatik.uni-bremen.de
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom GundersenStability : experimental
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom GundersenPortability : non-portable (imports Logic.Logic)
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersen
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom GundersenInstance of class Logic for the common logic
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersen-}
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersen
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersenmodule CommonLogic.Logic_CommonLogic where
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersen
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersenimport ATC.ProofTree ()
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersen
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersenimport Common.ProofTree
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersen
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersenimport CommonLogic.ATC_CommonLogic ()
d3cf48f4bd3d69a276f17aa7c910e0b35215cabaLennart Poetteringimport CommonLogic.Sign
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersenimport CommonLogic.AS_CommonLogic
a553fd32d14739b746a05ae502b8acc38e5f9a50Tom Gundersenimport CommonLogic.Symbol as Symbol
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersenimport CommonLogic.Analysis
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersenimport qualified CommonLogic.Parse_CLIF as CLIF
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersenimport qualified CommonLogic.Parse_KIF as KIF
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersenimport qualified CommonLogic.Print_KIF as Print_KIF
e877666c1553a3dd5b05b4c48090f889ffc079e6Patrik Flyktimport CommonLogic.Morphism
d3cf48f4bd3d69a276f17aa7c910e0b35215cabaLennart Poetteringimport CommonLogic.OMDocExport
d3cf48f4bd3d69a276f17aa7c910e0b35215cabaLennart Poetteringimport CommonLogic.OMDocImport as OMDocImport
d3cf48f4bd3d69a276f17aa7c910e0b35215cabaLennart Poetteringimport CommonLogic.OMDoc
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersenimport CommonLogic.Sublogic
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersen
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersenimport qualified Data.Map as Map
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersenimport Data.Monoid
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersen
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersenimport Logic.Logic
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersen
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersendata CommonLogic = CommonLogic deriving Show
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersen
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gunderseninstance Language CommonLogic where
4b6141c42497dc199618f95fa3f359615eecfaa0Tom Gundersen description _ = "CommonLogic Logic\n"
4b6141c42497dc199618f95fa3f359615eecfaa0Tom Gundersen
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gunderseninstance Category Sign Morphism
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersen where
d3cf48f4bd3d69a276f17aa7c910e0b35215cabaLennart Poettering ide = idMor
d3cf48f4bd3d69a276f17aa7c910e0b35215cabaLennart Poettering dom = source
da927ba997d68401563b927f92e6e40e021a8e5cMichal Schmidt cod = target
d3cf48f4bd3d69a276f17aa7c910e0b35215cabaLennart Poettering isInclusion = Map.null . propMap
d3cf48f4bd3d69a276f17aa7c910e0b35215cabaLennart Poettering legal_mor = isLegalMorphism
d3cf48f4bd3d69a276f17aa7c910e0b35215cabaLennart Poettering composeMorphisms = composeMor
fe8db0c5ee3365a2fc80ee7ebffa238f9a0a2ae2Tom Gundersen
fe8db0c5ee3365a2fc80ee7ebffa238f9a0a2ae2Tom Gunderseninstance Sentences CommonLogic
85b5673b337048fa881a5afb1d00d1a7b95950fbTom Gundersen TEXT_META
0ea51a1129b9984a3c6d96cef1b0e33c99b5e9cfTom Gundersen Sign
c33b329709ebe2755181980a050d02ec7c81ed87Michal Schmidt Morphism
0ea51a1129b9984a3c6d96cef1b0e33c99b5e9cfTom Gundersen Symbol
85b5673b337048fa881a5afb1d00d1a7b95950fbTom Gundersen where
0ea51a1129b9984a3c6d96cef1b0e33c99b5e9cfTom Gundersen negation CommonLogic = Just . negForm
c33b329709ebe2755181980a050d02ec7c81ed87Michal Schmidt sym_of CommonLogic = singletonList . symOf
0ea51a1129b9984a3c6d96cef1b0e33c99b5e9cfTom Gundersen symmap_of CommonLogic = getSymbolMap -- returns the symbol map
85b5673b337048fa881a5afb1d00d1a7b95950fbTom Gundersen sym_name CommonLogic = getSymbolName -- returns the name of a symbol
0ea51a1129b9984a3c6d96cef1b0e33c99b5e9cfTom Gundersen map_sen CommonLogic = mapSentence -- TODO
c33b329709ebe2755181980a050d02ec7c81ed87Michal Schmidt symsOfSen CommonLogic = symsOfTextMeta
fe8db0c5ee3365a2fc80ee7ebffa238f9a0a2ae2Tom Gundersen symKind CommonLogic = Symbol.symKind
49699bac94d24b444274f91f85c82e6fad04d029Susant Sahani
49699bac94d24b444274f91f85c82e6fad04d029Susant Sahaniinstance Monoid BASIC_SPEC where
49699bac94d24b444274f91f85c82e6fad04d029Susant Sahani mempty = Basic_spec []
49699bac94d24b444274f91f85c82e6fad04d029Susant Sahani mappend (Basic_spec l1) (Basic_spec l2) = Basic_spec $ l1 ++ l2
49699bac94d24b444274f91f85c82e6fad04d029Susant Sahani
49699bac94d24b444274f91f85c82e6fad04d029Susant Sahaniinstance Syntax CommonLogic
d3cf48f4bd3d69a276f17aa7c910e0b35215cabaLennart Poettering BASIC_SPEC
d3cf48f4bd3d69a276f17aa7c910e0b35215cabaLennart Poettering Symbol
d3cf48f4bd3d69a276f17aa7c910e0b35215cabaLennart Poettering SYMB_ITEMS
d3cf48f4bd3d69a276f17aa7c910e0b35215cabaLennart Poettering SYMB_MAP_ITEMS
bddfc8afd329ac68a23f66a3512d4e249af25191Tom Gundersen where
d3cf48f4bd3d69a276f17aa7c910e0b35215cabaLennart Poettering parsersAndPrinters CommonLogic =
d3cf48f4bd3d69a276f17aa7c910e0b35215cabaLennart Poettering addSyntax "KIF" (KIF.basicSpec, Print_KIF.printBasicSpec)
d3cf48f4bd3d69a276f17aa7c910e0b35215cabaLennart Poettering $ addSyntax "CLIF" (CLIF.basicSpec, pretty)
186fe1db20902b6542cee58ba499ced914d687a8Lennart Poettering $ makeDefault (CLIF.basicSpec, pretty)
186fe1db20902b6542cee58ba499ced914d687a8Lennart Poettering parse_symb_items CommonLogic = Just CLIF.symbItems
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersen parse_symb_map_items CommonLogic = Just CLIF.symbMapItems
1f6d9bc9ee894d4023b7eacea1754986f25bce57Tom Gundersen
da927ba997d68401563b927f92e6e40e021a8e5cMichal Schmidtinstance Logic CommonLogic
4b6141c42497dc199618f95fa3f359615eecfaa0Tom Gundersen CommonLogicSL -- Sublogics
1f6d9bc9ee894d4023b7eacea1754986f25bce57Tom Gundersen BASIC_SPEC -- basic_spec
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersen TEXT_META -- sentence
f0c4cd7a2c2835a392b5b1807d8c506ab0af44deTom Gundersen SYMB_ITEMS -- symb_items
1f6d9bc9ee894d4023b7eacea1754986f25bce57Tom Gundersen SYMB_MAP_ITEMS -- symb_map_items
da927ba997d68401563b927f92e6e40e021a8e5cMichal Schmidt Sign -- sign
4b6141c42497dc199618f95fa3f359615eecfaa0Tom Gundersen Morphism -- morphism
1f6d9bc9ee894d4023b7eacea1754986f25bce57Tom Gundersen Symbol -- symbol
3bef724f7e7f7eaca69881548b06e221b77d7031Tom Gundersen Symbol -- raw_symbol
505f8da7325591defe5f751f328bd26915267602Tom Gundersen ProofTree -- proof_tree
1346b1f0388f4100bb3c2a2bb23bc881769c020cTom Gundersen where
da927ba997d68401563b927f92e6e40e021a8e5cMichal Schmidt stability CommonLogic = Testing
1346b1f0388f4100bb3c2a2bb23bc881769c020cTom Gundersen all_sublogics CommonLogic = sublogics_all
1346b1f0388f4100bb3c2a2bb23bc881769c020cTom Gundersen empty_proof_tree CommonLogic = emptyProofTree
1346b1f0388f4100bb3c2a2bb23bc881769c020cTom Gundersen provers CommonLogic = []
45af44d47da6933b260c734ad9ff721f63f80a4dTom Gundersen omdoc_metatheory CommonLogic = Just clMetaTheory
45af44d47da6933b260c734ad9ff721f63f80a4dTom Gundersen export_senToOmdoc CommonLogic = exportSenToOmdoc
45af44d47da6933b260c734ad9ff721f63f80a4dTom Gundersen export_symToOmdoc CommonLogic = exportSymToOmdoc
45af44d47da6933b260c734ad9ff721f63f80a4dTom Gundersen omdocToSen CommonLogic = OMDocImport.omdocToSen
45af44d47da6933b260c734ad9ff721f63f80a4dTom Gundersen omdocToSym CommonLogic = OMDocImport.omdocToSym
45af44d47da6933b260c734ad9ff721f63f80a4dTom Gundersen
73432d67b590c8c8954cf2f8954d174a55d58c7bTom Gundersen
73432d67b590c8c8954cf2f8954d174a55d58c7bTom Gunderseninstance StaticAnalysis CommonLogic
4b6141c42497dc199618f95fa3f359615eecfaa0Tom Gundersen BASIC_SPEC
4b6141c42497dc199618f95fa3f359615eecfaa0Tom Gundersen TEXT_META
4b6141c42497dc199618f95fa3f359615eecfaa0Tom Gundersen SYMB_ITEMS
f882c247ad59776c3a7753bb963c1f8e2386cb79Tom Gundersen SYMB_MAP_ITEMS
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersen Sign
1f6d9bc9ee894d4023b7eacea1754986f25bce57Tom Gundersen Morphism
da927ba997d68401563b927f92e6e40e021a8e5cMichal Schmidt Symbol
4b6141c42497dc199618f95fa3f359615eecfaa0Tom Gundersen Symbol
1f6d9bc9ee894d4023b7eacea1754986f25bce57Tom Gundersen where
4b6141c42497dc199618f95fa3f359615eecfaa0Tom Gundersen basic_analysis CommonLogic = Just basicCommonLogicAnalysis
4b6141c42497dc199618f95fa3f359615eecfaa0Tom Gundersen empty_signature CommonLogic = emptySig
4b6141c42497dc199618f95fa3f359615eecfaa0Tom Gundersen is_subsig CommonLogic = isSubSigOf
af4ec4309e8f82aad87a8d574785c12f8763d5f8Lennart Poettering subsig_inclusion CommonLogic s = return . inclusionMap s
4b6141c42497dc199618f95fa3f359615eecfaa0Tom Gundersen signature_union CommonLogic = sigUnion
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersen symbol_to_raw CommonLogic = symbolToRaw
4b6141c42497dc199618f95fa3f359615eecfaa0Tom Gundersen id_to_raw CommonLogic = idToRaw
f579559b3a14c1f1ef96c372e7626c4733e6ef7dTom Gundersen matches CommonLogic = Symbol.matches
stat_symb_items CommonLogic _ = mkStatSymbItems
stat_symb_map_items CommonLogic _ _ = mkStatSymbMapItem
induced_from_morphism CommonLogic = inducedFromMorphism
induced_from_to_morphism CommonLogic = inducedFromToMorphism
add_symb_to_sign CommonLogic = addSymbToSign -- TODO
{-
stat_symb_items CommonLogic = ()
stat_symb_map_items CommonLogic = ()
morphism_union CommonLogic = ()
-}
signature_colimit CommonLogic = signColimit
-- | Sublogics
instance SemiLatticeWithTop CommonLogicSL where
lub = sublogics_max
top = CommonLogic.Sublogic.top
instance MinSublogic CommonLogicSL BASIC_SPEC where
minSublogic = sl_basic_spec bottom
instance MinSublogic CommonLogicSL Sign where
minSublogic = sl_sig bottom
instance SublogicName CommonLogicSL where
sublogicName = sublogics_name
instance MinSublogic CommonLogicSL TEXT_META where
minSublogic tm = sublogic_text bottom $ getText tm
instance MinSublogic CommonLogicSL NAME where
minSublogic = sublogic_name bottom
instance MinSublogic CommonLogicSL Symbol where
minSublogic = sl_sym bottom
instance MinSublogic CommonLogicSL Morphism where
minSublogic = sl_mor bottom
instance MinSublogic CommonLogicSL SYMB_MAP_ITEMS where
minSublogic = sl_symmap bottom
instance MinSublogic CommonLogicSL SYMB_ITEMS where
minSublogic = sl_symitems bottom
instance ProjectSublogic CommonLogicSL BASIC_SPEC where
projectSublogic = prBasicSpec
instance ProjectSublogicM CommonLogicSL NAME where
projectSublogicM = prName
instance ProjectSublogicM CommonLogicSL SYMB_MAP_ITEMS where
projectSublogicM = prSymMapM
instance ProjectSublogicM CommonLogicSL SYMB_ITEMS where
projectSublogicM = prSymItemsM
instance ProjectSublogic CommonLogicSL Sign where
projectSublogic = prSig
instance ProjectSublogic CommonLogicSL Morphism where
projectSublogic = prMor
instance ProjectSublogicM CommonLogicSL Symbol where
projectSublogicM = prSymbolM