hets/CommonLogic/Logic_CommonLogic.hs

	Logic_CommonLogic.hs revision a65c6747c9acbbebc93baba7bae94d2e3d8cdafb


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu{- |
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert SavuModule      :  $Header$
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert SavuDescription :  Instance of class Logic for common logic
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert SavuCopyright   :  (c) Karl Luc, DFKI Bremen 2010, Eugen Kuksa and Uni Bremen 2011
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert SavuLicense     :  GPLv2 or higher, see LICENSE.txt
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert SavuMaintainer  :  eugenk@informatik.uni-bremen.de
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert SavuStability   :  experimental
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert SavuPortability :  non-portable (imports Logic.Logic)
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert SavuInstance of class Logic for the common logic
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu-}
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savumodule CommonLogic.Logic_CommonLogic where
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savuimport ATC.ProofTree ()
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savuimport Common.ProofTree
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savuimport CommonLogic.ATC_CommonLogic ()
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savuimport CommonLogic.Sign
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savuimport CommonLogic.AS_CommonLogic
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savuimport CommonLogic.Symbol as Symbol
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savuimport CommonLogic.Analysis
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savuimport qualified CommonLogic.Parse_CLIF as CLIF
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savuimport qualified CommonLogic.Parse_KIF as KIF
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savuimport qualified CommonLogic.Print_KIF as Print_KIF
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savuimport CommonLogic.Morphism
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savuimport CommonLogic.OMDocExport
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savuimport CommonLogic.OMDocImport as OMDocImport
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savuimport CommonLogic.OMDoc
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savuimport CommonLogic.Sublogic
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savuimport qualified Data.Map as Map
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savuimport Data.Monoid
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savuimport Logic.Logic
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savudata CommonLogic = CommonLogic deriving Show
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savuinstance Language CommonLogic where
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu    description _ = "CommonLogic Logic\n"
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savuinstance Category Sign Morphism
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu    where
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu      ide = idMor
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu      dom = source
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu      cod = target
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu      isInclusion = Map.null . propMap
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu      legal_mor = isLegalMorphism
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu      composeMorphisms = composeMor
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savuinstance Sentences CommonLogic
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu    TEXT_META
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu    Sign
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu    Morphism
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu    Symbol
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu    where
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu      negation CommonLogic = Just . negForm
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu      sym_of CommonLogic = singletonList . symOf
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu      symmap_of CommonLogic = getSymbolMap -- returns the symbol map
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu      sym_name CommonLogic = getSymbolName -- returns the name of a symbol
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu      map_sen CommonLogic = mapSentence -- TODO
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu      symsOfSen CommonLogic = symsOfTextMeta
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu      symKind CommonLogic = Symbol.symKind
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savuinstance Monoid BASIC_SPEC where
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu    mempty = Basic_spec []
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu    mappend (Basic_spec l1) (Basic_spec l2) = Basic_spec $ l1 ++ l2
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu
bb1a72b84b087ebe2aae9e73ecf3caaefcb8a206Robert Savuinstance Syntax CommonLogic
bb1a72b84b087ebe2aae9e73ecf3caaefcb8a206Robert Savu    BASIC_SPEC
bb1a72b84b087ebe2aae9e73ecf3caaefcb8a206Robert Savu    Symbol
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu    SYMB_ITEMS
bb1a72b84b087ebe2aae9e73ecf3caaefcb8a206Robert Savu    SYMB_MAP_ITEMS
bb1a72b84b087ebe2aae9e73ecf3caaefcb8a206Robert Savu    where
bb1a72b84b087ebe2aae9e73ecf3caaefcb8a206Robert Savu      parsersAndPrinters CommonLogic =
bb1a72b84b087ebe2aae9e73ecf3caaefcb8a206Robert Savu        addSyntax "KIF" (KIF.basicSpec, Print_KIF.printBasicSpec)
bb1a72b84b087ebe2aae9e73ecf3caaefcb8a206Robert Savu        $ addSyntax "CLIF" (CLIF.basicSpec, pretty)
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu        $ makeDefault (CLIF.basicSpec, pretty)
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu      parse_symb_items CommonLogic = Just CLIF.symbItems
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu      parse_symb_map_items CommonLogic = Just CLIF.symbMapItems
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savuinstance Logic CommonLogic
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu    CommonLogicSL     -- Sublogics
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu    BASIC_SPEC        -- basic_spec
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu    TEXT_META         -- sentence
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu    SYMB_ITEMS        -- symb_items
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu    SYMB_MAP_ITEMS    -- symb_map_items
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu    Sign              -- sign
bb1a72b84b087ebe2aae9e73ecf3caaefcb8a206Robert Savu    Morphism          -- morphism
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu    Symbol            -- symbol
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu    Symbol            -- raw_symbol
    ProofTree         -- proof_tree
    where
       stability CommonLogic = Testing
       all_sublogics CommonLogic = sublogics_all
       empty_proof_tree CommonLogic = emptyProofTree
       provers CommonLogic = []
       omdoc_metatheory CommonLogic = Just clMetaTheory
       export_senToOmdoc CommonLogic = exportSenToOmdoc
       export_symToOmdoc CommonLogic = exportSymToOmdoc
       omdocToSen CommonLogic = OMDocImport.omdocToSen
       omdocToSym CommonLogic = OMDocImport.omdocToSym


instance StaticAnalysis CommonLogic
    BASIC_SPEC
    TEXT_META
    SYMB_ITEMS
    SYMB_MAP_ITEMS
    Sign
    Morphism
    Symbol
    Symbol
    where
      basic_analysis CommonLogic = Just basicCommonLogicAnalysis
      empty_signature CommonLogic = emptySig
      is_subsig CommonLogic = isSubSigOf
      subsig_inclusion CommonLogic s = return . inclusionMap s
      signature_union CommonLogic = sigUnion
      symbol_to_raw CommonLogic = symbolToRaw
      id_to_raw CommonLogic = idToRaw
      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 = ()
-}

-- | Sublogics
instance SemiLatticeWithTop CommonLogicSL where
    join = 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