type.icl 159 KB
Newer Older
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
1
2
3
implementation module type

import StdEnv
4
import syntax, typesupport, check, analtypes, overloading, unitype, refmark, predef, utilities, compare_constructor // , RWSDebug
5
import compilerSwitches
6
import genericsupport // AA
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
7
8

::	TypeInput =
9
10
11
	{	ti_common_defs	:: !{# CommonDefs }
	,	ti_functions	:: !{# {# FunType }}
	,	ti_main_dcl_module_n :: !Int
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
12
13
14
	}

::	TypeState =
15
16
17
18
19
20
	{	ts_fun_env			:: !.{! FunctionType}
	,	ts_var_store		:: !TempVarId
	,	ts_attr_store		:: !TempAttrId
	,	ts_var_heap			:: !.VarHeap 
	,	ts_type_heaps		:: !.TypeHeaps
	,	ts_expr_heap		:: !.ExpressionHeap 
21
	,	ts_generic_heap		:: !.GenericHeap
22
23
24
25
	,	ts_td_infos			:: !.TypeDefInfos
	,	ts_cons_variables	:: ![TempVarId]
	,	ts_exis_variables	:: ![(CoercionPosition, [TempAttrId])]
	,	ts_error			:: !.ErrorAdmin
26
	,	ts_fun_defs			:: !.{#FunDef}
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
27
28
29
30
31
32
33
34
35
36
	}

::	TypeCoercion =
	{	tc_demanded		:: !AType
	,	tc_offered		:: !AType
	,	tc_position		:: !CoercionPosition
	,	tc_coercible	:: !Bool
	}

::	SharedAttribute = 
Sjaak Smetsers's avatar
Sjaak Smetsers committed
37
	{	sa_attr_nr	:: !Int
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
38
39
40
41
42
43
	,	sa_position	:: !Expression
	}

::	Requirements =
	{	req_overloaded_calls	:: ![ExprInfoPtr]
	,	req_type_coercions		:: ![TypeCoercion]
44
	,	req_type_coercion_groups:: ![TypeCoercionGroup]
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
45
46
47
	,	req_attr_coercions		:: ![AttrCoercion]
	,	req_case_and_let_exprs	:: ![ExprInfoPtr]
	}
48
49
50
51
52
53

::	TypeCoercionGroup =
	{	tcg_type_coercions	:: ![TypeCoercion]
	,	tcg_position		:: !Position
	}

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
54
55
56
57
instance toString BoundVar
where
	toString varid = varid.var_name.id_name

58
class arraySubst type :: !type !u:{!Type} -> (!Bool,!type, !u:{! Type})
59
60
61
62

instance arraySubst AType
where
	arraySubst atype=:{at_type} subst
63
		# (changed, at_type, subst) = arraySubst at_type subst
64
		| changed
65
66
			= (True, { atype & at_type = at_type }, subst)
			= (False, atype, subst)
67
68
69
70
		
instance arraySubst Type
where
	arraySubst tv=:(TempV tv_number) subst
Sjaak Smetsers's avatar
Sjaak Smetsers committed
71
		# (type, subst) = subst![tv_number]
72
		= case type of
73
74
75
76
77
78
			TE	-> (False,tv, subst)
			_
				# (_, type, subst) = arraySubst type subst
				-> (True, type, subst)
	arraySubst type=:(arg_type --> res_type) subst
		# (changed, (arg_type, res_type), subst) = arraySubst (arg_type, res_type) subst
79
		| changed
80
81
			= (changed, arg_type --> res_type, subst)
			= (False, type, subst)
82
	arraySubst type=:(TA cons_id cons_args) subst
83
		# (changed, cons_args, subst) = arraySubst cons_args subst
84
		| changed
85
86
87
88
89
90
			= (True, TA cons_id cons_args, subst)
			= (False,type, subst) 
	arraySubst type=:(TAS cons_id cons_args strictness) subst
		# (changed, cons_args, subst) = arraySubst cons_args subst
		| changed
			= (True, TAS cons_id cons_args strictness, subst)
91
			= (False,type, subst) 
92
	arraySubst tcv=:(TempCV tv_number :@: types) subst
Sjaak Smetsers's avatar
Sjaak Smetsers committed
93
		# (type, subst) = subst![tv_number]
94
95
		= case type of
			TE
96
				# (changed,types, subst) = arraySubst types subst
97
				| changed
98
99
					-> (True, TempCV tv_number :@: types, subst)
					-> (False, tcv, subst)
100
			_
101
102
103
104
105
				# (_, (type, types), subst) = arraySubst (type, types) subst
				  (ok, simplified_type) = simplifyTypeApplication type types
				| ok
					-> (True, simplified_type, subst)
					-> (False, tcv, subst)
106
107
108
109
110
111
112
113
//AA..					
	arraySubst type=:(TArrow1 arg_type) subst
		# (changed, arg_type, subst) = arraySubst arg_type subst
		| changed
			= (changed, TArrow1 arg_type, subst)
			= (False, type, subst)
//..AA					

114
115
116
117
118
	arraySubst tfa_type=:(TFA vars type) subst
		# (changed, type, subst) = arraySubst type subst
		| changed
			= (changed, TFA vars type, subst)
			= (False, tfa_type, subst)
119

120
	arraySubst type subst
121
		= (False, type, subst)
122

123
124
125
126
127
128
129
130
instance arraySubst (a,b) | arraySubst a & arraySubst b
where
	arraySubst (x,y) subst
		# (changed_x, x, subst) =  arraySubst x subst
		  (changed_y, y, subst) =  arraySubst y subst
		= (changed_x || changed_y, (x,y), subst)
		
instance arraySubst [a] | arraySubst a
131
132
where
	arraySubst [] subst
133
134
135
		= (False, [], subst)
	arraySubst t=:[type : types ] subst
		# (changed, (type, types), subst) = arraySubst (type, types) subst
136
		| changed
137
138
			= (True, [type : types ], subst)
			= (False, t, subst)
139
140
141
142
	
instance arraySubst TempSymbolType
where
	arraySubst tst=:{tst_args,tst_result,tst_context} subst
143
		# (changed, (tst_args, (tst_result, tst_context)), subst) = arraySubst (tst_args, (tst_result, tst_context)) subst
144
		| changed
145
146
			= (True, {tst & tst_args = tst_args, tst_result = tst_result, tst_context = tst_context}, subst)
			= (False, tst, subst)
147
148
149
150

instance arraySubst TypeContext
where
	arraySubst tc=:{tc_types} subst
151
		# (changed, tc_types, subst) = arraySubst tc_types subst
152
153
154
155
		| changed
			= (True,{ tc & tc_types = tc_types}, subst)
			= (False, tc, subst)

156
instance arraySubst CaseType
157
where
158
159
	arraySubst ct=:{ct_pattern_type, ct_result_type, ct_cons_types} subst
		# (changed, (ct_pattern_type, (ct_result_type, ct_cons_types)), subst) = arraySubst (ct_pattern_type, (ct_result_type, ct_cons_types)) subst
160
161
		| changed
			= (True,{ ct & ct_pattern_type = ct_pattern_type, ct_result_type = ct_result_type, ct_cons_types = ct_cons_types }, subst)
162
			= (False, ct, subst)
163

164
class containsTypeVariable a :: !Int !a !{!Type} -> Bool
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
165

166
instance containsTypeVariable [a] | containsTypeVariable a
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
167
where
168
169
170
	containsTypeVariable var_id [elem:list] subst
		= containsTypeVariable var_id elem subst || containsTypeVariable var_id list subst
	containsTypeVariable var_id [] _
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
171
172
		= False

173
instance containsTypeVariable AType
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
174
where
175
	containsTypeVariable var_id {at_type} subst = containsTypeVariable var_id at_type subst
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
176

177
instance containsTypeVariable Type
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
178
where
179
180
181
182
183
184
185
	containsTypeVariable var_id (TempV tv_number) subst
		# type = subst.[tv_number]
		| isIndirection type
			= containsTypeVariable var_id type subst 
			= tv_number == var_id
	containsTypeVariable var_id (arg_type --> res_type) subst
		= containsTypeVariable var_id arg_type subst || containsTypeVariable var_id res_type subst
186
187
188
189
//AA..
	containsTypeVariable var_id (TArrow1 arg_type) subst
		= containsTypeVariable var_id arg_type subst
//..AA
190
191
	containsTypeVariable var_id (TA cons_id cons_args) subst
		= containsTypeVariable var_id cons_args subst
192
193
	containsTypeVariable var_id (TAS cons_id cons_args _) subst
		= containsTypeVariable var_id cons_args subst
194
195
196
	containsTypeVariable var_id (type :@: types) subst
		= containsTypeVariable var_id type subst || containsTypeVariable var_id types subst
	containsTypeVariable _ _ _
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
197
198
		= False

199
instance containsTypeVariable ConsVariable
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
200
where
201
202
203
204
205
206
	containsTypeVariable var_id (TempCV tv_number) subst
		# type = subst.[tv_number]
		| isIndirection type
			= containsTypeVariable var_id type subst 
			= tv_number == var_id
	containsTypeVariable var_id _ _
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
207
208
		= False

209
210
type_error =: "Type error"
type_error_format =: { form_properties = cNoProperties, form_attr_position = No }
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
211

212
cannotUnify t1 t2 position=:(CP_Expression expr) err=:{ea_loc=[ip:_]} 
213
214
215
	= case tryToOptimizePosition expr of
		Yes (id_name, line)
			# err = pushErrorAdmin { ip & ip_ident.id_name = id_name, ip_line = line } err
216
217
			  err = errorHeading type_error err
			  err = popErrorAdmin err
218
219
220
221
//			-> { err & ea_file = err.ea_file <<< " cannot unify " <:: (type_error_format, t1, Yes initialTypeVarBeautifulizer) 
//											<<< " with " <:: (type_error_format, t2, Yes initialTypeVarBeautifulizer) <<< '\n' }
			-> { err & ea_file = err.ea_file <<< " cannot unify " <:: (type_error_format, t1, No) 
											<<< " with " <:: (type_error_format, t2, No) <<< '\n' }
222
223
224
225
226
227
228
229
230
231
		_
			-> cannot_unify t1 t2 position err 
cannotUnify t1 t2 position err 
	= cannot_unify t1 t2 position err 

cannot_unify t1 t2 position err
	# (err=:{ea_file}) = errorHeading type_error err
	  ea_file = case position of
				CP_FunArg _ _
					-> ea_file <<< "\"" <<< position <<< "\""
232
233
				CP_LiftedFunArg _ _
					-> ea_file <<< "\"" <<< position <<< "\""
234
235
				_
					-> ea_file
236
237
238
239
	  ea_file = ea_file <<< " cannot unify " <:: (type_error_format, t1, No) 
						<<< " with " <:: (type_error_format, t2, No)
//	  ea_file = ea_file <<< " cannot unify " <:: (type_error_format, t1, Yes initialTypeVarBeautifulizer) 
//						<<< " with " <:: (type_error_format, t2, Yes initialTypeVarBeautifulizer)
240
	  ea_file = case position of
241
  				CP_Expression _
242
	  				-> ea_file <<< " near " <<< position
243
244
	  			_
	  				-> ea_file
245
246
	= { err & ea_file = ea_file <<< '\n' }

247
248
249
250
251
252
253
254
255
256
257
258
259

existentialError position=:(CP_Expression expr) err=:{ea_loc=[ip:_]} 
	= case tryToOptimizePosition expr of
		Yes (id_name, line)
			# err = pushErrorAdmin { ip & ip_ident.id_name = id_name, ip_line = line } err
			  err = errorHeading type_error err
			  err = popErrorAdmin err
			-> { err & ea_file = err.ea_file <<< " attribute variable could not be universally quantified"<<< '\n' }
		_
			# err = errorHeading type_error err
			-> { err & ea_file = err.ea_file <<< " attribute variable could not be universally quantified"<<< '\n' }
			

260
261
262
263
264
265
266
tryToOptimizePosition (Case {case_ident=Yes {id_name}})
	= optBeautifulizeIdent id_name
tryToOptimizePosition (App {app_symb={symb_name}})
	= optBeautifulizeIdent symb_name.id_name
tryToOptimizePosition (fun @ _)
	= tryToOptimizePosition fun
tryToOptimizePosition _
Martin Wierich's avatar
Martin Wierich committed
267
	= No
268

269
270
271
isIndirection TE	= False
isIndirection type	= True

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
272
273
class unify a :: !a !a !TypeInput !*{! Type} !*TypeHeaps -> (!Bool, !*{! Type}, !*TypeHeaps)

274
instance unify (a, b) | unify a & unify b
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
275
276
277
278
279
280
281
where
	unify (t1x, t1y) (t2x, t2y) modules subst heaps
		# (succ, subst, heaps) =  unify t1y t2y modules subst heaps
		| succ
	      = unify t1x t2x modules subst heaps
	      = (False, subst, heaps)

282
instance unify [a] | unify a
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
283
284
285
286
287
288
289
290
291
292
293
294
295
where
	unify [t1 : ts1] [t2 : ts2] modules subst heaps
		= unify (t1,ts1) (t2,ts2) modules subst heaps
	unify [] [] modules subst heaps
		= (True, subst, heaps)
	unify _ _ modules subst heaps
		= (False, subst, heaps)

instance unify AType
where
	unify t1 t2 modules subst heaps = unifyTypes t1.at_type t1.at_attribute t2.at_type t2.at_attribute modules subst heaps

unifyTypes :: !Type !TypeAttribute !Type !TypeAttribute !TypeInput !*{! Type} !*TypeHeaps -> (!Bool, !*{! Type}, !*TypeHeaps)
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
unifyTypes tv=:(TempV tv_number) attr1 type2 attr2 modules subst heaps
	# (type1, subst) = subst![tv_number]
	| isIndirection type1
		= unifyTypes type1 attr1 type2 attr2 modules subst heaps
		# (succ, subst) = unify_variable_with_type tv_number type2 subst
		= (succ, subst, heaps)
	where	
		unify_variable_with_type tv_number1 tv=:(TempV tv_number2) subst
			# (type2, subst) = subst![tv_number2]
			| isIndirection type2
				= unify_variable_with_type tv_number type2 subst
			| tv_number1 == tv_number2
				= (True, subst)
				= (True, { subst & [tv_number1] = tv})
		unify_variable_with_type tv_number type subst
			| containsTypeVariable tv_number type subst
				= (False, subst)
313
//					---> "unify_variable_with_type"
314
				= (True, { subst & [tv_number] = type})
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
315
316
317
318
319
320
unifyTypes type attr1 tv=:(TempV _) attr2 modules subst heaps
	= unifyTypes tv attr2 type attr1 modules subst heaps
unifyTypes t1=:(TB tb1) attr1 t2=:(TB tb2) attr2 modules subst heaps
	| tb1 == tb2
		= (True, subst, heaps)
		= (False, subst, heaps)
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
unifyTypes t1=:(TA cons_id1 cons_args1) attr1 t2=:(TA cons_id2 cons_args2) attr2 modules subst heaps
	| cons_id1 == cons_id2
		= unify cons_args1 cons_args2 modules subst heaps
		= expandAndUnifyTypes t1 attr1 t2 attr2 modules subst heaps
unifyTypes t1=:(TA cons_id1 cons_args1) attr1 t2=:(TAS cons_id2 cons_args2 _) attr2 modules subst heaps
	| cons_id1 == cons_id2
		= unify cons_args1 cons_args2 modules subst heaps
		= expandAndUnifyTypes t1 attr1 t2 attr2 modules subst heaps
unifyTypes t1=:(TAS cons_id1 cons_args1 _) attr1 t2=:(TA cons_id2 cons_args2) attr2 modules subst heaps
	| cons_id1 == cons_id2
		= unify cons_args1 cons_args2 modules subst heaps
		= expandAndUnifyTypes t1 attr1 t2 attr2 modules subst heaps
unifyTypes t1=:(TAS cons_id1 cons_args1 _) attr1 t2=:(TAS cons_id2 cons_args2 _) attr2 modules subst heaps
	| cons_id1 == cons_id2
		= unify cons_args1 cons_args2 modules subst heaps
		= expandAndUnifyTypes t1 attr1 t2 attr2 modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
337
338
unifyTypes (arg_type1 --> res_type1) attr1 (arg_type2 --> res_type2) attr2 modules subst heaps
	= unify (arg_type1,res_type1) (arg_type2,res_type2) modules subst heaps
339
340
341
342
unifyTypes TArrow attr1 TArrow attr2 modules subst heaps
	= (True, subst, heaps)	
unifyTypes (TArrow1 t1) attr1 (TArrow1 t2) attr2 modules subst heaps
	= unify t1 t2 modules subst heaps	
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
343
unifyTypes (cons_var :@: types) attr1 type2 attr2 modules subst heaps
344
345
	# (_, type2, heaps) = tryToExpand type2 attr2 modules.ti_common_defs heaps
	= unifyTypeApplications cons_var attr1 types type2 attr2 modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
346
unifyTypes type1 attr1 (cons_var :@: types) attr2 modules subst heaps
347
348
	# (_, type1, heaps) = tryToExpand type1 attr1 modules.ti_common_defs heaps
	= unifyTypeApplications cons_var attr2 types type1 attr1 modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
349
350
351
352
353
354
355
unifyTypes t1=:(TempQV qv_number1) attr1 t2=:(TempQV qv_number2) attr2 modules subst heaps
	= (qv_number1 == qv_number2, subst, heaps)
unifyTypes (TempQV qv_number) attr1 type attr2 modules subst heaps
	= (False, subst, heaps)
unifyTypes type attr1 (TempQV qv_number1) attr2 modules subst heaps
	= (False, subst, heaps)
unifyTypes type1 attr1 type2 attr2 modules subst heaps
356
357
	# (succ1, type1, heaps) = tryToExpand type1 attr1 modules.ti_common_defs heaps
	  (succ2, type2, heaps) = tryToExpand type2 attr2 modules.ti_common_defs heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
358
359
360
361
	| succ1 || succ2
		= unifyTypes type1 attr1 type2 attr2 modules subst heaps
		= (False, subst, heaps)

362
363
364
365
366
367
368
expandAndUnifyTypes t1 attr1 t2 attr2 modules subst heaps
	# (succ1, t1, heaps) = tryToExpand t1 attr1 modules.ti_common_defs heaps
	  (succ2, t2, heaps) = tryToExpand t2 attr2 modules.ti_common_defs heaps
	| succ1 || succ2
		= unifyTypes t1 attr1 t2 attr2 modules subst heaps
		= (False, subst, heaps)

369
370
tryToExpand :: !Type !TypeAttribute !{# CommonDefs} !*TypeHeaps -> (!Bool, !Type, !*TypeHeaps)
tryToExpand type=:(TA {type_index={glob_object,glob_module}} type_args) type_attr ti_common_defs type_heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
371
372
373
	#! type_def = ti_common_defs.[glob_module].com_type_defs.[glob_object]
	= case type_def.td_rhs of
		SynType {at_type}
374
375
			# (_, expanded_type, type_heaps) = substituteType type_def.td_attribute type_attr type_def.td_args type_args at_type type_heaps
			-> (True, expanded_type, type_heaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
376
377
		_
			-> (False, type, type_heaps)
378
379
380
381
382
383
384
385
tryToExpand type=:(TAS {type_index={glob_object,glob_module}} type_args _) type_attr ti_common_defs type_heaps
	#! type_def = ti_common_defs.[glob_module].com_type_defs.[glob_object]
	= case type_def.td_rhs of
		SynType {at_type}
			# (_, expanded_type, type_heaps) = substituteType type_def.td_attribute type_attr type_def.td_args type_args at_type type_heaps
			-> (True, expanded_type, type_heaps)
		_
			-> (False, type, type_heaps)
386
tryToExpand type type_attr modules type_heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
387
388
	= (False, type, type_heaps)

389
390
391
392
393
394
395
396
397
398
399
400
401
toTV is_exist temp_var_id
	| is_exist
		= TempQV temp_var_id
		= TempV temp_var_id

toCV is_exist temp_var_id
	| is_exist
		= TempQCV temp_var_id
		= TempCV temp_var_id

simplifyTypeApplication :: !Type ![AType] -> (!Bool, !Type)
simplifyTypeApplication (TA type_cons=:{type_arity} cons_args) type_args
	= (True, TA { type_cons & type_arity = type_arity + length type_args } (cons_args ++ type_args))
402
403
simplifyTypeApplication (TAS type_cons=:{type_arity} cons_args strictness) type_args
	= (True, TAS { type_cons & type_arity = type_arity + length type_args } (cons_args ++ type_args) strictness)
404
405
406
407
408
409
simplifyTypeApplication (cons_var :@: types) type_args
	= (True, cons_var :@: (types ++ type_args))
simplifyTypeApplication (TempV tv_number) type_args
	= (True, TempCV tv_number :@: type_args)
simplifyTypeApplication (TempQV tv_number) type_args
	= (True, TempQCV tv_number :@: type_args)
410
411
412
//AA..
simplifyTypeApplication TArrow [type1, type2] 
	= (True, type1 --> type2)
Artem Alimarine's avatar
Artem Alimarine committed
413
414
simplifyTypeApplication TArrow [type] 
	= (True, TArrow1 type)
415
416
417
simplifyTypeApplication (TArrow1 type1) [type2] 
	= (True, type1 --> type2)
//..AA
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
simplifyTypeApplication type type_args
	= (False, type)

unifyTypeApplications (TempCV tv_number) attr1 type_args type2 attr2 modules subst heaps
	# (type1, subst) = subst![tv_number]
	| isIndirection type1
		# (ok, simplified_type) = simplifyTypeApplication type1 type_args
		| ok
			= unifyTypes simplified_type attr1 type2 attr2 modules subst heaps
			= (False, subst, heaps)
		= unifyCVwithType False tv_number type_args type2 modules subst heaps
unifyTypeApplications (TempQCV tv_number) attr1 type_args type2 attr2 modules subst heaps
	= unifyCVwithType True tv_number type_args type2 modules subst heaps
		
unifyCVwithType is_exist tv_number1 type_args1 type=:(cv :@: type_args2) modules subst heaps
	= case cv of
		TempCV tv_number2
			# (type2, subst) = subst![tv_number2]
			| isIndirection type2
				# (ok, simplified_type) = simplifyTypeApplication type2 type_args2
				| ok
					-> unifyCVwithType is_exist tv_number1 type_args1 simplified_type modules subst heaps
					-> (False, subst, heaps)
				-> unifyCVApplicationwithCVApplication is_exist tv_number1 type_args1 False tv_number2 type_args2 modules subst heaps
		TempQCV tv_number2
				-> unifyCVApplicationwithCVApplication is_exist tv_number1 type_args1 True tv_number2 type_args2 modules subst heaps

unifyCVwithType is_exist tv_number type_args type=:(TA type_cons cons_args) modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
446
447
448
449
	# diff = type_cons.type_arity - length type_args
	| diff >= 0 
		# (succ, subst, heaps) = unify type_args (drop diff cons_args) modules subst heaps
		| succ
450
			= unifyTypes (toTV is_exist tv_number) TA_Multi (TA { type_cons & type_arity = diff } (take diff cons_args)) TA_Multi modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
451
452
		    = (False, subst, heaps)
		= (False, subst, heaps)
453

454
455
456
457
458
459
460
461
462
unifyCVwithType is_exist tv_number type_args type=:(TAS type_cons cons_args strictness) modules subst heaps
	# diff = type_cons.type_arity - length type_args
	| diff >= 0 
		# (succ, subst, heaps) = unify type_args (drop diff cons_args) modules subst heaps
		| succ
			= unifyTypes (toTV is_exist tv_number) TA_Multi (TAS { type_cons & type_arity = diff } (take diff cons_args) strictness) TA_Multi modules subst heaps
		    = (False, subst, heaps)
		= (False, subst, heaps)

Artem Alimarine's avatar
Artem Alimarine committed
463
// AA..
464
465
466
467
468
469
470
471
472
473
unifyCVwithType is_exist tv_number [type_arg1, type_arg2] type=:(atype1 --> atype2) modules subst heaps
	# (succ, subst, heaps) = unify (type_arg1, type_arg2) (atype1, atype2) modules subst heaps
	| succ
		= unifyTypes (toTV is_exist tv_number) TA_Multi TArrow TA_Multi modules subst heaps
		= (False, subst, heaps)		
unifyCVwithType is_exist tv_number [type_arg] type=:(atype1 --> atype2) modules subst heaps
	# (succ, subst, heaps) = unify type_arg atype2 modules subst heaps
	| succ
		= unifyTypes (toTV is_exist tv_number) TA_Multi (TArrow1 atype1) TA_Multi modules subst heaps
		= (False, subst, heaps)
Artem Alimarine's avatar
Artem Alimarine committed
474
475
476
477
478
479
480
481
482
483
484
485
486
unifyCVwithType is_exist tv_number [] type=:(atype1 --> atype2) modules subst heaps
	= unifyTypes (toTV is_exist tv_number) TA_Multi type TA_Multi modules subst heaps
		
unifyCVwithType is_exist tv_number [type_arg] type=:(TArrow1 atype) modules subst heaps
	# (succ, subst, heaps) = unify type_arg atype modules subst heaps
	| succ
		= unifyTypes (toTV is_exist tv_number) TA_Multi TArrow TA_Multi modules subst heaps
		= (False, subst, heaps)
unifyCVwithType is_exist tv_number [] type=:(TArrow1 atype) modules subst heaps
	= unifyTypes (toTV is_exist tv_number) TA_Multi type TA_Multi modules subst heaps

unifyCVwithType is_exist tv_number [] TArrow modules subst heaps
	= unifyTypes (toTV is_exist tv_number) TA_Multi TArrow TA_Multi modules subst heaps
487
// ..AA 		
Artem Alimarine's avatar
Artem Alimarine committed
488

489
490
491
492
493
494
unifyCVwithType is_exist tv_number type_args type modules subst heaps
	= (False, subst, heaps)

unifyCVApplicationwithCVApplication is_exist1 tv_number1 type_args1 is_exist2 tv_number2 type_args2 modules subst heaps
	# arity1 = length type_args1
	  arity2 = length type_args2
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
495
496
	  diff = arity1 - arity2
	| diff == 0
497
		# (succ, subst) = unify_cv_with_cv is_exist1 tv_number1 is_exist2 tv_number2 subst
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
498
		| succ
499
		    = unify type_args1 type_args2 modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
500
501
502
			= (False, subst, heaps)
	| diff < 0
		# diff = 0 - diff
503
		  (succ, subst, heaps) = unifyTypes (toTV is_exist1 tv_number1) TA_Multi (toCV is_exist2 tv_number2 :@: take diff type_args2) TA_Multi modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
504
		| succ
505
		    = unify type_args1 (drop diff type_args2) modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
506
			= (False, subst, heaps)
507
//	| otherwise
508
		# (succ, subst, heaps) = unifyTypes (toCV is_exist1 tv_number1 :@: take diff type_args1) TA_Multi (toTV is_exist2 tv_number2) TA_Multi modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
509
		| succ
510
		    = unify (drop diff type_args1) type_args2 modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
511
			= (False, subst, heaps)
512
513
514
515
516
517
518
519
520
521
522
523
	where
		unify_cv_with_cv is_exist1 tv_number1 is_exist2 tv_number2 subst
			| tv_number1 == tv_number2
				= (True, subst)
			| is_exist1
				| is_exist2
					= (False, subst)
					= (True, { subst & [tv_number2] = TempQV tv_number1})
				| is_exist2
					= (True, { subst & [tv_number1] = TempQV tv_number2})
					= (True, { subst & [tv_number1] = TempV tv_number2})
		
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
524
525
526
527
528
529
530
	
instance fromInt TypeAttribute
where
	fromInt AttrUni		= TA_Unique
	fromInt AttrMulti	= TA_Multi
	fromInt av_number	= TA_TempVar av_number

531
532


533
class freshCopy a :: !a !*TypeHeaps -> (!a, !*TypeHeaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
534
535
536
537
538
539
540
541
542
543
544

instance freshCopy [a] | freshCopy a
where
	freshCopy l ls = mapSt freshCopy l ls

freshCopyOfAttributeVar {av_name,av_info_ptr} attr_var_heap
	# (av_info, attr_var_heap) = readPtr av_info_ptr attr_var_heap
	= case av_info of
		AVI_Attr attr
			-> (attr, attr_var_heap)
		_
545
			-> abort ("freshCopyOfAttributeVar (type,icl)" ---> (av_name,av_info_ptr))
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
546

Sjaak Smetsers's avatar
Sjaak Smetsers committed
547

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
548
549
550
freshCopyOfTypeAttribute (TA_Var avar) attr_var_heap
	= freshCopyOfAttributeVar avar attr_var_heap
freshCopyOfTypeAttribute (TA_RootVar avar) attr_var_heap
551
	= freshCopyOfAttributeVar avar attr_var_heap
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
552
553
554
555
556
557
558
559
560
561
freshCopyOfTypeAttribute TA_None attr_var_heap
	= (TA_Multi, attr_var_heap)
freshCopyOfTypeAttribute TA_Unique attr_var_heap
	= (TA_Unique, attr_var_heap)
freshCopyOfTypeAttribute attr attr_var_heap
	= (attr, attr_var_heap)

cIsExistential 		:== True
cIsNotExistential	:== False

562
563
564
freshCopyOfTypeVariable {tv_name,tv_info_ptr} type_heaps=:{th_vars}
	# (TVI_Type fresh_var, th_vars)	= readPtr tv_info_ptr th_vars
	= (fresh_var, { type_heaps & th_vars = th_vars })
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
565
566

freshConsVariable {tv_info_ptr} type_var_heap
567
	# (tv_info, type_var_heap) = readPtr tv_info_ptr type_var_heap
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
568
569
	= (to_constructor_variable tv_info, type_var_heap)
	where
570
571
572
573
574
575
		to_constructor_variable (TVI_Type fresh_type)
			= case fresh_type of
				TempV temp_var_id
					-> TempCV temp_var_id
				TempQV temp_var_id
					-> TempQCV temp_var_id
576
				TV var		
577
					-> CV var
578
579
580
581
				_ 	
					-> abort "type.icl: to_constructor_variable, fresh_type\n" ---> fresh_type		
		to_constructor_variable tvi 
			= abort "type.icl: to_constructor_variable, tvi\n" ---> tvi
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
582
583
584

instance freshCopy AType
where 	
585
586
587
588
589
590
591
592
593
	freshCopy type=:{at_type = cv :@: types, at_attribute} type_heaps=:{th_attrs}
		# (fresh_attribute, th_attrs)	= freshCopyOfTypeAttribute at_attribute th_attrs
		# (fresh_types, type_heaps)		= freshCopy types { type_heaps & th_attrs = th_attrs }
		= case cv of
			CV tv
				# (fresh_cons_var, th_vars)	= freshConsVariable tv type_heaps.th_vars
				-> ({type & at_type = fresh_cons_var :@: fresh_types, at_attribute = fresh_attribute }, { type_heaps & th_vars = th_vars })
			_
				-> ({type & at_type = cv :@: fresh_types, at_attribute = fresh_attribute}, type_heaps)
594
595
596
597
	freshCopy type=:{at_type, at_attribute} type_heaps=:{th_attrs}
		# (fresh_attribute, th_attrs)	= freshCopyOfTypeAttribute at_attribute th_attrs
		  (fresh_type, type_heaps)		= freshCopy at_type { type_heaps & th_attrs = th_attrs }
		= ({ type & at_type = fresh_type, at_attribute = fresh_attribute }, type_heaps)
598

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
599
600
instance freshCopy Type
where
601
602
603
604
605
	freshCopy (TV tv) type_heaps
		= freshCopyOfTypeVariable tv type_heaps
	freshCopy (TA cons_id=:{type_index={glob_object,glob_module}} cons_args)  type_heaps
		# (cons_args, type_heaps) = freshCopy cons_args type_heaps
		= (TA cons_id cons_args, type_heaps)
606
607
608
	freshCopy (TAS cons_id=:{type_index={glob_object,glob_module}} cons_args strictness)  type_heaps
		# (cons_args, type_heaps) = freshCopy cons_args type_heaps
		= (TAS cons_id cons_args strictness, type_heaps)
609
610
611
612
	freshCopy (arg_type --> res_type) type_heaps
		# (arg_type, type_heaps) = freshCopy arg_type type_heaps
		  (res_type, type_heaps) = freshCopy res_type type_heaps
		= (arg_type --> res_type, type_heaps)
613
614
615
616
617
//AA..
	freshCopy (TArrow1 arg_type) type_heaps
		# (arg_type, type_heaps) = freshCopy arg_type type_heaps
		= (TArrow1 arg_type, type_heaps)
//..AA		
618
	freshCopy (TFA vars type) type_heaps
619
		= freshCopyOfTFAType vars type type_heaps
620
621
	freshCopy type type_heaps
		= (type, type_heaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
622

623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
freshCopyOfTFAType vars type type_heaps
	# (fresh_vars, type_heaps) = foldSt bind_var_and_attr vars ([], type_heaps)
	  (type, type_heaps) = freshCopy type type_heaps
	  type_heaps = foldSt clear_binding_of_var_and_attr fresh_vars type_heaps
	= (TFA fresh_vars type, type_heaps)
	where
		bind_var_and_attr atv=:{atv_attribute, atv_variable = tv=:{tv_info_ptr}} (fresh_vars, type_heaps=:{th_vars,th_attrs})
			# (fresh_vars, th_attrs) = bind_attr atv_attribute atv (fresh_vars, th_attrs)
			= (fresh_vars, { type_heaps & th_vars = th_vars <:= (tv_info_ptr, TVI_Type (TV tv)), th_attrs = th_attrs })

		bind_attr var=:(TA_Var {av_info_ptr}) atv (fresh_vars, attr_heap)
			# (av_info, attr_heap) = readPtr av_info_ptr attr_heap
			= case av_info of
				AVI_Empty
					-> ([atv : fresh_vars], attr_heap <:= (av_info_ptr, AVI_Attr var))
				AVI_Attr (TA_TempVar _)
					-> ([{ atv & atv_attribute = TA_Multi } : fresh_vars], attr_heap)
		bind_attr attr atv (fresh_vars, attr_heap)
			= ([atv : fresh_vars], attr_heap)


		clear_binding_of_var_and_attr {atv_attribute, atv_variable = tv=:{tv_info_ptr}} type_heaps=:{th_vars,th_attrs}
				= { type_heaps & th_vars = th_vars <:= (tv_info_ptr, TVI_Empty), th_attrs = clear_attr atv_attribute th_attrs }
	
		clear_attr var=:(TA_Var {av_info_ptr}) attr_heap
			= attr_heap <:= (av_info_ptr, AVI_Empty)
		clear_attr attr attr_heap
			= attr_heap


653
654
freshExistentialVariables type_variables var_store attr_store type_heaps
	= foldSt fresh_existential_variable type_variables ([], var_store, attr_store, type_heaps) 
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
655
where
656
657
658
659
660
661
	fresh_existential_variable {atv_variable={tv_info_ptr},atv_attribute} (exi_attr_vars, var_store, attr_store, type_heaps =: {th_vars, th_attrs})
		# th_vars = th_vars <:= (tv_info_ptr, TVI_Type (TempQV var_store))
		# var_store = inc var_store
		# (exi_attr_vars, attr_store, th_attrs) = fresh_existential_attribute atv_attribute (exi_attr_vars, attr_store, th_attrs)
		= (exi_attr_vars, var_store, attr_store, { type_heaps & th_vars = th_vars, th_attrs = th_attrs })

662
	fresh_existential_attribute (TA_Var {av_name,av_info_ptr}) (exi_attr_vars, attr_store, attr_heap)
663
		= ([ attr_store : exi_attr_vars ], inc attr_store, attr_heap <:= (av_info_ptr, AVI_Attr (TA_TempVar attr_store)))
664
//			---> ("fresh_existential_attribute", av_info_ptr,av_name)
665
666
667
	fresh_existential_attribute attr state
		= state
	
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
fresh_type_variables :: [ATypeVar] *(*Heap TypeVarInfo,Int) -> *(!*Heap TypeVarInfo,!Int);
fresh_type_variables type_variables state
	= foldSt (\{atv_variable={tv_info_ptr}} (var_heap, var_store) -> (var_heap <:= (tv_info_ptr, TVI_Type (TempV var_store)), inc var_store))
				type_variables state

fresh_attributes :: [AttributeVar] *(*Heap AttrVarInfo,Int) -> *(!*Heap AttrVarInfo,!Int);
fresh_attributes attributes state
	= foldSt (\{av_info_ptr} (attr_heap, attr_store) -> (attr_heap <:= (av_info_ptr, AVI_Attr (TA_TempVar attr_store)), inc attr_store))
		attributes state

fresh_environment :: [AttrInequality] [AttrCoercion] *(Heap AttrVarInfo) -> *(![AttrCoercion],!*Heap AttrVarInfo);
fresh_environment inequalities attr_env attr_heap
	= foldSt fresh_inequality inequalities (attr_env, attr_heap)
	where
		fresh_inequality {ai_demanded,ai_offered} (attr_env, attr_heap)
			# (AVI_Attr dem_temp_attr, attr_heap) = readPtr ai_demanded.av_info_ptr attr_heap
			  (AVI_Attr off_temp_attr, attr_heap) = readPtr ai_offered.av_info_ptr attr_heap
			= case dem_temp_attr of
				TA_TempVar dem_attr_var
					-> case off_temp_attr of
						TA_TempVar off_attr_var
							| is_new_ineqality  dem_attr_var off_attr_var attr_env
								-> ([{ac_demanded = dem_attr_var, ac_offered = off_attr_var} : attr_env ], attr_heap)
								-> (attr_env, attr_heap)
						_
							-> (attr_env, attr_heap)
				_
					-> (attr_env, attr_heap)
			
		is_new_ineqality dem_attr_var off_attr_var [{ac_demanded, ac_offered} : attr_env]
			= (dem_attr_var <> ac_demanded || off_attr_var <> ac_offered) && is_new_ineqality dem_attr_var off_attr_var  attr_env
		is_new_ineqality dem_attr_var off_attr_var []
			= True


703
704
705
706
707
708
freshUniversalVariables type_variables state
	= foldSt fresh_universal_variable type_variables state 
where
	fresh_universal_variable {atv_variable={tv_info_ptr}} (var_heap, var_store)
		= (var_heap <:= (tv_info_ptr, TVI_Type (TempQV var_store)), inc var_store)

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
709
freshAlgebraicType :: !(Global Int) ![AlgebraicPattern] !{#CommonDefs} !*TypeState -> (![[AType]],!AType,![AttrCoercion],!*TypeState)
710
freshAlgebraicType {glob_module, glob_object} patterns common_defs ts=:{ts_var_store,ts_attr_store,ts_type_heaps,ts_exis_variables}
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
711
712
713
	# {td_rhs,td_args,td_attrs,td_name,td_attribute} = common_defs.[glob_module].com_type_defs.[glob_object]
	# (th_vars, ts_var_store)		= fresh_type_variables td_args (ts_type_heaps.th_vars, ts_var_store)
	  (th_attrs, ts_attr_store)		= fresh_attributes td_attrs (ts_type_heaps.th_attrs, ts_attr_store)
714
715
716
717
718
	  ts_type_heaps					= { ts_type_heaps & th_vars = th_vars, th_attrs = th_attrs }
	  (cons_types, alg_type, attr_env, ts_var_store, ts_attr_store, ts_type_heaps, ts_exis_variables)
	  		= fresh_symbol_types patterns common_defs.[glob_module].com_cons_defs ts_var_store ts_attr_store ts_type_heaps ts_exis_variables
	= (cons_types, alg_type, attr_env,
			{ ts & ts_var_store = ts_var_store, ts_attr_store = ts_attr_store, ts_type_heaps = ts_type_heaps, ts_exis_variables = ts_exis_variables })
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
719
//		---> ("freshAlgebraicType", alg_type, cons_types)
720
721
where
	fresh_symbol_types [{ap_symbol={glob_object},ap_expr}] cons_defs var_store attr_store type_heaps all_exis_variables
722
		# {cons_type = ct=:{st_args,st_attr_env,st_result}, cons_index, cons_exi_vars} = cons_defs.[glob_object.ds_index]
723
		  (exis_variables, var_store, attr_store, type_heaps) = freshExistentialVariables cons_exi_vars var_store attr_store type_heaps
724
//		  	-?-> (not (isEmpty cons_exi_vars), ("fresh_symbol_types", cons_exi_vars, ct))
725
726
727
728
729
730
731
732
	  	  (attr_env, th_attrs) 		= fresh_environment st_attr_env [] type_heaps.th_attrs
	  	  (result_type, type_heaps)	= freshCopy st_result { type_heaps & th_attrs = th_attrs }
	  	  (fresh_args, type_heaps)	= freshCopy st_args type_heaps
	  	  all_exis_variables		= add_exis_variables ap_expr exis_variables all_exis_variables
		= ([fresh_args], result_type, attr_env, var_store, attr_store, type_heaps, all_exis_variables)
	fresh_symbol_types [{ap_symbol={glob_object},ap_expr} : patterns] cons_defs var_store attr_store type_heaps all_exis_variables
		# (cons_types, result_type, attr_env, var_store, attr_store, type_heaps, all_exis_variables)
				= fresh_symbol_types patterns cons_defs var_store attr_store type_heaps all_exis_variables
733
		  {cons_type = ct=:{st_args,st_attr_env}, cons_index, cons_exi_vars} = cons_defs.[glob_object.ds_index]
734
		  (exis_variables, var_store, attr_store, type_heaps) = freshExistentialVariables cons_exi_vars var_store attr_store type_heaps
735
//		  	-?-> (not (isEmpty cons_exi_vars), ("fresh_symbol_types", cons_exi_vars, ct))
736
737
738
739
740
741
742
743
744
		  (attr_env, th_attrs) 		= fresh_environment st_attr_env attr_env type_heaps.th_attrs
	  	  (fresh_args, type_heaps) 	= freshCopy st_args { type_heaps & th_attrs = th_attrs }
	  	  all_exis_variables		= add_exis_variables ap_expr exis_variables all_exis_variables
		= ([fresh_args : cons_types], result_type, attr_env, var_store, attr_store, type_heaps, all_exis_variables)

	add_exis_variables expr [] exis_variables
		= exis_variables
	add_exis_variables expr new_exis_variables exis_variables
		= [(CP_Expression expr, new_exis_variables) : exis_variables]
Sjaak Smetsers's avatar
Sjaak Smetsers committed
745

746
747
748
749
750
751
752
753
754
755
756
757
758
759
fresh_overloaded_list_type [{ap_symbol}:patterns] pd_cons_symbol pd_nil_symbol decons_u_index nil_u_index stdStrictLists_index pos functions common_defs ts
	| ap_symbol.glob_module==cPredefinedModuleIndex
		| ap_symbol.glob_object.ds_index==pd_cons_symbol-FirstConstructorPredefinedSymbolIndex
			# (argument_types,result_type,tst_context,tst_attr_env,ts) = make_cons_type_from_decons_type stdStrictLists_index decons_u_index common_defs ts
			= case patterns of
				[]
					-> ([argument_types],result_type,tst_context,tst_attr_env,ts)
				[pattern=:{ap_symbol}]
					| ap_symbol.glob_module==cPredefinedModuleIndex && ap_symbol.glob_object.ds_index==pd_nil_symbol-FirstConstructorPredefinedSymbolIndex
						-> ([argument_types,[]],result_type,tst_context,tst_attr_env,ts)
		| ap_symbol.glob_object.ds_index==pd_nil_symbol-FirstConstructorPredefinedSymbolIndex
			= case patterns of
				[]
					# {ft_type,ft_symb,ft_type_ptr,ft_specials} = functions.[stdStrictLists_index].[nil_u_index]
760
					# (fun_type_copy, ts) = determineSymbolTypeOfFunction pos ft_symb 0 ft_type ft_type_ptr common_defs ts
761
762
763
764
765
766
767
					  {tst_args,tst_result,tst_context,tst_attr_env}=fun_type_copy
					-> ([tst_args],tst_result,tst_context,tst_attr_env,ts)
				[pattern=:{ap_symbol}]
					| ap_symbol.glob_module==cPredefinedModuleIndex && ap_symbol.glob_object.ds_index==pd_cons_symbol-FirstConstructorPredefinedSymbolIndex
						# (argument_types,result_type,tst_context,tst_attr_env,ts) = make_cons_type_from_decons_type stdStrictLists_index decons_u_index common_defs ts
						-> ([[],argument_types],result_type,tst_context,tst_attr_env,ts)
			= abort "fresh_overloaded_list_type"
768
	where
769
770
		make_cons_type_from_decons_type stdStrictLists_index decons_u_index common_defs ts
			# {me_symb,me_type,me_type_ptr} = common_defs.[stdStrictLists_index].com_member_defs.[decons_u_index]
771
			  (fun_type_copy,ts) = determineSymbolTypeOfFunction pos me_symb 1 me_type me_type_ptr common_defs ts
772
773
			  {tst_args,tst_arity,tst_lifted,tst_result,tst_context,tst_attr_env}=fun_type_copy						  
			# result_type = case tst_args of [t] -> t
774
775
776
			# argument_types = case tst_result.at_type of
									TA _ args=:[arg1,arg2] -> args
									TAS _ args=:[arg1,arg2] _ -> args
777
778
779
780
781
782
783
784
785
786
787
788
789
			= (argument_types,result_type,tst_context,tst_attr_env,ts)

freshOverloadedListType :: !OverloadedListType !CoercionPosition ![AlgebraicPattern] !{#CommonDefs} !{#{#FunType }} !*TypeState -> (![[AType]],!AType,![TypeContext],![AttrCoercion],!*TypeState)
freshOverloadedListType (UnboxedList _ stdStrictLists_index decons_u_index nil_u_index) pos patterns common_defs functions ts
	= fresh_overloaded_list_type patterns PD_UnboxedConsSymbol PD_UnboxedNilSymbol decons_u_index nil_u_index stdStrictLists_index pos functions common_defs ts
freshOverloadedListType (UnboxedTailStrictList _ stdStrictLists_index decons_u_index nil_u_index) pos patterns common_defs functions ts
	= fresh_overloaded_list_type patterns PD_UnboxedTailStrictConsSymbol PD_UnboxedTailStrictNilSymbol decons_u_index nil_u_index stdStrictLists_index pos functions common_defs ts
freshOverloadedListType (OverloadedList _ stdStrictLists_index decons_u_index nil_u_index) pos patterns common_defs functions ts
	= fresh_overloaded_list_type patterns PD_OverloadedConsSymbol PD_OverloadedNilSymbol decons_u_index nil_u_index stdStrictLists_index pos functions common_defs ts

cWithFreshContextVars 		:== True
cWithoutFreshContextVars 	:== False

790
freshSymbolType :: !(Optional CoercionPosition) !Bool !SymbolType {#u:CommonDefs} !*TypeState -> (!TempSymbolType,!*TypeState)
791
freshSymbolType is_appl fresh_context_vars st=:{st_vars,st_args,st_result,st_context,st_attr_vars,st_attr_env,st_arity} common_defs
792
				ts=:{ts_var_store,ts_attr_store,ts_type_heaps,ts_var_heap,ts_cons_variables,ts_exis_variables}
793
	# (th_vars, ts_var_store)	= fresh_type_variables st_vars (ts_type_heaps.th_vars, ts_var_store)
Sjaak Smetsers's avatar
Sjaak Smetsers committed
794
	  (th_attrs, ts_attr_store)	= fresh_attributes st_attr_vars (ts_type_heaps.th_attrs, ts_attr_store)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
795
	  (attr_env, th_attrs)		= freshEnvironment st_attr_env th_attrs 
796
	  type_heaps 				= { ts_type_heaps & th_vars = th_vars, th_attrs = th_attrs }
797
798
799
	  (tst_args, (ts_var_store, ts_attr_store, ts_exis_variables, type_heaps))
	  							= fresh_arg_types is_appl st_args (ts_var_store, ts_attr_store, ts_exis_variables, type_heaps)
	  (tst_result, type_heaps)	= freshCopy st_result type_heaps
800
	  (tst_context, (type_heaps, ts_var_heap)) 	= freshTypeContexts fresh_context_vars st_context (type_heaps, ts_var_heap)
801
	  th_attrs					= clear_attributes st_attr_vars th_attrs
802
803
804
805
	  cons_variables			= foldSt (collect_cons_variables_in_tc common_defs) tst_context [] 
	= ({ tst_args = tst_args, tst_result = tst_result, tst_context = tst_context, tst_attr_env = attr_env, tst_arity = st_arity, tst_lifted = 0 },
	   { ts & ts_var_store = ts_var_store, ts_attr_store = ts_attr_store, ts_type_heaps = type_heaps, ts_var_heap = ts_var_heap,
	   				ts_cons_variables = cons_variables ++ ts_cons_variables, ts_exis_variables = ts_exis_variables })
806
		//---> ("freshSymbolType", st, tst_args, tst_result, tst_context)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
807
	where
808
		fresh_type_variables :: [TypeVar] !(!*TypeVarHeap, !Int) -> (!*TypeVarHeap, !Int)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
809
		fresh_type_variables type_variables state
810
811
812
813
814
815
			= foldSt fresh_type_variable type_variables state
		where
			fresh_type_variable {tv_info_ptr} (var_heap, var_store)
				= (var_heap <:= (tv_info_ptr, TVI_Type (TempV var_store)), inc var_store)
			
		fresh_attributes :: [AttributeVar] !(!*AttrVarHeap, !Int) -> (!*AttrVarHeap, !Int)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
816
		fresh_attributes attributes state
817
818
819
820
821
822
			= foldSt fresh_attribute attributes state
		where
			fresh_attribute {av_info_ptr} (attr_heap, attr_store)
				= (attr_heap <:= (av_info_ptr, AVI_Attr (TA_TempVar attr_store)), inc attr_store)


John van Groningen's avatar
John van Groningen committed
823
		clear_attributes :: [AttributeVar] !*AttrVarHeap -> *AttrVarHeap
824
825
826
827
828
829
		clear_attributes attributes attr_heap
			= foldSt clear_attribute attributes attr_heap
		where
			clear_attribute {av_info_ptr} attr_heap
				= attr_heap <:= (av_info_ptr, AVI_Empty)

830

831
		collect_cons_variables_in_tc common_defs tc=:{tc_class=TCClass {glob_module,glob_object={ds_index}}, tc_types} collected_cons_vars
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
832
833
			# {class_cons_vars} = common_defs.[glob_module].com_class_defs.[ds_index]
			= collect_cons_variables tc_types class_cons_vars collected_cons_vars
834
835
836
		collect_cons_variables_in_tc common_defs tc=:{tc_class=TCGeneric {gtc_class}} collected_cons_vars
			= collect_cons_variables_in_tc common_defs {tc & tc_class=TCClass gtc_class} collected_cons_vars 
		 
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
		collect_cons_variables [] class_cons_vars collected_cons_vars
			= collected_cons_vars
		collect_cons_variables [type : tc_types] class_cons_vars collected_cons_vars
			| class_cons_vars bitand 1 == 0
				= collect_cons_variables tc_types (class_cons_vars >> 1) collected_cons_vars
				= case type of
					TempV temp_var_id 
						-> collect_cons_variables tc_types (class_cons_vars >> 1) (add_variable temp_var_id collected_cons_vars)
//							---> ("collect_cons_variables", temp_var_id)
					_
						-> collect_cons_variables tc_types (class_cons_vars >> 1) collected_cons_vars
						
		add_variable new_var_id []
			= [new_var_id]
		add_variable new_var_id vars=:[var_id : var_ids]
			| new_var_id == var_id
				= vars
				= [var_id : add_variable new_var_id var_ids]
855
856
				
		fresh_arg_types No arg_types (var_store, attr_store, exis_variables, type_heaps)
857
			# (arg_types, type_heaps) = mapSt fresh_arg_type arg_types type_heaps
858
			= (arg_types, (var_store, attr_store, exis_variables, type_heaps))
859
860
861
862
863
864
865
866
		where
			fresh_arg_type at=:{at_attribute, at_type = TFA vars type} type_heaps
				# (fresh_attribute, th_attrs)	= freshCopyOfTypeAttribute at_attribute type_heaps.th_attrs
				  (at_type, type_heaps)			= freshCopyOfTFAType vars type { type_heaps & th_attrs = th_attrs }
				= ({ at &  at_attribute = fresh_attribute, at_type = at_type }, type_heaps)
			fresh_arg_type at type_heaps
				= freshCopy at type_heaps

867
868
869
870
871
		fresh_arg_types (Yes pos) arg_types (var_store, attr_store, exis_variables, type_heaps)
			= mapSt (fresh_arg_type pos) arg_types (var_store, attr_store, exis_variables, type_heaps)
		where
			fresh_arg_type pos at=:{at_attribute, at_type = TFA vars type} (var_store, attr_store, exis_variables, type_heaps)
				# (fresh_attribute, th_attrs)	= freshCopyOfTypeAttribute at_attribute type_heaps.th_attrs
872
873
874
875
876
				# (var_store, attr_store, new_exis_variables, bound_attr_vars, type_heaps)
						= foldSt fresh_var_and_attr vars (var_store, attr_store, [], [], { type_heaps & th_attrs = th_attrs })
				  (fresh_type, type_heaps) = freshCopy type type_heaps
				  type_heaps = { type_heaps & th_vars = foldSt clear_binding_of_type_var vars type_heaps.th_vars,
				  							  th_attrs = foldSt clear_binding_of_attr_var bound_attr_vars type_heaps.th_attrs }
877
				= ({ at &  at_attribute = fresh_attribute, at_type = fresh_type },
878
						(var_store, attr_store, addToExistentialVariables pos new_exis_variables exis_variables, type_heaps))
879
880
881
882
			fresh_arg_type _ at (var_store, attr_store, exis_variables, type_heaps)
				# (fresh_at, type_heaps) = freshCopy at type_heaps
				= (fresh_at, (var_store, attr_store, exis_variables, type_heaps))

883
884
885
886
887
			fresh_var_and_attr {atv_attribute, atv_variable = tv=:{tv_info_ptr}} (var_store, attr_store, exis_variables, bound_attr_vars, type_heaps)
				# (attr_store, exis_variables, bound_attr_vars, th_attrs)
						= fresh_attr atv_attribute (attr_store, exis_variables, bound_attr_vars, type_heaps.th_attrs)
				= (inc var_store,  attr_store, exis_variables, bound_attr_vars,
						{ type_heaps & th_vars = type_heaps.th_vars <:= (tv_info_ptr, TVI_Type (TempQV var_store)), th_attrs = th_attrs })
888
			where
889
890
891
892
893
894
895
				fresh_attr var=:(TA_Var {av_info_ptr}) (attr_store, exis_variables, bound_attr_vars, attr_heap)
					# (av_info, attr_heap) = readPtr av_info_ptr attr_heap
					= case av_info of
						AVI_Empty
							-> (inc attr_store, [attr_store : exis_variables], [av_info_ptr : bound_attr_vars], attr_heap <:= (av_info_ptr, AVI_Attr (TA_TempVar attr_store)))
						AVI_Attr (TA_TempVar _)
							-> (attr_store, exis_variables, bound_attr_vars, attr_heap)
896
						_ -> (abort "invalid av_info") ---> ("freshSymbolType av_info", var, av_info)	
897
898
				fresh_attr attr state
					= state
899
900
901
902
903
904
905
				
			clear_binding_of_type_var {atv_variable = {tv_info_ptr}} type_var_heap
					= type_var_heap <:= (tv_info_ptr, TVI_Empty)
					
			clear_binding_of_attr_var av_info_ptr attr_var_heap
				= attr_var_heap <:= (av_info_ptr, AVI_Empty)

906
			
907
908
909
910
addToExistentialVariables pos [] exis_variables
	= exis_variables
addToExistentialVariables pos new_exis_variables exis_variables
	= [(pos, new_exis_variables) : exis_variables]
911

912
	
913
freshInequality :: AttrInequality *(Heap AttrVarInfo) -> (!AttrCoercion,!.Heap AttrVarInfo);
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
914
915
916
917
918
919
920
921
922
923
924
925
926
927
freshInequality {ai_demanded,ai_offered} attr_heap
	# (av_dem_info, attr_heap) = readPtr ai_demanded.av_info_ptr attr_heap
	  (av_off_info, attr_heap) = readPtr ai_offered.av_info_ptr attr_heap
	  (AVI_Attr (TA_TempVar dem_attr_var)) = av_dem_info
	  (AVI_Attr (TA_TempVar off_attr_var)) = av_off_info
	= ({ac_demanded = dem_attr_var, ac_offered = off_attr_var}, attr_heap) // <<- (av_dem_info,av_off_info)
	
freshEnvironment [ineq : ineqs] attr_heap
	# (fresh_ineq, attr_heap) = freshInequality ineq attr_heap
	  (fresh_env, attr_heap) = freshEnvironment ineqs attr_heap
	= ([fresh_ineq : fresh_env], attr_heap)
freshEnvironment [] attr_heap
	= ([], attr_heap)

Sjaak Smetsers's avatar
Sjaak Smetsers committed
928
929
freshTypeContexts fresh_context_vars tcs cs_and_var_heap
	= mapSt (fresh_type_context fresh_context_vars) tcs cs_and_var_heap
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
930
where	
931
932
	fresh_type_context fresh_context_vars tc=:{tc_types} (type_heaps, var_heap)
		# (tc_types, type_heaps) = mapSt fresh_context_type tc_types type_heaps
Sjaak Smetsers's avatar
Sjaak Smetsers committed
933
934
		| fresh_context_vars
			# (new_info_ptr, var_heap) = newPtr VI_Empty var_heap
935
936
			= ({ tc & tc_types = tc_types, tc_var = new_info_ptr }, (type_heaps, var_heap))
			= ({ tc & tc_types = tc_types}, (type_heaps, var_heap))
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
937

938
939
940
941
942
943
	fresh_context_type (CV tv :@: types) type_heaps=:{th_vars}
		# (fresh_cons_var, th_vars)		= freshConsVariable tv th_vars
		  (types, type_heaps) = freshCopy types { type_heaps & th_vars = th_vars }
		= (fresh_cons_var :@: types, type_heaps)
	fresh_context_type type type_heaps
		= freshCopy type type_heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
944
945
946

freshAttributedVariable :: !u:TypeState -> (!AType, !u:TypeState)
freshAttributedVariable ts=:{ts_var_store,ts_attr_store}
947
	= ({ at_attribute = TA_TempVar ts_attr_store, at_type = TempV ts_var_store },
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
948
949
950
951
	     {ts & ts_var_store = inc ts_var_store, ts_attr_store = inc ts_attr_store})

freshNonUniqueVariable :: !u:TypeState -> (!AType, !u:TypeState)
freshNonUniqueVariable ts=:{ts_var_store}
952
	= ({ at_attribute = TA_Multi, at_type = TempV ts_var_store },
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
953
954
955
956
957
958
959
960
961
962
963
964
	     {ts & ts_var_store = inc ts_var_store})

freshAttribute :: !u:TypeState -> (!TypeAttribute, !u:TypeState)
freshAttribute ts=:{ts_attr_store}
	= (TA_TempVar ts_attr_store, {ts & ts_attr_store = inc ts_attr_store})


::	PropState =
	{	prop_type_heaps	:: !.TypeHeaps
	,	prop_td_infos	:: !.TypeDefInfos
	,	prop_attr_vars	:: ![AttributeVar]
	,	prop_attr_env	:: ![AttrInequality]
965
	,	prop_error		:: !.Optional .ErrorAdmin
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
966
967
	}

968
attribute_error type_attr No
969
	= No // XXX abort ("sanity check nr 723 failed in module type"--->("type_attr", type_attr))
970
attribute_error type_attr (Yes err)
971
	# err = errorHeading "Type error" err
972
	= Yes { err & ea_file = err.ea_file <<< "* attribute expected instead of " <<< type_attr <<< '\n' }
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
973

974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
add_propagation_attributes_to_atypes modules [] ps
	= ([], [], ps) 
add_propagation_attributes_to_atypes modules [atype : atypes] ps
	# (atype, prop_class, ps) = addPropagationAttributesToAType modules atype ps
	  (atypes, prop_classes, ps) = add_propagation_attributes_to_atypes modules atypes ps
	= ([atype : atypes], [prop_class : prop_classes], ps)

determine_attribute_of_cons modules TA_Unique cons_args prop_class attr_var_heap attr_vars attr_env ps_error
	= (TA_Unique, prop_class >> length cons_args, attr_var_heap, attr_vars, attr_env, ps_error)
determine_attribute_of_cons modules cons_attr cons_args prop_class attr_var_heap attr_vars attr_env ps_error
	# (cumm_attr, prop_attrs, prop_class) = determine_cummulative_attribute cons_args TA_Multi [] prop_class
	  (comb_attr, attr_var_heap, attr_vars, attr_env, ps_error)
	  		= combine_attributes cons_attr cumm_attr prop_attrs attr_var_heap attr_vars attr_env ps_error
	= (comb_attr, prop_class, attr_var_heap, attr_vars, attr_env, ps_error)
where
	determine_cummulative_attribute [] cumm_attr attr_vars prop_class
		= (cumm_attr, attr_vars, prop_class)
991
	determine_cummulative_attribute [t=:{at_attribute} : types ] cumm_attr attr_vars prop_class