Cross Reference: /hets/Comorphisms/CASL2HasCASL.hs
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
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder{- |
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian MaederModule : $Header$
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerCopyright : (c) Till Mossakowski and Uni Bremen 2003
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian MaederLicence : All rights reserved.
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian Maeder
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian MaederMaintainer : hets@tzi.de
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian MaederStability : provisional
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian MaederPortability : non-portable (imports Logic.Logic)
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian Maeder
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian Maeder
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian Maeder The embedding comorphism from CASL to HasCASL.
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian Maeder
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maeder-}
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maeder
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maedermodule Comorphisms.CASL2HasCASL where
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder
9f93b2a8b552789cd939d599504d39732672dc84Christian Maederimport Logic.Logic
38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maederimport Logic.Comorphism
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maederimport Common.Id
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maederimport qualified Common.Lib.Map as Map
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maederimport Common.Lib.Set as Set
ab0274ab68a174d3e92235b4c4ca865c03901583Christian Maederimport Data.Dynamic
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maeder
d3f192025f2836285d9705a959542350e057f281Christian Maeder-- CASL
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maederimport CASL.Logic_CASL
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maederimport CASL.AS_Basic_CASL
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maederimport CASL.Sublogic
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maederimport CASL.StaticAna
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maederimport CASL.Morphism
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maederimport HasCASL.Logic_HasCASL
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maederimport HasCASL.As
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maederimport HasCASL.Le
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maederimport HasCASL.Symbol
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maederimport HasCASL.Morphism
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder-- | The identity of the comorphism
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maederdata CASL2HasCASL = CASL2HasCASL deriving (Show)
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maeder
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maederinstance Language CASL2HasCASL -- default definition is okay
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maedertycon_CASL2HasCASL :: TyCon
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maedertycon_CASL2HasCASL = mkTyCon "G_sign"
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maederinstance Typeable CASL2HasCASL where
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maeder typeOf _ = mkAppTy tycon_CASL2HasCASL []
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maederinstance Comorphism CASL2HasCASL
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maeder CASL CASL.Sublogic.CASL_Sublogics
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder BASIC_SPEC Sentence SYMB_ITEMS SYMB_MAP_ITEMS
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maeder Sign
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maeder CASL.Morphism.Morphism
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maeder CASL.Morphism.Symbol CASL.Morphism.RawSymbol ()
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder HasCASL HasCASL_Sublogics
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maeder BasicSpec Term SymbItems SymbMapItems
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maeder HasCASL.Le.Env
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder HasCASL.Morphism.Morphism
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 }
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
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian MaedersortTypeinfo :: TypeInfo
9f93b2a8b552789cd939d599504d39732672dc84Christian MaedersortTypeinfo = TypeInfo { typeKind = star,
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder otherTypeKinds = [],
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maeder superTypes = [],
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maeder typeDefn = NoTypeDefn
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder }
9f93b2a8b552789cd939d599504d39732672dc84Christian MaedermakeType :: Id -> HasCASL.As.Type
9f93b2a8b552789cd939d599504d39732672dc84Christian MaedermakeType i = TypeName i star 0
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maeder
ab0274ab68a174d3e92235b4c4ca865c03901583Christian MaedertrOpType :: CASL.StaticAna.OpType -> HasCASL.Le.OpInfo
9f93b2a8b552789cd939d599504d39732672dc84Christian MaedertrOpType ot = OpInfo { opType = simpleTypeScheme t,
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maeder opAttrs = [],
ab0274ab68a174d3e92235b4c4ca865c03901583Christian Maeder opDefn = NoOpDefn Op
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder }
d3f192025f2836285d9705a959542350e057f281Christian Maeder where t = if null args then res
df15a183ca8bf1c25db69775979905198d7cc8bbChristian Maeder else FunType arg arrow res []
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder arrow = case opKind ot of
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder CASL.StaticAna.Total -> FunArr
d3f192025f2836285d9705a959542350e057f281Christian Maeder CASL.StaticAna.Partial -> PFunArr
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
38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder
df15a183ca8bf1c25db69775979905198d7cc8bbChristian MaedertrPredType :: CASL.StaticAna.PredType -> HasCASL.Le.OpInfo
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian MaedertrPredType pt = OpInfo { opType = simpleTypeScheme t,
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder opAttrs = [],
66ea26416f702f5e00759ffc767f0f785cc86058Christian Maeder opDefn = NoOpDefn Pred
d3f192025f2836285d9705a959542350e057f281Christian Maeder }
df15a183ca8bf1c25db69775979905198d7cc8bbChristian Maeder where t = if null args then logicalType else
df15a183ca8bf1c25db69775979905198d7cc8bbChristian Maeder predType arg
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder args = map makeType $ predArgs pt
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder arg = if isSingle args then head args else
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder ProductType args []
d3f192025f2836285d9705a959542350e057f281Christian Maeder
df15a183ca8bf1c25db69775979905198d7cc8bbChristian MaedermapSignature :: CASL.StaticAna.Sign -> Maybe(HasCASL.Le.Env,[Term])
499b6cb3ab95a336a324545123e18f387ee4d2a3Christian MaedermapSignature sign = Just (initialEnv {
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder classMap = Map.empty,
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 }, [])
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder where
d3f192025f2836285d9705a959542350e057f281Christian Maeder opmap = Map.map (map trOpType . Set.toList) $ opMap sign
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder predmap = Map.map (map trPredType . Set.toList) $ predMap sign
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder