Cross Reference: /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
1047N/A{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
1047N/A{- |
1047N/AModule : $Header$
1047N/ADescription : Instance of class Logic for common logic
1047N/ACopyright : (c) Karl Luc, DFKI Bremen 2010, Eugen Kuksa and Uni Bremen 2011
1047N/ALicense : GPLv2 or higher, see LICENSE.txt
1047N/A
1047N/AMaintainer : eugenk@informatik.uni-bremen.de
1047N/AStability : experimental
1047N/APortability : non-portable (imports Logic.Logic)
1047N/A
1047N/AInstance of class Logic for the common logic
1047N/A-}
1047N/A
1047N/Amodule CommonLogic.Logic_CommonLogic where
1047N/A
1047N/Aimport ATC.ProofTree ()
1047N/A
1047N/Aimport Common.ProofTree
1047N/A
1047N/Aimport CommonLogic.ATC_CommonLogic ()
1047N/Aimport CommonLogic.Sign
1047N/Aimport CommonLogic.AS_CommonLogic
1047N/Aimport CommonLogic.Symbol as Symbol
4268N/Aimport CommonLogic.Analysis
1047N/Aimport qualified CommonLogic.Parse_CLIF as CLIF
1047N/Aimport qualified CommonLogic.Parse_KIF as KIF
1047N/Aimport qualified CommonLogic.Print_KIF as Print_KIF
1047N/Aimport CommonLogic.Morphism
4268N/Aimport CommonLogic.OMDocExport
4268N/Aimport CommonLogic.OMDocImport as OMDocImport
4268N/Aimport CommonLogic.OMDoc
1047N/Aimport CommonLogic.Sublogic
1047N/A
1047N/Aimport qualified Data.Map as Map
1047N/Aimport Data.Monoid
1047N/A
1907N/Aimport Logic.Logic
3503N/A
2324N/Adata CommonLogic = CommonLogic deriving Show
1047N/A
1047N/Ainstance Language CommonLogic where
3397N/A description _ = "CommonLogic Logic\n"
1935N/A
1047N/Ainstance Category Sign Morphism
1047N/A where
1047N/A ide = idMor
1047N/A dom = source
1907N/A cod = target
1047N/A isInclusion = Map.null . propMap
1047N/A legal_mor = isLegalMorphism
1047N/A composeMorphisms = composeMor
1907N/A
1907N/Ainstance Sentences CommonLogic
4268N/A TEXT_META
4268N/A Sign
4268N/A Morphism
1047N/A Symbol
1047N/A where
1047N/A negation CommonLogic = Just . negForm
1907N/A sym_of CommonLogic = singletonList . symOf
1047N/A symmap_of CommonLogic = getSymbolMap -- returns the symbol map
1907N/A sym_name CommonLogic = getSymbolName -- returns the name of a symbol
1047N/A map_sen CommonLogic = mapSentence -- TODO
1907N/A symsOfSen CommonLogic = symsOfTextMeta
1907N/A symKind CommonLogic = Symbol.symKind
1907N/A
1907N/Ainstance Monoid BASIC_SPEC where
1907N/A mempty = Basic_spec []
1907N/A mappend (Basic_spec l1) (Basic_spec l2) = Basic_spec $ l1 ++ l2
1907N/A
1907N/Ainstance Syntax CommonLogic
1907N/A BASIC_SPEC
1047N/A Symbol
1047N/A SYMB_ITEMS
1047N/A SYMB_MAP_ITEMS
1047N/A where
4268N/A parsersAndPrinters CommonLogic =
1047N/A addSyntax "KIF" (KIF.basicSpec, Print_KIF.printBasicSpec)
1047N/A $ addSyntax "CLIF" (CLIF.basicSpec, pretty)
1047N/A $ makeDefault (CLIF.basicSpec, pretty)
1047N/A parse_symb_items CommonLogic = Just CLIF.symbItems
1935N/A parse_symb_map_items CommonLogic = Just CLIF.symbMapItems
1047N/A
1935N/Ainstance Logic CommonLogic
1047N/A CommonLogicSL -- Sublogics
1047N/A BASIC_SPEC -- basic_spec
1047N/A TEXT_META -- sentence
3042N/A SYMB_ITEMS -- symb_items
3042N/A SYMB_MAP_ITEMS -- symb_map_items
3042N/A Sign -- sign
1907N/A Morphism -- morphism
1047N/A Symbol -- symbol
1047N/A Symbol -- raw_symbol
1047N/A ProofTree -- proof_tree
2210N/A where
1516N/A stability CommonLogic = Testing
1907N/A all_sublogics CommonLogic = sublogics_all
1907N/A empty_proof_tree CommonLogic = emptyProofTree
2324N/A provers CommonLogic = []
2324N/A omdoc_metatheory CommonLogic = Just clMetaTheory
2324N/A export_senToOmdoc CommonLogic = exportSenToOmdoc
2324N/A export_symToOmdoc CommonLogic = exportSymToOmdoc
2324N/A omdocToSen CommonLogic = OMDocImport.omdocToSen
2324N/A omdocToSym CommonLogic = OMDocImport.omdocToSym
2324N/A
1907N/A
1907N/Ainstance StaticAnalysis CommonLogic
1516N/A BASIC_SPEC
1907N/A TEXT_META
4268N/A SYMB_ITEMS
1907N/A SYMB_MAP_ITEMS
1907N/A Sign
1907N/A Morphism
1047N/A Symbol
1907N/A Symbol
1502N/A where
1047N/A basic_analysis CommonLogic = Just basicCommonLogicAnalysis
1047N/A empty_signature CommonLogic = emptySig
2324N/A is_subsig CommonLogic = isSubSigOf
4268N/A subsig_inclusion CommonLogic s = return . inclusionMap s
2324N/A signature_union CommonLogic = sigUnion
2324N/A symbol_to_raw CommonLogic = symbolToRaw
2324N/A id_to_raw CommonLogic = idToRaw
2324N/A matches CommonLogic = Symbol.matches
4268N/A stat_symb_items CommonLogic _ = mkStatSymbItems
2324N/A stat_symb_map_items CommonLogic _ _ = mkStatSymbMapItem
2324N/A induced_from_morphism CommonLogic = inducedFromMorphism
2324N/A induced_from_to_morphism CommonLogic = inducedFromToMorphism
2324N/A add_symb_to_sign CommonLogic = addSymbToSign -- TODO
2324N/A
2324N/A{-
1047N/A stat_symb_items CommonLogic = ()
1047N/A stat_symb_map_items CommonLogic = ()
3042N/A morphism_union CommonLogic = ()
3042N/A signature_colimit CommonLogic = ()
2831N/A-}
4576N/A
1047N/A-- | Sublogics
1047N/Ainstance SemiLatticeWithTop CommonLogicSL where
1047N/A join = sublogics_max
1047N/A top = CommonLogic.Sublogic.top
4268N/A
1907N/Ainstance MinSublogic CommonLogicSL BASIC_SPEC where
1907N/A minSublogic = sl_basic_spec bottom
1907N/A
1907N/Ainstance MinSublogic CommonLogicSL Sign where
3503N/A minSublogic = sl_sig bottom
3503N/A
3503N/Ainstance SublogicName CommonLogicSL where
3503N/A sublogicName = sublogics_name
3503N/A
3503N/Ainstance MinSublogic CommonLogicSL TEXT_META where
3503N/A minSublogic tm = sublogic_text bottom $ getText tm
3503N/A
1047N/Ainstance MinSublogic CommonLogicSL NAME where
3571N/A minSublogic = sublogic_name bottom
3571N/A
4268N/Ainstance MinSublogic CommonLogicSL Symbol where
3571N/A minSublogic = sl_sym bottom
3571N/A
3571N/Ainstance MinSublogic CommonLogicSL Morphism where
3571N/A minSublogic = sl_mor bottom
3571N/A
4268N/Ainstance MinSublogic CommonLogicSL SYMB_MAP_ITEMS where
4268N/A minSublogic = sl_symmap bottom
4268N/A
4268N/Ainstance MinSublogic CommonLogicSL SYMB_ITEMS where
4268N/A minSublogic = sl_symitems bottom
4268N/A
1047N/Ainstance ProjectSublogic CommonLogicSL BASIC_SPEC where
1047N/A projectSublogic = prBasicSpec
1047N/A
1047N/Ainstance 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