definition module type_io_equal_types

import StdEnv

import type_io_read

// 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)

class EqTypes a
where
	equal_types :: a a !*{#TIO_CommonDefs} !*TypeIOState -> (!Bool,!*{#TIO_CommonDefs},!*TypeIOState)
	
instance EqTypes TIO_TypeReference

// -------------------------------------------------------------------------------------------
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;

class EqTypesExtended a
where
	equal_type_defs :: !a !a !{#*TypeTable} !*EqTypesState -> (!Bool,!{#*TypeTable},!*EqTypesState)
	
instance EqTypesExtended TypeTableTypeReference;