implementation module type_io_equal_types

import StdEnv
from containers import equal_strictness_lists
import type_io_read
from ExtInt import between
import typetable
import BitSet;
import StdMaybe;
import StdDynamicTypes;

// dereference a type reference
dereference_type_reference {tio_tr_module_n,tio_tr_type_def_n} tio_common_defs type_io_state=:{tis_n_common_defs}
	| tio_tr_module_n == tis_n_common_defs
		= abort "dereference_type_reference; internal error predefined type cannot be indexed in tio_common_defs";
	
	# (tio_check_type_def,tio_common_defs)
		= tio_common_defs![tio_tr_module_n].tio_com_type_defs.[tio_tr_type_def_n];
	= (tio_check_type_def,tio_common_defs,type_io_state);
		
// converts a a type reference into an (unique) index
compute_index_in_type_cache :: !TIO_TypeReference !TIO_TypeReference !*TypeIOState -> (!Int,!*TypeIOState)
compute_index_in_type_cache ref1 ref2 type_io_state=:{tis_max_types}
	# (ref1_bitset_index,type_io_state)
		= compute_index_in_tis_is_type_already_checked ref1 type_io_state
	# (ref2_bitset_index,type_io_state)
		= compute_index_in_tis_is_type_already_checked ref2 type_io_state
	# bitset_index
		= ref1_bitset_index * tis_max_types + ref2_bitset_index
	= (bitset_index,type_io_state)
where
	compute_index_in_tis_is_type_already_checked {tio_tr_module_n,tio_tr_type_def_n} type_io_state
		# (base_index,type_io_state)
			= type_io_state!tis_max_types_per_module.[tio_tr_module_n];
		= ((base_index + tio_tr_type_def_n),type_io_state);

// equality on type definitions
class EqTypes a
where
	equal_types :: a a !*{#TIO_CommonDefs} !*TypeIOState -> (!Bool,!*{#TIO_CommonDefs},!*TypeIOState)
	
instance EqTypes TIO_TypeReference
where
	equal_types ref1=:{tio_tr_module_n=tio_tr_module_n1,tio_tr_type_def_n=tio_tr_type_def_n1} ref2=:{tio_tr_module_n=tio_tr_module_n2,tio_tr_type_def_n=tio_tr_type_def_n2} 
		tio_common_defs type_io_state =:{tis_left_module_index,tis_right_module_index}
		| tio_tr_module_n1 == tio_tr_module_n2 && tio_tr_type_def_n1 == tio_tr_type_def_n2
			= (True,tio_common_defs,type_io_state);
			
		# (bitset_index,type_io_state)
			= compute_index_in_type_cache ref1 ref2 type_io_state
					
		# (type_pair_has_already_been_checked,type_io_state)
			= isBitSetMemberE select_bitset type_io_state bitset_index;
		| type_pair_has_already_been_checked
			= (True,tio_common_defs,type_io_state);

		// mark type pair as being checked			
		# type_io_state
			= AddBitSetE select_bitset update_bitset type_io_state bitset_index;

		// get actual types
		# (type1,tio_common_defs,type_io_state)
			= dereference_type_reference ref1 tio_common_defs type_io_state
		# (type2,tio_common_defs,type_io_state)
			= dereference_type_reference ref2 tio_common_defs type_io_state
			
		// set current defining module indices
		# type_io_state
			= { type_io_state &
				tis_left_module_index			= tio_tr_module_n1
			,	tis_right_module_index			= tio_tr_module_n2
			};
		# (type1_equals_type2,tio_common_defs,type_io_state)
			= equal_types type1 type2 tio_common_defs type_io_state;

		// restore original defining module indices
		# type_io_state
			= { type_io_state &
				tis_left_module_index			= tis_left_module_index
			,	tis_right_module_index			= tis_right_module_index
			};
		| type1_equals_type2		
			= (True,tio_common_defs,type_io_state);
			
			# type_io_state
				= DelBitSetE select_bitset update_bitset type_io_state bitset_index;
			= (False,tio_common_defs,type_io_state);
			
instance EqTypes (TIO_TypeDef a) | EqTypes a
where
	equal_types {tio_td_name=tio_td_name1,tio_td_arity=tio_td_arity1,tio_td_rhs=tio_td_rhs1} 
				{tio_td_name=tio_td_name2,tio_td_arity=tio_td_arity2,tio_td_rhs=tio_td_rhs2} tio_common_defs type_io_state
		| tio_td_name1 == tio_td_name1 && tio_td_arity1 == tio_td_arity2
			= equal_types tio_td_rhs1 tio_td_rhs2 tio_common_defs type_io_state
			= (False,tio_common_defs,type_io_state);
		
instance EqTypes TIO_TypeRhs
where
	equal_types (TIO_AlgType tio_defined_symbols1) (TIO_AlgType tio_defined_symbols2) tio_common_defs type_io_state
		= equal_types tio_defined_symbols1 tio_defined_symbols2 tio_common_defs type_io_state;
	equal_types (TIO_SynType syn1) (TIO_SynType syn2) tio_common_defs type_io_state
		= equal_types syn1 syn2 tio_common_defs type_io_state;
	equal_types (TIO_RecordType tio_record_type1) (TIO_RecordType tio_record_type2) tio_common_defs type_io_state
		= equal_types tio_record_type1 tio_record_type2 tio_common_defs type_io_state;
	equal_types (TIO_AbstractType _) (TIO_AbstractType _) tio_common_defs type_io_state
		= abort "TIO_AbstractType"
	equal_types TIO_UnknownType TIO_UnknownType tio_common_defs type_io_state
		= abort "UnknownType"
	equal_types q2 q1 tio_common_defs type_io_state
		= (False,tio_common_defs,type_io_state)
		
instance EqTypes TIO_RecordType
where
	equal_types {tio_rt_fields=tio_rt_fields1} {tio_rt_fields=tio_rt_fields2} tio_common_defs type_io_state
		= equal_types tio_rt_fields1 tio_rt_fields2 tio_common_defs type_io_state;

instance EqTypes TIO_DefinedSymbol
where
	equal_types {tio_ds_ident=tio_ds_ident1,tio_ds_arity=tio_ds_arity1,tio_ds_index=tio_ds_index1} {tio_ds_ident=tio_ds_ident2,tio_ds_arity=tio_ds_arity2,tio_ds_index=tio_ds_index2} 
			tio_common_defs type_io_state=:{tis_left_module_index,tis_right_module_index}
		| tio_ds_ident1 == tio_ds_ident2 && tio_ds_arity1 == tio_ds_arity2
			# (tio_cons_symb1,tio_common_defs)
				= tio_common_defs![tis_left_module_index].tio_com_cons_defs.[tio_ds_index1];
			# (tio_cons_symb2,tio_common_defs)
				= tio_common_defs![tis_right_module_index].tio_com_cons_defs.[tio_ds_index2];
			= equal_types tio_cons_symb1 tio_cons_symb2 tio_common_defs type_io_state;
			
			= (False,tio_common_defs,type_io_state);
			
instance EqTypes TIO_ConsDef
where
	equal_types {tio_cons_symb=tio_cons_symb1,tio_cons_type=tio_cons_type1,tio_cons_exi_vars=tio_cons_exi_vars1} 
				{tio_cons_symb=tio_cons_symb2,tio_cons_type=tio_cons_type2,tio_cons_exi_vars=tio_cons_exi_vars2} tio_common_defs type_io_state
		| tio_cons_symb1 == tio_cons_symb2
			// constructors are equally named
			= equal_types tio_cons_type1 tio_cons_type2 tio_common_defs type_io_state;
		
			= (False,tio_common_defs,type_io_state);
						
instance EqTypes TIO_SymbolType
where
	equal_types {tio_st_vars=tio_st_vars1,tio_st_args=tio_st_args1,tio_st_arity=tio_st_arity1,tio_st_result=tio_st_result1,tio_st_args_strictness=tio_st_args_strictness1}
				{tio_st_vars=tio_st_vars2,tio_st_args=tio_st_args2,tio_st_arity=tio_st_arity2,tio_st_result=tio_st_result2,tio_st_args_strictness=tio_st_args_strictness2} tio_common_defs type_io_state
		| tio_st_arity1 == tio_st_arity2 && equal_strictness_lists tio_st_args_strictness1 tio_st_args_strictness2
			# (are_st_vars_equal,tio_common_defs,type_io_state)
				= equal_types tio_st_vars1 tio_st_vars2 tio_common_defs type_io_state;
			| are_st_vars_equal
				# (are_st_args_equal,tio_common_defs,type_io_state)
					= equal_types tio_st_args1 tio_st_args2 tio_common_defs type_io_state;
				| are_st_args_equal
					= equal_types tio_st_result1 tio_st_result2 tio_common_defs type_io_state;
					
					// tio_st_args1 <> tio_st_args2
					= (False,tio_common_defs,type_io_state);
					
				// tio_st_vars1 <> tio_st_vars2
				= (False,tio_common_defs,type_io_state);
						
			// tio_st_arity1 <> tio_st_arity2
			= (False,tio_common_defs,type_io_state);

instance EqTypes TIO_AType
where
	equal_types {tio_at_type=tio_at_type1} {tio_at_type=tio_at_type2} tio_common_defs type_io_state
		= equal_types tio_at_type1 tio_at_type2 tio_common_defs type_io_state;
			
instance EqTypes TIO_Type
where
	equal_types (TIO_TAS tio_type_symb_ident1 tio_atypes1 strictness_list1) (TIO_TAS tio_type_symb_ident2 tio_atypes2 strictness_list2) tio_common_defs type_io_state
		# (are_type_symb_idents_equal,tio_common_defs,type_io_state)
			= equal_types tio_type_symb_ident1 tio_type_symb_ident2 tio_common_defs type_io_state;
		| are_type_symb_idents_equal && equal_strictness_lists strictness_list1 strictness_list2 
			= equal_types tio_atypes1 tio_atypes2 tio_common_defs type_io_state;
			= (False,tio_common_defs,type_io_state);
			
	equal_types (tio_atype1a ----> tio_atype1b) (tio_atype2a ----> tio_atype2b) tio_common_defs type_io_state
		# (are_atypes1_equal,tio_common_defs,type_io_state)
			= equal_types tio_atype1a tio_atype2a tio_common_defs type_io_state;
		| are_atypes1_equal
			= equal_types tio_atype1b tio_atype2b tio_common_defs type_io_state;
		
			= (False,tio_common_defs,type_io_state);
			
	equal_types (tio_cons_variable1 :@@: tio_atypes1) (tio_cons_variable2 :@@: tio_atypes2) tio_common_defs type_io_state
		# (are_tio_cons_variables_equal,tio_common_defs,type_io_state)
			= equal_types tio_cons_variable1 tio_cons_variable2 tio_common_defs type_io_state;
		| are_tio_cons_variables_equal
			= equal_types tio_atypes1 tio_atypes2 tio_common_defs type_io_state;
		
			= (False,tio_common_defs,type_io_state);
	
	equal_types (TIO_TB tio_basic_type1) (TIO_TB tio_basic_type2) tio_common_defs type_io_state
		= equal_types tio_basic_type1 tio_basic_type2 tio_common_defs type_io_state;
	
	equal_types (TIO_GTV tio_type_var1) (TIO_GTV tio_type_var2) tio_common_defs type_io_state
		= equal_types tio_type_var1 tio_type_var2 tio_common_defs type_io_state;

	equal_types (TIO_TV tio_type_var1) (TIO_TV tio_type_var2) tio_common_defs type_io_state
		= equal_types tio_type_var1 tio_type_var2 tio_common_defs type_io_state;
		
	equal_types (TIO_TQV tio_type_var1) (TIO_TQV tio_type_var2) tio_common_defs type_io_state
		= equal_types tio_type_var1 tio_type_var2 tio_common_defs type_io_state;

	equal_types TIO_TE TIO_TE tio_common_defs type_io_state
		= (True,tio_common_defs,type_io_state);
		
	equal_types _ _ tio_common_defs type_io_state
		= (False,tio_common_defs,type_io_state);
			
instance EqTypes TIO_BasicType
where
	equal_types TIO_BT_Int TIO_BT_Int tio_common_defs type_io_state
		= (True,tio_common_defs,type_io_state);
		
	equal_types TIO_BT_Char TIO_BT_Char tio_common_defs type_io_state
		= (True,tio_common_defs,type_io_state);

	equal_types TIO_BT_Real TIO_BT_Real tio_common_defs type_io_state
		= (True,tio_common_defs,type_io_state);
		
	equal_types TIO_BT_Bool TIO_BT_Bool tio_common_defs type_io_state
		= (True,tio_common_defs,type_io_state);
	
	equal_types TIO_BT_Dynamic TIO_BT_Dynamic tio_common_defs type_io_state
		= (True,tio_common_defs,type_io_state);

	equal_types TIO_BT_File TIO_BT_File tio_common_defs type_io_state
		= (True,tio_common_defs,type_io_state);

	equal_types TIO_BT_World TIO_BT_World tio_common_defs type_io_state
		= (True,tio_common_defs,type_io_state);

	equal_types (TIO_BT_String tio_type1) (TIO_BT_String tio_type2) tio_common_defs type_io_state
		= equal_types tio_type1 tio_type2 tio_common_defs type_io_state;
		
	equal_types _ _ tio_common_defs type_io_state
		= (False,tio_common_defs,type_io_state);

instance EqTypes TIO_ConsVariable
where
	equal_types _ _ _ _
		= abort "instance equal_types TIO_ConsVariable";
		
instance EqTypes TIO_TypeSymbIdent
where
	equal_types {tio_type_name_ref=tio_type_name_ref1,tio_type_arity=tio_type_arity1} {tio_type_name_ref=tio_type_name_ref2,tio_type_arity=tio_type_arity2} tio_common_defs type_io_state
		| tio_type_arity1 == tio_type_arity2
			= equal_types tio_type_name_ref1 tio_type_name_ref2 tio_common_defs type_io_state;
	
instance EqTypes TIO_ATypeVar
where
	equal_types {tio_atv_variable=tio_atv_variable1} {tio_atv_variable=tio_atv_variable2} tio_common_defs type_io_state
		= equal_types tio_atv_variable1 tio_atv_variable2 tio_common_defs type_io_state;
			
instance EqTypes TIO_TypeVar
where
	equal_types {tio_tv_name=tio_tv_name1} {tio_tv_name=tio_tv_name2} tio_common_defs type_io_state
		= (tio_tv_name1 == tio_tv_name2,tio_common_defs,type_io_state); 
		
instance EqTypes TIO_Annotation
where
	equal_types TIO_AN_Strict TIO_AN_Strict tio_common_defs type_io_state
		= (True,tio_common_defs,type_io_state);
	equal_types TIO_AN_None TIO_AN_None tio_common_defs type_io_state
		= (True,tio_common_defs,type_io_state);
	equal_types _ _ tio_common_defs type_io_state
		= (False,tio_common_defs,type_io_state);

instance EqTypes TIO_FieldSymbol
where
	equal_types {tio_fs_name=tio_fs_name1,tio_fs_var=tio_fs_var1,tio_fs_index=tio_fs_index1}
				{tio_fs_name=tio_fs_name2,tio_fs_var=tio_fs_var2,tio_fs_index=tio_fs_index2} tio_common_defs type_io_state=:{tis_left_module_index,tis_right_module_index}
		| tio_fs_name1 == tio_fs_name2 && tio_fs_var1 == tio_fs_var2
		
			# (tio_select_def1,tio_common_defs)
				= tio_common_defs![tis_left_module_index].tio_com_selector_defs.[tio_fs_index1];
			# (tio_select_def2,tio_common_defs)
				= tio_common_defs![tis_right_module_index].tio_com_selector_defs.[tio_fs_index2];
			= equal_types tio_select_def1 tio_select_def2 tio_common_defs type_io_state;
			
			= (False,tio_common_defs,type_io_state);

instance EqTypes TIO_SelectorDef
where
	equal_types {tio_sd_type=tio_sd_type1} {tio_sd_type=tio_sd_type2} tio_common_defs type_io_state
		= equal_types tio_sd_type1 tio_sd_type2 tio_common_defs type_io_state;
		
instance EqTypes [a] | EqTypes a
where
	equal_types [] [] tio_common_defs type_io_state
		= (True,tio_common_defs,type_io_state);
	equal_types [type1:types1] [type2:types2] tio_common_defs type_io_state
		# (type1_equals_type2,tio_common_defs,type_io_state)
			= equal_types type1 type2 tio_common_defs type_io_state;
		| not type1_equals_type2
			= (False,tio_common_defs,type_io_state);
		= equal_types types1 types2 tio_common_defs type_io_state;

	equal_types _ _ tio_common_defs type_io_state
		= (False,tio_common_defs,type_io_state);

instance EqTypes {#a} | Array {#} a & EqTypes a
where
	equal_types a1 a2 tio_common_defs type_io_state
		| s_a1 <> s_a2
			= (False,tio_common_defs,type_io_state)
			
		= equal_types_loop 0 s_a1 tio_common_defs type_io_state
	where 
		equal_types_loop i limit tio_common_defs type_io_state
			| i == limit
				= (True,tio_common_defs,type_io_state);
			
			# (elements_are_equal,tio_common_defs,type_io_state)
				= equal_types a1.[i] a2.[i] tio_common_defs type_io_state;
			| not elements_are_equal
				= (False,tio_common_defs,type_io_state);
			= equal_types_loop (inc i) limit tio_common_defs type_io_state;
	
		s_a1
			= size a1
		s_a2
			= size a2
			
:: OrderedTypeRef
	= {
		otr_type_ref1	:: TypeTableTypeReference
	,	otr_type_ref2	:: TypeTableTypeReference
	};
	
:: *EqTypesState
	= {
		ets_within_type_table			:: !Bool	// iff ets_left_i == ets_right_i

	,	ets_left_i						:: !Int		// type table index for left type (1st arg)
	,	ets_right_i						:: !Int		// type table index for right type (2nd arg)
	
	,	ets_left_module_i				:: !Int		// left module index
	,	ets_right_module_i				:: !Int		// right module index
	
	,	ets_assumed_type_equivalences	:: [OrderedTypeRef]
	,	ets_proven_type_equivalences	:: [OrderedTypeRef]
	
	,	ets_left_string_table			:: !String
	,	ets_right_string_table			:: !String
	}; 
	
default_eq_types_state :: *EqTypesState;
default_eq_types_state
	= { 
		ets_within_type_table			= False

	,	ets_left_i						= -1
	,	ets_right_i						= -1

	,	ets_left_module_i				= -1
	,	ets_right_module_i				= -1

	,	ets_assumed_type_equivalences	= []
	,	ets_proven_type_equivalences	= []

	,	ets_left_string_table			= {}
	,	ets_right_string_table			= {}
	}; 
	
find_type_equivalence ordered_type_ref ets=:{ets_assumed_type_equivalences,ets_proven_type_equivalences}
	# ets_assumed_type_equivalent
		= filter ((==) ordered_type_ref) ets_assumed_type_equivalences
	# ets_proven_type_equivalent
		= filter ((==) ordered_type_ref) ets_proven_type_equivalences
	# found
		= not (isEmpty ets_assumed_type_equivalent) || not (isEmpty ets_proven_type_equivalent)
	= (found,ets)

assume_type_equivalence ordered_type_ref ets=:{ets_assumed_type_equivalences}
	= {ets & ets_assumed_type_equivalences = [ordered_type_ref:ets_assumed_type_equivalences] } 
	
get_assumed_type_equivalence ets=:{ets_assumed_type_equivalences=[assumed_type_equivalence:ets_assumed_type_equivalences]}
	# ets
		= { ets &
			ets_assumed_type_equivalences	= ets_assumed_type_equivalences
		}	
	= (assumed_type_equivalence,ets)
	
enter_proven_assumption proven_type_equivalence ets=:{ets_proven_type_equivalences}
	# ets
		= { ets &
			ets_proven_type_equivalences	= [proven_type_equivalence:ets_proven_type_equivalences]
		}
	= ets
	
// type_table1 <> type_table2 otherwise it would be within a type table. it suffices for nf
order_type_ref type_ref1=:(TypeTableTypeReference type_table1 tio_type_ref1) type_ref2=:(TypeTableTypeReference type_table2 tio_type_ref2)
	| type_table1 < type_table2
		= {otr_type_ref1 = type_ref1,otr_type_ref2 = type_ref2}
		| type_table1 > type_table2
			= {otr_type_ref1 = type_ref2,otr_type_ref2 = type_ref1};
			= order_tio_type_reference tio_type_ref1 tio_type_ref2;
where
	order_tio_type_reference {tio_type_without_definition=Just _} {tio_type_without_definition=Just _}
		= {otr_type_ref1 = type_ref1,otr_type_ref2 = type_ref2};
	order_tio_type_reference t1=:{tio_tr_module_n=tio_tr_module_n1,tio_tr_type_def_n=tio_tr_type_def_n1} t2=:{tio_tr_module_n=tio_tr_module_n2,tio_tr_type_def_n=tio_tr_type_def_n2}
		| tio_tr_module_n1 < tio_tr_module_n2
			= {otr_type_ref1 = type_ref1,otr_type_ref2 = type_ref2};
			|  tio_tr_module_n1 > tio_tr_module_n2
				= {otr_type_ref1 = type_ref2,otr_type_ref2 = type_ref1};
				
				| tio_tr_type_def_n1 < tio_tr_type_def_n2
					= {otr_type_ref1 = type_ref1,otr_type_ref2 = type_ref2};
					| tio_tr_type_def_n1 > tio_tr_type_def_n2
						= {otr_type_ref1 = type_ref2,otr_type_ref2 = type_ref1};
						
						= {otr_type_ref1 = type_ref1,otr_type_ref2 = type_ref2};

instance == OrderedTypeRef
where
	(==) ordered_type_refA ordered_type_refB
		= ordered_type_refA.otr_type_ref1 == ordered_type_refB.otr_type_ref1 &&
		  ordered_type_refA.otr_type_ref2 == ordered_type_refB.otr_type_ref2
			
// Properties:
// - the order of type tables is maintained. 1st arg b
class EqTypesExtended a
where
	equal_type_defs :: !a !a !{#*TypeTable} !*EqTypesState -> (!Bool,!{#*TypeTable},!*EqTypesState)

// only externally called
instance EqTypesExtended TypeTableTypeReference
where 
	equal_type_defs pt1=:(TypeTableTypeReference _ {tio_type_without_definition=Just type_name1}) pt2=:(TypeTableTypeReference _ {tio_type_without_definition=Just type_name2}) type_tables ets
		= (type_name1 == type_name2,type_tables,ets)

	equal_type_defs type_ref1=:(TypeTableTypeReference type_table1 type_reference1=:{tio_type_without_definition=Nothing}) type_ref2=:(TypeTableTypeReference type_table2 type_reference2=:{tio_type_without_definition=Nothing}) type_tables ets
		| type_ref1 == type_ref2
			= (True,type_tables,ets)

		# ets_within_type_table
			= type_table1 == type_table2
			
		// select {left,right} string tables
		# (ets_left_string_table,type_tables)
			= type_tables![type_table1].tt_type_io_state.tis_string_table
		# (ets_right_string_table,type_tables)
			= type_tables![type_table2].tt_type_io_state.tis_string_table

		// 
		# ets
			= { ets &
				ets_within_type_table	= ets_within_type_table

			,	ets_left_i				= type_table1
			,	ets_right_i				= type_table2

			,	ets_left_string_table	= if ets_within_type_table {} ets_left_string_table
			,	ets_right_string_table	= if ets_within_type_table {} ets_right_string_table

			}; 
		= equal_type_defs type_reference1 type_reference2 type_tables ets
		
	equal_type_defs _ _ type_tables ets
		= (False,type_tables,ets)

class DerefTypeReference a
where
	deref_type_reference :: a !{#TypeTable} -> (TIO_CheckedTypeDef,!{#TypeTable})

instance DerefTypeReference TypeTableTypeReference
where
	deref_type_reference type1=:(TypeTableTypeReference type_table_i type=:{tio_tr_module_n,tio_tr_type_def_n,tio_type_without_definition=Nothing}) type_tables
		# (s_type_tables,type_tables)
			= usize type_tables
		| not (between 0 type_table_i (dec s_type_tables))
			= abort ("deref_type_reference: invalid type table reference " +++ toString type_table_i +++ " - " +++ toString s_type_tables)
		
		= type_tables![type_table_i].tt_tio_common_defs.[tio_tr_module_n].tio_com_type_defs.[tio_tr_type_def_n]

// types within one type table and types across type tables
instance EqTypesExtended TIO_TypeReference
where
	equal_type_defs type_ref1a=:{tio_tr_module_n=tio_tr_module_n1} type_ref2a=:{tio_tr_module_n=tio_tr_module_n2} type_tables ets=:{/*ets_within_type_table=False,*/ets_left_module_i,ets_right_module_i,ets_left_i,ets_right_i}
		# type_ref1 = TypeTableTypeReference ets_left_i type_ref1a
		# type_ref2 = TypeTableTypeReference ets_right_i type_ref2a
		
		| type_ref1 == type_ref2
			= (True,type_tables,ets)

			// check whether type pair is assumed or proven to be equivalent
			# ordered_type_ref
				= order_type_ref type_ref1 type_ref2
			# (are_types_equivalent,ets)
				= find_type_equivalence ordered_type_ref ets
			| are_types_equivalent
				= (True,type_tables,ets)
	
				// assume type equivalence (termination)
				# ets
					= assume_type_equivalence ordered_type_ref ets
	
				// dereference type reference
				# (type1,type_tables)
					= deref_type_reference type_ref1 type_tables
				# (type2,type_tables )
					= deref_type_reference type_ref2 type_tables
										
				// set defining modules of new types
				# ets
					= { ets &
						ets_left_module_i				= tio_tr_module_n1
					,	ets_right_module_i				= tio_tr_module_n2
					}
					
				// check it
				# (is_type_pair_equivalent,type_tables,ets)
					= equal_type_defs type1 type2 type_tables ets
	
				// restore old defining modules
				# ets
					= { ets &
						ets_left_module_i				= ets_left_module_i
					,	ets_right_module_i				= ets_right_module_i
					}
					
				# (assumed_type_equivalence,ets)
					= get_assumed_type_equivalence ets
				| is_type_pair_equivalent
					// assumption has been proven
					# ets
						= enter_proven_assumption assumed_type_equivalence ets				
					= (True,type_tables,ets)
	
					= (False,type_tables,ets)
					
	equal_type_defs t1 t2 type_tables ets
		= abort "equal_type_defs; internal error";

instance EqTypesExtended (TIO_TypeDef a) | EqTypesExtended a
where
	equal_type_defs {tio_td_name=tio_td_name1,tio_td_arity=tio_td_arity1,tio_td_rhs=tio_td_rhs1} 
				{tio_td_name=tio_td_name2,tio_td_arity=tio_td_arity2,tio_td_rhs=tio_td_rhs2} type_tables ets=:{ets_within_type_table,ets_left_string_table,ets_right_string_table}
		# tio_td_name
			= if ets_within_type_table (tio_td_name1 == tio_td_name2) (get_name_from_string_table tio_td_name1 ets_left_string_table == get_name_from_string_table tio_td_name2 ets_right_string_table)
		| tio_td_name && tio_td_arity1 == tio_td_arity2
			= equal_type_defs tio_td_rhs1 tio_td_rhs2 type_tables ets
			= (False,type_tables,ets)
	
instance EqTypesExtended TIO_TypeRhs
where
	equal_type_defs (TIO_AlgType tio_defined_symbols1) (TIO_AlgType tio_defined_symbols2) type_tables ets
		= equal_type_defs tio_defined_symbols1 tio_defined_symbols2 type_tables ets;
	equal_type_defs (TIO_RecordType tio_record_type1) (TIO_RecordType tio_record_type2) type_tables ets
		= equal_type_defs tio_record_type1 tio_record_type2 type_tables ets;
	equal_type_defs TIO_UnknownType TIO_UnknownType type_tables ets
		= abort "UnknownType";
	equal_type_defs (TIO_SynType syn_type1) (TIO_SynType syn_type2) type_tables ets
		= equal_type_defs syn_type1 syn_type2 type_tables ets;
	equal_type_defs _ _ type_tables ets
		= (False,type_tables,ets)
		
instance EqTypesExtended TIO_RecordType
where
	equal_type_defs {tio_rt_fields=tio_rt_fields1} {tio_rt_fields=tio_rt_fields2} type_tables ets
		= equal_type_defs tio_rt_fields1 tio_rt_fields2 type_tables ets
		
instance EqTypesExtended TIO_DefinedSymbol
where
	equal_type_defs {tio_ds_ident=tio_ds_ident1,tio_ds_arity=tio_ds_arity1,tio_ds_index=tio_ds_index1} {tio_ds_ident=tio_ds_ident2,tio_ds_arity=tio_ds_arity2,tio_ds_index=tio_ds_index2} 
			type_tables ets=:{ets_within_type_table,ets_left_string_table,ets_right_string_table,ets_left_i,ets_right_i,ets_left_module_i,ets_right_module_i}
		# tio_ds_ident
			= if ets_within_type_table (tio_ds_ident1 == tio_ds_ident2) 
				(get_name_from_string_table tio_ds_ident1 ets_left_string_table == get_name_from_string_table tio_ds_ident2 ets_right_string_table)
		| tio_ds_ident && tio_ds_arity1 == tio_ds_arity2 
			# (tio_cons_symb1,type_tables)
				= type_tables![ets_left_i].tt_tio_common_defs.[ets_left_module_i].tio_com_cons_defs.[tio_ds_index1];
			# (tio_cons_symb2,type_tables)
				= type_tables![ets_right_i].tt_tio_common_defs.[ets_right_module_i].tio_com_cons_defs.[tio_ds_index2];
			= equal_type_defs tio_cons_symb1 tio_cons_symb2 type_tables ets;
			
			= (False,type_tables,ets);
	equal_type_defs _ _ type_tables ets
		= abort "instance EqTypesExtended TIO_DefinedSymbol";

instance EqTypesExtended TIO_ConsDef
where
	equal_type_defs {tio_cons_symb=tio_cons_symb1,tio_cons_type=tio_cons_type1,tio_cons_exi_vars=tio_cons_exi_vars1} 
				{tio_cons_symb=tio_cons_symb2,tio_cons_type=tio_cons_type2,tio_cons_exi_vars=tio_cons_exi_vars2} type_tables ets=:{ets_within_type_table,ets_left_string_table,ets_right_string_table}
		# tio_cons_symb
			= if ets_within_type_table (tio_cons_symb1 == tio_cons_symb2) (get_name_from_string_table tio_cons_symb1 ets_left_string_table == get_name_from_string_table tio_cons_symb2 ets_right_string_table)
		| tio_cons_symb
			// constructors are equally named
			= equal_type_defs tio_cons_type1 tio_cons_type2 type_tables ets 

			= (False,type_tables,ets);

instance EqTypesExtended TIO_SymbolType
where
	equal_type_defs {tio_st_vars=tio_st_vars1,tio_st_args=tio_st_args1,tio_st_arity=tio_st_arity1,tio_st_result=tio_st_result1,tio_st_args_strictness=tio_st_args_strictness1}
				{tio_st_vars=tio_st_vars2,tio_st_args=tio_st_args2,tio_st_arity=tio_st_arity2,tio_st_result=tio_st_result2,tio_st_args_strictness=tio_st_args_strictness2} type_tables ets
		| tio_st_arity1 == tio_st_arity2 && equal_strictness_lists tio_st_args_strictness1 tio_st_args_strictness2
			# (are_st_vars_equal,type_tables,ets)
				= equal_type_defs tio_st_vars1 tio_st_vars2 type_tables ets;
			| are_st_vars_equal
				# (are_st_args_equal,type_tables,ets)
					= equal_type_defs tio_st_args1 tio_st_args2 type_tables ets;
				| are_st_args_equal
					= equal_type_defs tio_st_result1 tio_st_result2 type_tables ets;
					
					// tio_st_args1 <> tio_st_args2
					= (False,type_tables,ets) 
					
				// tio_st_vars1 <> tio_st_vars2
				= (False,type_tables,ets)
						
			// tio_st_arity1 <> tio_st_arity2
			= (False,type_tables,ets)
			
	equal_type_defs _ _ type_tables ets
		= abort "instance EqTypesExtended TIO_SymbolType";

instance EqTypesExtended TIO_AType
where
	equal_type_defs {tio_at_type=tio_at_type1} {tio_at_type=tio_at_type2} type_tables ets
		= equal_type_defs tio_at_type1 tio_at_type2 type_tables ets;
			
instance EqTypesExtended TIO_Type
where
	equal_type_defs (TIO_TAS tio_type_symb_ident1 tio_atypes1 strictness1) (TIO_TAS tio_type_symb_ident2 tio_atypes2 strictness2) type_tables ets
		# (are_type_symb_idents_equal,type_tables,ets)
			= equal_type_defs tio_type_symb_ident1 tio_type_symb_ident2 type_tables ets;
		| are_type_symb_idents_equal && equal_strictness_lists strictness1 strictness2
			= equal_type_defs tio_atypes1 tio_atypes2 type_tables ets;
			= (False,type_tables,ets);
			
	equal_type_defs (tio_atype1a ----> tio_atype1b) (tio_atype2a ----> tio_atype2b) type_tables ets
		# (are_atypes1_equal,type_tables,ets)
			= equal_type_defs tio_atype1a tio_atype2a type_tables ets;
		| are_atypes1_equal
			= equal_type_defs tio_atype1b tio_atype2b type_tables ets;
		
			= (False,type_tables,ets);
			
	equal_type_defs (tio_cons_variable1 :@@: tio_atypes1) (tio_cons_variable2 :@@: tio_atypes2) type_tables ets
		# (are_tio_cons_variables_equal,type_tables,ets)
			= equal_type_defs tio_cons_variable1 tio_cons_variable2 type_tables ets;
		| are_tio_cons_variables_equal
			= equal_type_defs tio_atypes1 tio_atypes2 type_tables ets;
		
			= (False,type_tables,ets);
	
	equal_type_defs (TIO_TB tio_basic_type1) (TIO_TB tio_basic_type2) type_tables ets
		= equal_type_defs tio_basic_type1 tio_basic_type2 type_tables ets;
	
	equal_type_defs (TIO_GTV tio_type_var1) (TIO_GTV tio_type_var2) type_tables ets
		= equal_type_defs tio_type_var1 tio_type_var2 type_tables ets;

	equal_type_defs (TIO_TV tio_type_var1) (TIO_TV tio_type_var2) type_tables ets
		= equal_type_defs tio_type_var1 tio_type_var2 type_tables ets;
		
	equal_type_defs (TIO_TQV tio_type_var1) (TIO_TQV tio_type_var2) type_tables ets
		= equal_type_defs tio_type_var1 tio_type_var2 type_tables ets;

	equal_type_defs TIO_TE TIO_TE type_tables ets
		= (True,type_tables,ets)
		
	equal_type_defs _ _ type_tables ets
		= (False,type_tables,ets);
		
instance EqTypesExtended TIO_BasicType
where
	equal_type_defs TIO_BT_Int TIO_BT_Int type_tables ets
		= (True,type_tables,ets)
		
	equal_type_defs TIO_BT_Char TIO_BT_Char type_tables ets
		= (True,type_tables,ets)

	equal_type_defs TIO_BT_Real TIO_BT_Real type_tables ets
		= (True,type_tables,ets)
		
	equal_type_defs TIO_BT_Bool TIO_BT_Bool type_tables ets
		= (True,type_tables,ets)
	
	equal_type_defs TIO_BT_Dynamic TIO_BT_Dynamic type_tables ets
		= (True,type_tables,ets)

	equal_type_defs TIO_BT_File TIO_BT_File type_tables ets
		= (True,type_tables,ets)

	equal_type_defs TIO_BT_World TIO_BT_World type_tables ets
		= (True,type_tables,ets)

	equal_type_defs (TIO_BT_String tio_type1) (TIO_BT_String tio_type2) type_tables ets
		= equal_type_defs tio_type1 tio_type2 type_tables ets;
		
	equal_type_defs _ _ type_tables ets
		= (False,type_tables,ets);
		
instance EqTypesExtended TIO_ConsVariable
where
	equal_type_defs (TIO_CV tio_type_var1) (TIO_CV tio_type_var2) type_tables ets
		= equal_type_defs tio_type_var1 tio_type_var2 type_tables ets;
	equal_type_defs (TIO_TempCV _) (TIO_TempCV _) type_tables ets
		= abort "instance equal_type_defs TIO_ConsVariable; TIO_TempCV";
	equal_type_defs (TIO_TempQCV _) (TIO_TempQCV _) type_tables ets
		= abort "instance equal_type_defs TIO_ConsVariable; TIO_TempQCV";
	equal_type_defs _ _ type_tables ets
		= (False,type_tables,ets);

instance EqTypesExtended TIO_TypeSymbIdent
where
	equal_type_defs {tio_type_name_ref=tio_type_name_ref1,tio_type_arity=tio_type_arity1} {tio_type_name_ref=tio_type_name_ref2,tio_type_arity=tio_type_arity2} type_tables ets
		| tio_type_arity1 == tio_type_arity2
			= equal_type_defs tio_type_name_ref1 tio_type_name_ref2 type_tables ets;

			= (False,type_tables,ets);

instance EqTypesExtended TIO_ATypeVar
where
	equal_type_defs {tio_atv_variable=tio_atv_variable1} {tio_atv_variable=tio_atv_variable2} type_tables ets
		= equal_type_defs tio_atv_variable1 tio_atv_variable2 type_tables ets;

instance EqTypesExtended TIO_TypeVar
where
	equal_type_defs {tio_tv_name=tio_tv_name1} {tio_tv_name=tio_tv_name2} type_tables ets=:{ets_within_type_table,ets_left_string_table,ets_right_string_table}
		= (tio_tv_name1 == tio_tv_name2,type_tables,ets)
		
instance EqTypesExtended TIO_Annotation
where
	equal_type_defs TIO_AN_Strict TIO_AN_Strict type_tables ets
		= (True,type_tables,ets)
	equal_type_defs TIO_AN_None TIO_AN_None type_tables ets
		= (True,type_tables,ets)
	equal_type_defs _ _ type_tables ets
		= (False,type_tables,ets);
		
instance EqTypesExtended TIO_FieldSymbol
where
	equal_type_defs {tio_fs_name=tio_fs_name1,tio_fs_var=tio_fs_var1,tio_fs_index=tio_fs_index1}
				{tio_fs_name=tio_fs_name2,tio_fs_var=tio_fs_var2,tio_fs_index=tio_fs_index2} type_tables 
				ets=:{ets_within_type_table,ets_left_string_table,ets_right_string_table,ets_left_i,ets_right_i,ets_left_module_i,ets_right_module_i}
		# w1 = get_name_from_string_table tio_fs_name1 ets_left_string_table;
		# w2 = get_name_from_string_table tio_fs_name2 ets_right_string_table;
		# q =(w1 == w2);
		# tio_fs_name
			= if ets_within_type_table (tio_fs_name1 == tio_fs_name2) q
		| tio_fs_name
		
			# (tio_select_def1,type_tables)
				= type_tables![ets_left_i].tt_tio_common_defs.[ets_left_module_i].tio_com_selector_defs.[tio_fs_index1];
			# (tio_select_def2,type_tables)
				= type_tables![ets_right_i].tt_tio_common_defs.[ets_right_module_i].tio_com_selector_defs.[tio_fs_index2];
			= equal_type_defs tio_select_def1 tio_select_def2 type_tables ets;
			
			= (False,type_tables,ets);

instance EqTypesExtended TIO_SelectorDef
where
	equal_type_defs {tio_sd_type=tio_sd_type1} {tio_sd_type=tio_sd_type2} type_tables ets
		= equal_type_defs tio_sd_type1 tio_sd_type2 type_tables ets;

instance EqTypesExtended [a] | EqTypesExtended a
where
	equal_type_defs [] [] tio_common_defs type_io_state
		= (True,tio_common_defs,type_io_state);
	equal_type_defs [type1:types1] [type2:types2] tio_common_defs type_io_state
		# (type1_equals_type2,tio_common_defs,type_io_state)
			= equal_type_defs type1 type2 tio_common_defs type_io_state;
		| not type1_equals_type2
			= (False,tio_common_defs,type_io_state);
		= equal_type_defs types1 types2 tio_common_defs type_io_state;
	equal_type_defs _ _ tio_common_defs type_io_state
		= (False,tio_common_defs,type_io_state);
			
instance EqTypesExtended {#a} | Array {#} a & EqTypesExtended a
where
	equal_type_defs a1 a2 type_tables ets
		| s_a1 <> s_a2
			= (False,type_tables,ets)
		= equal_type_defs_loop 0 s_a1 type_tables ets
	where 
		equal_type_defs_loop i limit type_tables ets
			| i == limit
				= (True,type_tables,ets)
			
			# (elements_are_equal,type_tables,ets)
				= equal_type_defs a1.[i] a2.[i] type_tables ets;
			| not elements_are_equal
				= (False,type_tables,ets);
			= equal_type_defs_loop (inc i) limit type_tables ets;
	
		s_a1
			= size a1
		s_a2
			= size a2