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
{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module : $Header$
Description : Instance of class Logic for ExtModal
Copyright : DFKI GmbH 2009
License : GPLv2 or higher, see LICENSE.txt
Maintainer : codruta.liliana@gmail.com
Stability : experimental
Portability : non-portable (imports Logic)
Instance of class Logic for ExtModal
-}
module ExtModal.Logic_ExtModal where
import ExtModal.AS_ExtModal
import ExtModal.ExtModalSign
import ExtModal.ATC_ExtModal ()
import ExtModal.Parse_AS
import ExtModal.Print_AS
import ExtModal.StatAna
import ExtModal.MorphismExtension
import CASL.Sign
import CASL.Morphism
import CASL.SymbolMapAnalysis
import CASL.AS_Basic_CASL
import CASL.MapSentence
import CASL.Parse_AS_Basic
import CASL.SymbolParser
import CASL.SimplifySen
import CASL.Taxonomy
import CASL.Logic_CASL ()
import Logic.Logic
import qualified Data.Map as Map
data ExtModal = ExtModal deriving Show
instance Language ExtModal where
description _ = unlines
[ "ExtModal is the 'extended modal logic' extension of CASL. "
, "Syntax for ordinary modalities, multi-modal logic, dynamic "
, "logic, graded modal logic, hybrid logic, CTL* and mu-calculus "
, "is provided. Specific modal logics can be optained via "
, "restrictions to sublanguages."
]
type ExtModalSign = Sign EM_FORMULA EModalSign
type ExtModalMorph = Morphism EM_FORMULA EModalSign MorphExtension
type ExtModalFORMULA = FORMULA EM_FORMULA
instance SignExtension EModalSign where
isSubSignExtension = isSubEModalSign
instance Syntax ExtModal EM_BASIC_SPEC SYMB_ITEMS SYMB_MAP_ITEMS where
parse_basic_spec ExtModal = Just $ basicSpec ext_modal_reserved_words
parse_symb_items ExtModal = Just $ symbItems ext_modal_reserved_words
parse_symb_map_items ExtModal =
Just $ symbMapItems ext_modal_reserved_words
-- Modal formula mapping via signature morphism
map_EM_FORMULA :: MapSen EM_FORMULA EModalSign MorphExtension
map_EM_FORMULA morph (BoxOrDiamond choice t_m leq_geq number f pos) =
let new_tm tm = case tm of
Simple_modality sm ->
let mds = mod_map (extended_map morph) in
if Map.member sm mds then Simple_modality (mds Map.! sm) else tm
Composition tm1 tm2 -> Composition (new_tm tm1) (new_tm tm2)
Union tm1 tm2 -> Union (new_tm tm1) (new_tm tm2)
TransitiveClosure tm1 -> TransitiveClosure (new_tm tm1)
Guard frm -> Guard (mapSen map_EM_FORMULA morph frm)
new_f = mapSen map_EM_FORMULA morph f
in BoxOrDiamond choice (new_tm t_m) leq_geq number new_f pos
map_EM_FORMULA morph (Hybrid choice nm f pos) =
let new_nom = case nm of
Nominal nom -> let nms = nom_map (extended_map morph) in
if Map.member nom nms then Nominal (nms Map.! nom) else nm
new_f = mapSen map_EM_FORMULA morph f
in Hybrid choice new_nom new_f pos
map_EM_FORMULA morph (UntilSince choice f1 f2 pos) =
let new_f1 = mapSen map_EM_FORMULA morph f1
new_f2 = mapSen map_EM_FORMULA morph f2
in UntilSince choice new_f1 new_f2 pos
map_EM_FORMULA morph (NextY choice f pos) =
let new_f = mapSen map_EM_FORMULA morph f
in NextY choice new_f pos
map_EM_FORMULA morph (PathQuantification choice f pos) =
let new_f = mapSen map_EM_FORMULA morph f
in PathQuantification choice new_f pos
map_EM_FORMULA morph (StateQuantification t_dir choice f pos) =
let new_f = mapSen map_EM_FORMULA morph f
in StateQuantification t_dir choice new_f pos
map_EM_FORMULA morph (FixedPoint choice p_var f pos) =
let new_f = mapSen map_EM_FORMULA morph f
in FixedPoint choice p_var new_f pos
-- Simplification of formulas - simplifySen for ExtFORMULA
simEMSen :: Sign EM_FORMULA EModalSign -> EM_FORMULA -> EM_FORMULA
simEMSen sign (BoxOrDiamond choice tm leq_geq number f pos) =
BoxOrDiamond choice tm leq_geq number
(simplifySen frmTypeAna simEMSen sign f) pos
simEMSen sign (Hybrid choice nom f pos) =
Hybrid choice nom (simplifySen frmTypeAna simEMSen sign f) pos
simEMSen sign (UntilSince choice f1 f2 pos) =
UntilSince choice (simplifySen frmTypeAna simEMSen sign f1)
(simplifySen frmTypeAna simEMSen sign f2) pos
simEMSen sign (NextY choice f pos) =
NextY choice (simplifySen frmTypeAna simEMSen sign f) pos
simEMSen sign (PathQuantification choice f pos) =
PathQuantification choice (simplifySen frmTypeAna simEMSen sign f) pos
simEMSen sign (StateQuantification t_dir choice f pos) =
StateQuantification t_dir choice
(simplifySen frmTypeAna simEMSen sign f) pos
simEMSen sign (FixedPoint choice p_var f pos) =
FixedPoint choice p_var (simplifySen frmTypeAna simEMSen sign f) pos
instance Sentences ExtModal ExtModalFORMULA ExtModalSign ExtModalMorph Symbol
where
map_sen ExtModal morph = return . mapSen map_EM_FORMULA morph
simplify_sen ExtModal = simplifySen frmTypeAna simEMSen
print_sign ExtModal sig = printSign
(printEModalSign $ simplifySen frmTypeAna simEMSen sig) sig
sym_of ExtModal = symOf
symmap_of ExtModal = morphismToSymbMap
sym_name ExtModal = symName
instance StaticAnalysis ExtModal EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol where
basic_analysis ExtModal = Just basicEModalAnalysis
stat_symb_map_items ExtModal = statSymbMapItems
stat_symb_items ExtModal = statSymbItems
symbol_to_raw ExtModal = symbolToRaw
id_to_raw ExtModal = idToRaw
matches ExtModal = CASL.Morphism.matches
empty_signature ExtModal = emptySign emptyEModalSign
signature_union ExtModal sgn = return . addSig addEModalSign sgn
intersection ExtModal sgn = return . interSig interEModalSign sgn
final_union ExtModal = finalUnion addEModalSign
morphism_union ExtModal = plainMorphismUnion addEModalSign
is_subsig ExtModal = isSubSig isSubEModalSign
subsig_inclusion ExtModal = sigInclusion emptyMorphExtension
generated_sign ExtModal = generatedSign emptyMorphExtension
cogenerated_sign ExtModal = cogeneratedSign emptyMorphExtension
induced_from_morphism ExtModal = inducedFromMorphism emptyMorphExtension
induced_from_to_morphism ExtModal =
inducedFromToMorphism emptyMorphExtension isSubEModalSign
diffEModalSign
theory_to_taxonomy ExtModal = convTaxo
instance Logic ExtModal () EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () where
stability _ = Experimental
empty_proof_tree _ = ()