uniqueness unification for types of functions that are generated

during the transformation phase

frontend/analunitypes.icl

@@ -305,6 +305,11 @@ signClassOfType type _ _ _ _ scs
 propClassification :: !Index !Index ![PropClassification] !{# CommonDefs } !*TypeVarHeap !*TypeDefInfos
 	-> (!PropClassification, !*TypeVarHeap, !*TypeDefInfos)
 propClassification type_index module_index hio_props defs type_var_heap td_infos
+// MW3..
+	| type_index>=size td_infos.[module_index]
+		// must be a dictionary => doesn't propagate
+		= (0, type_var_heap, td_infos)
+// ..MW3
 	# {td_args, td_name} = defs.[module_index].com_type_defs.[type_index]
 	  (td_info, td_infos) = td_infos![module_index].[type_index]
 	= determinePropClassOfTypeDef type_index module_index td_args td_info hio_props defs type_var_heap td_infos
@@ -540,6 +545,3 @@ where
 propClassOfType _ _ _ pcs
 	= (NoPropClass, NoPropClass, pcs)
 
-instance == SignClassification
-where
-	== sc1 sc2 = sc1.sc_pos_vect == sc2.sc_pos_vect && sc1.sc_neg_vect == sc2.sc_neg_vect

frontend/frontend.icl

@@ -118,7 +118,7 @@ frontEndInterface upToPhase mod_ident search_paths dcl_modules functions_and_mac
 	| upToPhase == FrontEndPhaseCheck
 		=	frontSyntaxTree cached_functions_and_macros n_functions_and_macros_in_dcl_modules main_dcl_module_n predef_symbols hash_table files error io out icl_mod dcl_mods fun_defs components array_instances optional_dcl_icl_conversions global_fun_range heaps
 
-	# (ok, fun_defs, array_instances, type_code_instances, common_defs, imported_funs, heaps, predef_symbols, error,out)
+	# (ok, fun_defs, array_instances, type_code_instances, common_defs, imported_funs, type_def_infos, heaps, predef_symbols, error,out)
 		= typeProgram (components -*-> "Typing") main_dcl_module_n icl_functions icl_specials list_inferred_types icl_common [a\\a<-:icl_import] dcl_mods icl_used_module_numbers heaps predef_symbols error out
 
 	| not ok
@@ -145,7 +145,7 @@ frontEndInterface upToPhase mod_ident search_paths dcl_modules functions_and_mac
 		 = analyseGroups common_defs array_instances main_dcl_module_n (components -*-> "Analyse") fun_defs var_heap expression_heap
 
 	  (components, fun_defs, dcl_types, used_conses, var_heap, type_heaps, expression_heap)
-	  	= transformGroups cleanup_info main_dcl_module_n (components -*-> "Transform")  fun_defs acc_args common_defs imported_funs dcl_types used_conses_in_dynamics var_heap type_heaps expression_heap
+	  	= transformGroups cleanup_info main_dcl_module_n (components -*-> "Transform")  fun_defs acc_args common_defs imported_funs dcl_types used_conses_in_dynamics type_def_infos var_heap type_heaps expression_heap
 
 	| upToPhase == FrontEndPhaseTransformGroups
 		# heaps = {hp_var_heap=var_heap, hp_type_heaps=type_heaps, hp_expression_heap=expression_heap}

frontend/syntax.dcl

@@ -54,7 +54,6 @@ instance toString Ident
 				| STE_Imported !STE_Kind !Index
 				| STE_DclFunction
 				| STE_Module !(Module (CollectedDefinitions ClassInstance IndexRange))
-				| STE_OpenModule !Int !(Module (CollectedDefinitions ClassInstance IndexRange))
 				| STE_ClosedModule
 				| STE_Empty
 					/* for creating class dictionaries */
@@ -833,17 +832,15 @@ cNonRecursiveAppl	:== False
 					| TVI_CorrespondenceNumber !Int /* auxiliary used in module comparedefimp */
 					| TVI_AType !AType /* auxiliary used in module comparedefimp */
 					| TVI_Used /* to administer that this variable is encountered (in checkOpenTypes) */
-//					| TVI_Clean !Int /* to keep the unique number that has been assigned to this variable during 'clean_up' */
 					| TVI_TypeCode !TypeCodeExpression
-// MdM
 					| TVI_CPSLocalTypeVar !Int /* MdM - the index of the variable as generated by the theorem prover */
-// ... MdM
-
+					
 ::	TypeVarInfoPtr	:== Ptr TypeVarInfo
 ::	TypeVarHeap 	:== Heap TypeVarInfo
 
 ::	AttrVarInfo  	= AVI_Empty | AVI_Attr !TypeAttribute | AVI_Forward !TempAttrId 
 					| AVI_CorrespondenceNumber !Int /* auxiliary used in module comparedefimp */
+					| AVI_Used
 					| AVI_Count !Int /* auxiliary used in module typesupport */
 					
 ::	AttrVarInfoPtr	:== Ptr AttrVarInfo
@@ -866,9 +863,10 @@ cNonRecursiveAppl	:== False
 	}
 
 ::	TypeAttribute = TA_Unique | TA_Multi | TA_Var !AttributeVar | TA_RootVar AttributeVar | TA_TempVar !Int  | TA_TempExVar
-				  | TA_Anonymous | TA_None
-				  | TA_List !Int !TypeAttribute | TA_Locked !TypeAttribute
-
+					| TA_Anonymous | TA_None
+					| TA_List !Int !TypeAttribute | TA_Locked !TypeAttribute
+					| TA_MultiOfPropagatingConsVar // only filled in after type checking, semantically equal to TA_Multi
+							
 ::	AttributeVar =
 	{	av_name			:: !Ident
 	,	av_info_ptr		:: !AttrVarInfoPtr

frontend/syntax.icl

@@ -54,7 +54,6 @@ where toString {import_module} = toString import_module
 				| STE_Imported !STE_Kind !Index
 				| STE_DclFunction
 				| STE_Module !(Module (CollectedDefinitions ClassInstance IndexRange))
-				| STE_OpenModule !Int !(Module (CollectedDefinitions ClassInstance IndexRange))
 				| STE_ClosedModule
 				| STE_Empty 
 				| STE_DictType !CheckedTypeDef
@@ -425,8 +424,8 @@ cIsALocalVar	:== False
 
 ::	ConsClasses =
 	{	cc_size			::!Int
-	,	cc_args			::![ConsClass]	// the lists have the
-	,	cc_linear_bits	::![Bool]		// same length
+	,	cc_args			::![ConsClass]
+	,	cc_linear_bits	::![Bool]
 	}
 					
 ::	ConsClass	:== Int
@@ -778,15 +777,14 @@ cNotVarNumber :== -1
 					| TVI_AType !AType /* auxiliary used in module comparedefimp */
 					| TVI_Used /* to adminster that this variable is encountered (in checkOpenTypes) */
 					| TVI_TypeCode !TypeCodeExpression
-// MdM
 					| TVI_CPSLocalTypeVar !Int /* MdM - the index of the variable as generated by the theorem prover */
-// ... MdM
 
 ::	TypeVarInfoPtr	:== Ptr TypeVarInfo
 ::	TypeVarHeap 	:== Heap TypeVarInfo
 
 ::	AttrVarInfo  	= AVI_Empty | AVI_Attr !TypeAttribute | AVI_Forward !TempAttrId
 					| AVI_CorrespondenceNumber !Int /* auxiliary used in module comparedefimp */
+					| AVI_Used
 					| AVI_Count !Int /* auxiliary used in module typesupport */
 
 ::	AttrVarInfoPtr	:== Ptr AttrVarInfo
@@ -810,8 +808,9 @@ cNotVarNumber :== -1
 	}
 
 ::	TypeAttribute = TA_Unique | TA_Multi | TA_Var !AttributeVar | TA_RootVar AttributeVar | TA_TempVar !Int | TA_TempExVar
-				  | TA_Anonymous | TA_None
-				  | TA_List !Int !TypeAttribute | TA_Locked !TypeAttribute
+					| TA_Anonymous | TA_None
+					| TA_List !Int !TypeAttribute | TA_Locked !TypeAttribute
+					| TA_MultiOfPropagatingConsVar
 
 ::	AttributeVar =
 	{	av_name			:: !Ident
@@ -1219,6 +1218,8 @@ where
 		= ""
 	toString TA_Multi
 		= "o "
+	toString TA_MultiOfPropagatingConsVar
+		= "@@ "
 	toString (TA_List _ _)
 		= "??? "
 	toString TA_TempExVar
@@ -1344,8 +1345,7 @@ where
 
 instance <<< AlgebraicPattern
 where
-//	(<<<) file g = file <<< g.ap_symbol <<< g.ap_vars <<< " -> " <<< g.ap_expr
-	(<<<) file g = file <<< g.ap_symbol <<< g.ap_vars <<< " " <<< g.ap_position <<< "-> " <<< g.ap_expr
+	(<<<) file g = file <<< g.ap_symbol <<< g.ap_vars <<< " -> " <<< g.ap_expr
 
 instance <<< BasicPattern
 where
@@ -1585,10 +1585,8 @@ where
 	(<<<) file {fun_symb,fun_body=ParsedBody bodies} = file <<< fun_symb <<< '.' <<< ' ' <<< bodies 
 	(<<<) file {fun_symb,fun_body=CheckedBody {cb_args,cb_rhs},fun_info={fi_free_vars,fi_def_level,fi_calls}} = file <<< fun_symb <<< '.'
 			<<< "C " <<< cb_args <<< " = " <<< cb_rhs 
-//			<<< '.' <<< fi_def_level <<< ' ' <<< '[' <<< fi_free_vars <<< ']' <<< cb_args <<< " = " <<< cb_rhs 
-	(<<<) file {fun_symb,fun_body=TransformedBody {tb_args,tb_rhs},fun_info={fi_free_vars,fi_def_level,fi_calls}} = file <<< fun_symb <<< '.'
-			<<< "T "  <<< tb_args <<< '[' <<< fi_calls <<< ']' <<< " = " <<< tb_rhs 
-//			<<< '.' <<< fi_def_level <<< ' ' <<< '[' <<< fi_free_vars <<< ']' <<< tb_args <<< " = " <<< tb_rhs 
+	(<<<) file {fun_symb,fun_index,fun_body=TransformedBody {tb_args,tb_rhs},fun_info={fi_free_vars,fi_def_level,fi_calls}} = file <<< fun_symb <<< '@' <<< fun_index
+			<<< tb_args <<< " = " <<< tb_rhs 
 	(<<<) file {fun_symb,fun_body=BackendBody body,fun_type=Yes type} = file <<< type <<< '\n' <<< fun_symb <<< '.'
 			<<< body <<< '\n'
 	(<<<) file {fun_symb,fun_body=NoBody,fun_type=Yes type} = file <<< type <<< '\n' <<< fun_symb <<< '.'
@@ -1830,7 +1828,7 @@ where
 		show_expression file (Update expr1 selectors expr2)
 			= file <<< "update"
 		show_expression file (TupleSelect {ds_arity} elem_nr expr)
-			= file <<< "argument" <<< (elem_nr + 1) <<< " of " <<< ds_arity <<< "-tuple"
+			= file <<< "argument " <<< (elem_nr + 1) <<< " of " <<< ds_arity <<< "-tuple"
 		show_expression file (BasicExpr bv _)
 			= file <<< bv
 		show_expression file (MatchExpr _ _ expr)
@@ -1890,9 +1888,6 @@ where
 	(<<<) file
 		(STE_Module _)
 			= file <<< "STE_Module"
-	(<<<) file
-		(STE_OpenModule _ _)
-			= file <<< "STE_OpenModule"
 	(<<<) file
 		STE_ClosedModule
 			= file <<< "STE_ClosedModule"

frontend/trans.dcl

@@ -14,8 +14,8 @@ analyseGroups	:: !{# CommonDefs} !IndexRange !Int !*{! Group} !*{#FunDef} !*VarH
 				-> (!CleanupInfo, !*{! ConsClasses}, !*{! Group}, !*{#FunDef}, !*VarHeap, !*ExpressionHeap)
 
 transformGroups :: !CleanupInfo !Int !*{! Group} !*{#FunDef} !{!.ConsClasses} !{# CommonDefs}  !{# {# FunType} }
-		!*{#{# CheckedTypeDef}} !ImportedConstructors !*VarHeap !*TypeHeaps !*ExpressionHeap
-			-> (!*{! Group}, !*{#FunDef}, !*{#{# CheckedTypeDef}}, !ImportedConstructors, !*VarHeap, !*TypeHeaps, !*ExpressionHeap)
+					!*{#{# CheckedTypeDef}} !ImportedConstructors !*TypeDefInfos !*VarHeap !*TypeHeaps !*ExpressionHeap
+				-> (!*{! Group}, !*{#FunDef}, !*{#{# CheckedTypeDef}}, !ImportedConstructors, !*VarHeap, !*TypeHeaps, !*ExpressionHeap)
 
 partitionateFunctions :: !*{# FunDef} ![IndexRange] -> (!*{! Group}, !*{# FunDef})
 

frontend/type.dcl

@@ -4,4 +4,28 @@ import StdArray
 import syntax, check
 
 typeProgram ::!{! Group} !Int !*{# FunDef} !IndexRange !(Optional Bool) !CommonDefs ![Declaration] !{# DclModule} !NumberSet !*Heaps !*PredefinedSymbols !*File !*File
-	-> (!Bool, !*{# FunDef}, !IndexRange, {! GlobalTCType}, !{# CommonDefs}, !{# {# FunType} }, !*Heaps, !*PredefinedSymbols, !*File, !*File)
+	-> (!Bool, !*{# FunDef}, !IndexRange, {! GlobalTCType}, !{# CommonDefs}, !{# {# FunType} }, !.TypeDefInfos, !*Heaps, !*PredefinedSymbols, !*File, !*File)
+
+addPropagationAttributesToAType :: {#CommonDefs} !AType !*PropState -> *(!AType,Int,!*PropState);
+
+::	PropState =
+	{	prop_type_heaps	:: !.TypeHeaps
+	,	prop_td_infos	:: !.TypeDefInfos
+	,	prop_attr_vars	:: ![AttributeVar]
+	,	prop_attr_env	:: ![AttrInequality]
+	,	prop_error		:: !.Optional .ErrorAdmin
+	}
+
+class unify a :: !a !a !TypeInput !*{! Type} !*TypeHeaps -> (!Bool, !*{! Type}, !*TypeHeaps)
+
+instance unify AType
+
+::	TypeInput =
+	{	ti_common_defs	:: !{# CommonDefs }
+	,	ti_functions	:: !{# {# FunType }}
+	,	ti_main_dcl_module_n :: !Int
+	}
+
+class arraySubst type :: !type !u:{!Type} -> (!type, !u:{! Type})
+
+instance arraySubst AType

frontend/typesupport.dcl

@@ -44,6 +44,8 @@ expandTypeApplication :: ![ATypeVar] !TypeAttribute !Type ![AType] !TypeAttribut
 
 equivalent :: !SymbolType !TempSymbolType !Int !{# CommonDefs} !*AttributeEnv !*TypeHeaps -> (!Bool, !*AttributeEnv, !*TypeHeaps) 
 
+NewAttrVarId :: !Int -> Ident
+
 beautifulizeAttributes :: !SymbolType !*AttrVarHeap -> (!SymbolType, !.AttrVarHeap)
 
 ::	AttrCoercion =
@@ -68,15 +70,18 @@ updateExpressionTypes :: !SymbolType !SymbolType ![ExprInfoPtr] !*TypeHeaps !*Ex
 
 class substitute a :: !a !*TypeHeaps -> (!a, !*TypeHeaps)
 
-instance substitute AType, Type, TypeContext, AttrInequality, CaseType, [a] | substitute a
+instance substitute AType, Type, TypeContext, AttrInequality, CaseType, [a] | substitute a,
+			(a,b) | substitute a & substitute b
 
 instance <<< TempSymbolType
 
 removeInequality :: !Int !Int !*Coercions -> .Coercions
 flattenCoercionTree :: !u:CoercionTree -> (![Int], !u:CoercionTree)
+	// retrieve all numbers from a coercion tree
 assignNumbersToAttrVars :: !SymbolType !*AttrVarHeap -> (!Int, ![AttributeVar], !.AttrVarHeap)
+	// returns the number and a list of all attribute variables
 getImplicitAttrInequalities :: !SymbolType -> [AttrInequality]
-	// retrieve those inequalities  that are implied by propagation
+	// retrieve those inequalities that are implied by propagation
 emptyCoercions :: !Int -> .Coercions
 	// Int: nr of attribute variables
 addAttrEnvInequalities :: ![AttrInequality] !*Coercions !u:AttrVarHeap
@@ -85,6 +90,7 @@ addAttrEnvInequalities :: ![AttrInequality] !*Coercions !u:AttrVarHeap
 	// nr corresponds to the attribute variable
 optBeautifulizeIdent :: !String -> Optional (!String, !LineNr)
 	// convert something like "c;8;2" to Yes ("comprehension", 8)
+removeUnusedAttrVars :: !{!CoercionTree} ![Int] -> Coercions
 	
 //accCoercionTree :: !.(u:CoercionTree -> (.a,u:CoercionTree)) !Int !*{!u:CoercionTree} -> (!.a,!{!u:CoercionTree})
 accCoercionTree f i coercion_trees
@@ -103,3 +109,26 @@ appCoercionTree f i coercion_trees
 		# (coercion_tree, coercion_trees) = replace coercion_trees i CT_Empty
 		= snd (replace coercion_trees i (f coercion_tree))
 	
+class performOnTypeVars a :: !(TypeAttribute TypeVar .st -> .st) !a !.st -> .st
+// run through a type and do something on each type variable
+
+instance performOnTypeVars Type, AType, ConsVariable, [a] | performOnTypeVars a,
+		(a, b) | performOnTypeVars a & performOnTypeVars b
+
+getTypeVars :: !a !*TypeVarHeap -> (!.[TypeVar],!.TypeVarHeap) | performOnTypeVars a
+
+class performOnAttrVars a :: !(AttributeVar .st -> .st) !a !.st -> .st
+// run through a type and do something on each attribute variable
+
+getAttrVars :: !a !*AttrVarHeap -> (!.[AttributeVar],!.AttrVarHeap) | performOnAttrVars a
+
+instance performOnAttrVars Type, AType, [a] | performOnAttrVars a,
+		(a, b) | performOnAttrVars a & performOnAttrVars b
+
+initializeToTVI_Empty :: a !TypeVar !*TypeVarHeap -> .TypeVarHeap
+initializeToAVI_Empty :: !AttributeVar !*AttrVarHeap -> .AttrVarHeap
+
+appTypeVarHeap f type_heaps :== let th_vars = f type_heaps.th_vars in { type_heaps & th_vars = th_vars }
+accTypeVarHeap f type_heaps :== let (r, th_vars) = f type_heaps.th_vars in (r, { type_heaps & th_vars = th_vars })
+accAttrVarHeap f type_heaps :== let (r, th_attrs) = f type_heaps.th_attrs in (r, { type_heaps & th_attrs = th_attrs })
+	

frontend/typesupport.icl

@@ -493,20 +493,12 @@ where
 instance substitute TypeAttribute
 where
 	substitute (TA_Var {av_name, av_info_ptr}) heaps=:{th_attrs}
-/* 
-	This alternative's code can be replaced with the original again, when the fusion algorithm becomes able to
-    infer correct type attributes
-*/
 		#! av_info = sreadPtr av_info_ptr th_attrs
 		= case av_info of
 			AVI_Attr attr
 				-> (attr, heaps)
 			_
 				-> (TA_Multi, heaps)
-/* Sjaak ...				-> SwitchFusion
-						(TA_Multi, heaps)
-						(abort "compiler bug nr 7689 in module typesupport")
-... Sjaak */
 	substitute TA_None heaps
 		= (TA_Multi, heaps)
 	substitute attr heaps
@@ -540,7 +532,7 @@ substituteTypeVariable tv=:{tv_name,tv_info_ptr} heaps=:{th_vars}
 	  heaps = { heaps & th_vars = th_vars }
 	= case tv_info of
 		TVI_Type type
-			-> (type, heaps)
+				-> (type, heaps)
 		_
 			-> (TV tv, heaps)
 
@@ -548,16 +540,28 @@ instance substitute Type
 where
 	substitute (TV tv) heaps
 		= substituteTypeVariable tv heaps
-	substitute (arg_type --> res_type)  heaps
+	substitute (arg_type --> res_type) heaps
 		# ((arg_type, res_type), heaps) = substitute (arg_type, res_type) heaps
 		= (arg_type --> res_type, heaps)
-	substitute (TA cons_id cons_args)  heaps
+	substitute (TA cons_id cons_args) heaps
 		# (cons_args, heaps) = substitute cons_args heaps
 		= (TA cons_id cons_args,  heaps)
-	substitute (CV type_var :@: types)  heaps
+/* MW3 was
+	substitute (CV type_var :@: types) heaps
 		# (type, heaps) = substituteTypeVariable type_var heaps
 		  (types, heaps) = substitute types heaps
 		= (simplifyTypeApplication type types, heaps)
+*/
+	substitute (CV type_var :@: types) heaps=:{th_vars}
+		# (tv_info, th_vars) = readPtr type_var.tv_info_ptr th_vars
+		  heaps = { heaps & th_vars = th_vars }
+		  (types, heaps) = substitute types heaps
+		= case tv_info of
+			TVI_Type tv=:(TempV i)
+				-> (TempCV i :@: types, heaps)
+			_
+				# (type, heaps) = substituteTypeVariable type_var heaps
+				-> (simplifyTypeApplication type types, heaps)
 	substitute type heaps
 		= (type, heaps)
 
@@ -605,6 +609,7 @@ NewVarId var_store
 AttrVarIdTable :: {# String}
 AttrVarIdTable =: { "u", "v", "w", "x", "y", "z" }
 
+NewAttrVarId :: !Int -> Ident
 NewAttrVarId attr_var_store
 	| attr_var_store < size AttrVarIdTable
  		= newIdent AttrVarIdTable.[attr_var_store]
@@ -1295,41 +1300,34 @@ beautifulizeAttributes symbol_type th_attrs
 assignNumbersToAttrVars :: !SymbolType !*AttrVarHeap -> (!Int, ![AttributeVar], !.AttrVarHeap)
 assignNumbersToAttrVars {st_attr_vars, st_args, st_result, st_attr_env} th_attrs
 	# th_attrs
-			= foldSt initialise_to_AVI_Empty st_attr_vars th_attrs
-	  (next_number, numbered_vars_accu, th_attrs)
-	  		= foldSt assign_numbers_attr_ineq st_attr_env
-				(assign_numbers_atype st_result
-					(foldSt assign_numbers_atype st_args (0, [], th_attrs)))
-	= (next_number, reverse numbered_vars_accu, th_attrs)
+			= foldSt initializeToAVI_Empty st_attr_vars th_attrs
+	  (nr_of_attr_vars, attr_vars, th_attrs)
+	  		= performOnAttrVars assign_number_to_unencountered_attr_var (st_args, st_result)
+	  				(0, [], th_attrs)
+	| fst (foldSt hasnt_got_a_number st_attr_env (False, th_attrs))
+		= abort "sanity check nr 834 in module typesupport failed"
+ 	= (nr_of_attr_vars, attr_vars, th_attrs)
   where
-	assign_numbers_atype atype=:{at_attribute=TA_Var av=:{av_info_ptr}, at_type}
-						(next_number, numbered_vars_accu, th_attrs)
+	assign_number_to_unencountered_attr_var av=:{av_info_ptr} (next_number, attr_vars_accu, th_attrs)
 		# (avi, th_attrs) = readPtr av_info_ptr th_attrs
-		= assign_numbers_type at_type
-			(assign_number avi av (next_number, numbered_vars_accu, th_attrs))
-	assign_numbers_atype atype=:{at_type} assign_state
-		= assign_numbers_type at_type assign_state
-
-	assign_numbers_type (TA _ args) assign_state
-		= foldSt assign_numbers_atype args assign_state
-	assign_numbers_type (l --> r) assign_state
-		= assign_numbers_atype l (assign_numbers_atype r assign_state)
-	assign_numbers_type (_ :@: args) assign_state
-		= foldSt assign_numbers_atype args assign_state
-	assign_numbers_type _ assign_state
-		= assign_state
-
-	assign_numbers_attr_ineq {ai_offered, ai_demanded} (next_number, numbered_vars_accu, th_attrs)
-		# (avi_offered, th_attrs) = readPtr ai_offered.av_info_ptr th_attrs
-		  (avi_demanded, th_attrs) = readPtr ai_demanded.av_info_ptr th_attrs
-		= assign_number avi_offered ai_offered
-			(assign_number avi_demanded ai_demanded (next_number, numbered_vars_accu, th_attrs))
+		= case avi of
+			AVI_Empty
+				-> (next_number+1, [av:attr_vars_accu],
+					writePtr av_info_ptr (AVI_Attr (TA_TempVar next_number)) th_attrs)
+			_
+				-> (next_number, attr_vars_accu, th_attrs)
 	
-	assign_number AVI_Empty av=:{av_info_ptr} (next_number, numbered_vars_accu, th_attrs)
-		= (next_number+1, [av:numbered_vars_accu],
-			writePtr av_info_ptr (AVI_Attr (TA_TempVar next_number)) th_attrs)
-	assign_number _ _ assign_state
-		= assign_state
+	hasnt_got_a_number {ai_offered, ai_demanded} (or_of_all, th_attrs)
+		# hnn1 = has_no_number ai_offered th_attrs
+		  hnn2 = has_no_number ai_demanded th_attrs
+		= (hnn1 || hnn2 || or_of_all, th_attrs)
+		
+	has_no_number {av_info_ptr} th_attrs
+		= case sreadPtr av_info_ptr th_attrs of
+			AVI_Empty
+				-> True
+			_
+				-> False
 
 //accCoercionTree :: !.(u:CoercionTree -> (.a,u:CoercionTree)) !Int !*{!u:CoercionTree} -> (!.a,!{!u:CoercionTree})
 accCoercionTree f i coercion_trees
@@ -1351,12 +1349,12 @@ flattenCoercionTree :: !u:CoercionTree -> (![Int], !u:CoercionTree)
 flattenCoercionTree tree
 	= flatten_ct ([], tree)
   where
-	flatten_ct (accu, CT_Empty)
-		= (accu, CT_Empty)
 	flatten_ct (accu, CT_Node i left right)
 		# (accu, right) = flatten_ct (accu, right)
 		  (accu, left) = flatten_ct ([i:accu], left)
 		= (accu, CT_Node i left right)
+	flatten_ct (accu, _)
+		= (accu, CT_Empty)
 
 anonymizeAttrVars :: !SymbolType ![AttrInequality] !*AttrVarHeap -> (!SymbolType, !.AttrVarHeap)
 anonymizeAttrVars st=:{st_attr_vars, st_args, st_result, st_attr_env} implicit_inequalities th_attrs
@@ -1446,32 +1444,28 @@ anonymizeAttrVars st=:{st_attr_vars, st_args, st_result, st_attr_env} implicit_i
 			_
 				-> th_attrs
 				
-initialise_to_AVI_Empty {av_info_ptr} th_attrs
-	= writePtr av_info_ptr AVI_Empty th_attrs
-
 removeInequality :: !Int !Int !*Coercions -> .Coercions
 removeInequality offered demanded attr_env_coercions=:{coer_offered, coer_demanded}
 	# coer_offered = appCoercionTree (removeNode offered) demanded coer_offered
 	  coer_demanded = appCoercionTree (removeNode demanded) offered coer_demanded
 	= { attr_env_coercions & coer_demanded = coer_demanded, coer_offered = coer_offered }
-  where
-	removeNode :: !Int !*CoercionTree -> !.CoercionTree
-	removeNode i1 (CT_Node i2 left right)
-		| i1<i2
-			= CT_Node i2 (removeNode i1 left) right
-		| i1>i2
-			= CT_Node i2 left (removeNode i1 right)
-		= rightInsert left right
-	removeNode i1 CT_Empty
-		= CT_Empty
 
+removeNode :: !Int !*CoercionTree -> !.CoercionTree
+removeNode i1 (CT_Node i2 left right)
+	| i1<i2
+		= CT_Node i2 (removeNode i1 left) right
+	| i1>i2
+		= CT_Node i2 left (removeNode i1 right)
+	= rightInsert left right
+  where
 	rightInsert :: !*CoercionTree !*CoercionTree -> !.CoercionTree
 	rightInsert CT_Empty right
 		= right
 	rightInsert (CT_Node i left right2) right1
 		= CT_Node i left (rightInsert right2 right1)
+removeNode i1 CT_Empty
+	= CT_Empty
 
-			
 emptyCoercions :: !Int -> .Coercions
 emptyCoercions nr_of_attr_vars
 		= { coer_demanded = create_a_unique_array nr_of_attr_vars,
@@ -1523,3 +1517,152 @@ searchlArrElt p s i
 			= i
 		= searchl s (i+1)
 // ..MW4
+
+removeUnusedAttrVars :: !{!CoercionTree} ![Int] -> Coercions
+removeUnusedAttrVars demanded unused_attr_vars
+	# nr_of_attr_vars
+			= size demanded
+	  coercions
+			= emptyCoercions nr_of_attr_vars
+	  coercions
+	  		= iFoldSt (add_inequalities demanded) 0 nr_of_attr_vars coercions
+	= foldSt redirect_inequalities_that_contain_unused_attr_var unused_attr_vars coercions
+	  
+  where
+	add_inequalities :: !{!CoercionTree} !Int !*Coercions -> *Coercions
+	add_inequalities demanded i coercions	
+		= foldSt (\demanded coercions -> newInequality i demanded coercions)
+				(fst (flattenCoercionTree demanded.[i])) coercions
+	redirect_inequalities_that_contain_unused_attr_var :: !Int !*Coercions -> *Coercions
+	redirect_inequalities_that_contain_unused_attr_var unused_attr_var 
+				coercions=:{coer_offered, coer_demanded}
+		# (offered_attr_vars, coer_offered)
+				= accCoercionTree flattenCoercionTree unused_attr_var coer_offered
+		  (demanded_attr_vars, coer_demanded)
+				= accCoercionTree flattenCoercionTree unused_attr_var coer_demanded
+		  coer_offered = { coer_offered & [unused_attr_var] = CT_Empty }
+		  coer_offered = foldSt (appCoercionTree (removeNode unused_attr_var)) demanded_attr_vars coer_offered
+		  coer_demanded = { coer_demanded & [unused_attr_var] = CT_Empty }
+		  coer_demanded = foldSt (appCoercionTree (removeNode unused_attr_var)) offered_attr_vars coer_demanded
+		= foldSt (\(offered, demanded) coercions -> newInequality offered demanded coercions)
+				[(offered, demanded) \\ offered<-offered_attr_vars, demanded<-demanded_attr_vars]
+				{ coercions & coer_offered = coer_offered, coer_demanded = coer_demanded }
+	
+getTypeVars :: !a !*TypeVarHeap -> (!.[TypeVar],!.TypeVarHeap) | performOnTypeVars a
+getTypeVars type th_vars
+	# th_vars
+			= performOnTypeVars initializeToTVI_Empty type th_vars
+	= performOnTypeVars accum_unencountered_type_var type ([], th_vars)
+  where
+	accum_unencountered_type_var _ tv=:{tv_info_ptr} (type_var_accu, th_vars)
+		# (tvi, th_vars) = readPtr tv_info_ptr th_vars
+		= case tvi of
+			TVI_Empty
+				-> ([tv:type_var_accu], writePtr tv_info_ptr TVI_Used th_vars)
+			TVI_Used
+				-> (type_var_accu, th_vars)
+
+getAttrVars :: !a !*AttrVarHeap -> (!.[AttributeVar],!.AttrVarHeap) | performOnAttrVars a
+getAttrVars type th_attrs
+	# th_attrs
+			= performOnAttrVars initializeToAVI_Empty type th_attrs
+	= performOnAttrVars accum_unencountered_attr_var type ([], th_attrs)
+  where
+	accum_unencountered_attr_var av=:{av_info_ptr} (attr_var_accu, th_attrs)
+		# (avi, th_attrs) = readPtr av_info_ptr th_attrs
+		= case avi of
+			AVI_Empty
+				-> ([av:attr_var_accu], writePtr av_info_ptr AVI_Used th_attrs)
+			AVI_Used
+				-> (attr_var_accu, th_attrs)
+
+class performOnTypeVars a :: !(TypeAttribute TypeVar .st -> .st) !a !.st -> .st
+// run through a type and do something on each type variable
+
+instance performOnTypeVars Type
+  where
+	performOnTypeVars f (TA _ args) st
+		= performOnTypeVars f args st
+	performOnTypeVars f (at1 --> at2) st
+		= performOnTypeVars f at2 (performOnTypeVars f at1 st)
+	performOnTypeVars f (cv :@: at) st
+		= performOnTypeVars f cv (performOnTypeVars f at st)
+	performOnTypeVars f _ st
+		= st
+
+instance performOnTypeVars AType
+  where
+	performOnTypeVars f {at_attribute, at_type=TV type_var} st
+		= f at_attribute type_var st
+	performOnTypeVars f {at_attribute, at_type=GTV type_var} st
+		= f at_attribute type_var st
+	performOnTypeVars f {at_attribute, at_type=TQV type_var} st
+		= f at_attribute type_var st
+	performOnTypeVars f {at_attribute, at_type} st
+		= performOnTypeVars f at_type st
+
+instance performOnTypeVars ConsVariable
+  where
+	performOnTypeVars f (CV type_var) st
+		= f TA_Multi type_var st
+
+instance performOnTypeVars [a] | performOnTypeVars a
+  where
+	performOnTypeVars f [] st