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
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
|
implementation module checkKindCorrectness
import StdEnv
import syntax, containers, checksupport, utilities
//import RWSDebug
checkKindCorrectness :: !Index !Index IndexRange !{#CommonDefs} !Int !u:{# FunDef} !*{#DclModule} !*TypeVarHeap !*TypeDefInfos !*ErrorAdmin
-> (!u:{# FunDef}, !*{#DclModule}, !*TypeVarHeap, !*TypeDefInfos, !*ErrorAdmin)
checkKindCorrectness main_dcl_module_n first_uncached_function icl_instances common_defs n_cached_dcl_modules fun_defs dcl_mods th_vars td_infos error_admin
#! n_fun_defs = size fun_defs
size_dcl_mods = size dcl_mods
# (dcl_mods, th_vars, td_infos, error_admin)
= iFoldSt (\mod_index state
-> if (mod_index<n_cached_dcl_modules)
state
(check_classes mod_index state))
0 size_dcl_mods (dcl_mods, th_vars, td_infos, error_admin)
icl_common_defs
= common_defs.[main_dcl_module_n]
(_, th_vars, td_infos, error_admin)
= foldrArraySt (check_class icl_common_defs.com_member_defs)
icl_common_defs.com_class_defs
([], th_vars, td_infos, error_admin)
bv_uninitialized_mods = bitvectSetFirstN n_cached_dcl_modules (bitvectCreate size_dcl_mods)
(bv_uninitialized_mods, th_vars, td_infos, error_admin)
= iFoldSt (\mod_index state
-> if (mod_index<n_cached_dcl_modules)
state
(check_instances_and_class_and_member_contexts
common_defs common_defs.[mod_index] state))
0 size_dcl_mods (bv_uninitialized_mods, th_vars, td_infos, error_admin)
// check_icl_function: don't check the types that were generated for instances
state
= iFoldSt (check_icl_function common_defs) first_uncached_function /* 0 */ icl_instances.ir_from
(fun_defs, bv_uninitialized_mods, th_vars, td_infos, error_admin)
(fun_defs, bv_uninitialized_mods, th_vars, td_infos, error_admin)
= iFoldSt (check_icl_function common_defs) icl_instances.ir_to n_fun_defs state
(dcl_mods, bv_uninitialized_mods, th_vars, td_infos, error_admin)
= iFoldSt (\mod_index state
-> if (mod_index<n_cached_dcl_modules || mod_index==main_dcl_module_n)
state
(check_dcl_functions common_defs mod_index state))
0 size_dcl_mods
(dcl_mods, bv_uninitialized_mods, th_vars, td_infos, error_admin)
= (fun_defs, dcl_mods, th_vars, td_infos, error_admin)
where
check_classes mod_index (dcl_mods, th_vars, td_infos, error_admin)
# (dcl_mod, dcl_mods)
= dcl_mods![mod_index]
{com_class_defs, com_member_defs}
= dcl_mod.dcl_common
(class_defs_with_cacheable_kind_info, th_vars, td_infos, error_admin)
= foldrArraySt (check_class com_member_defs) com_class_defs
([], th_vars, td_infos, error_admin)
dcl_mods
= { dcl_mods & [mod_index].dcl_common.com_class_defs
= { el \\ el <- class_defs_with_cacheable_kind_info }}
= (dcl_mods, th_vars, td_infos, error_admin)
check_class com_member_defs class_def=:{class_name, class_args, class_members}
(class_defs_accu, th_vars, td_infos, error_admin)
# th_vars
= init_type_vars class_args th_vars
(th_vars, td_infos, error_admin)
= foldlArraySt (\{ds_index} state
-> check_member_without_context class_args
com_member_defs.[ds_index] state)
class_members (th_vars, td_infos, error_admin)
(derived_kinds, th_vars)
= mapFilterYesSt get_opt_kind class_args th_vars
= ([{ class_def & class_arg_kinds = derived_kinds }:class_defs_accu], th_vars, td_infos, error_admin)
check_member_without_context class_args
{me_symb, me_pos, me_class_vars, me_type=me_type=:{st_vars, st_args, st_result}}
(th_vars, td_infos, error_admin)
# error_admin
= setErrorAdmin (newPosition me_symb me_pos) error_admin
th_vars
= init_type_vars st_vars th_vars
th_vars
= fold2St copy_TVI class_args me_class_vars th_vars
(th_vars, td_infos, error_admin)
= unsafeFold2St (check_atype KindConst)
[0..] [st_result:st_args] (th_vars, td_infos, error_admin)
th_vars
= fold2St copy_TVI me_class_vars class_args th_vars
= (th_vars, td_infos, error_admin)
where
copy_TVI src dst th_vars
# (tvi, th_vars)
= readPtr src.tv_info_ptr th_vars
= writePtr dst.tv_info_ptr tvi th_vars
check_instances_and_class_and_member_contexts common_defs
{com_instance_defs, com_class_defs, com_member_defs} state
# state
= foldlArraySt (check_instance common_defs) com_instance_defs state
state
= foldlArraySt
(check_class_context_and_member_contexts common_defs com_member_defs)
com_class_defs state
= state
check_instance common_defs {ins_is_generic, ins_class, ins_ident, ins_pos, ins_type}
(bv_uninitialized_mods, th_vars, td_infos, error_admin)
| ins_is_generic
// kind correctness of user supplied generic instances
// is checked during generic phase
= (bv_uninitialized_mods, th_vars, td_infos, error_admin)
# (expected_kinds, bv_uninitialized_mods, th_vars)
= get_expected_kinds ins_class common_defs bv_uninitialized_mods th_vars
error_admin
= setErrorAdmin (newPosition ins_ident ins_pos) error_admin
th_vars
= init_type_vars ins_type.it_vars th_vars
(th_vars, td_infos, error_admin)
= unsafeFold3St possibly_check_type expected_kinds [1..]
ins_type.it_types (th_vars, td_infos, error_admin)
state
= foldSt (check_context common_defs) ins_type.it_context
(bv_uninitialized_mods, th_vars, td_infos, error_admin)
= state
get_expected_kinds class_index=:{glob_module, glob_object} common_defs bv_uninitialized_mods th_vars
| bitvectSelect glob_module bv_uninitialized_mods
// ---> ("get_expected_kinds", glob_module)
/* the desired class is defined in a module which is a cached one
=> check_classes has not been called for all the classes
within that module
=> the kind information for the class args is not in the heap
=> put it in the heap now
*/
# th_vars
= foldlArraySt write_kind_info common_defs.[glob_module].com_class_defs th_vars
= get_expected_kinds class_index common_defs (bitvectReset glob_module bv_uninitialized_mods)
th_vars
# {class_args, class_arg_kinds}
= common_defs.[glob_module].com_class_defs.[glob_object.ds_index]
(expected_kinds, th_vars)
= mapSt get_tvi class_args th_vars
= (expected_kinds, bv_uninitialized_mods, th_vars)
write_kind_info {class_name, class_args, class_arg_kinds} th_vars
= write_ki class_args class_arg_kinds th_vars
write_ki [{tv_info_ptr}:class_args] [class_arg_kind:class_arg_kinds] th_vars
= write_ki class_args class_arg_kinds (writePtr tv_info_ptr (TVI_Kind class_arg_kind) th_vars)
write_ki [{tv_info_ptr}:class_args] [] th_vars
= write_ki class_args [] (writePtr tv_info_ptr TVI_Empty th_vars)
write_ki [] [] th_vars
= th_vars
possibly_check_type TVI_Empty _ _ state
// This can happen for stooopid classes like StdClass::Ord, where the member type is ignored at all
= state
possibly_check_type (TVI_Kind expected_kind) arg_nr type state
= check_type expected_kind arg_nr type state
check_class_context_and_member_contexts common_defs com_member_defs
{class_name, class_pos, class_context, class_members, class_args}
(bv_uninitialized_mods, th_vars, td_infos, error_admin)
# error_admin
= setErrorAdmin (newPosition class_name class_pos) error_admin
state
= foldSt (check_context common_defs) class_context
(bv_uninitialized_mods, th_vars, td_infos, error_admin)
state
= foldlArraySt (check_member_context common_defs com_member_defs)
class_members state
= state
check_member_context common_defs com_member_defs {ds_index}
(bv_uninitialized_mods, th_vars, td_infos, error_admin)
# {me_symb, me_pos, me_type}
= com_member_defs.[ds_index]
error_admin
= setErrorAdmin (newPosition me_symb me_pos) error_admin
= foldSt (check_context common_defs) me_type.st_context
(bv_uninitialized_mods, th_vars, td_infos, error_admin)
get_tvi {tv_info_ptr} th_vars
= readPtr tv_info_ptr th_vars
get_opt_kind {tv_info_ptr} th_vars
# (tvi, th_vars)
= readPtr tv_info_ptr th_vars
#! opt_kind
= case tvi of
TVI_Kind kind -> Yes kind
_ -> No
= (opt_kind, th_vars)
check_icl_function common_defs fun_n
(fun_defs, bv_uninitialized_mods, th_vars, td_infos, error_admin)
# (fun_def, fun_defs) = fun_defs![fun_n]
= case fun_def.fun_type of
No
-> (fun_defs, bv_uninitialized_mods, th_vars, td_infos, error_admin)
Yes st
# (bv_uninitialized_mods, th_vars, td_infos, error_admin)
= check_symbol_type common_defs fun_def.fun_symb fun_def.fun_pos
st (bv_uninitialized_mods, th_vars, td_infos, error_admin)
-> (fun_defs, bv_uninitialized_mods, th_vars, td_infos, error_admin)
check_dcl_functions common_defs mod_index
(dcl_mods, bv_uninitialized_mods, th_vars, td_infos, error_admin)
# ({dcl_functions, dcl_instances, dcl_macros}, dcl_mods)
= dcl_mods![mod_index]
(bv_uninitialized_mods, th_vars, td_infos, error_admin)
= iFoldSt (\i state
-> if (in_index_range i dcl_instances || in_index_range i dcl_macros) // yawn
state
(let ({ft_symb, ft_pos, ft_type}) = dcl_functions.[i]
in check_symbol_type common_defs ft_symb ft_pos ft_type
state))
0 (size dcl_functions) (bv_uninitialized_mods, th_vars, td_infos, error_admin)
= (dcl_mods, bv_uninitialized_mods, th_vars, td_infos, error_admin)
check_symbol_type common_defs fun_symb fun_pos
st=:{st_vars, st_args, st_result, st_context}
(bv_uninitialized_mods, th_vars, td_infos, error_admin)
# error_admin
= setErrorAdmin (newPosition fun_symb fun_pos) error_admin
th_vars
= init_type_vars st_vars th_vars
(th_vars, td_infos, error_admin)
= unsafeFold2St (check_atype KindConst)
[0..] [st_result:st_args] (th_vars, td_infos, error_admin)
(bv_uninitialized_mods, th_vars, td_infos, error_admin)
= foldSt (check_context common_defs) st_context
(bv_uninitialized_mods, th_vars, td_infos, error_admin)
= (bv_uninitialized_mods, th_vars, td_infos, error_admin)
check_atype expected_kind arg_nr {at_type} state
= check_type expected_kind arg_nr at_type state
check_type expected_kind arg_nr (TA {type_name,type_index} args)
(th_vars, td_infos, error_admin)
# ({tdi_kinds}, td_infos)
= td_infos![type_index.glob_module,type_index.glob_object]
(th_vars, td_infos, error_admin)
= unsafeFold2St (flip check_atype arg_nr) tdi_kinds args
(th_vars, td_infos, error_admin)
n_args
= length args
kind_of_application
= if (n_args==length tdi_kinds)
KindConst
(KindArrow (drop n_args tdi_kinds))
error_admin
= check_equality_of_kinds arg_nr expected_kind kind_of_application error_admin
= (th_vars, td_infos, error_admin)
check_type expected_kind _ (TV tv) (th_vars, td_infos, error_admin)
# (th_vars, error_admin)
= unify_var_kinds expected_kind tv th_vars error_admin
= (th_vars, td_infos, error_admin)
check_type expected_kind _ (GTV tv) (th_vars, td_infos, error_admin)
# (th_vars, error_admin)
= unify_var_kinds expected_kind tv th_vars error_admin
= (th_vars, td_infos, error_admin)
check_type expected_kind arg_nr (l --> r) state
# state
= check_atype KindConst arg_nr l state
(th_vars, td_infos, error_admin)
= check_atype KindConst arg_nr r state
error_admin
= check_equality_of_kinds arg_nr expected_kind KindConst error_admin
= (th_vars, td_infos, error_admin)
//AA..
check_type expected_kind arg_nr TArrow (th_vars, td_infos, error_admin)
# error_admin
= check_equality_of_kinds arg_nr expected_kind (KindArrow [KindConst,KindConst]) error_admin
= (th_vars, td_infos, error_admin)
check_type expected_kind arg_nr (TArrow1 arg) state
# (th_vars, td_infos, error_admin) = check_atype KindConst arg_nr arg state
# error_admin
= check_equality_of_kinds arg_nr expected_kind (KindArrow [KindConst]) error_admin
= (th_vars, td_infos, error_admin)
//..AA
check_type expected_kind arg_nr ((CV tv) :@: args) state
# (th_vars, td_infos, error_admin)
= foldSt (check_atype KindConst arg_nr) args state
expected_kind_of_cons_var
= KindArrow (repeatn (length args) KindConst)
(th_vars, error_admin)
= unify_var_kinds expected_kind_of_cons_var tv th_vars error_admin
error_admin
= check_equality_of_kinds arg_nr expected_kind KindConst error_admin
= (th_vars, td_infos, error_admin)
check_type expected_kind arg_nr (TB _) (th_vars, td_infos, error_admin)
# error_admin
= check_equality_of_kinds arg_nr expected_kind KindConst error_admin
= (th_vars, td_infos, error_admin)
// Sjaak ... 170801
check_type expected_kind arg_nr (TFA vars type) (th_vars, td_infos, error_admin)
# th_vars = init_type_vars [ atv_variable \\ {atv_variable} <- vars ] th_vars
= check_type expected_kind arg_nr type (th_vars, td_infos, error_admin)
// ... Sjaak 170801
check_context common_defs {tc_class, tc_types}
(bv_uninitialized_mods, th_vars, td_infos, error_admin)
# (expected_kinds, bv_uninitialized_mods, th_vars)
= get_expected_kinds tc_class common_defs bv_uninitialized_mods th_vars
(th_vars, td_infos, error_admin)
= unsafeFold3St possibly_check_type expected_kinds (descending (-1))
tc_types (th_vars, td_infos, error_admin)
= (bv_uninitialized_mods, th_vars, td_infos, error_admin)
where
descending i = [i:descending (i-1)]
init_type_vars vars tv_heap
= foldSt init_type_var vars tv_heap
where
init_type_var {tv_info_ptr} tv_heap
= tv_heap <:= (tv_info_ptr, TVI_Empty)
unify_var_kinds expected_kind tv=:{tv_name, tv_info_ptr} th_vars error_admin
# (tvi, th_vars)
= readPtr tv_info_ptr th_vars
= case tvi of
TVI_Empty
-> (writePtr tv_info_ptr (TVI_Kind expected_kind) th_vars, error_admin)
TVI_Kind kind
| expected_kind==kind
-> (th_vars, error_admin)
-> (th_vars, checkError "cannot consistently assign a kind to type variable"
tv_name.id_name error_admin)
check_equality_of_kinds arg_nr expected_kind kind error_admin
| expected_kind==kind
= error_admin
= checkError "inconsistent kind in" (arg_nr_to_string arg_nr) error_admin
arg_nr_to_string 0 = "result type"
arg_nr_to_string i
| i >0
= "type of argument nr "+++toString i
= "type context nr "+++toString (~i)
in_index_range test ir :== test>=ir.ir_from && test < ir.ir_to
|
