implementation module check_types;

import StdEnv;
import pdObjectToMem;
import link_switches;
from DynamicLinkerInterface import ::TypeReference(..),::LibraryID(..),
	 instance EnDecode TypeReference, instance DefaultElem TypeReference;
import EnDecode;
import utilities;
import ExtArray;
import ExtInt;
import StdDynamicLowLevelInterface;
import type_io_equal_types;
import type_io_read;
import StdDynamicTypes;
import typetable;
import LibraryInstance;
import LinkerMessages;
import StdMaybe;
import _SystemDynamic;

CheckTypeDefinitions :: !ProcessSerialNumber ![{#.Char}] !*DLServerState !*f -> *(Bool,ProcessSerialNumber,*DLServerState,!*f) | FileEnv f;
CheckTypeDefinitions client_id [arg] s io
	#! (client_exists,dl_client_state,s) 
		= RemoveFromDLServerState client_id s;
	| not client_exists
		= internal_error "CheckTypeDefinitions (internal error): client not registered" client_id dl_client_state s io;

	# l = decode ( arg );

	#! (dl_client_state) = AddDebugMessage ("CheckTypeDefinitions" +++ toString (length l)) dl_client_state;

	/*
		for each pair of types:
			- replace Address by Number if necessary
			- apply equal_types to both types
				if type definitions are equivalent then continue with next pair else quit 
				
		changes to equal_types:
			- two self-contained tio_common_defs; may require extracting info from type_io_state
			- a general type check state
	*/
	
	#! (type_defs_are_equivalent,dl_client_state,io)
		= CheckAndEnterType l Nothing dl_client_state io;

	#! io
		= SendAddressToClient client_id (encode type_defs_are_equivalent) io;
	# ok
		= True
	= (not ok,client_id,AddToDLServerState dl_client_state s,/*KillClient3 client_id ok*/ io);

// Task:
// 1. checks type definitions in the 1st-arg list
// 2. if all type defs checks succeed, then these type (and the types they depend upon) are entered into the type implementation table
CheckAndEnterType :: [.TypeReference] !(Maybe Int) !*DLClientState !*f -> *(Bool,*DLClientState,!*f) | FileEnv f;
CheckAndEnterType l library_instance_i_implements_type_equivalence_class dl_client_state io
	/*
		for each pair of types:
			- replace Address by Number if necessary
			- apply equal_types to both types
				if type definitions are equivalent then continue with next pair else quit 
				
		changes to equal_types:
			- two self-contained tio_common_defs; may require extracting info from type_io_state
			- a general type check state
				
	*/

	// pass 1: establish equivalences
	# (type_defs_are_equivalent,equivalent_type_defs,dl_client_state,io)
		= foldSt check_type_pair l (True,[],dl_client_state,io);
	# (dl_client_state,io)
		= case (type_defs_are_equivalent && not (isEmpty equivalent_type_defs)) of {
			True
				// pass 2: generate type equations

				// print results
				# dl_client_state
					= print_type_implementation_table dl_client_state;
				-> (dl_client_state,io);
			_
				-> (dl_client_state,io);
		};
	= (type_defs_are_equivalent,dl_client_state,io);
where {
	check_type_pair {tr_type_name,tr_module_name1,tr_module_name2,tr_library1,tr_library2} (True,equivalent_types,dl_client_state,io)
		// build type references
		# (library_instance_i1,rt_type_reference1,dl_client_state,io)
			= convert_T_ypeID_to_internal_type_reference_LibraryID tr_type_name tr_module_name1 tr_library1 dl_client_state io;
		# (library_instance_i2,rt_type_reference2,dl_client_state,io)
			= convert_T_ypeID_to_internal_type_reference_LibraryID tr_type_name tr_module_name2 tr_library2 dl_client_state io;
			
		// check type definitions
		# (type_tables,dl_client_state)
			= get_type_tables dl_client_state;
		# (ets,dl_client_state)
			= get_ets dl_client_state;

		# (equivalent_type_defs,type_tables,ets)
			= equal_type_defs rt_type_reference1 rt_type_reference2 type_tables ets;
			
		# (ets_proven_type_equivalences,ets)
			= ets!ets_proven_type_equivalences;
		
		# dl_client_state
			= { dl_client_state & 
				cs_type_tables = type_tables
			,	cs_intra_type_equalities = ets
			 };

		| library_instance_i1 == library_instance_i2
			= (equivalent_type_defs,equivalent_types,dl_client_state,io);

		// print result
		# type1 = tr_module_name1 +++ toString rt_type_reference1;
		# type2 = tr_module_name2 +++ toString rt_type_reference2;

		#! (dl_client_state)
			= AddDebugMessage (tr_type_name +++ ": " +++ type1 +++ 
					(if equivalent_type_defs " == " " <> ")
					+++ type2 ) dl_client_state;

		# equivalent_type
			= (convert_to_library_instance_type_reference library_instance_i1 rt_type_reference1,
			   convert_to_library_instance_type_reference library_instance_i2 rt_type_reference2);
		= (equivalent_type_defs,[equivalent_type:equivalent_types],dl_client_state,io);
		
	check_type_pair _ s
		= s;		
};

// Conversion of {LibraryID,Int} to LibRef/TypeTableTypeReference
convert_to_library_instance_type_reference :: !LibRef !TypeTableTypeReference -> LibraryInstanceTypeReference;
convert_to_library_instance_type_reference lib_ref  (TypeTableTypeReference type_table_i tio_type_ref)
	= LIT_TypeReference lib_ref tio_type_ref;

convert_T_ypeID_to_internal_type_reference_LibraryID tr_type_name tr_module_name tr_library dl_client_state io
	# (library_instance_i,dl_client_state)
		= GetLibraryInstanceIndex tr_library dl_client_state;
	= convert_T_ypeID_to_internal_type_reference_Int tr_type_name tr_module_name library_instance_i dl_client_state io;

convert_T_ypeID_to_internal_type_reference_Int :: !String !String !Int !*DLClientState !*f -> *(LibRef,!TypeTableTypeReference,*DLClientState,*f) | FileEnv f;
convert_T_ypeID_to_internal_type_reference_Int tr_type_name tr_module_name library_instance_i dl_client_state io
	# (type_table_i,library_instance_i,dl_client_state,io)
		= case (LLI_IS_MAIN_LIBRARY_INSTANCE library_instance_i) of {
			True
				# (type_table_i,dl_client_state)
					= dl_client_state!cs_library_instances.lis_library_instances.[library_instance_i].li_type_table_i;
				-> (type_table_i,LibRef library_instance_i,dl_client_state,io);
			_
				-> abort "convert_T_ypeID_to_internal_type_reference_Int; internal error";						
		};

	# (type_tables,dl_client_state)
		= get_type_tables dl_client_state;
		
	# (maybe_tio_type_reference,type_tables)
		= findTypeUsingTypeName tr_type_name tr_module_name type_table_i type_tables;
		
	# dl_client_state
		= { dl_client_state & 
			cs_type_tables = type_tables
		};

	# q 
		= TypeTableTypeReference type_table_i (fromJust maybe_tio_type_reference);
	= (library_instance_i,q,dl_client_state,io);
where {
	lookup_defining_module type_table_i tis_string_table tio_common_def_i dl_client_state
		# (module_name_index,dl_client_state)
			= dl_client_state!cs_type_tables.[type_table_i].tt_tio_common_defs.[tio_common_def_i].tio_module;
		# module_name
			= get_name_from_string_table module_name_index tis_string_table;
		| module_name <> tr_module_name
			= (Nothing,dl_client_state);
			
			# (tio_com_type_defs,dl_client_state)
				= dl_client_state!cs_type_tables.[type_table_i].tt_tio_common_defs.[tio_common_def_i].tio_com_type_defs;
			# maybe_type_name
				= findAi lookup_type_name tio_com_type_defs;
			| isNothing maybe_type_name
				= abort "create_type_reference: interal error; defining module not found";
			= (maybe_type_name,dl_client_state)
	where {
		lookup_type_name tio_com_type_def_i {tio_td_name}
			# type_name
				= get_name_from_string_table tio_td_name tis_string_table;
			| type_name <> tr_type_name
				= Nothing;
				
			# rt_type_reference
				= { default_elem &
					tio_tr_module_n		= tio_common_def_i
				,	tio_tr_type_def_n	= tio_com_type_def_i
				}
			| True
			= Just rt_type_reference;
	};
};

class GetLibraryInstanceIndex a :: a !*DLClientState -> (!Int,!*DLClientState);

instance GetLibraryInstanceIndex LibraryID
where {
	GetLibraryInstanceIndex (Address address) dl_client_state
		= GetLibraryInstanceIndex address dl_client_state;
	GetLibraryInstanceIndex (Number library_instance_i) dl_client_state
		= (library_instance_i,dl_client_state);
};
	
instance GetLibraryInstanceIndex Int
where {
	GetLibraryInstanceIndex address dl_client_state
		# (lis_n_library_instances,dl_client_state)
			= dl_client_state!cs_library_instances.lis_n_library_instances

		# (result,dl_client_state)
			= findAst find_library_instance dl_client_state lis_n_library_instances;
		| isJust result
			= (fromJust result,dl_client_state);
			= abort ("GetLibraryInstanceIndex Int; unknown address: " +++ toString address);
	where {
		find_library_instance library_instance_i dl_client_state
			#! (li_memory_areas,dl_client_state)
				= dl_client_state!cs_library_instances.lis_library_instances.[library_instance_i].li_memory_areas;
			#! li_memory_areas
				= filter (\{ma_begin,ma_end} -> between ma_begin address ma_end) li_memory_areas;
			| isEmpty li_memory_areas
				= (Nothing,dl_client_state);
				= (Just library_instance_i,dl_client_state);
	}
};