check.icl

implementation module check

import StdEnv, compare_types

import syntax, typesupport, parse, checksupport, utilities, checktypes, transform, predef
import explicitimports, comparedefimp, checkFunctionBodies, containers
import genericsupport
import typereify
from checkgenerics import checkGenericDefs,checkGenericCaseDefs,convert_generic_instances,create_gencase_funtypes

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

checkTypeClasses :: !Index !(Optional (CopiedDefinitions, Int)) !*{#ClassDef} !*{#MemberDef} !*{#CheckedTypeDef} !*{#DclModule} !*Heaps !*CheckState
	-> (!*{#ClassDef}, !*{#MemberDef}, !*{#CheckedTypeDef}, !*{#DclModule}, !*Heaps, !*CheckState)
checkTypeClasses module_index opt_icl_info class_defs member_defs type_defs modules heaps=:{hp_type_heaps} cs
	#! n_classes = size class_defs
	# (class_defs,member_defs,type_defs,modules,hp_type_heaps,cs) 
		= iFoldSt (check_type_class module_index opt_icl_info) 0 n_classes (class_defs, member_defs, type_defs, modules, hp_type_heaps, cs)
	= (class_defs,member_defs,type_defs,modules,{heaps & hp_type_heaps = hp_type_heaps},cs)
where
	check_type_class module_index opt_icl_info class_index (class_defs, member_defs, type_defs, modules, type_heaps, cs=:{cs_symbol_table,cs_error})
		| has_to_be_checked module_index opt_icl_info class_index
			# (class_def=:{class_ident,class_pos,class_args,class_context,class_members}, class_defs) = class_defs![class_index]
			  cs = {cs & cs_error = setErrorAdmin (newPosition class_ident 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 
			= (class_defs, member_defs, type_defs, modules, type_heaps, cs)
			= (class_defs, member_defs, type_defs, modules, type_heaps, cs)

	has_to_be_checked module_index No class_index
		= True
	has_to_be_checked module_index (Yes ({copied_class_defs}, n_cached_dcl_mods)) class_index
		= not (module_index < n_cached_dcl_mods && class_index < size copied_class_defs && copied_class_defs.[class_index])

	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,!*PredefinedSymbols,!*ErrorAdmin)
	-> (!Special, !(!Index, ![FunType], !*Heaps,!*PredefinedSymbols, !*ErrorAdmin))
checkSpecial mod_index fun_type=:{ft_type} fun_index subst (next_inst_index, special_types, heaps, predef_symbols,error)
	# (special_type, hp_type_heaps, error) = substitute_type ft_type subst heaps.hp_type_heaps error
	  (spec_types, predef_symbols, error) = checkAndCollectTypesOfContextsOfSpecials special_type.st_context predef_symbols 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 = FSP_FunIndex fun_index, ft_type_ptr = new_info_ptr} : special_types ],
					{ heaps & hp_type_heaps = hp_type_heaps, hp_var_heap = hp_var_heap }, predef_symbols, 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, error)
			= instantiateTypes st_vars st_attr_vars [ st_result : st_args ] st_context st_attr_env environment [] type_heaps 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_ident,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_ident 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_predef_symbols,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_predef_symbols 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_predef_symbols=cs_predef_symbols,cs_error = cs_error }

	check_specials :: !Index !FunType !Index !FunSpecials !Index ![FunType] !*Heaps !*PredefinedSymbols !*ErrorAdmin
										 -> (!FunSpecials,!Index,![FunType],!*Heaps,!*PredefinedSymbols,!*ErrorAdmin)
	check_specials mod_index fun_type fun_index (FSP_Substitutions substs) next_inst_index all_instances heaps predef_symbols error
		# (list_of_specials, (next_inst_index, all_instances, heaps, cs_predef_symbols,cs_error))
				= mapSt (checkSpecial mod_index fun_type fun_index) substs (next_inst_index, all_instances, heaps, predef_symbols,error)
		= (FSP_ContextTypes list_of_specials, next_inst_index, all_instances, heaps, cs_predef_symbols,cs_error)
	check_specials mod_index fun_type fun_index FSP_None next_inst_index all_instances heaps predef_symbols error
		= (FSP_None, next_inst_index, all_instances, heaps, predef_symbols,error)

checkDclInstanceMemberTypes :: !*{#ClassInstance} !ModuleIndex !v:{#CheckedTypeDef} !w:{#ClassDef} !v:{#DclModule} !*Heaps !*CheckState
						  				-> (!*{#ClassInstance},!v:{#CheckedTypeDef},!w:{#ClassDef},!v:{#DclModule},!*Heaps,!*CheckState)
checkDclInstanceMemberTypes instance_defs mod_index type_defs class_defs modules heaps cs
	= check_instance_member_types 0 instance_defs mod_index type_defs class_defs modules heaps cs
where
	check_instance_member_types :: !Index !*{#ClassInstance} !ModuleIndex !v:{#CheckedTypeDef} !w:{#ClassDef} !v:{#DclModule} !*Heaps !*CheckState
									  			   -> (!*{#ClassInstance},!v:{#CheckedTypeDef},!w:{#ClassDef},!v:{#DclModule},!*Heaps,!*CheckState)
	check_instance_member_types inst_index instance_defs module_index type_defs class_defs modules heaps cs
		| inst_index < size instance_defs
			# (instance_def, instance_defs) = instance_defs![inst_index]
			  (ins_member_types, type_defs, class_defs, modules, heaps, cs)
				= check_function_types instance_def.ins_member_types module_index type_defs class_defs modules heaps cs
			  instance_defs = {instance_defs & [inst_index].ins_member_types = sort ins_member_types }
			= check_instance_member_types (inc inst_index) instance_defs module_index type_defs class_defs modules heaps cs
			= (instance_defs,type_defs,class_defs,modules,heaps,cs)

	check_function_types :: ![FunType] !ModuleIndex !v:{#CheckedTypeDef} !w:{#ClassDef} !v:{#DclModule} !*Heaps !*CheckState
									 -> (![FunType],!v:{#CheckedTypeDef},!w:{#ClassDef},!v:{#DclModule},!*Heaps,!*CheckState)
	check_function_types [fun_type=:{ft_ident,ft_type,ft_pos,ft_specials} : fun_types] module_index type_defs class_defs modules heaps cs
		# position = newPosition ft_ident 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
		  (new_info_ptr, hp_var_heap) = newPtr VI_Empty heaps.hp_var_heap
		  heaps = { heaps & hp_type_heaps = hp_type_heaps, hp_var_heap = hp_var_heap }
		  fun_type = { fun_type & ft_type = ft_type, ft_specials = ft_specials, ft_type_ptr = new_info_ptr }
		  (fun_types, type_defs, class_defs, modules, heaps, cs)
			= check_function_types fun_types module_index type_defs class_defs modules heaps cs
		= ([fun_type:fun_types], type_defs, class_defs, modules, heaps, cs)
	check_function_types [] module_index type_defs class_defs modules heaps cs
		= ( [], type_defs, class_defs, modules, heaps, cs)

checkSpecialsOfInstances :: !Index !Index ![ClassInstance] !Index ![ClassInstance] ![FunType] {# FunType} *{! [Special] } !*Heaps !*PredefinedSymbols !*ErrorAdmin
		-> (!Index, ![ClassInstance], ![FunType], !*{! [Special]}, !*Heaps, !*PredefinedSymbols,!*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 predef_symbols error
	= case ins_specials of
		SP_TypeOffset type_offset
			# (next_inst_index, rev_mem_specials, all_specials, all_spec_types, heaps,predef_symbols, 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 predef_symbols 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 predef_symbols 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 predef_symbols error
where
	check_and_build_members :: !Index !Index !Int {#ClassInstanceMember} !Int !Index ![ClassInstanceMember] ![FunType] !{#FunType}
					!*{![Special]} !*Heaps !*PredefinedSymbols !*ErrorAdmin
		-> (!Index,![ClassInstanceMember],![FunType],
					!*{![Special]},!*Heaps,!*PredefinedSymbols,!*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 predef_symbols error
		| member_offset < size ins_members
			# member = ins_members.[member_offset]
			  member_index = member.cim_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]
		 	  (FSP_Substitutions specials) = mem_inst.ft_specials
		 	  env = specials !! type_offset
			  member = {member & cim_index = next_inst_index}
			  (spec_type, (next_inst_index, all_specials, heaps, predef_symbols,error))
			  		= checkSpecial mod_index mem_inst member_index env (next_inst_index, all_specials, heaps, predef_symbols,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 predef_symbols error
			= (next_inst_index, rev_mem_specials, all_specials, all_spec_types, heaps, predef_symbols,error)
checkSpecialsOfInstances mod_index first_mem_index [] next_inst_index all_class_instances all_specials inst_spec_defs all_spec_types heaps predef_symbols error
	= (next_inst_index, all_class_instances, all_specials, all_spec_types, heaps, predef_symbols,error)

checkMemberTypes :: !Index !(Optional (CopiedDefinitions, Int)) !*{#MemberDef} !*{#CheckedTypeDef} !*{#ClassDef} !*{#DclModule} !*Heaps !*CheckState
	-> (!*{#MemberDef}, !*{#CheckedTypeDef}, !*{#ClassDef}, !*{#DclModule}, !*Heaps, !*CheckState)
checkMemberTypes module_index opt_icl_info member_defs type_defs class_defs modules heaps=:{hp_type_heaps,hp_var_heap} cs
	#! nr_of_members = size member_defs
	# (mds,tds,cds,modules,hp_type_heaps,hp_var_heap,cs) 
		= iFoldSt (check_class_member module_index opt_icl_info) 0 nr_of_members (member_defs, type_defs, class_defs, modules, hp_type_heaps, hp_var_heap, cs)
	= (mds,tds,cds,modules,{heaps & hp_type_heaps = hp_type_heaps,hp_var_heap = hp_var_heap},cs) 
where
	check_class_member module_index opt_icl_info member_index (member_defs, type_defs, class_defs, modules, type_heaps, var_heap, cs)
		# (member_def=:{me_ident,me_type,me_pos,me_class}, member_defs) = member_defs![member_index]
		| has_to_be_checked opt_icl_info me_class
			# position = newPosition me_ident 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)
			= (member_defs, type_defs, class_defs, modules, type_heaps, var_heap, cs)

	has_to_be_checked No glob_class_index
		= True
	has_to_be_checked (Yes ({copied_class_defs}, n_cached_dcl_mods)) {glob_module,glob_object}
		= not (glob_module < n_cached_dcl_mods && glob_object < size copied_class_defs && copied_class_defs.[glob_object])

::	InstanceSymbols =
	{	is_type_defs		:: !.{# CheckedTypeDef}
	,	is_class_defs		:: !.{# ClassDef}
	,	is_member_defs		:: !.{# MemberDef}
	,	is_modules			:: !.{# DclModule}
	}

checkInstanceDefs :: !Index !*{#ClassInstance} !u:{#CheckedTypeDef} !u:{#ClassDef} !u:{#MemberDef} !u:{#DclModule} !*Heaps !*CheckState
						-> (!.{#ClassInstance},!u:{#CheckedTypeDef},!u:{#ClassDef},!u:{#MemberDef},!u:{#DclModule},!.Heaps,!.CheckState)
checkInstanceDefs mod_index instance_defs type_defs class_defs member_defs modules heaps=:{hp_type_heaps} cs
	# is = { is_type_defs = type_defs, is_class_defs = class_defs, is_member_defs = member_defs, is_modules = modules }
	  (instance_defs, is, hp_type_heaps, cs) = check_instance_defs 0 mod_index instance_defs is hp_type_heaps cs
	= (instance_defs, is.is_type_defs, is.is_class_defs, is.is_member_defs, is.is_modules, {heaps & hp_type_heaps = hp_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 instance_def mod_index 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 :: !ClassInstance !Index !u:InstanceSymbols !*TypeHeaps !*CheckState -> (!ClassInstance, !u:InstanceSymbols, !*TypeHeaps, !*CheckState)
	check_instance ins=:{ins_class_ident={ci_ident=Ident {id_name,id_info}},ins_pos,ins_ident} module_index is type_heaps cs=:{cs_symbol_table}
		#  	({ste_index,ste_kind}, 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 ste_kind of
				STE_Class
					# (class_def, is) = is!is_class_defs.[ste_index]
					-> check_class_instance	class_def module_index ste_index module_index ins is type_heaps cs 
				STE_Imported STE_Class decl_index
 					# (class_def, is) = is!is_modules.[decl_index].dcl_common.com_class_defs.[ste_index]
					-> check_class_instance class_def module_index ste_index decl_index ins is type_heaps cs
				ste -> (ins, is, type_heaps, { cs & cs_error = checkError id_name "class undefined" cs.cs_error })
		= (ins, is, type_heaps, popErrorAdmin cs)
	check_instance ins=:{ins_class_ident={ci_ident=QualifiedIdent module_ident class_name},ins_pos,ins_ident}
			module_index is type_heaps cs
		# cs = pushErrorAdmin (newPosition ins_ident ins_pos) cs
		# (found,{decl_kind,decl_ident=type_ident,decl_index=class_index},cs) = search_qualified_ident module_ident class_name ClassNameSpaceN cs
		| not found
			# cs = {cs & cs_error = checkError ("'"+++module_ident.id_name+++"'."+++class_name) "class undefined" cs.cs_error}
			= (ins, is, type_heaps, popErrorAdmin cs)
			= case decl_kind of
				STE_Imported STE_Class class_module
					# (class_def, is) = is!is_modules.[class_module].dcl_common.com_class_defs.[class_index]
					# ins = {ins & ins_class_ident.ci_ident=Ident class_def.class_ident}
					-> check_class_instance class_def module_index class_index class_module ins is type_heaps cs
				_
					# cs = {cs & cs_error = checkError ("'"+++module_ident.id_name+++"'."+++class_name) "class undefined" cs.cs_error}
					-> (ins, is, type_heaps, popErrorAdmin cs)

	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_class_ident=ins_class_ident=:{ci_ident,ci_arity},ins_type,ins_specials,ins_pos,ins_ident}
			is=:{is_class_defs,is_modules} type_heaps cs=:{cs_symbol_table}	
		| class_def.class_arity == ci_arity
			# ins_class_index = {gi_index = class_index, gi_module = class_mod_index}
			  (ins_type, ins_specials, is_type_defs, is_class_defs, is_modules, type_heaps, cs)
			  		= checkInstanceType module_index ins_class_index ins_class_ident 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_index = ins_class_index, ins_type = ins_type, ins_specials = ins_specials}, is, type_heaps, cs)
			# (Ident {id_name}) = ci_ident
			# cs = {cs & cs_error = checkError id_name ("wrong arity: expected "+++toString class_def.class_arity+++" found "+++toString ci_arity) cs.cs_error}
			= (ins, is, type_heaps, cs)

checkIclInstances :: !Index    !*CommonDefs !u:{# DclModule} !*VarHeap !*TypeHeaps !*CheckState
	-> (![(Index,SymbolType)], !*CommonDefs,!u:{# DclModule},!*VarHeap,!*TypeHeaps,!*CheckState)
checkIclInstances 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_icl_instances 0 mod_index [] com_instance_defs com_class_defs com_member_defs 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, 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_icl_instances :: !Index !Index ![(Index,SymbolType)]
								   !x:{#ClassInstance} !w:{#ClassDef} !v:{#MemberDef} !w:{#GenericDef} !z:{#CheckedTypeDef} !u:{#DclModule} !*VarHeap !*TypeHeaps !*CheckState
		-> (![(Index,SymbolType)], !x:{#ClassInstance},!w:{#ClassDef},!v:{#MemberDef},!w:{#GenericDef},!z:{#CheckedTypeDef},!u:{#DclModule},!*VarHeap,!*TypeHeaps,!*CheckState)
	check_icl_instances inst_index mod_index instance_types instance_defs class_defs member_defs generic_defs type_defs modules var_heap type_heaps cs
		| inst_index < size instance_defs
			# (instance_def=:{ins_ident, ins_pos}, instance_defs) = instance_defs![inst_index]
			# (instance_types, class_defs, member_defs, generic_defs, type_defs, modules, var_heap, type_heaps, cs) =
					check_class_instance instance_def mod_index instance_types class_defs member_defs generic_defs type_defs modules var_heap type_heaps cs				 
			= check_icl_instances (inc inst_index) mod_index instance_types instance_defs class_defs member_defs generic_defs type_defs modules var_heap type_heaps cs 
			= (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_index,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_ident}, class_defs, modules) = getClassDef ins_class_index 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_icl_instance_members mod_index ins_class_index.gi_module
					0 class_size ins_members class_members class_ident 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)
			# cs = { cs & cs_error = checkErrorWithIdentPos (newPosition class_ident ins_pos) "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_icl_instance_members :: !Index !Index !Int !Int !{#ClassInstanceMember} !{#DefinedSymbol} Ident !Position !InstanceType
			![(Index,SymbolType)] !v:{# MemberDef} !z:{#CheckedTypeDef} !u:{#DclModule} !*VarHeap !*TypeHeaps !*CheckState
		-> (![(Index,SymbolType)],!v:{# MemberDef},!z:{#CheckedTypeDef},!u:{#DclModule},!*VarHeap,!*TypeHeaps,!*CheckState)
	check_icl_instance_members module_index member_mod_index mem_offset class_size ins_members class_members
				class_ident 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]
			  cs = setErrorAdmin (newPosition class_ident ins_pos) cs
			| ins_member.cim_ident <> class_member.ds_ident
				= check_icl_instance_members module_index member_mod_index (inc mem_offset) class_size ins_members class_members class_ident 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.cim_arity <> class_member.ds_arity
				= check_icl_instance_members module_index member_mod_index (inc mem_offset) class_size ins_members class_members class_ident 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_ident, me_type,me_class_vars,me_pos}, member_defs, modules) = getMemberDef member_mod_index class_member.ds_index module_index member_defs modules
				  (instance_type, _, type_heaps, Yes (modules, type_defs), cs_error)
				  		= determineTypeOfMemberInstance me_type me_class_vars ins_type SP_None type_heaps (Yes (modules, type_defs, x_main_dcl_module_n)) cs.cs_error
				  (st_context, var_heap) = initializeContextVariables instance_type.st_context var_heap
				  instance_type = { instance_type & st_context = st_context }
				= check_icl_instance_members module_index member_mod_index (inc mem_offset) class_size ins_members class_members class_ident ins_pos ins_type
						[ (ins_member.cim_index, instance_type) : instance_types ] member_defs type_defs modules var_heap type_heaps { cs & cs_error = cs_error }

getClassDef :: !GlobalIndex !Int !u:{#ClassDef} !v:{#DclModule} -> (!ClassDef,!u:{#ClassDef},!v:{#DclModule})
getClassDef {gi_module,gi_index} mod_index class_defs modules
	| gi_module == mod_index
		# (class_def, class_defs) = class_defs![gi_index]
		= (class_def, class_defs, modules)
		# (dcl_mod, modules) = modules![gi_module]
		= (dcl_mod.dcl_common.com_class_defs.[gi_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)

instantiateTypes :: ![TypeVar] ![AttributeVar] ![AType] ![TypeContext] ![AttrInequality] !SpecialSubstitution ![SpecialSubstitution] !*TypeHeaps !*ErrorAdmin
	-> (![TypeVar], ![AttributeVar], ![AType], ![TypeContext], ![AttrInequality], ![SpecialSubstitution], !*TypeHeaps, !*ErrorAdmin)
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} 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_var_subst ss_attrs ([], th_attrs)

	  type_heaps = foldSt build_type_subst ss_environ { type_heaps & th_vars = th_vars, th_attrs = th_attrs }
	  (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_var_subst old_attr_vars (new_attr_vars, type_heaps.th_attrs)

	  (inst_types, (ok2, type_heaps))	= mapSt substitue_arg_type types (True, { type_heaps & th_vars = th_vars, th_attrs = th_attrs })
//	  (ok2, inst_types, type_heaps)		= substitute types { type_heaps & th_vars = th_vars, th_attrs = th_attrs }
	  (inst_contexts, type_heaps)	= substitute type_contexts type_heaps
	  (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
	= (inst_vars, inst_attr_vars, inst_types, new_ss_context ++ inst_contexts, inst_attr_env, special_subst_list, { type_heaps & th_vars = th_vars }, 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
// RWS ...
/*
	FIXME: this is a patch for the following incorrect function type (in a dcl module)


    f :: a | c a b special
        a=[], b = Int
        a=T, b = Char

   The type variable b doesn't occur in f's type, but this is checked in a later
   phase. Probably it's a better solution to change the order of checking.

*/
		| isNilPtr bind_dst.tv_info_ptr
			= type_heaps
// ... RWS
		= { type_heaps & th_vars = writePtr bind_dst.tv_info_ptr (TVI_Type bind_src) type_heaps.th_vars}

	substitue_arg_type at=:{at_type = TFA type_vars type} (was_ok, type_heaps)
		# (fresh_type_vars, type_heaps) = foldSt build_avar_subst type_vars ([], type_heaps)
		  (new_at, type_heaps) = substitute {at & at_type = type} type_heaps
		= ({ new_at & at_type = TFA fresh_type_vars new_at.at_type}, (was_ok, type_heaps))
	substitue_arg_type type (was_ok, type_heaps)
		# (type, type_heaps) = substitute type type_heaps
		= (type, (was_ok, type_heaps))
		
	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_avar_subst atv=:{atv_variable,atv_attribute} (free_vars, type_heaps)
		# (new_info_ptr, th_vars) = newPtr TVI_Empty type_heaps.th_vars
		  new_fv = { atv_variable & tv_info_ptr = new_info_ptr}
		  th_vars = th_vars <:= (atv_variable.tv_info_ptr, TVI_Type (TV new_fv))
		  (new_attr, th_attrs) = build_attr_subst atv_attribute type_heaps.th_attrs
		= ([ { atv & atv_variable = new_fv, atv_attribute = new_attr } : free_vars], { type_heaps & th_vars = th_vars, th_attrs = th_attrs })
	where		  
		 build_attr_subst (TA_Var avar) attr_var_heap
			# (new_info_ptr, attr_var_heap) = newPtr AVI_Empty attr_var_heap
			  new_attr = { avar & av_info_ptr = new_info_ptr}
			= (TA_Var new_attr, attr_var_heap <:= (avar.av_info_ptr, AVI_Attr (TA_Var new_attr)))
		 build_attr_subst attr attr_var_heap
			= (attr, attr_var_heap)

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

determineTypeOfMemberInstance :: !SymbolType ![TypeVar] !InstanceType !Specials !*TypeHeaps !u:(Optional (v:{#DclModule}, w:{#CheckedTypeDef}, Index)) !*ErrorAdmin
												 -> (!SymbolType, !FunSpecials, !*TypeHeaps,!u: Optional (v:{#DclModule}, w:{#CheckedTypeDef}), !*ErrorAdmin)
determineTypeOfMemberInstance mem_st class_vars {it_types,it_vars,it_attr_vars,it_context} specials type_heaps opt_modules 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, error)
	  		= determine_type_of_member_instance mem_st env specials type_heaps error
	  (type_heaps, opt_modules, error)
	  		= check_attribution_consistency mem_st type_heaps opt_modules error
	= (st, specials, type_heaps, opt_modules, error)
where
	determine_type_of_member_instance mem_st=:{st_context} env (SP_Substitutions substs) type_heaps error
		# (mem_st, substs, type_heaps, error) 
				= substitute_symbol_type { mem_st &  st_context = tl st_context } env substs type_heaps error
		= (mem_st, FSP_Substitutions substs, type_heaps, error) 
	determine_type_of_member_instance mem_st=:{st_context} env SP_None type_heaps error
		# (mem_st, _, type_heaps, error)
				= substitute_symbol_type { mem_st &  st_context = tl st_context } env [] type_heaps error
		= (mem_st, FSP_None, type_heaps, error)

	substitute_symbol_type st=:{st_vars,st_attr_vars,st_args,st_result,st_context,st_attr_env} environment specials type_heaps error
		# (st_vars, st_attr_vars, [st_result : st_args], st_context, st_attr_env, specials, type_heaps, error)
			= instantiateTypes st_vars st_attr_vars [ st_result : st_args ] st_context st_attr_env environment specials type_heaps 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, error)

	check_attribution_consistency {st_args, st_result} type_heaps No error
		= (type_heaps, No, error)
	check_attribution_consistency {st_args, st_result} type_heaps=:{th_vars} (Yes (modules, type_defs, x_main_dcl_module_n)) 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), 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_ident, 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_ident, type_index} _
				-> must_not_be_essentially_unique_for_TA type_ident type_index th_vars
			TAS {type_ident, type_index} _ _
				-> must_not_be_essentially_unique_for_TA type_ident type_index th_vars
			_
				-> (False, th_vars, modules, type_defs, error)
		where
			must_not_be_essentially_unique_for_TA type_ident type_index th_vars
				# (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_ident 
								(   "is unique but instanciates class variable "
								 +++tv_ident.id_name
								 +++" that is non uniquely used in a member type"
								) 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)

determineTypesOfDclInstances :: !Index !Index !*{#ClassInstance} !*{# ClassDef} !*{# MemberDef} 
							 !*{#DclModule} !*TypeHeaps !*VarHeap !*CheckState
	-> (![FunType], !Index, ![ClassInstance], !*{#ClassInstance}, !*{# ClassDef}, !*{# MemberDef}, !*{#DclModule}, !*TypeHeaps, !*VarHeap, !*CheckState)
determineTypesOfDclInstances first_memb_inst_index mod_index com_instance_defs com_class_defs com_member_defs
		modules type_heaps var_heap cs=:{cs_error,cs_predef_symbols,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_predef_symbols,cs_error)
				= determine_types_of_dcl_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_predef_symbols 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_predef_symbols=cs_predef_symbols,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_dcl_instances :: !Index !Index !Index !Index !Index ![ClassInstance]
												  !v:{#ClassDef} !w:{#MemberDef} !x:{#DclModule} !*{#ClassInstance} !*TypeHeaps !*VarHeap !*PredefinedSymbols !*ErrorAdmin
		-> (![FunType], !Index, ![ClassInstance], !v:{#ClassDef},!w:{#MemberDef},!x:{#DclModule},!*{#ClassInstance},!*TypeHeaps,!*VarHeap,!*PredefinedSymbols,!*ErrorAdmin)
	determine_types_of_dcl_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 predef_symbols error
		| inst_index < size instance_defs
			# (instance_def=:{ins_class_index,ins_pos,ins_type,ins_member_types,ins_specials}, instance_defs) = instance_defs![inst_index]
			# ({class_ident, class_members}, class_defs, modules) = getClassDef ins_class_index mod_index class_defs modules
			  class_size = size class_members
			  (ins_members, memb_inst_defs1, member_defs, modules, type_heaps, var_heap, error)
			  		= determine_dcl_instance_symbols_and_types 0 ins_member_types x_main_dcl_module_n next_mem_inst_index mod_index ins_class_index.gi_module class_size class_members
			  				ins_type ins_specials class_ident 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, predef_symbols,error)
					= check_instance_specials mod_index instance_def inst_index ins_specials next_class_inst_index all_class_specials type_heaps predef_symbols error
			  (memb_inst_defs2, next_mem_inst_index, all_class_specials, class_defs, member_defs, modules, instance_defs, type_heaps, var_heap, predef_symbols,error)
			  		= determine_types_of_dcl_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 predef_symbols 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, predef_symbols,error)
			= ([], next_mem_inst_index, all_class_specials, class_defs, member_defs, modules, instance_defs, type_heaps, var_heap, predef_symbols,error)

	determine_dcl_instance_symbols_and_types :: !Index ![FunType] !Index !Index !Index !Index !Int !{#DefinedSymbol} !InstanceType !Specials Ident !Position
															!w:{#MemberDef} !u:{#DclModule} !*TypeHeaps !*VarHeap !*ErrorAdmin
					-> (![ClassInstanceMember], ![FunType], !w:{#MemberDef},!u:{#DclModule},!*TypeHeaps,!*VarHeap,!.ErrorAdmin)
	determine_dcl_instance_symbols_and_types mem_offset member_types x_main_dcl_module_n first_inst_index module_index member_mod_index class_size class_members
			ins_type ins_specials class_ident 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_ident,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_ident ins_pos) cs_error
			  (instance_type, new_ins_specials, type_heaps, Yes (modules, _), cs_error)
			  		= determineTypeOfMemberInstance me_type me_class_vars ins_type ins_specials type_heaps (Yes (modules, {}, cUndef)) cs_error
			  (instance_type, new_ins_specials, member_types, modules, type_heaps, cs_error)
				= if_instance_member_type_specified_compare_and_use member_types instance_type new_ins_specials me_ident modules type_heaps cs_error
			  cs_error = popErrorAdmin cs_error
			  (new_info_ptr, var_heap) = newPtr VI_Empty var_heap
			  inst_def = MakeNewFunctionType me_ident 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_dcl_instance_symbols_and_types (inc mem_offset) member_types x_main_dcl_module_n first_inst_index module_index member_mod_index
			 				class_size class_members ins_type ins_specials class_ident ins_pos member_defs modules type_heaps var_heap cs_error
			  class_member = {cim_ident=class_member.ds_ident, cim_arity=class_member.ds_arity, cim_index = first_inst_index +  mem_offset}
			= ([class_member : inst_symbols], [inst_def : memb_inst_defs], member_defs, modules, type_heaps, var_heap, cs_error)
	where
		if_instance_member_type_specified_compare_and_use :: [FunType] SymbolType FunSpecials Ident !u:{#DclModule} !*TypeHeaps !*ErrorAdmin
															-> (!SymbolType,!FunSpecials,![FunType],!u:{#DclModule},!*TypeHeaps,!*ErrorAdmin)
		if_instance_member_type_specified_compare_and_use member_types=:[] instance_type specials me_ident modules type_heaps cs_error
			= (instance_type, specials, member_types, modules, type_heaps, cs_error)
		if_instance_member_type_specified_compare_and_use member_types=:[{ft_ident,ft_type,ft_arity}:tl_member_types] instance_type specials me_ident modules type_heaps cs_error
			| ft_ident.id_name<me_ident.id_name
				= if_instance_member_type_specified_compare_and_use tl_member_types instance_type specials me_ident modules type_heaps cs_error
			| ft_ident.id_name<>me_ident.id_name
				= (instance_type, specials, member_types, modules, type_heaps, cs_error)
			| ft_arity<>instance_type.st_arity
				# cs_error = specified_member_type_incorrect_error CEC_NrArgsNotOk cs_error
				= (instance_type, specials, member_types, modules, type_heaps, cs_error)
			# (error_code,type_heaps) = compare_specified_and_derived_instance_types ft_type instance_type type_heaps
			| error_code==CEC_Ok || error_code==CEC_OkWithFirstMoreStrictness
				= (ft_type, specials, member_types, modules, type_heaps, cs_error)
				# cs_error = specified_member_type_incorrect_error error_code cs_error
				= (instance_type, specials, member_types, modules, type_heaps, cs_error)

	check_instance_specials :: !Index !ClassInstance !Index !Specials !Index ![ClassInstance] !*TypeHeaps !*PredefinedSymbols !*ErrorAdmin
		-> (!Specials, !Index, ![ClassInstance], !*TypeHeaps, !*PredefinedSymbols,!*ErrorAdmin)
	check_instance_specials mod_index inst_type inst_index (SP_Substitutions substs) next_inst_index all_instances type_heaps predef_symbols error
		# (list_of_specials, next_inst_index, all_instances, type_heaps, predef_symbols,error)
			= check_specials mod_index inst_type 0 substs [] next_inst_index all_instances type_heaps predef_symbols error
		= (SP_ContextTypes list_of_specials, next_inst_index, all_instances, type_heaps, predef_symbols, error)
	where
		check_specials mod_index inst=:{ins_type} type_offset [ subst : substs ] list_of_specials next_inst_index all_instances type_heaps predef_symbols error
			# (special_type, type_heaps, error) = substitute_instance_type ins_type subst type_heaps error
			  (spec_types, predef_symbols,error) = checkAndCollectTypesOfContextsOfSpecials special_type.it_context predef_symbols 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 predef_symbols error
		where
			substitute_instance_type :: !InstanceType !SpecialSubstitution !*TypeHeaps !*ErrorAdmin -> (!InstanceType,!*TypeHeaps,!.ErrorAdmin)
			substitute_instance_type it=:{it_vars,it_attr_vars,it_types,it_context} environment type_heaps cs_error
				# (it_vars, it_attr_vars, it_atypes, it_context, _, _, type_heaps, cs_error)	
					= instantiateTypes it_vars it_attr_vars [MakeAttributedType type \\ type <- it_types] it_context [] environment [] type_heaps cs_error
				= ({it & it_vars = it_vars, it_types = [ at_type \\ {at_type} <- it_atypes ], it_attr_vars = it_attr_vars, it_context = it_context }, type_heaps, cs_error)			
		check_specials mod_index inst=:{ins_type} type_offset [] list_of_specials next_inst_index all_instances type_heaps predef_symbols error
			= (list_of_specials,  next_inst_index, all_instances, type_heaps, predef_symbols, error)
	check_instance_specials mod_index fun_type fun_index SP_None next_inst_index all_instances type_heaps predef_symbols error
		= (SP_None, next_inst_index, all_instances, type_heaps, predef_symbols,error)
	
checkAndCollectTypesOfContextsOfSpecials :: [TypeContext] *PredefinedSymbols *ErrorAdmin -> (![[Type]],!*PredefinedSymbols,!*ErrorAdmin);
checkAndCollectTypesOfContextsOfSpecials type_contexts predef_symbols error
	= mapSt2 check_and_collect_context_types_of_special type_contexts predef_symbols error
where	
	check_and_collect_context_types_of_special {tc_class=TCClass {glob_object={ds_ident,ds_index},glob_module},tc_types} predef_symbols error
		| hasNoTypeVariables tc_types
			= (tc_types, predef_symbols,error)
		# {pds_def,pds_module} = predef_symbols.[PD_ArrayClass]
		| glob_module==pds_module && ds_index==pds_def && is_lazy_or_strict_array tc_types predef_symbols
			= (tc_types, predef_symbols,error)
		# {pds_def,pds_module} = predef_symbols.[PD_ListClass]
		| glob_module==pds_module && ds_index==pds_def && is_lazy_or_strict_list tc_types predef_symbols
			= (tc_types, predef_symbols,error)
			= (tc_types, predef_symbols,checkError ds_ident.id_name "illegal specialization" error)
	check_and_collect_context_types_of_special {tc_class=TCGeneric {gtc_generic},tc_types} predef_symbols error
		= (tc_types, predef_symbols,checkError gtc_generic.glob_object.ds_ident.id_name "generic specials are illegal" error)

	hasNoTypeVariables []
		= True
	hasNoTypeVariables [TV tvar : types]
		= False
	hasNoTypeVariables [ _ : types]
		= hasNoTypeVariables types
	
	is_lazy_or_strict_array [TA {type_index={glob_module,glob_object}} [],TV var] predef_symbols
		# {pds_def,pds_module} = predef_symbols.[PD_LazyArrayType]
		| glob_module==pds_module && glob_object==pds_def
			= True
		# {pds_def,pds_module} = predef_symbols.[PD_StrictArrayType]
		| glob_module==pds_module && glob_object==pds_def
			= True
			= False
	is_lazy_or_strict_array _ predef_symbols
		= False

	is_lazy_or_strict_list [TA {type_index={glob_module,glob_object}} [],TV var] predef_symbols
		# {pds_def,pds_module} = predef_symbols.[PD_ListType]
		| glob_module==pds_module && glob_object==pds_def
			= True
		# {pds_def,pds_module} = predef_symbols.[PD_StrictListType]
		| glob_module==pds_module && glob_object==pds_def
			= True
		# {pds_def,pds_module} = predef_symbols.[PD_TailStrictListType]
		| glob_module==pds_module && glob_object==pds_def
			= True
		# {pds_def,pds_module} = predef_symbols.[PD_StrictTailStrictListType]
		| glob_module==pds_module && glob_object==pds_def
			= True
			= False
	is_lazy_or_strict_list _ predef_symbols
		= False

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)

ident_for_errors_from_fun_symb_and_fun_kind :: Ident FunKind -> Ident;
ident_for_errors_from_fun_symb_and_fun_kind {id_name} (FK_Function fun_name_is_location_dependent)
	| fun_name_is_location_dependent && size id_name>0
		# beautiful_name = if (id_name.[0]==backslash) "lambda" "comprehension"
		= { id_name=beautiful_name, id_info=nilPtr }
ident_for_errors_from_fun_symb_and_fun_kind fun_ident _
	= fun_ident

// check that there are no strict lets, mark top-level cases as explicit
class checkMacro a :: !Bool !a !*ErrorAdmin -> (!a, !*ErrorAdmin)

instance checkMacro [a] | checkMacro a where
	checkMacro topLevel l ea
		=	mapSt (checkMacro topLevel) l ea

instance checkMacro FunctionBody where
	checkMacro topLevel (CheckedBody body) ea
		# (body, ea)
			=	checkMacro topLevel body ea
		= (CheckedBody body, ea)

instance checkMacro CheckedBody where
	checkMacro topLevel body=:{cb_rhs} ea
		# (cb_rhs, ea)
			=	checkMacro topLevel cb_rhs ea
		= ({body & cb_rhs = cb_rhs}, ea)

instance checkMacro CheckedAlternative where
	checkMacro topLevel alt=:{ca_rhs} ea
		# (ca_rhs, ea)
			=	checkMacro topLevel ca_rhs ea
		= ({alt & ca_rhs = ca_rhs}, ea)

instance checkMacro Expression where
	checkMacro topLevel (Let lad) ea
		# (lad, ea)
			=	checkMacro topLevel lad ea
		=	(Let lad, ea)
	checkMacro topLevel (Case kees) ea
		# (kees, ea)
			=	checkMacro topLevel kees ea
		=	(Case kees, ea)
	checkMacro _ expr ea
		=	(expr, ea)

instance checkMacro Let where
	checkMacro topLevel lad=:{let_strict_binds, let_expr} ea
		# ea
			=	check_strict_binds let_strict_binds ea
		# (let_expr, ea)
			=	checkMacro topLevel let_expr ea
		= ({lad & let_expr = let_expr}, ea)
		where
			check_strict_binds [] ea
				=	ea
			check_strict_binds _ ea
				=	checkError "#! not allowed in macros" "" ea

instance checkMacro Case where
	checkMacro topLevel kees=:{case_guards, case_explicit} ea
		# (case_guards, ea)
			=	checkMacro False case_guards ea
		= ({kees & case_guards = case_guards,case_explicit = topLevel || case_explicit}, ea)

instance checkMacro CasePatterns where
	checkMacro topLevel (AlgebraicPatterns type patterns) ea
		# (patterns, ea)
			=	checkMacro topLevel patterns ea	
		=	(AlgebraicPatterns type patterns, ea)
	checkMacro topLevel (BasicPatterns type patterns) ea
		# (patterns, ea)
			=	checkMacro topLevel patterns ea	
		=	(BasicPatterns type patterns, ea)
	checkMacro topLevel (NewTypePatterns type patterns) ea
		# (patterns, ea) = checkMacro topLevel patterns ea	
		= (NewTypePatterns type patterns, ea)
	checkMacro topLevel (DynamicPatterns patterns) ea
		# (patterns, ea)
			=	checkMacro topLevel patterns ea	
		=	(DynamicPatterns patterns, ea)
	checkMacro topLevel (OverloadedListPatterns type decons patterns) ea
		# (patterns, ea)
			=	checkMacro topLevel patterns ea	
		=	(OverloadedListPatterns type decons patterns, ea)
	checkMacro _ NoPattern ea
		=	(NoPattern, ea)

instance checkMacro AlgebraicPattern where
	checkMacro topLevel pattern=:{ap_expr} ea
		# (ap_expr, ea)
			=	checkMacro topLevel ap_expr ea	
		=	({pattern & ap_expr = ap_expr}, ea)

instance checkMacro BasicPattern where
	checkMacro topLevel pattern=:{bp_expr} ea
		# (bp_expr, ea)
			=	checkMacro topLevel bp_expr ea	
		=	({pattern & bp_expr = bp_expr}, ea)

instance checkMacro DynamicPattern where
	checkMacro topLevel pattern=:{dp_rhs} ea
		# (dp_rhs, ea)
			=	checkMacro topLevel dp_rhs ea	
		=	({pattern & dp_rhs = dp_rhs}, ea)

checkFunctionBodyIfMacro :: !FunKind !FunctionBody !*ErrorAdmin -> (!FunctionBody, !*ErrorAdmin)
checkFunctionBodyIfMacro FK_Macro def ea
	=	checkMacro True def ea
checkFunctionBodyIfMacro _ def ea
	=	(def, ea)

checkFunction :: !FunDef !Index !FunctionOrMacroIndex !Level !Int !*{#FunDef} !*ExpressionInfo !*Heaps !*CheckState
													  -> (!FunDef,!*{#FunDef},!*ExpressionInfo,!*Heaps,!*CheckState);
checkFunction fun_def=:{fun_ident,fun_pos,fun_body,fun_type,fun_kind} mod_index fun_index def_level local_functions_index_offset
			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,hp_generic_heap} cs=:{cs_error}			
	# function_ident_for_errors = ident_for_errors_from_fun_symb_and_fun_kind fun_ident fun_kind
	# cs = {cs & cs_error = pushErrorAdmin (newPosition function_ident_for_errors fun_pos) 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 (fun_kind == FK_Caf) 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_generic_heap=hp_generic_heap,
	  				es_dynamics = [], es_calls = [], es_fun_defs = fun_defs}
	  e_input = { ei_expr_level = inc def_level, ei_fun_index = fun_index, ei_fun_level = inc def_level, ei_mod_index = mod_index, ei_local_functions_index_offset=local_functions_index_offset }
	  (fun_body, free_vars, e_state, e_info, cs) = checkFunctionBodies fun_body function_ident_for_errors e_input e_state e_info cs

	# {es_fun_defs,es_calls,es_var_heap,es_expr_heap,es_type_heaps,es_generic_heap,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
	  (fun_body, cs_error) = checkFunctionBodyIfMacro fun_kind fun_bo