hets/Comorphisms/CASL2CspCASL.hs

	CASL2CspCASL.hs revision f2c050360525df494e6115073b0edc4c443a847c


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
18861N/A{- |
18861N/AModule      :  $Header$
18861N/ACopyright   :  (c) Till Mossakowski and Uni Bremen 2003
18861N/ALicense     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
18861N/A
18861N/AMaintainer  :  M.Roggenbach@swansea.ac.uk
18861N/AStability   :  provisional
18861N/APortability :  non-portable (imports Logic.Logic)
18861N/A
18861N/AThe embedding comorphism from CASL to CspCASL.
18861N/A-}
18861N/A
18861N/Amodule Comorphisms.CASL2CspCASL where
18861N/A
18861N/Aimport Logic.Logic
18861N/Aimport Logic.Comorphism
18861N/Aimport qualified Data.Map as Map
18861N/A
18861N/A-- CASL
18861N/Aimport CASL.Logic_CASL
18861N/Aimport CASL.Sublogic as SL
18861N/Aimport CASL.Sign
18861N/Aimport CASL.AS_Basic_CASL
18861N/Aimport CASL.Morphism
18861N/A
18861N/A-- CspCASL
18861N/Aimport CspCASL.Logic_CspCASL
18861N/Aimport CspCASL.AS_CspCASL (BASIC_CSP_CASL_SPEC (..))
18861N/Aimport CspCASL.SignCSP
18861N/A
18861N/A-- | The identity of the comorphism
18861N/Adata CASL2CspCASL = CASL2CspCASL deriving (Show)
18861N/A
18861N/Ainstance Language CASL2CspCASL -- default definition is okay
18861N/A
18861N/Ainstance Comorphism CASL2CspCASL
18861N/A               CASL CASL_Sublogics
18861N/A               CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
18861N/A               CASLSign
18861N/A               CASLMor
18861N/A               Symbol RawSymbol ()
18861N/A               CspCASL ()
18861N/A               BASIC_CSP_CASL_SPEC () SYMB_ITEMS SYMB_MAP_ITEMS
18861N/A               CSPSign
18861N/A               CSPMorphism
18861N/A               () () () where
18861N/A    sourceLogic CASL2CspCASL = CASL
18861N/A    sourceSublogic CASL2CspCASL = SL.top
18861N/A    targetLogic CASL2CspCASL = CspCASL
18861N/A    mapSublogic CASL2CspCASL _ = ()
18861N/A    map_theory CASL2CspCASL = return . simpleTheoryMapping mapSig (const ())
18861N/A    map_morphism CASL2CspCASL = return . mapMor
18861N/A    map_sentence CASL2CspCASL _sig = return . (const ()) -- toSentence sig
18861N/A    map_symbol = errMapSymbol -- Set.singleton . mapSym
18861N/A    has_model_expansion CASL2CspCASL = True
18861N/A    is_weakly_amalgamable CASL2CspCASL = True
18861N/A
18861N/AmapSig :: CASLSign -> CSPSign
18861N/AmapSig sign =
18861N/A     (emptySign emptyCSPAddSign) {sortSet = sortSet sign
18861N/A               , sortRel = sortRel sign
18861N/A               , opMap = opMap sign
18861N/A               , assocOps = assocOps sign
18861N/A               , predMap = predMap sign }
18861N/A
18861N/AmapMor :: CASLMor -> CSPMorphism
18861N/AmapMor m = Morphism {msource = mapSig $ msource m
18861N/A                   , mtarget = mapSig $ mtarget m
18861N/A                   , sort_map = sort_map m
18861N/A                   , fun_map = fun_map m
18861N/A                   , pred_map = pred_map m
18861N/A                   , extended_map =
18861N/A                       CSPAddMorphism { channelMap = Map.empty,
18861N/A                                        processMap = Map.empty
18861N/A                    }}
18861N/A
18861N/A