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

3
import StdEnv, compare_types
4
import syntax, checksupport, typesupport, utilities
5
import genericsupport
6
from explicitimports import search_qualified_ident,::NameSpaceN,TypeNameSpaceN,ClassNameSpaceN
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
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
	}

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

27
28
29
bindArgAType :: !CurrentTypeInfo !AType !v:{#ClassDef}  !(!*TypeSymbols, !*TypeInfo, !*CheckState)
			-> (!AType, !TypeAttribute, !v:{#ClassDef}, !(!*TypeSymbols, !*TypeInfo, !*CheckState))
bindArgAType cti {at_attribute,at_type=TFA vars type} class_defs (ts, ti=:{ti_type_heaps}, cs)
30
31
32
33
	# (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 & cs_symbol_table = removeAttributedTypeVarsFromSymbolTable cRankTwoScope type_vars cs.cs_symbol_table
	  at_type = TFA type_vars type
34
35
36
37
38
39
40
41
42
43
44
	  (attype,combined_attribute,ts_ti_cs) = bindAttributes TA_Multi cti at_attribute at_type (ts, ti, cs)
	= (attype,combined_attribute,class_defs,ts_ti_cs)
bindArgAType cti {at_attribute,at_type=TFAC vars type contexts} class_defs (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)
	  (contexts,class_defs,ts,ti,cs) = bind_rank2_context_of_cons contexts cti class_defs ts ti cs
	  cs & cs_symbol_table = removeAttributedTypeVarsFromSymbolTable cRankTwoScope type_vars cs.cs_symbol_table
	  at_type = TFAC type_vars type contexts
	  (attype,combined_attribute,ts_ti_cs) = bindAttributes TA_Multi cti at_attribute at_type (ts, ti, cs)
	= (attype,combined_attribute,class_defs,ts_ti_cs)
bindArgAType cti {at_attribute,at_type} class_defs ts_ti_cs
45
	# (at_type, type_attr, ts_ti_cs) = bindTypes cti at_type ts_ti_cs
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
	  (attype,combined_attribute,ts_ti_cs) = bindAttributes type_attr cti at_attribute at_type ts_ti_cs
	= (attype,combined_attribute,class_defs,ts_ti_cs)

bind_rank2_context_of_cons [context=:{tc_class,tc_types}:contexts] cti class_defs ts ti cs
	# (tc_class, class_defs, modules, cs=:{cs_error}) = check_context_class tc_class tc_types cti.cti_module_index class_defs ts.ts_modules cs
	  ts = {ts & ts_modules=modules}
	| cs_error.ea_ok
	 	# (tc_types, _, (ts,ti,cs)) = bindTypes cti tc_types (ts,ti,cs)
		  cs = check_context_types tc_class tc_types cs
		  (contexts,class_defs,ts,ti,cs) = bind_rank2_context_of_cons contexts cti class_defs ts ti cs
		#! contexts = [{context & tc_class=tc_class, tc_types=tc_types}:contexts]
		| cs_error.ea_ok
			# cs = foldSt check_rank2_vars_in_type tc_types cs
			= (contexts,class_defs,ts,ti,cs)
			= (contexts,class_defs,ts,ti,cs)
		# (contexts,class_defs,ts,ti,cs) = bind_rank2_context_of_cons contexts cti class_defs ts ti cs
		= ([{context & tc_types = []}:contexts],class_defs,ts,ti,cs)
where
	check_rank2_vars_in_atypes [{at_type}:tc_types] cs
		= check_rank2_vars_in_atypes tc_types (check_rank2_vars_in_type at_type cs)
	check_rank2_vars_in_atypes [] cs
		= cs
	
	check_rank2_vars_in_type (TV {tv_ident}) cs=:{cs_symbol_table}
		| (sreadPtr tv_ident.id_info cs_symbol_table).ste_def_level==cRankTwoScope
			= cs
			= {cs & cs_error = checkError tv_ident "universally quantified type variable expected" cs.cs_error}
	check_rank2_vars_in_type (TA _ atypes) cs
		= check_rank2_vars_in_atypes atypes cs
	check_rank2_vars_in_type (TAS _ atypes _) cs
		= check_rank2_vars_in_atypes atypes cs
	check_rank2_vars_in_type (arg_type --> res_type) cs
		= check_rank2_vars_in_type res_type.at_type (check_rank2_vars_in_type arg_type.at_type cs)
	check_rank2_vars_in_type (TArrow1 {at_type}) cs
		= check_rank2_vars_in_type at_type cs
	check_rank2_vars_in_type (CV {tv_ident} :@: types) cs=:{cs_symbol_table}
		| (sreadPtr tv_ident.id_info cs_symbol_table).ste_def_level==cRankTwoScope
			= check_rank2_vars_in_atypes types cs
			# cs & cs_error = checkError tv_ident "universally quantified type variable expected" cs.cs_error
			= check_rank2_vars_in_atypes types cs
	check_rank2_vars_in_type _ cs
		= cs
bind_rank2_context_of_cons [] cti class_defs ts ti cs
	= ([],class_defs,ts,ti,cs)
90

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
91
class bindTypes type :: !CurrentTypeInfo !type !(!*TypeSymbols, !*TypeInfo, !*CheckState)
92
					-> (!type, !TypeAttribute, !(!*TypeSymbols, !*TypeInfo, !*CheckState))
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
93
94
95

instance bindTypes AType
where
96
97
98
	bindTypes cti {at_attribute,at_type} ts_ti_cs
		# (at_type, type_attr, ts_ti_cs) = bindTypes cti at_type ts_ti_cs
		= bindAttributes type_attr cti at_attribute at_type ts_ti_cs
John van Groningen's avatar
John van Groningen committed
99

100
101
102
103
104
105
106
107
108
109
110
111
112
bindAttributes :: !TypeAttribute !CurrentTypeInfo !TypeAttribute !Type !(!*TypeSymbols, !*TypeInfo, !*CheckState)
										   -> (!AType, !TypeAttribute, !(!*TypeSymbols, !*TypeInfo, !*CheckState))
bindAttributes type_attr cti at_attribute 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
	= ({ 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
			= (to_root_attr root_attr, error)
			= (TA_Multi, checkError "conflicting attribution of type definition" "" error)
	where
113
114
115
116
		to_root_attr (TA_Var var)
			= TA_RootVar var
		to_root_attr attr
			= attr
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
	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_ident == attr_var2.av_ident
	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 TA_Anonymous (CV tv :@: types) error
		= checkError tv "attribute variable not allowed" error
	check_attr_of_type_var attr _ error
		= error
				
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
149
150
instance bindTypes TypeVar
where
151
	bindTypes cti tv=:{tv_ident=var_id=:{id_info}} (ts, ti, cs=:{cs_symbol_table})
152
153
		# (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
154
		= case var_def.ste_kind of
155
			STE_BoundTypeVariable {stv_info_ptr,stv_attribute}
156
				-> ({ tv & tv_info_ptr = stv_info_ptr}, stv_attribute, (ts, ti, cs))
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
157
			_
John van Groningen's avatar
John van Groningen committed
158
				-> (tv, TA_Multi, (ts, ti, {cs & cs_error = checkError var_id "type variable undefined" cs.cs_error}))
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
159
160
161
162
163
164
165
166
167
168

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)

169
retrieveTypeDefinition :: SymbolPtr !Index !*SymbolTable ![SymbolPtr] -> (!Index, !Index, !*SymbolTable, ![SymbolPtr])
170
retrieveTypeDefinition type_ptr mod_index symbol_table used_types
171
172
173
	# (entry=:{ste_kind,ste_def_level,ste_index}, symbol_table)	= readPtr type_ptr symbol_table
	= case ste_kind of
		this_kind=:(STE_Imported STE_Type ste_mod_index)
174
			-> (ste_index, ste_mod_index, symbol_table <:= (type_ptr, { entry & ste_kind = STE_UsedType ste_mod_index this_kind }), [type_ptr : used_types])
175
		this_kind=:STE_Type
176
			| ste_def_level == cGlobalScope
177
178
				-> (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)
179
		STE_UsedType mod_index _
180
			-> (ste_index, mod_index, symbol_table, used_types)
181
182
		this_kind=:(STE_UsedQualifiedType uqt_mod_index uqt_index orig_kind)
			| uqt_mod_index==mod_index && uqt_index==ste_index
183
				-> (ste_index, mod_index, symbol_table, used_types) 
184
185
186
187
				-> retrieve_type_definition orig_kind
		with
			retrieve_type_definition (STE_UsedQualifiedType uqt_mod_index uqt_index orig_kind)
				| uqt_mod_index==mod_index && uqt_index==ste_index
188
					= (ste_index, mod_index, symbol_table, used_types)
189
190
					= retrieve_type_definition orig_kind
			retrieve_type_definition (STE_Imported STE_Type ste_mod_index)
191
				= (ste_index, ste_mod_index, symbol_table <:= (type_ptr, { entry & ste_kind = STE_UsedType ste_mod_index this_kind }), used_types)
192
193
			retrieve_type_definition STE_Type
				| ste_def_level == cGlobalScope
194
195
					= (ste_index, mod_index, symbol_table <:= (type_ptr, { entry & ste_kind = STE_UsedType mod_index this_kind }), used_types)
					= (NotFound, mod_index, symbol_table, used_types)
196
			retrieve_type_definition (STE_UsedType mod_index _)
197
				= (ste_index, mod_index, symbol_table, used_types)
198
			retrieve_type_definition _
199
				= (NotFound, mod_index, symbol_table, used_types)
200
		_
201
			-> (NotFound, mod_index, symbol_table, used_types)
202

203
204
205
determine_type_attribute TA_Unique		= TA_Unique
determine_type_attribute _				= TA_Multi

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
206
207
208
209
210
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)
211
	bindTypes cti=:{cti_module_index,cti_type_index,cti_lhs_attribute} type=:(TA type_cons=:{type_ident=type_ident=:{id_info}} types)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
212
					(ts=:{ts_type_defs,ts_modules}, ti, cs=:{cs_symbol_table})
213
		# (type_index, type_module, cs_symbol_table, ti_used_types) = retrieveTypeDefinition id_info cti_module_index cs_symbol_table ti.ti_used_types
214
215
		  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
216
		| type_index <> NotFound
217
			# ({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
218
			  ts = { ts & ts_type_defs = ts_type_defs, ts_modules = ts_modules }
219
			| checkArityOfType type_cons.type_arity td_arity td_rhs
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
220
221
222
223
224
				# (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)
225
226
227
				= (TE, TA_Multi, (ts, ti, { cs & cs_error = checkError type_cons.type_ident "used with wrong arity" cs.cs_error }))
			= (TE, TA_Multi, (ts, ti, { cs & cs_error = checkError type_cons.type_ident "undefined" cs.cs_error}))
	bindTypes cti=:{cti_module_index,cti_type_index,cti_lhs_attribute} type=:(TAS type_cons=:{type_ident=type_ident=:{id_info}} types strictness)
228
					(ts=:{ts_type_defs,ts_modules}, ti, cs=:{cs_symbol_table})
229
		# (type_index, type_module, cs_symbol_table, ti_used_types) = retrieveTypeDefinition id_info cti_module_index cs_symbol_table ti.ti_used_types
230
231
232
233
234
235
236
237
238
239
240
		  ti = { ti & ti_used_types = ti_used_types }
		# cs = { cs & cs_symbol_table = cs_symbol_table }
		| 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
					= (TAS { type_cons & type_index = { glob_object = type_index, glob_module = type_module}} types strictness, cti_lhs_attribute, ts_ti_cs)
					= (TAS { type_cons & type_index = { glob_object = type_index, glob_module = type_module}} types strictness,
								determine_type_attribute td_attribute, ts_ti_cs)
241
242
				= (TE, TA_Multi, (ts, ti, { cs & cs_error = checkError type_cons.type_ident "used with wrong arity" cs.cs_error }))
			= (TE, TA_Multi, (ts, ti, { cs & cs_error = checkError type_cons.type_ident "undefined" cs.cs_error}))	
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
243
244
245
246
	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)
247
248
249
	bindTypes cti (TArrow1 type) ts_ti_cs
		# (type, _, ts_ti_cs) = bindTypes cti type ts_ti_cs
		= (TArrow1 type, TA_Multi, ts_ti_cs)	
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
250
251
252
253
	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)
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
	bindTypes cti=:{cti_module_index,cti_type_index,cti_lhs_attribute} type=:(TQualifiedIdent module_id type_name types)
					(ts=:{ts_type_defs,ts_modules}, ti, cs)
		# (found,{decl_kind,decl_ident=type_ident,decl_index=type_index},cs) = search_qualified_ident module_id type_name TypeNameSpaceN cs
		| not found
			= (TE, TA_Multi, (ts, ti, cs))
			= case decl_kind of
				STE_Imported STE_Type type_module
					# ({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 }
					  (cs_symbol_table, ti_used_types) = add_qualified_type_to_used_types type_ident.id_info type_module type_index cs.cs_symbol_table ti.ti_used_types
					  cs = {cs & cs_symbol_table = cs_symbol_table}
					  ti = { ti & ti_used_types = ti_used_types }					  
					# type_cons = MakeNewTypeSymbIdent type_ident (length types)
					| 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, TA_Multi, (ts, ti, { cs & cs_error = checkError type_cons.type_ident "used with wrong arity" cs.cs_error }))
				_
275
					-> (TE, TA_Multi, (ts, ti, { cs & cs_error = checkError ("'"+++module_id.id_name+++"'."+++type_name) "not imported" cs.cs_error}))
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
		where
			add_qualified_type_to_used_types symbol_table_ptr type_module type_index symbol_table used_types
				# (entry=:{ste_kind,ste_index}, symbol_table) = readPtr symbol_table_ptr symbol_table
				= case ste_kind of
					STE_UsedQualifiedType mod_index decl_index next_kind
						 | (mod_index==type_module && decl_index==type_index) || qualified_type_occurs next_kind ste_index type_module type_index
						 	-> (symbol_table, used_types)
						 	# entry = {entry & ste_kind = STE_UsedQualifiedType type_module type_index ste_kind }
						 	-> (writePtr symbol_table_ptr entry symbol_table, used_types)
					STE_UsedType ste_module next_kind
						 | (ste_module==type_module && ste_index==type_index) || qualified_type_occurs next_kind ste_index type_module type_index
						 	-> (symbol_table, used_types)
						 	# entry = {entry & ste_kind = STE_UsedQualifiedType type_module type_index ste_kind }
						 	-> (writePtr symbol_table_ptr entry symbol_table, used_types)
					_
						 	# entry = {entry & ste_kind = STE_UsedQualifiedType type_module type_index ste_kind }
						 	-> (writePtr symbol_table_ptr entry symbol_table, [symbol_table_ptr:used_types])

			qualified_type_occurs (STE_UsedQualifiedType mod_index decl_index next_kind) ste_index type_module type_index
				| mod_index==type_module && decl_index==type_index
					= True
					= qualified_type_occurs next_kind ste_index type_module type_index
			qualified_type_occurs (STE_UsedType ste_module next_kind) ste_index type_module type_index
				 | ste_module==type_module && ste_index==type_index
				 	= True
					= qualified_type_occurs next_kind ste_index type_module type_index
			qualified_type_occurs _ _ _ _
				= False
304
305
306
	bindTypes cti type=:(TFA vars _) (ts, ti, cs)
		# cs = universal_quantifier_error vars cs
		= (type, TA_Multi, (ts, ti, cs))
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
307
308
309
	bindTypes cti type ts_ti_cs
		= (type, TA_Multi, ts_ti_cs)

310
311
312
313
314
universal_quantifier_error [{atv_variable={tv_ident}}:_] cs
	= {cs & cs_error = checkError tv_ident "universally quantified type variable not allowed here" cs.cs_error}
universal_quantifier_error _ cs
	= {cs & cs_error = checkError "" "universal quantifier not allowed here" cs.cs_error}

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
315
316
317
318
319
320
321
322
323
324
325
326
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
327
	= (attr_env, checkError "inconsistent attribution of type definition" "" error)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
328

329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
check_context_class :: TCClass [Type] Int u:{#ClassDef} v:{#DclModule} *CheckState
							  -> (TCClass,u:{#ClassDef},v:{#DclModule},*CheckState)
check_context_class (TCClass cl) tc_types mod_index class_defs modules cs
	# (entry, cs_symbol_table) = readPtr cl.glob_object.ds_ident.id_info cs.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_arity}, class_index, class_defs, modules) = getClassDef class_index class_module mod_index class_defs modules
		| class_arity == cl.glob_object.ds_arity
			# checked_class = {cl & glob_module = class_module, glob_object = {cl.glob_object & ds_index = class_index}}
			= (TCClass checked_class, class_defs, modules, cs) 
			# cs_error = checkError cl.glob_object.ds_ident	"class used with wrong arity" cs.cs_error
			= (TCClass cl, class_defs, modules, {cs & cs_error = cs_error})
		# cs_error = checkError cl.glob_object.ds_ident	"class undefined" cs.cs_error	
		= (TCClass cl, class_defs, modules, {cs & cs_error = cs_error})
check_context_class tc_class=:(TCQualifiedIdent module_id class_name) tc_types mod_index class_defs modules cs
	# (found,{decl_kind,decl_ident=type_ident,decl_index=class_index},cs) = search_qualified_ident module_id class_name ClassNameSpaceN cs
	| not found
		= (tc_class, class_defs, modules, cs)
		= case decl_kind of
			STE_Imported STE_Class class_module
				# ({class_ident,class_arity}, class_index, class_defs, modules) = getClassDef class_index class_module mod_index class_defs modules
				| class_arity == length tc_types
					# checked_class = { glob_object = MakeDefinedSymbol class_ident class_index class_arity, glob_module = class_module }
					-> (TCClass checked_class, class_defs, modules, cs)
					# cs_error = checkError ("'"+++module_id.id_name+++"'."+++class_name) "class used with wrong arity" cs.cs_error
					-> (tc_class, class_defs, modules, {cs & cs_error = cs_error})
			_
				-> (tc_class, class_defs, modules, {cs & cs_error = checkError ("'"+++module_id.id_name+++"'."+++class_name) "class undefined" cs.cs_error})
check_context_class (TCGeneric gtc=:{gtc_generic, gtc_kind}) tc_types mod_index class_defs modules cs
  	# gen_ident = gtc_generic.glob_object.ds_ident
	# (entry, cs_symbol_table) = readPtr gen_ident.id_info cs.cs_symbol_table
  	# cs = { cs & cs_symbol_table = cs_symbol_table }
  	# clazz =
  		{ glob_module = -1
		, glob_object = {ds_ident = genericIdentToClassIdent gen_ident.id_name gtc_kind, ds_arity = 1, ds_index = -1}
		}
	# (generic_index, generic_module) = retrieveGlobalDefinition entry STE_Generic mod_index
	| generic_index <> NotFound
		| gtc_generic.glob_object.ds_arity == 1
			# checked_gen = 
				{ glob_module = generic_module
				, glob_object = {gtc_generic.glob_object & ds_index = generic_index}					
				}
			  ({pds_module,pds_def},cs) = cs!cs_predef_symbols.[PD_TypeGenericDict]
			  generic_dict = {gi_module=pds_module, gi_index=pds_def}
375
376
377
378
379
			#! tc_class = TCGeneric {gtc & gtc_generic = checked_gen, gtc_class=clazz, gtc_generic_dict=generic_dict}
			| not cs.cs_x.x_check_dynamic_types
				= (tc_class, class_defs, modules, cs)
				# cs = {cs & cs_error = checkError gen_ident "a generic context is not allowed in a dynamic type" cs.cs_error}
				= (tc_class, class_defs, modules, cs)
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
			# cs_error = checkError gen_ident "generic used with wrong arity: generic has always has one class argument" cs.cs_error  
			= (TCGeneric {gtc & gtc_class=clazz}, class_defs, modules, {cs & cs_error = cs_error})
		# cs_error = checkError gen_ident "generic undefined" cs.cs_error
		= (TCGeneric {gtc & gtc_class=clazz}, class_defs, modules, {cs & cs_error = cs_error})

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_ident}) :@: _):_] cs=:{cs_error}
	= cs
//		= { cs & cs_error = checkError tv_ident "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

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
395
396
emptyIdent name :== { id_name = name, id_info = nilPtr }

397
398
checkTypeDef :: !Index !Index !v:{#ClassDef} !*TypeSymbols !*TypeInfo !*CheckState -> (!v:{#ClassDef},!*TypeSymbols,!*TypeInfo,!*CheckState);
checkTypeDef type_index module_index class_defs ts=:{ts_type_defs} ti=:{ti_type_heaps} cs=:{cs_error}
399
	# (type_def, ts_type_defs) = ts_type_defs![type_index]
400
	# {td_ident,td_pos,td_args,td_attribute,td_index} = type_def
401
	| td_index == NoIndex
402
		# position = newPosition td_ident td_pos
403
		  cs_error = pushErrorAdmin position cs_error
404
		  (td_attribute, attr_vars, th_attrs) = determine_root_attribute td_attribute td_ident.id_name ti_type_heaps.th_attrs
405
406
		  (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 }
407
		  type_def = { type_def & td_args = type_vars, td_index = type_index, td_attrs = attr_vars, td_attribute = td_attribute }
408
		  (td_rhs, (class_defs,ts,ti,cs)) = check_rhs_of_TypeDef type_def attr_vars
409
				{ cti_module_index = module_index, cti_type_index = type_index, cti_lhs_attribute = td_attribute }
410
					(class_defs, {ts & ts_type_defs = ts_type_defs}, {ti & ti_type_heaps = ti_type_heaps}, cs)
411
		  (td_used_types, cs_symbol_table) = retrieve_used_types ti.ti_used_types cs.cs_symbol_table
412
413
		  cs = {cs &	cs_error = popErrorAdmin cs.cs_error,
						cs_symbol_table = removeAttributedTypeVarsFromSymbolTable cGlobalScope type_vars cs_symbol_table}
414
415
		= (class_defs, {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)
		= (class_defs, {ts & ts_type_defs = ts_type_defs}, ti, cs)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
416
417
418
where
	determine_root_attribute TA_None name attr_var_heap
		# (attr_info_ptr, attr_var_heap) = newPtr AVI_Empty attr_var_heap
419
		  new_var = { av_ident = emptyIdent name, av_info_ptr = attr_info_ptr}
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
420
421
422
423
		= (TA_Var new_var, [new_var], attr_var_heap)
	determine_root_attribute TA_Unique name attr_var_heap
		= (TA_Unique, [], attr_var_heap)

424
425
426
427
	check_rhs_of_TypeDef :: !CheckedTypeDef ![AttributeVar] !CurrentTypeInfo
					  !(!v:{#ClassDef},!*TypeSymbols,!*TypeInfo,!*CheckState)
		-> (!TypeRhs, !(!v:{#ClassDef},!*TypeSymbols,!*TypeInfo,!*CheckState))
	check_rhs_of_TypeDef {td_ident,td_arity,td_args,td_rhs = td_rhs=:AlgType conses} attr_vars cti=:{cti_module_index,cti_type_index,cti_lhs_attribute} class_defs_ts_ti_cs
428
		# type_lhs = { at_attribute = cti_lhs_attribute,
429
				  	   at_type = TA (MakeTypeSymbIdent { glob_object = cti_type_index, glob_module = cti_module_index } td_ident td_arity)
430
									[{at_attribute = atv_attribute,at_type = TV atv_variable} \\ {atv_variable, atv_attribute} <- td_args]}
431
432
		  class_defs_ts_ti_cs = bind_types_of_constructors cti 0 (atype_vars_to_type_vars td_args) attr_vars type_lhs conses class_defs_ts_ti_cs
		= (td_rhs, class_defs_ts_ti_cs)
433
	check_rhs_of_TypeDef {td_ident,td_arity,td_args,td_rhs = td_rhs=:RecordType {rt_constructor={ds_index,ds_arity}, rt_fields}}
434
			attr_vars cti=:{cti_module_index,cti_type_index,cti_lhs_attribute} (class_defs,ts,ti,cs)
435
		# type_lhs = {	at_attribute = cti_lhs_attribute,
436
						at_type = TA (MakeTypeSymbIdent { glob_object = cti_type_index, glob_module = cti_module_index } td_ident td_arity)
437
									[{ at_attribute = atv_attribute,at_type = TV atv_variable} \\ {atv_variable, atv_attribute} <- td_args]}
438
439
440
		  cs = if (ds_arity>32)
				{ cs & cs_error = checkError ("Record has too many fields ("+++toString ds_arity+++",") "32 are allowed)" cs.cs_error }
				cs;
441
		  (class_defs,ts,ti,cs) = bind_types_of_constructor cti 0 (atype_vars_to_type_vars td_args) attr_vars type_lhs ds_index (class_defs,ts,ti,cs)
442
443
444
445
		# (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
446
		= (td_rhs, (class_defs,{ts & ts_selector_defs = ts_selector_defs},{ti & ti_var_heap = ti_var_heap},{cs & cs_error = cs_error}))
447
448
449
450
451
452
453
454
	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
455
				# (sel_type, (sel_vars, sel_attr_vars)) = lift_quantifier sel_type (st_vars, st_attr_vars)
456
457
				# (st_attr_env, error) = addToAttributeEnviron sel_type.at_attribute rec_type.at_attribute [] error
				# (new_type_ptr, var_heap) = newPtr VI_Empty var_heap
458
459
				  sd_type = { sel_def.sd_type &  st_arity = 1, st_args = [rec_type], st_result = sel_type,
				  				st_vars = sel_vars, st_attr_vars = sel_attr_vars, st_attr_env = st_attr_env }
460
461
462
463
				  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
464
		where
465
466
467
468
			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))
469
				
470
471
472
473
474
475
476
			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
477
478
479
480
	check_rhs_of_TypeDef {td_rhs = SynType type} _ cti (class_defs,ts,ti,cs)
		# (type, type_attr, (ts,ti,cs)) = bindTypes cti type (ts,ti,cs)
		= (SynType type, (class_defs,ts,ti,cs))
	check_rhs_of_TypeDef {td_ident,td_arity,td_args,td_rhs = td_rhs=:NewType {ds_index}} attr_vars cti=:{cti_module_index,cti_type_index,cti_lhs_attribute} class_defs_ts_ti_cs
John van Groningen's avatar
John van Groningen committed
481
482
483
		# type_lhs = { at_attribute = cti_lhs_attribute,
				  	   at_type = TA (MakeTypeSymbIdent { glob_object = cti_type_index, glob_module = cti_module_index } td_ident td_arity)
									[{at_attribute = atv_attribute,at_type = TV atv_variable} \\ {atv_variable, atv_attribute} <- td_args]}
484
485
486
487
488
		  class_defs_ts_ti_cs = bind_types_of_constructor cti -2 (atype_vars_to_type_vars td_args) attr_vars type_lhs ds_index class_defs_ts_ti_cs
		= (td_rhs, class_defs_ts_ti_cs)
	check_rhs_of_TypeDef {td_rhs = AbstractSynType properties type} _ cti (class_defs,ts,ti,cs)
		# (type, type_attr, (ts,ti,cs)) = bindTypes cti type (ts,ti,cs)
		= (AbstractSynType properties type, (class_defs,ts,ti,cs))
489
	check_rhs_of_TypeDef {td_ident,td_arity,td_args,td_rhs = td_rhs=:ExtensibleAlgType conses} attr_vars cti=:{cti_module_index,cti_type_index,cti_lhs_attribute} class_defs_ts_ti_cs
490
491
492
493
494
		# type_lhs = { at_attribute = cti_lhs_attribute,
				  	   at_type = TA (MakeTypeSymbIdent {glob_object = cti_type_index, glob_module = cti_module_index} td_ident td_arity)
									[{at_attribute = atv_attribute,at_type = TV atv_variable} \\ {atv_variable, atv_attribute} <- td_args]}
		  class_defs_ts_ti_cs = bind_types_of_constructors cti 0 (atype_vars_to_type_vars td_args) attr_vars type_lhs conses class_defs_ts_ti_cs
		= (td_rhs, class_defs_ts_ti_cs)
495
496
	check_rhs_of_TypeDef {td_ident,td_arity,td_args,td_rhs = td_rhs=:UncheckedAlgConses type_ext_ident conses} attr_vars cti=:{cti_module_index,cti_type_index,cti_lhs_attribute} class_defs_ts_ti_cs
		# (class_defs,ts,ti,cs) = class_defs_ts_ti_cs
497
498
499
500
		  (type_index, type_module, cs_symbol_table, ti_used_types) = retrieveTypeDefinition td_ident.id_info cti_module_index cs.cs_symbol_table ti.ti_used_types
		  ti & ti_used_types = ti_used_types
		  cs & cs_symbol_table = cs_symbol_table
		| type_index <> NotFound
501
		 	# class_defs_ts_ti_cs = (class_defs,ts,ti,cs)
502
			// to do check if ExtensibleAlgType
503
504
505
			# type_lhs = { at_attribute = cti_lhs_attribute,
					  	   at_type = TA (MakeTypeSymbIdent { glob_object = type_index, glob_module = type_module } td_ident td_arity)
										[{at_attribute = atv_attribute,at_type = TV atv_variable} \\ {atv_variable, atv_attribute} <- td_args]}
506
507
			  class_defs_ts_ti_cs = bind_types_of_added_constructors cti (atype_vars_to_type_vars td_args) attr_vars type_lhs conses class_defs_ts_ti_cs
			= (AlgConses conses {gi_module=type_module,gi_index=type_index}, class_defs_ts_ti_cs)
508
			# cs & cs_error = checkError td_ident "undefined" cs.cs_error
509
510
511
			= (td_rhs, (class_defs,ts,ti,cs))
	check_rhs_of_TypeDef {td_rhs} _ _ class_defs_ts_ti_cs
		= (td_rhs, class_defs_ts_ti_cs)
512

513
514
515
	atype_vars_to_type_vars atype_vars
		= [atv_variable \\ {atv_variable} <- atype_vars]

516
517
518
519
	bind_types_of_constructors :: !CurrentTypeInfo !Index ![TypeVar] ![AttributeVar] !AType ![DefinedSymbol]
								!(!v:{#ClassDef},!*TypeSymbols,!*TypeInfo,!*CheckState)
							->   (!v:{#ClassDef},!*TypeSymbols,!*TypeInfo,!*CheckState)
	bind_types_of_constructors cti cons_number free_vars free_attrs type_lhs [{ds_arity,ds_ident,ds_index}:conses] (class_defs,ts,ti,cs)
520
		# (ts,cs) = if (ds_arity>32)
521
						(constructor_has_too_many_arguments ds_index ds_ident ds_arity ts cs)
522
						(ts,cs);
523
524
525
526
		# class_defs_ts_ti_cs = bind_types_of_constructor cti cons_number free_vars free_attrs type_lhs ds_index (class_defs,ts,ti,cs)
		= bind_types_of_constructors cti (inc cons_number) free_vars free_attrs type_lhs conses class_defs_ts_ti_cs
	bind_types_of_constructors _ _ _ _ _ [] class_defs_ts_ti_cs
		= class_defs_ts_ti_cs
527

528
	bind_types_of_added_constructors :: !CurrentTypeInfo ![TypeVar] ![AttributeVar] !AType ![DefinedSymbol]
529
530
531
								!(!v:{#ClassDef},!*TypeSymbols,!*TypeInfo,!*CheckState)
							->   (!v:{#ClassDef},!*TypeSymbols,!*TypeInfo,!*CheckState)
	bind_types_of_added_constructors cti free_vars free_attrs type_lhs [{ds_arity,ds_ident,ds_index}:conses] (class_defs,ts,ti,cs)
532
533
534
		# (ts,cs) = if (ds_arity>32)
						(constructor_has_too_many_arguments ds_index ds_ident ds_arity ts cs)
						(ts,cs);
535
		# class_defs_ts_ti_cs = bind_types_of_constructor cti -3 free_vars free_attrs type_lhs ds_index (class_defs,ts,ti,cs)
536
537
538
539
		= bind_types_of_added_constructors cti free_vars free_attrs type_lhs conses class_defs_ts_ti_cs
	bind_types_of_added_constructors _ _ _ _ [] class_defs_ts_ti_cs
		= class_defs_ts_ti_cs

540
541
542
543
	constructor_has_too_many_arguments ds_index ds_ident ds_arity ts cs
		# (cons_pos,ts2) = ts!ts_cons_defs.[ds_index].cons_pos
		= (ts2, {cs & cs_error = checkErrorWithPosition ds_ident cons_pos ("Constructor has too many arguments ("+++toString ds_arity+++", 32 are allowed)") cs.cs_error})

544
545
546
547
	bind_types_of_constructor :: !CurrentTypeInfo !Index ![TypeVar] ![AttributeVar] !AType !Index
					!(!v:{#ClassDef},!*TypeSymbols,!*TypeInfo,!*CheckState)
				->	 (!v:{#ClassDef},!*TypeSymbols,!*TypeInfo,!*CheckState)
	bind_types_of_constructor cti=:{cti_lhs_attribute} cons_number free_vars free_attrs type_lhs cons_index (class_defs, ts, ti=:{ti_type_heaps}, cs)
548
		# (cons_def, ts) = ts!ts_cons_defs.[cons_index]
549
550
		# (exi_vars, (ti_type_heaps, cs))
		  		= addExistentionalTypeVariablesToSymbolTable cti_lhs_attribute cons_def.cons_exi_vars ti_type_heaps cs
551
552
553
554
		  (st_args, st_attr_env,class_defs,(ts, ti, cs))
		  		= bind_types_of_cons cons_def.cons_type.st_args cti free_vars [] class_defs (ts, {ti & ti_type_heaps = ti_type_heaps}, cs)
		  (st_context,class_defs,ts,ti,cs)
		  		= bind_context_of_cons cons_def.cons_type.st_context cti class_defs ts ti cs
555
		  symbol_table = removeAttributedTypeVarsFromSymbolTable cGlobalScope /* cOuterMostLevel */ exi_vars cs.cs_symbol_table
556
		  attr_vars = add_universal_attr_vars st_args free_attrs
557
		  cons_type = {cons_def.cons_type & st_vars = free_vars, st_args = st_args, st_result = type_lhs, st_context = st_context, st_attr_vars = attr_vars, st_attr_env = st_attr_env}
558
		  (new_type_ptr, ti_var_heap) = newPtr VI_Empty ti.ti_var_heap
559
		  cons_def = { cons_def & cons_type = cons_type, cons_number = cons_number, cons_type_index = cti.cti_type_index, cons_exi_vars = exi_vars,
560
		  						  cons_type_ptr = new_type_ptr }
561
		= (class_defs, {ts & ts_cons_defs.[cons_index] = cons_def}, {ti & ti_var_heap = ti_var_heap}, {cs & cs_symbol_table=symbol_table})
562
	where
563
564
565
566
567
568
569
570
		bind_types_of_cons :: ![AType] !CurrentTypeInfo ![TypeVar] ![AttrInequality] !v:{#ClassDef} !(!*TypeSymbols, !*TypeInfo, !*CheckState)
													 -> (![AType], ![AttrInequality],!v:{#ClassDef},!(!*TypeSymbols, !*TypeInfo, !*CheckState))
		bind_types_of_cons [] cti free_vars attr_env class_defs ts_ti_cs
			= ([], attr_env, class_defs, ts_ti_cs)
		bind_types_of_cons [type : types] cti free_vars attr_env class_defs ts_ti_cs
			# (types, attr_env, class_defs, ts_ti_cs)
					= bind_types_of_cons types cti free_vars attr_env class_defs ts_ti_cs
			  (type, type_attr, class_defs, (ts, ti, cs)) = bindArgAType cti type class_defs ts_ti_cs
571
			  (attr_env, cs_error) = addToAttributeEnviron type_attr cti.cti_lhs_attribute attr_env cs.cs_error
572
573
574
575
576
577
578
579
580
581
582
583
584
585
			= ([type : types], attr_env, class_defs, (ts, ti, {cs & cs_error = cs_error}))

		bind_context_of_cons [context=:{tc_class,tc_types,tc_var}:contexts] cti class_defs ts ti cs
			# (tc_class, class_defs, modules, cs=:{cs_error}) = check_context_class tc_class tc_types cti.cti_module_index class_defs ts.ts_modules cs
			  ts = {ts & ts_modules=modules}
			| cs_error.ea_ok
			 	# (tc_types, _, (ts,ti,cs)) = bindTypes cti tc_types (ts,ti,cs)
				  cs = check_context_types tc_class tc_types cs
				  (contexts,class_defs,ts,ti,cs) = bind_context_of_cons contexts cti class_defs ts ti cs
				= ([{context & tc_class=tc_class, tc_types=tc_types}:contexts],class_defs,ts,ti,cs)
				# (contexts,class_defs,ts,ti,cs) = bind_context_of_cons contexts cti class_defs ts ti cs
				= ([{context & tc_types = []}:contexts],class_defs,ts,ti,cs)
		bind_context_of_cons [] cti class_defs ts ti cs
			= ([],class_defs,ts,ti,cs)
586

587
588
589
		add_universal_attr_vars [] attr_vars
			= attr_vars
		add_universal_attr_vars [{at_type=TFA vars type}:types] attr_vars
590
			= add_universal_attr_vars types (add_attr_vars vars attr_vars)
591
592
		add_universal_attr_vars [{at_type=TFAC vars type contexts}:types] attr_vars
			= add_universal_attr_vars types (add_attr_vars vars attr_vars)
593
		add_universal_attr_vars [type:types] attr_vars
594
			= add_universal_attr_vars types attr_vars
595
596
597

		add_attr_vars vars attr_vars
			= foldSt add_attr_var vars attr_vars
598
599
600
601
602
603
		where
			add_attr_var {atv_attribute=TA_Var av=:{av_info_ptr}} attr_vars
				= [av : attr_vars]
			add_attr_var _ attr_vars
				= attr_vars

604
605
	retrieve_used_types symb_ptrs symbol_table
		= foldSt retrieve_used_type symb_ptrs ([], symbol_table)
606
	where
607
		retrieve_used_type symb_ptr (used_types, symbol_table)
608
609
610
611
612
613
614
615
616
617
618
619
620
			# (ste=:{ste_kind,ste_index}, symbol_table) = readPtr symb_ptr symbol_table
			# (orig_kind,used_types) = retrieve_used_types_of_ident ste_kind ste_index used_types 
			= (used_types, symbol_table <:= (symb_ptr, { ste & ste_kind = orig_kind }))

		retrieve_used_types_of_ident (STE_UsedType mod_index orig_kind) ste_index used_types
			# used_types = [{gi_module = mod_index, gi_index = ste_index} : used_types]
			= retrieve_used_types_of_ident orig_kind ste_index used_types
		retrieve_used_types_of_ident (STE_UsedQualifiedType mod_index decl_index orig_kind) ste_index used_types
			# used_types = [{gi_module = mod_index, gi_index = decl_index} : used_types]
			= retrieve_used_types_of_ident orig_kind ste_index used_types
		retrieve_used_types_of_ident orig_kind ste_index used_types
			= (orig_kind,used_types)

621
622
CS_Checked	:== 1
CS_Checking	:== 0
623

624
625
626
627
checkTypeDefs :: !Index !(Optional (CopiedDefinitions, Int))
		!*{#CheckedTypeDef} !*{#ConsDef} !*{#SelectorDef} !v:{#ClassDef} !*{#DclModule} !*Heaps !*CheckState
	-> (!*{#CheckedTypeDef},!*{#ConsDef},!*{#SelectorDef},!v:{#ClassDef},!*{#DclModule},!*Heaps,!*CheckState)
checkTypeDefs module_index opt_icl_info type_defs cons_defs selector_defs class_defs modules heaps=:{hp_type_heaps,hp_var_heap} cs
628
	#! nr_of_types = size type_defs
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
629
	#  ts = { ts_type_defs = type_defs, ts_cons_defs = cons_defs, ts_selector_defs = selector_defs, ts_modules = modules }
630
	   ti = { ti_type_heaps = hp_type_heaps, ti_var_heap = hp_var_heap, ti_used_types = [] }
631
632
633
	   (class_defs, {ts_type_defs,ts_cons_defs, ts_selector_defs, ts_modules}, {ti_var_heap,ti_type_heaps}, cs)
	  		= iFoldSt (check_type_def module_index opt_icl_info) 0 nr_of_types (class_defs, ts, ti, cs)
	= (ts_type_defs, ts_cons_defs, ts_selector_defs, class_defs, ts_modules, {heaps& hp_var_heap=ti_var_heap, hp_type_heaps=ti_type_heaps}, cs)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
634
where
635
	check_type_def module_index opt_icl_info type_index (class_defs, ts, ti, cs)
636
		| has_to_be_checked module_index opt_icl_info type_index
637
638
			= checkTypeDef type_index module_index class_defs ts ti cs
			= (class_defs, ts, ti, cs)
639
640
641
642
643
644

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

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
645
646
647
648
649
650
651
652
653
654
655
656
657

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

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

658
determineAttributeVariable attr_var=:{av_ident=attr_name=:{id_info}} oti=:{oti_heaps,oti_all_attrs} symbol_table
659
	# (entry=:{ste_kind,ste_def_level}, symbol_table) = readPtr id_info symbol_table
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
660
661
662
663
664
665
666
667
668
669
	| 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
670
671
672
673
674
instance toString DemandedAttributeKind where
	toString DAK_Ignore = "DAK_Ignore"
	toString DAK_Unique = "DAK_Unique"
	toString DAK_None = "DAK_None"
	
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
675

676
newAttribute :: !DemandedAttributeKind {#Char} TypeAttribute !*OpenTypeInfo !*CheckState -> (!TypeAttribute, !*OpenTypeInfo, !*CheckState)
677
newAttribute DAK_Ignore var_ident attr oti cs
678
679
680
681
682
683
	= case attr of
		TA_Multi
			-> (TA_Multi, oti, cs)
		TA_None
			-> (TA_Multi, oti, cs)
		_
684
685
			-> (TA_Multi, oti, { cs & cs_error = checkError var_ident "attribute not allowed" cs.cs_error })
newAttribute DAK_Unique var_ident new_attr  oti cs
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
686
687
688
689
690
691
692
693
	= case new_attr of
		TA_Unique
			-> (TA_Unique, oti, cs)
		TA_Multi
			-> (TA_Unique, oti, cs)
		TA_None
			-> (TA_Unique, oti, cs)
		_
694
695
			-> (TA_Unique, oti, { cs & cs_error = checkError var_ident "inconsistently attributed (2)" cs.cs_error })
newAttribute DAK_None var_ident (TA_Var attr_var) oti cs=:{cs_symbol_table}
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
696
	# (attr_var, oti, cs_symbol_table) = determineAttributeVariable attr_var oti cs_symbol_table
697
	= (TA_Var attr_var, oti, {cs & cs_symbol_table = cs_symbol_table})
698
newAttribute DAK_None var_ident TA_Anonymous oti=:{oti_heaps, oti_all_attrs} cs
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
699
	# (new_attr_ptr, th_attrs) = newPtr AVI_Empty oti_heaps.th_attrs
700
701
	  new_attr = {av_info_ptr = new_attr_ptr, av_ident = emptyIdent var_ident}
	= (TA_Var new_attr, {oti & oti_heaps = {oti_heaps & th_attrs = th_attrs}, oti_all_attrs = [new_attr : oti_all_attrs] }, cs)
702
newAttribute DAK_None var_ident TA_Unique oti cs
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
703
	= (TA_Unique, oti, cs)
704
newAttribute DAK_None var_ident attr oti cs
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
705
706
707
708
709
710
	= (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
711
		# (type_def, type_defs) = type_defs![type_index]
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
712
		= (type_def, type_index, type_defs, modules)
713
		# ({dcl_common={com_type_defs}}, modules) = modules![type_module]
714
		  type_def = com_type_defs.[type_index]
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
715
716
		= (type_def, type_index, type_defs, modules)

717
718
719
720
721
checkArityOfType act_arity form_arity (SynType _)
	= form_arity == act_arity
checkArityOfType act_arity form_arity _
	= form_arity >= act_arity

John van Groningen's avatar
John van Groningen committed
722
checkAbstractType type_index (AbstractType _)			= type_index <> cPredefinedModuleIndex 
723
724
checkAbstractType type_index (AbstractSynType _ _)		= type_index <> cPredefinedModuleIndex 
checkAbstractType _ _									= False
725

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
726
727
728
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
729
		# (class_def, class_defs) = class_defs![class_index]
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
730
		= (class_def, class_index, class_defs, modules)
731
		# ({dcl_common={com_class_defs}}, modules) = modules![type_module]
732
		  class_def = com_class_defs.[class_index]
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
733
734
		= (class_def, class_index, class_defs, modules)

735
736
checkTypeVar :: !Level !DemandedAttributeKind !TypeVar !TypeAttribute !(!*OpenTypeInfo, !*CheckState)
					-> (! TypeVar, !TypeAttribute, !(!*OpenTypeInfo, !*CheckState))
737
checkTypeVar scope dem_attr tv=:{tv_ident=var_ident=:{id_name,id_info}} tv_attr (oti, cs=:{cs_symbol_table})
738
	# (entry=:{ste_kind,ste_def_level},cs_symbol_table) = readPtr id_info cs_symbol_table
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
739
	| ste_kind == STE_Empty || ste_def_level == cModuleScope
740
		# (new_attr, oti=:{oti_heaps,oti_all_vars}, cs) = newAttribute dem_attr id_name tv_attr oti {cs & cs_symbol_table = cs_symbol_table}
741
		  (new_var_ptr, th_vars) = newPtr (TVI_AttrAndRefCount new_attr 1) oti_heaps.th_vars
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
742
		  new_var = { tv & tv_info_ptr = new_var_ptr }
743
		= (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
744
745
746
747
				{ 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
748
749
		  (tv_info, th_vars) = readPtr tv_info_ptr oti_heaps.th_vars
		  th_vars = incr_ref_count tv_info_ptr tv_info th_vars	
750
751
752
		  (var_attr, oti, cs) = check_attribute id_name dem_attr tv_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
753
where
754
755
756
757
758
	incr_ref_count tv_info_ptr (TVI_AttrAndRefCount prev_attr ref_count) th_vars
		= th_vars <:=	(tv_info_ptr, TVI_AttrAndRefCount prev_attr (inc ref_count))			
	incr_ref_count tv_info_ptr _ th_vars
		= th_vars

759
	check_attribute var_ident DAK_Ignore (TVI_AttrAndRefCount prev_attr ref_count) this_attr oti cs=:{cs_error}
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
760
		= (TA_Multi, oti, cs)
761
762
	check_attribute var_ident dem_attr (TVI_AttrAndRefCount prev_attr ref_count) this_attr oti cs=:{cs_error}
		# (new_attr, cs_error) = determine_attribute var_ident dem_attr this_attr cs_error
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
763
764
765
766
767
768
769
		= 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,
770
						cs_error = checkError new_var.av_ident "inconsistently attributed (3)" cs_error })
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
771
772
773
774
775
776
777
		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)
				_
778
					-> (TA_Unique, oti, { cs & cs_error = checkError var_ident "inconsistently attributed (4)" cs.cs_error })
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
779
780
781
782
783
784
785
		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)
				_
786
					-> (TA_Multi, oti, { cs & cs_error = checkError var_ident "inconsistently attributed (5)" cs.cs_error })
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
787
		check_var_attribute var_attr new_attr oti cs
788
			= (var_attr, oti, { cs & cs_error = checkError var_ident "inconsistently attributed (6)" cs.cs_error })// ---> (var_attr, new_attr)
John van Groningen's avatar
John van Groningen committed
789

790
		determine_attribute var_ident DAK_Unique new_attr error
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
791
792
793
794
795
796
797
798
			= case new_attr of
				 TA_Multi
				 	-> (TA_Unique, error)
				 TA_None
				 	-> (TA_Unique, error)
				 TA_Unique
				 	-> (TA_Unique, error)
				 _
799
800
				 	-> (TA_Unique, checkError var_ident "inconsistently attributed (1)" error)
		determine_attribute var_ident dem_attr TA_None error
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
801
			= (TA_Multi, error)
802
		determine_attribute var_ident dem_attr new_attr error
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
803
			= (new_attr, error)
804
	check_attribute var_ident dem_attr _ this_attr oti cs
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
805
806
		= (TA_Multi, oti, cs)

807
808
809
810
811
812
813
814
815
816
817
818
819
820
check_args_of_type_cons :: !Index !Int !DemandedAttributeKind ![AType] ![ATypeVar] !(!u:OpenTypeSymbols, !*OpenTypeInfo, !*CheckState)
	-> (![AType], !(!u:OpenTypeSymbols, !*OpenTypeInfo, !*CheckState))
check_args_of_type_cons mod_index scope dem_attr_kind [] _ cot_state
	= ([], cot_state)
check_args_of_type_cons mod_index scope dem_attr_kind [arg_type : arg_types] [ {atv_attribute} : td_args ] cot_state
	# (arg_type, cot_state) = checkOpenAType mod_index scope (new_demanded_attribute dem_attr_kind /* DAK_None */ atv_attribute) arg_type cot_state
	  (arg_types, cot_state) = check_args_of_type_cons mod_index scope dem_attr_kind 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_kind _
821
	= DAK_None /* dem_attr_kind */
822

823
824
825
checkOpenArgAType :: !Index !Int !DemandedAttributeKind !AType !(!u:OpenTypeSymbols, !*OpenTypeInfo, !*CheckState)
												   -> (!AType, !(!u:OpenTypeSymbols, !*OpenTypeInfo, !*CheckState))
checkOpenArgAType mod_index scope dem_attr atype=:{at_type = TFA vars type, at_attribute} (ots, oti, cs)
826
	# (vars, (oti, cs)) = add_universal_vars vars oti cs
827
	  (checked_type, (ots, oti, cs)) = checkOpenAType mod_index cRankTwoScope dem_attr { atype & at_type = type } (ots, oti, cs)
828
829
	  cs = {cs & cs_symbol_table = remove_universal_vars vars cs.cs_symbol_table}
	= ({checked_type & at_type = TFA vars checked_type.at_type }, (ots, oti, cs))
830
831
832
833
834
checkOpenArgAType mod_index scope dem_attr atype=:{at_type = TFAC vars type contexts, at_attribute} (ots, oti, cs)
	# cs = add_universal_vars_again vars cs
	  (checked_type, (ots, oti, cs)) = checkOpenAType mod_index cRankTwoScope dem_attr {atype & at_type = type} (ots, oti, cs)
	  cs = {cs & cs_symbol_table = remove_universal_vars vars cs.cs_symbol_table}
	= ({checked_type & at_type = TFAC vars checked_type.at_type contexts}, (ots, oti, cs))
835
836
837
checkOpenArgAType mod_index scope dem_attr type ots_oti_cs
	= checkOpenAType mod_index scope dem_attr type ots_oti_cs

838
checkOpenAType :: !Index !Int !DemandedAttributeKind !AType !(!u:OpenTypeSymbols, !*OpenTypeInfo, !*CheckState)
839
												-> (!AType, !(!u:OpenTypeSymbols, !*OpenTypeInfo, !*CheckState))
840
checkOpenAType mod_index scope dem_attr type=:{at_type = TV tv, at_attribute} (ots, oti, cs)
841
	# (tv, at_attribute, (oti, cs)) = checkTypeVar scope dem_attr tv at_attribute (oti, cs) 
842
	= ({ type & at_type = TV tv, at_attribute = at_attribute }, (ots, oti, cs))
843
844
845
checkOpenAType mod_index scope dem_attr type=:{at_type = GTV var_id=:{tv_ident={id_info}}, at_attribute} (ots, oti, cs)
	# (new_attr, oti=:{oti_heaps,oti_global_vars}, cs=:{cs_symbol_table}) = newAttribute dem_attr "GTV" at_attribute oti cs
	  (entry, cs_symbol_table) = readPtr id_info cs_symbol_table
846
	  (type_var, oti_global_vars, th_vars, entry) = retrieve_global_variable var_id entry oti_global_vars oti_heaps.th_vars
847
	= ({type & at_type = TV type_var, at_attribute = new_attr }, (ots, { oti & oti_heaps = { oti_heaps & th_vars = th_vars }, oti_global_vars = oti_global_vars },
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
								{ 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 })
868
checkOpenAType mod_index scope dem_attr_kind type=:{ at_type=TA type_cons=:{type_ident=type_ident=:{id_name,id_info}} types, at_attribute}
869
		(ots=:{ots_type_defs,ots_modules}, oti, cs=:{cs_symbol_table,cs_x={x_check_dynamic_types}})