CASL2HasCASL.hs revision 1230de6014625bfe0585d50eaf8c5340e088137a
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
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian MaederModule : $Header$
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerCopyright : (c) Till Mossakowski and Uni Bremen 2003
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian MaederLicence : All rights reserved.
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian MaederMaintainer : hets@tzi.de
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian MaederStability : provisional
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian MaederPortability : non-portable (imports Logic.Logic)
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian Maeder The embedding comorphism from CASL to HasCASL.
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maederimport qualified Common.Lib.Map as Map
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder-- | The identity of the comorphism
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maederdata CASL2HasCASL = CASL2HasCASL deriving (Show)
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maederinstance Language CASL2HasCASL -- default definition is okay
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maedertycon_CASL2HasCASL :: TyCon
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maedertycon_CASL2HasCASL = mkTyCon "G_sign"
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maederinstance Typeable CASL2HasCASL where
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maeder typeOf _ = mkAppTy tycon_CASL2HasCASL []
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maederinstance Comorphism CASL2HasCASL
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder BASIC_SPEC Sentence SYMB_ITEMS SYMB_MAP_ITEMS
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maeder CASL.Morphism.Symbol CASL.Morphism.RawSymbol ()
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder HasCASL HasCASL_Sublogics
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maeder BasicSpec Term SymbItems SymbMapItems
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder HasCASL.Morphism.Symbol HasCASL.Morphism.RawSymbol () where
ab0274ab68a174d3e92235b4c4ca865c03901583Christian Maeder sourceLogic _ = CASL
ab0274ab68a174d3e92235b4c4ca865c03901583Christian Maeder sourceSublogic _ = CASL_SL
ab0274ab68a174d3e92235b4c4ca865c03901583Christian Maeder { has_sub = False, -- no subsorting in HasCASL yet...
ab0274ab68a174d3e92235b4c4ca865c03901583Christian Maeder has_part = True,
ab0274ab68a174d3e92235b4c4ca865c03901583Christian Maeder has_cons = True,
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder has_eq = True,
ab0274ab68a174d3e92235b4c4ca865c03901583Christian Maeder has_pred = True,
ab0274ab68a174d3e92235b4c4ca865c03901583Christian Maeder which_logic = FOL
ab0274ab68a174d3e92235b4c4ca865c03901583Christian Maeder targetLogic _ = HasCASL
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder targetSublogic _ = ()
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder map_sign _ = mapSignature
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder --map_morphism _ morphism1 -> Maybe morphism2
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder --map_sentence _ sign1 -> sentence1 -> Maybe sentence2
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder --map_symbol :: cid -> symbol1 -> Set symbol2
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian MaedersortTypeinfo :: TypeInfo
9f93b2a8b552789cd939d599504d39732672dc84Christian MaedersortTypeinfo = TypeInfo { typeKind = star,
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder otherTypeKinds = [],
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maeder superTypes = [],
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maeder typeDefn = NoTypeDefn
9f93b2a8b552789cd939d599504d39732672dc84Christian MaedermakeType :: Id -> HasCASL.As.Type
9f93b2a8b552789cd939d599504d39732672dc84Christian MaedermakeType i = TypeName i star 0
ab0274ab68a174d3e92235b4c4ca865c03901583Christian MaedertrOpType :: CASL.StaticAna.OpType -> HasCASL.Le.OpInfo
9f93b2a8b552789cd939d599504d39732672dc84Christian MaedertrOpType ot = OpInfo { opType = simpleTypeScheme t,
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maeder opAttrs = [],
ab0274ab68a174d3e92235b4c4ca865c03901583Christian Maeder opDefn = NoOpDefn Op
d3f192025f2836285d9705a959542350e057f281Christian Maeder where t = if null args then res
df15a183ca8bf1c25db69775979905198d7cc8bbChristian Maeder else FunType arg arrow res []
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder arrow = case opKind ot of
df15a183ca8bf1c25db69775979905198d7cc8bbChristian Maeder args = map makeType $ opArgs ot
df15a183ca8bf1c25db69775979905198d7cc8bbChristian Maeder arg = if isSingle args then head args else
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder ProductType args []
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder res = makeType $ opRes ot
df15a183ca8bf1c25db69775979905198d7cc8bbChristian MaedertrPredType :: CASL.StaticAna.PredType -> HasCASL.Le.OpInfo
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian MaedertrPredType pt = OpInfo { opType = simpleTypeScheme t,
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder opAttrs = [],
66ea26416f702f5e00759ffc767f0f785cc86058Christian Maeder opDefn = NoOpDefn Pred
df15a183ca8bf1c25db69775979905198d7cc8bbChristian Maeder where t = if null args then logicalType else
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder args = map makeType $ predArgs pt
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder arg = if isSingle args then head args else
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder ProductType args []
df15a183ca8bf1c25db69775979905198d7cc8bbChristian MaedermapSignature :: CASL.StaticAna.Sign -> Maybe(HasCASL.Le.Env,[Term])
499b6cb3ab95a336a324545123e18f387ee4d2a3Christian MaedermapSignature sign = Just (initialEnv {
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder typeMap = Map.fromList $ map (\s -> (s,sortTypeinfo))
d3f192025f2836285d9705a959542350e057f281Christian Maeder $ Set.toList $ sortSet sign,
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder assumps = Map.map OpInfos $ Map.unionWith (++) opmap predmap }, [])
d3f192025f2836285d9705a959542350e057f281Christian Maeder opmap = Map.map (map trOpType . Set.toList) $ opMap sign
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder predmap = Map.map (map trPredType . Set.toList) $ predMap sign