checktypes.icl 77.3 KB
Newer Older
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
1
2
3
implementation module checktypes

import StdEnv
Martin Wierich's avatar
Martin Wierich committed
4
5
import syntax, checksupport, check, typesupport, utilities,
		compilerSwitches //, RWSDebug
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
6
7
8
9
10
11
12
13
14
15


::	TypeSymbols = 
	{	ts_type_defs		:: !.{# CheckedTypeDef}
	,	ts_cons_defs 		:: !.{# ConsDef}
	,	ts_selector_defs	:: !.{# SelectorDef}
	,	ts_modules			:: !.{# DclModule}
	}
	
::	TypeInfo =
16
17
	{	ti_var_heap			:: !.VarHeap
	,	ti_type_heaps		:: !.TypeHeaps
18
	,	ti_used_types		:: ![SymbolPtr]
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
	}

::	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
Martin Wierich's avatar
Martin Wierich committed
34
35
		  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
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
36
37
38
39
40
41
		= ({ 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)
Martin Wierich's avatar
Martin Wierich committed
42
				= (TA_Multi, checkError "conflicting attribution of type definition" "" error)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
43
44
45
		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)
Martin Wierich's avatar
Martin Wierich committed
46
				= (TA_Multi, checkError "conflicting attribution of type definition" "" error)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
		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
Martijn Vervoort's avatar
Martijn Vervoort committed
65

Martin Wierich's avatar
Martin Wierich committed
66
67
68
69
70
71
72
		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
		
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
73
74
instance bindTypes TypeVar
where
75
	bindTypes cti tv=:{tv_name=var_id=:{id_info}} (ts, ti, cs=:{cs_symbol_table})
76
77
		# (var_def, cs_symbol_table) = readPtr id_info cs_symbol_table
		  cs = { cs & cs_symbol_table = cs_symbol_table }
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
78
		= case var_def.ste_kind of
79
			STE_BoundTypeVariable bv=:{stv_attribute, stv_info_ptr, stv_count}
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
80
				# cs = { cs & cs_symbol_table = cs.cs_symbol_table <:= (id_info, { var_def & ste_kind = STE_BoundTypeVariable { bv & stv_count = inc stv_count }})}
81
				-> ({ tv & tv_info_ptr = stv_info_ptr}, stv_attribute, (ts, ti, cs))
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
82
83
84
85
86
87
88
89
90
91
92
93
94
			_
				-> (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)
	

95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
retrieveTypeDefinition :: SymbolPtr !Index !*SymbolTable ![SymbolPtr] -> ((!Index, !Index), !*SymbolTable, ![SymbolPtr])
retrieveTypeDefinition type_ptr mod_index symbol_table used_types
	# (entry, symbol_table)	= readPtr type_ptr symbol_table
	= case entry of
		({ste_kind = this_kind =: STE_Imported STE_Type decl_index, ste_def_level, ste_index})
			-> ((ste_index, decl_index), symbol_table <:= (type_ptr, { entry & ste_kind = STE_UsedType decl_index this_kind }), [type_ptr : used_types])
		({ste_kind = this_kind =: STE_Type, ste_def_level, ste_index})
			| ste_def_level == cGlobalScope
				-> ((ste_index, mod_index), symbol_table <:= (type_ptr, { entry & ste_kind = STE_UsedType mod_index this_kind }), [type_ptr : used_types])
				-> ((NotFound, mod_index), symbol_table, used_types)
		({ste_kind = STE_UsedType mod_index _, ste_def_level, ste_index})
			-> ((ste_index, mod_index), symbol_table, used_types)
		_
			-> ((NotFound, mod_index), symbol_table, used_types)

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
110
111
112
113
114
115
116
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})
117
118
119
		# ((type_index, type_module), cs_symbol_table, ti_used_types) = retrieveTypeDefinition id_info cti_module_index cs_symbol_table ti.ti_used_types
		  ti = { ti & ti_used_types = ti_used_types }
		# cs = { cs & cs_symbol_table = cs_symbol_table }
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
120
		| type_index <> NotFound
121
			# ({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
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
122
			  ts = { ts & ts_type_defs = ts_type_defs, ts_modules = ts_modules }
123
			| checkArityOfType type_cons.type_arity td_arity td_rhs
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
124
125
126
127
128
				# (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)
129
130
				= (TE, TA_Multi, (ts, ti, { cs & cs_error = checkError type_cons.type_name "used with wrong arity" cs.cs_error }))
			= (TE, TA_Multi, (ts, ti, { cs & cs_error = checkError type_cons.type_name "undefined" cs.cs_error}))
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
131
132
133
134
135
136
137
138
	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)
139
140
141
142
143
//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		
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
144
145
146
147
	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)
148
149
150
151
152
153
154
// 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
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
	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
Martin Wierich's avatar
Martin Wierich committed
171
	= (attr_env, checkError "inconsistent attribution of type definition" "" error)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
172

Martijn Vervoort's avatar
Martijn Vervoort committed
173
						
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
174
175
176

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

177
178
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}
179
	# (type_def, ts_type_defs) = ts_type_defs![type_index]
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
	# {td_name,td_pos,td_args,td_attribute,td_index} = type_def
	| td_index == NoIndex
		# 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)) = check_rhs_of_TypeDef 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)
		  (td_used_types, cs_symbol_table) = retrieve_used_types ti.ti_used_types cs.cs_symbol_table
		= ({ ts & ts_type_defs = { ts.ts_type_defs & [type_index] = { type_def & td_rhs = td_rhs, td_used_types = td_used_types }}}, { ti & ti_used_types = [] },
					{ cs &	cs_error = popErrorAdmin cs.cs_error,
							cs_symbol_table = removeAttributedTypeVarsFromSymbolTable cGlobalScope type_vars cs_symbol_table})
		= ({ ts & ts_type_defs = ts_type_defs }, ti, cs)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
196
197
198
199
200
201
202
203
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)

204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
	//
	check_rhs_of_TypeDef :: !CheckedTypeDef ![AttributeVar] !CurrentTypeInfo !(!*TypeSymbols, !*TypeInfo, !*CheckState)
		-> (!TypeRhs, !(!*TypeSymbols, !*TypeInfo, !*CheckState))
	//
	check_rhs_of_TypeDef {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 = bind_types_of_constructors cti 0 [ atv_variable \\ {atv_variable} <- td_args] attr_vars type_lhs conses ts_ti_cs
		= (td_rhs, ts_ti_cs)
	check_rhs_of_TypeDef {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) = bind_types_of_constructors 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
		# (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)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
243
		where
244
245
246
247
			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))
248
				
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
			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
				
	check_rhs_of_TypeDef {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)
	check_rhs_of_TypeDef {td_rhs} _ _ ts_ti_cs
		= (td_rhs, ts_ti_cs)

	bind_types_of_constructors :: !CurrentTypeInfo !Index ![TypeVar] ![AttributeVar] !AType ![DefinedSymbol] !(!*TypeSymbols,!*TypeInfo,!*CheckState)
		-> (!*TypeSymbols, !*TypeInfo, !*CheckState)
	bind_types_of_constructors _ _ _ _ _ [] ts_ti_cs
		= ts_ti_cs
	bind_types_of_constructors 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) = bind_types_of_constructors 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)
282
	where
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
		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}}))

	retrieve_used_types symb_ptrs symbol_table
		= foldSt retrieve_used_type symb_ptrs ([], symbol_table)
	where		
		retrieve_used_type symb_ptr (used_types, symbol_table)
			# (ste=:{ste_kind=STE_UsedType decl_index orig_kind,ste_index}, symbol_table) = readPtr symb_ptr symbol_table
			= ([{gi_module = decl_index, gi_index = ste_index} : used_types], symbol_table <:= (symb_ptr, { ste & ste_kind = orig_kind }))
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
309
	
310
311
CS_Checked	:== 1
CS_Checking	:== 0
312

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
313

314
checkTypeDefs :: !Bool !*{# CheckedTypeDef} !Index !*{# ConsDef} !*{# SelectorDef} !*{# DclModule} !*VarHeap !*TypeHeaps !*CheckState
315
	-> (!*{# CheckedTypeDef}, !*{# ConsDef}, !*{# SelectorDef}, !*{# DclModule}, !*VarHeap, !*TypeHeaps, !*CheckState)
316
checkTypeDefs is_main_dcl type_defs module_index  cons_defs selector_defs modules var_heap type_heaps cs
317
	#! nr_of_types = size type_defs
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
318
	#  ts = { ts_type_defs = type_defs, ts_cons_defs = cons_defs, ts_selector_defs = selector_defs, ts_modules = modules }
319
	   ti = { ti_type_heaps = type_heaps, ti_var_heap = var_heap, ti_used_types = []  }
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
320
321
	= check_type_defs is_main_dcl 0 nr_of_types module_index ts ti cs
where
322
	check_type_defs is_main_dcl type_index nr_of_types module_index ts ti=:{ti_type_heaps,ti_var_heap} cs
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
323
		| type_index == nr_of_types
324
			= (ts.ts_type_defs, ts.ts_cons_defs, ts.ts_selector_defs, ts.ts_modules, ti_var_heap, ti_type_heaps, cs)
325
			# (ts, ti, cs) = checkTypeDef  type_index module_index ts ti cs
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
			= check_type_defs is_main_dcl (inc type_index) nr_of_types module_index ts ti cs

::	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
341
	# (entry=:{ste_kind,ste_def_level}, symbol_table) = readPtr id_info symbol_table
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
342
343
344
345
346
347
348
349
350
351
352
	| 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

353
newAttribute :: !DemandedAttributeKind {#Char} TypeAttribute !*OpenTypeInfo !*CheckState -> (!TypeAttribute, !*OpenTypeInfo, !*CheckState)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
354
355
356
357
358
359
360
361
362
363
364
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)
		_
365
			-> (TA_Unique, oti, { cs & cs_error = checkError var_name "inconsistently attributed (2)" cs.cs_error })
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
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
382
		# (type_def, type_defs) = type_defs![type_index]
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
383
		= (type_def, type_index, type_defs, modules)
384
385
386
		# ({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
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
387
388
		= (type_def, type_index, type_defs, modules)

389
390
391
392
393
checkArityOfType act_arity form_arity (SynType _)
	= form_arity == act_arity
checkArityOfType act_arity form_arity _
	= form_arity >= act_arity

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
394
395
396
397
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
398
		# (class_def, class_defs) = class_defs![class_index]
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
399
		= (class_def, class_index, class_defs, modules)
400
401
402
		# ({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
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
403
404
		= (class_def, class_index, class_defs, modules)

405
406
407
408
409
410
411
412
413
414
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)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
415

416
417
418
419
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
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
420
	| ste_kind == STE_Empty || ste_def_level == cModuleScope
421
		# (new_attr, oti=:{oti_heaps,oti_all_vars}, cs) = newAttribute dem_attr id_name tv_attr oti { cs & cs_symbol_table = cs_symbol_table }
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
422
423
		  (new_var_ptr, th_vars) = newPtr (TVI_Attribute new_attr) oti_heaps.th_vars
		  new_var = { tv & tv_info_ptr = new_var_ptr }
424
		= (new_var, new_attr, ({ oti & oti_heaps = { oti_heaps & th_vars = th_vars }, oti_all_vars = [new_var : oti_all_vars]},
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
425
426
427
428
429
				{ 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
430
431
432
		  (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))
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
433
434
435
436
437
438
439
440
441
442
443
444
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,
445
						cs_error = checkError new_var.av_name "inconsistently attributed (3)" cs_error })
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
446
447
448
449
450
451
452
		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)
				_
453
					-> (TA_Unique, oti, { cs & cs_error = checkError var_name "inconsistently attributed (4)" cs.cs_error })
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
454
455
456
457
458
459
460
		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)
				_
461
					-> (TA_Multi, oti, { cs & cs_error = checkError var_name "inconsistently attributed (5)" cs.cs_error })
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
462
		check_var_attribute var_attr new_attr oti cs
463
			= (var_attr, oti, { cs & cs_error = checkError var_name "inconsistently attributed (6)" cs.cs_error })// ---> (var_attr, new_attr)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
464
465
466
467
468
469
470
471
472
473
474
		
		
		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)
				 _
475
				 	-> (TA_Unique, checkError var_name "inconsistently attributed (1)" error)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
476
477
478
479
480
481
482
483
		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)

484
485
checkOpenAType :: !Index !Int !DemandedAttributeKind !AType !(!u:OpenTypeSymbols, !*OpenTypeInfo, !*CheckState)
	-> (!AType, !(!u:OpenTypeSymbols, !*OpenTypeInfo, !*CheckState))
486
checkOpenAType mod_index scope dem_attr type=:{at_type = TV tv, at_attribute} (ots, oti, cs)
487
	# (tv, at_attribute, (oti, cs)) = checkTypeVar scope dem_attr tv at_attribute (oti, cs) 
488
	= ({ type & at_type = TV tv, at_attribute = at_attribute }, (ots, oti, cs))
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
489
490
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
491
	  (type_var, oti_global_vars, th_vars, entry) = retrieve_global_variable var_id entry oti_global_vars oti_heaps.th_vars
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
	= ({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 })
513
//
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
514
checkOpenAType mod_index scope dem_attr type=:{ at_type=TA type_cons=:{type_name=type_name=:{id_name,id_info}} types, at_attribute}
515
516
517
518
		(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
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
519
	| type_index <> NotFound
520
		# ({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
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
521
		  ots = { ots & ots_type_defs = ots_type_defs, ots_modules = ots_modules }
522
		| checkArityOfType type_cons.type_arity td_arity td_rhs
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
523
			# type_cons = { type_cons & type_index = { glob_object = type_index, glob_module = type_module }}
524
			  (types, (ots, oti, cs)) = check_args_of_type_cons mod_index scope /* dem_attr */ types td_args (ots, oti, cs)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
525
526
			  (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)) 
527
528
			= (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}))
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
529
where
530
531
	check_args_of_type_cons :: !Index !Int ![AType] ![ATypeVar] !(!u:OpenTypeSymbols, !*OpenTypeInfo, !*CheckState)
		-> (![AType], !(!u:OpenTypeSymbols, !*OpenTypeInfo, !*CheckState))
532
533
534
535
536
537
	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)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
538
539
540
541
542
543
544
545
546
547
548
549
550

	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))
551
552
553
554
555
556
//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
557
checkOpenAType mod_index scope dem_attr type=:{at_type = CV tv :@: types, at_attribute} (ots, oti, cs)
558
	# (cons_var, _, (oti, cs)) = checkTypeVar scope DAK_None tv TA_Multi (oti, cs)
559
	  (types, (ots, oti, cs)) = mapSt (checkOpenAType mod_index scope DAK_None) types (ots, oti, cs)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
560
561
	  (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))
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
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

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
584
585
586
587
588
589
590
591
592
593
594
595
596
597
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

Martin Wierich's avatar
Martin Wierich committed
598
checkInstanceType :: !Index !(Global DefinedSymbol) !InstanceType !Specials !u:{# CheckedTypeDef} !v:{# ClassDef} !u:{# DclModule} !*TypeHeaps !*CheckState
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
599
	-> (!InstanceType, !Specials, !u:{# CheckedTypeDef}, !v:{# ClassDef}, !u:{# DclModule}, !*TypeHeaps, !*CheckState)
Martin Wierich's avatar
Martin Wierich committed
600
601
602
603
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 }
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
604
	  oti = { oti_heaps = heaps, oti_all_vars = [], oti_all_attrs = [], oti_global_vars= [] }
605
606
607
608
609
	  (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
Martin Wierich's avatar
Martin Wierich committed
610
	  (specials, cs) = checkSpecialTypeVars specials { cs & cs_error = cs_error }
611
612
	  cs_symbol_table = removeVariablesFromSymbolTable cGlobalScope it_vars cs.cs_symbol_table
	  cs_symbol_table = removeAttributesFromSymbolTable it_attr_vars cs_symbol_table
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
613
	  (specials, type_defs, modules, heaps, cs) = checkSpecialTypes mod_index specials type_defs modules heaps { cs & cs_symbol_table = cs_symbol_table }
614
	= ({it & it_vars = it_vars, it_types = it_types, it_attr_vars = it_attr_vars, it_context = it_context },
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
615
	    	specials, type_defs, class_defs, modules, heaps, cs)
Martin Wierich's avatar
Martin Wierich committed
616
617
618
  where
	check_fully_polymorphity it_types it_context cs_error
		| all is_type_var it_types && not (isEmpty it_context)
Martin Wierich's avatar
Martin Wierich committed
619
			= checkError "context restriction not allowed for fully polymorph instance" "" cs_error
Martin Wierich's avatar
Martin Wierich committed
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
		= 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
638
639
640
641
642
643
//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			
Martin Wierich's avatar
Martin Wierich committed
644
645
646
647
648
649
650
651
652
		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

653
654
655
656
657
658
659
660
661
662
663
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) 
Martin Wierich's avatar
Martin Wierich committed
664

665
checkSymbolType :: !Bool !Index !SymbolType !Specials !u:{# CheckedTypeDef} !v:{# ClassDef} !u:{# DclModule} !*TypeHeaps !*CheckState
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
666
	-> (!SymbolType, !Specials, !u:{# CheckedTypeDef}, !v:{# ClassDef}, !u:{# DclModule}, !*TypeHeaps, !*CheckState)
667
checkSymbolType is_function mod_index st=:{st_args,st_result,st_context,st_attr_env} specials type_defs class_defs modules heaps cs
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
668
669
670
	# 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)
671
//	   ---> ("checkSymbolType", st_args))
672
673
674
675
676
	  (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
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
677
	  (specials, cs) = checkSpecialTypeVars specials cs 
678
679
	  cs_symbol_table = removeVariablesFromSymbolTable cGlobalScope st_vars cs.cs_symbol_table
	  cs_symbol_table = removeAttributesFromSymbolTable st_attr_vars cs_symbol_table
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
680
	  (specials, type_defs, modules, heaps, cs) = checkSpecialTypes mod_index specials type_defs modules heaps { cs & cs_symbol_table = cs_symbol_table }
681
682
	  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 }
683
	= (checked_st, specials, type_defs, class_defs, modules, heaps, cs)
684
//			---> ("checkSymbolType", checked_st)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
685
686
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}
687
		# (dem_entry, cs_symbol_table) = readPtr dem_name.id_info cs_symbol_table
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
688
689
		# (found_dem_attr, dem_attr_ptr) = retrieve_attribute dem_entry
		| found_dem_attr
690
		   	# (off_entry, cs_symbol_table) = readPtr off_name.id_info cs_symbol_table
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
691
692
			# (found_off_attr, off_attr_ptr) = retrieve_attribute off_entry
			| found_off_attr
693
694
695
696
				= ({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 })
697
698
699
700
701
702
703
704
705
706
707
708
	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

709
710
711
712
// 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
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
	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})
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
734
where
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
	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))
Martin Wierich's avatar
Martin Wierich committed
767
768
			= (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 }))
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
where
	
	check_context_types tc_class [] cs=:{cs_error}
		= { cs & cs_error = checkError tc_class "type context should contain one or more type variables" cs_error}
	check_context_types tc_class [((CV {tv_name}) :@: _):_] cs=:{cs_error}
		= cs
//		= { cs & cs_error = checkError tv_name "not allowed as higher order type variable in context" cs_error}
	check_context_types tc_class [TV _ : types] cs
		= cs
	check_context_types tc_class [type : types] cs
		= check_context_types tc_class types cs

checkTypeContext1 ::  !Index !TypeContext !(!v:{# ClassDef}, !x:{# GenericDef}, !u:OpenTypeSymbols, !*OpenTypeInfo, !*CheckState)
	-> (!TypeContext,!(!v:{# ClassDef}, !x:{# GenericDef}, !u:OpenTypeSymbols, !*OpenTypeInfo, !*CheckState))
checkTypeContext1 mod_index tc (class_defs, generic_defs, ots, oti, cs)
	# (entry, cs) = get_entry tc cs
	= check_context mod_index entry tc (class_defs, generic_defs, ots, oti, cs)
where
	get_entry tc cs=:{cs_symbol_table}
		# (entry, cs_symbol_table) = readPtr tc.tc_class.glob_object.ds_ident.id_info cs_symbol_table
		= (entry, {cs & cs_symbol_table = cs_symbol_table}) 

	check_context 
			mod_index 
			entry 
			tc=:{tc_class=tc_class=:{glob_object=class_name=:{ds_ident=ds_ident=:{id_name,id_info},ds_arity}},tc_types}
	  		(class_defs, generic_defs, ots, oti, cs)
		# (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, generic_defs, ots, oti, cs))
				= (tc, (class_defs, generic_defs, ots, oti, { cs & cs_error = checkError id_name "used with wrong arity" cs.cs_error }))
			= ({tc & tc_types = []}, (class_defs, generic_defs, ots, oti, { cs & cs_error = checkError id_name "class undefined" cs.cs_error }))
	check_context 
			mod_index
			entry
			tc=:{tc_class=tc_class=:{glob_object=class_name=:{ds_ident=ds_ident=:{id_name,id_info},ds_arity}},tc_types}
			(class_defs, generic_defs, ots, oti, cs)	
		# 	(generic_index, generic_module) = retrieveGlobalDefinition entry STE_Generic mod_index
		| generic_index <> NotFound
			# (generic_def, generic_index, generic_defs, ots_modules) = getGenericDef generic_index generic_module mod_index generic_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 	generic_def.gen_name tc_types cs
			  tc = { tc & tc_class = { tc_class & glob_object = { class_name & ds_index = generic_index }, glob_module = generic_module }, tc_types = tc_types}
			| ds_arity == 1
				= (tc, (class_defs, generic_defs, ots, oti, cs))
				= (tc, (class_defs, generic_defs, ots, oti, { cs & cs_error = checkError id_name "used with wrong arity" cs.cs_error }))
			= ({tc & tc_types = []}, (class_defs, generic_defs, ots, oti, { cs & cs_error = checkError id_name "generic undefined" cs.cs_error }))
			
824
	check_context_types tc_class [] cs=:{cs_error}
Martin Wierich's avatar
Martin Wierich committed
825
		= { cs & cs_error = checkError tc_class "type context should contain one or more type variables" cs_error}
Martin Wierich's avatar
Martin Wierich committed
826
	check_context_types tc_class [((CV {tv_name}) :@: _):_] cs=:{cs_error}
827
828
		= cs
//		= { cs & cs_error = checkError tv_name "not allowed as higher order type variable in context" cs_error}
829
830
831
832
833
	check_context_types tc_class [TV _ : types] cs
		= cs
	check_context_types tc_class [type : types] cs
		= check_context_types tc_class types cs

834
835
836
837
838
839
840
841
842
843
844
845
846
checkTypeContexts :: ![TypeContext] !Index !v:{# ClassDef} !u:OpenTypeSymbols !*OpenTypeInfo !*CheckState
	-> (![TypeContext], !u:{# CheckedTypeDef}, !v:{# ClassDef}, u:{# DclModule}, !*TypeHeaps, !*CheckState)
checkTypeContexts tcs mod_index class_defs ots oti cs
	# (tcs, (class_defs, { ots_modules, ots_type_defs}, oti, cs)) = mapSt (checkTypeContext mod_index) tcs (class_defs, ots, oti, cs)
	  cs = check_class_variables oti.oti_all_vars cs
	  cs = check_class_attributes oti.oti_all_attrs cs
	= (tcs, ots_type_defs, class_defs, ots_modules, oti.oti_heaps, cs)
where
	check_class_variables class_variables cs
		= foldSt check_class_variable class_variables cs
	where
		check_class_variable {tv_name} cs=:{cs_symbol_table,cs_error}
			= { cs & cs_symbol_table	= removeDefinitionFromSymbolTable cGlobalScope tv_name cs_symbol_table,
Martin Wierich's avatar
Martin Wierich committed
847
					 cs_error			= checkError tv_name "wrongly used or not used at all" cs_error}
848
849
850
851
852
853
	
	check_class_attributes class_attributes cs
		= foldSt check_class_attribute class_attributes cs
	where
		check_class_attribute {av_name} cs=:{cs_symbol_table,cs_error}
			= { cs & cs_symbol_table	= removeDefinitionFromSymbolTable cGlobalScope av_name cs_symbol_table,
Martin Wierich's avatar
Martin Wierich committed
854
					 cs_error			= checkError av_name "undefined" cs_error}
855

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
856
857
858
859
860
861
862
863
864
865
866
867
868
869

checkDynamicTypes :: !Index ![ExprInfoPtr] !(Optional SymbolType) !u:{# CheckedTypeDef} !u:{# DclModule} !*TypeHeaps !*ExpressionHeap !*CheckState
	-> (!u:{# CheckedTypeDef}, !u:{# DclModule}, !*TypeHeaps, !*ExpressionHeap, !*CheckState)
checkDynamicTypes mod_index dyn_type_ptrs No type_defs modules type_heaps expr_heap cs
	# (type_defs, modules, heaps, expr_heap, cs) = checkDynamics mod_index (inc cModuleScope) dyn_type_ptrs type_defs modules type_heaps expr_heap cs
	  (expr_heap, cs_symbol_table) = remove_global_type_variables_in_dynamics dyn_type_ptrs (expr_heap, cs.cs_symbol_table)
	= (type_defs, modules, heaps, expr_heap, { cs & cs_symbol_table = cs_symbol_table })
where
	remove_global_type_variables_in_dynamics dyn_info_ptrs expr_heap_and_symbol_table
		= foldSt remove_global_type_variables_in_dynamic dyn_info_ptrs expr_heap_and_symbol_table
	where
		remove_global_type_variables_in_dynamic dyn_info_ptr (expr_heap, symbol_table)
			# (dyn_info, expr_heap) = readPtr dyn_info_ptr expr_heap
			= case dyn_info of
Martijn Vervoort's avatar
Martijn Vervoort committed
870
				EI_Dynamic (Yes {dt_global_vars}) _
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
871
					-> (expr_heap, remove_global_type_variables dt_global_vars symbol_table)
Martijn Vervoort's avatar
Martijn Vervoort committed
872
				EI_Dynamic No _
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
873
874
875
876
877
878
879
880
881
882
883
884
885
					-> (expr_heap, symbol_table)
				EI_DynamicTypeWithVars loc_type_vars {dt_global_vars} loc_dynamics
					-> remove_global_type_variables_in_dynamics loc_dynamics (expr_heap, remove_global_type_variables dt_global_vars symbol_table)
						
	
		remove_global_type_variables global_vars symbol_table
			= foldSt remove_global_type_variable global_vars symbol_table
		where		
			remove_global_type_variable {tv_name=tv_name=:{id_info}} symbol_table
				# (entry, symbol_table) = readPtr id_info symbol_table
				| entry.ste_kind == STE_Empty
					= symbol_table
					= symbol_table <:= (id_info, entry.ste_previous)
886
887


Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
							 
checkDynamicTypes mod_index dyn_type_ptrs (Yes {st_vars}) type_defs modules type_heaps expr_heap cs=:{cs_symbol_table}
	# (th_vars, cs_symbol_table) = foldSt add_type_variable_to_symbol_table st_vars (type_heaps.th_vars, cs_symbol_table)
	  (type_defs, modules, heaps, expr_heap, cs) = checkDynamics mod_index (inc cModuleScope) dyn_type_ptrs type_defs modules
	  		{ type_heaps & th_vars = th_vars } expr_heap { cs & cs_symbol_table = cs_symbol_table }
	  cs_symbol_table =	removeVariablesFromSymbolTable cModuleScope st_vars cs.cs_symbol_table
	  (expr_heap, cs) = check_global_type_variables_in_dynamics dyn_type_ptrs (expr_heap, { cs & cs_symbol_table = cs_symbol_table })
	= (type_defs, modules, heaps, expr_heap, cs) 
where
	add_type_variable_to_symbol_table {tv_name={id_info},tv_info_ptr} (var_heap,symbol_table)
		# (entry, symbol_table) = readPtr id_info symbol_table
		= (	var_heap <:= (tv_info_ptr, TVI_Empty),
			symbol_table <:= (id_info, {ste_index = NoIndex, ste_kind = STE_TypeVariable tv_info_ptr,
									ste_def_level = cModuleScope, ste_previous = entry }))

	check_global_type_variables_in_dynamics dyn_info_ptrs expr_heap_and_cs
		= foldSt check_global_type_variables_in_dynamic dyn_info_ptrs expr_heap_and_cs
	where
		check_global_type_variables_in_dynamic dyn_info_ptr (expr_heap, cs)
			# (dyn_info, expr_heap) = readPtr dyn_info_ptr expr_heap
			= case dyn_info of
Martijn Vervoort's avatar
Martijn Vervoort committed
909
				EI_Dynamic (Yes {dt_global_vars}) _
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
910
					-> (expr_heap, check_global_type_variables dt_global_vars cs)
Martijn Vervoort's avatar
Martijn Vervoort committed
911
				EI_Dynamic No _
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
912
913
914
915
916
917
918
919
920
921
922
923
924
					-> (expr_heap, cs)
				EI_DynamicTypeWithVars loc_type_vars {dt_global_vars} loc_dynamics
					-> check_global_type_variables_in_dynamics loc_dynamics (expr_heap, check_global_type_variables dt_global_vars cs)
						
	
		check_global_type_variables global_vars cs
			= foldSt check_global_type_variable global_vars cs
		where		
			check_global_type_variable {tv_name=tv_name=:{id_info}} cs=:{cs_symbol_table, cs_error}
				# (entry, cs_symbol_table) = readPtr id_info cs_symbol_table
				| entry.ste_kind == STE_Empty
					= { cs & cs_symbol_table = cs_symbol_table }
					= { cs & cs_symbol_table = cs_symbol_table <:= (id_info, entry.ste_previous),
Martin Wierich's avatar
Martin Wierich committed
925
							 cs_error = checkError tv_name.id_name "global type variable not used in type of the function" cs_error }
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
926
927
928
929
930
931
932

checkDynamics mod_index scope dyn_type_ptrs type_defs modules type_heaps expr_heap cs
	= foldSt (check_dynamic mod_index scope) dyn_type_ptrs (type_defs, modules, type_heaps, expr_heap, cs)
where	
	check_dynamic mod_index scope dyn_info_ptr (type_defs, modules, type_heaps, expr_heap, cs)
		# (dyn_info, expr_heap) = readPtr dyn_info_ptr expr_heap
		= case dyn_info of
Martijn Vervoort's avatar
Martijn Vervoort committed
933
			EI_Dynamic opt_type ei_dynamic_id
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
934
935
936
937
				-> case opt_type of
					Yes dyn_type
						# (dyn_type, loc_type_vars, type_defs, modules, type_heaps, cs) = check_dynamic_type mod_index scope dyn_type type_defs modules type_heaps cs
						| isEmpty loc_type_vars
Martijn Vervoort's avatar
Martijn Vervoort committed
938
							-> (type_defs, modules, type_heaps, expr_heap <:= (dyn_info_ptr, EI_Dynamic (Yes dyn_type) ei_dynamic_id), cs)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
939
				  			# cs_symbol_table = removeVariablesFromSymbolTable scope loc_type_vars cs.cs_symbol_table
Martin Wierich's avatar
Martin Wierich committed
940
							  cs_error = checkError loc_type_vars "type variable(s) not defined" cs.cs_error
Martijn Vervoort's avatar
Martijn Vervoort committed
941
							-> (type_defs, modules, type_heaps, expr_heap <:= (dyn_info_ptr, EI_Dynamic (Yes dyn_type) ei_dynamic_id),
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
									{ cs & cs_error = cs_error, cs_symbol_table = cs_symbol_table })
					No
						-> (type_defs, modules, type_heaps, expr_heap, cs)
			EI_DynamicType dyn_type loc_dynamics
				# (dyn_type, loc_type_vars, type_defs, modules, type_heaps, cs) = check_dynamic_type mod_index scope dyn_type type_defs modules type_heaps cs
				  (type_defs, modules, type_heaps, expr_heap, cs) = check_local_dynamics mod_index scope loc_dynamics type_defs modules type_heaps expr_heap cs
				  cs_symbol_table = removeVariablesFromSymbolTable scope loc_type_vars cs.cs_symbol_table
				-> (type_defs, modules, type_heaps, expr_heap <:= (dyn_info_ptr, EI_DynamicTypeWithVars loc_type_vars dyn_type loc_dynamics),
							{ cs & cs_symbol_table = cs_symbol_table }) 
						// ---> ("check_dynamic ", scope, dyn_type, loc_type_vars)

	check_local_dynamics mod_index scope local_dynamics type_defs modules type_heaps expr_heap cs
		= foldSt (check_dynamic mod_index (inc scope)) local_dynamics (type_defs, modules, type_heaps, expr_heap, cs)

	check_dynamic_type mod_index scope dt=:{dt_uni_vars,dt_type} type_defs modules type_heaps=:{th_vars} cs
		# (dt_uni_vars, (th_vars, cs)) = mapSt (add_type_variable_to_symbol_table scope) dt_uni_vars (th_vars, cs)
		  ots = { ots_type_defs = type_defs, ots_modules = modules }
		  oti = { oti_heaps = { type_heaps & th_vars = th_vars }, oti_all_vars = [], oti_all_attrs = [], oti_global_vars = [] }
		  (dt_type, ( {ots_type_defs, ots_modules}, {oti_heaps,oti_all_vars,oti_all_attrs, oti_global_vars}, cs))
		  		= checkOpenAType mod_index scope DAK_Ignore dt_type (ots, oti, cs)
		  th_vars = foldSt (\{tv_info_ptr} -> writePtr tv_info_ptr TVI_Empty) oti_global_vars oti_heaps.th_vars
	  	  cs_symbol_table = removeAttributedTypeVarsFromSymbolTable scope dt_uni_vars cs.cs_symbol_table
		| isEmpty oti_all_attrs
			= ({ dt & dt_uni_vars = dt_uni_vars, dt_global_vars = oti_global_vars, dt_type = dt_type },
					oti_all_vars, ots_type_defs, ots_modules, { oti_heaps & th_vars = th_vars }, { cs & cs_symbol_table = cs_symbol_table })
			# cs_symbol_table = removeAttributesFromSymbolTable oti_all_attrs cs_symbol_table
			= ({ dt & dt_uni_vars = dt_uni_vars, dt_global_vars = oti_global_vars, dt_type = dt_type },
					oti_all_vars, ots_type_defs, ots_modules, { oti_heaps & th_vars = th_vars },
Martin Wierich's avatar
Martin Wierich committed
970
					{ cs & cs_symbol_table = cs_symbol_table, cs_error = checkError (hd oti_all_attrs).av_name "type attribute variable not allowed" cs.cs_error})
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
971
972
973
		
	add_type_variable_to_symbol_table :: !Level !ATypeVar !*(!*TypeVarHeap,!*CheckState) -> (!ATypeVar,!(!*TypeVarHeap, !*CheckState))
	add_type_variable_to_symbol_table scope atv=:{atv_variable=atv_variable=:{tv_name}, atv_attribute} (type_var_heap, cs=:{cs_symbol_table,cs_error})
974
975
		#  var_info = tv_name.id_info
		   (var_entry, cs_symbol_table) = readPtr var_info cs_symbol_table
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
976
977
978
979
980
981
		| var_entry.ste_kind == STE_Empty || scope < var_entry.ste_def_level
			#! (new_var_ptr, type_var_heap) = newPtr TVI_Empty type_var_heap
			# cs_symbol_table = cs_symbol_table <:=
				(var_info, {ste_index = NoIndex, ste_kind = STE_TypeVariable new_var_ptr, ste_def_level = scope, ste_previous = var_entry })
			= ({atv & atv_attribute = TA_Multi, atv_variable = { atv_variable & tv_info_ptr = new_var_ptr }}, (type_var_heap,
					{ cs & cs_symbol_table = cs_symbol_table, cs_error = check_attribute atv_attribute cs_error}))
Martin Wierich's avatar
Martin Wierich committed
982
			= (atv, (type_var_heap, { cs & cs_symbol_table = cs_symbol_table, cs_error = checkError tv_name.id_name "type variable already defined" cs_error }))
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
983
984
985
986
987
988
989
990

	check_attribute TA_Unique error
		= error
	check_attribute TA_Multi error
		= error
	check_attribute TA_None error
		= error
	check_attribute attr error
Martin Wierich's avatar
Martin Wierich committed
991
		= checkError attr "attribute not allowed in type of dynamic" error
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
992
993
994
995
996
997
998
999
	
	
checkSpecialTypeVars :: !Specials !*CheckState -> (!Specials, !*CheckState)
checkSpecialTypeVars (SP_ParsedSubstitutions env) cs
	# (env, cs) = mapSt (mapSt check_type_var) env cs
	= (SP_ParsedSubstitutions env, cs)
where		
	check_type_var bind=:{bind_dst=type_var=:{tv_name={id_name,id_info}}} cs=:{cs_symbol_table,cs_error}
1000
		# ({ste_kind,ste_def_level}, cs_symbol_table) = readPtr id_info cs_symbol_table
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
1001
1002
		| ste_kind <> STE_Empty && ste_def_level == cGlobalScope
			# (STE_TypeVariable tv_info_ptr) = ste_kind
1003
			= ({ bind & bind_dst = { type_var & tv_info_ptr = tv_info_ptr}}, { cs & cs_symbol_table = cs_symbol_table })
Martin Wierich's avatar
Martin Wierich committed
1004
			= (bind, { cs & cs_symbol_table= cs_symbol_table, cs_error = checkError id_name "type variable not defined" cs_error })
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
1005
1006
checkSpecialTypeVars SP_None cs
	= (SP_None, cs)
1007
1008
1009

checkSpecialTypes :: !Index !Specials !v:{#CheckedTypeDef} !u:{#.DclModule} !*TypeHeaps !*CheckState
	-> (!Specials,!x:{#CheckedTypeDef},!w:{#DclModule},!.TypeHeaps,!.CheckState), [u v <= w, v u <= x];
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
checkSpecialTypes mod_index (SP_ParsedSubstitutions envs) type_defs modules heaps cs
	# ots = { ots_type_defs = type_defs, ots_modules = modules }
	  (specials, (heaps, ots, cs)) = mapSt (check_environment mod_index) envs (heaps, ots, cs)
	= (SP_Substitutions specials, ots.ots_type_defs, ots.ots_modules, heaps, cs)
where
	check_environment mod_index env (heaps, ots, cs)
	 	# oti = { oti_heaps = heaps, oti_all_vars = [], oti_all_attrs = [], oti_global_vars = [] }
	 	  (env, (ots, {oti_heaps,oti_all_vars,oti_all_attrs}, cs)) = mapSt (check_substituted_type mod_index) env (ots, oti, cs)
	  	  cs_symbol_table = removeVariablesFromSymbolTable cGlobalScope oti_all_vars cs.cs_symbol_table
		  cs_symbol_table = removeAttributesFromSymbolTable oti_all_attrs cs_symbol_table
		= ({ ss_environ = env, ss_context = [], ss_vars = oti_all_vars, ss_attrs = oti_all_attrs}, (oti_heaps, ots, { cs & cs_symbol_table = cs_symbol_table }))

	check_substituted_type mod_index bind=:{bind_src} cot_state
		 # (bind_src, cot_state) = checkOpenType mod_index cGlobalScope DAK_Ignore bind_src cot_state
		 = ({ bind & bind_src = bind_src }, cot_state)
checkSpecialTypes mod_index SP_None type_defs modules heaps cs
	= (SP_None, type_defs, modules, heaps, cs)

1028
/* cOuterMostLevel :== 0 */
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
1029

1030
addTypeVariablesToSymbolTable :: !Level ![ATypeVar] ![AttributeVar] !*TypeHeaps !*CheckState