implementation module check_types;

import StdEnv;

// Linker
import DLState;
import CollectTypes;
import link_library_instance;
import pdObjectToMem;

// StdDynamicEnv
from DynamicLinkerInterface import ::TypeReference(..), ::LazyDynamicReference(..), ::LibraryID(..), ::RunTimeIDW(..)
	, instance EnDecode RunTimeIDW, instance EnDecode LazyDynamicReference, instance EnDecode TypeReference
	, instance DefaultElem RunTimeIDW, instance DefaultElem LazyDynamicReference, instance DefaultElem TypeReference;
import EnDecode;

// Compiler
import utilities;

// StdDynamicEnv
from DynamicLinkerInterface import ::TypeReference(..), ::LibraryID(..);

// Extended env
import ExtArray;
import DebugUtilities;
import ExtInt;

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;
	| F "CheckTypeDefinitions" not client_exists
		= internal_error "CheckTypeDefinitions (internal error): client not registered" client_id dl_client_state s io;

	# l
		= decode ( arg /* { c \\ c <-: arg}*/ );


	#! (dl_client_state)
		= AddMessage (Verbose ("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
				# (dl_client_state,io)
					= foldSt generate_type_equations equivalent_type_defs (dl_client_state,io);

				// 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)
			= AddMessage (Verbose (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;
		
	generate_type_equations (LIT_TypeReference lr_left tio_type_ref_left,LIT_TypeReference lr_right tio_type_ref_right) (dl_client_state,io)
		// get types table for left and right types of the above tuple
		# (type_table_left_i,dl_client_state)
			= extractTypeTable_i lr_left dl_client_state;
		# (type_table_right_i,dl_client_state)
			= extractTypeTable_i lr_right dl_client_state;

		// collect types
		# type_left
			= TypeTableTypeReference type_table_left_i tio_type_ref_left;
		# type_right
			= TypeTableTypeReference type_table_right_i tio_type_ref_right;
			
		# (type_tables,dl_client_state)
			= get_type_tables dl_client_state;
		# (cts=:{cts_type_dependencies,cts_type_tables=type_tables})
			= collect_types type_left type_right {default_collect_types_state & cts_type_tables = type_tables};
		# dl_client_state
			= { dl_client_state &
				cs_type_tables = type_tables
			};	
			
		# (dl_client_state,io)
			= foldSt add_type_implementation cts_type_dependencies (dl_client_state,io);
		= (dl_client_state,io);
		where {
			// TIO_TypeReference
			add_type_implementation (tio_type_ref_left,tio_type_ref_right) (dl_client_state,io)
				# left_library_instance_type_ref
					= LIT_TypeReference lr_left tio_type_ref_left;
				# right_library_instance_type_ref
					= LIT_TypeReference lr_right tio_type_ref_right;
					
				# (_,dl_client_state,io)
					= old_enter_type_equation left_library_instance_type_ref right_library_instance_type_ref dl_client_state io;
				= (dl_client_state,io);			
		}; //isTypeWithoutDefinition
};

// 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);
			_
				| IS_COLLECT_AND_RENUMBER_EXTERNAL_TYPE_REFERENCES
					#! (lib_ref=:(LazyLibRef ith_type_redirection lazy_dynamic_i type_table_i))
						= decode_lib_ref library_instance_i;
					-> (type_table_i,lib_ref,dl_client_state,io);

					// A lazy reference has been detected. Such a reference consists of:
					// - lazy dynamic index
					// - lazy library instance index
					# lazy_dynamic_index
						= LLI_EXTRACT_LAZY_DYNAMIC_INDEX library_instance_i;
					# lazy_library_instance_index
						= LLI_EXTRACT_LAZY_LIBRARY_INSTANCE_INDEX library_instance_i;
						
					# (maybe_initialized_lazy_dynamic,dl_client_state)
						= dl_client_state!cs_lazy_dynamic_index_to_dynamic_id.[lazy_dynamic_index];
					# maybe_initialized_lazy_dynamic
						= maybe_initialized_lazy_dynamic.ldi_lazy_dynamic_index_to_dynamic;
					| isJust maybe_initialized_lazy_dynamic
						// the dynamic refered to by the lazy reference has been initialized, so the
						// lazy reference can be dereferenced.
						# lazy_dynamic_i
							= fromJust maybe_initialized_lazy_dynamic;
						# (library_instance_i,dl_client_state)
							= dl_client_state!cs_dynamic_info.[lazy_dynamic_i].di_disk_id_to_library_instance_i.[lazy_library_instance_index];
							
						// DynamicInfo
						# (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);

						// uninitialized lazy dynamic
						// Using the index of the main dynamic which contains the lazy dynamic, the library
						// The main dynamic index is the index of the dynamic containing the
						// lazy dynamic.
						# (Just (disk_lazy_dynamic_index,main_dynamic_index),dl_client_state)
							= get_dynamic_id lazy_dynamic_index dl_client_state;
						# (library_instance_kind,dl_client_state)
							= dl_client_state!cs_dynamic_info.[main_dynamic_index].di_library_instance_to_library_index.[lazy_library_instance_index];
						# (library_name,dl_client_state)
							= case library_instance_kind of {
								LIK_LazyLibraryInstance {LIK_LazyLibraryInstance | lik_index_in_di_library_index_to_library_name=library_name_index}
									# (library_name,dl_client_state)
										= dl_client_state!cs_dynamic_info.[main_dynamic_index].di_library_index_to_library_name.[library_name_index];
									-> (library_name,dl_client_state);
								_
									// The current *lazy* type reference should refer to entry in the
									// library instance table reflecting this fact.
									-> abort "create_type_reference: internal error";
							};
	
						// allocate & load required type table
						# (type_table_i,dl_client_state)
							= AddReferenceToTypeTable library_name dl_client_state;
						# (dl_client_state,io)
							= LoadTypeTable type_table_i dl_client_state io;
						
						# lib_ref_via_lazy_dynamic
							= LibRefViaLazyDynamic lazy_library_instance_index lazy_dynamic_index type_table_i
						-> (type_table_i,lib_ref_via_lazy_dynamic,dl_client_state,io);
							
		};

	// ensure required type table is loaded
	# (dl_client_state,io)
		= case library_instance_i of {
			(LibRef library_instance_i)
				-> initialize_predefined_type_equations library_instance_i dl_client_state io;
			_
				-> (dl_client_state,io);
		};
		
	# (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
				}
			| F ("****************" +++ type_name +++ " - " +++ toString type_table_i +++ " - " +++ toString tio_common_def_i +++ " - " +++ toString 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);
	}
};