type.icl 158 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
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
instance toString BoundVar
where
56
	toString varid = varid.var_ident.id_name
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
57

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 = { err & ea_file = err.ea_file <<< " cannot unify types:\n" }
			# err = { err & ea_file = err.ea_file <<< " " <:: (type_error_format, t1, No) <<< '\n' }
			# err = { err & ea_file = err.ea_file <<< " " <:: (type_error_format, t2, No) <<< '\n' }
			-> err;
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
	  ea_file = case position of
238
  				CP_Expression _
239
	  				-> ea_file <<< " near " <<< position <<< " :"
240
241
	  			_
	  				-> ea_file
242
243
244
245
	  ea_file = ea_file <<< " cannot unify types:\n"
	  ea_file = ea_file <<< " " <:: (type_error_format, t1, No) <<< "\n"
	  ea_file = ea_file <<< " " <:: (type_error_format, t2, No) <<< "\n"
	= { err & ea_file = ea_file}
246
247
248
249
250
251
252
253
254
255
256
257
258

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' }
			

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

268
269
270
isIndirection TE	= False
isIndirection type	= True

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

273
instance unify (a, b) | unify a & unify b
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
274
275
276
277
278
279
280
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)

281
instance unify [a] | unify a
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
282
283
284
285
286
287
288
289
290
291
292
293
294
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)
295
296
297
298
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
299
300
301
302
		= unify_variable_with_type tv_number type2 attr2 subst modules heaps
	where
		unify_variable_with_type :: Int Type TypeAttribute *{!Type} TypeInput *TypeHeaps -> (!Bool,!*{!Type},!*TypeHeaps)
		unify_variable_with_type tv_number1 tv=:(TempV tv_number2) attr subst modules heaps
303
304
			# (type2, subst) = subst![tv_number2]
			| isIndirection type2
305
				= unify_variable_with_type tv_number1 type2 attr subst modules heaps
306
			| tv_number1 == tv_number2
307
308
309
				= (True, subst, heaps)
				= (True, { subst & [tv_number1] = tv}, heaps)
		unify_variable_with_type tv_number type attr subst modules heaps
310
			| containsTypeVariable tv_number type subst
311
312
313
314
315
				# (succ, type, heaps) = tryToExpand type attr modules.ti_common_defs heaps
				| succ
					= unify_variable_with_type tv_number type attr subst modules heaps
					= (False, subst, heaps)
				= (True, { subst & [tv_number] = type},heaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
316
317
318
319
320
321
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)
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
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
338
339
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
340
341
342
343
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
344
unifyTypes (cons_var :@: types) attr1 type2 attr2 modules subst heaps
345
346
	# (_, 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
347
unifyTypes type1 attr1 (cons_var :@: types) attr2 modules subst heaps
348
349
	# (_, 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
350
351
352
353
354
355
356
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
357
358
	# (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
359
360
361
362
	| succ1 || succ2
		= unifyTypes type1 attr1 type2 attr2 modules subst heaps
		= (False, subst, heaps)

363
364
365
366
367
368
369
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)

370
371
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
372
373
374
	#! type_def = ti_common_defs.[glob_module].com_type_defs.[glob_object]
	= case type_def.td_rhs of
		SynType {at_type}
375
			# (expanded_type, type_heaps) = substituteType type_def.td_attribute type_attr type_def.td_args type_args at_type type_heaps
376
			-> (True, expanded_type, type_heaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
377
378
		_
			-> (False, type, type_heaps)
379
380
381
382
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}
383
			# (expanded_type, type_heaps) = substituteType type_def.td_attribute type_attr type_def.td_args type_args at_type type_heaps
384
385
386
			-> (True, expanded_type, type_heaps)
		_
			-> (False, type, type_heaps)
387
tryToExpand type type_attr modules type_heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
388
389
	= (False, type, type_heaps)

390
391
392
393
394
395
396
397
398
399
400
401
402
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))
403
404
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)
405
406
407
408
409
410
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)
411
412
413
//AA..
simplifyTypeApplication TArrow [type1, type2] 
	= (True, type1 --> type2)
Artem Alimarine's avatar
Artem Alimarine committed
414
415
simplifyTypeApplication TArrow [type] 
	= (True, TArrow1 type)
416
417
418
simplifyTypeApplication (TArrow1 type1) [type2] 
	= (True, type1 --> type2)
//..AA
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
446
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
447
448
449
450
	# diff = type_cons.type_arity - length type_args
	| diff >= 0 
		# (succ, subst, heaps) = unify type_args (drop diff cons_args) modules subst heaps
		| succ
451
			= 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
452
453
		    = (False, subst, heaps)
		= (False, subst, heaps)
454

455
456
457
458
459
460
461
462
463
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
464
// AA..
465
466
467
468
469
470
471
472
473
474
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
475
476
477
478
479
480
481
482
483
484
485
486
487
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
488
// ..AA 		
Artem Alimarine's avatar
Artem Alimarine committed
489

490
491
492
493
494
495
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
496
497
	  diff = arity1 - arity2
	| diff == 0
498
		# (succ, subst) = unify_cv_with_cv is_exist1 tv_number1 is_exist2 tv_number2 subst
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
499
		| succ
500
		    = unify type_args1 type_args2 modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
501
502
503
			= (False, subst, heaps)
	| diff < 0
		# diff = 0 - diff
504
		  (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
505
		| succ
506
		    = unify type_args1 (drop diff type_args2) modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
507
			= (False, subst, heaps)
508
//	| otherwise
509
		# (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
510
		| succ
511
		    = unify (drop diff type_args1) type_args2 modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
512
			= (False, subst, heaps)
513
514
515
516
517
518
519
520
521
522
523
524
	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
525
526
527
528
529
530
531
	
instance fromInt TypeAttribute
where
	fromInt AttrUni		= TA_Unique
	fromInt AttrMulti	= TA_Multi
	fromInt av_number	= TA_TempVar av_number

532
533


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

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

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

Sjaak Smetsers's avatar
Sjaak Smetsers committed
548

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
549
550
551
freshCopyOfTypeAttribute (TA_Var avar) attr_var_heap
	= freshCopyOfAttributeVar avar attr_var_heap
freshCopyOfTypeAttribute (TA_RootVar avar) attr_var_heap
552
	= freshCopyOfAttributeVar avar attr_var_heap
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
553
554
555
556
557
558
559
560
561
562
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

563
freshCopyOfTypeVariable {tv_ident,tv_info_ptr} type_heaps=:{th_vars}
564
565
	# (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
566
567

freshConsVariable {tv_info_ptr} type_var_heap
568
	# (tv_info, type_var_heap) = readPtr tv_info_ptr type_var_heap
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
569
570
	= (to_constructor_variable tv_info, type_var_heap)
	where
571
572
573
574
575
576
		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
577
				TV var		
578
					-> CV var
579
580
581
582
				_ 	
					-> 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
583
584
585

instance freshCopy AType
where 	
586
587
588
589
590
591
592
593
594
	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)
595
596
597
598
	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)
599

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
600
601
instance freshCopy Type
where
602
603
604
605
606
	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)
607
608
609
	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)
610
611
612
613
	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)
614
615
616
617
618
//AA..
	freshCopy (TArrow1 arg_type) type_heaps
		# (arg_type, type_heaps) = freshCopy arg_type type_heaps
		= (TArrow1 arg_type, type_heaps)
//..AA		
619
	freshCopy (TFA vars type) type_heaps
620
		= freshCopyOfTFAType vars type type_heaps
621
622
	freshCopy type type_heaps
		= (type, type_heaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
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
653
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


654
655
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
656
where
657
658
659
660
661
662
	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 })

663
	fresh_existential_attribute (TA_Var {av_ident,av_info_ptr}) (exi_attr_vars, attr_store, attr_heap)
664
		= ([ attr_store : exi_attr_vars ], inc attr_store, attr_heap <:= (av_info_ptr, AVI_Attr (TA_TempVar attr_store)))
665
//			---> ("fresh_existential_attribute", av_info_ptr,av_ident)
666
667
668
	fresh_existential_attribute attr state
		= state
	
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
703
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


704
705
706
707
708
709
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)

710
freshAlgebraicType :: !(Global Int) ![AlgebraicPattern] !{#CommonDefs} !*TypeState -> (![[AType]],!AType,![AttrCoercion],!TypeRhs,!*TypeState)
711
freshAlgebraicType {glob_module, glob_object} patterns common_defs ts=:{ts_var_store,ts_attr_store,ts_type_heaps,ts_exis_variables}
712
	# {td_rhs,td_args,td_attrs,td_ident,td_attribute} = common_defs.[glob_module].com_type_defs.[glob_object]
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
713
714
	# (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)
715
716
717
	  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
718
	= (cons_types, alg_type, attr_env, td_rhs,
719
			{ 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
720
//		---> ("freshAlgebraicType", alg_type, cons_types)
721
722
where
	fresh_symbol_types [{ap_symbol={glob_object},ap_expr}] cons_defs var_store attr_store type_heaps all_exis_variables
723
		# {cons_type = ct=:{st_args,st_attr_env,st_result}, cons_exi_vars} = cons_defs.[glob_object.ds_index]
724
		  (exis_variables, var_store, attr_store, type_heaps) = freshExistentialVariables cons_exi_vars var_store attr_store type_heaps
725
//		  	-?-> (not (isEmpty cons_exi_vars), ("fresh_symbol_types", cons_exi_vars, ct))
726
727
728
729
730
731
732
733
	  	  (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
734
		  {cons_type = ct=:{st_args,st_attr_env}, cons_exi_vars} = cons_defs.[glob_object.ds_index]
735
		  (exis_variables, var_store, attr_store, type_heaps) = freshExistentialVariables cons_exi_vars var_store attr_store type_heaps
736
//		  	-?-> (not (isEmpty cons_exi_vars), ("fresh_symbol_types", cons_exi_vars, ct))
737
738
739
740
741
742
743
744
745
		  (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
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
				[]
760
761
					# {ft_type,ft_ident,ft_type_ptr,ft_specials} = functions.[stdStrictLists_index].[nil_u_index]
					# (fun_type_copy, ts) = determineSymbolTypeOfFunction pos ft_ident 0 ft_type ft_type_ptr common_defs ts
762
763
764
765
766
767
768
					  {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"
769
	where
770
		make_cons_type_from_decons_type stdStrictLists_index decons_u_index common_defs ts
771
772
			# {me_ident,me_type,me_type_ptr} = common_defs.[stdStrictLists_index].com_member_defs.[decons_u_index]
			  (fun_type_copy,ts) = determineSymbolTypeOfFunction pos me_ident 1 me_type me_type_ptr common_defs ts
773
774
			  {tst_args,tst_arity,tst_lifted,tst_result,tst_context,tst_attr_env}=fun_type_copy						  
			# result_type = case tst_args of [t] -> t
775
776
777
			# argument_types = case tst_result.at_type of
									TA _ args=:[arg1,arg2] -> args
									TAS _ args=:[arg1,arg2] _ -> args
778
779
780
781
782
783
784
785
786
787
788
789
790
			= (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

791
freshSymbolType :: !(Optional CoercionPosition) !Bool !SymbolType {#u:CommonDefs} !*TypeState -> (!TempSymbolType,!*TypeState)
792
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
793
				ts=:{ts_var_store,ts_attr_store,ts_type_heaps,ts_var_heap,ts_cons_variables,ts_exis_variables}
794
	# (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
795
	  (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
796
	  (attr_env, th_attrs)		= freshEnvironment st_attr_env th_attrs 
797
	  type_heaps 				= { ts_type_heaps & th_vars = th_vars, th_attrs = th_attrs }
798
799
800
	  (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
801
	  (tst_context, (type_heaps, ts_var_heap)) 	= freshTypeContexts fresh_context_vars st_context (type_heaps, ts_var_heap)
802
	  type_heaps = {type_heaps & th_attrs = clear_attributes st_attr_vars type_heaps.th_attrs}
803
804
805
806
	  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 })
807
		//---> ("freshSymbolType", st, tst_args, tst_result, tst_context)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
808
	where
809
		
810
		fresh_type_variables :: [TypeVar] !(!*TypeVarHeap, !Int) -> (!*TypeVarHeap, !Int)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
811
		fresh_type_variables type_variables state
812
813
814
815
816
817
			= 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
818
		fresh_attributes attributes state
819
820
821
822
823
824
			= 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
825
		clear_attributes :: [AttributeVar] !*AttrVarHeap -> *AttrVarHeap
826
827
828
829
830
831
		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)

832

833
		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
834
835
			# {class_cons_vars} = common_defs.[glob_module].com_class_defs.[ds_index]
			= collect_cons_variables tc_types class_cons_vars collected_cons_vars
836
837
838
		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
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
		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]
857
858
				
		fresh_arg_types No arg_types (var_store, attr_store, exis_variables, type_heaps)
859
			# (arg_types, type_heaps) = mapSt fresh_arg_type arg_types type_heaps
860
			= (arg_types, (var_store, attr_store, exis_variables, type_heaps))
861
862
863
864
865
866
867
868
		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

869
870
871
872
873
		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
874
875
876
877
878
				# (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 }
879
				= ({ at &  at_attribute = fresh_attribute, at_type = fresh_type },
880
						(var_store, attr_store, addToExistentialVariables pos new_exis_variables exis_variables, type_heaps))
881
882
883
884
			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))

885
886
887
888
889
			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 })
890
			where
891
892
893
894
895
896
897
				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)
898
						_ -> (abort "invalid av_info") ---> ("freshSymbolType av_info", var, av_info)	
899
900
				fresh_attr attr state
					= state
901
902
903
904
905
906
907
				
			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)

908
			
909
910
911
912
addToExistentialVariables pos [] exis_variables
	= exis_variables
addToExistentialVariables pos new_exis_variables exis_variables
	= [(pos, new_exis_variables) : exis_variables]
913

914
	
915
freshInequality :: AttrInequality *(Heap AttrVarInfo) -> (!AttrCoercion,!.Heap AttrVarInfo);
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
916
917
918
919
920
921
922
923
924
925
926
927
928
929
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
930
931
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
932
where	
933
934
	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
935
936
		| fresh_context_vars
			# (new_info_ptr, var_heap) = newPtr VI_Empty var_heap
937
938
			= ({ 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
939

940
941
942
943
944
945
	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
946
947
948

freshAttributedVariable :: !u:TypeState -> (!AType, !u:TypeState)
freshAttributedVariable ts=:{ts_var_store,ts_attr_store}
949
	= ({ at_attribute = TA_TempVar ts_attr_store, at_type = TempV ts_var_store },
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
950
951
952
953
	     {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}
954
	= ({ at_attribute = TA_Multi, at_type = TempV ts_var_store },
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
955
956
957
958
959
960
961
962
963
964
965
966
	     {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