type.icl

implementation module type

import StdEnv, compare_types
import syntax, typesupport, check, analtypes, overloading, unitype, refmark, predef, utilities, compare_constructor
import genericsupport

::	TypeInput =
	! {	ti_common_defs	:: !{# CommonDefs }
	,	ti_functions	:: !{# {# FunType }}
	,	ti_main_dcl_module_n :: !Int
	,	ti_expand_newtypes :: !Bool
	}

::	TypeState =
	{	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_generic_heap		:: !.GenericHeap
	,	ts_td_infos			:: !.TypeDefInfos
	,	ts_cons_variables	:: ![TempVarId]
	,	ts_exis_variables	:: ![(CoercionPosition, [TempAttrId])]
	,	ts_error			:: !.ErrorAdmin
	,	ts_fun_defs			:: !.{#FunDef}
	}

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

::	SharedAttribute = 
	{	sa_attr_nr	:: !Int
	,	sa_position	:: !Expression
	}

::	Requirements =
	{	req_overloaded_calls	:: ![ExprInfoPtr]
	,	req_type_coercions		:: ![TypeCoercion]
	,	req_type_coercion_groups:: ![TypeCoercionGroup]
	,	req_attr_coercions		:: ![AttrCoercion]
	,	req_case_and_let_exprs	:: ![ExprInfoPtr]
	}

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

instance toString BoundVar
where
	toString varid = varid.var_ident.id_name

class arraySubst type :: !type !u:{!Type} -> (!Bool,!type, !u:{! Type})

instance arraySubst AType
where
	arraySubst atype=:{at_type} subst
		# (changed, at_type, subst) = arraySubst at_type subst
		| changed
			= (True, { atype & at_type = at_type }, subst)
			= (False, atype, subst)
		
instance arraySubst Type
where
	arraySubst tv=:(TempV tv_number) subst
		# (type, subst) = subst![tv_number]
		= case type of
			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
		| changed
			= (changed, arg_type --> res_type, subst)
			= (False, type, subst)
	arraySubst type=:(TA cons_id cons_args) subst
		# (changed, cons_args, subst) = arraySubst cons_args subst
		| changed
			= (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)
			= (False,type, subst) 
	arraySubst tcv=:(TempCV tv_number :@: types) subst
		# (type, subst) = subst![tv_number]
		= case type of
			TE
				# (changed,types, subst) = arraySubst types subst
				| changed
					-> (True, TempCV tv_number :@: types, subst)
					-> (False, tcv, subst)
			_
				# (_, (type, types), subst) = arraySubst (type, types) subst
				  (ok, simplified_type) = simplifyTypeApplication type types
				| ok
					-> (True, simplified_type, subst)
					-> (False, tcv, subst)
	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)
	arraySubst type=:(TArrow1 arg_type) subst
		# (changed, arg_type, subst) = arraySubst arg_type subst
		| changed
			= (changed, TArrow1 arg_type, subst)
			= (False, type, subst)
	arraySubst tfa_type=:(TFA vars type) subst
		# (changed, type, subst) = arraySubst type subst
		| changed
			= (changed, TFA vars type, subst)
			= (False, tfa_type, subst)

	arraySubst type subst
		= (False, type, subst)

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
where
	arraySubst [] subst
		= (False, [], subst)
	arraySubst t=:[type : types ] subst
		# (changed, (type, types), subst) = arraySubst (type, types) subst
		| changed
			= (True, [type : types ], subst)
			= (False, t, subst)

instance arraySubst TempSymbolType
where
	arraySubst tst=:{tst_args,tst_result,tst_context} subst
		# (changed, (tst_args, (tst_result, tst_context)), subst) = arraySubst (tst_args, (tst_result, tst_context)) subst
		| changed
			= (True, {tst & tst_args = tst_args, tst_result = tst_result, tst_context = tst_context}, subst)
			= (False, tst, subst)

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

instance arraySubst CaseType
where
	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
		| changed
			= (True,{ ct & ct_pattern_type = ct_pattern_type, ct_result_type = ct_result_type, ct_cons_types = ct_cons_types }, subst)
			= (False, ct, subst)

class containsTypeVariable a :: !Int !a !{!Type} -> Bool

instance containsTypeVariable [a] | containsTypeVariable a
where
	containsTypeVariable var_id [elem:list] subst
		= containsTypeVariable var_id elem subst || containsTypeVariable var_id list subst
	containsTypeVariable var_id [] _
		= False

instance containsTypeVariable AType
where
	containsTypeVariable var_id {at_type} subst = containsTypeVariable var_id at_type subst

instance containsTypeVariable Type
where
	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
	containsTypeVariable var_id (TAS 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 var_id (TArrow1 arg_type) subst
		= containsTypeVariable var_id arg_type subst
	containsTypeVariable _ _ _
		= False

instance containsTypeVariable ConsVariable
where
	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 _ _
		= False

type_error =: "Type error"
type_error_format =: { form_properties = cNoProperties, form_attr_position = No }

cannotUnify t1 t2 position=:(CP_Expression expr) common_defs 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 = { 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
		_
			-> cannot_unify t1 t2 position common_defs err
cannotUnify t1 t2 position common_defs err
	= cannot_unify t1 t2 position common_defs err

cannot_unify t1 t2 position common_defs err
	# (err=:{ea_file}) = errorHeading type_error err
	  ea_file = case position of
				CP_FunArg _ _
					-> ea_file <<< "\"" <<< position <<< "\""
				CP_SymbArg {symb_kind=SK_Constructor {glob_module,glob_object},symb_ident} arg_n
					#! 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
						RecordType {rt_fields}
							# field_name = rt_fields.[arg_n-1].fs_ident.id_name
							  record_name = symb_ident.id_name
							  record_name = if (record_name.[0]=='_') (record_name % (1,size record_name-1)) record_name
							-> ea_file <<< "\"" <<< "field " <<< field_name <<< " of " <<< record_name <<< "\""
						_
							-> ea_file <<< "\"" <<< position <<< "\""
				CP_SymbArg _ _
					-> ea_file <<< "\"" <<< position <<< "\""
				CP_LiftedFunArg _ _
					-> ea_file <<< "\"" <<< position <<< "\""
  				CP_Expression _
	  				-> ea_file <<< " near " <<< position <<< " :"
	  			_
	  				-> ea_file
	  ea_file = ea_file <<< " cannot unify demanded type with offered type:\n"
	  ea_file = ea_file <<< " " <:: (type_error_format, t1, No) <<< "\n"
	  ea_file = ea_file <<< " " <:: (type_error_format, t2, No) <<< "\n"
	= { err & ea_file = ea_file}

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

tryToOptimizePosition (Case {case_ident=Yes {id_name}})
	= optBeautifulizeIdent id_name
tryToOptimizePosition (App {app_symb={symb_ident}})
	= optBeautifulizeIdent symb_ident.id_name
tryToOptimizePosition (fun @ _)
	= tryToOptimizePosition fun
tryToOptimizePosition _
	= No

isIndirection TE	= False
isIndirection type	= True

class unify a :: !a !a !TypeInput !*{! Type} !*TypeHeaps -> (!Bool, !*{! Type}, !*TypeHeaps)

instance unify (a, b) | unify a & unify b
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)

instance unify [a] | unify a
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)
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
		= 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
			# (type2, subst) = subst![tv_number2]
			| isIndirection type2
				= unify_variable_with_type tv_number1 type2 attr subst modules heaps
			| tv_number1 == tv_number2
				= (True, subst, heaps)
				= (True, { subst & [tv_number1] = tv}, heaps)
		unify_variable_with_type tv_number type attr subst modules heaps
			| containsTypeVariable tv_number type subst
				# (succ, type, heaps) = tryToExpandInUnify type attr modules heaps
				| succ
					= unify_variable_with_type tv_number type attr subst modules heaps
					= (False, subst, heaps)
				= (True, { subst & [tv_number] = type},heaps)
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 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
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
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	
unifyTypes (cons_var :@: types) attr1 type2 attr2 modules subst heaps
	# (_, type2, heaps) = tryToExpandInUnify type2 attr2 modules heaps
	= unifyTypeApplications cons_var attr1 types type2 attr2 modules subst heaps
unifyTypes type1 attr1 (cons_var :@: types) attr2 modules subst heaps
	# (_, type1, heaps) = tryToExpandInUnify type1 attr1 modules heaps
	= unifyTypeApplications cons_var attr2 types type1 attr1 modules subst heaps
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 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)
unifyTypes type1 attr1 type2 attr2 modules subst heaps
	# (succ1, type1, heaps) = tryToExpandInUnify type1 attr1 modules heaps
	  (succ2, type2, heaps) = tryToExpandInUnify type2 attr2 modules heaps
	| succ1 || succ2
		= unifyTypes type1 attr1 type2 attr2 modules subst heaps
		= (False, subst, heaps)

expandAndUnifyTypes t1 attr1 t2 attr2 modules subst heaps
	# (succ1, t1, heaps) = tryToExpandInUnify t1 attr1 modules heaps
	  (succ2, t2, heaps) = tryToExpandInUnify t2 attr2 modules heaps
	| succ1 || succ2
		= unifyTypes t1 attr1 t2 attr2 modules subst heaps
		= (False, subst, heaps)

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)

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
	#! type_def = ti_common_defs.[glob_module].com_type_defs.[glob_object]
	= case type_def.td_rhs of
		SynType {at_type}
			# (expanded_type, type_heaps) = substituteType type_def.td_attribute type_attr type_def.td_args type_args at_type type_heaps
			-> (True, expanded_type, type_heaps)
		_
			-> (False, type, type_heaps)
tryToExpand type=:(TAS {type_index={glob_object,glob_module}} type_args _) type_attr ti_common_defs type_heaps
	#! type_def = ti_common_defs.[glob_module].com_type_defs.[glob_object]
	= case type_def.td_rhs of
		SynType {at_type}
			# (expanded_type, type_heaps) = substituteType type_def.td_attribute type_attr type_def.td_args type_args at_type type_heaps
			-> (True, expanded_type, type_heaps)
		_
			-> (False, type, type_heaps)
tryToExpand type type_attr modules type_heaps
	= (False, type, type_heaps)

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 (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)
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)
simplifyTypeApplication (TempQDV tv_number) type_args
	= (True, TempQCDV tv_number :@: type_args)
simplifyTypeApplication TArrow [type1, type2] 
	= (True, type1 --> type2)
simplifyTypeApplication TArrow [type] 
	= (True, TArrow1 type)
simplifyTypeApplication (TArrow1 type1) [type2] 
	= (True, type1 --> type2)
simplifyTypeApplication type type_args
	= (False, type)

unifyTypeApplications cv=:(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 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
		TempCV tv_number2
			# (type2, subst) = subst![tv_number2]
			| isIndirection type2
				# (ok, simplified_type) = simplifyTypeApplication type2 type_args2
				| ok
					-> unifyCVwithType cv1 type_args1 simplified_type modules subst heaps
					-> (False, subst, heaps)
				-> unifyCVApplicationwithCVApplication cv1 type_args1 cv2 type_args2 modules subst heaps
		TempQCV tv_number2
			-> 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
	# diff = type_cons.type_arity - length type_args
	| diff >= 0 
		# (succ, subst, heaps) = unify type_args (drop diff cons_args) modules subst heaps
		| succ
			= unifyTypes (toTV cv) TA_Multi (TA { type_cons & type_arity = diff } (take diff cons_args)) TA_Multi modules subst heaps
		    = (False, subst, heaps)
		= (False, subst, heaps)
unifyCVwithType cv type_args type=:(TAS type_cons cons_args strictness) modules subst heaps
	# diff = type_cons.type_arity - length type_args
	| diff >= 0 
		# (succ, subst, heaps) = unify type_args (drop diff cons_args) modules subst heaps
		| succ
			= unifyTypes (toTV cv) TA_Multi (TAS { type_cons & type_arity = diff } (take diff cons_args) strictness) TA_Multi modules subst heaps
		    = (False, subst, heaps)
		= (False, subst, heaps)
unifyCVwithType cv [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 cv) TA_Multi TArrow TA_Multi modules subst heaps
		= (False, subst, heaps)		
unifyCVwithType cv [type_arg] type=:(atype1 --> atype2) modules subst heaps
	# (succ, subst, heaps) = unify type_arg atype2 modules subst heaps
	| succ
		= unifyTypes (toTV cv) TA_Multi (TArrow1 atype1) TA_Multi modules subst heaps
		= (False, subst, heaps)
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
	# (succ, subst, heaps) = unify type_arg atype modules subst heaps
	| succ
		= unifyTypes (toTV cv) TA_Multi TArrow TA_Multi modules subst heaps
		= (False, subst, heaps)
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
	= (False, subst, heaps)

unifyCVApplicationwithCVApplication cv1 type_args1 cv2 type_args2 modules subst heaps
	# arity1 = length type_args1
	  arity2 = length type_args2
	  diff = arity1 - arity2
	| diff == 0
		# (succ, subst) = unify_cv_with_cv cv1 cv2 subst
		| succ
		    = unify type_args1 type_args2 modules subst heaps
			= (False, subst, heaps)
	| diff < 0
		# diff = 0 - diff
		  (succ, subst, heaps) = unifyTypes (toTV cv1) TA_Multi (cv2 :@: take diff type_args2) TA_Multi modules subst heaps
		| succ
		    = unify type_args1 (drop diff type_args2) modules subst heaps
			= (False, subst, heaps)
		# (succ, subst, heaps) = unifyTypes (cv1 :@: take diff type_args1) TA_Multi (toTV cv2) TA_Multi modules subst heaps
		| succ
		    = unify (drop diff type_args1) type_args2 modules subst heaps
			= (False, subst, heaps)
	where
		unify_cv_with_cv (TempCV tv_number1) (TempCV tv_number2) subst
			| tv_number1 == tv_number2
				= (True, subst)
				= (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

instance fromInt TypeAttribute
where
	fromInt AttrUni		= TA_Unique
	fromInt AttrMulti	= TA_Multi
	fromInt av_number	= TA_TempVar av_number

class freshCopy a :: !a !*TypeHeaps -> (!a, !*TypeHeaps)

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

freshCopyOfAttributeVar {av_ident,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)
		_
			-> abort ("freshCopyOfAttributeVar (type,icl)" ---> (av_ident,av_info_ptr))


freshCopyOfTypeAttribute (TA_Var avar) attr_var_heap
	= freshCopyOfAttributeVar avar attr_var_heap
freshCopyOfTypeAttribute (TA_RootVar avar) attr_var_heap
	= freshCopyOfAttributeVar avar attr_var_heap
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

freshCopyOfTypeVariable {tv_ident,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 })

freshConsVariable {tv_info_ptr} type_var_heap
	# (tv_info, type_var_heap) = readPtr tv_info_ptr type_var_heap
	= (to_constructor_variable tv_info, type_var_heap)
	where
		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
				TempQDV temp_var_id
					-> TempQCDV temp_var_id
				TV var
					-> CV var
				_ 	
					-> abort "type.icl: to_constructor_variable, fresh_type\n" ---> fresh_type		
		to_constructor_variable tvi 
			= abort "type.icl: to_constructor_variable, tvi\n" ---> tvi

instance freshCopy AType
where
	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)
	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)

instance freshCopy Type
where
	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 (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)
	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)
	freshCopy (TArrow1 arg_type) type_heaps
		# (arg_type, type_heaps) = freshCopy arg_type type_heaps
		= (TArrow1 arg_type, type_heaps)
	freshCopy (TFA vars type) type_heaps
		= freshCopyOfTFAType vars type type_heaps
	freshCopy type type_heaps
		= (type, type_heaps)

freshCopyOfTFAType vars type type_heaps
	# (fresh_vars, type_heaps) = bind_TFA_vars_and_attrs vars type_heaps
	  (type, type_heaps) = freshCopy type type_heaps
	  type_heaps = clear_binding_of_TFA_vars_and_attrs fresh_vars type_heaps
	= (TFA fresh_vars type, type_heaps)

bind_TFA_vars_and_attrs vars type_heaps
	= foldSt bind_var_and_attr vars ([], type_heaps)
	where
		bind_var_and_attr atv=:{atv_attribute, atv_variable = tv=:{tv_info_ptr}} (fresh_vars, type_heaps=:{th_vars,th_attrs})
			# (fresh_vars, th_attrs) = bind_attr atv_attribute atv (fresh_vars, th_attrs)
			= (fresh_vars, {type_heaps & th_vars = th_vars <:= (tv_info_ptr, TVI_Type (TV tv)), th_attrs = th_attrs})

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

clear_binding_of_TFA_vars_and_attrs fresh_vars type_heaps
	= foldSt clear_binding_of_var_and_attr fresh_vars type_heaps
	where
		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

freshExistentialVariables type_variables var_store attr_store type_heaps
	= foldSt fresh_existential_variable type_variables ([], var_store, attr_store, type_heaps) 
where
	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 })

	fresh_existential_attribute (TA_Var {av_ident,av_info_ptr}) (exi_attr_vars, attr_store, attr_heap)
		= ([ 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
	
fresh_type_variables :: [ATypeVar] *(*TypeVarHeap,Int) -> *(!*TypeVarHeap,!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

freshAlgebraicType :: !(Global Int) ![AlgebraicPattern] !{#CommonDefs} !*TypeState -> (![[AType]],!AType,![AttrCoercion],!TypeRhs,!*TypeState)
freshAlgebraicType {glob_module,glob_object} patterns common_defs ts=:{ts_var_store,ts_attr_store,ts_type_heaps,ts_exis_variables}
	# {td_rhs,td_args,td_attrs,td_ident,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)
	  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, td_rhs,
			{ ts & ts_var_store = ts_var_store, ts_attr_store = ts_attr_store, ts_type_heaps = ts_type_heaps, ts_exis_variables = ts_exis_variables })
where
	fresh_symbol_types [{ap_symbol={glob_object},ap_expr}] cons_defs var_store attr_store type_heaps all_exis_variables
		# {cons_type = ct=:{st_args,st_attr_env,st_result}, cons_exi_vars} = cons_defs.[glob_object.ds_index]
		  (exis_variables, var_store, attr_store, type_heaps) = freshExistentialVariables cons_exi_vars var_store attr_store type_heaps
	  	  (attr_env, th_attrs) 		= fresh_environment st_attr_env [] type_heaps.th_attrs
	  	  (result_type, type_heaps)	= freshCopy st_result { type_heaps & th_attrs = th_attrs }
	  	  (fresh_args, type_heaps)	= freshCopy st_args type_heaps
	  	  all_exis_variables		= add_exis_variables ap_expr exis_variables all_exis_variables
		= ([fresh_args], result_type, attr_env, var_store, attr_store, type_heaps, all_exis_variables)
	fresh_symbol_types [{ap_symbol={glob_object},ap_expr} : patterns] cons_defs var_store attr_store type_heaps all_exis_variables
		# (cons_types, result_type, attr_env, var_store, attr_store, type_heaps, all_exis_variables)
				= fresh_symbol_types patterns cons_defs var_store attr_store type_heaps all_exis_variables
		  {cons_type = ct=:{st_args,st_attr_env}, cons_exi_vars} = cons_defs.[glob_object.ds_index]
		  (exis_variables, var_store, attr_store, type_heaps) = freshExistentialVariables cons_exi_vars var_store attr_store type_heaps
		  (attr_env, th_attrs) 		= fresh_environment st_attr_env attr_env type_heaps.th_attrs
	  	  (fresh_args, type_heaps) 	= freshCopy st_args { type_heaps & th_attrs = th_attrs }
	  	  all_exis_variables		= add_exis_variables ap_expr exis_variables all_exis_variables
		= ([fresh_args : cons_types], result_type, attr_env, var_store, attr_store, type_heaps, all_exis_variables)

	add_exis_variables expr [] exis_variables
		= exis_variables
	add_exis_variables expr new_exis_variables exis_variables
		= [(CP_Expression expr, new_exis_variables) : exis_variables]

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_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
					  {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"
	where
		make_cons_type_from_decons_type stdStrictLists_index decons_u_index common_defs ts
			# {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
			  {tst_args,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
									TAS _ 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)
freshSymbolType is_appl fresh_context_vars {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_var_heap,ts_cons_variables,ts_exis_variables}
	# (th_vars, ts_var_store)	= fresh_type_variables st_vars (ts_type_heaps.th_vars, ts_var_store)
	  (th_attrs, ts_attr_store)	= fresh_attributes st_attr_vars (ts_type_heaps.th_attrs, ts_attr_store)
	  (attr_env, th_attrs)		= freshEnvironment st_attr_env th_attrs 
	  type_heaps 				= {ts_type_heaps & th_vars = th_vars, th_attrs = th_attrs}
	  (tst_args, (ts_var_store,ts_attr_store,ts_exis_variables,type_heaps))
								= fresh_arg_types is_appl st_args ts_var_store ts_attr_store ts_exis_variables type_heaps
	  (tst_result, type_heaps)	= freshCopy st_result type_heaps
	  (tst_context, (type_heaps, ts_var_heap)) = freshTypeContexts fresh_context_vars st_context (type_heaps, ts_var_heap)
	  type_heaps = {type_heaps & th_attrs = clear_attributes st_attr_vars type_heaps.th_attrs}
	  cons_variables			= foldSt (collect_cons_variables_in_tc common_defs) tst_context []
	  tst = {tst_args=tst_args, tst_result=tst_result, tst_context=tst_context, tst_attr_env=attr_env,
			 tst_arity=st_arity, tst_lifted=0}
	= (tst, {ts & ts_var_store = ts_var_store, ts_attr_store = ts_attr_store, ts_type_heaps = type_heaps, ts_var_heap = ts_var_heap,
	   			  ts_cons_variables = cons_variables ++ ts_cons_variables, ts_exis_variables = ts_exis_variables})
	where
		fresh_type_variables :: [TypeVar] !(!*TypeVarHeap, !Int) -> (!*TypeVarHeap, !Int)
		fresh_type_variables type_variables state
			= foldSt fresh_type_variable type_variables state
		where
			fresh_type_variable {tv_info_ptr} (var_heap, var_store)
				= (var_heap <:= (tv_info_ptr, TVI_Type (TempV var_store)), inc var_store)
			
		fresh_attributes :: [AttributeVar] !(!*AttrVarHeap, !Int) -> (!*AttrVarHeap, !Int)
		fresh_attributes attributes state
			= foldSt fresh_attribute attributes state
		where
			fresh_attribute {av_info_ptr} (attr_heap, attr_store)
				= (attr_heap <:= (av_info_ptr, AVI_Attr (TA_TempVar attr_store)), inc attr_store)

		clear_attributes :: [AttributeVar] !*AttrVarHeap -> *AttrVarHeap
		clear_attributes attributes attr_heap
			= foldSt clear_attribute attributes attr_heap
		where
			clear_attribute {av_info_ptr} attr_heap
				= attr_heap <:= (av_info_ptr, AVI_Empty)

		collect_cons_variables_in_tc common_defs tc=:{tc_class=TCClass {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_in_tc common_defs tc=:{tc_class=TCGeneric {gtc_class}} collected_cons_vars
			= collect_cons_variables_in_tc common_defs {tc & tc_class=TCClass gtc_class} collected_cons_vars 
		 
		collect_cons_variables [] class_cons_vars collected_cons_vars
			= collected_cons_vars
		collect_cons_variables [type : tc_types] class_cons_vars collected_cons_vars
			| class_cons_vars bitand 1 == 0
				= collect_cons_variables tc_types (class_cons_vars >> 1) collected_cons_vars
				= case type of
					TempV temp_var_id 
						-> collect_cons_variables tc_types (class_cons_vars >> 1) (add_variable temp_var_id collected_cons_vars)
					_
						-> collect_cons_variables tc_types (class_cons_vars >> 1) collected_cons_vars

		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]