check.icl

implementation module check

import StdEnv

import syntax, typesupport, parse, checksupport, utilities, checktypes, transform, predef
import explicitimports, comparedefimp, checkFunctionBodies, containers, portToNewSyntax

cPredefinedModuleIndex 	:== 1
cUndef :== (-1)
cDummyArray :== {}

isMainModule :: ModuleKind -> Bool
isMainModule MK_Main	= True
isMainModule _ 			= False

// AA..
checkGenerics :: !Index !Index !*{#GenericDef} !*{#ClassDef} !*{#CheckedTypeDef} !*{#DclModule} !*TypeHeaps !*CheckState
	-> (!*{#GenericDef}, !*{#ClassDef}, !*{#CheckedTypeDef}, !*{#DclModule}, !*TypeHeaps, !*CheckState)
checkGenerics 
		gen_index module_index generic_defs class_defs type_defs modules 
		type_heaps=:{th_vars} 
		cs=:{cs_symbol_table, cs_error}
	| gen_index == size generic_defs
		= (generic_defs, class_defs, type_defs, modules, type_heaps, cs)
	// otherwise
		# (generic_def=:{gen_name, gen_type, gen_pos}, generic_defs) = generic_defs![gen_index]
		# position = newPosition gen_name gen_pos
		# cs_error = setErrorAdmin position cs_error
			//---> ("checkGenerics generic type 1", gen_type.gt_type)

		// add * for kind-star instances and *->* for arrays
		# kinds = 
			[	KindConst
			, 	KindArrow [KindConst, KindConst]
			]
		# (kinds_ptr, th_vars) = newPtr (TVI_Kinds kinds) th_vars
		# (cons_ptr, th_vars) = newPtr (TVI_Empty) th_vars

		# cs = {cs & cs_error = cs_error, cs_symbol_table = cs_symbol_table }
		# type_heaps = {type_heaps & th_vars = th_vars}

		# (gt_type, type_defs, class_defs, modules, type_heaps, cs) =
			checkMemberType module_index gen_type.gt_type type_defs class_defs modules type_heaps cs

		#! {cs_error} = cs
		#! (gt_vars, st_vars, cs_error) = split_vars gen_type.gt_vars  gt_type.st_vars cs_error
		#! cs = {cs & cs_error = cs_error}
		#! gt_type = {gt_type & st_vars = st_vars}

		# generic_def =
			{	generic_def &
				gen_type = { gen_type & gt_vars = gt_vars, gt_type = gt_type }
			,	gen_kinds_ptr = kinds_ptr
			, 	gen_cons_ptr = cons_ptr
			}

		# generic_defs = {generic_defs & [gen_index] = generic_def}				
			//---> ("checkGenerics generic type 2", gt_type)
		= checkGenerics (inc gen_index) module_index generic_defs class_defs type_defs modules type_heaps cs
where	
	split_vars [] st_vars error
		= ([], st_vars, error)
	split_vars [gv:gvs] st_vars error
		# (gv, st_vars, error) = find gv st_vars error
		# (gvs, st_vars, error) = split_vars gvs st_vars error
		= ([gv:gvs], st_vars, error) 
	where
		find gv [] error = (gv, [], checkError gv.tv_name.id_name "generic variable not used" error)
		find gv	[st_var:st_vars] error
			| st_var.tv_name.id_name == gv.tv_name.id_name
				= (st_var, st_vars, error)
				# (gv, st_vars, error) = find gv st_vars error 
				= (gv, [st_var:st_vars], error)
				

checkTypeClasses :: !Index !Index !*{#ClassDef} !*{#MemberDef} !*{#CheckedTypeDef} !*{#DclModule} !*TypeHeaps !*CheckState
	-> (!*{#ClassDef}, !*{#MemberDef}, !*{#CheckedTypeDef}, !*{#DclModule}, !*TypeHeaps, !*CheckState)
checkTypeClasses class_index module_index class_defs member_defs type_defs modules type_heaps cs=:{cs_symbol_table,cs_error}
	| class_index == size class_defs
		= (class_defs, member_defs, type_defs, modules, type_heaps, cs)
		# (class_def=:{class_name,class_pos,class_args,class_context,class_members}, class_defs) = class_defs![class_index]
		  cs = {cs & cs_error = setErrorAdmin (newPosition class_name class_pos) cs_error }
		  (class_args, class_context, type_defs, class_defs, modules, type_heaps, cs)
		  		= checkSuperClasses class_args class_context module_index type_defs class_defs modules type_heaps cs
		  class_defs = { class_defs & [class_index] = { class_def & class_context = class_context, class_args = class_args }}
		  member_defs = set_classes_in_member_defs 0 class_members {glob_object = class_index, glob_module = module_index} member_defs 
		= checkTypeClasses (inc class_index) module_index class_defs member_defs type_defs modules type_heaps cs
where
	set_classes_in_member_defs mem_offset class_members glob_class_index member_defs
		| mem_offset == size class_members
			= member_defs
			# {ds_index} = class_members.[mem_offset]
			# (member_def, member_defs) = member_defs![ds_index]
			= set_classes_in_member_defs (inc mem_offset) class_members glob_class_index { member_defs & [ds_index] = { member_def & me_class = glob_class_index }}

checkSpecial :: !Index !FunType !Index !SpecialSubstitution (!Index, ![FunType], !*Heaps, !*ErrorAdmin)
	-> (!Special, (!Index, ![FunType], !*Heaps, !*ErrorAdmin))
checkSpecial mod_index fun_type=:{ft_type} fun_index subst (next_inst_index, special_types, heaps, error)
	# (special_type, hp_type_heaps, error) = substitute_type ft_type subst heaps.hp_type_heaps error
	  (spec_types, error) = checkAndCollectTypesOfContexts special_type.st_context error
	  ft_type = { special_type & st_context = [] }
	  (new_info_ptr, hp_var_heap) = newPtr VI_Empty heaps.hp_var_heap
	= ( { spec_index = { glob_module = mod_index, glob_object = next_inst_index }, spec_types = spec_types, spec_vars = subst.ss_vars, spec_attrs = subst.ss_attrs },
			((inc next_inst_index), [{ fun_type & ft_type = ft_type, ft_specials = SP_FunIndex fun_index, ft_type_ptr = new_info_ptr} : special_types ],
					{ heaps & hp_type_heaps = hp_type_heaps, hp_var_heap = hp_var_heap }, error))
where	
	substitute_type st=:{st_vars,st_attr_vars,st_args,st_result,st_context,st_attr_env} environment type_heaps error
		# (st_vars, st_attr_vars, [st_result : st_args], st_context, st_attr_env, _, type_heaps, Yes error)
			= instantiateTypes st_vars st_attr_vars [ st_result : st_args ] st_context st_attr_env environment [] type_heaps (Yes error)
		= ({st & st_vars = st_vars, st_args = st_args, st_result = st_result, st_attr_vars = st_attr_vars,
			st_context = st_context, st_attr_env = st_attr_env }, type_heaps, error)

checkDclFunctions :: !Index !Index ![FunType] !v:{#CheckedTypeDef} !x:{#ClassDef} !v:{#.DclModule} !*Heaps !*CheckState
	-> (!Index, ![FunType], ![FunType], !v:{#CheckedTypeDef}, !x:{#ClassDef}, !v:{#DclModule}, !*Heaps, !*CheckState)
checkDclFunctions module_index first_inst_index fun_types type_defs class_defs modules heaps cs
	= check_dcl_functions module_index fun_types 0 first_inst_index [] [] type_defs class_defs modules heaps cs
where
	check_dcl_functions ::  !Index ![FunType]   !Index  !Index ![FunType] ![FunType] !v:{#CheckedTypeDef} !x:{#ClassDef} !v:{#DclModule} !*Heaps !*CheckState
		 -> (!Index, ![FunType], ![FunType],!v:{#CheckedTypeDef}, !x:{#ClassDef}, !v:{#DclModule}, !*Heaps, !*CheckState)
	check_dcl_functions module_index [] fun_index next_inst_index collected_funtypes collected_instances type_defs class_defs modules heaps cs
		= (next_inst_index, collected_funtypes, collected_instances, type_defs, class_defs, modules, heaps, cs)
	check_dcl_functions module_index [fun_type=:{ft_symb,ft_type,ft_pos,ft_specials} : fun_types] fun_index
			next_inst_index collected_funtypes collected_instances type_defs class_defs modules heaps cs
		# position = newPosition ft_symb ft_pos
		  cs = { cs & cs_error = setErrorAdmin position cs.cs_error }
		  (ft_type, ft_specials, type_defs,  class_defs, modules, hp_type_heaps, cs)
		  		= checkFunctionType module_index ft_type ft_specials type_defs class_defs modules heaps.hp_type_heaps cs
		  (spec_types, next_inst_index, collected_instances, heaps, cs_error)
		  		= check_specials module_index { fun_type & ft_type = ft_type } fun_index ft_specials next_inst_index collected_instances
		  				{ heaps & hp_type_heaps = hp_type_heaps } cs.cs_error
		  (new_info_ptr, hp_var_heap) = newPtr VI_Empty heaps.hp_var_heap
		= check_dcl_functions module_index fun_types (inc fun_index) next_inst_index [
				{ fun_type & ft_type = ft_type, ft_specials = spec_types, ft_type_ptr = new_info_ptr } : collected_funtypes]
					collected_instances type_defs class_defs modules { heaps & hp_var_heap = hp_var_heap } { cs & cs_error = cs_error }

	check_specials :: !Index !FunType !Index !Specials !Index ![FunType] !*Heaps !*ErrorAdmin
		-> (!Specials, !Index, ![FunType], !*Heaps, !*ErrorAdmin)
	check_specials mod_index fun_type fun_index (SP_Substitutions substs) next_inst_index all_instances heaps error
		# (list_of_specials, (next_inst_index, all_instances, heaps, cs_error))
				= mapSt (checkSpecial mod_index fun_type fun_index) substs (next_inst_index, all_instances, heaps, error)
		= (SP_ContextTypes list_of_specials, next_inst_index, all_instances, heaps, cs_error)
	check_specials mod_index fun_type fun_index SP_None next_inst_index all_instances heaps error
		= (SP_None, next_inst_index, all_instances, heaps, error)


checkSpecialsOfInstances :: !Index !Index ![ClassInstance] !Index ![ClassInstance] ![FunType] {# FunType} *{! [Special] } !*Heaps !*ErrorAdmin
		-> (!Index, ![ClassInstance], ![FunType], !*{! [Special]}, !*Heaps, !*ErrorAdmin)
checkSpecialsOfInstances mod_index first_mem_index [class_inst=:{ins_members,ins_specials} : class_insts] next_inst_index all_class_instances all_specials
		new_inst_defs all_spec_types heaps error
	= case ins_specials of
		SP_TypeOffset type_offset
			# (next_inst_index, rev_mem_specials, all_specials, all_spec_types, heaps, error)
				= check_and_build_members mod_index first_mem_index 0 ins_members type_offset next_inst_index [] all_specials new_inst_defs all_spec_types heaps error
			  class_inst = { class_inst & ins_members = { mem \\ mem <- reverse rev_mem_specials } }
			-> checkSpecialsOfInstances mod_index first_mem_index class_insts next_inst_index [class_inst : all_class_instances]
					all_specials new_inst_defs all_spec_types heaps error
		SP_None
			-> checkSpecialsOfInstances mod_index first_mem_index class_insts next_inst_index [class_inst : all_class_instances]
					all_specials new_inst_defs all_spec_types heaps error
where
	check_and_build_members :: !Index !Index !Int {# DefinedSymbol} !Int !Index ![DefinedSymbol] ![FunType] !{#FunType} !*{! [Special]} !*Heaps !*ErrorAdmin
		-> (!Index, ![DefinedSymbol], ![FunType], !*{! [Special]}, !*Heaps, !*ErrorAdmin)
	check_and_build_members mod_index first_mem_index member_offset ins_members type_offset next_inst_index rev_mem_specials all_specials inst_spec_defs
			all_spec_types heaps error
		| member_offset < size ins_members
			# member = ins_members.[member_offset]
			  member_index = member.ds_index
			  spec_member_index = member_index - first_mem_index
		 	# (spec_types, all_spec_types) = all_spec_types![spec_member_index]
		 	# mem_inst = inst_spec_defs.[spec_member_index]
		 	  (SP_Substitutions specials) = mem_inst.ft_specials
		 	  env = specials !! type_offset
			  member = { member & ds_index = next_inst_index }
			  (spec_type, (next_inst_index, all_specials, heaps, error))
			  		= checkSpecial mod_index mem_inst member_index env (next_inst_index, all_specials, heaps, error)
			  all_spec_types = { all_spec_types & [spec_member_index] = [ spec_type : spec_types] }
			= check_and_build_members mod_index first_mem_index (inc member_offset) ins_members type_offset next_inst_index [ member : rev_mem_specials ]
					all_specials inst_spec_defs all_spec_types heaps error
			= (next_inst_index, rev_mem_specials, all_specials, all_spec_types, heaps, error)

checkSpecialsOfInstances mod_index first_mem_index [] next_inst_index all_class_instances all_specials inst_spec_defs all_spec_types heaps error
	= (next_inst_index, all_class_instances, all_specials, all_spec_types, heaps, error)	

checkMemberTypes :: !Index !*{#MemberDef} !*{#CheckedTypeDef} !*{#ClassDef} !*{#DclModule} !*TypeHeaps !*VarHeap !*CheckState
	-> (!*{#MemberDef}, !*{#CheckedTypeDef}, !*{#ClassDef}, !*{#DclModule}, !*TypeHeaps,  !*VarHeap, !*CheckState)
checkMemberTypes module_index member_defs type_defs class_defs modules type_heaps var_heap cs
	#! nr_of_members = size member_defs
	= iFoldSt (check_class_member module_index) 0 nr_of_members (member_defs, type_defs, class_defs, modules, type_heaps, var_heap, cs)
where
	check_class_member module_index member_index (member_defs, type_defs, class_defs, modules, type_heaps, var_heap, cs)
		# (member_def=:{me_symb,me_type,me_pos}, member_defs) = member_defs![member_index]
		  position = newPosition me_symb me_pos
		  cs = { cs & cs_error = setErrorAdmin position cs.cs_error }
		  (me_type, type_defs, class_defs, modules, type_heaps, cs)
		   		= checkMemberType module_index me_type type_defs class_defs modules type_heaps cs
		  me_class_vars = [ type_var \\ (TV type_var) <- (hd me_type.st_context).tc_types ]
		  (me_type_ptr, var_heap) = newPtr VI_Empty var_heap		   
		= ({ member_defs & [member_index] = { member_def & me_type = me_type, me_class_vars = me_class_vars, me_type_ptr = me_type_ptr }},
				type_defs, class_defs, modules, type_heaps, var_heap, cs)
	
::	InstanceSymbols =
	{	is_type_defs		:: !.{# CheckedTypeDef}
	,	is_class_defs		:: !.{# ClassDef}
	,	is_member_defs		:: !.{# MemberDef}
	, 	is_generic_defs		:: !.{# GenericDef} // AA
	,	is_modules			:: !.{# DclModule}
	}

// AA..
checkInstanceDefs :: !Index !*{#ClassInstance} !u:{#CheckedTypeDef} !u:{#ClassDef} !u:{#MemberDef} /*AA*/!u:{#GenericDef} !u:{#DclModule} !*TypeHeaps !*CheckState
	-> (!.{#ClassInstance},!u:{#CheckedTypeDef},!u:{#ClassDef},!u:{#MemberDef}, /*AA*/!u:{#GenericDef}, !u:{#DclModule},!.TypeHeaps,!.CheckState)
checkInstanceDefs mod_index instance_defs type_defs class_defs member_defs generic_defs modules type_heaps cs
	# is = { is_type_defs = type_defs, is_class_defs = class_defs, is_member_defs = member_defs, /*AA*/is_generic_defs = generic_defs, is_modules = modules }
	  (instance_defs, is, type_heaps, cs) = check_instance_defs 0 mod_index instance_defs is type_heaps cs
	= (instance_defs, is.is_type_defs, is.is_class_defs, is.is_member_defs, /*AA*/is.is_generic_defs, is.is_modules, type_heaps, cs)
where
	check_instance_defs :: !Index !Index !*{# ClassInstance} !u:InstanceSymbols !*TypeHeaps !*CheckState
		-> (!*{# ClassInstance},!u:InstanceSymbols,!*TypeHeaps,!*CheckState)
	check_instance_defs inst_index mod_index instance_defs is type_heaps cs
		| inst_index < size instance_defs
			# (instance_def, instance_defs) = instance_defs![inst_index]
			  (instance_def, is, type_heaps, cs) = check_instance mod_index instance_def is type_heaps cs
			= check_instance_defs (inc inst_index) mod_index { instance_defs & [inst_index] = instance_def } is type_heaps cs
			= (instance_defs, is, type_heaps, cs)
			
	check_instance :: !Index !ClassInstance !u:InstanceSymbols !*TypeHeaps !*CheckState -> (!ClassInstance, !u:InstanceSymbols, !*TypeHeaps, !*CheckState)
	check_instance module_index
			ins=:{ins_members,ins_class={glob_object = class_name =: {ds_ident = {id_name,id_info},ds_arity}},ins_type,ins_specials,ins_pos,ins_ident}
			is=:{is_class_defs,is_generic_defs, is_modules} type_heaps cs=:{cs_symbol_table}
		#  	(entry, cs_symbol_table) = readPtr id_info cs_symbol_table
		# 	cs = pushErrorAdmin (newPosition ins_ident ins_pos) { cs & cs_symbol_table = cs_symbol_table }
		#   (ins, is, type_heaps, cs) = case entry.ste_kind of
				STE_Class				
					# (class_def, is) = class_by_index entry.ste_index is
					-> check_class_instance	class_def module_index entry.ste_index module_index ins is type_heaps cs 
				STE_Imported STE_Class decl_index	
					# (class_def, is) = class_by_module_index decl_index entry.ste_index is
					-> check_class_instance class_def module_index entry.ste_index decl_index ins is type_heaps cs
				STE_Generic 
					# (generic_def, is) = generic_by_index entry.ste_index is
					-> check_generic_instance generic_def module_index entry.ste_index module_index ins is type_heaps cs
				STE_Imported STE_Generic decl_index	
					# (gen_def, is) = generic_by_module_index decl_index entry.ste_index is
					-> check_generic_instance gen_def module_index entry.ste_index decl_index ins is type_heaps cs
				ste -> (ins, is, type_heaps, { cs & cs_error = checkError id_name "class or generic undefined" cs.cs_error })
		= (ins, is, type_heaps, popErrorAdmin cs)

	where
			class_by_index class_index is=:{is_class_defs}
				#	(class_def, is_class_defs) = is_class_defs![class_index]
 				= (class_def, {is & is_class_defs = is_class_defs})
			class_by_module_index decl_index class_index is=:{is_modules}
 				# 	(dcl_mod, is_modules) = is_modules![decl_index]
					class_def = dcl_mod.dcl_common.com_class_defs.[class_index]
				= (class_def, {is & is_modules = is_modules })
			generic_by_index gen_index is=:{is_generic_defs}
				# 	(gen_def, is_generic_defs) = is_generic_defs![gen_index]
				= (gen_def, {is & is_generic_defs = is_generic_defs})
			generic_by_module_index decl_index gen_index is=:{is_modules}	
 				# 	(dcl_mod, is_modules) = is_modules![decl_index]
					gen_def = dcl_mod.dcl_common.com_generic_defs.[gen_index]
				= (gen_def, {is & is_modules = is_modules })
				
	check_class_instance :: ClassDef !Index !Index !Index !ClassInstance !u:InstanceSymbols !*TypeHeaps !*CheckState 
		-> (!ClassInstance, !u:InstanceSymbols, !*TypeHeaps, !*CheckState)
	check_class_instance class_def module_index class_index class_mod_index
			ins=:{ins_members,ins_class={glob_object = class_name =: {ds_ident = {id_name,id_info},ds_arity}},ins_type,ins_specials,ins_pos,ins_ident,ins_generate}
			is=:{is_class_defs,is_modules} type_heaps cs=:{cs_symbol_table}	
		| ins_generate
			= ( ins
			  , is
			  , type_heaps
			  , { cs & cs_error = checkError id_name "cannot generate class instance" cs.cs_error }
			  )
		| class_def.class_arity == ds_arity
			# ins_class = { glob_object = { class_name & ds_index = class_index }, glob_module = class_mod_index}
			  (ins_type, ins_specials, is_type_defs, is_class_defs, is_modules, type_heaps, cs)
			  		= checkInstanceType module_index ins_class ins_type ins_specials
							is.is_type_defs is.is_class_defs is.is_modules type_heaps cs
			  is = { is & is_type_defs = is_type_defs, is_class_defs = is_class_defs, is_modules = is_modules }
			= ({ins & ins_class = ins_class, ins_type = ins_type, ins_specials = ins_specials}, is, type_heaps, cs)
		// otherwise
			= ( ins
			  , is
			  , type_heaps
			  , { cs & cs_error = checkError id_name ("wrong arity: expected "+++toString class_def.class_arity+++" found "+++toString ds_arity) cs.cs_error }
			  )
	check_generic_instance :: GenericDef !Index !Index !Index !ClassInstance !u:InstanceSymbols !*TypeHeaps !*CheckState -> (!ClassInstance, !u:InstanceSymbols, !*TypeHeaps, !*CheckState)
	check_generic_instance 
			class_def module_index generic_index generic_module_index
			ins=:{
				ins_members,
				ins_class={glob_object = class_name =: {ds_ident = {id_name,id_info},ds_arity, ds_index} },
				ins_type,
				ins_specials,
				ins_pos,
				ins_ident, 
				ins_is_generic}
			is=:{is_class_defs,is_modules} 
			type_heaps 
			cs=:{cs_symbol_table, cs_error}
		# class_name = {class_name & ds_index = generic_index}	
		# ins_class = { glob_object = class_name, glob_module = generic_module_index}
		| ds_arity == 1
			# (ins_type, ins_specials, is_type_defs, is_class_defs, is_modules, type_heaps, cs)
			  = checkInstanceType module_index ins_class ins_type ins_specials
							is.is_type_defs is.is_class_defs is.is_modules type_heaps cs
			# is = { is & is_type_defs = is_type_defs, is_class_defs = is_class_defs, is_modules = is_modules }		 
			# ins = { ins & 
				ins_is_generic = True,
				ins_generic = {glob_module = module_index, glob_object = generic_index}, 
				ins_class = ins_class, 
				ins_type = ins_type, 
				ins_specials = ins_specials 
				}  
			= (ins, is, type_heaps, cs)
		// otherwise
			# cs_error = checkError id_name "arity of generic instance must be 1" cs_error 
			# cs = {cs & cs_error = cs_error}
			= (ins, is, type_heaps, cs)
						 
checkInstances :: !Index !*CommonDefs !u:{# DclModule} !*VarHeap !*TypeHeaps !*CheckState
	-> (![(Index,SymbolType)], !*CommonDefs, !u:{# DclModule}, !*VarHeap , !*TypeHeaps, !*CheckState)
checkInstances mod_index icl_common=:{com_instance_defs,com_class_defs,com_member_defs,com_generic_defs,com_type_defs} modules var_heap type_heaps cs=:{cs_error}
	| cs_error.ea_ok
		# (instance_types, com_instance_defs, com_class_defs, com_member_defs, com_generic_defs, com_type_defs, modules, var_heap, type_heaps, cs)
				= check_instances 0 mod_index [] com_instance_defs com_class_defs com_member_defs /*AA*/com_generic_defs com_type_defs modules var_heap type_heaps cs
		= (instance_types, { icl_common & com_instance_defs = com_instance_defs,com_class_defs = com_class_defs,com_member_defs = com_member_defs, /*AA*/com_generic_defs = com_generic_defs, com_type_defs = com_type_defs },
			 	modules, var_heap, type_heaps, cs)
		= ([], icl_common, modules, var_heap, type_heaps, cs)
where
	check_instances :: !Index !Index ![(Index,SymbolType)] !x:{# ClassInstance} !w:{# ClassDef} !v:{# MemberDef} /*AA*/!w:{# GenericDef} !nerd:{# CheckedTypeDef} !u:{# DclModule}
		!*VarHeap !*TypeHeaps !*CheckState
			-> (![(Index,SymbolType)], !x:{# ClassInstance}, !w:{# ClassDef}, !v:{# MemberDef}, /*AA*/!w:{# GenericDef}, !nerd:{# CheckedTypeDef}, !u:{# DclModule}, !*VarHeap, !*TypeHeaps, !*CheckState)
	check_instances inst_index mod_index instance_types instance_defs class_defs member_defs generic_defs type_defs modules var_heap type_heaps cs
// AA..
		| inst_index < size instance_defs
			# (instance_def=:{ins_ident,ins_is_generic, ins_pos}, instance_defs) = instance_defs![inst_index]
			# (instance_types, class_defs, member_defs, generic_defs, type_defs, modules, var_heap, type_heaps, cs) =
				(if ins_is_generic check_generic_instance check_class_instance)  
					instance_def mod_index instance_types class_defs member_defs generic_defs type_defs modules var_heap type_heaps cs				 
			= check_instances (inc inst_index) mod_index instance_types instance_defs class_defs member_defs generic_defs type_defs modules var_heap type_heaps cs 
		// otherwise
			= (instance_types, instance_defs, class_defs, member_defs, generic_defs, type_defs, modules, var_heap, type_heaps, cs)
													
	check_class_instance {ins_pos,ins_class,ins_members,ins_type} mod_index instance_types class_defs member_defs generic_defs type_defs modules var_heap type_heaps cs
			# ({class_members,class_name}, class_defs, modules) = getClassDef ins_class mod_index class_defs modules
			  class_size = size class_members
			| class_size == size ins_members
				# (instance_types, member_defs, type_defs, modules, var_heap, type_heaps, cs) 
						= check_member_instances mod_index ins_class.glob_module
			  	        	 0 class_size ins_members class_members class_name ins_pos ins_type instance_types member_defs type_defs modules var_heap type_heaps cs
				= (instance_types, class_defs, member_defs, generic_defs, type_defs, modules, var_heap, type_heaps, cs)
			// otherwise
				# cs = { cs & cs_error = checkError class_name "different number of members specified" cs.cs_error }
				= (instance_types, class_defs, member_defs, generic_defs, type_defs, modules, var_heap, type_heaps, cs)
	
	check_generic_instance {ins_class, ins_members, ins_generate} mod_index instance_types class_defs member_defs generic_defs type_defs modules var_heap type_heaps cs
			# ({gen_name, gen_member_name}, generic_defs, modules) = getGenericDef ins_class mod_index generic_defs modules		
			| ins_generate 
				= (instance_types, class_defs, member_defs, generic_defs, type_defs, modules, var_heap, type_heaps, cs)				
			| size ins_members <> 1 				
				# cs = { cs & cs_error = checkError gen_name "generic instance must have one memeber" cs.cs_error }
				= (instance_types, class_defs, member_defs, generic_defs, type_defs, modules, var_heap, type_heaps, cs)
			# member_name = ins_members.[0].ds_ident
			| member_name <> gen_member_name
				# cs = { cs & cs_error = checkError member_name "wrong member name" cs.cs_error }
				= (instance_types, class_defs, member_defs, generic_defs, type_defs, modules, var_heap, type_heaps, cs)				
			// otherwise
				= (instance_types, class_defs, member_defs, generic_defs, type_defs, modules, var_heap, type_heaps, cs)
// ..AA

	check_member_instances :: !Index !Index !Int !Int !{#DefinedSymbol} !{#DefinedSymbol} Ident !Position !InstanceType ![(Index,SymbolType)]
		!v:{# MemberDef} !blah:{# CheckedTypeDef} !u:{# DclModule} !*VarHeap !*TypeHeaps !*CheckState
			-> (![(Index,SymbolType)], !v:{# MemberDef}, !blah:{# CheckedTypeDef}, !u:{# DclModule},!*VarHeap, !*TypeHeaps, !*CheckState)

	check_member_instances module_index member_mod_index mem_offset class_size ins_members class_members
				class_name ins_pos ins_type instance_types member_defs type_defs modules var_heap type_heaps cs=:{cs_x={x_main_dcl_module_n}}
		| mem_offset == class_size
			= (instance_types, member_defs, type_defs, modules, var_heap, type_heaps, cs)
			# ins_member = ins_members.[mem_offset]
			  class_member = class_members.[mem_offset]
			| ins_member.ds_ident <> class_member.ds_ident
				= check_member_instances module_index member_mod_index (inc mem_offset) class_size ins_members class_members class_name ins_pos ins_type 
						instance_types member_defs type_defs modules var_heap type_heaps
							{ cs & cs_error = checkError class_member.ds_ident "instance of class member expected" cs.cs_error}
			| ins_member.ds_arity <> class_member.ds_arity
				= check_member_instances module_index member_mod_index (inc mem_offset) class_size ins_members class_members class_name ins_pos ins_type
						instance_types member_defs type_defs modules var_heap type_heaps
							{ cs & cs_error = checkError class_member.ds_ident "used with wrong arity" cs.cs_error}
				# ({me_symb, me_type,me_class_vars,me_pos}, member_defs, modules) = getMemberDef member_mod_index class_member.ds_index module_index member_defs modules
				  cs_error = pushErrorAdmin (newPosition class_name ins_pos) cs.cs_error
				  (instance_type, _, type_heaps, Yes (modules, type_defs), Yes cs_error)
				  		= determineTypeOfMemberInstance me_type me_class_vars ins_type SP_None type_heaps (Yes (modules, type_defs, x_main_dcl_module_n)) (Yes cs_error)
				  (type_defs, modules, cs_error) = checkTopLevelKinds x_main_dcl_module_n True me_symb instance_type type_defs modules cs_error
				  cs_error = popErrorAdmin cs_error
				  (st_context, var_heap) = initializeContextVariables instance_type.st_context var_heap
				= check_member_instances module_index member_mod_index (inc mem_offset) class_size ins_members class_members class_name ins_pos ins_type
						[ (ins_member.ds_index, { instance_type & st_context = st_context }) : instance_types ] member_defs type_defs modules var_heap type_heaps { cs & cs_error = cs_error }


getClassDef :: !(Global DefinedSymbol) !Int !u:{#ClassDef} !v:{#DclModule} -> (!ClassDef,!u:{#ClassDef},!v:{#DclModule})
getClassDef {glob_module, glob_object={ds_ident, ds_index}} mod_index class_defs modules
	| glob_module == mod_index
		# (class_def, class_defs) = class_defs![ds_index]
		= (class_def, class_defs, modules)
		# (dcl_mod, modules) = modules![glob_module]
		= (dcl_mod.dcl_common.com_class_defs.[ds_index], class_defs, modules)
		
getMemberDef :: !Int Int !Int !u:{#MemberDef} !v:{#DclModule} -> (!MemberDef,!u:{#MemberDef},!v:{#DclModule})
getMemberDef mem_mod mem_index mod_index member_defs modules
	| mem_mod == mod_index
		# (member_def,member_defs) = member_defs![mem_index]
		= (member_def, member_defs, modules)
		# (dcl_mod,modules) = modules![mem_mod]
		= (dcl_mod.dcl_common.com_member_defs.[mem_index], member_defs, modules)

// AA..
getGenericDef :: !(Global DefinedSymbol) !Int !u:{#GenericDef} !v:{#DclModule} -> (!GenericDef,!u:{#GenericDef},!v:{#DclModule})
getGenericDef {glob_module, glob_object={ds_ident, ds_index}} mod_index generic_defs modules
	| glob_module == mod_index
		# (generic_def, generic_defs) = generic_defs![ds_index]
		= (generic_def, generic_defs, modules)
		# (dcl_mod, modules) = modules![glob_module]
		= (dcl_mod.dcl_common.com_generic_defs.[ds_index], generic_defs, modules)
// ..AA

instantiateTypes :: ![TypeVar] ![AttributeVar] !types ![TypeContext] ![AttrInequality] !SpecialSubstitution ![SpecialSubstitution] !*TypeHeaps !(Optional *ErrorAdmin)
	-> (![TypeVar], ![AttributeVar], !types , ![TypeContext], ![AttrInequality], ![SpecialSubstitution], !*TypeHeaps, !(Optional *ErrorAdmin)) | substitute types
instantiateTypes old_type_vars old_attr_vars types type_contexts attr_env {ss_environ, ss_vars, ss_attrs, ss_context} special_subst_list type_heaps=:{th_vars, th_attrs} opt_error
	# th_vars = clear_vars old_type_vars th_vars

	  (new_type_vars, th_vars) = foldSt build_var_subst ss_vars ([], th_vars)
	  (new_attr_vars, th_attrs) = foldSt build_attr_subst ss_attrs ([], th_attrs)

	  type_heaps = foldSt build_type_subst ss_environ { type_heaps & th_vars = th_vars, th_attrs = th_attrs }
	  (ok1, new_ss_context, type_heaps) = substitute ss_context type_heaps

	  (inst_vars, th_vars) =  foldSt determine_free_var old_type_vars (new_type_vars, type_heaps.th_vars) 
	  (inst_attr_vars, th_attrs) = foldSt build_attr_subst old_attr_vars (new_attr_vars, type_heaps.th_attrs)

	  (ok2, inst_types, type_heaps)		= substitute types { type_heaps & th_vars = th_vars, th_attrs = th_attrs }
	  (ok3, inst_contexts, type_heaps)	= substitute type_contexts type_heaps
	  (ok4, inst_attr_env, type_heaps)	= substitute attr_env type_heaps
	  (special_subst_list, th_vars) =  mapSt adjust_special_subst special_subst_list type_heaps.th_vars
	
	  opt_error = case ok1 && ok2 && ok3 && ok4 of
	  				True -> opt_error
	  				_ -> case opt_error of
	  						No -> No
	  						Yes error_admin
	  							-> Yes (checkError "instance type incompatible with class type" "" 
	  										error_admin)
	  								// e.g.:class c a :: (a Int); instance c Real

	= (inst_vars, inst_attr_vars, inst_types, inst_contexts ++ new_ss_context, inst_attr_env, special_subst_list, { type_heaps & th_vars = th_vars }, opt_error)
where
	clear_vars type_vars type_var_heap = foldSt (\tv -> writePtr tv.tv_info_ptr TVI_Empty) type_vars type_var_heap
	
	determine_free_var tv=:{tv_info_ptr} (free_vars, type_var_heap)
		# (type_var_info, type_var_heap) = readPtr tv_info_ptr type_var_heap
		= case type_var_info of
			TVI_Empty
				-> build_var_subst tv (free_vars, type_var_heap)
			_
				-> (free_vars, type_var_heap)

	build_type_subst {bind_src,bind_dst} type_heaps
		# (_, bind_src, type_heaps) = substitute bind_src type_heaps
		= { type_heaps & th_vars = writePtr bind_dst.tv_info_ptr (TVI_Type bind_src) type_heaps.th_vars}

	build_var_subst var (free_vars, type_var_heap)
		# (new_info_ptr, type_var_heap) = newPtr TVI_Empty type_var_heap
		  new_fv = { var & tv_info_ptr = new_info_ptr}
	  	= ([ new_fv : free_vars ], writePtr var.tv_info_ptr (TVI_Type (TV new_fv)) type_var_heap)

	build_attr_subst attr (free_attrs, attr_var_heap)
		# (new_info_ptr, attr_var_heap) = newPtr AVI_Empty attr_var_heap
		  new_attr = { attr & av_info_ptr = new_info_ptr}
		= ([new_attr : free_attrs], writePtr attr.av_info_ptr (AVI_Attr (TA_Var new_attr)) attr_var_heap)
	
	adjust_special_subst special_subst=:{ss_environ} type_var_heap
		# (ss_environ, type_var_heap) = mapSt adjust_special_bind ss_environ type_var_heap
		= ({ special_subst & ss_environ = ss_environ }, type_var_heap)
		
	adjust_special_bind bind=:{bind_dst={tv_info_ptr}} type_var_heap
		# (TVI_Type (TV new_tv), type_var_heap) = readPtr tv_info_ptr type_var_heap
		= ({ bind & bind_dst = new_tv }, type_var_heap)

substituteInstanceType :: !InstanceType !SpecialSubstitution !*TypeHeaps !*ErrorAdmin -> (!InstanceType,!*TypeHeaps,!.ErrorAdmin)
substituteInstanceType it=:{it_vars,it_attr_vars,it_types,it_context} environment type_heaps cs_error
	# (it_vars, it_attr_vars, it_types, it_context, _, _, type_heaps, Yes cs_error)
		= instantiateTypes it_vars it_attr_vars it_types it_context [] environment [] type_heaps (Yes cs_error)
	= ({it & it_vars = it_vars, it_types = it_types, it_attr_vars = it_attr_vars, it_context = it_context }, type_heaps, cs_error)

hasTypeVariables []
	= False
hasTypeVariables [TV tvar : types]
	= True
hasTypeVariables [ _ : types]
	= hasTypeVariables types

determineTypeOfMemberInstance :: !SymbolType ![TypeVar] !InstanceType !Specials !*TypeHeaps !u:(Optional (v:{#DclModule}, w:{#CheckedTypeDef}, Index)) !(Optional *ErrorAdmin)
		-> (!SymbolType, !Specials, !*TypeHeaps, !u:Optional (v:{#DclModule}, w:{#CheckedTypeDef}), !Optional *ErrorAdmin)
determineTypeOfMemberInstance mem_st class_vars {it_types,it_vars,it_attr_vars,it_context} specials type_heaps opt_modules opt_error
	# env = { ss_environ = foldl2 (\binds var type -> [ {bind_src = type, bind_dst = var} : binds]) [] class_vars it_types,
			  ss_context = it_context, ss_vars = it_vars, ss_attrs = it_attr_vars} 
	  (st, specials, type_heaps, opt_error)
	  		= determine_type_of_member_instance mem_st env specials type_heaps opt_error
	  (type_heaps, opt_modules, opt_error)
	  		= check_attribution_consistency mem_st type_heaps opt_modules opt_error
	= (st, specials, type_heaps, opt_modules, opt_error)
where
	determine_type_of_member_instance mem_st=:{st_context} env (SP_Substitutions substs) type_heaps opt_error
		# (mem_st, substs, type_heaps, opt_error) 
				= substitute_symbol_type { mem_st &  st_context = tl st_context } env substs type_heaps opt_error
		= (mem_st, SP_Substitutions substs, type_heaps, opt_error) 
	determine_type_of_member_instance mem_st=:{st_context} env SP_None type_heaps opt_error
		# (mem_st, _, type_heaps, opt_error)
				= substitute_symbol_type { mem_st &  st_context = tl st_context } env [] type_heaps opt_error
		= (mem_st, SP_None, type_heaps, opt_error)

	substitute_symbol_type st=:{st_vars,st_attr_vars,st_args,st_result,st_context,st_attr_env} environment specials type_heaps opt_error
		# (st_vars, st_attr_vars, [st_result : st_args], st_context, st_attr_env, specials, type_heaps, opt_error)
			= instantiateTypes st_vars st_attr_vars [ st_result : st_args ] st_context st_attr_env environment specials type_heaps opt_error
		= ({st & st_vars = st_vars, st_args = st_args, st_result = st_result, st_attr_vars = st_attr_vars,
			st_context = st_context, st_attr_env = st_attr_env }, specials, type_heaps, opt_error)

	check_attribution_consistency {st_args, st_result} type_heaps No No
		= (type_heaps, No, No)
	check_attribution_consistency {st_args, st_result} type_heaps=:{th_vars} (Yes (modules, type_defs, x_main_dcl_module_n)) (Yes error)
		// it is assumed that all type vars bindings done in instantiateTypes are still valid
		# (_, th_vars, modules, type_defs, error)
				= foldSt (foldATypeSt (check_it x_main_dcl_module_n) (\_ st -> st))
						[st_result:st_args]
						(False, th_vars, modules, type_defs, error)
		= ({ type_heaps & th_vars = th_vars }, Yes (modules, type_defs), Yes error)
	
	check_it _ {at_attribute} (error_already_given, th_vars, modules, type_defs, error)
		| at_attribute==TA_Unique || error_already_given
			= (error_already_given, th_vars, modules, type_defs, error)
		// otherwise GOTO next alternative
	check_it x_main_dcl_module_n {at_type=TV tv} (_, th_vars, modules, type_defs, error)
  		= must_not_be_essentially_unique x_main_dcl_module_n tv th_vars modules type_defs error
	check_it x_main_dcl_module_n {at_type= (CV tv) :@: _} (_, th_vars, modules, type_defs, error)
  		= must_not_be_essentially_unique x_main_dcl_module_n tv th_vars modules type_defs error
	check_it _ _ state
		= state
		
	must_not_be_essentially_unique x_main_dcl_module_n {tv_name, tv_info_ptr} th_vars modules type_defs error
		# (TVI_Type type, th_vars)
				= readPtr tv_info_ptr th_vars
		= case type of
			TA {type_name, type_index} _
				# (type_def, type_defs, modules)
						= getTypeDef x_main_dcl_module_n type_index type_defs modules
				-> case type_def.td_attribute of
					TA_Unique
						-> (True, th_vars, modules, type_defs,
							checkError type_name 
								(   "is unique but instanciates class variable "
								 +++tv_name.id_name
								 +++" that is non uniquely used in a member type"
								) error
						   )
					_
						-> (False, th_vars, modules, type_defs, error)
			_
				-> (False, th_vars, modules, type_defs, error)

getTypeDef :: !Index !(Global Index) !v:{#CheckedTypeDef} !w:{#DclModule}
		-> (!CheckedTypeDef, !v:{#CheckedTypeDef}, !w:{#DclModule})
getTypeDef x_main_dcl_module_n {glob_module,glob_object} type_defs modules
	| glob_module==x_main_dcl_module_n
		# (type_def, type_defs)
				= type_defs![glob_object]
		= (type_def, type_defs, modules)
	# (type_def, modules)
			= modules![glob_module].dcl_common.com_type_defs.[glob_object]
	= (type_def, type_defs, modules)
		
determineTypesOfInstances :: !Index !Index !*{#ClassInstance} !*{# ClassDef} !*{# MemberDef}
							 !*{#DclModule} !*TypeHeaps !*VarHeap !*CheckState
	-> (![FunType], !Index, ![ClassInstance], !*{#ClassInstance}, !*{# ClassDef}, !*{# MemberDef}, !*{#DclModule}, !*TypeHeaps, !*VarHeap, !*CheckState)
determineTypesOfInstances first_memb_inst_index mod_index com_instance_defs com_class_defs com_member_defs
		modules type_heaps var_heap cs=:{cs_error, cs_x={x_main_dcl_module_n}}
	| cs_error.ea_ok
		#! nr_of_class_instances = size com_instance_defs
		# (memb_inst_defs, next_mem_inst_index, all_class_specials, com_class_defs, com_member_defs, modules, com_instance_defs, type_heaps, var_heap, cs_error)
				= determine_types_of_instances x_main_dcl_module_n 0 nr_of_class_instances first_memb_inst_index mod_index [] com_class_defs com_member_defs
						modules com_instance_defs type_heaps var_heap cs_error
		= (memb_inst_defs, next_mem_inst_index, all_class_specials, com_instance_defs, com_class_defs,
		   com_member_defs, modules, type_heaps, var_heap, { cs & cs_error = cs_error })
		= ([], first_memb_inst_index, [], com_instance_defs, com_class_defs, com_member_defs, modules, type_heaps, var_heap, cs)
where

	determine_types_of_instances :: !Index !Index !Index !Index !Index ![ClassInstance] !v:{#ClassDef} !w:{#MemberDef}
		!x:{#DclModule} !*{#ClassInstance} !*TypeHeaps !*VarHeap !*ErrorAdmin
			-> (![FunType], !Index, ![ClassInstance], !v:{#ClassDef}, !w:{#MemberDef}, !x:{#DclModule}, !*{#ClassInstance}, !*TypeHeaps, !*VarHeap, !*ErrorAdmin)
	determine_types_of_instances x_main_dcl_module_n inst_index next_class_inst_index next_mem_inst_index mod_index all_class_specials
			class_defs member_defs modules instance_defs type_heaps var_heap error
		| inst_index < size instance_defs
			# (instance_def, instance_defs) = instance_defs![inst_index]
			# {ins_class,ins_pos,ins_type,ins_specials} = instance_def
			  ({class_name, class_members}, class_defs, modules) = getClassDef ins_class mod_index class_defs modules
			  class_size = size class_members
			  (ins_members, memb_inst_defs1, member_defs, modules, type_heaps, var_heap, error)
			  		= determine_instance_symbols_and_types x_main_dcl_module_n next_mem_inst_index 0 mod_index ins_class.glob_module class_size class_members
			  				ins_type ins_specials class_name ins_pos member_defs modules type_heaps var_heap error
			  instance_def = { instance_def & ins_members = { member \\ member <- ins_members }}
			  (ins_specials, next_class_inst_index, all_class_specials, type_heaps, error)
					= check_instance_specials mod_index instance_def inst_index ins_specials next_class_inst_index all_class_specials type_heaps error
			  (memb_inst_defs2, next_mem_inst_index, all_class_specials, class_defs, member_defs, modules, instance_defs, type_heaps, var_heap, error)
			  		= determine_types_of_instances x_main_dcl_module_n (inc inst_index) next_class_inst_index (next_mem_inst_index + class_size) mod_index all_class_specials
			  				class_defs member_defs modules { instance_defs & [inst_index] = { instance_def & ins_specials = ins_specials }} type_heaps var_heap error

			= (memb_inst_defs1 ++ memb_inst_defs2, next_mem_inst_index, all_class_specials, class_defs, member_defs, modules, instance_defs, type_heaps, var_heap, error)
			= ([], next_mem_inst_index, all_class_specials, class_defs, member_defs, modules, instance_defs, type_heaps, var_heap, error)

	determine_instance_symbols_and_types :: !Index !Index !Index !Index !Index !Int !{#DefinedSymbol} !InstanceType !Specials Ident !Position
			!w:{#MemberDef} !u:{#DclModule} !*TypeHeaps !*VarHeap !*ErrorAdmin
					-> (![DefinedSymbol], ![FunType], !w:{#MemberDef}, !u:{#DclModule}, !*TypeHeaps, !*VarHeap, !.ErrorAdmin)
	determine_instance_symbols_and_types x_main_dcl_module_n first_inst_index mem_offset module_index member_mod_index class_size class_members
			ins_type ins_specials class_name ins_pos member_defs modules type_heaps var_heap cs_error
		| mem_offset == class_size
			=  ([], [], member_defs, modules, type_heaps, var_heap, cs_error)
			# class_member = class_members.[mem_offset]
			  ({me_symb,me_type,me_priority,me_class_vars}, member_defs, modules) = getMemberDef member_mod_index class_member.ds_index module_index member_defs modules
			  cs_error
			  		= pushErrorAdmin (newPosition class_name ins_pos) cs_error
			  (instance_type, new_ins_specials, type_heaps, Yes (modules, _), Yes cs_error)
			  		= determineTypeOfMemberInstance me_type me_class_vars ins_type ins_specials type_heaps (Yes (modules, {}, cUndef)) (Yes cs_error)
			  (_, modules, cs_error) = checkTopLevelKinds x_main_dcl_module_n False me_symb instance_type cDummyArray modules cs_error
			  cs_error
			  		= popErrorAdmin cs_error
			  (new_info_ptr, var_heap) = newPtr VI_Empty var_heap
			  inst_def = MakeNewFunctionType me_symb me_type.st_arity me_priority instance_type ins_pos new_ins_specials new_info_ptr
			  (inst_symbols, memb_inst_defs, member_defs, modules, type_heaps, var_heap, cs_error)
			  		= determine_instance_symbols_and_types x_main_dcl_module_n first_inst_index (inc mem_offset) module_index member_mod_index
			  				class_size class_members ins_type ins_specials class_name ins_pos member_defs modules type_heaps var_heap cs_error
			= ([{ class_member & ds_index = first_inst_index +  mem_offset } : inst_symbols], [inst_def : memb_inst_defs], member_defs, modules, type_heaps, var_heap, cs_error)

	check_instance_specials :: !Index !ClassInstance !Index !Specials !Index ![ClassInstance] !*TypeHeaps !*ErrorAdmin
		-> (!Specials, !Index, ![ClassInstance], !*TypeHeaps, !*ErrorAdmin)
	check_instance_specials mod_index inst_type inst_index (SP_Substitutions substs) next_inst_index all_instances type_heaps error
		# (list_of_specials, next_inst_index, all_instances, type_heaps, error)
			= check_specials mod_index inst_type 0 substs [] next_inst_index all_instances type_heaps error
		= (SP_ContextTypes list_of_specials, next_inst_index, all_instances, type_heaps, error)
	where
		check_specials mod_index inst=:{ins_type} type_offset [ subst : substs ] list_of_specials next_inst_index all_instances type_heaps error
			# (special_type, type_heaps, error) = substituteInstanceType ins_type subst type_heaps error
			  (spec_types, error) = checkAndCollectTypesOfContexts special_type.it_context error
			  special = { spec_index = { glob_module = mod_index, glob_object = next_inst_index }, spec_types = spec_types,
			  				spec_vars = subst.ss_vars, spec_attrs = subst.ss_attrs }
			= check_specials mod_index inst (inc type_offset) substs [ special : list_of_specials ] (inc next_inst_index)
					[{ inst & ins_type = { special_type & it_context = [] }, ins_specials = SP_TypeOffset type_offset} : all_instances ] type_heaps error
		check_specials mod_index inst=:{ins_type} type_offset [] list_of_specials next_inst_index all_instances type_heaps error
			= (list_of_specials,  next_inst_index, all_instances, type_heaps, error)
	
	check_instance_specials mod_index fun_type fun_index SP_None next_inst_index all_instances type_heaps error
		= (SP_None, next_inst_index, all_instances, type_heaps, error)

checkAndCollectTypesOfContexts type_contexts error
	= mapSt check_and_collect_context_types type_contexts error
where	
	check_and_collect_context_types {tc_class={glob_object={ds_ident}},tc_types} error
		| hasTypeVariables tc_types
			= (tc_types, checkError ds_ident.id_name "illegal specialization" error)
			= (tc_types, error)


checkTopLevelKinds :: !Index !Bool Ident !SymbolType n:{# CheckedTypeDef} !r:{# DclModule} !*ErrorAdmin
					-> (!n:{# CheckedTypeDef}, !r:{# DclModule}, !*ErrorAdmin)
checkTopLevelKinds x_main_dcl_module_n is_icl_module me_symb st=:{st_args, st_result} type_defs modules cs_error
	#! first_wrong = firstIndex (\{at_type} -> not (kind_is_ok x_main_dcl_module_n is_icl_module type_defs modules 0 at_type)) [st_result:st_args]
	# cs_error
	  		= case first_wrong of
	  			(-1)
	  				-> cs_error
	  			_ 
	  				-> checkError "instance type has wrong kind" 
	  				  			(   "(e.g. "
	  				  			 +++arg_string first_wrong
	  				  			 +++" of member "
	  				  			 +++toString me_symb
	  				  			 +++")"
	  				  			) 
	  				  			cs_error
= (type_defs, modules, cs_error)
  where
	kind_is_ok x_main_dcl_module_n is_icl_module type_defs modules demanded_kind type=:(TA {type_index={glob_object,glob_module}} args)
		# {td_arity}
				= if (glob_module==x_main_dcl_module_n && is_icl_module) type_defs.[glob_object]
				     modules.[glob_module].dcl_common.com_type_defs.[glob_object]
		= demanded_kind == td_arity-length args
	kind_is_ok _ _ _ modules 0 (_ --> _)
		= True
	kind_is_ok _ _ _ modules _ (_ :@: _)
		= True
	kind_is_ok _ _ _ _ 0 (TB _)
		= True
	kind_is_ok _ _ _ _ _ (GTV _)
		= True
	kind_is_ok _ _ _ _ _ (TV _)
		= True
	kind_is_ok _ _ _ _ _ (TQV _)
		= True
	kind_is_ok _ _ _ _ _ _
		= False
		


consOptional (Yes thing) things
	= [ thing : things]
consOptional No things
	= things



initializeContextVariables :: ![TypeContext] !*VarHeap ->  (![TypeContext], !*VarHeap)
initializeContextVariables contexts var_heap
	= mapSt add_variable_to_context contexts var_heap
where
	add_variable_to_context context var_heap
		# (new_info_ptr, var_heap) = newPtr VI_Empty var_heap
		= ({ context & tc_var = new_info_ptr}, var_heap)

checkFunction :: !Index !Index !Level !*{#FunDef} !*ExpressionInfo !*Heaps !*CheckState -> (!*{#FunDef},!*ExpressionInfo, !*Heaps, !*CheckState);
checkFunction mod_index fun_index def_level fun_defs
			e_info=:{ef_type_defs,ef_modules,ef_class_defs,ef_is_macro_fun} heaps=:{hp_var_heap,hp_expression_heap,hp_type_heaps} cs=:{cs_error}
	# (fun_def,fun_defs) = fun_defs![fun_index]
	# {fun_symb,fun_pos,fun_body,fun_type,fun_kind} = fun_def
	  cs = { cs & cs_error = push_error_admin_beautifully fun_symb fun_pos fun_kind cs_error }
	  (fun_type, ef_type_defs, ef_class_defs, ef_modules, hp_var_heap, hp_type_heaps, cs)
			= check_function_type fun_type mod_index ef_type_defs ef_class_defs ef_modules hp_var_heap hp_type_heaps cs
	  e_info  = { e_info & ef_type_defs = ef_type_defs, ef_class_defs = ef_class_defs, ef_modules = ef_modules }
	  e_state = {   es_var_heap = hp_var_heap, es_expr_heap = hp_expression_heap, es_type_heaps = hp_type_heaps,
	  				es_dynamics = [], es_calls = [], es_fun_defs = fun_defs, es_dynamic_expr_count = 0}
	  e_input = { ei_expr_level = inc def_level, ei_fun_index = fun_index, ei_fun_level = inc def_level, ei_mod_index = mod_index }
	  (fun_body, free_vars, e_state, e_info, cs) = checkFunctionBodies fun_body e_input e_state e_info cs

	# {es_fun_defs,es_calls,es_var_heap,es_expr_heap,es_type_heaps,es_dynamics} = e_state
	  (ef_type_defs, ef_modules, es_type_heaps, es_expr_heap, cs) = 
	  	checkDynamicTypes mod_index es_dynamics fun_type e_info.ef_type_defs e_info.ef_modules es_type_heaps es_expr_heap cs
	  cs = { cs & cs_error = popErrorAdmin cs.cs_error }
	  fi_properties = (if ef_is_macro_fun FI_IsMacroFun 0) bitor (has_type fun_type)
	  fun_info = { fun_def.fun_info & fi_calls = es_calls, fi_def_level = def_level, fi_free_vars = free_vars, fi_dynamics = es_dynamics,
	  								  fi_properties = fi_properties }
	  fun_defs = { es_fun_defs & [fun_index] = { fun_def & fun_body = fun_body, fun_index = fun_index, fun_info = fun_info, fun_type = fun_type}}
	  (fun_defs, cs_symbol_table) = remove_calls_from_symbol_table fun_index def_level es_calls fun_defs cs.cs_symbol_table
	= (fun_defs,
			{ e_info & ef_type_defs = ef_type_defs, ef_modules = ef_modules },
			{ heaps & hp_var_heap = es_var_heap, hp_expression_heap = es_expr_heap, hp_type_heaps = es_type_heaps }, 
			{ cs & cs_symbol_table = cs_symbol_table })

where
	has_type (Yes _) 	= FI_HasTypeSpec
	has_type no 		= 0
	
	check_function_type (Yes ft) module_index type_defs class_defs modules var_heap type_heaps cs
		# (ft, _, type_defs, class_defs, modules, type_heaps, cs) = checkFunctionType module_index ft SP_None type_defs class_defs modules type_heaps cs
		  (st_context, var_heap) = initializeContextVariables ft.st_context var_heap
		= (Yes { ft & st_context = st_context } , type_defs,  class_defs, modules, var_heap, type_heaps, cs)

	check_function_type No module_index type_defs class_defs modules var_heap type_heaps cs
		= (No, type_defs,  class_defs, modules, var_heap, type_heaps, cs)

	remove_calls_from_symbol_table fun_index fun_level [{fc_index, fc_level} : fun_calls] fun_defs symbol_table
		| fc_level <= fun_level
			# ({fun_symb=fun_symb=:{id_info}}, fun_defs) = fun_defs![fc_index]
			# (entry, symbol_table) = readPtr id_info symbol_table
			# (c,cs) = get_calls entry.ste_kind 
			| fun_index == c
				= remove_calls_from_symbol_table fun_index fun_level fun_calls fun_defs (symbol_table <:= (id_info,{ entry & ste_kind = STE_FunctionOrMacro cs}))
				= abort " Error in remove_calls_from_symbol_table"
			= remove_calls_from_symbol_table fun_index fun_level fun_calls fun_defs symbol_table
	remove_calls_from_symbol_table fun_index fun_level [] fun_defs symbol_table
		= (fun_defs, symbol_table)

	get_calls (STE_FunctionOrMacro [x:xs]) = (x,xs)
	get_calls ste_kind = abort "get_calls (check.icl)" // <<- ste_kind

	push_error_admin_beautifully {id_name} fun_pos (FK_ImpFunction fun_name_is_location_dependent) cs_error
		| fun_name_is_location_dependent && size id_name>0
			# beautiful_name = if (id_name.[0]==backslash) "lambda" "comprehension"
			= pushErrorAdmin (newPosition { id_name=beautiful_name, id_info=nilPtr } fun_pos) cs_error
	push_error_admin_beautifully {id_name} fun_pos (FK_DefFunction fun_name_is_location_dependent) cs_error
		| fun_name_is_location_dependent && size id_name>0
			# beautiful_name = if (id_name.[0]==backslash) "lambda" "comprehension"
			= pushErrorAdmin (newPosition { id_name=beautiful_name, id_info=nilPtr } fun_pos) cs_error
	push_error_admin_beautifully fun_symb fun_pos _ cs_error
		= pushErrorAdmin (newPosition fun_symb fun_pos) cs_error

checkFunctions :: !Index !Level !Index !Index !*{#FunDef} !*ExpressionInfo !*Heaps !*CheckState -> (!*{#FunDef}, !*ExpressionInfo, !*Heaps, !*CheckState)
checkFunctions mod_index level from_index to_index fun_defs e_info heaps cs
	| from_index == to_index
		= (fun_defs, e_info, heaps, cs)
		# (fun_defs, e_info, heaps, cs) = checkFunction mod_index from_index level fun_defs e_info heaps cs
		= checkFunctions mod_index level (inc from_index) to_index fun_defs e_info heaps cs

checkMacros ::  !Index !IndexRange !*{#FunDef} !*ExpressionInfo !*Heaps !*CheckState
	-> (!*{#FunDef}, !*ExpressionInfo, !*Heaps, !*CheckState);
checkMacros mod_index range fun_defs e_info=:{ef_is_macro_fun=ef_is_macro_fun_old} heaps cs
	# (fun_defs, e_info, heaps=:{hp_var_heap, hp_expression_heap}, cs=:{cs_symbol_table, cs_predef_symbols, cs_error})
			= checkFunctions mod_index cGlobalScope range.ir_from range.ir_to fun_defs { e_info & ef_is_macro_fun=True } heaps cs
	  (e_info=:{ef_modules}) = { e_info & ef_is_macro_fun=ef_is_macro_fun_old }
	  (pds_alias_dummy, cs_predef_symbols) = cs_predef_symbols![PD_DummyForStrictAliasFun]
	  (fun_defs, ef_modules, hp_var_heap, hp_expression_heap, cs_symbol_table, cs_error)
	  		= partitionateMacros range mod_index pds_alias_dummy fun_defs ef_modules hp_var_heap hp_expression_heap cs_symbol_table cs_error
	= (fun_defs, { e_info & ef_modules = ef_modules }, {heaps &  hp_var_heap = hp_var_heap, hp_expression_heap = hp_expression_heap},
			{ cs & cs_symbol_table = cs_symbol_table, cs_predef_symbols = cs_predef_symbols, cs_error = cs_error })

checkInstanceBodies :: !IndexRange !*{#FunDef} !*ExpressionInfo !*Heaps !*CheckState -> (!*{#FunDef},!*ExpressionInfo,!*Heaps, !*CheckState);
checkInstanceBodies {ir_from, ir_to} fun_defs e_info heaps cs=:{cs_x}
	= checkFunctions cs_x.x_main_dcl_module_n cGlobalScope ir_from ir_to fun_defs e_info heaps cs

instance < FunDef 
where
	(<) fd1 fd2 = fd1.fun_symb.id_name < fd2.fun_symb.id_name

createCommonDefinitions {def_types,def_constructors,def_selectors,def_macros,def_classes,def_members,def_instances, def_generics}
	=	{	com_type_defs		= { type \\ type <- def_types }
	
		,	com_unexpanded_type_defs = {}

		,	com_cons_defs		= { cons \\ cons <- def_constructors }
		,	com_selector_defs	= { sel \\ sel <- def_selectors }
		,	com_class_defs		= { class_def \\ class_def <- def_classes }
		,	com_member_defs		= { member \\ member <- def_members }
		,	com_instance_defs	= { next_instance \\ next_instance <- def_instances }
		,	com_generic_defs	= { gen \\ gen <- def_generics }		
		}

array_plus_list a [] = a
array_plus_list a l = arrayPlusList a l

checkCommonDefinitions :: !Bool !Index !*CommonDefs !*{# DclModule} !*TypeHeaps !*VarHeap !*CheckState
	-> (!*CommonDefs, !*{# DclModule}, !*TypeHeaps,  !*VarHeap, !*CheckState)
checkCommonDefinitions is_dcl module_index common modules type_heaps var_heap cs
	#! is_main_dcl_mod = is_dcl && module_index == cs.cs_x.x_main_dcl_module_n
	# (com_type_defs, com_cons_defs, com_selector_defs, modules, var_heap, type_heaps, cs)
			= checkTypeDefs is_dcl is_main_dcl_mod common.com_type_defs module_index
							common.com_cons_defs common.com_selector_defs modules var_heap type_heaps cs
	  (com_class_defs, com_member_defs, com_type_defs, modules, type_heaps, cs)
	  		= checkTypeClasses 0 module_index common.com_class_defs common.com_member_defs com_type_defs modules type_heaps cs
	  (com_member_defs, com_type_defs, com_class_defs, modules, type_heaps, var_heap, cs)
	  		= checkMemberTypes module_index com_member_defs com_type_defs com_class_defs modules type_heaps var_heap cs
// AA..
	  (com_generic_defs, com_class_defs, com_type_defs, modules, type_heaps, cs)
			= checkGenerics 0 module_index common.com_generic_defs com_class_defs com_type_defs modules type_heaps cs
// ..AA
	  (com_instance_defs, com_type_defs, com_class_defs, com_member_defs, /*AA*/com_generic_defs, modules, type_heaps, cs)
	  		= checkInstanceDefs module_index common.com_instance_defs com_type_defs com_class_defs com_member_defs /*AA*/com_generic_defs modules type_heaps cs
	
	  (size_com_type_defs,com_type_defs) = usize com_type_defs
	  (size_com_selector_defs,com_selector_defs) = usize com_selector_defs
	  (size_com_cons_defs,com_cons_defs) = usize com_cons_defs

	  (com_class_defs, modules, new_type_defs, new_selector_defs, new_cons_defs, th_vars, var_heap, cs)
	  	= createClassDictionaries module_index com_class_defs modules size_com_type_defs size_com_selector_defs size_com_cons_defs
	  		type_heaps.th_vars var_heap cs

	  com_type_defs = array_plus_list com_type_defs new_type_defs
	  com_selector_defs = array_plus_list com_selector_defs new_selector_defs
	  com_cons_defs = array_plus_list com_cons_defs new_cons_defs

	= ({common & com_type_defs = com_type_defs, com_cons_defs = com_cons_defs, com_selector_defs = com_selector_defs, com_class_defs = com_class_defs,
			com_member_defs = com_member_defs,  com_instance_defs = com_instance_defs, /* AA */ com_generic_defs = com_generic_defs }, modules, { type_heaps & th_vars = th_vars }, var_heap, cs)

collectCommonfinitions :: !(CollectedDefinitions ClassInstance a) -> (!*{# Int}, ![Declaration])
collectCommonfinitions {def_types,def_constructors,def_selectors,def_macros,def_classes,def_members,def_instances, def_generics} 
	// MW: the order in which the declarations appear in the returned list is essential (explicit imports)
	# sizes = createArray cConversionTableSize 0
	  (size, defs) = foldSt cons_def_to_dcl def_constructors (0, [])
	  sizes = { sizes & [cConstructorDefs] = size }
	  (size, defs) = foldSt selector_def_to_dcl def_selectors (0, defs)
	  sizes = { sizes & [cSelectorDefs] = size }
	  (size, defs) = foldSt type_def_to_dcl def_types (0, defs)
	  sizes = { sizes & [cTypeDefs] = size }
	  (size, defs) = foldSt member_def_to_dcl def_members (0, defs)
	  sizes = { sizes & [cMemberDefs] = size }
	  (size, defs) = foldSt class_def_to_dcl def_classes (0, defs)
	  sizes = { sizes & [cClassDefs] = size }
	  (size, defs) = foldSt instance_def_to_dcl def_instances (0, defs)
	  sizes = { sizes & [cInstanceDefs] = size }
// AA..
	  (size, defs) = foldSt generic_def_to_dcl def_generics (0, defs)
	  sizes = { sizes & [cGenericDefs] = size }
// ..AA
	= (sizes, defs)
where
	type_def_to_dcl {td_name, td_pos} (decl_index, decls)
		= (inc decl_index, [Declaration { decl_ident = td_name, decl_pos = td_pos, decl_kind = STE_Type, decl_index = decl_index } : decls]) 
	cons_def_to_dcl {cons_symb, cons_pos} (decl_index, decls)
		= (inc decl_index, [Declaration { decl_ident = cons_symb, decl_pos = cons_pos, decl_kind = STE_Constructor, decl_index = decl_index } : decls]) 
	selector_def_to_dcl {sd_symb, sd_field, sd_pos} (decl_index, decls)
		= (inc decl_index, [Declaration { decl_ident = sd_field, decl_pos = sd_pos, decl_kind = STE_Field sd_symb, decl_index = decl_index } : decls]) 
	class_def_to_dcl {class_name, class_pos} (decl_index, decls)
		= (inc decl_index, [Declaration { decl_ident = class_name, decl_pos = class_pos, decl_kind = STE_Class, decl_index = decl_index } : decls]) 
	member_def_to_dcl {me_symb, me_pos} (decl_index, decls)
		= (inc decl_index, [Declaration { decl_ident = me_symb, decl_pos = me_pos, decl_kind = STE_Member, decl_index = decl_index } : decls]) 
	instance_def_to_dcl {ins_class, ins_ident, ins_pos} (decl_index, decls)
		= (inc decl_index, [Declaration { decl_ident = ins_ident, decl_pos = ins_pos, decl_kind = STE_Instance ins_class.glob_object.ds_ident, decl_index = decl_index } : decls])
// AA..
	generic_def_to_dcl {gen_name, gen_member_name, gen_type, gen_pos} (decl_index, decls)
		# generic_decl = Declaration { decl_ident = gen_name, decl_pos = gen_pos, decl_kind = STE_Generic, decl_index = decl_index }
		# member_decl = Declaration { decl_ident = gen_member_name, decl_pos = gen_pos, decl_kind = STE_Generic, decl_index = decl_index }
		= (inc decl_index, [generic_decl, member_decl : decls]) 
// ..AA

collectMacros {ir_from,ir_to} macro_defs sizes_defs
	= collectGlobalFunctions cMacroDefs ir_from ir_to macro_defs sizes_defs

collectFunctionTypes fun_types (sizes, defs)
	# (size, defs) = foldSt fun_type_to_dcl fun_types (0, defs)
	= ({ sizes & [cFunctionDefs] = size }, defs)
where
	fun_type_to_dcl {ft_symb, ft_pos} (decl_index, decls) 
		= (inc decl_index, [Declaration { decl_ident = ft_symb, decl_pos = ft_pos, decl_kind = STE_DclFunction,