definition module TypeImplementationTable;

import type_io_read;
import StdMaybe;

:: *TypeImplementationTable
	= {
		teit_n_type_implementations		:: !Int
	,	teit_type_implementations_a		:: !*{#TypeImplementation}
	};
	
default_type_implementation_table :: !*TypeImplementationTable;
			
:: TypeImplementation
	= {
		tei_type_implementations		:: [LibraryInstanceTypeReference]
	,	tei_chosen_type_implementation	:: !Maybe !LibraryInstanceTypeReference
	};

:: TypeImplementationReference :== Int;

create_type_equivalent_class type1 type2 tit :== enter_type_equation type1 type2 tit;

class enter_type_equation s :: LibraryInstanceTypeReference LibraryInstanceTypeReference !*s -> (Maybe (!TypeImplementationReference,!Bool),!*s);

instance enter_type_equation TypeImplementationTable;

// Type equivalence classes
class enter_implementation_type_for_equivalence_class s :: !TypeImplementationReference !Int !*s -> !*s;
instance enter_implementation_type_for_equivalence_class TypeImplementationTable;

class enter_implementation_type_for_equivalence_class2 s :: !TypeImplementationReference !LibraryInstanceTypeReference !*s -> !*s;
instance enter_implementation_type_for_equivalence_class2 TypeImplementationTable;

// Accessors
class findImplementationType s :: !LibraryInstanceTypeReference !*s -> (!Bool,!Maybe !TypeImplementationReference,!*s);

instance findImplementationType TypeImplementationTable;

class get_type_implementation s :: !Int !*s -> (!TypeImplementation,!*s);

instance get_type_implementation TypeImplementationTable;

class getImplementationType s :: !TypeImplementationReference !*s -> *(Maybe LibraryInstanceTypeReference,*s);
instance getImplementationType TypeImplementationTable;

// A set of *lazy* type equations are directly inserted in the type implementation table. These types may
// not be implemented i.e. linked already!
//add_lazy_type_equations :: !.Int [.LibraryInstanceTypeReference] !*TypeImplementationTable -> *TypeImplementationTable;
class add_lazy_type_equations s :: !.Int [.LibraryInstanceTypeReference] !*s -> *s;

instance add_lazy_type_equations TypeImplementationTable;

find_TypeImplementationTable :: (Int -> .(TypeImplementation -> .(.a -> (Maybe b,.a)))) !*TypeImplementationTable .a -> *(Maybe b,*(*TypeImplementationTable,.a));

class set_type_equations s :: !.Int [.LibraryInstanceTypeReference] !*s -> *s;

instance set_type_equations TypeImplementationTable;