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

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

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

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

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

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

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

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

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

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

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

108 109 110 111 112
	arraySubst tfa_type=:(TFA vars type) subst
		# (changed, type, subst) = arraySubst type subst
		| changed
			= (changed, TFA vars type, subst)
			= (False, tfa_type, subst)
113

114
	arraySubst type subst
115
		= (False, type, subst)
116

117 118 119 120 121 122 123 124
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
125 126
where
	arraySubst [] subst
127 128 129
		= (False, [], subst)
	arraySubst t=:[type : types ] subst
		# (changed, (type, types), subst) = arraySubst (type, types) subst
130
		| changed
131 132
			= (True, [type : types ], subst)
			= (False, t, subst)
133 134 135 136
	
instance arraySubst TempSymbolType
where
	arraySubst tst=:{tst_args,tst_result,tst_context} subst
137
		# (changed, (tst_args, (tst_result, tst_context)), subst) = arraySubst (tst_args, (tst_result, tst_context)) subst
138
		| changed
139 140
			= (True, {tst & tst_args = tst_args, tst_result = tst_result, tst_context = tst_context}, subst)
			= (False, tst, subst)
141 142 143 144

instance arraySubst TypeContext
where
	arraySubst tc=:{tc_types} subst
145
		# (changed, tc_types, subst) = arraySubst tc_types subst
146 147 148 149
		| changed
			= (True,{ tc & tc_types = tc_types}, subst)
			= (False, tc, subst)

150
instance arraySubst CaseType
151
where
152 153
	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
154 155
		| changed
			= (True,{ ct & ct_pattern_type = ct_pattern_type, ct_result_type = ct_result_type, ct_cons_types = ct_cons_types }, subst)
156
			= (False, ct, subst)
157

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

160
instance containsTypeVariable [a] | containsTypeVariable a
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
161
where
162 163 164
	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
165 166
		= False

167
instance containsTypeVariable AType
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
168
where
169
	containsTypeVariable var_id {at_type} subst = containsTypeVariable var_id at_type subst
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
170

171
instance containsTypeVariable Type
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
172
where
173 174 175 176 177 178 179
	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
180 181 182 183
//AA..
	containsTypeVariable var_id (TArrow1 arg_type) subst
		= containsTypeVariable var_id arg_type subst
//..AA
184 185 186 187 188
	containsTypeVariable var_id (TA cons_id cons_args) subst
		= containsTypeVariable var_id cons_args subst
	containsTypeVariable var_id (type :@: types) subst
		= containsTypeVariable var_id type subst || containsTypeVariable var_id types subst
	containsTypeVariable _ _ _
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
189 190
		= False

191
instance containsTypeVariable ConsVariable
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
192
where
193 194 195 196 197 198
	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
199 200
		= False

201 202
type_error =: "Type error"
type_error_format =: { form_properties = cNoProperties, form_attr_position = No }
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
203

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

cannot_unify t1 t2 position err
	# (err=:{ea_file}) = errorHeading type_error err
	  ea_file = case position of
				CP_FunArg _ _
					-> ea_file <<< "\"" <<< position <<< "\""
				_
					-> ea_file
226 227 228 229
	  ea_file = ea_file <<< " cannot unify " <:: (type_error_format, t1, No) 
						<<< " with " <:: (type_error_format, t2, No)
//	  ea_file = ea_file <<< " cannot unify " <:: (type_error_format, t1, Yes initialTypeVarBeautifulizer) 
//						<<< " with " <:: (type_error_format, t2, Yes initialTypeVarBeautifulizer)
230 231 232 233 234 235 236
	  ea_file = case position of
	  			CP_FunArg _ _
	  				-> ea_file
  				_
	  				-> ea_file <<< " near " <<< position
	= { err & ea_file = ea_file <<< '\n' }

237 238 239 240 241 242 243 244 245 246 247 248 249

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

250 251 252 253 254 255 256
tryToOptimizePosition (Case {case_ident=Yes {id_name}})
	= optBeautifulizeIdent id_name
tryToOptimizePosition (App {app_symb={symb_name}})
	= optBeautifulizeIdent symb_name.id_name
tryToOptimizePosition (fun @ _)
	= tryToOptimizePosition fun
tryToOptimizePosition _
Martin Wierich's avatar
Martin Wierich committed
257
	= No
258

259 260 261
isIndirection TE	= False
isIndirection type	= True

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

264
instance unify (a, b) | unify a & unify b
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
265 266 267 268 269 270 271
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)

272
instance unify [a] | unify a
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
273 274 275 276 277 278 279 280 281 282 283 284 285
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)
286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302
unifyTypes tv=:(TempV tv_number) attr1 type2 attr2 modules subst heaps
	# (type1, subst) = subst![tv_number]
	| isIndirection type1
		= unifyTypes type1 attr1 type2 attr2 modules subst heaps
		# (succ, subst) = unify_variable_with_type tv_number type2 subst
		= (succ, subst, heaps)
	where	
		unify_variable_with_type tv_number1 tv=:(TempV tv_number2) subst
			# (type2, subst) = subst![tv_number2]
			| isIndirection type2
				= unify_variable_with_type tv_number type2 subst
			| tv_number1 == tv_number2
				= (True, subst)
				= (True, { subst & [tv_number1] = tv})
		unify_variable_with_type tv_number type subst
			| containsTypeVariable tv_number type subst
				= (False, subst)
303
//					---> "unify_variable_with_type"
304
				= (True, { subst & [tv_number] = type})
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
305 306 307 308 309 310 311 312
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)
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
313 314 315 316 317 318
//AA..	
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	
//..AA
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
319 320 321
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
322 323
		# (succ1, t1, heaps) = tryToExpand t1 attr1 modules.ti_common_defs heaps
		  (succ2, t2, heaps) = tryToExpand t2 attr2 modules.ti_common_defs heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
324 325 326
		| succ1 || succ2
			= unifyTypes t1 attr1 t2 attr2 modules subst heaps
			= (False, subst, heaps)
327
//				---> "unifyTypes1"
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
328
unifyTypes (cons_var :@: types) attr1 type2 attr2 modules subst heaps
329 330
	# (_, type2, heaps) = tryToExpand type2 attr2 modules.ti_common_defs heaps
	= unifyTypeApplications cons_var attr1 types type2 attr2 modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
331
unifyTypes type1 attr1 (cons_var :@: types) attr2 modules subst heaps
332 333
	# (_, type1, heaps) = tryToExpand type1 attr1 modules.ti_common_defs heaps
	= unifyTypeApplications cons_var attr2 types type1 attr1 modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
334 335 336 337 338 339 340
unifyTypes t1=:(TempQV qv_number1) attr1 t2=:(TempQV qv_number2) attr2 modules subst heaps
	= (qv_number1 == qv_number2, subst, heaps)
unifyTypes (TempQV qv_number) attr1 type attr2 modules subst heaps
	= (False, subst, heaps)
unifyTypes type attr1 (TempQV qv_number1) attr2 modules subst heaps
	= (False, subst, heaps)
unifyTypes type1 attr1 type2 attr2 modules subst heaps
341 342
	# (succ1, type1, heaps) = tryToExpand type1 attr1 modules.ti_common_defs heaps
	  (succ2, type2, heaps) = tryToExpand type2 attr2 modules.ti_common_defs heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
343 344 345 346
	| succ1 || succ2
		= unifyTypes type1 attr1 type2 attr2 modules subst heaps
		= (False, subst, heaps)

347 348
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
349 350 351
	#! type_def = ti_common_defs.[glob_module].com_type_defs.[glob_object]
	= case type_def.td_rhs of
		SynType {at_type}
352 353
			# (_, expanded_type, type_heaps) = substituteType type_def.td_attribute type_attr type_def.td_args type_args at_type type_heaps
			-> (True, expanded_type, type_heaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
354 355
		_
			-> (False, type, type_heaps)
356
tryToExpand type type_attr modules type_heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
357 358
	= (False, type, type_heaps)

359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377
toTV is_exist temp_var_id
	| is_exist
		= TempQV temp_var_id
		= TempV temp_var_id

toCV is_exist temp_var_id
	| is_exist
		= TempQCV temp_var_id
		= TempCV temp_var_id

simplifyTypeApplication :: !Type ![AType] -> (!Bool, !Type)
simplifyTypeApplication (TA type_cons=:{type_arity} cons_args) type_args
	= (True, TA { type_cons & type_arity = type_arity + length type_args } (cons_args ++ type_args))
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)
378 379 380
//AA..
simplifyTypeApplication TArrow [type1, type2] 
	= (True, type1 --> type2)
Artem Alimarine's avatar
Artem Alimarine committed
381 382
simplifyTypeApplication TArrow [type] 
	= (True, TArrow1 type)
383 384 385
simplifyTypeApplication (TArrow1 type1) [type2] 
	= (True, type1 --> type2)
//..AA
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
simplifyTypeApplication type type_args
	= (False, type)

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

unifyCVwithType is_exist tv_number type_args type=:(TA type_cons cons_args) modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
414 415 416 417
	# diff = type_cons.type_arity - length type_args
	| diff >= 0 
		# (succ, subst, heaps) = unify type_args (drop diff cons_args) modules subst heaps
		| succ
418
			= unifyTypes (toTV is_exist tv_number) TA_Multi (TA { type_cons & type_arity = diff } (take diff cons_args)) TA_Multi modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
419 420
		    = (False, subst, heaps)
		= (False, subst, heaps)
421

Artem Alimarine's avatar
Artem Alimarine committed
422
// AA..
423 424 425 426 427 428 429 430 431 432
unifyCVwithType is_exist tv_number [type_arg1, type_arg2] type=:(atype1 --> atype2) modules subst heaps
	# (succ, subst, heaps) = unify (type_arg1, type_arg2) (atype1, atype2) modules subst heaps
	| succ
		= unifyTypes (toTV is_exist tv_number) TA_Multi TArrow TA_Multi modules subst heaps
		= (False, subst, heaps)		
unifyCVwithType is_exist tv_number [type_arg] type=:(atype1 --> atype2) modules subst heaps
	# (succ, subst, heaps) = unify type_arg atype2 modules subst heaps
	| succ
		= unifyTypes (toTV is_exist tv_number) TA_Multi (TArrow1 atype1) TA_Multi modules subst heaps
		= (False, subst, heaps)
Artem Alimarine's avatar
Artem Alimarine committed
433 434 435 436 437 438 439 440 441 442 443 444 445
unifyCVwithType is_exist tv_number [] type=:(atype1 --> atype2) modules subst heaps
	= unifyTypes (toTV is_exist tv_number) TA_Multi type TA_Multi modules subst heaps
		
unifyCVwithType is_exist tv_number [type_arg] type=:(TArrow1 atype) modules subst heaps
	# (succ, subst, heaps) = unify type_arg atype modules subst heaps
	| succ
		= unifyTypes (toTV is_exist tv_number) TA_Multi TArrow TA_Multi modules subst heaps
		= (False, subst, heaps)
unifyCVwithType is_exist tv_number [] type=:(TArrow1 atype) modules subst heaps
	= unifyTypes (toTV is_exist tv_number) TA_Multi type TA_Multi modules subst heaps

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

448 449 450 451 452 453
unifyCVwithType is_exist tv_number type_args type modules subst heaps
	= (False, subst, heaps)

unifyCVApplicationwithCVApplication is_exist1 tv_number1 type_args1 is_exist2 tv_number2 type_args2 modules subst heaps
	# arity1 = length type_args1
	  arity2 = length type_args2
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
454 455
	  diff = arity1 - arity2
	| diff == 0
456
		# (succ, subst) = unify_cv_with_cv is_exist1 tv_number1 is_exist2 tv_number2 subst
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
457
		| succ
458
		    = unify type_args1 type_args2 modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
459 460 461
			= (False, subst, heaps)
	| diff < 0
		# diff = 0 - diff
462
		  (succ, subst, heaps) = unifyTypes (toTV is_exist1 tv_number1) TA_Multi (toCV is_exist2 tv_number2 :@: take diff type_args2) TA_Multi modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
463
		| succ
464
		    = unify type_args1 (drop diff type_args2) modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
465
			= (False, subst, heaps)
466
//	| otherwise
467
		# (succ, subst, heaps) = unifyTypes (toCV is_exist1 tv_number1 :@: take diff type_args1) TA_Multi (toTV is_exist2 tv_number2) TA_Multi modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
468
		| succ
469
		    = unify (drop diff type_args1) type_args2 modules subst heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
470
			= (False, subst, heaps)
471 472 473 474 475 476 477 478 479 480 481 482
	where
		unify_cv_with_cv is_exist1 tv_number1 is_exist2 tv_number2 subst
			| tv_number1 == tv_number2
				= (True, subst)
			| is_exist1
				| is_exist2
					= (False, subst)
					= (True, { subst & [tv_number2] = TempQV tv_number1})
				| is_exist2
					= (True, { subst & [tv_number1] = TempQV tv_number2})
					= (True, { subst & [tv_number1] = TempV tv_number2})
		
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
483 484 485 486 487 488 489
	
instance fromInt TypeAttribute
where
	fromInt AttrUni		= TA_Unique
	fromInt AttrMulti	= TA_Multi
	fromInt av_number	= TA_TempVar av_number

490
class freshCopy a :: !a !*TypeHeaps -> (!a, !*TypeHeaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
491 492 493 494 495 496 497 498 499 500 501

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

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

Sjaak Smetsers's avatar
Sjaak Smetsers committed
504

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
505 506 507
freshCopyOfTypeAttribute (TA_Var avar) attr_var_heap
	= freshCopyOfAttributeVar avar attr_var_heap
freshCopyOfTypeAttribute (TA_RootVar avar) attr_var_heap
508
	= freshCopyOfAttributeVar avar attr_var_heap
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
509 510 511 512 513 514 515 516 517 518
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

519 520 521
freshCopyOfTypeVariable {tv_name,tv_info_ptr} type_heaps=:{th_vars}
	# (TVI_Type fresh_var, th_vars)	= readPtr tv_info_ptr th_vars
	= (fresh_var, { type_heaps & th_vars = th_vars })
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
522 523

freshConsVariable {tv_info_ptr} type_var_heap
524
	# (tv_info, type_var_heap) = readPtr tv_info_ptr type_var_heap
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
525 526 527 528 529 530 531 532 533
	= (to_constructor_variable tv_info, type_var_heap)
	where
		to_constructor_variable (TVI_Type (TempV temp_var_id))
			= TempCV temp_var_id
		to_constructor_variable (TVI_Type (TempQV temp_var_id))
			= TempQCV temp_var_id

instance freshCopy AType
where 	
534 535 536 537 538 539 540 541 542
	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)
543 544 545 546
	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)
547

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
548 549
instance freshCopy Type
where
550 551 552 553 554 555 556 557 558
	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)
	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)
559 560 561 562 563
//AA..
	freshCopy (TArrow1 arg_type) type_heaps
		# (arg_type, type_heaps) = freshCopy arg_type type_heaps
		= (TArrow1 arg_type, type_heaps)
//..AA		
564 565 566
	freshCopy (TFA vars type) type_heaps
		# type_heaps = foldSt bind_var_and_attr vars type_heaps
		  (type, type_heaps) = freshCopy type type_heaps
567
		# type_heaps = clearBindings vars type_heaps
568 569 570 571 572 573 574 575 576 577 578
		= (TFA vars type, type_heaps)
	where
		bind_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_Type (TV tv)), th_attrs = bind_attr atv_attribute th_attrs }
		where
			bind_attr var=:(TA_Var {av_info_ptr}) attr_heap
				= attr_heap <:= (av_info_ptr, AVI_Attr var)
			bind_attr attr attr_heap
				= attr_heap
	freshCopy type type_heaps
		= (type, type_heaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
579

580 581
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
582
where
583 584 585 586 587 588
	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 })

589
	fresh_existential_attribute (TA_Var {av_name,av_info_ptr}) (exi_attr_vars, attr_store, attr_heap)
590
		= ([ attr_store : exi_attr_vars ], inc attr_store, attr_heap <:= (av_info_ptr, AVI_Attr (TA_TempVar attr_store)))
591
//			---> ("fresh_existential_attribute", av_info_ptr,av_name)
592 593 594
	fresh_existential_attribute attr state
		= state
	
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 625 626 627 628 629
fresh_type_variables :: [ATypeVar] *(*Heap TypeVarInfo,Int) -> *(!*Heap TypeVarInfo,!Int);
fresh_type_variables type_variables state
	= foldSt (\{atv_variable={tv_info_ptr}} (var_heap, var_store) -> (var_heap <:= (tv_info_ptr, TVI_Type (TempV var_store)), inc var_store))
				type_variables state

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

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


630 631 632 633 634 635
freshUniversalVariables type_variables state
	= foldSt fresh_universal_variable type_variables state 
where
	fresh_universal_variable {atv_variable={tv_info_ptr}} (var_heap, var_store)
		= (var_heap <:= (tv_info_ptr, TVI_Type (TempQV var_store)), inc var_store)

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
636
freshAlgebraicType :: !(Global Int) ![AlgebraicPattern] !{#CommonDefs} !*TypeState -> (![[AType]],!AType,![AttrCoercion],!*TypeState)
637
freshAlgebraicType {glob_module, glob_object} patterns common_defs ts=:{ts_var_store,ts_attr_store,ts_type_heaps,ts_td_infos,ts_exis_variables}
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
638 639 640
	# {td_rhs,td_args,td_attrs,td_name,td_attribute} = common_defs.[glob_module].com_type_defs.[glob_object]
	# (th_vars, ts_var_store)		= fresh_type_variables td_args (ts_type_heaps.th_vars, ts_var_store)
	  (th_attrs, ts_attr_store)		= fresh_attributes td_attrs (ts_type_heaps.th_attrs, ts_attr_store)
641 642 643 644 645
	  ts_type_heaps					= { ts_type_heaps & th_vars = th_vars, th_attrs = th_attrs }
	  (cons_types, alg_type, attr_env, ts_var_store, ts_attr_store, ts_type_heaps, ts_exis_variables)
	  		= fresh_symbol_types patterns common_defs.[glob_module].com_cons_defs ts_var_store ts_attr_store ts_type_heaps ts_exis_variables
	= (cons_types, alg_type, attr_env,
			{ ts & ts_var_store = ts_var_store, ts_attr_store = ts_attr_store, ts_type_heaps = ts_type_heaps, ts_exis_variables = ts_exis_variables })
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
646
//		---> ("freshAlgebraicType", alg_type, cons_types)
647 648
where
	fresh_symbol_types [{ap_symbol={glob_object},ap_expr}] cons_defs var_store attr_store type_heaps all_exis_variables
649
		# {cons_type = ct=:{st_args,st_attr_env,st_result}, cons_index, cons_exi_vars} = cons_defs.[glob_object.ds_index]
650
		  (exis_variables, var_store, attr_store, type_heaps) = freshExistentialVariables cons_exi_vars var_store attr_store type_heaps
651
//		  	-?-> (not (isEmpty cons_exi_vars), ("fresh_symbol_types", cons_exi_vars, ct))
652 653 654 655 656 657 658 659
	  	  (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
660
		  {cons_type = ct=:{st_args,st_attr_env}, cons_index, cons_exi_vars} = cons_defs.[glob_object.ds_index]
661
		  (exis_variables, var_store, attr_store, type_heaps) = freshExistentialVariables cons_exi_vars var_store attr_store type_heaps
662
//		  	-?-> (not (isEmpty cons_exi_vars), ("fresh_symbol_types", cons_exi_vars, ct))
663 664 665 666 667 668 669 670 671
		  (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
672

673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694
fresh_overloaded_list_type [{ap_symbol}:patterns] pd_cons_symbol pd_nil_symbol decons_u_index nil_u_index stdStrictLists_index pos functions common_defs ts
	| ap_symbol.glob_module==cPredefinedModuleIndex
		| ap_symbol.glob_object.ds_index==pd_cons_symbol-FirstConstructorPredefinedSymbolIndex
			# (argument_types,result_type,tst_context,tst_attr_env,ts) = make_cons_type_from_decons_type stdStrictLists_index decons_u_index common_defs ts
			= case patterns of
				[]
					-> ([argument_types],result_type,tst_context,tst_attr_env,ts)
				[pattern=:{ap_symbol}]
					| ap_symbol.glob_module==cPredefinedModuleIndex && ap_symbol.glob_object.ds_index==pd_nil_symbol-FirstConstructorPredefinedSymbolIndex
						-> ([argument_types,[]],result_type,tst_context,tst_attr_env,ts)
		| ap_symbol.glob_object.ds_index==pd_nil_symbol-FirstConstructorPredefinedSymbolIndex
			= case patterns of
				[]
					# {ft_type,ft_symb,ft_type_ptr,ft_specials} = functions.[stdStrictLists_index].[nil_u_index]
					# (fun_type_copy, ts) = determineSymbolTypeOfFunction pos ft_symb 0/*symb_arity*/ ft_type ft_type_ptr common_defs ts
					  {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"
695
	where
696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715
		make_cons_type_from_decons_type stdStrictLists_index decons_u_index common_defs ts
			# {me_symb,me_type,me_type_ptr} = common_defs.[stdStrictLists_index].com_member_defs.[decons_u_index]
			  (fun_type_copy,ts) = determineSymbolTypeOfFunction pos me_symb 1/*symb_arity*/ me_type me_type_ptr common_defs ts
			  {tst_args,tst_arity,tst_lifted,tst_result,tst_context,tst_attr_env}=fun_type_copy						  
			# result_type = case tst_args of [t] -> t
			# argument_types = case tst_result.at_type of (TA _ args=:[arg1,arg2]) ->args
			= (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

freshSymbolType :: !(Optional CoercionPosition) !Bool !SymbolType {#u:CommonDefs} !*TypeState -> (!TempSymbolType,!*TypeState)
716 717
freshSymbolType is_appl fresh_context_vars st=:{st_vars,st_args,st_result,st_context,st_attr_vars,st_attr_env,st_arity} common_defs
				ts=:{ts_var_store,ts_attr_store,ts_type_heaps,ts_td_infos,ts_var_heap,ts_cons_variables,ts_exis_variables}
718
	# (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
719
	  (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
720
	  (attr_env, th_attrs)		= freshEnvironment st_attr_env th_attrs 
721
	  type_heaps 				= { ts_type_heaps & th_vars = th_vars, th_attrs = th_attrs }
722 723 724
	  (tst_args, (ts_var_store, ts_attr_store, ts_exis_variables, type_heaps))
	  							= fresh_arg_types is_appl st_args (ts_var_store, ts_attr_store, ts_exis_variables, type_heaps)
	  (tst_result, type_heaps)	= freshCopy st_result type_heaps
725
	  (tst_context, (type_heaps, ts_var_heap)) 	= freshTypeContexts fresh_context_vars st_context (type_heaps, ts_var_heap)
726 727 728 729
	  cons_variables			= foldSt (collect_cons_variables_in_tc common_defs) tst_context [] 
	= ({ tst_args = tst_args, tst_result = tst_result, tst_context = tst_context, tst_attr_env = attr_env, tst_arity = st_arity, tst_lifted = 0 },
	   { ts & ts_var_store = ts_var_store, ts_attr_store = ts_attr_store, ts_type_heaps = type_heaps, ts_var_heap = ts_var_heap,
	   				ts_cons_variables = cons_variables ++ ts_cons_variables, ts_exis_variables = ts_exis_variables })
730
		//---> ("freshSymbolType", st, tst_args, tst_result, tst_context)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
731
	where
732
		fresh_type_variables :: .[TypeVar] *(*Heap TypeVarInfo,.Int) -> (!.Heap TypeVarInfo,!Int);
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
733 734 735
		fresh_type_variables type_variables state
			= foldr (\{tv_info_ptr} (var_heap, var_store) -> (writePtr tv_info_ptr (TVI_Type (TempV var_store)) var_heap, inc var_store))
							state type_variables
736 737

		fresh_attributes :: .[AttributeVar] *(*Heap AttrVarInfo,.Int) -> (!.Heap AttrVarInfo,!Int);
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
738 739 740
		fresh_attributes attributes state
			= foldr (\{av_info_ptr} (attr_heap, attr_store) -> (writePtr av_info_ptr (AVI_Attr (TA_TempVar attr_store)) attr_heap, inc attr_store))
							state attributes
741

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763
		collect_cons_variables_in_tc common_defs tc=:{tc_class={glob_module,glob_object={ds_index}}, tc_types} collected_cons_vars
			# {class_cons_vars} = common_defs.[glob_module].com_class_defs.[ds_index]
			= collect_cons_variables tc_types class_cons_vars collected_cons_vars
		
		collect_cons_variables [] class_cons_vars collected_cons_vars
			= collected_cons_vars
		collect_cons_variables [type : tc_types] class_cons_vars collected_cons_vars
			| class_cons_vars bitand 1 == 0
				= collect_cons_variables tc_types (class_cons_vars >> 1) collected_cons_vars
				= case type of
					TempV temp_var_id 
						-> collect_cons_variables tc_types (class_cons_vars >> 1) (add_variable temp_var_id collected_cons_vars)
//							---> ("collect_cons_variables", temp_var_id)
					_
						-> collect_cons_variables tc_types (class_cons_vars >> 1) collected_cons_vars
						
		add_variable new_var_id []
			= [new_var_id]
		add_variable new_var_id vars=:[var_id : var_ids]
			| new_var_id == var_id
				= vars
				= [var_id : add_variable new_var_id var_ids]
764 765 766 767 768 769 770 771 772 773 774 775 776 777
				
		fresh_arg_types No arg_types (var_store, attr_store, exis_variables, type_heaps)
			# (arg_types, type_heaps) = freshArgumentsOfSymbolType arg_types type_heaps
			= (arg_types, (var_store, attr_store, exis_variables, type_heaps))
		fresh_arg_types (Yes pos) arg_types (var_store, attr_store, exis_variables, type_heaps)
			= mapSt (fresh_arg_type pos) arg_types (var_store, attr_store, exis_variables, type_heaps)
		where
			fresh_arg_type pos at=:{at_attribute, at_type = TFA vars type} (var_store, attr_store, exis_variables, type_heaps)
				# (fresh_attribute, th_attrs)	= freshCopyOfTypeAttribute at_attribute type_heaps.th_attrs
				# (var_store, attr_store, new_exis_variables, type_heaps)
						= foldSt fresh_var_and_attr vars (var_store, attr_store, [], { type_heaps & th_attrs = th_attrs })
				  (fresh_type, type_heaps)				= freshCopy type type_heaps
				  type_heaps							= clearBindings vars type_heaps
				= ({ at &  at_attribute = fresh_attribute, at_type = fresh_type },
778
						(var_store, attr_store, addToExistentialVariables pos new_exis_variables exis_variables, type_heaps))
779 780 781 782 783 784 785 786 787 788 789 790 791
			fresh_arg_type _ at (var_store, attr_store, exis_variables, type_heaps)
				# (fresh_at, type_heaps) = freshCopy at type_heaps
				= (fresh_at, (var_store, attr_store, exis_variables, type_heaps))

			fresh_var_and_attr {atv_attribute, atv_variable = tv=:{tv_info_ptr}} (var_store, attr_store, exis_variables, type_heaps)
				# (attr_store, exis_variables, th_attrs) = fresh_attr atv_attribute (attr_store, exis_variables, type_heaps.th_attrs)
				= (inc var_store,  attr_store, exis_variables, { type_heaps & th_vars = type_heaps.th_vars <:= (tv_info_ptr, TVI_Type (TempQV var_store)), th_attrs = th_attrs })
			where
				fresh_attr var=:(TA_Var {av_info_ptr}) (attr_store, exis_variables, attr_heap)
					= (inc attr_store, [attr_store : exis_variables], attr_heap <:= (av_info_ptr, AVI_Attr (TA_TempVar attr_store)))
				fresh_attr attr state
					= state
			
792 793 794 795
addToExistentialVariables pos [] exis_variables
	= exis_variables
addToExistentialVariables pos new_exis_variables exis_variables
	= [(pos, new_exis_variables) : exis_variables]
796

797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815
freshArgumentsOfSymbolType :: ![AType] !*TypeHeaps -> (![AType], !*TypeHeaps)
freshArgumentsOfSymbolType atypes type_heaps = mapSt fresh_arg_type atypes type_heaps
where
	fresh_arg_type at=:{at_attribute, at_type = TFA vars type} type_heaps
		# (fresh_attribute, th_attrs)			= freshCopyOfTypeAttribute at_attribute type_heaps.th_attrs
		# type_heaps							= foldSt bind_var_and_attr vars { type_heaps & th_attrs = th_attrs }
		  (fresh_type, type_heaps)				= freshCopy type type_heaps
		  type_heaps							= clearBindings vars type_heaps
		= ({ at &  at_attribute = fresh_attribute, at_type = TFA vars fresh_type }, type_heaps)
	where
		bind_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_Type (TV tv)), th_attrs = bind_attr atv_attribute th_attrs }
		where
			bind_attr var=:(TA_Var {av_info_ptr}) attr_heap
				= attr_heap <:= (av_info_ptr, AVI_Attr var)
			bind_attr attr attr_heap
				= attr_heap
	fresh_arg_type at type_heaps
		= freshCopy at type_heaps
816 817
	
freshInequality :: AttrInequality *(Heap AttrVarInfo) -> (!AttrCoercion,!.Heap AttrVarInfo);
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
818 819 820 821 822 823 824 825 826 827 828 829 830 831
freshInequality {ai_demanded,ai_offered} attr_heap
	# (av_dem_info, attr_heap) = readPtr ai_demanded.av_info_ptr attr_heap
	  (av_off_info, attr_heap) = readPtr ai_offered.av_info_ptr attr_heap
	  (AVI_Attr (TA_TempVar dem_attr_var)) = av_dem_info
	  (AVI_Attr (TA_TempVar off_attr_var)) = av_off_info
	= ({ac_demanded = dem_attr_var, ac_offered = off_attr_var}, attr_heap) // <<- (av_dem_info,av_off_info)
	
freshEnvironment [ineq : ineqs] attr_heap
	# (fresh_ineq, attr_heap) = freshInequality ineq attr_heap
	  (fresh_env, attr_heap) = freshEnvironment ineqs attr_heap
	= ([fresh_ineq : fresh_env], attr_heap)
freshEnvironment [] attr_heap
	= ([], attr_heap)

Sjaak Smetsers's avatar
Sjaak Smetsers committed
832 833
freshTypeContexts fresh_context_vars tcs cs_and_var_heap
	= mapSt (fresh_type_context fresh_context_vars) tcs cs_and_var_heap
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
834
where	
835 836
	fresh_type_context fresh_context_vars tc=:{tc_types} (type_heaps, var_heap)
		# (tc_types, type_heaps) = mapSt fresh_context_type tc_types type_heaps
Sjaak Smetsers's avatar
Sjaak Smetsers committed
837 838
		| fresh_context_vars
			# (new_info_ptr, var_heap) = newPtr VI_Empty var_heap
839 840
			= ({ tc & tc_types = tc_types, tc_var = new_info_ptr }, (type_heaps, var_heap))
			= ({ tc & tc_types = tc_types}, (type_heaps, var_heap))
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
841

842 843 844 845 846 847
	fresh_context_type (CV tv :@: types) type_heaps=:{th_vars}
		# (fresh_cons_var, th_vars)		= freshConsVariable tv th_vars
		  (types, type_heaps) = freshCopy types { type_heaps & th_vars = th_vars }
		= (fresh_cons_var :@: types, type_heaps)
	fresh_context_type type type_heaps
		= freshCopy type type_heaps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868

freshAttributedVariable :: !u:TypeState -> (!AType, !u:TypeState)
freshAttributedVariable ts=:{ts_var_store,ts_attr_store}
	= ({ at_attribute = TA_TempVar ts_attr_store, at_annotation = AN_None, at_type = TempV ts_var_store },
	     {ts & ts_var_store = inc ts_var_store, ts_attr_store = inc ts_attr_store})

freshNonUniqueVariable :: !u:TypeState -> (!AType, !u:TypeState)
freshNonUniqueVariable ts=:{ts_var_store}
	= ({ at_attribute = TA_Multi, at_annotation = AN_None, at_type = TempV ts_var_store },
	     {ts & ts_var_store = inc ts_var_store})

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


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

872
attribute_error type_attr No
873
	= No // XXX abort ("sanity check nr 723 failed in module type"--->("type_attr", type_attr))
874
attribute_error type_attr (Yes err)
875
	# err = errorHeading "Type error" err
876
	= Yes { err & ea_file = err.ea_file <<< "* attribute expected instead of " <<< type_attr <<< '\n' }
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
877

878 879
addPropagationAttributesToAType :: {#CommonDefs} !AType !*PropState -> *(!AType,Int,!*PropState);
addPropagationAttributesToAType modules type=:{at_type = TA cons_id=:{type_index={glob_object,glob_module},type_name} cons_args, at_attribute} ps
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915
	# (cons_args, props, ps=:{prop_td_infos,prop_type_heaps,prop_attr_vars,prop_attr_env,prop_error})
			= add_propagation_attributes_to_atypes modules cons_args ps
	  (prop_class, th_vars, prop_td_infos) = propClassification glob_object glob_module props modules prop_type_heaps.th_vars prop_td_infos
	  (at_attribute, prop_class, th_attrs, prop_attr_vars, prop_attr_env, prop_error)
	  		= determine_attribute_of_cons modules at_attribute cons_args prop_class prop_type_heaps.th_attrs prop_attr_vars prop_attr_env prop_error
	= ({ type & at_type = TA cons_id cons_args, at_attribute = at_attribute }, prop_class,  { ps & prop_attr_vars = prop_attr_vars,
			prop_td_infos = prop_td_infos, prop_attr_env = prop_attr_env,
				prop_type_heaps = { prop_type_heaps & th_vars = th_vars, th_attrs = th_attrs}, prop_error = prop_error })
	where
		add_propagation_attributes_to_atypes modules [] ps
			= ([], [], ps) 
		add_propagation_attributes_to_atypes modules [atype : atypes] ps
			# (atype, prop_class, ps) = addPropagationAttributesToAType modules atype ps
			  (atypes, prop_classes, ps) = add_propagation_attributes_to_atypes modules atypes ps
			= ([atype : atypes], [prop_class : prop_classes], ps)
	
		determine_attribute_of_cons modules TA_Unique cons_args prop_class attr_var_heap attr_vars attr_env ps_error
			= (TA_Unique, prop_class >> length cons_args, attr_var_heap, attr_vars, attr_env, ps_error)
		determine_attribute_of_cons modules cons_attr cons_args prop_class attr_var_heap attr_vars attr_env ps_error
			# (cumm_attr, prop_attrs, prop_class) = determine_cummulative_attribute cons_args TA_Multi [] prop_class
			  (comb_attr, attr_var_heap, attr_vars, attr_env, ps_error)
			  		= combine_attributes cons_attr cumm_attr prop_attrs attr_var_heap attr_vars attr_env ps_error
			= (comb_attr, prop_class, attr_var_heap, attr_vars, attr_env, ps_error)
			  
		determine_cummulative_attribute [] cumm_attr attr_vars prop_class
			= (cumm_attr, attr_vars, prop_class)
		determine_cummulative_attribute [{at_attribute} : types ] cumm_attr attr_vars prop_class
			| prop_class bitand 1 == 0
				= determine_cummulative_attribute types cumm_attr attr_vars (prop_class >> 1)
				= case at_attribute of
					TA_Unique
						-> (TA_Unique, [],