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

3
import StdEnv, compare_types
4
import syntax, typesupport, check, analtypes, overloading, unitype, refmark, predef, utilities, compare_constructor
5
import genericsupport
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
6
7

::	TypeInput =
John van Groningen's avatar
John van Groningen committed
8
	! {	ti_common_defs	:: !{# CommonDefs }
9
10
	,	ti_functions	:: !{# {# FunType }}
	,	ti_main_dcl_module_n :: !Int
John van Groningen's avatar
John van Groningen committed
11
	,	ti_expand_newtypes :: !Bool
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
	arraySubst tcv=:((cv=:CV _) :@: types) subst
		// should occur only for A. type variables
		# (changed,types, subst) = arraySubst types subst
		| changed
			= (True, cv :@: types, subst)
			= (False, tcv, subst)
112
113
114
115
116
	arraySubst type=:(TArrow1 arg_type) subst
		# (changed, arg_type, subst) = arraySubst arg_type subst
		| changed
			= (changed, TArrow1 arg_type, subst)
			= (False, type, subst)
117
118
119
120
121
	arraySubst tfa_type=:(TFA vars type) subst
		# (changed, type, subst) = arraySubst type subst
		| changed
			= (changed, TFA vars type, subst)
			= (False, tfa_type, subst)
122

123
	arraySubst type subst
124
		= (False, type, subst)
125

126
127
128
129
130
131
132
133
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
134
135
where
	arraySubst [] subst
136
137
138
		= (False, [], subst)
	arraySubst t=:[type : types ] subst
		# (changed, (type, types), subst) = arraySubst (type, types) subst
139
		| changed
140
141
			= (True, [type : types ], subst)
			= (False, t, subst)
142

143
144
145
instance arraySubst TempSymbolType
where
	arraySubst tst=:{tst_args,tst_result,tst_context} subst
146
		# (changed, (tst_args, (tst_result, tst_context)), subst) = arraySubst (tst_args, (tst_result, tst_context)) subst
147
		| changed
148
149
			= (True, {tst & tst_args = tst_args, tst_result = tst_result, tst_context = tst_context}, subst)
			= (False, tst, subst)
150
151
152
153

instance arraySubst TypeContext
where
	arraySubst tc=:{tc_types} subst
154
		# (changed, tc_types, subst) = arraySubst tc_types subst
155
156
157
158
		| changed
			= (True,{ tc & tc_types = tc_types}, subst)
			= (False, tc, subst)

159
instance arraySubst CaseType
160
where
161
162
	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
163
164
		| changed
			= (True,{ ct & ct_pattern_type = ct_pattern_type, ct_result_type = ct_result_type, ct_cons_types = ct_cons_types }, subst)
165
			= (False, ct, subst)
166

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

169
instance containsTypeVariable [a] | containsTypeVariable a
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
170
where
171
172
173
	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
174
175
		= False

176
instance containsTypeVariable AType
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
177
where
178
	containsTypeVariable var_id {at_type} subst = containsTypeVariable var_id at_type subst
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
179

180
instance containsTypeVariable Type
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
181
where
182
183
184
185
186
187
188
189
190
	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
	containsTypeVariable var_id (TA cons_id cons_args) subst
		= containsTypeVariable var_id cons_args subst
191
192
	containsTypeVariable var_id (TAS cons_id cons_args _) subst
		= containsTypeVariable var_id cons_args subst
193
194
	containsTypeVariable var_id (type :@: types) subst
		= containsTypeVariable var_id type subst || containsTypeVariable var_id types subst
195
196
	containsTypeVariable var_id (TArrow1 arg_type) subst
		= containsTypeVariable var_id arg_type subst
197
	containsTypeVariable _ _ _
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
198
199
		= False

200
instance containsTypeVariable ConsVariable
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
201
where
202
203
204
205
206
207
	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
208
209
		= False

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

213
cannotUnify t1 t2 position=:(CP_Expression expr) common_defs err=:{ea_loc=[ip:_]}
214
215
216
	= case tryToOptimizePosition expr of
		Yes (id_name, line)
			# err = pushErrorAdmin { ip & ip_ident.id_name = id_name, ip_line = line } err
217
218
			  err = errorHeading type_error err
			  err = popErrorAdmin err
219
220
221
222
			  err = { err & ea_file = err.ea_file <<< " cannot unify demanded type with offered type:\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
223
		_
224
225
226
			-> cannot_unify t1 t2 position common_defs err
cannotUnify t1 t2 position common_defs err
	= cannot_unify t1 t2 position common_defs err
227

228
cannot_unify t1 t2 position common_defs err
229
230
231
232
	# (err=:{ea_file}) = errorHeading type_error err
	  ea_file = case position of
				CP_FunArg _ _
					-> ea_file <<< "\"" <<< position <<< "\""
233
				CP_SymbArg {symb_kind=SK_Constructor {glob_module,glob_object},symb_ident} arg_n
234
235
					#! type_index = common_defs.[glob_module].com_cons_defs.[glob_object].cons_type_index
					-> case common_defs.[glob_module].com_type_defs.[type_index].td_rhs of
236
237
238
239
240
241
242
243
244
						RecordType {rt_fields}
							# field_name = rt_fields.[arg_n-1].fs_ident.id_name
							  record_name = symb_ident.id_name
							  record_name = if (record_name.[0]=='_') (record_name % (1,size record_name-1)) record_name
							-> ea_file <<< "\"" <<< "field " <<< field_name <<< " of " <<< record_name <<< "\""
						_
							-> ea_file <<< "\"" <<< position <<< "\""
				CP_SymbArg _ _
					-> ea_file <<< "\"" <<< position <<< "\""
245
246
247
				CP_LiftedFunArg _ _
					-> ea_file <<< "\"" <<< position <<< "\""
  				CP_Expression _
248
	  				-> ea_file <<< " near " <<< position <<< " :"
249
250
	  			_
	  				-> ea_file
251
	  ea_file = ea_file <<< " cannot unify demanded type with offered type:\n"
252
253
254
	  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}
255
256
257
258
259
260
261
262
263
264
265
266
267

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

268
269
tryToOptimizePosition (Case {case_ident=Yes {id_name}})
	= optBeautifulizeIdent id_name
270
271
tryToOptimizePosition (App {app_symb={symb_ident}})
	= optBeautifulizeIdent symb_ident.id_name
272
273
274
tryToOptimizePosition (fun @ _)
	= tryToOptimizePosition fun
tryToOptimizePosition _
Martin Wierich's avatar
Martin Wierich committed
275
	= No
276

277
278
279
isIndirection TE	= False
isIndirection type	= True

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

282
instance unify (a, b) | unify a & unify b
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
283
284
285
286
287
288
289
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)

290
instance unify [a] | unify a
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
291
292
293
294
295
296
297
298
299
300
301
302
303
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)
304
305
306
307
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
308
309
310
311
		= 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
312
313
			# (type2, subst) = subst![tv_number2]
			| isIndirection type2
314
				= unify_variable_with_type tv_number1 type2 attr subst modules heaps
315
			| tv_number1 == tv_number2
316
317
318
				= (True, subst, heaps)
				= (True, { subst & [tv_number1] = tv}, heaps)
		unify_variable_with_type tv_number type attr subst modules heaps
319
			| containsTypeVariable tv_number type subst
John van Groningen's avatar
John van Groningen committed
320
				# (succ, type, heaps) = tryToExpandInUnify type attr modules heaps
321
322
323
324
				| 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
325
326
327
328
329
330
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)
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
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
347
348
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
349
350
351
352
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
353
unifyTypes (cons_var :@: types) attr1 type2 attr2 modules subst heaps
John van Groningen's avatar
John van Groningen committed
354
	# (_, type2, heaps) = tryToExpandInUnify type2 attr2 modules heaps
355
	= unifyTypeApplications cons_var attr1 types type2 attr2 modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
356
unifyTypes type1 attr1 (cons_var :@: types) attr2 modules subst heaps
John van Groningen's avatar
John van Groningen committed
357
	# (_, type1, heaps) = tryToExpandInUnify type1 attr1 modules heaps
358
	= unifyTypeApplications cons_var attr2 types type1 attr1 modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
359
360
361
362
363
364
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)
365
366
367
368
369
370
unifyTypes t1=:(TempQDV qv_number1) attr1 t2=:(TempQDV qv_number2) attr2 modules subst heaps
	= (qv_number1 == qv_number2, subst, heaps)
unifyTypes (TempQDV qv_number) attr1 type attr2 modules subst heaps
	= (False, subst, heaps)
unifyTypes type attr1 (TempQDV qv_number1) attr2 modules subst heaps
	= (False, subst, heaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
371
unifyTypes type1 attr1 type2 attr2 modules subst heaps
John van Groningen's avatar
John van Groningen committed
372
373
	# (succ1, type1, heaps) = tryToExpandInUnify type1 attr1 modules heaps
	  (succ2, type2, heaps) = tryToExpandInUnify type2 attr2 modules heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
374
375
376
377
	| succ1 || succ2
		= unifyTypes type1 attr1 type2 attr2 modules subst heaps
		= (False, subst, heaps)

378
expandAndUnifyTypes t1 attr1 t2 attr2 modules subst heaps
John van Groningen's avatar
John van Groningen committed
379
380
	# (succ1, t1, heaps) = tryToExpandInUnify t1 attr1 modules heaps
	  (succ2, t2, heaps) = tryToExpandInUnify t2 attr2 modules heaps
381
382
383
384
	| succ1 || succ2
		= unifyTypes t1 attr1 t2 attr2 modules subst heaps
		= (False, subst, heaps)

John van Groningen's avatar
John van Groningen committed
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
tryToExpandInUnify :: !Type !TypeAttribute !TypeInput !*TypeHeaps -> (!Bool, !Type, !*TypeHeaps)
tryToExpandInUnify type=:(TA {type_index={glob_object,glob_module}} type_args) type_attr type_input type_heaps
	#! type_def = type_input.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)
		NewType {ds_index}
			| type_input.ti_expand_newtypes
				# {cons_type={st_args=[{at_type}:_]}} = type_input.ti_common_defs.[glob_module].com_cons_defs.[ds_index];
				# (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)
tryToExpandInUnify type=:(TAS {type_index={glob_object,glob_module}} type_args _) type_attr type_input type_heaps
	#! type_def = type_input.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)
		NewType {ds_index}
			| type_input.ti_expand_newtypes
				# {cons_type={st_args=[{at_type}:_]}} = type_input.ti_common_defs.[glob_module].com_cons_defs.[ds_index];
				# (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)
tryToExpandInUnify type type_attr modules type_heaps
	= (False, type, type_heaps)

415
416
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
417
418
419
	#! type_def = ti_common_defs.[glob_module].com_type_defs.[glob_object]
	= case type_def.td_rhs of
		SynType {at_type}
420
			# (expanded_type, type_heaps) = substituteType type_def.td_attribute type_attr type_def.td_args type_args at_type type_heaps
421
			-> (True, expanded_type, type_heaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
422
423
		_
			-> (False, type, type_heaps)
424
425
426
427
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}
428
			# (expanded_type, type_heaps) = substituteType type_def.td_attribute type_attr type_def.td_args type_args at_type type_heaps
429
430
431
			-> (True, expanded_type, type_heaps)
		_
			-> (False, type, type_heaps)
432
tryToExpand type type_attr modules type_heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
433
434
	= (False, type, type_heaps)

435
436
437
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))
438
439
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)
440
441
442
443
444
445
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)
446
447
simplifyTypeApplication (TempQDV tv_number) type_args
	= (True, TempQCDV tv_number :@: type_args)
448
449
simplifyTypeApplication TArrow [type1, type2] 
	= (True, type1 --> type2)
Artem Alimarine's avatar
Artem Alimarine committed
450
451
simplifyTypeApplication TArrow [type] 
	= (True, TArrow1 type)
452
453
simplifyTypeApplication (TArrow1 type1) [type2] 
	= (True, type1 --> type2)
454
455
456
simplifyTypeApplication type type_args
	= (False, type)

457
unifyTypeApplications cv=:(TempCV tv_number) attr1 type_args type2 attr2 modules subst heaps
458
459
460
461
462
463
	# (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)
464
465
466
467
468
469
470
471
		= unifyCVwithType cv type_args type2 modules subst heaps
unifyTypeApplications cv=:(TempQCV tv_number) attr1 type_args type2 attr2 modules subst heaps
	= unifyCVwithType cv type_args type2 modules subst heaps
unifyTypeApplications cv=:(TempQCDV tv_number) attr1 type_args type2 attr2 modules subst heaps
	= unifyCVwithType cv type_args type2 modules subst heaps

unifyCVwithType cv1 type_args1 type=:(cv2 :@: type_args2) modules subst heaps
	= case cv2 of
472
473
474
475
476
		TempCV tv_number2
			# (type2, subst) = subst![tv_number2]
			| isIndirection type2
				# (ok, simplified_type) = simplifyTypeApplication type2 type_args2
				| ok
477
					-> unifyCVwithType cv1 type_args1 simplified_type modules subst heaps
478
					-> (False, subst, heaps)
479
				-> unifyCVApplicationwithCVApplication cv1 type_args1 cv2 type_args2 modules subst heaps
480
		TempQCV tv_number2
481
482
483
484
			-> unifyCVApplicationwithCVApplication cv1 type_args1 cv2 type_args2 modules subst heaps
		TempQCDV tv_number2
			-> unifyCVApplicationwithCVApplication cv1 type_args1 cv2 type_args2 modules subst heaps
unifyCVwithType cv type_args type=:(TA type_cons cons_args) modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
485
486
487
488
	# diff = type_cons.type_arity - length type_args
	| diff >= 0 
		# (succ, subst, heaps) = unify type_args (drop diff cons_args) modules subst heaps
		| succ
489
			= unifyTypes (toTV cv) 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
490
491
		    = (False, subst, heaps)
		= (False, subst, heaps)
492
unifyCVwithType cv type_args type=:(TAS type_cons cons_args strictness) modules subst heaps
493
494
495
496
	# diff = type_cons.type_arity - length type_args
	| diff >= 0 
		# (succ, subst, heaps) = unify type_args (drop diff cons_args) modules subst heaps
		| succ
497
			= unifyTypes (toTV cv) TA_Multi (TAS { type_cons & type_arity = diff } (take diff cons_args) strictness) TA_Multi modules subst heaps
498
499
		    = (False, subst, heaps)
		= (False, subst, heaps)
500
unifyCVwithType cv [type_arg1, type_arg2] type=:(atype1 --> atype2) modules subst heaps
501
502
	# (succ, subst, heaps) = unify (type_arg1, type_arg2) (atype1, atype2) modules subst heaps
	| succ
503
		= unifyTypes (toTV cv) TA_Multi TArrow TA_Multi modules subst heaps
504
		= (False, subst, heaps)		
505
unifyCVwithType cv [type_arg] type=:(atype1 --> atype2) modules subst heaps
506
507
	# (succ, subst, heaps) = unify type_arg atype2 modules subst heaps
	| succ
508
		= unifyTypes (toTV cv) TA_Multi (TArrow1 atype1) TA_Multi modules subst heaps
509
		= (False, subst, heaps)
510
511
512
unifyCVwithType cv [] type=:(atype1 --> atype2) modules subst heaps
	= unifyTypes (toTV cv) TA_Multi type TA_Multi modules subst heaps
unifyCVwithType cv [type_arg] type=:(TArrow1 atype) modules subst heaps
Artem Alimarine's avatar
Artem Alimarine committed
513
514
	# (succ, subst, heaps) = unify type_arg atype modules subst heaps
	| succ
515
		= unifyTypes (toTV cv) TA_Multi TArrow TA_Multi modules subst heaps
Artem Alimarine's avatar
Artem Alimarine committed
516
		= (False, subst, heaps)
517
518
519
520
521
unifyCVwithType cv [] type=:(TArrow1 atype) modules subst heaps
	= unifyTypes (toTV cv) TA_Multi type TA_Multi modules subst heaps
unifyCVwithType cv [] TArrow modules subst heaps
	= unifyTypes (toTV cv) TA_Multi TArrow TA_Multi modules subst heaps
unifyCVwithType cv type_args type modules subst heaps
522
523
	= (False, subst, heaps)

524
unifyCVApplicationwithCVApplication cv1 type_args1 cv2 type_args2 modules subst heaps
525
526
	# arity1 = length type_args1
	  arity2 = length type_args2
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
527
528
	  diff = arity1 - arity2
	| diff == 0
529
		# (succ, subst) = unify_cv_with_cv cv1 cv2 subst
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
530
		| succ
531
		    = unify type_args1 type_args2 modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
532
533
534
			= (False, subst, heaps)
	| diff < 0
		# diff = 0 - diff
535
		  (succ, subst, heaps) = unifyTypes (toTV cv1) TA_Multi (cv2 :@: take diff type_args2) TA_Multi modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
536
		| succ
537
		    = unify type_args1 (drop diff type_args2) modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
538
			= (False, subst, heaps)
539
		# (succ, subst, heaps) = unifyTypes (cv1 :@: take diff type_args1) TA_Multi (toTV cv2) TA_Multi modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
540
		| succ
541
		    = unify (drop diff type_args1) type_args2 modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
542
			= (False, subst, heaps)
543
	where
544
		unify_cv_with_cv (TempCV tv_number1) (TempCV tv_number2) subst
545
546
			| tv_number1 == tv_number2
				= (True, subst)
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
				= (True, {subst & [tv_number1] = TempV tv_number2})
		unify_cv_with_cv (TempCV tv_number1) (TempQCV tv_number2) subst
			| tv_number1 == tv_number2
				= (True, subst)
				= (True, {subst & [tv_number1] = TempQV tv_number2})
		unify_cv_with_cv (TempCV tv_number1) (TempQCDV tv_number2) subst
			| tv_number1 == tv_number2
				= (True, subst)
				= (True, {subst & [tv_number1] = TempQDV tv_number2})
		unify_cv_with_cv (TempQCV tv_number1) (TempCV tv_number2) subst
			| tv_number1 == tv_number2
				= (True, subst)
				= (True, {subst & [tv_number2] = TempQV tv_number1})
		unify_cv_with_cv (TempQCV tv_number1) (TempQCV tv_number2) subst
			| tv_number1 == tv_number2
				= (True, subst)
				= (False, subst)
		unify_cv_with_cv (TempQCV tv_number1) (TempQCDV tv_number2) subst
			| tv_number1 == tv_number2
				= (True, subst)
				= (False, subst)
		unify_cv_with_cv (TempQCDV tv_number1) (TempCV tv_number2) subst
			| tv_number1 == tv_number2
				= (True, subst)
				= (True, {subst & [tv_number2] = TempQDV tv_number1})
		unify_cv_with_cv (TempQCDV tv_number1) (TempQCV tv_number2) subst
			| tv_number1 == tv_number2
				= (True, subst)
				= (False, subst)
		unify_cv_with_cv (TempQCDV tv_number1) (TempQCDV tv_number2) subst
			| tv_number1 == tv_number2
				= (True, subst)
				= (False, subst)

toTV (TempCV temp_var_id) = TempV temp_var_id
toTV (TempQCV temp_var_id) = TempQV temp_var_id
toTV (TempQCDV temp_var_id) = TempQDV temp_var_id

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
585
586
587
588
589
590
instance fromInt TypeAttribute
where
	fromInt AttrUni		= TA_Unique
	fromInt AttrMulti	= TA_Multi
	fromInt av_number	= TA_TempVar av_number

591
class freshCopy a :: !a !*TypeHeaps -> (!a, !*TypeHeaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
592
593
594
595
596

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

597
freshCopyOfAttributeVar {av_ident,av_info_ptr} attr_var_heap
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
598
599
600
601
602
	# (av_info, attr_var_heap) = readPtr av_info_ptr attr_var_heap
	= case av_info of
		AVI_Attr attr
			-> (attr, attr_var_heap)
		_
603
			-> abort ("freshCopyOfAttributeVar (type,icl)" ---> (av_ident,av_info_ptr))
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
604

Sjaak Smetsers's avatar
Sjaak Smetsers committed
605

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
606
607
608
freshCopyOfTypeAttribute (TA_Var avar) attr_var_heap
	= freshCopyOfAttributeVar avar attr_var_heap
freshCopyOfTypeAttribute (TA_RootVar avar) attr_var_heap
609
	= freshCopyOfAttributeVar avar attr_var_heap
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
610
611
612
613
614
615
616
617
618
619
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

620
freshCopyOfTypeVariable {tv_ident,tv_info_ptr} type_heaps=:{th_vars}
621
622
	# (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
623
624

freshConsVariable {tv_info_ptr} type_var_heap
625
	# (tv_info, type_var_heap) = readPtr tv_info_ptr type_var_heap
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
626
627
	= (to_constructor_variable tv_info, type_var_heap)
	where
628
629
630
631
632
633
		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
634
635
636
				TempQDV temp_var_id
					-> TempQCDV temp_var_id
				TV var
637
					-> CV var
638
639
640
641
				_ 	
					-> 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
642
643

instance freshCopy AType
644
where
645
646
647
648
649
650
651
652
653
	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)
654
655
656
657
	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)
658

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
659
660
instance freshCopy Type
where
661
662
663
664
665
	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)
666
667
668
	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)
669
670
671
672
	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)
673
674
675
	freshCopy (TArrow1 arg_type) type_heaps
		# (arg_type, type_heaps) = freshCopy arg_type type_heaps
		= (TArrow1 arg_type, type_heaps)
676
	freshCopy (TFA vars type) type_heaps
677
		= freshCopyOfTFAType vars type type_heaps
678
679
	freshCopy type type_heaps
		= (type, type_heaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
680

681
freshCopyOfTFAType vars type type_heaps
682
	# (fresh_vars, type_heaps) = bind_TFA_vars_and_attrs vars type_heaps
683
	  (type, type_heaps) = freshCopy type type_heaps
684
	  type_heaps = clear_binding_of_TFA_vars_and_attrs fresh_vars type_heaps
685
	= (TFA fresh_vars type, type_heaps)
686
687
688

bind_TFA_vars_and_attrs vars type_heaps
	= foldSt bind_var_and_attr vars ([], type_heaps)
689
690
691
	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)
692
			= (fresh_vars, {type_heaps & th_vars = th_vars <:= (tv_info_ptr, TVI_Type (TV tv)), th_attrs = th_attrs})
693
694
695
696
697
698
699
700
701
702
703

		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)

704
705
706
clear_binding_of_TFA_vars_and_attrs fresh_vars type_heaps
	= foldSt clear_binding_of_var_and_attr fresh_vars type_heaps
	where
707
708
709
710
711
712
713
714
		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

715
716
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
717
where
718
719
720
721
722
723
	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 })

724
	fresh_existential_attribute (TA_Var {av_ident,av_info_ptr}) (exi_attr_vars, attr_store, attr_heap)
725
726
727
728
		= ([ attr_store : exi_attr_vars ], inc attr_store, attr_heap <:= (av_info_ptr, AVI_Attr (TA_TempVar attr_store)))
	fresh_existential_attribute attr state
		= state
	
729
fresh_type_variables :: [ATypeVar] *(*TypeVarHeap,Int) -> *(!*TypeVarHeap,!Int);
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
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

763
freshAlgebraicType :: !(Global Int) ![AlgebraicPattern] !{#CommonDefs} !*TypeState -> (![[AType]],!AType,![AttrCoercion],!TypeRhs,!*TypeState)
764
freshAlgebraicType {glob_module,glob_object} patterns common_defs ts=:{ts_var_store,ts_attr_store,ts_type_heaps,ts_exis_variables}
765
	# {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
766
767
	# (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)
768
769
770
	  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
771
	= (cons_types, alg_type, attr_env, td_rhs,
772
773
774
			{ 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 })
where
	fresh_symbol_types [{ap_symbol={glob_object},ap_expr}] cons_defs var_store attr_store type_heaps all_exis_variables
775
		# {cons_type = ct=:{st_args,st_attr_env,st_result}, cons_exi_vars} = cons_defs.[glob_object.ds_index]
776
777
778
779
780
781
782
783
784
		  (exis_variables, var_store, attr_store, type_heaps) = freshExistentialVariables cons_exi_vars var_store attr_store type_heaps
	  	  (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
785
		  {cons_type = ct=:{st_args,st_attr_env}, cons_exi_vars} = cons_defs.[glob_object.ds_index]
786
787
788
789
790
791
792
793
794
795
		  (exis_variables, var_store, attr_store, type_heaps) = freshExistentialVariables cons_exi_vars var_store attr_store type_heaps
		  (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
796

797
798
799
800
801
802
803
804
805
806
807
808
809
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
				[]
810
811
					# {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
812
813
814
815
816
817
818
					  {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"
819
	where
820
		make_cons_type_from_decons_type stdStrictLists_index decons_u_index common_defs ts
821
822
			# {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
823
			  {tst_args,tst_lifted,tst_result,tst_context,tst_attr_env}=fun_type_copy
824
			# result_type = case tst_args of [t] -> t
825
826
827
			# argument_types = case tst_result.at_type of
									TA _ args=:[arg1,arg2] -> args
									TAS _ args=:[arg1,arg2] _ -> args
828
829
830
831
832
833
834
835
836
837
838
839
840
			= (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

841
freshSymbolType :: !(Optional CoercionPosition) !Bool !SymbolType {#u:CommonDefs} !*TypeState -> (!TempSymbolType,!*TypeState)
842
freshSymbolType is_appl fresh_context_vars {st_vars,st_args,st_result,st_context,st_attr_vars,st_attr_env,st_arity} common_defs
843
				ts=:{ts_var_store,ts_attr_store,ts_type_heaps,ts_var_heap,ts_cons_variables,ts_exis_variables}
844
	# (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
845
	  (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
846
	  (attr_env, th_attrs)		= freshEnvironment st_attr_env th_attrs 
847
848
849
	  type_heaps 				= {ts_type_heaps & th_vars = th_vars, th_attrs = th_attrs}
	  (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
850
	  (tst_result, type_heaps)	= freshCopy st_result type_heaps
851
	  (tst_context, (type_heaps, ts_var_heap)) = freshTypeContexts fresh_context_vars st_context (type_heaps, ts_var_heap)
852
	  type_heaps = {type_heaps & th_attrs = clear_attributes st_attr_vars type_heaps.th_attrs}
853
854
855
856
857
	  cons_variables			= foldSt (collect_cons_variables_in_tc common_defs) tst_context []
	  tst = {tst_args=tst_args, tst_result=tst_result, tst_context=tst_context, tst_attr_env=attr_env,
			 tst_arity=st_arity, tst_lifted=0}
	= (tst, {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})
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
858
	where
859
		fresh_type_variables :: [TypeVar] !(!*TypeVarHeap, !Int) -> (!*TypeVarHeap, !Int)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
860
		fresh_type_variables type_variables state
861
862
863
864
865
866
			= 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
867
		fresh_attributes attributes state
868
869
870
871
872
			= 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
873
		clear_attributes :: [AttributeVar] !*AttrVarHeap -> *AttrVarHeap
874
875
876
877
878
879
		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)

880
		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
881
882
			# {class_cons_vars} = common_defs.[glob_module].com_class_defs.[ds_index]
			= collect_cons_variables tc_types class_cons_vars collected_cons_vars
883
884
885
		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
886
887
888
889
890
891
892
893
894
895
		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 tc_types (class_cons_vars >> 1) collected_cons_vars
896

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
897
898
899
900
901
902
		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]
903