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
{- |
Module : $Header$
Copyright : (c) Till Mossakowski and Uni Bremen 2003
Licence : All rights reserved.
Maintainer : hets@tzi.de
Stability : provisional
Portability : non-portable (imports Logic.Logic)
The embedding comorphism from CASL to HasCASL.
-}
module Comorphisms.CASL2HasCASL where
import Logic.Logic
import Logic.Comorphism
import Common.Id
import qualified Common.Lib.Map as Map
import Common.Lib.Set as Set
import Data.Dynamic
-- CASL
import CASL.Logic_CASL
import CASL.AS_Basic_CASL
import CASL.Sublogic
import CASL.StaticAna
import CASL.Morphism
import HasCASL.Logic_HasCASL
import HasCASL.As
import HasCASL.Le
import HasCASL.Symbol
import HasCASL.Morphism
-- | The identity of the comorphism
data CASL2HasCASL = CASL2HasCASL deriving (Show)
instance Language CASL2HasCASL -- default definition is okay
tycon_CASL2HasCASL :: TyCon
tycon_CASL2HasCASL = mkTyCon "G_sign"
instance Typeable CASL2HasCASL where
typeOf _ = mkAppTy tycon_CASL2HasCASL []
instance Comorphism CASL2HasCASL
BASIC_SPEC Sentence SYMB_ITEMS SYMB_MAP_ITEMS
Sign
HasCASL HasCASL_Sublogics
BasicSpec Term SymbItems SymbMapItems
sourceLogic _ = CASL
sourceSublogic _ = CASL_SL
{ has_sub = False, -- no subsorting in HasCASL yet...
has_part = True,
has_cons = True,
has_eq = True,
has_pred = True,
which_logic = FOL
}
targetLogic _ = HasCASL
targetSublogic _ = ()
map_sign _ = mapSignature
--map_morphism _ morphism1 -> Maybe morphism2
--map_sentence _ sign1 -> sentence1 -> Maybe sentence2
--map_symbol :: cid -> symbol1 -> Set symbol2
sortTypeinfo :: TypeInfo
sortTypeinfo = TypeInfo { typeKind = star,
otherTypeKinds = [],
superTypes = [],
typeDefn = NoTypeDefn
}
makeType :: Id -> HasCASL.As.Type
makeType i = TypeName i star 0
trOpType :: CASL.StaticAna.OpType -> HasCASL.Le.OpInfo
trOpType ot = OpInfo { opType = simpleTypeScheme t,
opAttrs = [],
opDefn = NoOpDefn Op
}
where t = if null args then res
else FunType arg arrow res []
arrow = case opKind ot of
CASL.StaticAna.Total -> FunArr
CASL.StaticAna.Partial -> PFunArr
args = map makeType $ opArgs ot
arg = if isSingle args then head args else
ProductType args []
res = makeType $ opRes ot
trPredType :: CASL.StaticAna.PredType -> HasCASL.Le.OpInfo
trPredType pt = OpInfo { opType = simpleTypeScheme t,
opAttrs = [],
opDefn = NoOpDefn Pred
}
where t = if null args then logicalType else
predType arg
args = map makeType $ predArgs pt
arg = if isSingle args then head args else
ProductType args []
mapSignature :: CASL.StaticAna.Sign -> Maybe(HasCASL.Le.Env,[Term])
mapSignature sign = Just (initialEnv {
classMap = Map.empty,
typeMap = Map.fromList $ map (\s -> (s,sortTypeinfo))
$ Set.toList $ sortSet sign,
assumps = Map.map OpInfos $ Map.unionWith (++) opmap predmap }, [])
where
opmap = Map.map (map trOpType . Set.toList) $ opMap sign
predmap = Map.map (map trPredType . Set.toList) $ predMap sign