Cross Reference: /hets/CASL/Logic_CASL.hs
Logic_CASL.hs revision 1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79
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
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
{-# LANGUAGE CPP, MultiParamTypeClasses, TypeSynonymInstances
, FlexibleInstances #-}
{- |
Module : $Header$
Description : Instance of class Logic for the CASL logic
Copyright : (c) Klaus Luettich, Uni Bremen 2002-2005
License : GPLv2 or higher, see LICENSE.txt
Maintainer : till@informatik.uni-bremen.de
Stability : provisional
Portability : non-portable (imports Logic.Logic)
Instance of class Logic for the CASL logic
Also the instances for Syntax and Category.
-}
module CASL.Logic_CASL where
import ATC.ProofTree ()
import CASL.AS_Basic_CASL
import CASL.Parse_AS_Basic
import CASL.Kif
import CASL.Kif2CASL
import CASL.Fold
import CASL.ToDoc
import CASL.ToItem (bsToItem)
import CASL.SymbolParser
import CASL.MapSentence
import CASL.Amalgamability
import CASL.ATC_CASL ()
import CASL.Sublogic as SL
import CASL.Sign
import CASL.StaticAna
import CASL.ColimSign
import CASL.Morphism
import CASL.SymbolMapAnalysis
import CASL.Taxonomy
import CASL.Simplify
import CASL.SimplifySen
import CASL.CCC.FreeTypes
import CASL.CCC.OnePoint () -- currently unused
import CASL.Qualify
import CASL.Quantification
import qualified CASL.OMDocImport as OMI
import CASL.OMDocExport
import CASL.Freeness
#ifdef UNI_PACKAGE
import CASL.QuickCheck
#endif
import Common.ProofTree
import Common.Consistency
import Common.DocUtils
import Data.Monoid
import qualified Data.Set as Set
import Logic.Logic
data CASL = CASL deriving Show
instance Language CASL where
description _ = unlines
[ "CASL - the Common algebraic specification language"
, "This logic is subsorted partial first-order logic"
, " with sort generation constraints"
, "See the CASL User Manual, LNCS 2900, Springer Verlag"
, "and the CASL Reference Manual, LNCS 2960, Springer Verlag"
, "See also http://www.cofi.info/CASL.html"
, ""
, "Abbreviations of sublogic names indicate the following feature:"
, " Sub -> with subsorting"
, " Sul -> with a locally filtered subsort relation"
, " P -> with partial functions"
, " C -> with sort generation constraints"
, " eC -> C without renamings"
, " sC -> C with injective constructors"
, " seC -> sC and eC"
, " FOL -> first order logic"
, " FOAlg -> FOL without predicates"
, " Horn -> positive conditional logic"
, " GHorn -> generalized Horn"
, " GCond -> GHorn without predicates"
, " Cond -> Horn without predicates"
, " Atom -> atomic logic"
, " Eq -> Atom without predicates"
, " = -> with equality"
, ""
, "Examples:"
, " SubPCFOL= -> the CASL logic itself"
, " FOAlg= -> first order algebra (without predicates)"
, " SubPHorn= -> the positive conditional fragement of CASL"
, " SubPAtom -> the atomic subset of CASL"
, " SubPCAtom -> SubPAtom with sort generation constraints"
, " Eq= -> classical equational logic" ]
type CASLBasicSpec = BASIC_SPEC () () ()
trueC :: a -> b -> Bool
trueC _ _ = True
instance (Ord f, Ord e, Ord m, MorphismExtension e m) =>
Category (Sign f e) (Morphism f e m) where
ide sig = idMor (ideMorphismExtension $ extendedInfo sig) sig
inverse = inverseMorphism inverseMorphismExtension
composeMorphisms = composeM composeMorphismExtension
dom = msource
cod = mtarget
isInclusion = isInclusionMorphism isInclusionMorphismExtension
legal_mor = legalMor
instance Monoid (BASIC_SPEC b s f) where
mempty = Basic_spec []
mappend (Basic_spec l1) (Basic_spec l2) = Basic_spec $ l1 ++ l2
-- abstract syntax, parsing (and printing)
instance Syntax CASL CASLBasicSpec
SYMB_ITEMS SYMB_MAP_ITEMS
where
parsersAndPrinters CASL = addSyntax "KIF"
(const $ fmap kif2CASL kifBasic, pretty)
$ makeDefault (basicSpec [], pretty)
parse_symb_items CASL = Just $ symbItems []
parse_symb_map_items CASL = Just $ symbMapItems []
toItem CASL = bsToItem
-- lattices (for sublogics)
instance Lattice a => SemiLatticeWithTop (CASL_SL a) where
join = sublogics_max
top = SL.top
class Lattice a => MinSL a f where
minSL :: f -> CASL_SL a
instance MinSL () () where
minSL () = bottom
class NameSL a where
nameSL :: a -> String
instance NameSL () where
nameSL _ = ""
class Lattice a => ProjForm a f where
projForm :: CASL_SL a -> f -> Maybe (FORMULA f)
instance Lattice a => ProjForm a () where
projForm _ = Just . ExtFORMULA
class (Lattice a, ProjForm a f) => ProjSigItem a s f where
projSigItems :: CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT])
instance (Lattice a, ProjForm a f) => ProjSigItem a () f where
projSigItems _ s = (Just $ Ext_SIG_ITEMS s, [])
class (Lattice a, ProjForm a f) => ProjBasic a b s f where
projBasicItems :: CASL_SL a -> b -> (Maybe (BASIC_ITEMS b s f), [SORT])
instance (Lattice a, ProjForm a f, ProjSigItem a s f)
=> ProjBasic a () s f where
projBasicItems _ b = (Just $ Ext_BASIC_ITEMS b, [])
instance (NameSL a) => SublogicName (CASL_SL a) where
sublogicName = sublogics_name nameSL
instance (MinSL a f, MinSL a s, MinSL a b) =>
MinSublogic (CASL_SL a) (BASIC_SPEC b s f) where
minSublogic = sl_basic_spec minSL minSL minSL
instance MinSL a f => MinSublogic (CASL_SL a) (FORMULA f) where
minSublogic = sl_sentence minSL
instance Lattice a => MinSublogic (CASL_SL a) SYMB_ITEMS where
minSublogic = sl_symb_items
instance Lattice a => MinSublogic (CASL_SL a) SYMB_MAP_ITEMS where
minSublogic = sl_symb_map_items
instance MinSL a e => MinSublogic (CASL_SL a) (Sign f e) where
minSublogic = sl_sign minSL
instance MinSL a e => MinSublogic (CASL_SL a) (Morphism f e m) where
minSublogic = sl_morphism minSL
instance Lattice a => MinSublogic (CASL_SL a) Symbol where
minSublogic = sl_symbol
instance (MinSL a f, MinSL a s, MinSL a b, ProjForm a f,
ProjSigItem a s f, ProjBasic a b s f) =>
ProjectSublogic (CASL_SL a) (BASIC_SPEC b s f) where
projectSublogic = pr_basic_spec projBasicItems projSigItems projForm
instance Lattice a => ProjectSublogicM (CASL_SL a) SYMB_ITEMS where
projectSublogicM = pr_symb_items
instance Lattice a => ProjectSublogicM (CASL_SL a) SYMB_MAP_ITEMS where
projectSublogicM = pr_symb_map_items
instance MinSL a e => ProjectSublogic (CASL_SL a) (Sign f e) where
projectSublogic = pr_sign
instance MinSL a e => ProjectSublogic (CASL_SL a) (Morphism f e m) where
projectSublogic = pr_morphism
instance Lattice a => ProjectSublogicM (CASL_SL a) Symbol where
projectSublogicM = pr_symbol
-- CASL logic
instance Sentences CASL CASLFORMULA CASLSign CASLMor Symbol where
map_sen CASL m = return . mapSen (const id) m
negation CASL = negateFormula
sym_of CASL = symOf
mostSymsOf CASL = sigSymsOf
symmap_of CASL = morphismToSymbMap
sym_name CASL = symName
symKind CASL = show . pretty . symbolKind . symbType
symsOfSen CASL = Set.toList
. foldFormula (symbolsRecord $ const Set.empty)
simplify_sen CASL = simplifyCASLSen
print_named CASL = printTheoryFormula
instance StaticAnalysis CASL CASLBasicSpec CASLFORMULA
SYMB_ITEMS SYMB_MAP_ITEMS
CASLSign
CASLMor
Symbol RawSymbol where
basic_analysis CASL = Just basicCASLAnalysis
stat_symb_map_items CASL = statSymbMapItems
stat_symb_items CASL = statSymbItems
signature_colimit CASL diag = return $ signColimit diag extCASLColimit
quotient_term_algebra CASL = quotientTermAlgebra
ensures_amalgamability CASL (opts, diag, sink, desc) =
ensuresAmalgamability opts diag sink desc
qualify CASL = qualifySig
symbol_to_raw CASL = symbolToRaw
id_to_raw CASL = idToRaw
matches CASL = CASL.Morphism.matches
is_transportable CASL = isSortInjective
is_injective CASL = isInjective
empty_signature CASL = emptySign ()
add_symb_to_sign CASL = addSymbToSign
signature_union CASL s = return . addSig const s
signatureDiff CASL s = return . diffSig const s
intersection CASL s = return . interSig const s
morphism_union CASL = plainMorphismUnion const
final_union CASL = finalUnion const
is_subsig CASL = isSubSig trueC
subsig_inclusion CASL = sigInclusion ()
cogenerated_sign CASL = cogeneratedSign ()
generated_sign CASL = generatedSign ()
induced_from_morphism CASL = inducedFromMorphism ()
induced_from_to_morphism CASL = inducedFromToMorphism () trueC const
theory_to_taxonomy CASL = convTaxo
instance Logic CASL CASL_Sublogics
CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
CASLSign
CASLMor
Symbol RawSymbol ProofTree where
stability CASL = Stable
proj_sublogic_epsilon CASL = pr_epsilon ()
all_sublogics CASL = sublogics_all []
sublogicDimensions CASL = sDims []
parseSublogic CASL = parseSL (\ s -> Just ((), s))
conservativityCheck CASL = [ConservativityChecker "CCC" checkFreeType]
empty_proof_tree CASL = emptyProofTree
omdoc_metatheory CASL = Just caslMetaTheory
export_senToOmdoc CASL = exportSenToOmdoc
export_symToOmdoc CASL = exportSymToOmdoc
export_theoryToOmdoc CASL = exportTheoryToOmdoc
omdocToSen CASL = OMI.omdocToSen
omdocToSym CASL = OMI.omdocToSym
addOMadtToTheory CASL = OMI.addOMadtToTheory
addOmdocToTheory CASL = OMI.addOmdocToTheory
syntaxTable CASL = Just . getSyntaxTable
#ifdef UNI_PACKAGE
provers CASL = [quickCheckProver]
#endif