2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina{- |

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaModule : ./CommonLogic/Logic_CommonLogic.hs

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaDescription : Instance of class Logic for common logic

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaCopyright : (c) Karl Luc, DFKI Bremen 2010, Eugen Kuksa and Uni Bremen 2011

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaLicense : GPLv2 or higher, see LICENSE.txt

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaMaintainer : eugenk@informatik.uni-bremen.de

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaStability : experimental

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaPortability : non-portable (imports Logic.Logic)

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaInstance of class Logic for the common logic

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina-}

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinamodule CommonLogic.Logic_CommonLogic where

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport ATC.ProofTree ()

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport Common.ProofTree

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport CommonLogic.ATC_CommonLogic ()

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport CommonLogic.Sign

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport CommonLogic.AS_CommonLogic

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport CommonLogic.Symbol as Symbol

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport CommonLogic.Analysis

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport qualified CommonLogic.Parse_CLIF as CLIF

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport qualified CommonLogic.Parse_KIF as KIF

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport qualified CommonLogic.Print_KIF as Print_KIF

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel Březinaimport CommonLogic.Morphism

d117004902c767d46430848b6ef1c11c3ad82835Pavel Březinaimport CommonLogic.OMDocExport

2a25713afc6beefb11a799903a43f695c5d7a4f9Adam Tkacimport CommonLogic.OMDocImport as OMDocImport

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport CommonLogic.OMDoc

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport CommonLogic.Sublogic

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport qualified Data.Map as Map

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport Data.Monoid

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport Logic.Logic

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinadata CommonLogic = CommonLogic deriving Show

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinainstance Language CommonLogic where

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina description _ = "CommonLogic (an ISO standard)\n"

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinainstance Category Sign Morphism

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina where

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce ide = idMor

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce dom = source

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce cod = target

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce isInclusion = Map.null . propMap

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce legal_mor = isLegalMorphism

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina composeMorphisms = composeMor

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashovinstance Sentences CommonLogic

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov TEXT_META

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina Sign

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina Morphism

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina Symbol

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce where

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina negation CommonLogic = Just . negForm

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina sym_of CommonLogic = singletonList . symOf

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov symmap_of CommonLogic = getSymbolMap -- returns the symbol map

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina sym_name CommonLogic = getSymbolName -- returns the name of a symbol

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina map_sen CommonLogic = mapSentence -- TODO

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce symsOfSen CommonLogic _ = symsOfTextMeta

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina symKind CommonLogic = Symbol.symKind

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorceinstance Monoid BASIC_SPEC where

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina mempty = Basic_spec []

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina mappend (Basic_spec l1) (Basic_spec l2) = Basic_spec $ l1 ++ l2

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinainstance Syntax CommonLogic

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina BASIC_SPEC

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina Symbol

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina SYMB_ITEMS

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina SYMB_MAP_ITEMS

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina where

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina parsersAndPrinters CommonLogic =

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina addSyntax "KIF" (KIF.basicSpec, Print_KIF.printBasicSpec)

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina $ addSyntax "CLIF" (CLIF.basicSpec, pretty)

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina $ makeDefault (CLIF.basicSpec, pretty)

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina parse_symb_items CommonLogic = Just CLIF.symbItems

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina parse_symb_map_items CommonLogic = Just CLIF.symbMapItems

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinainstance Logic CommonLogic

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina CommonLogicSL -- Sublogics

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov BASIC_SPEC -- basic_spec

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov TEXT_META -- sentence

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina SYMB_ITEMS -- symb_items

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina SYMB_MAP_ITEMS -- symb_map_items

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina Sign -- sign

7379170a0860790f2739e07fffe3d6ec85264566Pavel Březina Morphism -- morphism

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina Symbol -- symbol

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina Symbol -- raw_symbol

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina ProofTree -- proof_tree

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina where

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina stability CommonLogic = Stable

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina all_sublogics CommonLogic = sublogics_all

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina empty_proof_tree CommonLogic = emptyProofTree

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina provers CommonLogic = []

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel Březina omdoc_metatheory CommonLogic = Just clMetaTheory

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina export_senToOmdoc CommonLogic = exportSenToOmdoc

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina export_symToOmdoc CommonLogic = exportSymToOmdoc

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina omdocToSen CommonLogic = OMDocImport.omdocToSen

5ff1c3c5a12930692cb6284d14f7fda3a974af8ePavel Březina omdocToSym CommonLogic = OMDocImport.omdocToSym

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinainstance StaticAnalysis CommonLogic

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina BASIC_SPEC

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel Březina TEXT_META

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březina SYMB_ITEMS

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel Březina SYMB_MAP_ITEMS

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březina Sign

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel Březina Morphism

55fdd0d28e7c88f333ad78183b0ba37a1da34160Pavel Březina Symbol

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov Symbol

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov where

55fdd0d28e7c88f333ad78183b0ba37a1da34160Pavel Březina basic_analysis CommonLogic = Just basicCommonLogicAnalysis

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březina empty_signature CommonLogic = emptySig

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březina is_subsig CommonLogic = isSubSigOf

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel Březina subsig_inclusion CommonLogic s = return . inclusionMap s

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel Březina signature_union CommonLogic = sigUnion

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel Březina symbol_to_raw CommonLogic = symbolToRaw

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel Březina id_to_raw CommonLogic = idToRaw

55fdd0d28e7c88f333ad78183b0ba37a1da34160Pavel Březina matches CommonLogic = Symbol.matches

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov stat_symb_items CommonLogic _ = mkStatSymbItems

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov stat_symb_map_items CommonLogic _ _ = mkStatSymbMapItem

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel Březina induced_from_morphism CommonLogic = inducedFromMorphism

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel Březina induced_from_to_morphism CommonLogic = inducedFromToMorphism

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina add_symb_to_sign CommonLogic = addSymbToSign -- TODO

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březina

7379170a0860790f2739e07fffe3d6ec85264566Pavel Březina{-

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina stat_symb_items CommonLogic = ()

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina stat_symb_map_items CommonLogic = ()

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina morphism_union CommonLogic = ()

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina-}

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina signature_colimit CommonLogic = signColimit

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina-- | Sublogics

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinainstance SemiLatticeWithTop CommonLogicSL where

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina lub = sublogics_max

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina top = CommonLogic.Sublogic.top

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinainstance MinSublogic CommonLogicSL BASIC_SPEC where

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina minSublogic = sl_basic_spec bottom

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinainstance MinSublogic CommonLogicSL Sign where

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina minSublogic = sl_sig bottom

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinainstance SublogicName CommonLogicSL where

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina sublogicName = sublogics_name

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinainstance MinSublogic CommonLogicSL TEXT_META where

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina minSublogic tm = sublogic_text bottom $ getText tm

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březinainstance MinSublogic CommonLogicSL NAME where

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina minSublogic = sublogic_name bottom

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinainstance MinSublogic CommonLogicSL Symbol where

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina minSublogic = sl_sym bottom

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březinainstance MinSublogic CommonLogicSL Morphism where

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina minSublogic = sl_mor bottom

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinainstance MinSublogic CommonLogicSL SYMB_MAP_ITEMS where

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina minSublogic = sl_symmap bottom

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinainstance MinSublogic CommonLogicSL SYMB_ITEMS where

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel Březina minSublogic = sl_symitems bottom

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina

76db25eab9010a33657f35e5afc8477c996df7a3Pavel Březinainstance ProjectSublogic CommonLogicSL BASIC_SPEC where

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina projectSublogic = prBasicSpec

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březinainstance ProjectSublogicM CommonLogicSL NAME where

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina projectSublogicM = prName

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorceinstance ProjectSublogicM CommonLogicSL SYMB_MAP_ITEMS where

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce projectSublogicM = prSymMapM

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březinainstance ProjectSublogicM CommonLogicSL SYMB_ITEMS where

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina projectSublogicM = prSymItemsM

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinainstance ProjectSublogic CommonLogicSL Sign where

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březina projectSublogic = prSig

1509d1723d39124f840c214327e698aff3b3f683Pavel Březina

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashovinstance ProjectSublogic CommonLogicSL Morphism where

1509d1723d39124f840c214327e698aff3b3f683Pavel Březina projectSublogic = prMor

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březinainstance ProjectSublogicM CommonLogicSL Symbol where

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina projectSublogicM = prSymbolM

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina