implementation module type_io_equal_types

import StdEnv

import type_io_read
from ExtInt import between

F a b :== b

// dereference a type reference
dereference_type_reference tio_type_reference tio_common_defs type_io_state
	:== dereference_type_reference tio_type_reference tio_common_defs type_io_state;
where 
//	dereference_type_reference :: TIO_TypeReference !*{#TIO_CommonDefs} _ -> (TIO_CheckedTypeDef,!*{#TIO_CommonDefs},_);
	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_string_table, tis_max_types,*/ 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;
		| F ("bitset: " +++ toString bitset_index) type_pair_has_already_been_checked
			
			/*
			# (string_name,tio_common_defs)
				= get_type_name ref1 tis_string_table tio_common_defs;
			# string_name
				= string_name +++ " (" +++ toString tio_tr_module_n1 +++ "," +++ toString tio_tr_type_def_n1 +++ ") and ("+++ toString tio_tr_module_n2 +++ "," +++ toString tio_tr_type_def_n2 +++ ")";
			= F (string_name +++ " Equal (cached; might be wrong)") 
			*/
			= (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
			};
			
		/*
		# (string_name,tio_common_defs)
			= get_type_name ref1 tis_string_table tio_common_defs;
		# string_name
			= string_name +++ " (" +++ toString tio_tr_module_n1 +++ "," +++ toString tio_tr_type_def_n1 +++ ") and ("+++ toString tio_tr_module_n2 +++ "," +++ toString tio_tr_type_def_n2 +++ ")";
		*/
		| type1_equals_type2		
			= /*F (string_name +++ " Equal")*/ (True,tio_common_defs,type_io_state);
			
			# type_io_state
				= DelBitSetE select_bitset update_bitset type_io_state bitset_index;
			= /*F (string_name +++ " Not equal")*/ (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 <<- ("instance EqTypes/*equal_types*/ (TIO_TypeDef a) | EqTypes a")
			= 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_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_UnknownType TIO_UnknownType tio_common_defs type_io_state
		= abort "UnknownType" //(True,tio_common_defs,type_io_state)
	equal_types _ _ tio_common_defs type_io_state
		= abort "instance EqTypes TIO_TypeRhs";
//		= (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 /*,tis_string_table*/}
		| 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);
						
// TIO_SymbolType
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_vars=tio_st_vars2,tio_st_args=tio_st_args2,tio_st_arity=tio_st_arity2,tio_st_result=tio_st_result2} tio_common_defs type_io_state
		| tio_st_arity1 == tio_st_arity2
			# (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_annotation=tio_at_annotation1,tio_at_type=tio_at_type1} {tio_at_annotation=tio_at_annotation2,tio_at_type=tio_at_type2} tio_common_defs type_io_state
		# (are_annotations_equal,tio_common_defs,type_io_state)
			= equal_types tio_at_annotation1 tio_at_annotation2 tio_common_defs type_io_state;
		| are_annotations_equal
			= equal_types tio_at_type1 tio_at_type2 tio_common_defs type_io_state;
			= (False,tio_common_defs,type_io_state);
			
instance EqTypes TIO_Type
where
	equal_types (TIO_TA tio_type_symb_ident1 tio_atypes1) (TIO_TA tio_type_symb_ident2 tio_atypes2) 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_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_annotation=tio_atv_annotation1,tio_atv_variable=tio_atv_variable1} {tio_atv_annotation=tio_atv_annotation2,tio_atv_variable=tio_atv_variable2} tio_common_defs type_io_state
		# (are_annotations_equal,tio_common_defs,type_io_state)
			= equal_types tio_atv_annotation1 tio_atv_annotation2 tio_common_defs type_io_state;
		| are_annotations_equal
			= equal_types tio_atv_variable1 tio_atv_variable2 tio_common_defs type_io_state;
			= (False,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);


//1.3		
instance EqTypes {#a} | ArrayElem, EqTypes a
//3.1
/*2.0
instance EqTypes {#a} | Array {#} a & EqTypes a
0.2*/
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
			
// -------------------------------------------------------------------------------------------
import typetable

:: 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) // <<- ("find_type_equivalence: ",found,ets_assumed_type_equivalences)

assume_type_equivalence ordered_type_ref ets=:{ets_assumed_type_equivalences}
	= {ets & ets_assumed_type_equivalences = [ordered_type_ref:ets_assumed_type_equivalences] } 
	// <<- ("assume_type_equivalence: ",ordered_type_ref)
	
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
	
	
	
/*
:: OrderedTypeRef
	= {
		otr_type_ref1	:: TypeTableTypeReference
	,	otr_type_ref2	:: TypeTableTypeReference
	};
	
:: TypeTableTypeReference
	= TypeTableTypeReference !Int !TIO_TypeReference
*/

	
// 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 //<<- ("hallo",type_ref1)
			= {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_type_ref type_ref1=:(PredefinedType type_table1 _) type_ref2=:(PredefinedType type_table2 _)
	| type_table1 < type_table2
		= {otr_type_ref1 = type_ref1,otr_type_ref2 = type_ref2}
		= {otr_type_ref1 = type_ref2,otr_type_ref2 = type_ref1}
*/

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
			
/*
instance == RTTypeReference
where
	(==) (TypeReference type_table1 {tio_tr_module_n=tio_tr_module_n1,tio_tr_type_def_n=tio_tr_type_def_n1})
	     (TypeReference type_table2 {tio_tr_module_n=tio_tr_module_n2,tio_tr_type_def_n=tio_tr_type_def_n2}) 
			= type_table1 == type_table2 && tio_tr_module_n1 == tio_tr_module_n2 && tio_tr_type_def_n1 == tio_tr_type_def_n2;
	(==) (PredefinedType _ type_name1) (PredefinedType _ type_name2)		
			= type_name1 == type_name2;
	(==) _ _
			= False;
*/
import RWSDebugChoice;

// 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=:(PredefinedType _ type_name1) pt2=:(PredefinedType _ type_name2) type_tables ets
		| type_name1 == type_name2	
			# ets
				= enter_proven_assumption (order_type_ref pt1 pt2) ets	
			= (True,type_tables,ets)
			= (False,type_tables,ets)
		
	equal_type_defs (TypeReference type_table1 type_reference1) (TypeReference type_table2 type_reference2) type_tables ets
*/

	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	
			# ets
				= enter_proven_assumption (order_type_ref pt1 pt2) ets	
			= (True,type_tables,ets)
			= (False,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 // <<- ("equal_type_defs (TypeTableTypeReference):",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)

/*
dereference_type_reference tio_type_reference tio_common_defs type_io_state
	:== dereference_type_reference tio_type_reference tio_common_defs type_io_state;
where 
//	dereference_type_reference :: TIO_TypeReference !*{#TIO_CommonDefs} _ -> (TIO_CheckedTypeDef,!*{#TIO_CommonDefs},_);
	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);
*/

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

/*	
instance DerefTypeReference (RTTypeReference,RTTypeReference)
where
	 (rt_type_ref1,rt_type_ref2) type_tables
		= (tio_check_type_def1,tio_check_type_def2)
*/

/*
print_type_table_reference ({#}) :: !.Int !.TIO_TypeReference !{#*TypeTable} -> *({#Char},{#*TypeTable});
print_type_table_reference type_table_i {tio_tr_module_n,tio_tr_type_def_n,tio_type_without_definition=Nothing} type_tables
	#! (string_table_i,type_tables)
		= type_tables![type_table_i].tt_type_io_state.tis_string_table;
	#! (tio_td_name,type_tables)
		= type_tables![type_table_i].tt_tio_common_defs.[tio_tr_module_n].tio_com_type_defs.[tio_tr_type_def_n].tio_td_name;
	#! type_name
		= get_name_from_string_table tio_td_name string_table_i;
	= (type_name,type_tables);

*/		
//from DLState import print_type_table_reference;	
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)) // <<- ("deref_type_reference",type_table_i,tio_tr_module_n,tio_tr_type_def_n)
			= abort ("deref_type_reference: invalid type table reference " +++ toString type_table_i +++ " - " +++ toString s_type_tables) <<- type_tables;
		
//		# (type_name,type_tables)
//			= print_type_table_reference type_table_i type type_tables;
//		| True <<- type_name //(type_name,type1)
			
			
			
		= 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}
//	 tio_common_defs type_io_state=:{/*tis_string_table,*/tis_max_types,tis_left_module_index,tis_right_module_index}
		# type_ref1 = TypeTableTypeReference ets_left_i type_ref1a
		# type_ref2 = TypeTableTypeReference ets_right_i type_ref2a
		| type_ref1 == type_ref2 // <<- ("equal_type_defs:\n",type_ref1,"\n",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)

/*
		// 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
			};
			
		/*
		# (string_name,tio_common_defs)
			= get_type_name ref1 tis_string_table tio_common_defs;
		# string_name
			= string_name +++ " (" +++ toString tio_tr_module_n1 +++ "," +++ toString tio_tr_type_def_n1 +++ ") and ("+++ toString tio_tr_module_n2 +++ "," +++ toString tio_tr_type_def_n2 +++ ")";
		*/
		| type1_equals_type2		
			= /*F (string_name +++ " Equal")*/ (True,tio_common_defs,type_io_state);
			
			# type_io_state
				= DelBitSetE select_bitset update_bitset type_io_state bitset_index;
			= /*F (string_name +++ " Not equal")*/ (False,tio_common_defs,type_io_state);

*/






//			= (True,type_tables,ets)
				
				
//				= abort "types are *not* equivalent"
		
/*		
		# (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;
		| F ("bitset: " +++ toString bitset_index) type_pair_has_already_been_checked
			
			/*
			# (string_name,tio_common_defs)
				= get_type_name ref1 tis_string_table tio_common_defs;
			# string_name
				= string_name +++ " (" +++ toString tio_tr_module_n1 +++ "," +++ toString tio_tr_type_def_n1 +++ ") and ("+++ toString tio_tr_module_n2 +++ "," +++ toString tio_tr_type_def_n2 +++ ")";
			= F (string_name +++ " Equal (cached; might be wrong)") 
			*/
			= (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
			};
			
		/*
		# (string_name,tio_common_defs)
			= get_type_name ref1 tis_string_table tio_common_defs;
		# string_name
			= string_name +++ " (" +++ toString tio_tr_module_n1 +++ "," +++ toString tio_tr_type_def_n1 +++ ") and ("+++ toString tio_tr_module_n2 +++ "," +++ toString tio_tr_type_def_n2 +++ ")";
		*/
		| type1_equals_type2		
			= /*F (string_name +++ " Equal")*/ (True,tio_common_defs,type_io_state);
			
			# type_io_state
				= DelBitSetE select_bitset update_bitset type_io_state bitset_index;
			= /*F (string_name +++ " Not equal")*/ (False,tio_common_defs,type_io_state);

*/ 

*/

// *****
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
//			= abort (get_name_from_string_table tio_td_name1 ets_left_string_table +++ "- " +++ get_name_from_string_table tio_td_name2 ets_right_string_table) //
			= (False,type_tables,ets)
	
import RWSDebugChoice;

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" //(True,tio_common_defs,type_io_state)
	equal_type_defs (TIO_SynType syn_type1) (TIO_SynType syn_type2) type_tables ets
//		| True <<- "instance EqTypesExtended TIO_TypeRhs; synonym types not yet supported"
		= equal_type_defs syn_type1 syn_type2 type_tables ets;
		
//		= abort "UnknownType" //(True,tio_common_defs,type_io_state)

	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 
//		<<- ("########", (ets_left_i, ets_left_module_i, tio_ds_index1), (ets_right_i, ets_right_module_i, tio_ds_index2))
			# (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_ref1a type_ref2a type_tables ets
		= abort "instance EqTypesExtended TIO_DefinedSymbol";

//import RWSDebug
			
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 
			// <<- ("TIO_ConsDef type:" +++ get_name_from_string_table tio_cons_symb1 ets_left_string_table +++ "\n", tio_cons_type1,"\n",tio_cons_type2); //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_vars=tio_st_vars2,tio_st_args=tio_st_args2,tio_st_arity=tio_st_arity2,tio_st_result=tio_st_result2} type_tables ets
		| tio_st_arity1 == tio_st_arity2
			# (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_ref1a type_ref2a type_tables ets
		= abort "instance EqTypesExtended TIO_SymbolType";


instance EqTypesExtended TIO_AType
where
	equal_type_defs {tio_at_annotation=tio_at_annotation1,tio_at_type=tio_at_type1} {tio_at_annotation=tio_at_annotation2,tio_at_type=tio_at_type2} type_tables ets
		# (are_annotations_equal,type_tables,ets)
			= equal_type_defs tio_at_annotation1 tio_at_annotation2 type_tables ets;
		| are_annotations_equal
			= equal_type_defs tio_at_type1 tio_at_type2 type_tables ets;
			= (False,type_tables,ets);
			
instance EqTypesExtended TIO_Type
where
	equal_type_defs (TIO_TA tio_type_symb_ident1 tio_atypes1) (TIO_TA tio_type_symb_ident2 tio_atypes2) 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_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 _ _ _ _
		= abort "instance equal_type_defs TIO_ConsVariable";

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;
			
// new ...
			= (False,type_tables,ets);
// ... new

instance EqTypesExtended TIO_ATypeVar
where
	equal_type_defs {tio_atv_annotation=tio_atv_annotation1,tio_atv_variable=tio_atv_variable1} {tio_atv_annotation=tio_atv_annotation2,tio_atv_variable=tio_atv_variable2} type_tables ets
		# (are_annotations_equal,type_tables,ets)
			= equal_type_defs tio_atv_annotation1 tio_atv_annotation2 type_tables ets;
		| are_annotations_equal
			= equal_type_defs tio_atv_variable1 tio_atv_variable2 type_tables ets;
			= (False,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_name
			= (tio_tv_name1 == tio_tv_name2) //if True /*ets_within_type_table*/ (tio_tv_name1 == tio_tv_name2) 
			//(get_name_from_string_table tio_tv_name1 ets_left_string_table == get_name_from_string_table tio_tv_name2 ets_right_string_table)
		= (tio_tv_name,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);
//		| True <<- ("TIO_FieldSymbol", q,w1,w2)
		# tio_fs_name
			= if ets_within_type_table (tio_fs_name1 == tio_fs_name2) q
		| tio_fs_name //<<- ("TIO_FieldSymbol", q,w1,w2,tio_fs_name) // && tio_fs_var1 == tio_fs_var2 what do these fields signify?
		
			# (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
//		| True <<- ("TIO_SelectorDef",tio_sd_type1,tio_sd_type2)
		= 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);
			
//1.3		
instance EqTypesExtended {#a} | ArrayElem, EqTypesExtended a
//3.1
/*2.0
instance EqTypesExtended {#a} | Array {#} a & EqTypesExtended a
0.2*/
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
	
// *****	
