hets/Comorphisms/CspCASL2Modal.hs

	CspCASL2Modal.hs revision e54c5af823b9775dd2c058185ea5bdf7593950fa


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
0N/A{- |
0N/AModule      :  $Header$
0N/ACopyright   :  (c) Till Mossakowski and Uni Bremen 2004
292N/ALicense     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
0N/A
0N/AMaintainer  :  till@informatik.uni-bremen.de
0N/AStability   :  provisional
0N/APortability :  non-portable (imports Logic.Logic)
292N/A
292N/AThe embedding comorphism from CspCASL to ModalCASL.
292N/A   It keeps the CASL part and interprets the CspCASL LTS semantics as
292N/A   Kripke structure
0N/A-}
0N/A
0N/Amodule Comorphisms.CspCASL2Modal where
292N/A
292N/Aimport Logic.Logic
292N/Aimport Logic.Comorphism
292N/Aimport qualified Data.Set as Set
292N/Aimport Common.Id
292N/A
292N/A-- CASL
292N/Aimport CASL.Sign
292N/Aimport CASL.AS_Basic_CASL
292N/Aimport CASL.Morphism
292N/A
0N/A-- CspCASL
0N/Aimport CspCASL.Logic_CspCASL
0N/Aimport CspCASL.SignCSP
0N/Aimport CspCASL.AS_CspCASL (CspBasicSpec (..))
0N/A
0N/A-- ModalCASL
0N/Aimport Modal.Logic_Modal
0N/Aimport Modal.AS_Modal
0N/Aimport Modal.ModalSign
0N/A
0N/A-- | The identity of the comorphism
0N/Adata CspCASL2Modal = CspCASL2Modal deriving (Show)
0N/A
0N/Ainstance Language CspCASL2Modal -- default definition is okay
0N/A
0N/Ainstance Comorphism CspCASL2Modal
0N/A               CspCASL ()
0N/A               CspBasicSpec () SYMB_ITEMS SYMB_MAP_ITEMS
0N/A               CspCASLSign
0N/A               CspMorphism
0N/A               () () ()
0N/A               Modal ()
0N/A               M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
0N/A               MSign
0N/A               ModalMor
0N/A               Symbol RawSymbol () where
0N/A    sourceLogic CspCASL2Modal = CspCASL
0N/A    sourceSublogic CspCASL2Modal = ()
0N/A    targetLogic CspCASL2Modal = Modal
0N/A    mapSublogic CspCASL2Modal _ = Just ()
0N/A    map_theory CspCASL2Modal = return . simpleTheoryMapping mapSig mapSen
0N/A    map_morphism CspCASL2Modal = return . mapMor
0N/A    map_sentence CspCASL2Modal _ = return . mapSen
0N/A    map_symbol CspCASL2Modal = Set.singleton . mapSym
0N/A
0N/AmapSig :: CspCASLSign -> MSign
0N/AmapSig sign =
0N/A     (emptySign emptyModalSign) {sortSet = sortSet sign
0N/A               , sortRel = sortRel sign
0N/A               , opMap = opMap sign
0N/A               , assocOps = assocOps sign
0N/A               , predMap = predMap sign }
0N/A    -- ??? add modalities
0N/A
0N/AmapMor :: CspMorphism -> ModalMor
0N/AmapMor m = Morphism {msource = mapSig $ msource m
0N/A                   , mtarget = mapSig $ mtarget m
                   , sort_map = sort_map m
                   , fun_map = fun_map m
                   , pred_map = pred_map m
                   , extended_map = ()}
    -- ??? add modalities


mapSym :: () -> Symbol
mapSym = error "CspCASL2Modal.mapSym not yet implemented"
   -- needs to be changed once modal symbols are added


mapSen :: () -> ModalFORMULA
mapSen _f = True_atom nullRange

{- case f of
    Quantification q vs frm ps ->
        Quantification q vs (mapSen frm) ps
    Conjunction fs ps ->
        Conjunction (map mapSen fs) ps
    Disjunction fs ps ->
        Disjunction (map mapSen fs) ps
    Implication f1 f2 b ps ->
        Implication (mapSen f1) (mapSen f2) b ps
    Equivalence f1 f2 ps ->
        Equivalence (mapSen f1) (mapSen f2) ps
    Negation frm ps -> Negation (mapSen frm) ps
    True_atom ps -> True_atom ps
    False_atom ps -> False_atom ps
    Existl_equation t1 t2 ps ->
        Existl_equation (mapTERM t1) (mapTERM t2) ps
    Strong_equation t1 t2 ps ->
        Strong_equation (mapTERM t1) (mapTERM t2) ps
    Predication pn as qs ->
        Predication pn (map mapTERM as) qs
    Definedness t ps -> Definedness (mapTERM t) ps
    Membership t ty ps -> Membership (mapTERM t) ty ps
    Sort_gen_ax constrs isFree -> Sort_gen_ax constrs isFree
    _ -> error "CspCASL2Modal.mapSen"

mapTERM :: TERM () -> TERM M_FORMULA
mapTERM t = case t of
    Qual_var v ty ps -> Qual_var v ty ps
    Application opsym as qs  -> Application opsym (map mapTERM as) qs
    Sorted_term trm ty ps -> Sorted_term (mapTERM trm) ty ps
    Cast trm ty ps -> Cast (mapTERM trm) ty ps
    Conditional t1 f t2 ps ->
       Conditional (mapTERM t1) (mapSen f) (mapTERM t2) ps
    _ -> error "CspCASL2Modal.mapTERM"

-}