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

3
import StdEnv,StdOverloadedList,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
124
125
126
127
128
129
130
131
132
	arraySubst tfac_type=:(TFAC vars type contexts) subst
		# (changed, new_type, subst) = arraySubst type subst
		| changed
			# (changed,new_contexts,subst) = arraySubst contexts subst
			| changed
				= (True, TFAC vars new_type new_contexts, subst)
				= (True, TFAC vars new_type contexts, subst)
			# (changed,new_contexts,subst) = arraySubst contexts subst
			| changed
				= (True, TFAC vars type new_contexts, subst)
				= (False, tfac_type, subst)
133

134
	arraySubst type subst
135
		= (False, type, subst)
136

137
138
139
140
141
142
143
144
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
145
146
where
	arraySubst [] subst
147
148
149
		= (False, [], subst)
	arraySubst t=:[type : types ] subst
		# (changed, (type, types), subst) = arraySubst (type, types) subst
150
		| changed
151
152
			= (True, [type : types ], subst)
			= (False, t, subst)
153

154
155
156
instance arraySubst TempSymbolType
where
	arraySubst tst=:{tst_args,tst_result,tst_context} subst
157
		# (changed, (tst_args, (tst_result, tst_context)), subst) = arraySubst (tst_args, (tst_result, tst_context)) subst
158
		| changed
159
160
			= (True, {tst & tst_args = tst_args, tst_result = tst_result, tst_context = tst_context}, subst)
			= (False, tst, subst)
161
162
163
164

instance arraySubst TypeContext
where
	arraySubst tc=:{tc_types} subst
165
		# (changed, tc_types, subst) = arraySubst tc_types subst
166
167
168
169
		| changed
			= (True,{ tc & tc_types = tc_types}, subst)
			= (False, tc, subst)

170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
instance arraySubst (VarContexts TypeContext)
where
	arraySubst var_context=:(VarContext arg_n context arg_atype var_contexts) subst
		# (changed,new_context,subst) = arraySubst context subst
		| changed
			# (changed,new_arg_atype,subst) = arraySubst arg_atype subst
			| changed
				# (changed,new_var_contexts,subst) = arraySubst var_contexts subst
				| changed
					= (True,VarContext arg_n new_context new_arg_atype new_var_contexts,subst)
					= (True,VarContext arg_n new_context new_arg_atype var_contexts,subst)
				# (changed,new_var_contexts,subst) = arraySubst var_contexts subst
				| changed
					= (True,VarContext arg_n new_context arg_atype new_var_contexts,subst)
					= (True,VarContext arg_n new_context arg_atype var_contexts,subst)
			# (changed,new_arg_atype,subst) = arraySubst arg_atype subst
			| changed			
				# (changed,new_var_contexts,subst) = arraySubst var_contexts subst
				| changed
					= (True,VarContext arg_n context new_arg_atype new_var_contexts,subst)
					= (True,VarContext arg_n context new_arg_atype var_contexts,subst)
				# (changed,new_var_contexts,subst) = arraySubst var_contexts subst
				| changed
					= (True,VarContext arg_n context arg_atype new_var_contexts,subst)
					= (False,var_context,subst)
	arraySubst NoVarContexts subst
		= (False,NoVarContexts,subst)

198
instance arraySubst CaseType
199
where
200
201
	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
202
203
		| changed
			= (True,{ ct & ct_pattern_type = ct_pattern_type, ct_result_type = ct_result_type, ct_cons_types = ct_cons_types }, subst)
204
			= (False, ct, subst)
205

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

208
instance containsTypeVariable [a] | containsTypeVariable a
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
209
where
210
211
212
	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
213
214
		= False

215
instance containsTypeVariable AType
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
216
where
217
	containsTypeVariable var_id {at_type} subst = containsTypeVariable var_id at_type subst
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
218

219
instance containsTypeVariable Type
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
220
where
221
222
223
224
225
226
227
228
229
	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
230
231
	containsTypeVariable var_id (TAS cons_id cons_args _) subst
		= containsTypeVariable var_id cons_args subst
232
233
	containsTypeVariable var_id (type :@: types) subst
		= containsTypeVariable var_id type subst || containsTypeVariable var_id types subst
234
235
	containsTypeVariable var_id (TArrow1 arg_type) subst
		= containsTypeVariable var_id arg_type subst
236
	containsTypeVariable _ _ _
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
237
238
		= False

239
instance containsTypeVariable ConsVariable
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
240
where
241
242
243
244
245
246
	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
247
248
		= False

249
250
type_error =: "Type error"
type_error_format =: { form_properties = cNoProperties, form_attr_position = No }
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
251

252
cannotUnify t1 t2 position=:(CP_Expression expr) common_defs err=:{ea_loc=[ip:_]}
253
254
255
	= case tryToOptimizePosition expr of
		Yes (id_name, line)
			# err = pushErrorAdmin { ip & ip_ident.id_name = id_name, ip_line = line } err
256
257
			  err = errorHeading type_error err
			  err = popErrorAdmin err
258
259
260
261
			  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
262
		_
263
264
265
			-> cannot_unify t1 t2 position common_defs err
cannotUnify t1 t2 position common_defs err
	= cannot_unify t1 t2 position common_defs err
266

267
cannot_unify t1 t2 position common_defs err
268
269
270
271
	# (err=:{ea_file}) = errorHeading type_error err
	  ea_file = case position of
				CP_FunArg _ _
					-> ea_file <<< "\"" <<< position <<< "\""
272
				CP_SymbArgAndExpression {symb_kind=SK_Constructor {glob_module,glob_object},symb_ident} arg_n expression
273
274
					#! 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
275
276
277
278
						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
279
280
							-> ea_file <<< "\"" <<< "field " <<< field_name <<< " of " <<< record_name 
								<<< " : " <<< CP_Expression expression <<< "\""
281
282
						_
							-> ea_file <<< "\"" <<< position <<< "\""
283
				CP_SymbArgAndExpression _ _ _
284
					-> ea_file <<< "\"" <<< position <<< "\""
285
286
287
				CP_LiftedFunArg _ _
					-> ea_file <<< "\"" <<< position <<< "\""
  				CP_Expression _
288
	  				-> ea_file <<< " near " <<< position <<< " :"
289
290
	  			_
	  				-> ea_file
291
	  ea_file = ea_file <<< " cannot unify demanded type with offered type:\n"
292
293
294
	  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}
295
296
297
298
299
300
301
302
303
304
305
306
307

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

308
309
tryToOptimizePosition (Case {case_ident=Yes {id_name}})
	= optBeautifulizeIdent id_name
310
311
tryToOptimizePosition (App {app_symb={symb_ident}})
	= optBeautifulizeIdent symb_ident.id_name
312
313
314
tryToOptimizePosition (fun @ _)
	= tryToOptimizePosition fun
tryToOptimizePosition _
Martin Wierich's avatar
Martin Wierich committed
315
	= No
316

317
318
319
isIndirection TE	= False
isIndirection type	= True

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

322
instance unify (a, b) | unify a & unify b
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
323
324
325
326
327
328
329
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)

330
instance unify [a] | unify a
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
331
332
333
334
335
336
337
338
339
340
341
342
343
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)
344
345
346
347
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
348
349
350
351
		= 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
352
353
			# (type2, subst) = subst![tv_number2]
			| isIndirection type2
354
				= unify_variable_with_type tv_number1 type2 attr subst modules heaps
355
			| tv_number1 == tv_number2
356
357
358
				= (True, subst, heaps)
				= (True, { subst & [tv_number1] = tv}, heaps)
		unify_variable_with_type tv_number type attr subst modules heaps
359
			| containsTypeVariable tv_number type subst
John van Groningen's avatar
John van Groningen committed
360
				# (succ, type, heaps) = tryToExpandInUnify type attr modules heaps
361
362
363
364
				| 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
365
366
367
368
369
370
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)
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
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
387
388
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
389
390
391
392
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
393
unifyTypes (cons_var :@: types) attr1 type2 attr2 modules subst heaps
John van Groningen's avatar
John van Groningen committed
394
	# (_, type2, heaps) = tryToExpandInUnify type2 attr2 modules heaps
395
	= unifyTypeApplications cons_var attr1 types type2 attr2 modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
396
unifyTypes type1 attr1 (cons_var :@: types) attr2 modules subst heaps
John van Groningen's avatar
John van Groningen committed
397
	# (_, type1, heaps) = tryToExpandInUnify type1 attr1 modules heaps
398
	= unifyTypeApplications cons_var attr2 types type1 attr1 modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
399
400
401
402
403
404
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)
405
406
407
408
409
410
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
411
unifyTypes type1 attr1 type2 attr2 modules subst heaps
John van Groningen's avatar
John van Groningen committed
412
413
	# (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
414
415
416
417
	| succ1 || succ2
		= unifyTypes type1 attr1 type2 attr2 modules subst heaps
		= (False, subst, heaps)

418
expandAndUnifyTypes t1 attr1 t2 attr2 modules subst heaps
John van Groningen's avatar
John van Groningen committed
419
420
	# (succ1, t1, heaps) = tryToExpandInUnify t1 attr1 modules heaps
	  (succ2, t2, heaps) = tryToExpandInUnify t2 attr2 modules heaps
421
422
423
424
	| succ1 || succ2
		= unifyTypes t1 attr1 t2 attr2 modules subst heaps
		= (False, subst, heaps)

John van Groningen's avatar
John van Groningen committed
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
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)

455
456
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
457
458
459
	#! type_def = ti_common_defs.[glob_module].com_type_defs.[glob_object]
	= case type_def.td_rhs of
		SynType {at_type}
460
			# (expanded_type, type_heaps) = substituteType type_def.td_attribute type_attr type_def.td_args type_args at_type type_heaps
461
			-> (True, expanded_type, type_heaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
462
463
		_
			-> (False, type, type_heaps)
464
465
466
467
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}
468
			# (expanded_type, type_heaps) = substituteType type_def.td_attribute type_attr type_def.td_args type_args at_type type_heaps
469
470
471
			-> (True, expanded_type, type_heaps)
		_
			-> (False, type, type_heaps)
472
tryToExpand type type_attr modules type_heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
473
474
	= (False, type, type_heaps)

475
476
477
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))
478
479
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)
480
481
482
483
484
485
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)
486
487
simplifyTypeApplication (TempQDV tv_number) type_args
	= (True, TempQCDV tv_number :@: type_args)
488
489
simplifyTypeApplication TArrow [type1, type2] 
	= (True, type1 --> type2)
Artem Alimarine's avatar
Artem Alimarine committed
490
491
simplifyTypeApplication TArrow [type] 
	= (True, TArrow1 type)
492
493
simplifyTypeApplication (TArrow1 type1) [type2] 
	= (True, type1 --> type2)
494
495
496
simplifyTypeApplication type type_args
	= (False, type)

497
unifyTypeApplications cv=:(TempCV tv_number) attr1 type_args type2 attr2 modules subst heaps
498
499
500
501
502
503
	# (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)
504
505
506
507
508
509
510
511
		= 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
512
513
514
515
516
		TempCV tv_number2
			# (type2, subst) = subst![tv_number2]
			| isIndirection type2
				# (ok, simplified_type) = simplifyTypeApplication type2 type_args2
				| ok
517
					-> unifyCVwithType cv1 type_args1 simplified_type modules subst heaps
518
					-> (False, subst, heaps)
519
				-> unifyCVApplicationwithCVApplication cv1 type_args1 cv2 type_args2 modules subst heaps
520
		TempQCV tv_number2
521
522
523
524
			-> 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
525
526
527
528
	# diff = type_cons.type_arity - length type_args
	| diff >= 0 
		# (succ, subst, heaps) = unify type_args (drop diff cons_args) modules subst heaps
		| succ
529
			= 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
530
531
		    = (False, subst, heaps)
		= (False, subst, heaps)
532
unifyCVwithType cv type_args type=:(TAS type_cons cons_args strictness) modules subst heaps
533
534
535
536
	# diff = type_cons.type_arity - length type_args
	| diff >= 0 
		# (succ, subst, heaps) = unify type_args (drop diff cons_args) modules subst heaps
		| succ
537
			= unifyTypes (toTV cv) TA_Multi (TAS { type_cons & type_arity = diff } (take diff cons_args) strictness) TA_Multi modules subst heaps
538
539
		    = (False, subst, heaps)
		= (False, subst, heaps)
540
unifyCVwithType cv [type_arg1, type_arg2] type=:(atype1 --> atype2) modules subst heaps
541
542
	# (succ, subst, heaps) = unify (type_arg1, type_arg2) (atype1, atype2) modules subst heaps
	| succ
543
		= unifyTypes (toTV cv) TA_Multi TArrow TA_Multi modules subst heaps
544
		= (False, subst, heaps)		
545
unifyCVwithType cv [type_arg] type=:(atype1 --> atype2) modules subst heaps
546
547
	# (succ, subst, heaps) = unify type_arg atype2 modules subst heaps
	| succ
548
		= unifyTypes (toTV cv) TA_Multi (TArrow1 atype1) TA_Multi modules subst heaps
549
		= (False, subst, heaps)
550
551
552
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
553
554
	# (succ, subst, heaps) = unify type_arg atype modules subst heaps
	| succ
555
		= unifyTypes (toTV cv) TA_Multi TArrow TA_Multi modules subst heaps
Artem Alimarine's avatar
Artem Alimarine committed
556
		= (False, subst, heaps)
557
558
559
560
561
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
562
563
	= (False, subst, heaps)

564
unifyCVApplicationwithCVApplication cv1 type_args1 cv2 type_args2 modules subst heaps
565
566
	# arity1 = length type_args1
	  arity2 = length type_args2
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
567
568
	  diff = arity1 - arity2
	| diff == 0
569
		# (succ, subst) = unify_cv_with_cv cv1 cv2 subst
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
570
		| succ
571
		    = unify type_args1 type_args2 modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
572
573
574
			= (False, subst, heaps)
	| diff < 0
		# diff = 0 - diff
575
		  (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
576
		| succ
577
		    = unify type_args1 (drop diff type_args2) modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
578
			= (False, subst, heaps)
579
		# (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
580
		| succ
581
		    = unify (drop diff type_args1) type_args2 modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
582
			= (False, subst, heaps)
583
	where
584
		unify_cv_with_cv (TempCV tv_number1) (TempCV tv_number2) subst
585
586
			| tv_number1 == tv_number2
				= (True, subst)
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
				= (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
625
626
627
628
629
630
instance fromInt TypeAttribute
where
	fromInt AttrUni		= TA_Unique
	fromInt AttrMulti	= TA_Multi
	fromInt av_number	= TA_TempVar av_number

631
class freshCopy a :: !a !*TypeHeaps -> (!a, !*TypeHeaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
632
633
634
635
636

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

637
freshCopyOfAttributeVar {av_ident,av_info_ptr} attr_var_heap
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
638
639
640
641
642
	# (av_info, attr_var_heap) = readPtr av_info_ptr attr_var_heap
	= case av_info of
		AVI_Attr attr
			-> (attr, attr_var_heap)
		_
643
			-> abort ("freshCopyOfAttributeVar (type,icl)" ---> (av_ident,av_info_ptr))
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
644

Sjaak Smetsers's avatar
Sjaak Smetsers committed
645

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
646
647
648
freshCopyOfTypeAttribute (TA_Var avar) attr_var_heap
	= freshCopyOfAttributeVar avar attr_var_heap
freshCopyOfTypeAttribute (TA_RootVar avar) attr_var_heap
649
	= freshCopyOfAttributeVar avar attr_var_heap
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
650
651
652
653
654
655
656
657
658
659
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

660
freshCopyOfTypeVariable {tv_ident,tv_info_ptr} type_heaps=:{th_vars}
661
662
	# (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
663
664

freshConsVariable {tv_info_ptr} type_var_heap
665
	# (tv_info, type_var_heap) = readPtr tv_info_ptr type_var_heap
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
666
667
	= (to_constructor_variable tv_info, type_var_heap)
	where
668
669
670
671
672
673
		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
674
675
676
				TempQDV temp_var_id
					-> TempQCDV temp_var_id
				TV var
677
					-> CV var
678
679
680
681
				_ 	
					-> 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
682
683

instance freshCopy AType
684
where
685
686
687
688
	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)
689

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
690
691
instance freshCopy Type
where
692
693
694
695
696
	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)
697
698
699
	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)
700
701
702
703
	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)
704
705
706
707
708
709
710
	freshCopy (CV tv :@: types) type_heaps
		# (fresh_types, type_heaps) = freshCopy types type_heaps
		# (fresh_cons_var, th_vars)	= freshConsVariable tv type_heaps.th_vars
		= (fresh_cons_var :@: fresh_types, {type_heaps & th_vars = th_vars})
	freshCopy (cv :@: types) type_heaps
		# (fresh_types, type_heaps) = freshCopy types type_heaps
		= (cv :@: fresh_types, type_heaps)
711
712
713
	freshCopy (TArrow1 arg_type) type_heaps
		# (arg_type, type_heaps) = freshCopy arg_type type_heaps
		= (TArrow1 arg_type, type_heaps)
714
	freshCopy (TFA vars type) type_heaps
715
		= freshCopyOfTFAType vars type type_heaps
716
717
	freshCopy (TFAC vars type context) type_heaps
		= freshCopyOfTFACType vars type context type_heaps
718
719
	freshCopy type type_heaps
		= (type, type_heaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
720

721
freshCopyOfTFAType vars type type_heaps
722
	# (fresh_vars, type_heaps) = bind_TFA_vars_and_attrs vars type_heaps
723
	  (type, type_heaps) = freshCopy type type_heaps
724
	  type_heaps = clear_binding_of_TFA_vars_and_attrs fresh_vars type_heaps
725
	= (TFA fresh_vars type, type_heaps)
726

727
728
729
730
731
732
733
freshCopyOfTFACType vars type contexts type_heaps
	# (fresh_vars, type_heaps) = bind_TFA_vars_and_attrs vars type_heaps
	  (type, type_heaps) = freshCopy type type_heaps
	  (contexts, type_heaps) = freshTypeContexts_no_fresh_context_vars contexts type_heaps
	  type_heaps = clear_binding_of_TFA_vars_and_attrs fresh_vars type_heaps
	= (TFAC fresh_vars type contexts, type_heaps)

734
735
bind_TFA_vars_and_attrs vars type_heaps
	= foldSt bind_var_and_attr vars ([], type_heaps)
736
737
738
	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)
739
			= (fresh_vars, {type_heaps & th_vars = th_vars <:= (tv_info_ptr, TVI_Type (TV tv)), th_attrs = th_attrs})
740
741
742
743
744
745
746
747
748
749
750

		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)

751
752
753
clear_binding_of_TFA_vars_and_attrs fresh_vars type_heaps
	= foldSt clear_binding_of_var_and_attr fresh_vars type_heaps
	where
754
755
756
757
758
759
760
761
		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

762
763
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
764
where
765
766
767
768
769
770
	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 })

771
	fresh_existential_attribute (TA_Var {av_info_ptr}) (exi_attr_vars, attr_store, attr_heap)
772
773
774
775
		= ([ 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
	
776
fresh_type_variables :: [ATypeVar] *(*TypeVarHeap,Int) -> *(!*TypeVarHeap,!Int);
777
778
779
780
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

781
fresh_attributes :: [AttributeVar] *(*AttrVarHeap,Int) -> *(!*AttrVarHeap,!Int);
782
783
784
785
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

786
fresh_environment :: [AttrInequality] [AttrCoercion] *AttrVarHeap -> *(![AttrCoercion],!*AttrVarHeap);
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
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

810
811
freshAlgebraicType :: !GlobalIndex ![AlgebraicPattern] !{#CommonDefs} !*TypeState
					-> (![[AType]],!AType,![AttrCoercion],[(DefinedSymbol,[TypeContext])],!TypeRhs,!*TypeState)
812
813
freshAlgebraicType {gi_module,gi_index} patterns common_defs ts=:{ts_var_store,ts_attr_store,ts_type_heaps,ts_exis_variables}
	# {td_rhs,td_args,td_attrs}		= common_defs.[gi_module].com_type_defs.[gi_index]
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
814
815
	# (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)
816
	  ts_type_heaps					= { ts_type_heaps & th_vars = th_vars, th_attrs = th_attrs }
817
818
	  (cons_types, alg_type, attr_env, constructor_contexts, ts_var_store, ts_attr_store, ts_type_heaps, ts_exis_variables)
	  		= fresh_symbol_types patterns common_defs td_attrs td_args ts_var_store ts_attr_store ts_type_heaps ts_exis_variables
819
	= (cons_types, alg_type, attr_env, constructor_contexts, td_rhs,
820
821
			{ 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
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
	fresh_symbol_types [{ap_symbol={glob_object,glob_module},ap_expr}] common_defs td_attrs td_args var_store attr_store type_heaps all_exis_variables
		# {cons_type = {st_args,st_attr_env,st_result,st_context}, cons_exi_vars, cons_number, cons_type_index} = common_defs.[glob_module].com_cons_defs.[glob_object.ds_index]
		| cons_number <> -3
			# (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
			| isEmpty st_context
				= ([fresh_args], result_type, attr_env, [], var_store, attr_store, type_heaps, all_exis_variables)
				# (context, type_heaps) = freshTypeContexts_no_fresh_context_vars st_context type_heaps // fresh_context_vars are created later
				= ([fresh_args], result_type, attr_env, [(glob_object,context)], var_store, attr_store, type_heaps, all_exis_variables)
			# extension_type = common_defs.[glob_module].com_type_defs.[cons_type_index]
			  th_vars = copy_type_variables extension_type.td_args td_args type_heaps.th_vars
			  th_attrs = copy_attributes extension_type.td_attrs td_attrs type_heaps.th_attrs
			  type_heaps & th_vars = th_vars, th_attrs = th_attrs
			# (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
			| isEmpty st_context
				= ([fresh_args], result_type, attr_env, [], var_store, attr_store, type_heaps, all_exis_variables)
				# (context, type_heaps) = freshTypeContexts_no_fresh_context_vars st_context type_heaps // fresh_context_vars are created later
				= ([fresh_args], result_type, attr_env, [(glob_object,context)], var_store, attr_store, type_heaps, all_exis_variables)
	fresh_symbol_types [{ap_symbol={glob_object,glob_module},ap_expr} : patterns] common_defs td_attrs td_args var_store attr_store type_heaps all_exis_variables
		# (cons_types, result_type, attr_env, constructor_contexts, var_store, attr_store, type_heaps, all_exis_variables)
				= fresh_symbol_types patterns common_defs td_attrs td_args var_store attr_store type_heaps all_exis_variables
		# {cons_type = {st_args,st_attr_env,st_context}, cons_exi_vars,cons_number, cons_type_index} = common_defs.[glob_module].com_cons_defs.[glob_object.ds_index]
		| cons_number <> -3
			# (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
			| isEmpty st_context
				= ([fresh_args : cons_types], result_type, attr_env, constructor_contexts, var_store, attr_store, type_heaps, all_exis_variables)
			  	# (context, type_heaps) = freshTypeContexts_no_fresh_context_vars st_context type_heaps // fresh_context_vars are created later
				= ([fresh_args : cons_types], result_type, attr_env, [(glob_object,context):constructor_contexts], var_store, attr_store, type_heaps, all_exis_variables)
			# extension_type = common_defs.[glob_module].com_type_defs.[cons_type_index]
			  th_vars = copy_type_variables extension_type.td_args td_args type_heaps.th_vars
			  th_attrs = copy_attributes extension_type.td_attrs td_attrs type_heaps.th_attrs
			  type_heaps & th_vars = th_vars, th_attrs = th_attrs
			# (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
			| isEmpty st_context
				= ([fresh_args : cons_types], result_type, attr_env, constructor_contexts, var_store, attr_store, type_heaps, all_exis_variables)
			  	# (context, type_heaps) = freshTypeContexts_no_fresh_context_vars st_context type_heaps // fresh_context_vars are created later
				= ([fresh_args : cons_types], result_type, attr_env, [(glob_object,context):constructor_contexts], var_store, attr_store, type_heaps, all_exis_variables)
872
873
874
875
876

	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
877

878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
	copy_type_variables [dest_type_var:dest_type_vars] [source_type_var:source_type_vars] th_vars
		# (tv_info/*TVI_Type (TempV type_var_number)*/,th_vars) = readPtr source_type_var.atv_variable.tv_info_ptr th_vars
		# th_vars = writePtr dest_type_var.atv_variable.tv_info_ptr tv_info th_vars
		= copy_type_variables dest_type_vars source_type_vars th_vars
	copy_type_variables [] [] th_vars
		= th_vars

	copy_attributes [dest_attr:dest_attrs] [source_attr:source_attrs] th_attrs
		# (av_info/*AVI_Attr (TA_TempVar attr_number)*/,th_attrs) = readPtr source_attr.av_info_ptr th_attrs
		# th_attrs = writePtr dest_attr.av_info_ptr av_info th_attrs
		= copy_attributes dest_attrs source_attrs th_attrs
	copy_attributes [] [] th_attrs
		= th_attrs

create_fresh_context_vars [(cons_symbol,contexts):constructor_contexts] var_heap
	# (constructor_contexts,var_heap) = create_fresh_context_vars constructor_contexts var_heap
	# (contexts,var_heap) = mapSt fresh_type_context_var contexts var_heap
	= ([(cons_symbol,contexts):constructor_contexts],var_heap);
where
	fresh_type_context_var tc var_heap
		# (new_info_ptr, var_heap) = newPtr VI_Empty var_heap
		= ({tc & tc_var = new_info_ptr}, var_heap)
create_fresh_context_vars [] var_heap
	= ([],var_heap)

903
904
905
906
907
908
909
910
911
912
913
914
915
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
				[]
916
917
					# {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
918
919
920
921
922
923
924
					  {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"
925
	where
926
		make_cons_type_from_decons_type stdStrictLists_index decons_u_index common_defs ts
927
928
			# {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
929
			  {tst_args,tst_lifted,tst_result,tst_context,tst_attr_env}=fun_type_copy
930
			# result_type = case tst_args of [t] -> t
931
932
933
			# argument_types = case tst_result.at_type of
									TA _ args=:[arg1,arg2] -> args
									TAS _ args=:[arg1,arg2] _ -> args
934
935
936
937
938
939
940
941
942
943
944
945
946
			= (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