-
Notifications
You must be signed in to change notification settings - Fork 0
/
JST0P_constrain.hs
257 lines (207 loc) · 10.8 KB
/
JST0P_constrain.hs
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
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
module JST0P_constrain where
import JST0P_types
import JST0_type_aux
import Data.Map as Map
import Debugging
-- Annotated constraints
-- TODO think where we actually need them
data ConstrainAn = Gt [Annotation] [Annotation]
instance Show ConstrainAn where
show (Gt s1 s2) = (show_sum s1) ++ ">=" ++ (show_sum s2) ++ "\n"
-- show a sum represented as the list of summands
show_sum :: [Annotation] -> String
show_sum ([]) = "0"
show_sum [x] = (show x)
show_sum (x:xs) = (show x) ++ "+" ++ (show_sum xs)
----------------------------------------
-- compute constraints to make the resources in t1 less than t2
----------------------------------------
makeLess_Member :: (TypeAn,FieldType) -> (TypeAn,FieldType) -> [ConstrainAn]
makeLess_Member (t1,_f1) (t2,_f2) = makeLess_An t1 t2
makeLess_Members :: MembersAn -> MembersAn -> [ConstrainAn]
makeLess_Members mem1 mem2 = Map.foldrWithKey
(\k t c -> concat [makeLess_Member (membersAn_get mem1 k) t,c])
[]
mem2
makeLess_An :: TypeAn -> TypeAn -> [ConstrainAn]
makeLess_An (t1,n1) (t2,n2) = concat [[Gt [n2] [n1]],makeLess_P t1 t2]
makeLess_P :: TypeP -> TypeP -> [ConstrainAn]
makeLess_P (JST0P_Object a1 mem1) (JST0P_Object a2 mem2) = let
(m1,m2) = equalize_alpha (JST0P_Object a1 mem1) (JST0P_Object a2 mem2)
in makeLess_Members m1 m2
makeLess_P a b = makeEqual_P a b
makeLess_list :: [TypeP] -> [TypeP] -> [ConstrainAn]
makeLess_list as bs = concat (Prelude.zipWith makeLess_P as bs)
----------------------------------------
-- compute constraints to make the resources in t1 more than t2
----------------------------------------
makeMore_Member :: (TypeAn,FieldType) -> (TypeAn,FieldType) -> [ConstrainAn]
makeMore_Member (t1,_f1) (t2,_f2) = makeMore_An t1 t2
--FieldType Relation is already enforced from cg
makeMore_Members :: MembersAn -> MembersAn -> [ConstrainAn]
makeMore_Members mem1 mem2 = Map.foldrWithKey
(\k t c -> concat [makeMore_Member (membersAn_get mem1 k) t,c])
[]
mem2
makeMore_An :: TypeAn -> TypeAn -> [ConstrainAn]
makeMore_An (t1,n1) (t2,n2) = concat [[Gt [n1] [n2]],makeMore_P t1 t2]
makeMore_P :: TypeP -> TypeP -> [ConstrainAn]
makeMore_P (JST0P_Object a1 mem1) (JST0P_Object a2 mem2) = let
(m1,m2) = equalize_alpha (JST0P_Object a1 mem1) (JST0P_Object a2 mem2)
in makeMore_Members m1 m2
makeMore_P a b = makeEqual_P a b
makeMore_list :: [TypeP] -> [TypeP] -> [ConstrainAn]
makeMore_list as bs = concat (Prelude.zipWith makeMore_P as bs)
----------------------------------------
-- compute Constraints to make two types subtypes
----------------------------------------
makeSubtype_FieldType :: FieldType -> FieldType -> [ConstrainAn]
makeSubtype_FieldType a b | isSubtype_FieldType a b = []
makeSubtype_Member :: (TypeAn,FieldType) -> (TypeAn,FieldType) -> [ConstrainAn]
makeSubtype_Member (t1,f1) (t2,f2) = concat [makeSubtype_FieldType f1 f2,makeSubtype_An t1 t2]
makeSubtype_Members :: MembersAn -> MembersAn -> [ConstrainAn]
makeSubtype_Members mem1 mem2 = Map.foldrWithKey
(\k t c -> concat [c,
makeSubtype_Member (membersAn_get mem1 k) t])
[]
mem2
makeSubtype_An :: TypeAn -> TypeAn -> [ConstrainAn]
makeSubtype_An (t1,a1) (t2,a2) = concat [makeSubtype_P t1 t2,[Gt [a1] [a2]]]
makeSubtype_P :: TypeP -> TypeP -> [ConstrainAn]
makeSubtype_P (JST0P_Function o t n tp np) (JST0P_Function o2 t2 n2 tp2 np2) = let
co = makeEqual_P o o2
ct = makeEqual_list t t2
ctp= makeEqual_P tp tp2
cn = [Gt [n2] [n]]
cnp= [Gt [np,n2] [n,np2]]
in concat [co,ct,ctp,cn,cnp]
makeSubtype_P (JST0P_Object a1 mem1) (JST0P_Object a2 mem2) = let
(m1,m2) = equalize_alpha (JST0P_Object a1 mem1) (JST0P_Object a2 mem2)
in makeSubtype_Members m1 m2
makeSubtype_P a b | (a==b) = []
-- makeSubtype_P (JST0P_Alpha (Gamma a1)) (JST0P_Object (Beta a2) _)| (a1 == a2) = []
-- makeSubtype_P (JST0P_Object (Beta a2) _) (JST0P_Alpha (Gamma a1))| (a1 == a2) = []
makeSubtype_list :: [TypeP] -> [TypeP] -> [ConstrainAn]
makeSubtype_list [] [] = []
makeSubtype_list (x:xs) (y:ys) = let
c = makeSubtype_P x y
cs = makeSubtype_list xs ys
in concat [c,cs]
----------------------------------------
-- compute Contraints to make the resources in t1 equal to those in t2,
-- In the Theory that is noted as SubSet^EQ
----------------------------------------
makeEqual_Member :: (TypeAn,FieldType) -> (TypeAn,FieldType) -> [ConstrainAn]
makeEqual_Member (t1,_f1) (t2,_f2) = makeEqual_An t1 t2
-- The fieldType has already been verified in the first step of the inference
makeEqual_Members :: MembersAn -> MembersAn -> [ConstrainAn]
makeEqual_Members mem1 mem2 = Map.foldrWithKey
(\k t c -> concat[makeEqual_Member (membersAn_get mem1 k) t,c])
[]
mem2
makeEqual_An :: TypeAn -> TypeAn -> [ConstrainAn]
makeEqual_An (t1,a1) (t2,a2) = concat [[Gt [a1] [a2],Gt [a2] [a1]],makeEqual_P t1 t2]
makeEqual_P :: TypeP -> TypeP -> [ConstrainAn]
makeEqual_P t1 t2 | trace 30 ("makeEqual_P " ++ show t1 ++ " <-> " ++ show t2) False = undefined
makeEqual_P (JST0P_Object a1 mem1) (JST0P_Object a2 mem2) = let
(m1,m2) = equalize_alpha (JST0P_Object a1 mem1) (JST0P_Object a2 mem2)
in makeEqual_Members m1 m2
makeEqual_P (JST0P_Function o1 t1 n1 tp1 np1) (JST0P_Function o2 t2 n2 tp2 np2) = let
co = makeEqual_P o1 o2
ct = makeEqual_list t1 t2
ctp = makeEqual_P tp1 tp2
cn = [Gt [n1] [n2],Gt [n2] [n1],
Gt [np1] [np2],Gt [np2] [np1]]
in concat[cn,co,ct,ctp]
makeEqual_P a b | (a==b) = []
| otherwise = undefined
makeEqual_list :: [TypeP] -> [TypeP] -> [ConstrainAn]
makeEqual_list as bs = concat (Prelude.zipWith makeEqual_P as bs)
----------------------------------------
-- Compute set of Constraints to make the two types identical
----------------------------------------
makeIdentical_An :: TypeAn -> TypeAn -> [ConstrainAn]
makeIdentical_An (t1,a1) (t2,a2) = concat [[Gt [a1] [a2],Gt [a2] [a1]],makeIdentical_P t1 t2]
makeIdentical_Member :: (TypeAn,FieldType) -> (TypeAn,FieldType) -> [ConstrainAn]
makeIdentical_Member (t1,_f1) (t2,_f2) = makeIdentical_An t1 t2
-- The fieldType has already been verified in the first step of the inference
makeIdentical_Members :: MembersAn -> MembersAn -> [ConstrainAn]
makeIdentical_Members mem1 mem2 | Map.size mem1 == Map.size mem2 =
Map.foldrWithKey
(\k t c -> concat[makeIdentical_Member (membersAn_get mem1 k) t,c])
[]
mem2
| otherwise = undefined
makeIdentical_P :: TypeP -> TypeP -> [ConstrainAn]
makeIdentical_P t1 t2 | trace 30 ("makeIdentical_P " ++ show t1 ++ " <-> " ++ show t2) False = undefined
makeIdentical_P (JST0P_Object a1 mem1) (JST0P_Object a2 mem2) = let
(m1,m2) = equalize_alpha (JST0P_Object a1 mem1) (JST0P_Object a2 mem2)
in makeIdentical_Members m1 m2
makeIdentical_P (JST0P_Function o1 t1 n1 tp1 np1) (JST0P_Function o2 t2 n2 tp2 np2) = let
co = makeIdentical_P o1 o2
ct = makeIdentical_list t1 t2
ctp = makeIdentical_P tp1 tp2
cn = [Gt [n1] [n2],Gt [n2] [n1],
Gt [np1] [np2],Gt [np2] [np1]]
in concat[cn,co,ct,ctp]
makeIdentical_P a b | (a==b) = []
| otherwise = undefined
makeIdentical_list :: [TypeP] -> [TypeP] -> [ConstrainAn]
makeIdentical_list as bs = concat (Prelude.zipWith makeIdentical_P as bs)
----------------------------------------
-- Compute set of Constraints to make the three types match the Split definition
----------------------------------------
--makeSplit_FieldType :: FieldType -> FieldType -> FieldType -> [ConstrainAn]
--makeSplit_FieldType Definite Definite Definite = []
--makeSplit_FieldType _ _ Potential = []
makeSplit_Member :: (TypeAn,FieldType) -> (TypeAn,FieldType) -> (TypeAn,FieldType) -> [ConstrainAn]
makeSplit_Member (t1,f1) (t2,f2) (t3,f3) | f1 == f2 && f2==f3 = makeSplit_An t1 t2 t3
makeSplit_P :: TypeP -> TypeP -> TypeP -> [ConstrainAn]
makeSplit_P t1 t2 t3 | trace 30 ("makeSplitP " ++ show t1 ++ "+" ++ show t2 ++ "=" ++ show t3) False = undefined
makeSplit_P (JST0P_Object a1 mem1) (JST0P_Object a2 mem2) (JST0P_Object a3 mem3) = let
(m1,m2,m3) = equalize_alpha3 (JST0P_Object a1 mem1) (JST0P_Object a2 mem2) (JST0P_Object a3 mem3)
in makeSplit_Members m1 m2 m3
makeSplit_P t1 t2 t3 = concat [makeIdentical_P t1 t2,makeIdentical_P t2 t3]
makeSplit_An :: TypeAn -> TypeAn -> TypeAn -> [ConstrainAn]
makeSplit_An (t1,n1) (t2,n2) (t3,n3) = concat [makeSplit_P t1 t2 t3,[Gt [n1,n2] [n3],Gt [n3] [n1,n2]]]
makeSplit_Members :: MembersAn -> MembersAn -> MembersAn -> [ConstrainAn]
makeSplit_Members mem1 mem2 mem3 | ((Map.keysSet mem1) == (Map.keysSet mem2)) && ((Map.keysSet mem2) == (Map.keysSet mem3)) =
Map.foldrWithKey
(\k t c -> concat[c,
makeSplit_Member (membersAn_get mem1 k) (membersAn_get mem2 k) t])
[]
mem3
----------------------------------------
-- Compute set of Constraints to make the three types match the minimum Relation
----------------------------------------
makeMin_FieldType :: FieldType -> FieldType -> FieldType -> [ConstrainAn]
makeMin_FieldType Definite Definite Definite = []
makeMin_FieldType _ _ Potential = []
makeMin_Member :: (TypeAn,FieldType) -> (TypeAn,FieldType) -> (TypeAn,FieldType) -> [ConstrainAn]
makeMin_Member (t1,f1) (t2,f2) (t3,f3) = concat [makeMin_An t1 t2 t3,makeMin_FieldType f1 f2 f3]
makeMin_Members :: MembersAn -> MembersAn -> MembersAn -> [ConstrainAn]
makeMin_Members mem1 mem2 mem3 | ((Map.keysSet mem1) == (Map.keysSet mem2)) && ((Map.keysSet mem2) == (Map.keysSet mem3)) =
Map.foldrWithKey
(\k t c -> concat [c,
makeMin_Member (membersAn_get mem1 k) (membersAn_get mem2 k) t])
[]
mem3
makeMin_An :: TypeAn -> TypeAn -> TypeAn -> [ConstrainAn]
makeMin_An (t1,n1) (t2,n2) (t3,n3) = concat [makeMin_P t1 t2 t3,[Gt [n2] [n3],Gt [n1] [n3]]]
makeMin_P :: TypeP -> TypeP -> TypeP -> [ConstrainAn]
makeMin_P (JST0P_Object a1 mem1) (JST0P_Object a2 mem2) (JST0P_Object a3 mem3) = let
(m1,m2,m3) = equalize_alpha3 (JST0P_Object a1 mem1) (JST0P_Object a2 mem2) (JST0P_Object a3 mem3)
in makeMin_Members m1 m2 m3
makeMin_P t1 t2 t3 | (t1==t2) && (t2==t3) = []
| error ("Minimum of not compatible types required") = undefined
| otherwise = undefined
----------------------------------------
-- Compute a set of constraints that guarantees, that the given type does not hold any resource tickets
----------------------------------------
makeEmpty_P :: TypeP -> [ConstrainAn]
makeEmpty_P (JST0P_Object _alpha mem) = makeEmpty_Members mem
makeEmpty_P _ = []
makeEmpty_An :: TypeAn -> [ConstrainAn]
makeEmpty_An (t,n) = concat [[Gt [I 0] [n]],makeEmpty_P t]
makeEmpty_Members :: MembersAn -> [ConstrainAn]
makeEmpty_Members mem = Map.fold (\(t,_ft) r -> concat [r,makeEmpty_An t]) [] mem