Logic_ExtModal.hs revision 55cf6e01272ec475edea32aa9b7923de2d36cb42
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
55cf6e01272ec475edea32aa9b7923de2d36cb42Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian MaederModule : $Header$
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta GirleaDescription : Instance of class Logic for ExtModal
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian MaederCopyright : DFKI GmbH 2009
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
cb1bcdcebd18280e73151a05cf9846b940674518Codruta GirleaMaintainer : codruta.liliana@gmail.com
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta GirleaStability : experimental
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian MaederPortability : non-portable (imports Logic)
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta GirleaInstance of class Logic for ExtModal
cb1bcdcebd18280e73151a05cf9846b940674518Codruta Girleaimport qualified Data.Map as Map
cb1bcdcebd18280e73151a05cf9846b940674518Codruta Girleadata ExtModal = ExtModal deriving Show
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederinstance Language ExtModal where
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder description _ = unlines
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder [ "ExtModal is the 'extended modal logic' extension of CASL. "
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder , "Syntax for ordinary modalities, multi-modal logic, dynamic "
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder , "logic, graded modal logic, hybrid logic, CTL* and mu-calculus "
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder , "is provided. Specific modal logics can be optained via "
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder , "restrictions to sublanguages."
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maedertype ExtModalSign = Sign EM_FORMULA EModalSign
cb1bcdcebd18280e73151a05cf9846b940674518Codruta Girleatype ExtModalMorph = Morphism EM_FORMULA EModalSign MorphExtension
cb1bcdcebd18280e73151a05cf9846b940674518Codruta Girleatype ExtModalFORMULA = FORMULA EM_FORMULA
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederinstance SignExtension EModalSign where
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder isSubSignExtension = isSubEModalSign
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederinstance Syntax ExtModal EM_BASIC_SPEC SYMB_ITEMS SYMB_MAP_ITEMS where
cb5be4f31df88b8137ef3cabf4e8b0ddec52f351Christian Maeder parse_basic_spec ExtModal = Just $ basicSpec ext_modal_reserved_words
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder parse_symb_items ExtModal = Just $ symbItems ext_modal_reserved_words
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder parse_symb_map_items ExtModal =
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder Just $ symbMapItems ext_modal_reserved_words
cb1bcdcebd18280e73151a05cf9846b940674518Codruta Girlea-- Modal formula mapping via signature morphism
fd1c864a3dec70aa22ecb2bc85816ec8251c6decCodruta Girleamap_EM_FORMULA :: MapSen EM_FORMULA EModalSign MorphExtension
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maedermap_EM_FORMULA morph (BoxOrDiamond choice t_m leq_geq number f pos) =
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder let new_tm tm = case tm of
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder Simple_modality sm ->
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder let mds = mod_map (extended_map morph) in
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder if Map.member sm mds then Simple_modality (mds Map.! sm) else tm
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder Composition tm1 tm2 -> Composition (new_tm tm1) (new_tm tm2)
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder Union tm1 tm2 -> Union (new_tm tm1) (new_tm tm2)
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder TransitiveClosure tm1 -> TransitiveClosure (new_tm tm1)
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder Guard frm -> Guard (mapSen map_EM_FORMULA morph frm)
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder new_f = mapSen map_EM_FORMULA morph f
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder in BoxOrDiamond choice (new_tm t_m) leq_geq number new_f pos
fd1c864a3dec70aa22ecb2bc85816ec8251c6decCodruta Girleamap_EM_FORMULA morph (Hybrid choice nm f pos) =
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder let new_nom = case nm of
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder Nominal nom -> let nms = nom_map (extended_map morph) in
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder if Map.member nom nms then Nominal (nms Map.! nom) else nm
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder new_f = mapSen map_EM_FORMULA morph f
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder in Hybrid choice new_nom new_f pos
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maedermap_EM_FORMULA morph (UntilSince choice f1 f2 pos) =
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder let new_f1 = mapSen map_EM_FORMULA morph f1
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder new_f2 = mapSen map_EM_FORMULA morph f2
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder in UntilSince choice new_f1 new_f2 pos
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maedermap_EM_FORMULA morph (NextY choice f pos) =
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder let new_f = mapSen map_EM_FORMULA morph f
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder in NextY choice new_f pos
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maedermap_EM_FORMULA morph (PathQuantification choice f pos) =
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder let new_f = mapSen map_EM_FORMULA morph f
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder in PathQuantification choice new_f pos
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maedermap_EM_FORMULA morph (StateQuantification t_dir choice f pos) =
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder let new_f = mapSen map_EM_FORMULA morph f
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder in StateQuantification t_dir choice new_f pos
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maedermap_EM_FORMULA morph (FixedPoint choice p_var f pos) =
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder let new_f = mapSen map_EM_FORMULA morph f
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder in FixedPoint choice p_var new_f pos
cb1bcdcebd18280e73151a05cf9846b940674518Codruta Girlea-- Simplification of formulas - simplifySen for ExtFORMULA
cb1bcdcebd18280e73151a05cf9846b940674518Codruta GirleasimEMSen :: Sign EM_FORMULA EModalSign -> EM_FORMULA -> EM_FORMULA
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian MaedersimEMSen sign (BoxOrDiamond choice tm leq_geq number f pos) =
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder BoxOrDiamond choice tm leq_geq number
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder (simplifySen frmTypeAna simEMSen sign f) pos
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian MaedersimEMSen sign (Hybrid choice nom f pos) =
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder Hybrid choice nom (simplifySen frmTypeAna simEMSen sign f) pos
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian MaedersimEMSen sign (UntilSince choice f1 f2 pos) =
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder UntilSince choice (simplifySen frmTypeAna simEMSen sign f1)
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder (simplifySen frmTypeAna simEMSen sign f2) pos
cb1bcdcebd18280e73151a05cf9846b940674518Codruta GirleasimEMSen sign (NextY choice f pos) =
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder NextY choice (simplifySen frmTypeAna simEMSen sign f) pos
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian MaedersimEMSen sign (PathQuantification choice f pos) =
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder PathQuantification choice (simplifySen frmTypeAna simEMSen sign f) pos
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian MaedersimEMSen sign (StateQuantification t_dir choice f pos) =
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder StateQuantification t_dir choice
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder (simplifySen frmTypeAna simEMSen sign f) pos
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian MaedersimEMSen sign (FixedPoint choice p_var f pos) =
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder FixedPoint choice p_var (simplifySen frmTypeAna simEMSen sign f) pos
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederinstance Sentences ExtModal ExtModalFORMULA ExtModalSign ExtModalMorph Symbol
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder map_sen ExtModal morph = return . mapSen map_EM_FORMULA morph
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder simplify_sen ExtModal = simplifySen frmTypeAna simEMSen
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder print_sign ExtModal sig = printSign
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder (printEModalSign $ simplifySen frmTypeAna simEMSen sig) sig
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder sym_of ExtModal = symOf
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder symmap_of ExtModal = morphismToSymbMap
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder sym_name ExtModal = symName
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederinstance StaticAnalysis ExtModal EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol where
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder basic_analysis ExtModal = Just basicEModalAnalysis
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder stat_symb_map_items ExtModal = statSymbMapItems
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder stat_symb_items ExtModal = statSymbItems
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder symbol_to_raw ExtModal = symbolToRaw
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder id_to_raw ExtModal = idToRaw
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder matches ExtModal = CASL.Morphism.matches
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder empty_signature ExtModal = emptySign emptyEModalSign
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder signature_union ExtModal sgn = return . addSig addEModalSign sgn
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder intersection ExtModal sgn = return . interSig interEModalSign sgn
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder final_union ExtModal = finalUnion addEModalSign
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder morphism_union ExtModal = plainMorphismUnion addEModalSign
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder is_subsig ExtModal = isSubSig isSubEModalSign
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder subsig_inclusion ExtModal = sigInclusion emptyMorphExtension
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder generated_sign ExtModal = generatedSign emptyMorphExtension
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder cogenerated_sign ExtModal = cogeneratedSign emptyMorphExtension
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder induced_from_morphism ExtModal = inducedFromMorphism emptyMorphExtension
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder induced_from_to_morphism ExtModal =
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder inducedFromToMorphism emptyMorphExtension isSubEModalSign
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder diffEModalSign
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder theory_to_taxonomy ExtModal = convTaxo
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederinstance Logic ExtModal () EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () where
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder stability _ = Experimental
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder empty_proof_tree _ = ()