checktypes.icl

implementation module checktypes

import StdEnv
import syntax, checksupport, check, typesupport, utilities,
		compilerSwitches //, RWSDebug


::	TypeSymbols = 
	{	ts_type_defs		:: !.{# CheckedTypeDef}
	,	ts_cons_defs 		:: !.{# ConsDef}
	,	ts_selector_defs	:: !.{# SelectorDef}
	,	ts_modules			:: !.{# DclModule}
	}
	
::	TypeInfo =
	{	ti_var_heap			:: !.VarHeap
	,	ti_type_heaps		:: !.TypeHeaps
	}

::	CurrentTypeInfo =
	{	cti_module_index	:: !Index
	,	cti_type_index		:: !Index
	,	cti_lhs_attribute	:: !TypeAttribute
	}

class bindTypes type :: !CurrentTypeInfo !type !(!*TypeSymbols, !*TypeInfo, !*CheckState)
	-> (!type, !TypeAttribute, !(!*TypeSymbols, !*TypeInfo, !*CheckState))

instance bindTypes AType
where
	bindTypes cti atype=:{at_attribute,at_type} ts_ti_cs
		# (at_type, type_attr, (ts, ti, cs)) = bindTypes cti at_type ts_ti_cs
		  cs_error = check_attr_of_type_var at_attribute at_type cs.cs_error
		  (combined_attribute, cs_error) = check_type_attribute at_attribute type_attr cti.cti_lhs_attribute cs_error
		= ({ atype & at_attribute = combined_attribute, at_type = at_type }, combined_attribute, (ts, ti, { cs & cs_error = cs_error }))
	where
		check_type_attribute :: !TypeAttribute !TypeAttribute !TypeAttribute !*ErrorAdmin -> (!TypeAttribute,!*ErrorAdmin)
		check_type_attribute TA_Anonymous type_attr root_attr error
			| try_to_combine_attributes type_attr root_attr
				= (root_attr, error)
				= (TA_Multi, checkError "conflicting attribution of type definition" "" error)
		check_type_attribute TA_Unique type_attr root_attr error
			| try_to_combine_attributes TA_Unique type_attr || try_to_combine_attributes TA_Unique root_attr
				= (TA_Unique, error)
				= (TA_Multi, checkError "conflicting attribution of type definition" "" error)
		check_type_attribute (TA_Var var) _ _ error
			= (TA_Multi, checkError var "attribute variable not allowed" error)
		check_type_attribute (TA_RootVar var) _ _ error
			= (TA_Multi, checkError var "attribute variable not allowed" error)
		check_type_attribute _ type_attr root_attr error
			= (type_attr, error)

		try_to_combine_attributes :: !TypeAttribute !TypeAttribute -> Bool
		try_to_combine_attributes TA_Multi _
			= True
		try_to_combine_attributes (TA_Var attr_var1) (TA_Var attr_var2)
			= attr_var1.av_name == attr_var2.av_name
		try_to_combine_attributes TA_Unique TA_Unique
			= True
		try_to_combine_attributes TA_Unique TA_Multi
			= True
		try_to_combine_attributes _ _
			= False

		check_attr_of_type_var :: !TypeAttribute !Type !*ErrorAdmin -> .ErrorAdmin 
		check_attr_of_type_var TA_Unique (TV var) error
			// the case "TA_Var" is catched by check_type_attribute
			= checkError var "uniqueness attribute not allowed" error
		check_attr_of_type_var attr _ error
			= error
		
instance bindTypes TypeVar
where
	bindTypes cti tv=:{tv_name=var_id=:{id_info}} (ts, ti, cs=:{cs_symbol_table})
		# (var_def, cs_symbol_table) = readPtr id_info cs_symbol_table
		  cs = { cs & cs_symbol_table = cs_symbol_table }
		= case var_def.ste_kind of
			STE_BoundTypeVariable bv=:{stv_attribute, stv_info_ptr, stv_count}
				# cs = { cs & cs_symbol_table = cs.cs_symbol_table <:= (id_info, { var_def & ste_kind = STE_BoundTypeVariable { bv & stv_count = inc stv_count }})}
				-> ({ tv & tv_info_ptr = stv_info_ptr}, stv_attribute, (ts, ti, cs))
			_
				-> (tv, TA_Multi, (ts, ti, { cs & cs_error = checkError var_id "undefined" cs.cs_error }))

instance bindTypes [a] | bindTypes a
where
	bindTypes cti [] ts_ti_cs
		= ([], TA_Multi, ts_ti_cs)
	bindTypes cti [x : xs] ts_ti_cs
		# (x, _, ts_ti_cs) = bindTypes cti x ts_ti_cs
		  (xs, attr, ts_ti_cs) = bindTypes cti xs ts_ti_cs
		= ([x : xs], attr, ts_ti_cs)
	

instance bindTypes Type
where
	bindTypes cti (TV tv) ts_ti_cs
		# (tv, attr, ts_ti_cs) = bindTypes cti tv ts_ti_cs
		= (TV tv, attr, ts_ti_cs)
	bindTypes cti=:{cti_module_index,cti_type_index,cti_lhs_attribute} type=:(TA type_cons=:{type_name=type_name=:{id_info}} types)
					(ts=:{ts_type_defs,ts_modules}, ti, cs=:{cs_symbol_table})
		# (entry, cs_symbol_table)	= readPtr id_info cs_symbol_table
		  cs = { cs & cs_symbol_table = cs_symbol_table }
		  (type_index, type_module)	= retrieveGlobalDefinition entry STE_Type cti_module_index
		| type_index <> NotFound
			# ({td_arity,td_attribute,td_rhs},type_index,ts_type_defs,ts_modules) = getTypeDef type_index type_module cti_module_index ts_type_defs ts_modules
			  ts = { ts & ts_type_defs = ts_type_defs, ts_modules = ts_modules }
			| checkArityOfType type_cons.type_arity td_arity td_rhs
				# (types, _, ts_ti_cs) = bindTypes cti types (ts, ti, cs)
				| type_module == cti_module_index && cti_type_index == type_index
					= (TA { type_cons & type_index = { glob_object = type_index, glob_module = type_module}} types, cti_lhs_attribute, ts_ti_cs)
					= (TA { type_cons & type_index = { glob_object = type_index, glob_module = type_module}} types,
								determine_type_attribute td_attribute, ts_ti_cs)
				= (TE /* JVG was: type */, TA_Multi, (ts, ti, { cs & cs_error = checkError type_cons.type_name "used with wrong arity" cs.cs_error }))
			= (TE /* JVG was: type */, TA_Multi, (ts, ti, { cs & cs_error = checkError type_cons.type_name "undefined" cs.cs_error}))
	where
		determine_type_attribute TA_Unique		= TA_Unique
		determine_type_attribute _				= TA_Multi
	
	bindTypes cti (arg_type --> res_type) ts_ti_cs
		# (arg_type, _, ts_ti_cs) = bindTypes cti arg_type ts_ti_cs
		  (res_type, _, ts_ti_cs) = bindTypes cti res_type ts_ti_cs
		= (arg_type --> res_type, TA_Multi, ts_ti_cs)
//AA..
	bindTypes cti (TArrow1 type) ts_ti_cs
		# (type, _, ts_ti_cs) = bindTypes cti type ts_ti_cs
		= (TArrow1 type, TA_Multi, ts_ti_cs)	
//..AA		
	bindTypes cti (CV tv :@: types) ts_ti_cs
		# (tv, type_attr, ts_ti_cs) = bindTypes cti tv ts_ti_cs
		  (types, _, ts_ti_cs) = bindTypes cti types ts_ti_cs
		= (CV tv :@: types, type_attr, ts_ti_cs)
// Sjaak 16-08-01
	bindTypes cti (TFA vars type) (ts, ti=:{ti_type_heaps}, cs)
		# (type_vars, (_, ti_type_heaps, cs)) = addTypeVariablesToSymbolTable cRankTwoScope vars [] ti_type_heaps cs
		  (type, _, (ts, ti, cs)) = bindTypes cti type (ts, {ti & ti_type_heaps = ti_type_heaps}, cs)
		  cs_symbol_table = removeAttributedTypeVarsFromSymbolTable cRankTwoScope type_vars cs.cs_symbol_table
		= (TFA type_vars type, TA_Multi, (ts, ti, { cs & cs_symbol_table = cs_symbol_table }))
// ... Sjaak
	bindTypes cti type ts_ti_cs
		= (type, TA_Multi, ts_ti_cs)
	

addToAttributeEnviron :: !TypeAttribute !TypeAttribute ![AttrInequality] !*ErrorAdmin -> (![AttrInequality],!*ErrorAdmin)
addToAttributeEnviron TA_Multi _ attr_env error
	= (attr_env, error)
addToAttributeEnviron _ TA_Unique attr_env error
	= (attr_env, error)
addToAttributeEnviron (TA_Var attr_var) (TA_Var root_var) attr_env error
	| attr_var.av_info_ptr == root_var.av_info_ptr
		= (attr_env, error)
		= ([ { ai_demanded = attr_var, ai_offered = root_var } :  attr_env], error)
addToAttributeEnviron (TA_RootVar attr_var) root_attr attr_env error
	= (attr_env, error)
addToAttributeEnviron _ _ attr_env error
	= (attr_env, checkError "inconsistent attribution of type definition" "" error)

bindTypesOfConstructors :: !CurrentTypeInfo !Index ![TypeVar] ![AttributeVar] !AType ![DefinedSymbol] !(!*TypeSymbols,!*TypeInfo,!*CheckState)
	-> (!*TypeSymbols, !*TypeInfo, !*CheckState)
bindTypesOfConstructors _ _ _ _ _ [] ts_ti_cs
	= ts_ti_cs
bindTypesOfConstructors cti=:{cti_lhs_attribute} cons_index free_vars free_attrs type_lhs [{ds_index}:conses] (ts=:{ts_cons_defs}, ti=:{ti_type_heaps}, cs)
	# (cons_def, ts_cons_defs) = ts_cons_defs![ds_index]
	# (exi_vars, (ti_type_heaps, cs))
	  		= addExistentionalTypeVariablesToSymbolTable cti_lhs_attribute cons_def.cons_exi_vars ti_type_heaps cs
	  (st_args, cons_arg_vars, st_attr_env, (ts, ti, cs))
	  		= bind_types_of_cons cons_def.cons_type.st_args cti free_vars []
	  				({ ts & ts_cons_defs = ts_cons_defs }, { ti  & ti_type_heaps = ti_type_heaps }, cs)
	  cs_symbol_table = removeAttributedTypeVarsFromSymbolTable cGlobalScope /* cOuterMostLevel */ exi_vars cs.cs_symbol_table
	  (ts, ti, cs) = bindTypesOfConstructors cti (inc cons_index) free_vars free_attrs type_lhs conses
							(ts, ti, { cs & cs_symbol_table = cs_symbol_table }) 
	  cons_type = { cons_def.cons_type & st_vars = free_vars, st_args = st_args, st_result = type_lhs, st_attr_vars = free_attrs, st_attr_env = st_attr_env }
	  (new_type_ptr, ti_var_heap) = newPtr VI_Empty ti.ti_var_heap
	= ({ ts & ts_cons_defs = { ts.ts_cons_defs & [ds_index] =
			{ cons_def & cons_type = cons_type, cons_index = cons_index, cons_type_index = cti.cti_type_index, cons_exi_vars = exi_vars,
					cons_type_ptr = new_type_ptr, cons_arg_vars = cons_arg_vars }}}, { ti & ti_var_heap = ti_var_heap }, cs)
where
	bind_types_of_cons :: ![AType] !CurrentTypeInfo ![TypeVar] ![AttrInequality] !(!*TypeSymbols, !*TypeInfo, !*CheckState)
		-> !(![AType], ![[ATypeVar]], ![AttrInequality], !(!*TypeSymbols, !*TypeInfo, !*CheckState))
	bind_types_of_cons [] cti free_vars attr_env ts_ti_cs
		= ([], [], attr_env, ts_ti_cs)
	bind_types_of_cons [type : types] cti free_vars attr_env ts_ti_cs
		# (types, local_vars_list, attr_env, ts_ti_cs)
				= bind_types_of_cons types cti free_vars attr_env ts_ti_cs
		  (type, type_attr, (ts, ti, cs)) = bindTypes cti type ts_ti_cs
		  (local_vars, cs_symbol_table) = foldSt retrieve_local_vars free_vars ([], cs.cs_symbol_table)
		  (attr_env, cs_error) = addToAttributeEnviron type_attr cti.cti_lhs_attribute attr_env cs.cs_error
		= ([type : types], [local_vars : local_vars_list], attr_env, (ts, ti , { cs & cs_symbol_table = cs_symbol_table, cs_error = cs_error }))
	where 
		retrieve_local_vars tv=:{tv_name={id_info}} (local_vars, symbol_table)
			# (ste=:{ste_kind = STE_BoundTypeVariable bv=:{stv_attribute, stv_info_ptr, stv_count }}, symbol_table) = readPtr id_info symbol_table
			| stv_count == 0
				= (local_vars, symbol_table)
				
				= ([{ atv_variable = { tv & tv_info_ptr = stv_info_ptr}, atv_attribute = stv_attribute, atv_annotation = AN_None } : local_vars],
						symbol_table <:= (id_info, { ste & ste_kind = STE_BoundTypeVariable { bv & stv_count = 0}}))
						
//
checkRhsOfTypeDef :: !CheckedTypeDef ![AttributeVar] !CurrentTypeInfo !(!*TypeSymbols, !*TypeInfo, !*CheckState)
	-> (!TypeRhs, !(!*TypeSymbols, !*TypeInfo, !*CheckState))
//
checkRhsOfTypeDef {td_name,td_arity,td_args,td_rhs = td_rhs=:AlgType conses} attr_vars cti=:{cti_module_index,cti_type_index,cti_lhs_attribute} ts_ti_cs
	# type_lhs = { at_annotation = AN_None, at_attribute = cti_lhs_attribute,
			  	   at_type = TA (MakeTypeSymbIdent { glob_object = cti_type_index, glob_module = cti_module_index } td_name td_arity)
								[{at_annotation = AN_None, at_attribute = atv_attribute,at_type = TV atv_variable} \\ {atv_variable, atv_attribute} <- td_args]}
	  ts_ti_cs = bindTypesOfConstructors cti 0 [ atv_variable \\ {atv_variable} <- td_args] attr_vars type_lhs conses ts_ti_cs
	= (td_rhs, ts_ti_cs)
checkRhsOfTypeDef {td_name,td_arity,td_args,td_rhs = td_rhs=:RecordType {rt_constructor=rec_cons=:{ds_index}, rt_fields}}
		attr_vars cti=:{cti_module_index,cti_type_index,cti_lhs_attribute} ts_ti_cs
	# type_lhs = {	at_annotation = AN_None, at_attribute = cti_lhs_attribute,
					at_type = TA (MakeTypeSymbIdent { glob_object = cti_type_index, glob_module = cti_module_index } td_name td_arity)
			[{at_annotation = AN_None, at_attribute = atv_attribute,at_type = TV atv_variable} \\ {atv_variable, atv_attribute} <- td_args]}
	  (ts, ti, cs) = bindTypesOfConstructors cti 0  [ atv_variable \\ {atv_variable} <- td_args]
	  						attr_vars type_lhs [rec_cons] ts_ti_cs
	# (rec_cons_def, ts) = ts!ts_cons_defs.[ds_index]
	# {cons_type = { st_vars,st_args,st_result,st_attr_vars }, cons_exi_vars} = rec_cons_def

	| size rt_fields<>length st_args
		= abort ("checkRhsOfTypeDef "+++rt_fields.[0].fs_name.id_name+++" "+++rec_cons_def.cons_symb.id_name+++toString ds_index)

	# (ts_selector_defs, ti_var_heap, cs_error) = check_selectors 0 rt_fields cti_type_index st_args st_result st_vars st_attr_vars cons_exi_vars
				ts.ts_selector_defs ti.ti_var_heap cs.cs_error
	= (td_rhs, ({ ts & ts_selector_defs = ts_selector_defs }, { ti & ti_var_heap = ti_var_heap }, { cs & cs_error = cs_error}))
where
	check_selectors :: !Index !{# FieldSymbol} !Index ![AType] !AType ![TypeVar] ![AttributeVar] ![ATypeVar] !*{#SelectorDef} !*VarHeap !*ErrorAdmin
		-> (!*{#SelectorDef}, !*VarHeap, !*ErrorAdmin)
	check_selectors field_nr fields rec_type_index sel_types rec_type st_vars st_attr_vars exi_vars selector_defs var_heap error
		| field_nr < size fields
			# {fs_index} = fields.[field_nr]
			# (sel_def, selector_defs) = selector_defs![fs_index]
			  [sel_type : sel_types] = sel_types
			# (sel_type, (st_vars, st_attr_vars)) = lift_quantifier sel_type (st_vars, st_attr_vars)
			# (st_attr_env, error) = addToAttributeEnviron sel_type.at_attribute rec_type.at_attribute [] error
			# (new_type_ptr, var_heap) = newPtr VI_Empty var_heap
			  sd_type = { sel_def.sd_type &  st_arity = 1, st_args = [rec_type], st_result = sel_type, st_vars = st_vars,
			  				st_attr_vars = st_attr_vars, st_attr_env = st_attr_env }
			  selector_defs = { selector_defs & [fs_index] = { sel_def & sd_type = sd_type, sd_field_nr = field_nr, sd_type_index = rec_type_index,
			  									sd_type_ptr = new_type_ptr, sd_exi_vars = exi_vars  } }
			= check_selectors (inc field_nr) fields rec_type_index sel_types  rec_type st_vars st_attr_vars exi_vars selector_defs var_heap error
			= (selector_defs, var_heap, error)
	where
		lift_quantifier at=:{at_type = TFA vars type} (type_vars, attr_vars)
			= ({ at & at_type = type}, foldSt add_var_and_attr vars (type_vars, attr_vars))
		lift_quantifier at (type_vars, attr_vars)
			= (at, (type_vars, attr_vars))
			
		add_var_and_attr {atv_variable, atv_attribute} (type_vars, attr_vars)
			= ([atv_variable : type_vars], add_attr_var atv_attribute attr_vars)

		add_attr_var (TA_Var av) attr_vars
			= [av : attr_vars]
		add_attr_var attr attr_vars
			= attr_vars
			
checkRhsOfTypeDef {td_rhs = SynType type} _ cti ts_ti_cs
	# (type, type_attr, ts_ti_cs) = bindTypes cti type ts_ti_cs
	= (SynType type, ts_ti_cs)
checkRhsOfTypeDef {td_rhs} _ _ ts_ti_cs
	= (td_rhs, ts_ti_cs)

emptyIdent name :== { id_name = name, id_info = nilPtr }

isATopConsVar cv		:== cv < 0
encodeTopConsVar cv		:== dec (~cv)
decodeTopConsVar cv		:== ~(inc cv)

checkTypeDef :: !Index !Index !*TypeSymbols !*TypeInfo !*CheckState -> (!*TypeSymbols, !*TypeInfo, !*CheckState);
checkTypeDef type_index module_index ts=:{ts_type_defs} ti=:{ti_type_heaps} cs=:{cs_error}
	# (type_def, ts_type_defs) = ts_type_defs![type_index]
	# {td_name,td_pos,td_args,td_attribute} = type_def
	# position = newPosition td_name td_pos
	  cs_error = pushErrorAdmin position cs_error
	  (td_attribute, attr_vars, th_attrs) = determine_root_attribute td_attribute td_name.id_name ti_type_heaps.th_attrs
	  (type_vars, (attr_vars, ti_type_heaps, cs))
	  		= addTypeVariablesToSymbolTable cGlobalScope td_args attr_vars { ti_type_heaps & th_attrs = th_attrs } { cs & cs_error = cs_error }
	  type_def = {	type_def & td_args = type_vars, td_index = type_index, td_attrs = attr_vars, td_attribute = td_attribute }
	  (td_rhs, (ts, ti, cs)) = checkRhsOfTypeDef type_def attr_vars
			{ cti_module_index = module_index, cti_type_index = type_index, cti_lhs_attribute = td_attribute }
				({ ts & ts_type_defs = ts_type_defs },{ ti & ti_type_heaps = ti_type_heaps}, cs)
	= ({ ts & ts_type_defs = { ts.ts_type_defs & [type_index] = { type_def & td_rhs = td_rhs }}}, ti,
				{ cs &	cs_error = popErrorAdmin cs.cs_error,
						cs_symbol_table = removeAttributedTypeVarsFromSymbolTable cGlobalScope /* cOuterMostLevel */ type_vars cs.cs_symbol_table})
where
	determine_root_attribute TA_None name attr_var_heap
		# (attr_info_ptr, attr_var_heap) = newPtr AVI_Empty attr_var_heap
		  new_var = { av_name = emptyIdent name, av_info_ptr = attr_info_ptr}
		= (TA_Var new_var, [new_var], attr_var_heap)
	determine_root_attribute TA_Unique name attr_var_heap
		= (TA_Unique, [], attr_var_heap)


CS_Checked	:== 1
CS_Checking	:== 0

::	ExpandState =
	{	exp_type_defs	::!.{# CheckedTypeDef}
	,	exp_modules		::!.{# DclModule}
	,	exp_marks		::!.{# Int}
	,	exp_type_heaps	::!.TypeHeaps
	,	exp_error		::!.ErrorAdmin
	}

class expand a :: !Index !a  !*ExpandState -> (!a, !*ExpandState)

expandTypeVariable :: TypeVar !*ExpandState -> (!Type, !*ExpandState)
expandTypeVariable {tv_info_ptr} expst=:{exp_type_heaps}
	# (TVI_Type type, th_vars) = readPtr tv_info_ptr exp_type_heaps.th_vars
	= (type, { expst & exp_type_heaps = { exp_type_heaps & th_vars  = th_vars }})

expandTypeAttribute :: !TypeAttribute !*ExpandState -> (!TypeAttribute, !*ExpandState)
expandTypeAttribute (TA_Var {av_info_ptr}) expst=:{exp_type_heaps}
	# (AVI_Attr attr, th_attrs) = readPtr av_info_ptr exp_type_heaps.th_attrs
	= (attr, { expst & exp_type_heaps = { exp_type_heaps & th_attrs = th_attrs }})
expandTypeAttribute attr expst
	= (attr, expst)

instance expand Type
where
	expand module_index (TV tv) expst
		= expandTypeVariable tv expst
	expand module_index type=:(TA type_cons=:{type_name,type_index={glob_object,glob_module}} types) expst=:{exp_marks,exp_error}
		| module_index == glob_module
			#! mark = exp_marks.[glob_object]
			| mark == CS_NotChecked
				# expst = expandSynType module_index glob_object expst
				  (types, expst) = expand module_index types expst
				= (TA type_cons types,expst)
			| mark == CS_Checked
				# (types, expst) = expand module_index types expst
				= (TA type_cons types, expst)
//			| mark == CS_Checking
				= (type, { expst & exp_error = checkError type_name "cyclic dependency between type synonyms" exp_error })
			# (types, expst) = expand module_index types expst
			= (TA type_cons types, expst)
	expand module_index (arg_type --> res_type) expst
		# (arg_type, expst) = expand module_index arg_type expst
		  (res_type, expst) = expand module_index res_type expst
		= (arg_type --> res_type, expst)
// AA..
	expand module_index (TArrow1 type) expst
		# (type, expst) = expand module_index type expst
		= (TArrow1 type, expst)
// ..AA				
	expand module_index (CV tv=:{tv_name} :@: types) expst
		# (type, expst) = expandTypeVariable tv expst
		  (types, expst) = expand module_index types expst
		  (combined_type, exp_error) = simplify_type_appl tv_name type types expst.exp_error
		= (combined_type, { expst & exp_error = exp_error }) 
		where
			simplify_type_appl :: !Ident !Type ![AType] !*ErrorAdmin -> (!Type, *ErrorAdmin)
			simplify_type_appl cv (TA type_cons=:{type_arity} cons_args) type_args error
				= (TA { type_cons & type_arity = type_arity + length type_args } (cons_args ++ type_args), error)
			simplify_type_appl cv (TV tv) type_args error
				= (CV tv :@: type_args, error)
			simplify_type_appl cv TE t2 error
				= (TE, error)
			simplify_type_appl cv t1 t2 error
				= (TE, checkError cv "kind conflict in argument of type synonym" error)
				
	expand module_index (TFA vars type) expst
		# (type, expst) = expand module_index type expst
		= (TFA vars type, expst)
	expand module_index type expst
		= (type, expst)

instance expand [a] | expand a
where
	expand module_index [x:xs] expst
		# (x, expst) = expand module_index x expst
		  (xs, expst) = expand module_index xs expst
		= ([x:xs], expst)
	expand module_index [] expst
		= ([], expst)

instance expand AType
where
	expand module_index atype=:{at_type,at_attribute} expst
		# (at_attribute, expst) = expandTypeAttribute at_attribute expst
		  (at_type, expst) = expand module_index at_type expst
		= ({ atype & at_type = at_type, at_attribute = at_attribute }, expst)
/*
expandTypeApplication (CV tv={tv_name}) types expst
	# (type, expst) = expandTypeVariable tv expst
	  (types, expst) = expand module_index types expst
	  (combined_type, exp_error) = simplify_type_appl tv_name type types expst.exp_error
	= (simplify_type_appl type types, { expst & exp_error = exp_error }) 
	where
		simplify_type_appl :: !Ident !Type ![AType] !*ErrorAdmin -> (!Type, *ErrorAdmin)
		simplify_type_appl cv (TA type_cons=:{type_arity} cons_args) type_args error
			= (TA { type_cons & type_arity = type_arity + length type_args } (cons_args ++ type_args), error)
		simplify_type_appl cv (TV tv) type_args error
			= (CV tv :@: type_args, error)
		simplify_type_appl cv TE t2 error
			= (TE, error)
		simplify_type_appl cv t1 t2 error
			= (TE, checkError cv "kind conflict in argument of type synonym" error)
*/


class look_for_cycles a :: !Index !a !*ExpandState -> *ExpandState

instance look_for_cycles Type
where
	look_for_cycles module_index type=:(TA type_cons=:{type_name,type_index={glob_object,glob_module}} types) expst=:{exp_marks,exp_error}
		| module_index == glob_module
			#! mark = exp_marks.[glob_object]
			| mark == CS_NotChecked
				# expst = expandSynType module_index glob_object expst
				= look_for_cycles module_index types expst
			| mark == CS_Checked
				= look_for_cycles module_index types expst
				= { expst & exp_error = checkError type_name "cyclic dependency between type synonyms" exp_error }
		= look_for_cycles module_index types expst
	look_for_cycles module_index (arg_type --> res_type) expst
		= look_for_cycles module_index res_type (look_for_cycles module_index arg_type expst)
//AA..
	look_for_cycles module_index (TArrow1 arg_type) expst
		= look_for_cycles module_index arg_type expst
//..AA
	look_for_cycles module_index (type :@: types) expst
		= look_for_cycles module_index types expst
	look_for_cycles module_index type expst
		= expst
	
instance look_for_cycles [a] | look_for_cycles a
where
	look_for_cycles mod_index l expst
		= foldr (look_for_cycles mod_index) expst l

instance look_for_cycles AType
where
	look_for_cycles mod_index {at_type} expst
		= look_for_cycles mod_index at_type expst

import StdDebug

expandSynType ::  !Index !Index !*ExpandState -> *ExpandState
expandSynType mod_index type_index expst=:{exp_type_defs}
	# (type_def, exp_type_defs) = exp_type_defs![type_index]
	  expst = { expst & exp_type_defs = exp_type_defs }
	= case type_def.td_rhs of
		SynType type=:{at_type = TA {type_name,type_index={glob_object,glob_module}} types}		
	   		# ({td_args,td_attribute,td_rhs}, _, exp_type_defs, exp_modules) = getTypeDef glob_object glob_module mod_index expst.exp_type_defs expst.exp_modules
	   		  expst = { expst & exp_type_defs = exp_type_defs, exp_modules = exp_modules }
			-> case td_rhs of
				SynType rhs_type
					# exp_type_heaps = bindTypeVarsAndAttributes td_attribute type_def.td_attribute td_args types expst.exp_type_heaps
					  position = newPosition type_def.td_name type_def.td_pos
					  exp_error = pushErrorAdmin position expst.exp_error
	  		  		  exp_marks = { expst.exp_marks & [type_index] = CS_Checking }			  
					  (exp_type, expst) = expand mod_index rhs_type.at_type { expst & exp_marks = exp_marks,
										exp_error = exp_error, exp_type_heaps = exp_type_heaps }
					-> {expst & exp_type_defs = { expst.exp_type_defs & [type_index] = { type_def & td_rhs = SynType { type & at_type = exp_type }}},
						 		exp_marks = { expst.exp_marks & [type_index] = CS_Checked },
						 		exp_type_heaps = clearBindingsOfTypeVarsAndAttributes td_attribute td_args expst.exp_type_heaps,
								exp_error = popErrorAdmin expst.exp_error }
//										---> ("SynType", rhs_type, exp_type)

				_
					# exp_marks = { expst.exp_marks & [type_index] = CS_Checking }
					  position = newPosition type_def.td_name type_def.td_pos
	  		  		  expst = look_for_cycles mod_index types { expst & exp_marks = exp_marks, exp_error = pushErrorAdmin position expst.exp_error }
					-> { expst & exp_marks = { expst.exp_marks & [type_index] = CS_Checked }, exp_error = popErrorAdmin expst.exp_error }
		_
			-> { expst &  exp_marks = { expst.exp_marks & [type_index] = CS_Checked }}

checkTypeDefs :: !Bool !*{# CheckedTypeDef} !Index !*{# ConsDef} !*{# SelectorDef} !*{# DclModule} !*VarHeap !*TypeHeaps !*CheckState
	-> (!*{# CheckedTypeDef}, !*{# ConsDef}, !*{# SelectorDef}, !*{# DclModule}, !*VarHeap, !*TypeHeaps, !*CheckState)
checkTypeDefs is_main_dcl type_defs module_index  cons_defs selector_defs modules var_heap type_heaps cs
	#! nr_of_types = size type_defs
	#  ts = { ts_type_defs = type_defs, ts_cons_defs = cons_defs, ts_selector_defs = selector_defs, ts_modules = modules }
	   ti = { ti_type_heaps = type_heaps, ti_var_heap = var_heap  }
	= check_type_defs is_main_dcl 0 nr_of_types module_index ts ti cs
where
	check_type_defs is_main_dcl type_index nr_of_types module_index ts ti=:{ti_type_heaps,ti_var_heap} cs
		| type_index == nr_of_types
			= (ts.ts_type_defs, ts.ts_cons_defs, ts.ts_selector_defs, ts.ts_modules, ti_var_heap, ti_type_heaps, cs)
			# (ts, ti, cs) = checkTypeDef  type_index module_index ts ti cs
			= check_type_defs is_main_dcl (inc type_index) nr_of_types module_index ts ti cs

/*
Tracea_tn a
	# s=size a
	# f=stderr
	# r=t 0 f
	  with
	  	t i f
	  		| i<s && file_to_true (stderr <<< i <<< '\n' <<< a.[i] <<< '\n')
	  			= t (i+1) f
	  			= True
	 = r

file_to_true :: !File -> Bool;
file_to_true file = code {
  .inline file_to_true
          pop_b 2
          pushB TRUE
  .end
 }
*/

expandSynonymTypes :: !.Index !*{#CheckedTypeDef} !*{#.DclModule} !*TypeHeaps !*ErrorAdmin
	-> (!.{#CheckedTypeDef},!.{#DclModule},!.TypeHeaps,!.ErrorAdmin)
expandSynonymTypes module_index exp_type_defs exp_modules exp_type_heaps exp_error
	#! nr_of_types
			= size exp_type_defs
	# marks 
			= createArray nr_of_types CS_NotChecked
	  {exp_type_defs,exp_modules,exp_type_heaps,exp_error}
			= expand_syn_types module_index 0 nr_of_types
			  		{	exp_type_defs = exp_type_defs, exp_modules = exp_modules, exp_marks = marks,
			  			exp_type_heaps = exp_type_heaps, exp_error = exp_error }
	= (exp_type_defs,exp_modules,exp_type_heaps,exp_error)
where
	expand_syn_types module_index type_index nr_of_types expst
		| type_index == nr_of_types
			= expst
		| expst.exp_marks.[type_index] == CS_NotChecked
			# expst = expandSynType module_index type_index expst
			= expand_syn_types module_index (inc type_index) nr_of_types expst
			= expand_syn_types module_index (inc type_index) nr_of_types expst

::	OpenTypeInfo =
	{	oti_heaps		:: !.TypeHeaps
	,	oti_all_vars	:: ![TypeVar]
	,	oti_all_attrs	:: ![AttributeVar]
	,	oti_global_vars	:: ![TypeVar]
	}

::	OpenTypeSymbols =
	{	ots_type_defs	:: .{# CheckedTypeDef}
	,	ots_modules		:: .{# DclModule}
	}

determineAttributeVariable attr_var=:{av_name=attr_name=:{id_info}} oti=:{oti_heaps,oti_all_attrs} symbol_table
	# (entry=:{ste_kind,ste_def_level}, symbol_table) = readPtr id_info symbol_table
	| ste_kind == STE_Empty || ste_def_level == cModuleScope
		#! (new_attr_ptr, th_attrs) = newPtr AVI_Empty oti_heaps.th_attrs
		# symbol_table = symbol_table <:= (id_info,{	ste_index = NoIndex, ste_kind = STE_TypeAttribute new_attr_ptr,
														ste_def_level = cGlobalScope, ste_previous = entry })
		  new_attr = { attr_var & av_info_ptr = new_attr_ptr}
		= (new_attr, { oti & oti_heaps = { oti_heaps & th_attrs = th_attrs }, oti_all_attrs = [new_attr : oti_all_attrs] }, symbol_table)
		# (STE_TypeAttribute attr_ptr) = ste_kind
		= ({ attr_var & av_info_ptr = attr_ptr}, oti, symbol_table)

::	DemandedAttributeKind = DAK_Ignore | DAK_Unique | DAK_None

newAttribute :: !DemandedAttributeKind {#Char} TypeAttribute !*OpenTypeInfo !*CheckState -> (!TypeAttribute, !*OpenTypeInfo, !*CheckState)
newAttribute DAK_Ignore var_name _ oti cs
	= (TA_Multi, oti, cs)
newAttribute DAK_Unique var_name new_attr  oti cs
	= case new_attr of
		TA_Unique
			-> (TA_Unique, oti, cs)
		TA_Multi
			-> (TA_Unique, oti, cs)
		TA_None
			-> (TA_Unique, oti, cs)
		_
			-> (TA_Unique, oti, { cs & cs_error = checkError var_name "inconsistently attributed (2)" cs.cs_error })
newAttribute DAK_None var_name (TA_Var attr_var) oti cs=:{cs_symbol_table}
	# (attr_var, oti, cs_symbol_table) = determineAttributeVariable attr_var oti cs_symbol_table
	= (TA_Var attr_var, oti, { cs & cs_symbol_table = cs_symbol_table })
newAttribute DAK_None var_name TA_Anonymous oti=:{oti_heaps, oti_all_attrs} cs
	# (new_attr_ptr, th_attrs) = newPtr AVI_Empty oti_heaps.th_attrs
	  new_attr = { av_info_ptr = new_attr_ptr, av_name = emptyIdent var_name }
	= (TA_Var new_attr, { oti & oti_heaps = { oti_heaps & th_attrs = th_attrs }, oti_all_attrs = [new_attr : oti_all_attrs] }, cs)
newAttribute DAK_None var_name TA_Unique oti cs
	= (TA_Unique, oti, cs)
newAttribute DAK_None var_name attr oti cs
	= (TA_Multi, oti, cs)
			

getTypeDef :: !Index !Index !Index !u:{# CheckedTypeDef} !v:{# DclModule} -> (!CheckedTypeDef, !Index , !u:{# CheckedTypeDef}, !v:{# DclModule})
getTypeDef type_index type_module module_index type_defs modules
	| type_module == module_index
		# (type_def, type_defs) = type_defs![type_index]
		= (type_def, type_index, type_defs, modules)
		# ({dcl_common={com_type_defs},dcl_conversions}, modules) = modules![type_module]
		  type_def = com_type_defs.[type_index]
		  type_index = convertIndex type_index (toInt STE_Type) dcl_conversions
		= (type_def, type_index, type_defs, modules)

checkArityOfType act_arity form_arity (SynType _)
	= form_arity == act_arity
checkArityOfType act_arity form_arity _
	= form_arity >= act_arity

getClassDef :: !Index !Index !Index !u:{# ClassDef} !v:{# DclModule} -> (!ClassDef, !Index , !u:{# ClassDef}, !v:{# DclModule})
getClassDef class_index type_module module_index class_defs modules
	| type_module == module_index
		#! si = size class_defs
		# (class_def, class_defs) = class_defs![class_index]
		= (class_def, class_index, class_defs, modules)
		# ({dcl_common={com_class_defs},dcl_conversions}, modules) = modules![type_module]
		  class_def = com_class_defs.[class_index]
		  class_index = convertIndex class_index (toInt STE_Class) dcl_conversions
		= (class_def, class_index, class_defs, modules)

getGenericDef :: !Index !Index !Index !u:{# GenericDef} !v:{# DclModule} -> (!GenericDef, !Index , !u:{# GenericDef}, !v:{# DclModule})
getGenericDef generic_index type_module module_index generic_defs modules
	| type_module == module_index
		#! si = size generic_defs
		# (generic_def, generic_defs) = generic_defs![generic_index]
		= (generic_def, generic_index, generic_defs, modules)
		# ({dcl_common={com_generic_defs},dcl_conversions}, modules) = modules![type_module]
		  generic_def = com_generic_defs.[generic_index]
		  generic_index = convertIndex generic_index (toInt STE_Generic) dcl_conversions
		= (generic_def, generic_index, generic_defs, modules)

checkTypeVar :: !Level !DemandedAttributeKind !TypeVar !TypeAttribute !(!*OpenTypeInfo, !*CheckState)
					-> (! TypeVar, !TypeAttribute, !(!*OpenTypeInfo, !*CheckState))
checkTypeVar scope dem_attr tv=:{tv_name=var_name=:{id_name,id_info}} tv_attr (oti, cs=:{cs_symbol_table})
	# (entry=:{ste_kind,ste_def_level},cs_symbol_table) = readPtr id_info cs_symbol_table
	| ste_kind == STE_Empty || ste_def_level == cModuleScope
		# (new_attr, oti=:{oti_heaps,oti_all_vars}, cs) = newAttribute dem_attr id_name tv_attr oti { cs & cs_symbol_table = cs_symbol_table }
		  (new_var_ptr, th_vars) = newPtr (TVI_Attribute new_attr) oti_heaps.th_vars
		  new_var = { tv & tv_info_ptr = new_var_ptr }
		= (new_var, new_attr, ({ oti & oti_heaps = { oti_heaps & th_vars = th_vars }, oti_all_vars = [new_var : oti_all_vars]},
				{ cs & cs_symbol_table = cs.cs_symbol_table <:= (id_info, {ste_index = NoIndex, ste_kind = STE_TypeVariable new_var_ptr,
								ste_def_level = scope, ste_previous = entry })}))
		# (STE_TypeVariable tv_info_ptr) = ste_kind
		  {oti_heaps} = oti
		  (var_info, th_vars) = readPtr tv_info_ptr oti_heaps.th_vars
		  (var_attr, oti, cs) = check_attribute id_name dem_attr var_info tv_attr { oti & oti_heaps = { oti_heaps & th_vars = th_vars }}
		  								{ cs & cs_symbol_table = cs_symbol_table }
		= ({ tv & tv_info_ptr = tv_info_ptr }, var_attr, (oti, cs))
where
	check_attribute var_name DAK_Ignore (TVI_Attribute prev_attr) this_attr oti cs=:{cs_error}
		= (TA_Multi, oti, cs)
	check_attribute var_name dem_attr (TVI_Attribute prev_attr) this_attr oti cs=:{cs_error}
		# (new_attr, cs_error) = determine_attribute var_name dem_attr this_attr cs_error
		= check_var_attribute prev_attr new_attr oti { cs & cs_error = cs_error }
	where					
		check_var_attribute (TA_Var old_var) (TA_Var new_var) oti cs=:{cs_symbol_table,cs_error}
			# (new_var, oti, cs_symbol_table) = determineAttributeVariable new_var oti cs_symbol_table
			| old_var.av_info_ptr == new_var.av_info_ptr
				= (TA_Var old_var, oti, { cs &  cs_symbol_table = cs_symbol_table })
				= (TA_Var old_var, oti, { cs &  cs_symbol_table = cs_symbol_table,
						cs_error = checkError new_var.av_name "inconsistently attributed (3)" cs_error })
		check_var_attribute var_attr=:(TA_Var old_var) TA_Anonymous oti cs
			= (var_attr, oti, cs)
		check_var_attribute TA_Unique new_attr oti cs
			= case new_attr of
				TA_Unique
					-> (TA_Unique, oti, cs)
				_
					-> (TA_Unique, oti, { cs & cs_error = checkError var_name "inconsistently attributed (4)" cs.cs_error })
		check_var_attribute TA_Multi new_attr oti cs
			= case new_attr of
				TA_Multi
					-> (TA_Multi, oti, cs)
				TA_None
					-> (TA_Multi, oti, cs)
				_
					-> (TA_Multi, oti, { cs & cs_error = checkError var_name "inconsistently attributed (5)" cs.cs_error })
		check_var_attribute var_attr new_attr oti cs
			= (var_attr, oti, { cs & cs_error = checkError var_name "inconsistently attributed (6)" cs.cs_error })// ---> (var_attr, new_attr)
		
		
		determine_attribute var_name DAK_Unique new_attr error
			= case new_attr of
				 TA_Multi
				 	-> (TA_Unique, error)
				 TA_None
				 	-> (TA_Unique, error)
				 TA_Unique
				 	-> (TA_Unique, error)
				 _
				 	-> (TA_Unique, checkError var_name "inconsistently attributed (1)" error)
		determine_attribute var_name dem_attr TA_None error
			= (TA_Multi, error)
		determine_attribute var_name dem_attr new_attr error
			= (new_attr, error)

	check_attribute var_name dem_attr _ this_attr oti cs
		= (TA_Multi, oti, cs)

checkOpenAType :: !Index !Int !DemandedAttributeKind !AType !(!u:OpenTypeSymbols, !*OpenTypeInfo, !*CheckState)
	-> (!AType, !(!u:OpenTypeSymbols, !*OpenTypeInfo, !*CheckState))
checkOpenAType mod_index scope dem_attr type=:{at_type = TV tv, at_attribute} (ots, oti, cs)
	# (tv, at_attribute, (oti, cs)) = checkTypeVar scope dem_attr tv at_attribute (oti, cs) 
	= ({ type & at_type = TV tv, at_attribute = at_attribute }, (ots, oti, cs))
checkOpenAType mod_index scope dem_attr type=:{at_type = GTV var_id=:{tv_name={id_info}}} (ots, oti=:{oti_heaps,oti_global_vars}, cs=:{cs_symbol_table})
	# (entry, cs_symbol_table) = readPtr id_info cs_symbol_table
	  (type_var, oti_global_vars, th_vars, entry) = retrieve_global_variable var_id entry oti_global_vars oti_heaps.th_vars
	= ({type & at_type = TV type_var, at_attribute = TA_Multi }, (ots, { oti & oti_heaps = { oti_heaps & th_vars = th_vars }, oti_global_vars = oti_global_vars },
								{ cs & cs_symbol_table = cs_symbol_table <:= (id_info, entry) }))
where
	retrieve_global_variable var entry=:{ste_kind = STE_Empty} global_vars var_heap
		# (new_var_ptr, var_heap) = newPtr TVI_Used var_heap
		  var = { var & tv_info_ptr = new_var_ptr }
		= (var, [var : global_vars], var_heap, 
				{ entry  & ste_kind = STE_TypeVariable new_var_ptr, ste_def_level = cModuleScope, ste_previous = entry }) 
	retrieve_global_variable var entry=:{ste_kind,ste_def_level, ste_previous} global_vars var_heap
		| ste_def_level == cModuleScope
			= case ste_kind of
				STE_TypeVariable glob_info_ptr
					# var = { var & tv_info_ptr = glob_info_ptr }
					  (var_info, var_heap) = readPtr glob_info_ptr var_heap
					-> case var_info of
						TVI_Empty
							-> (var, [var : global_vars], var_heap <:= (glob_info_ptr, TVI_Used), entry)
						TVI_Used
							-> (var, global_vars, var_heap, entry)
			# (var, global_vars, var_heap, ste_previous) = retrieve_global_variable var ste_previous global_vars var_heap
			= (var, global_vars, var_heap, { entry & ste_previous = ste_previous })
//
checkOpenAType mod_index scope dem_attr type=:{ at_type=TA type_cons=:{type_name=type_name=:{id_name,id_info}} types, at_attribute}
		(ots=:{ots_type_defs,ots_modules}, oti, cs=:{cs_symbol_table})
	# (entry, cs_symbol_table) = readPtr id_info cs_symbol_table
	  cs = { cs & cs_symbol_table = cs_symbol_table }
	  (type_index, type_module) = retrieveGlobalDefinition entry STE_Type mod_index
	| type_index <> NotFound
		# ({td_arity,td_args,td_attribute,td_rhs},type_index,ots_type_defs,ots_modules) = getTypeDef type_index type_module mod_index ots_type_defs ots_modules
		  ots = { ots & ots_type_defs = ots_type_defs, ots_modules = ots_modules }
		| checkArityOfType type_cons.type_arity td_arity td_rhs
			# type_cons = { type_cons & type_index = { glob_object = type_index, glob_module = type_module }}
			  (types, (ots, oti, cs)) = check_args_of_type_cons mod_index scope /* dem_attr */ types td_args (ots, oti, cs)
			  (new_attr, oti, cs) = newAttribute (new_demanded_attribute dem_attr td_attribute) id_name at_attribute oti cs
			= ({ type & at_type = TA type_cons types, at_attribute = new_attr } , (ots, oti, cs)) 
			= (type, (ots, oti, {cs & cs_error = checkError type_name "used with wrong arity" cs.cs_error}))
		= (type, (ots, oti, {cs & cs_error = checkError type_name "undefined" cs.cs_error}))
where
	check_args_of_type_cons :: !Index !Int ![AType] ![ATypeVar] !(!u:OpenTypeSymbols, !*OpenTypeInfo, !*CheckState)
		-> (![AType], !(!u:OpenTypeSymbols, !*OpenTypeInfo, !*CheckState))
	check_args_of_type_cons mod_index scope [] _ cot_state
		= ([], cot_state)
	check_args_of_type_cons mod_index scope [arg_type : arg_types] [ {atv_attribute} : td_args ] cot_state
		# (arg_type, cot_state) = checkOpenAType mod_index scope (new_demanded_attribute DAK_None atv_attribute) arg_type cot_state
		  (arg_types, cot_state) = check_args_of_type_cons mod_index scope arg_types td_args cot_state
		= ([arg_type : arg_types], cot_state)

	new_demanded_attribute DAK_Ignore _
		= DAK_Ignore
	new_demanded_attribute _ TA_Unique
		= DAK_Unique
	new_demanded_attribute dem_attr _
		= dem_attr

checkOpenAType mod_index scope dem_attr type=:{at_type = arg_type --> result_type, at_attribute} cot_state
	# (arg_type, cot_state) = checkOpenAType mod_index scope DAK_None arg_type cot_state
	  (result_type, (ots, oti, cs)) = checkOpenAType mod_index scope DAK_None result_type cot_state
	  (new_attr, oti, cs) = newAttribute dem_attr "-->" at_attribute oti cs
	= ({ type & at_type = arg_type --> result_type, at_attribute = new_attr }, (ots, oti, cs))
//AA..
checkOpenAType mod_index scope dem_attr type=:{at_type = TArrow1 arg_type, at_attribute} cot_state
	# (arg_type, (ots, oti, cs)) = checkOpenAType mod_index scope DAK_None arg_type cot_state
	  (new_attr, oti, cs) = newAttribute dem_attr "TArrow1" at_attribute oti cs
	= ({ type & at_type = TArrow1 arg_type, at_attribute = new_attr }, (ots, oti, cs))
//..AA
checkOpenAType mod_index scope dem_attr type=:{at_type = CV tv :@: types, at_attribute} (ots, oti, cs)
	# (cons_var, _, (oti, cs)) = checkTypeVar scope DAK_None tv TA_Multi (oti, cs)
	  (types, (ots, oti, cs)) = mapSt (checkOpenAType mod_index scope DAK_None) types (ots, oti, cs)
	  (new_attr, oti, cs) = newAttribute dem_attr ":@:" at_attribute oti cs
	= ({ type & at_type = CV cons_var :@: types, at_attribute = new_attr }, (ots, oti, cs))
checkOpenAType mod_index scope dem_attr atype=:{at_type = TFA vars type, at_attribute} (ots, oti, cs)
	# (vars, (oti, cs)) = mapSt add_universal_var vars  (oti, cs) 
	  (checked_type, (ots, oti, cs)) = checkOpenAType mod_index cRankTwoScope dem_attr { atype & at_type = type } (ots, oti, cs)
	  cs = { cs & cs_symbol_table = foldSt remove_universal_var vars cs.cs_symbol_table }
	= ( { checked_type & at_type = TFA vars checked_type.at_type }, (ots, oti, cs))
where
	add_universal_var atv=:{atv_variable = tv=:{tv_name={id_name,id_info}}, atv_attribute} (oti, cs=:{cs_symbol_table,cs_error})
		# (entry=:{ste_kind,ste_def_level},cs_symbol_table) = readPtr id_info cs_symbol_table
		| ste_kind == STE_Empty || ste_def_level < cRankTwoScope
			# (new_attr, oti=:{oti_heaps}, cs) = newAttribute DAK_None id_name atv_attribute oti { cs & cs_symbol_table = cs_symbol_table }
			  (new_var_ptr, th_vars) = newPtr (TVI_Attribute new_attr) oti_heaps.th_vars
			= ({atv & atv_variable = { tv & tv_info_ptr = new_var_ptr}, atv_attribute = new_attr }, 
					({ oti & oti_heaps = { oti_heaps & th_vars = th_vars }}, { cs & cs_symbol_table =
							cs.cs_symbol_table <:= (id_info, {ste_index = NoIndex, ste_kind = STE_TypeVariable new_var_ptr,
									ste_def_level = cRankTwoScope, ste_previous = entry })}))
			= (atv, (oti, { cs & cs_error = checkError id_name "type variable already undefined" cs_error, cs_symbol_table = cs_symbol_table }))

	remove_universal_var {atv_variable = {tv_name}, atv_attribute = TA_Var {av_name}} cs_symbol_table
		= removeDefinitionFromSymbolTable cGlobalScope av_name (removeDefinitionFromSymbolTable cRankTwoScope tv_name cs_symbol_table)
	remove_universal_var {atv_variable = {tv_name}} cs_symbol_table
		= removeDefinitionFromSymbolTable cRankTwoScope tv_name cs_symbol_table

checkOpenAType mod_index scope dem_attr type=:{at_attribute} (ots, oti, cs)
	# (new_attr, oti, cs) = newAttribute dem_attr "." at_attribute oti cs
	= ({ type & at_attribute = new_attr}, (ots, oti, cs))

checkOpenTypes mod_index scope dem_attr types cot_state
	= mapSt (checkOpenType mod_index scope dem_attr) types cot_state

checkOpenType mod_index scope dem_attr type cot_state
	# ({at_type}, cot_state) = checkOpenAType mod_index scope dem_attr { at_type = type, at_attribute = TA_Multi, at_annotation = AN_None } cot_state
	= (at_type, cot_state)
	
checkOpenATypes mod_index scope types cot_state
	= mapSt (checkOpenAType mod_index scope DAK_None) types cot_state

checkInstanceType :: !Index !(Global DefinedSymbol) !InstanceType !Specials !u:{# CheckedTypeDef} !v:{# ClassDef} !u:{# DclModule} !*TypeHeaps !*CheckState
	-> (!InstanceType, !Specials, !u:{# CheckedTypeDef}, !v:{# ClassDef}, !u:{# DclModule}, !*TypeHeaps, !*CheckState)
checkInstanceType mod_index ins_class it=:{it_types,it_context} specials type_defs class_defs modules heaps cs
	# cs_error
			= check_fully_polymorphity it_types it_context cs.cs_error
	  ots = { ots_type_defs = type_defs, ots_modules = modules }
	  oti = { oti_heaps = heaps, oti_all_vars = [], oti_all_attrs = [], oti_global_vars= [] }
	  (it_types, (ots, oti=:{oti_all_vars = it_vars, oti_all_attrs = it_attr_vars}, cs))
	  	= checkOpenTypes mod_index cGlobalScope DAK_None it_types (ots, oti, { cs & cs_error = cs_error })
	  oti = { oti &  oti_all_vars = [], oti_all_attrs = [] }
	  (it_context, type_defs, class_defs, modules, heaps, cs) = checkTypeContexts it_context mod_index class_defs ots oti cs
	  cs_error = foldSt (compare_context_and_instance_types ins_class it_types) it_context cs.cs_error
	  (specials, cs) = checkSpecialTypeVars specials { cs & cs_error = cs_error }
	  cs_symbol_table = removeVariablesFromSymbolTable cGlobalScope it_vars cs.cs_symbol_table
	  cs_symbol_table = removeAttributesFromSymbolTable it_attr_vars cs_symbol_table
	  (specials, type_defs, modules, heaps, cs) = checkSpecialTypes mod_index specials type_defs modules heaps { cs & cs_symbol_table = cs_symbol_table }
	= ({it & it_vars = it_vars, it_types = it_types, it_attr_vars = it_attr_vars, it_context = it_context },
	    	specials, type_defs, class_defs, modules, heaps, cs)
  where
	check_fully_polymorphity it_types it_context cs_error
		| all is_type_var it_types && not (isEmpty it_context)
			= checkError "context restriction not allowed for fully polymorph instance" "" cs_error
		= cs_error
	  where
		is_type_var (TV _) = True
		is_type_var _ = False

	compare_context_and_instance_types ins_class it_types {tc_class, tc_types} cs_error
		| ins_class<>tc_class
			= cs_error
		# are_equal
				= fold2St compare_context_and_instance_type it_types tc_types True
		| are_equal
			= checkError ins_class.glob_object.ds_ident "context restriction equals instance type" cs_error
		= cs_error
	  where
		compare_context_and_instance_type (TA {type_index=ti1} _) (TA {type_index=ti2} _) are_equal_accu
			= ti1==ti2 && are_equal_accu
		compare_context_and_instance_type (_ --> _) (_ --> _) are_equal_accu
			= are_equal_accu
//AA..
		compare_context_and_instance_type TArrow TArrow are_equal_accu
			= are_equal_accu	
		compare_context_and_instance_type (TArrow1 _) (TArrow1 _) are_equal_accu
			= are_equal_accu	
//..AA			
		compare_context_and_instance_type (CV tv1 :@: _) (CV tv2 :@: _) are_equal_accu
			= tv1==tv2 && are_equal_accu
		compare_context_and_instance_type (TB bt1) (TB bt2) are_equal_accu
			= bt1==bt2 && are_equal_accu
		compare_context_and_instance_type (TV tv1) (TV tv2) are_equal_accu
			= tv1==tv2 && are_equal_accu
		compare_context_and_instance_type _ _ are_equal_accu
			= False

checkFunctionType :: !Index !SymbolType !Specials !u:{# CheckedTypeDef} !v:{# ClassDef} !u:{# DclModule} !*TypeHeaps !*CheckState
	-> (!SymbolType, !Specials, !u:{# CheckedTypeDef}, !v:{# ClassDef}, !u:{# DclModule}, !*TypeHeaps, !*CheckState)
checkFunctionType mod_index st specials type_defs class_defs modules heaps cs
	= checkSymbolType True mod_index st specials type_defs class_defs modules heaps cs

checkMemberType :: !Index !SymbolType !u:{# CheckedTypeDef} !v:{# ClassDef} !u:{# DclModule} !*TypeHeaps !*CheckState
	-> (!SymbolType, !u:{# CheckedTypeDef}, !v:{# ClassDef}, !u:{# DclModule}, !*TypeHeaps, !*CheckState)
checkMemberType mod_index st type_defs class_defs modules heaps cs
	# (checked_st, specials, type_defs, class_defs, modules, heaps, cs) 
			= checkSymbolType False mod_index st SP_None type_defs class_defs modules heaps cs
	= (checked_st, type_defs, class_defs, modules, heaps, cs) 

checkSymbolType :: !Bool !Index !SymbolType !Specials !u:{# CheckedTypeDef} !v:{# ClassDef} !u:{# DclModule} !*TypeHeaps !*CheckState
	-> (!SymbolType, !Specials, !u:{# CheckedTypeDef}, !v:{# ClassDef}, !u:{# DclModule}, !*TypeHeaps, !*CheckState)
checkSymbolType is_function mod_index st=:{st_args,st_result,st_context,st_attr_env} specials type_defs class_defs modules heaps cs
	# ots = { ots_type_defs = type_defs, ots_modules = modules }
	  oti = { oti_heaps = heaps, oti_all_vars = [], oti_all_attrs = [], oti_global_vars= [] }
	  (st_args, cot_state) = checkOpenATypes mod_index cGlobalScope st_args (ots, oti, cs)
//	   ---> ("checkSymbolType", st_args))
	  (st_result, (ots, oti=:{oti_all_vars = st_vars,oti_all_attrs = st_attr_vars}, cs))
	  	= checkOpenAType mod_index cGlobalScope DAK_None st_result cot_state
	  oti = { oti &  oti_all_vars = [], oti_all_attrs = [] }
	  (st_context, type_defs, class_defs, modules, heaps, cs) = check_type_contexts is_function st_context mod_index class_defs ots oti cs
	  (st_attr_env, cs) = mapSt check_attr_inequality st_attr_env cs
	  (specials, cs) = checkSpecialTypeVars specials cs 
	  cs_symbol_table = removeVariablesFromSymbolTable cGlobalScope st_vars cs.cs_symbol_table
	  cs_symbol_table = removeAttributesFromSymbolTable st_attr_vars cs_symbol_table
	  (specials, type_defs, modules, heaps, cs) = checkSpecialTypes mod_index specials type_defs modules heaps { cs & cs_symbol_table = cs_symbol_table }
	  checked_st = {st & st_vars = st_vars, st_args = st_args, st_result = st_result, st_context = st_context,
	    					st_attr_vars = st_attr_vars, st_attr_env = st_attr_env }
	= (checked_st, specials, type_defs, class_defs, modules, heaps, cs)
//			---> ("checkSymbolType", checked_st)
where
	check_attr_inequality ineq=:{ai_demanded=ai_demanded=:{av_name=dem_name},ai_offered=ai_offered=:{av_name=off_name}} cs=:{cs_symbol_table,cs_error}
		# (dem_entry, cs_symbol_table) = readPtr dem_name.id_info cs_symbol_table
		# (found_dem_attr, dem_attr_ptr) = retrieve_attribute dem_entry
		| found_dem_attr
		   	# (off_entry, cs_symbol_table) = readPtr off_name.id_info cs_symbol_table
			# (found_off_attr, off_attr_ptr) = retrieve_attribute off_entry
			| found_off_attr
				= ({ai_demanded = { ai_demanded & av_info_ptr = dem_attr_ptr }, ai_offered = { ai_offered & av_info_ptr = off_attr_ptr }},
						{ cs & cs_symbol_table = cs_symbol_table })
				= (ineq, { cs & cs_error = checkError off_name "attribute variable undefined" cs_error, cs_symbol_table = cs_symbol_table })
			= (ineq, { cs & cs_error = checkError dem_name "attribute variable undefined" cs_error, cs_symbol_table = cs_symbol_table })
	where
		retrieve_attribute {ste_kind = STE_TypeAttribute attr_ptr, ste_def_level, ste_index}
			| ste_def_level == cGlobalScope
				= (True, attr_ptr)
		retrieve_attribute entry
			= (False, abort "no attribute")

	check_type_contexts is_function st_context mod_index class_defs ots oti cs
		| is_function
		 	= checkTypeContexts st_context mod_index class_defs ots oti cs
			= check_member_contexts st_context mod_index class_defs ots oti cs

// AA.. generic members do not have a context at the moment of checking
	check_member_contexts [] mod_index class_defs ots oti cs
		= checkTypeContexts [] mod_index class_defs ots oti cs
// ..AA
	check_member_contexts [tc : tcs] mod_index class_defs ots oti cs
		# (tc, (class_defs, ots, oti, cs)) = checkTypeContext mod_index tc  (class_defs, ots, oti, cs)
		  cs_symbol_table = removeVariablesFromSymbolTable cGlobalScope [ tv \\ (TV tv) <- tc.tc_types] cs.cs_symbol_table
		  (tcs, type_defs, class_defs, modules, heaps, cs) =  checkTypeContexts tcs mod_index class_defs ots oti { cs & cs_symbol_table = cs_symbol_table }
		= ([tc : tcs], type_defs, class_defs, modules, heaps, cs)

NewEntry symbol_table symb_ptr def_kind def_index level previous :==
	 symbol_table <:= (symb_ptr,{  ste_kind = def_kind, ste_index = def_index, ste_def_level = level, ste_previous = previous })

checkSuperClasses :: ![TypeVar] ![TypeContext] !Index !u:{# CheckedTypeDef} !v:{# ClassDef} !u:{# DclModule} !*TypeHeaps !*CheckState
	-> (![TypeVar], ![TypeContext], !u:{#CheckedTypeDef}, !v:{# ClassDef}, !u:{# DclModule}, !*TypeHeaps, !*CheckState)
checkSuperClasses class_args class_contexts mod_index type_defs class_defs modules heaps=:{th_vars} cs=:{cs_symbol_table,cs_error}
	# (rev_class_args, cs_symbol_table, th_vars, cs_error)
			= foldSt add_variable_to_symbol_table class_args ([], cs_symbol_table, th_vars, cs_error)
	  cs = {cs & cs_symbol_table = cs_symbol_table, cs_error = cs_error }
	  ots = { ots_modules = modules, ots_type_defs = type_defs }
	  oti = { oti_heaps = { heaps & th_vars = th_vars }, oti_all_vars = [], oti_all_attrs = [], oti_global_vars = [] }
	  (class_contexts, type_defs, class_defs, modules, type_heaps, cs)
		  		= checkTypeContexts class_contexts mod_index class_defs ots oti cs
	  (class_args, cs_symbol_table) = retrieve_variables_from_symbol_table rev_class_args [] cs.cs_symbol_table
	= (class_args, class_contexts, type_defs, class_defs, modules, type_heaps, {cs & cs_symbol_table = cs_symbol_table})
where
	add_variable_to_symbol_table :: !TypeVar !(![TypeVar], !*SymbolTable, !*TypeVarHeap, !*ErrorAdmin)
		-> (![TypeVar],!*SymbolTable,!*TypeVarHeap,!*ErrorAdmin)
	add_variable_to_symbol_table tv=:{tv_name={id_name,id_info}} (rev_class_args, symbol_table, th_vars, error)
	  	# (entry, symbol_table) = readPtr id_info symbol_table
		| entry.ste_kind == STE_Empty || entry.ste_def_level < cGlobalScope
			# (new_var_ptr, th_vars) = newPtr TVI_Empty th_vars
			# symbol_table = NewEntry symbol_table id_info (STE_TypeVariable new_var_ptr) NoIndex cGlobalScope entry
			= ([{ tv & tv_info_ptr = new_var_ptr} : rev_class_args], symbol_table, th_vars, error)
			= (rev_class_args, symbol_table, th_vars, checkError id_name "(variable) already defined" error)

	retrieve_variables_from_symbol_table :: ![TypeVar] ![TypeVar] !*SymbolTable -> (![TypeVar],!*SymbolTable)
	retrieve_variables_from_symbol_table [var=:{tv_name={id_name,id_info}} : vars] class_args symbol_table
		# (entry, symbol_table) = readPtr id_info symbol_table
		= retrieve_variables_from_symbol_table vars [var : class_args] (symbol_table <:= (id_info,entry.ste_previous))
	retrieve_variables_from_symbol_table [] class_args symbol_table
		= (class_args, symbol_table)

checkTypeContext ::  !Index !TypeContext !(!v:{# ClassDef}, !u:OpenTypeSymbols, !*OpenTypeInfo, !*CheckState)
	-> (!TypeContext,!(!v:{# ClassDef}, !u:OpenTypeSymbols, !*OpenTypeInfo, !*CheckState))
checkTypeContext mod_index tc=:{tc_class=tc_class=:{glob_object=class_name=:{ds_ident=ds_ident=:{id_name,id_info},ds_arity}},tc_types}
	  	(class_defs, ots, oti, cs=:{cs_symbol_table, cs_predef_symbols})
	# (entry, cs_symbol_table) = readPtr id_info cs_symbol_table
	  cs = { cs & cs_symbol_table = cs_symbol_table }
	# (class_index, class_module) = retrieveGlobalDefinition entry STE_Class mod_index
	| class_index <> NotFound
		# (class_def, class_index, class_defs, ots_modules) = getClassDef class_index class_module mod_index class_defs ots.ots_modules
		  ots = { ots & ots_modules = ots_modules }
		  (tc_types, (ots, oti, cs)) = checkOpenTypes mod_index cGlobalScope DAK_Ignore tc_types (ots, oti, cs)
		  cs = check_context_types 	class_def.class_name tc_types cs
		  tc = { tc & tc_class = { tc_class & glob_object = { class_name & ds_index = class_index }, glob_module = class_module }, tc_types = tc_types}
		| class_def.class_arity == ds_arity
			= (tc, (class_defs, ots, oti, cs))
			= (tc, (class_defs, ots, oti, { cs & cs_error = checkError id_name "used with wrong arity" cs.cs_error }))
		= ({tc & tc_types = []}, (class_defs, ots, oti, { cs & cs_error = checkError id_name "undefined" cs.cs_error }))