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

import StdEnv, StdCompare
4
import syntax, parse, check, unitype, utilities, checktypes, compilerSwitches
5
import genericsupport
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

::	Store	:== Int

::	AttrCoercion =
	{	ac_demanded	:: !Int
	,	ac_offered	:: !Int
	}

::	TempSymbolType =
	{	tst_args		:: ![AType]
	,	tst_arity		:: !Int
	,	tst_lifted		:: !Int
	,	tst_result		:: !AType
	,	tst_context		:: ![TypeContext]
	,	tst_attr_env	:: ![AttrCoercion]
	}

Sjaak Smetsers's avatar
Sjaak Smetsers committed
23
24
25
::	FunctionType = CheckedType !SymbolType | SpecifiedType !SymbolType ![AType] !TempSymbolType
				 | UncheckedType !TempSymbolType | ExpandedType !SymbolType !TempSymbolType !TempSymbolType  | EmptyFunctionType

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
26

27
28
29
30
31
32
33
34
35
36
simplifyTypeApplication :: !Type ![AType] -> Type
simplifyTypeApplication type type_args
	# (ok, type)
		=	simplifyAndCheckTypeApplication type type_args
	| not ok
		=	abort "typesupport.simplifyTypeApplication: unexpected error"
	=	type

simplifyAndCheckTypeApplication :: !Type ![AType] -> (!Bool, !Type)
simplifyAndCheckTypeApplication (TA type_cons=:{type_arity} cons_args) type_args
Martin Wierich's avatar
Martin Wierich committed
37
	= (True, TA { type_cons & type_arity = type_arity + length type_args } (cons_args ++ type_args))
38
simplifyAndCheckTypeApplication (TAS type_cons=:{type_arity} cons_args strictness) type_args
39
	= (True, TAS { type_cons & type_arity = type_arity + length type_args } (cons_args ++ type_args) strictness)
40
simplifyAndCheckTypeApplication (CV tv :@: type_args1) type_args2
Martin Wierich's avatar
Martin Wierich committed
41
	= (True, CV tv :@: (type_args1 ++ type_args2))
42
simplifyAndCheckTypeApplication TArrow [type1, type2] 
43
	= (True, type1 --> type2)
44
simplifyAndCheckTypeApplication TArrow [type] 
45
	= (True, TArrow1 type)
46
simplifyAndCheckTypeApplication (TArrow1 type1) [type2] 
47
	= (True, type1 --> type2)
48
simplifyAndCheckTypeApplication (TV tv) type_args
49
	= (True, CV tv :@: type_args)
50
51
52
53
simplifyAndCheckTypeApplication (TempV i) type_args
	= (True, TempCV i :@: type_args)
simplifyAndCheckTypeApplication type type_args
	= (False, type)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
54
55
56
57
58

::	AttributeEnv	:== {! TypeAttribute }
::	VarEnv 			:== {! Type }

::	CleanUpState =
59
60
	{	cus_var_env					:: !.VarEnv
	,	cus_attr_env				:: !.AttributeEnv
Martin Wierich's avatar
Martin Wierich committed
61
	,	cus_appears_in_lifted_part	:: !.LargeBitvect
62
63
64
65
66
	,	cus_heaps					:: !.TypeHeaps
	,	cus_var_store				:: !Int
	,	cus_attr_store				:: !Int
	,	cus_exis_vars				:: ![(Int,TypeAttribute)]
	,	cus_error					:: !.ErrorAdmin
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
67
68
	}

69
::	CleanUpInput =
70
71
72
	{	cui_coercions		:: !{! CoercionTree}
	,	cui_attr_part		:: !AttributePartition
	,	cui_top_level		:: !Bool
Martin Wierich's avatar
Martin Wierich committed
73
	,	cui_is_lifted_part	:: !Bool
74
	}
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
75

76
class clean_up a ::  !CleanUpInput !a !*CleanUpState -> (!a, !*CleanUpState)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
77
78
79

instance clean_up AType
where
80
81
82
83
84
	clean_up cui atype=:{at_attribute, at_type = TempQV qv_number} cus
		| cui.cui_top_level
			# (at_attribute, cus)	= cleanUpTypeAttribute True cui at_attribute cus
			# (type, cus)			= cus!cus_var_env.[qv_number]
			  (var, cus)			= cleanUpVariable True type qv_number cus
85
			= ({atype & at_attribute = at_attribute, at_type = var},
86
87
88
89
90
91
					{cus & cus_exis_vars = add_new_variable type qv_number at_attribute cus.cus_exis_vars})
	where			
		add_new_variable TE ev_number ev_attr cus_exis_vars
			= [(ev_number, ev_attr) : cus_exis_vars]
		add_new_variable type ev_number ev_attr cus_exis_vars
			= cus_exis_vars
92
	clean_up cui atype=:{at_attribute,at_type} cus
93
		# (at_attribute, cus) = cleanUpTypeAttribute False cui at_attribute cus 
94
		  (at_type, cus) = clean_up cui at_type cus
95
		= ({atype & at_attribute = at_attribute, at_type = at_type}, cus)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
96

97

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
98
99
100
attrIsUndefined TA_None = True
attrIsUndefined _ 		= False

101
102
103
104
105
106
107
108
109
110
cleanUpTypeAttribute :: !Bool !CleanUpInput TypeAttribute !*CleanUpState -> (!TypeAttribute, !*CleanUpState)
cleanUpTypeAttribute _ cui TA_Unique cus
	= (TA_Unique, cus)
cleanUpTypeAttribute _ cui TA_Multi cus
	= (TA_Multi, cus)
cleanUpTypeAttribute may_be_existential cui tv=:(TA_TempVar av_number) cus
	| cui.cui_top_level
		# av_group_nr = cui.cui_attr_part.[av_number]
		  coercion_tree = cui.cui_coercions.[av_group_nr]
		| isNonUnique coercion_tree
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
111
			= (TA_Multi, cus)
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
		| isUnique coercion_tree
			= (TA_Unique, cus)
		# cus 			= check_appearance cui.cui_is_lifted_part av_group_nr cus
		# (attr, cus)	= clean_up_attribute_variable av_group_nr (cus!cus_attr_env.[av_group_nr])
		| isExistential coercion_tree
			| may_be_existential
				= (attr, { cus & cus_error = checkError "attribute variable could not be universally quantified" "" cus.cus_error})
				= (attr, cus)
			= (attr, cus)
		= (TA_Multi, cus)
where
	check_appearance is_lifted_part group_nr cus=:{cus_appears_in_lifted_part, cus_error}
		| is_lifted_part
			= { cus & cus_appears_in_lifted_part = bitvectSet group_nr cus_appears_in_lifted_part}
		| bitvectSelect group_nr cus_appears_in_lifted_part
			= { cus &	cus_appears_in_lifted_part = bitvectReset group_nr cus_appears_in_lifted_part,
						cus_error = checkError "attribute variable of lifted argument appears in the specified type" "" cus_error}
			= cus

	clean_up_attribute_variable av_group_nr (TA_None, cus=:{cus_heaps,cus_attr_store,cus_attr_env})
		# (av_info_ptr, th_attrs) = newPtr AVI_Empty cus_heaps.th_attrs
133
		  new_attr_var = TA_Var { av_ident = NewAttrVarId cus_attr_store, av_info_ptr = av_info_ptr }
134
135
136
137
138
139
		= (new_attr_var, { cus &	cus_attr_env = { cus_attr_env & [av_group_nr] = new_attr_var},
				 					cus_heaps = { cus_heaps & th_attrs = th_attrs }, cus_attr_store = inc cus_attr_store})	
	clean_up_attribute_variable av_group_nr attr_and_cus
		= attr_and_cus
		
cleanUpTypeAttribute _ cui av=:(TA_Var _) cus
140
	= (av, cus)			
141
			
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
142
143
instance clean_up Type
where
144
145
	clean_up cui (TempV tv_number) cus
		# (type, cus) = cus!cus_var_env.[tv_number]
146
147
148
		= cleanUpVariable cui.cui_top_level type tv_number cus
	clean_up cui (TA tc types) cus
		# (types, cus) = clean_up cui types cus
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
149
		= (TA tc types, cus)
150
151
152
	clean_up cui (TAS tc types strictness) cus
		# (types, cus) = clean_up cui types cus
		= (TAS tc types strictness, cus)
153
154
155
	clean_up cui (argtype --> restype) cus
		# (argtype, cus) = clean_up cui argtype cus
		  (restype, cus) = clean_up cui restype cus
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
156
		=  (argtype --> restype, cus)
157
158
159
160
//AA..
	clean_up cui (TArrow1 argtype) cus
		# (argtype, cus) = clean_up cui argtype cus
		=  (TArrow1 argtype, cus)
161
162
	clean_up cui t=:TArrow cus
		=  (t, cus)
163
//..AA		
164
	clean_up cui t=:(TB _) cus
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
165
		=  (t, cus)
166
	clean_up cui (TempCV tempvar :@: types) cus
167
		# (type, cus) = cus!cus_var_env.[tempvar]
168
169
		# (type, cus) = cleanUpVariable cui.cui_top_level type tempvar cus
		  (types, cus) = clean_up cui types cus
170
		= (simplifyTypeApplication type types, cus)
171
172
173
174
175
	clean_up cui (TempQCV tempvar :@: types) cus
		# (type, cus) = cus!cus_var_env.[tempvar]
		# (TV tv, cus) = cleanUpVariable cui.cui_top_level type tempvar cus
		  (types, cus) = clean_up cui types cus
		= (CV tv :@: types, cus)
176
177
178
	clean_up cui (cv :@: types) cus
		# (types, cus) = clean_up cui types cus
		= (cv :@: types, cus)
179
	clean_up cui (TempQV qv_number) cus=:{cus_error,cus_exis_vars}
180
		# (type, cus) = cus!cus_var_env.[qv_number]
181
		| cui.cui_top_level
182
			= cleanUpVariable True type qv_number {cus & cus_exis_vars = add_new_variable type qv_number cus_exis_vars}
183
			= cleanUpVariable False type qv_number cus
184
185
186
187
188
189
190
191
192
193
194
	where			
		add_new_variable TE qv_number cus_exis_vars
			= [(qv_number, TA_None) : cus_exis_vars]
		add_new_variable type qv_number cus_exis_vars
			= cus_exis_vars
			
	clean_up cui tv=:(TV _) cus
		= (tv, cus)
	clean_up cui (TFA vars type) cus=:{cus_heaps}
		# (type, cus) = clean_up cui type cus
		= (TFA vars type, cus)
195
196
	clean_up cui type cus
		= abort ("clean_up Type (typesupport.icl): unknown type " ---> ("clean_up Type", type))
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
197
198
199
				
instance clean_up [a] | clean_up a
where
200
	clean_up cui l cus = mapSt (clean_up cui) l cus
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
201

202
cleanUpVariable _ TE tv_number cus=:{cus_heaps,cus_var_store,cus_var_env}
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
203
	# (tv_info_ptr, th_vars) = newPtr TVI_Empty cus_heaps.th_vars
204
	  new_var = TV { tv_ident = NewVarId cus_var_store, tv_info_ptr = tv_info_ptr }
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
205
206
	= (new_var, { cus & cus_var_env = { cus_var_env & [tv_number] = new_var},
				cus_heaps = { cus_heaps & th_vars = th_vars }, cus_var_store = inc cus_var_store})
207
208
209
210
211
cleanUpVariable top_level (TLifted var) tv_number cus=:{cus_error}
	| top_level
		= (TV var, { cus & cus_error = liftedError var cus_error})
		= (TV var, cus)
cleanUpVariable _ type tv_number cus
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
212
213
	= (type, cus)

Sjaak Smetsers's avatar
Sjaak Smetsers committed
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233

::	CleanUpResult :== BITVECT

cClosed				:== 0
cDefinedVar			:== 1
cUndefinedVar		:== 2
cLiftedVar			:== 4

cleanUpClosedVariable TE env
	= (cUndefinedVar, TE, env)
cleanUpClosedVariable (TLifted tvar) env
	= (cLiftedVar, TV tvar, env)
cleanUpClosedVariable tvar env
	= (cDefinedVar, tvar, env)

combineCleanUpResults cur1 cur2 :== cur1 bitor cur2

checkCleanUpResult cur prop :== not (cur bitand prop == 0)

class cleanUpClosed a :: !a !u:VarEnv -> (!CleanUpResult, !a, !u:VarEnv)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
234
235
236
237

instance cleanUpClosed AType
where
	cleanUpClosed atype=:{at_type} env
Sjaak Smetsers's avatar
Sjaak Smetsers committed
238
239
		# (cur, at_type, env) = cleanUpClosed at_type env
		= (cur, { atype & at_attribute = TA_Multi, at_type = at_type}, env)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
240
241
242
243

instance cleanUpClosed Type
where
	cleanUpClosed (TempV tv_number) env
244
		# (type, env) = env![tv_number]
Sjaak Smetsers's avatar
Sjaak Smetsers committed
245
		= cleanUpClosedVariable type env
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
246
	cleanUpClosed (TA tc types) env
Sjaak Smetsers's avatar
Sjaak Smetsers committed
247
248
		# (cur, types, env) = cleanUpClosed types env
		= (cur, TA tc types, env)
249
250
251
	cleanUpClosed (TAS tc types strictness) env
		# (cur, types, env) = cleanUpClosed types env
		= (cur, TAS tc types strictness, env)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
252
	cleanUpClosed (argtype --> restype) env
Sjaak Smetsers's avatar
Sjaak Smetsers committed
253
254
		# (cur, (argtype,restype), env) = cleanUpClosed (argtype,restype) env
		= (cur, argtype --> restype, env)
255
256
257
	cleanUpClosed (TArrow1 argtype) env
		# (cur, argtype, env) = cleanUpClosed argtype env
		= (cur, TArrow1 argtype, env)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
258
	cleanUpClosed (TempCV tv_number :@: types) env
259
		# (type, env) = env![tv_number]
Sjaak Smetsers's avatar
Sjaak Smetsers committed
260
261
262
263
		# (cur1, type, env) = cleanUpClosedVariable type env
		| checkCleanUpResult cur1 cUndefinedVar
			= (cur1, TempCV tv_number :@: types, env)
			# (cur2, types, env) = cleanUpClosed types env
264
            = (combineCleanUpResults cur1 cur2, simplifyTypeApplication type types, env)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
265
	cleanUpClosed t env
Sjaak Smetsers's avatar
Sjaak Smetsers committed
266
		= (cClosed, t, env)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
267
268
269
270

instance cleanUpClosed (a,b) | cleanUpClosed a & cleanUpClosed b
where
	cleanUpClosed (x,y) env
Sjaak Smetsers's avatar
Sjaak Smetsers committed
271
272
273
274
275
		# (cur1, x, env) = cleanUpClosed x env
		| checkCleanUpResult cur1 cUndefinedVar
			= (cur1, (x,y), env)
			# (cur2, y, env) = cleanUpClosed y env
			= (combineCleanUpResults cur1 cur2, (x,y), env)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
276
277
278
279

instance cleanUpClosed [a] | cleanUpClosed a
where
	cleanUpClosed [] env
Sjaak Smetsers's avatar
Sjaak Smetsers committed
280
		= (cClosed, [], env)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
281
	cleanUpClosed [t:ts] env
Sjaak Smetsers's avatar
Sjaak Smetsers committed
282
283
		# (cur, (t,ts), env) = cleanUpClosed (t,ts) env
		= (cur, [t:ts], env)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
284

285
286
287
288
289
errorHeading :: !String !*ErrorAdmin -> *ErrorAdmin
errorHeading  error_kind err=:{ea_file,ea_loc = []}
	= { err & ea_file = ea_file <<< error_kind <<< ':', ea_ok = False }
errorHeading  error_kind err=:{ea_file,ea_loc = [ loc : _ ]}
	= { err & ea_file = ea_file <<< error_kind <<< ' ' <<< loc <<< ':', ea_ok = False }
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
290

Sjaak Smetsers's avatar
Sjaak Smetsers committed
291
292
293
294
295
296
297
contextError class_symb err
	# err = errorHeading "Overloading error" err
	= { err & ea_file = err.ea_file <<< " unresolved class \"" <<< class_symb <<< "\" not occurring in specified type\n"}

liftedContextError class_symb err
	# err = errorHeading "Overloading error" err
	= { err & ea_file = err.ea_file <<< " type variable of type of lifted argument appears in class \"" <<< class_symb <<< "\"\n"}
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
298
299

existentialError err
300
301
	# err = errorHeading "Type error" err
	= { err & ea_file = err.ea_file <<< "existential type variable appears in the derived type specification\n" }
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
302
303

liftedError var err
304
305
	# err = errorHeading "Type error" err
	= { err & ea_file = err.ea_file <<< "type variable of type of lifted argument " <<< var <<< " appears in the specified type\n" }
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
306

clean's avatar
clean committed
307
308
309
310
startRuleError mess err
	# err = errorHeading "Type error" err
	= { err & ea_file = err.ea_file <<< mess }

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
311
312
313
314
315
316
317
318
319
320
321
322
extendSymbolType :: !SymbolType !Int !*TypeHeaps -> (!SymbolType, !*TypeHeaps)
extendSymbolType st=:{st_arity,st_args,st_vars,st_attr_vars} nr_of_extra_args type_heaps
	| nr_of_extra_args > 0
		# (st_args, (st_vars, st_attr_vars, type_heaps))
			= newAttributedVariables nr_of_extra_args st_args (st_vars, st_attr_vars, type_heaps)
		= ({ st & st_args = st_args, st_vars = st_vars, st_attr_vars = st_attr_vars, st_arity = st_arity + nr_of_extra_args }, type_heaps)
		= (st, type_heaps)

cleanSymbolType :: !Int !*TypeHeaps -> (!SymbolType, !*TypeHeaps)
cleanSymbolType arity type_heaps
	# (st_result, clean_state) = newAttributedVariable 0 ([], [], type_heaps)
	  (st_args, (st_vars, st_attr_vars, type_heaps)) = newAttributedVariables arity [] clean_state
323
	= ({ st_arity = arity, st_vars = st_vars , st_args = st_args, st_args_strictness=NotStrict, st_result = st_result, st_context = [],
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
324
325
326
327
328
329
330
331
332
333
			st_attr_env = [], st_attr_vars = st_attr_vars }, type_heaps)

newAttributedVariables var_number attributed_variables clean_state=:(_,_,_) /* Temporary hack */
	| var_number == 0
		= (attributed_variables, clean_state)
		# (attributed_variable, clean_state) = newAttributedVariable var_number clean_state
		= newAttributedVariables (dec var_number) [ attributed_variable : attributed_variables ] clean_state

newAttributedVariable var_number (variables, attributes, type_heaps=:{th_vars,th_attrs})
	# (tv_info_ptr, th_vars) = newPtr TVI_Empty th_vars
334
	  new_var = { tv_ident = NewVarId var_number, tv_info_ptr = tv_info_ptr }
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
335
	  (av_info_ptr, th_attrs) = newPtr AVI_Empty th_attrs
336
	  new_attr_var = { av_ident = NewAttrVarId var_number, av_info_ptr = av_info_ptr }
337
	= ({ at_attribute = TA_Var new_attr_var, at_type = TV new_var},
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
338
339
		([ new_var : variables ], [ new_attr_var : attributes ], { type_heaps & th_vars = th_vars, th_attrs = th_attrs }))

Sjaak Smetsers's avatar
Sjaak Smetsers committed
340
341
342
cSpecifiedType	:== True
cDerivedType	:== False

clean's avatar
clean committed
343
cleanUpSymbolType :: !Bool !Bool !TempSymbolType ![TypeContext] ![ExprInfoPtr] !{! CoercionTree} !AttributePartition
Sjaak Smetsers's avatar
Sjaak Smetsers committed
344
345
						!*VarEnv !*AttributeEnv !*TypeHeaps !*VarHeap !*ExpressionHeap !*ErrorAdmin
							-> (!SymbolType, !*VarEnv, !*AttributeEnv, !*TypeHeaps, !*VarHeap, !*ExpressionHeap, !*ErrorAdmin)
clean's avatar
clean committed
346
cleanUpSymbolType is_start_rule spec_type tst=:{tst_arity,tst_args,tst_result,tst_context,tst_lifted} derived_context case_and_let_exprs
Sjaak Smetsers's avatar
Sjaak Smetsers committed
347
		coercions attr_part var_env attr_var_env heaps var_heap expr_heap error
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
348
349
	#! nr_of_temp_vars = size var_env
	#! max_attr_nr = size attr_var_env
Martin Wierich's avatar
Martin Wierich committed
350
	# cus = { cus_var_env = var_env, cus_attr_env = attr_var_env, cus_appears_in_lifted_part = bitvectCreate max_attr_nr,
351
				cus_heaps = heaps, cus_var_store = 0, cus_attr_store = 0, cus_error = error, cus_exis_vars = [] }
Martin Wierich's avatar
Martin Wierich committed
352
	  cui = { cui_coercions = coercions, cui_attr_part = attr_part, cui_top_level = True, cui_is_lifted_part = True }
353
	  (lifted_args, cus=:{cus_var_env}) = clean_up cui (take tst_lifted tst_args) cus
Martin Wierich's avatar
Martin Wierich committed
354
	  cui = { cui & cui_is_lifted_part = False }
355
	  (lifted_vars, cus_var_env) = determine_type_vars nr_of_temp_vars [] cus_var_env
356
357
	  (st_args, (_, cus))	= mapSt (clean_up_arg_type cui) (drop tst_lifted tst_args) ([], { cus & cus_var_env = cus_var_env })
	  (st_result, cus) = clean_up_result_type cui tst_result cus
Sjaak Smetsers's avatar
Sjaak Smetsers committed
358
	  (st_context, cus_var_env, var_heap, cus_error) = clean_up_type_contexts spec_type tst_context derived_context cus.cus_var_env var_heap cus.cus_error
359
	  (st_vars, cus_var_env) = determine_type_vars nr_of_temp_vars lifted_vars cus_var_env
Martin Wierich's avatar
Martin Wierich committed
360
361
	  (cus_attr_env, st_attr_vars, st_attr_env, cus_error)
	  		= build_attribute_environment cus.cus_appears_in_lifted_part 0 max_attr_nr coercions cus.cus_attr_env [] [] cus_error
362
	  (expr_heap, {cus_var_env,cus_attr_env,cus_heaps,cus_error}) = update_expression_types { cui & cui_top_level = False } case_and_let_exprs
Martin Wierich's avatar
Martin Wierich committed
363
364
365
				expr_heap { cus & cus_var_env = cus_var_env, cus_attr_env = cus_attr_env,
							 cus_appears_in_lifted_part = {el\\el<-:cus.cus_appears_in_lifted_part},
							 cus_error = cus_error }
366
	  st = {  st_arity = tst_arity, st_vars = st_vars , st_args = lifted_args ++ st_args, st_args_strictness=NotStrict, st_result = st_result, st_context = st_context,
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
367
			st_attr_env = st_attr_env, st_attr_vars = st_attr_vars }
clean's avatar
clean committed
368
	  cus_error = check_type_of_start_rule is_start_rule st cus_error
369
	= (st,			{ cus_var_env & [i] = TE \\ i <- [0..nr_of_temp_vars - 1]},
Sjaak Smetsers's avatar
Sjaak Smetsers committed
370
371
					{ cus_attr_env & [i] = TA_None \\ i <- [0..max_attr_nr - 1]}, cus_heaps, var_heap, expr_heap, cus_error)
//					---> ("cleanUpSymbolType", st)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
372
where
373
374
375
376
	determine_type_vars to_index all_vars var_env
		= iFoldSt determine_type_var 0 to_index (all_vars, var_env)
	where
		determine_type_var var_index (all_vars, var_env)
377
			# (type, var_env) = var_env![var_index]
378
379
380
381
382
383
			= case type of
				TV var
					-> ([var : all_vars], { var_env & [var_index] = TLifted var})
				_
					-> (all_vars, var_env)

384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
	clean_up_arg_type cui at=:{at_type = TFA avars type, at_attribute} (all_exi_vars, cus)
		# (at_attribute, cus) 	= cleanUpTypeAttribute False cui at_attribute cus
		  (type, cus)			= clean_up cui type cus
		| isEmpty cus.cus_exis_vars
			= ({ at & at_type = TFA avars type, at_attribute = at_attribute}, (all_exi_vars, cus))
			= ({ at & at_type = TFA avars type, at_attribute = at_attribute},
					(all_exi_vars, { cus & cus_error = existentialError cus.cus_error, cus_exis_vars = [] }))
	clean_up_arg_type cui at (all_exi_vars, cus)
		# (at, cus) = clean_up cui at cus
		  (cus_exis_vars, cus) = cus!cus_exis_vars
		| isEmpty cus_exis_vars
			= (at, (all_exi_vars, cus))
			# (new_exi_vars, all_exi_vars, cus) = foldSt check_existential_var cus_exis_vars ([], all_exi_vars, cus)
			= ({ at & at_type = TFA new_exi_vars at.at_type }, (all_exi_vars, { cus & cus_exis_vars = [] }))
	where
		check_existential_var (var_number,var_attr) (exi_vars, all_vars, cus)
			| isMember var_number all_vars
				# (type, cus) = cus!cus_var_env.[var_number]
				= case type of
					TE
						-> (exi_vars, all_vars, cus)
					_
						-> (exi_vars, all_vars, { cus & cus_var_env = { cus.cus_var_env & [var_number] = TE }, cus_error = existentialError cus.cus_error })
				# (TV var, cus) = cus!cus_var_env.[var_number]
408
				= ([{atv_attribute = var_attr, atv_variable = var } : exi_vars ],
409
410
411
412
413
414
415
						[var_number : all_vars], { cus & cus_var_env = { cus.cus_var_env & [var_number] = TE }})

	clean_up_result_type cui at cus
		# (at, cus=:{cus_exis_vars}) = clean_up cui at cus
		| isEmpty cus_exis_vars
			= (at, cus)
			= (at, { cus & cus_error = existentialError cus.cus_error })
416

Sjaak Smetsers's avatar
Sjaak Smetsers committed
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
	clean_up_type_contexts spec_type spec_context derived_context env var_heap error
		|  spec_type
			# var_heap = foldSt (mark_specified_context derived_context) spec_context var_heap
			  (rev_contexts, env, error) = foldSt clean_up_lifted_type_context derived_context ([], env, error)
			  (rev_contexts, env, error) = foldSt clean_up_type_context spec_context (rev_contexts, env, error)
			= (reverse rev_contexts, env, var_heap, error)
			# (rev_contexts, env, error) = foldSt clean_up_type_context derived_context ([], env, error)
			= (reverse rev_contexts, env, var_heap, error)

	mark_specified_context [] spec_tc var_heap
		= var_heap
	mark_specified_context [tc=:{tc_var} : tcs] spec_tc var_heap
		| spec_tc == tc
			| spec_tc.tc_var == tc_var
				= var_heap
				= var_heap <:= (spec_tc.tc_var, VI_ForwardClassVar tc_var)
			= mark_specified_context tcs spec_tc var_heap
				
435
436
	clean_up_type_context tc=:{tc_types, tc_class} (collected_contexts, env, error)
		# (cur, tc_types, env) = cleanUpClosed tc_types env
Sjaak Smetsers's avatar
Sjaak Smetsers committed
437
438
439
		| checkCleanUpResult cur cUndefinedVar
			= (collected_contexts, env, error)
		| checkCleanUpResult cur cLiftedVar
440
			= ([{ tc & tc_types = tc_types } : collected_contexts ], env, liftedContextError (toString tc_class) error)
Sjaak Smetsers's avatar
Sjaak Smetsers committed
441
442
443
444
445
446
			= ([{ tc & tc_types = tc_types } : collected_contexts ], env, error)

	clean_up_lifted_type_context tc=:{tc_types,tc_var} (collected_contexts, env, error)
		# (cur, tc_types, env) = cleanUpClosed tc.tc_types env
		| checkCleanUpResult cur cLiftedVar
			| checkCleanUpResult cur cDefinedVar
447
				= (collected_contexts, env, liftedContextError (toString tc.tc_class) error)
Sjaak Smetsers's avatar
Sjaak Smetsers committed
448
449
450
451
				= ([{ tc & tc_types = tc_types } : collected_contexts], env, error)
		| otherwise
			= (collected_contexts, env, error)
				
Martin Wierich's avatar
Martin Wierich committed
452
453
454
	build_attribute_environment :: !LargeBitvect !Index !Index !{! CoercionTree} !*AttributeEnv ![AttributeVar] ![AttrInequality] !*ErrorAdmin
		-> (!*AttributeEnv, ![AttributeVar], ![AttrInequality], !*ErrorAdmin)
	build_attribute_environment appears_in_lifted_part attr_group_index max_attr_nr coercions attr_env attr_vars inequalities error
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
455
		| attr_group_index == max_attr_nr
Martin Wierich's avatar
Martin Wierich committed
456
			= (attr_env, attr_vars, inequalities, error)
457
		# (attr, attr_env) = attr_env![attr_group_index]
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
458
459
		= case attr of
			TA_Var attr_var
Martin Wierich's avatar
Martin Wierich committed
460
461
462
463
464
465
466
467
468
469
470
				# (ok, attr_env, inequalities)
						= build_inequalities appears_in_lifted_part (bitvectSelect attr_group_index appears_in_lifted_part)
								attr_var coercions.[attr_group_index] coercions attr_env inequalities
				  error
				  		= case ok of
				  			True
				  				-> error
				  			_
				  				-> checkError "attribute variable of lifted argument appears in derived attribute inequality"
										"" error
				-> build_attribute_environment appears_in_lifted_part (inc attr_group_index) max_attr_nr coercions attr_env [attr_var : attr_vars] inequalities error
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
471
			TA_None
Martin Wierich's avatar
Martin Wierich committed
472
				-> build_attribute_environment appears_in_lifted_part (inc attr_group_index) max_attr_nr coercions attr_env attr_vars inequalities error
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
473
	
474
	build_inequalities :: {#Int} Bool AttributeVar !CoercionTree {!CoercionTree} *{!TypeAttribute} [AttrInequality] -> (!Bool,!*{!TypeAttribute},![AttrInequality])
Martin Wierich's avatar
Martin Wierich committed
475
476
477
478
479
480
	build_inequalities appears_in_lifted_part off_appears_in_lifted_part off_var (CT_Node dem_attr left right)
				coercions attr_env inequalities
		# (ok1, attr_env, inequalities)
				= build_inequalities appears_in_lifted_part off_appears_in_lifted_part off_var left coercions attr_env inequalities
		  (ok2, attr_env, inequalities)
		  		= build_inequalities appears_in_lifted_part off_appears_in_lifted_part off_var right coercions attr_env inequalities
481
		# (attr, attr_env) = attr_env![dem_attr]
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
482
483
484
		= case attr of
			TA_Var attr_var
				| is_new_inequality attr_var off_var inequalities
Martin Wierich's avatar
Martin Wierich committed
485
486
487
					# ok3 = off_appears_in_lifted_part == bitvectSelect dem_attr appears_in_lifted_part
					-> (ok1 && ok2 && ok3, attr_env, [{ ai_demanded = attr_var, ai_offered = off_var } : inequalities]) 
					-> (ok1 && ok2, attr_env, inequalities)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
488
			TA_None
Martin Wierich's avatar
Martin Wierich committed
489
490
491
492
493
494
				# (ok3, attr_env, inequalities)
						= build_inequalities appears_in_lifted_part off_appears_in_lifted_part 
								off_var coercions.[dem_attr] coercions attr_env inequalities
				-> (ok1 && ok2 && ok3, attr_env, inequalities)
	build_inequalities _ _ off_var tree coercions attr_env inequalities
		= (True, attr_env, inequalities)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
495
496
497
498
499
500

	is_new_inequality dem_var off_var []
		= True
	is_new_inequality dem_var off_var [{ ai_demanded, ai_offered } : inequalities]
		= (dem_var <> ai_demanded || off_var <> ai_offered) && is_new_inequality dem_var off_var inequalities

501
502
	update_expression_types :: !CleanUpInput ![ExprInfoPtr] !*ExpressionHeap !*CleanUpState -> (!*ExpressionHeap,!*CleanUpState);
	update_expression_types cui expr_ptrs expr_heap cus
Sjaak Smetsers's avatar
Sjaak Smetsers committed
503
504
//		= (expr_heap, cus)
		= foldSt (update_expression_type cui) expr_ptrs (expr_heap, cus)
505

506
	update_expression_type cui expr_ptr (expr_heap, cus)
507
508
509
		# (info, expr_heap) = readPtr expr_ptr expr_heap
		= case info of
			EI_CaseType case_type
510
				# (case_type, cus) = clean_up cui case_type cus
511
512
				-> (expr_heap <:= (expr_ptr, EI_CaseType case_type), cus)
			EI_LetType let_type
513
				# (let_type, cus) = clean_up cui let_type cus
514
				-> (expr_heap <:= (expr_ptr, EI_LetType let_type), cus)
Sjaak Smetsers's avatar
Sjaak Smetsers committed
515
516
517
518
			EI_DictionaryType dict_type
				# (dict_type, cus) = clean_up cui dict_type cus
				-> (expr_heap <:= (expr_ptr, EI_DictionaryType dict_type), cus)

519

clean's avatar
clean committed
520
521
522
523
524
525
526
527
528
529
530
531
532
533
 	check_type_of_start_rule is_start_rule {st_context,st_arity,st_args} cus_error
 		| is_start_rule
 			| isEmpty st_context
	 			| st_arity > 0
	 				| st_arity == 1
		 				= case st_args of
		 					[{at_type = TB BT_World} : _]
		 						-> cus_error
		 					_
		 						-> startRuleError "argument of Start rule should have type World.\n" cus_error
						= startRuleError "Start rule has too many arguments.\n" cus_error						
					= cus_error						
	 			= startRuleError "Start rule cannot be overloaded.\n" cus_error
	 		= cus_error
534
535
	 
	 	
536
537
instance clean_up CaseType
where
538
539
540
	clean_up cui ctype=:{ct_pattern_type,ct_result_type, ct_cons_types} cus
		# (ct_pattern_type, cus) = clean_up cui ct_pattern_type cus 
		  (ct_result_type, cus) = clean_up cui ct_result_type cus
541
		  (ct_cons_types, cus) = mapSt (mapSt (clean_up_arg_type cui)) ct_cons_types cus
542
		= ({ctype & ct_pattern_type = ct_pattern_type, ct_cons_types = ct_cons_types, ct_result_type = ct_result_type}, cus)
543
544
545
546
547
548
549
550
	where
		clean_up_arg_type cui at=:{at_type = TFA avars type, at_attribute} cus
			# (at_attribute, cus) 	= cleanUpTypeAttribute False cui at_attribute cus
			  (type, cus)			= clean_up cui type cus
			= ({ at & at_type = TFA avars type, at_attribute = at_attribute}, cus)
		clean_up_arg_type cui at cus
			= clean_up cui at cus

Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
551

552
553
554
555
556
557
/*
	In 'bindInstances t1 t2' type variables of t1 are bound to the corresponding subtypes of t2, provided that
	t2 is a substitution instance of t1. Binding is done by setting the 'tv_info_ptr' of the variables of t1
	to 'TVI_Type t' were t is the subtype to which the type variable is matched.
	Be careful with calling 'bindInstances': all the 'tv_info_ptr'-info's should be cleaned first, unless one 
	is sure that t1 does not contain any 'tv_info_ptr' with value  'TVI_Type ...'.
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
558
	
559

560
561
562
563
	instance bindInstances AType, Type, [a] | bindInstances a
*/ 

updateExpressionTypes :: !SymbolType !SymbolType ![ExprInfoPtr] !*TypeHeaps !*ExpressionHeap -> (!*TypeHeaps, !*ExpressionHeap)
Sjaak Smetsers's avatar
Sjaak Smetsers committed
564
updateExpressionTypes {st_args,st_vars,st_result,st_attr_vars} st_copy type_ptrs heaps=:{th_vars,th_attrs} expr_heap
565
566
	# th_vars = foldSt (\{tv_info_ptr} var_heap -> var_heap <:= (tv_info_ptr, TVI_Empty)) st_vars th_vars
	  th_attrs = foldSt (\{av_info_ptr} attr_heap -> attr_heap <:= (av_info_ptr, AVI_Empty)) st_attr_vars th_attrs
567
568
569
	  heaps = fold2St bind_instances_in_arg_type st_args st_copy.st_args {heaps & th_vars = th_vars, th_attrs = th_attrs}
	  th_vars = bindInstances st_result st_copy.st_result heaps.th_vars
	= foldSt update_expression_type type_ptrs ({heaps & th_vars = th_vars}, expr_heap)
570
where
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
	bind_instances_in_arg_type { at_type = TFA vars type1 } { at_type = TFA _ type2 } heaps
		# heaps = foldSt clear_atype_var vars heaps
		= { heaps & th_vars = bindInstances type1 type2 heaps.th_vars }
	where
		clear_atype_var {atv_variable={tv_info_ptr},atv_attribute} heaps=:{th_vars,th_attrs}
			= { heaps & th_vars = th_vars  <:= (tv_info_ptr, TVI_Empty), th_attrs = clear_attribute atv_attribute th_attrs }
		where
			clear_attribute (TA_Var {av_info_ptr}) attr_heap
				= attr_heap <:= (av_info_ptr, AVI_Empty)
			clear_attribute _ attr_heap
				= attr_heap
	bind_instances_in_arg_type { at_type } atype2 heaps=:{th_vars}
		= { heaps & th_vars = bindInstances at_type atype2.at_type th_vars }


586
587
588
589
	update_expression_type expr_ptr (type_heaps, expr_heap)
		# (info, expr_heap) = readPtr expr_ptr expr_heap
		= case info of
			EI_CaseType case_type
590
				# (case_type, type_heaps) = substitute case_type type_heaps
591
592
				-> (type_heaps, expr_heap <:= (expr_ptr, EI_CaseType case_type))
			EI_LetType let_type
593
				# (let_type, type_heaps) = substitute let_type type_heaps
594
				-> (type_heaps, expr_heap <:= (expr_ptr, EI_LetType let_type))
Sjaak Smetsers's avatar
Sjaak Smetsers committed
595
			EI_DictionaryType dict_type
596
				# (dict_type, type_heaps) = substitute dict_type type_heaps
Sjaak Smetsers's avatar
Sjaak Smetsers committed
597
				-> (type_heaps, expr_heap <:= (expr_ptr, EI_DictionaryType dict_type))
598
599
600
601
602


class bindInstances a :: !a !a !*TypeVarHeap -> *TypeVarHeap

instance bindInstances Type
603
  where
604
605
606
607
	bindInstances (TV {tv_info_ptr}) type type_var_heap
		# (tv_info, type_var_heap) = readPtr tv_info_ptr type_var_heap
		= case tv_info of
			TVI_Type ind_type
608
				-> type_var_heap
609
610
611
612
			_
				-> type_var_heap <:= (tv_info_ptr, TVI_Type type)
	bindInstances (TA _ arg_types1) (TA _ arg_types2) type_var_heap
		= bindInstances arg_types1 arg_types2 type_var_heap
613
614
615
616
617
618
	bindInstances (TA _ arg_types1) (TAS _ arg_types2 _) type_var_heap
		= bindInstances arg_types1 arg_types2 type_var_heap
	bindInstances (TAS _ arg_types1 _) (TA _ arg_types2) type_var_heap
		= bindInstances arg_types1 arg_types2 type_var_heap
	bindInstances (TAS _ arg_types1 _) (TAS _ arg_types2 _) type_var_heap
		= bindInstances arg_types1 arg_types2 type_var_heap
619
620
	bindInstances (l1 --> r1) (l2 --> r2) type_var_heap
		= bindInstances r1 r2 (bindInstances l1 l2 type_var_heap)
621
622
623
624
//AA..
	bindInstances (TArrow1 x1) (TArrow1 x2) type_var_heap
		= bindInstances x1 x2 type_var_heap
//..AA
625
	bindInstances (TB _) (TB _) type_var_heap
626
		= type_var_heap
627
628
	bindInstances (TFA _ type1) (TFA _ type2) type_var_heap
		= bindInstances type1 type2 type_var_heap
Sjaak Smetsers's avatar
Sjaak Smetsers committed
629
	bindInstances (CV l1 :@: r1) (CV l2 :@: r2) type_var_heap
630
		= bindInstances r1 r2 (bindInstances (TV l1) (TV l2) type_var_heap)
631

632
instance bindInstances [a] | bindInstances a
633
  where
634
	bindInstances [] [] type_var_heap
635
		= type_var_heap
636
637
	bindInstances [x:xs] [y:ys] type_var_heap
		= bindInstances xs ys (bindInstances x y type_var_heap)
638
	
639
instance bindInstances AType
640
  where
641
642
	bindInstances {at_type=t1} {at_type=t2} type_var_heap
			= bindInstances t1 t2 type_var_heap
643

644
substituteType :: !TypeAttribute !TypeAttribute ![ATypeVar] ![AType] !Type !*TypeHeaps -> (!Type, !*TypeHeaps)
645
646
substituteType form_root_attribute act_root_attribute form_type_args act_type_args orig_type type_heaps
	# type_heaps = bindTypeVarsAndAttributes form_root_attribute act_root_attribute form_type_args act_type_args type_heaps
647
648
	  (expanded_type, type_heaps) = substitute orig_type type_heaps
	= (expanded_type, clearBindingsOfTypeVarsAndAttributes form_root_attribute form_type_args type_heaps)
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675

bindTypeVarsAndAttributes :: !TypeAttribute !TypeAttribute ![ATypeVar] ![AType] !*TypeHeaps -> *TypeHeaps
bindTypeVarsAndAttributes form_root_attribute act_root_attribute form_type_args act_type_args type_heaps
	# th_attrs = bind_attribute form_root_attribute act_root_attribute type_heaps.th_attrs
	= fold2St bind_type_and_attr form_type_args act_type_args { type_heaps & th_attrs = th_attrs }
where
	bind_type_and_attr {atv_attribute, atv_variable={tv_info_ptr}} {at_type,at_attribute} type_heaps=:{th_vars,th_attrs}
		= { type_heaps &	th_vars = th_vars <:= (tv_info_ptr, TVI_Type at_type),
							th_attrs = bind_attribute atv_attribute at_attribute th_attrs }
		
	bind_attribute (TA_Var {av_info_ptr}) attr th_attrs
		= th_attrs <:= (av_info_ptr, AVI_Attr attr)
	bind_attribute _ _ th_attrs
		= th_attrs

clearBindingsOfTypeVarsAndAttributes :: !TypeAttribute ![ATypeVar] !*TypeHeaps -> *TypeHeaps
clearBindingsOfTypeVarsAndAttributes form_root_attribute form_type_args type_heaps
	# th_attrs = clear_attribute form_root_attribute type_heaps.th_attrs
	= foldSt clear_type_and_attr form_type_args { type_heaps & th_attrs = th_attrs }
where
	clear_type_and_attr {atv_attribute, atv_variable={tv_info_ptr}} type_heaps=:{th_vars,th_attrs}
		= { type_heaps & th_vars = th_vars <:= (tv_info_ptr, TVI_Empty), th_attrs = clear_attribute atv_attribute th_attrs }
		
	clear_attribute (TA_Var {av_info_ptr}) th_attrs
		= th_attrs <:= (av_info_ptr, AVI_Empty)
	clear_attribute _ th_attrs
		= th_attrs
676

677
class substitute a :: !a !*TypeHeaps -> (!a, !*TypeHeaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
678
679
680
681

instance substitute AType
where
	substitute atype=:{at_attribute,at_type} heaps
682
683
		# ((at_attribute,at_type), heaps)  = substitute (at_attribute,at_type) heaps
		= ({ atype & at_attribute = at_attribute, at_type = at_type }, heaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
684
685
686

instance substitute TypeAttribute
where
687
	substitute (TA_Var {av_ident, av_info_ptr}) heaps=:{th_attrs}
688
689
		#! av_info = sreadPtr av_info_ptr th_attrs
		= case av_info of
690
			AVI_Attr attr
691
				-> (attr, heaps)
692
			_
693
				-> (TA_Multi, heaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
694
	substitute TA_None heaps
695
		= (TA_Multi, heaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
696
	substitute attr heaps
697
		= (attr, heaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
698
699
700
701

instance substitute (a,b) | substitute a & substitute b
where
	substitute (x,y) heaps
702
703
704
		# (x, heaps) = substitute x heaps
		  (y, heaps) = substitute y heaps
		= ((x,y), heaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
705
706
707
708
	
instance substitute [a] | substitute a
where
	substitute [] heaps
709
		= ( [], heaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
710
	substitute [t:ts] heaps
711
712
713
		# (t, heaps) = substitute t heaps
		  ( ts, heaps) = substitute ts heaps
		= ([t:ts], heaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
714
715
716
717

instance substitute TypeContext
where
	substitute tc=:{tc_types} heaps
718
719
		# (tc_types, heaps) = substitute tc_types heaps
		= ({ tc & tc_types = tc_types }, heaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
720
721
722

instance substitute Type
where
723
724
725
726
727
	substitute tv=:(TV {tv_info_ptr}) heaps=:{th_vars}
		# (tv_info, th_vars) = readPtr tv_info_ptr th_vars
		  heaps = { heaps & th_vars = th_vars }
		= case tv_info of
			TVI_Type type
728
				-> (type, heaps)
729
			_
730
				-> (tv, heaps)
731
	substitute (arg_type --> res_type) heaps
732
733
		# ((arg_type, res_type), heaps) = substitute (arg_type, res_type) heaps
		= (arg_type --> res_type, heaps)
734
	substitute (TArrow1 arg_type) heaps
735
736
		# (arg_type, heaps) = substitute arg_type heaps
		= (TArrow1 arg_type, heaps)
737
	substitute (TA cons_id cons_args) heaps
738
739
		# (cons_args, heaps) = substitute cons_args heaps
		= (TA cons_id cons_args,  heaps)
740
	substitute (TAS cons_id cons_args strictness) heaps
741
742
		# (cons_args, heaps) = substitute cons_args heaps
		= (TAS cons_id cons_args strictness,  heaps)
743
744
745
	substitute (CV type_var :@: types) heaps=:{th_vars}
		# (tv_info, th_vars) = readPtr type_var.tv_info_ptr th_vars
		  heaps = { heaps & th_vars = th_vars }
746
		  (types, heaps) = substitute types heaps
747
		= case tv_info of
748
			TVI_Type type
749
750
751
752
753
754
755
				#  (ok, simplified_type) = simplifyAndCheckTypeApplication type types
				| ok
					-> (simplified_type, heaps)
				// otherwise
					// this will lead to a kind check error later on
					-> 	(CV type_var :@: types, heaps)
			-> 	(CV type_var :@: types, heaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
756
	substitute type heaps
757
		= (type, heaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
758
759
760

instance substitute AttributeVar
where
761
	substitute av=:{av_info_ptr} heaps=:{th_attrs}
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
762
		#! av_info = sreadPtr av_info_ptr th_attrs
763
764
		= case av_info of
			AVI_Attr (TA_Var attr_var)
765
				-> (attr_var, heaps)
766
			_
767
				-> (av, heaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
768
769
770
771

instance substitute AttrInequality
where
	substitute {ai_demanded,ai_offered} heaps
772
773
		# ((ai_demanded, ai_offered), heaps) = substitute (ai_demanded, ai_offered) heaps
		= ({ai_demanded = ai_demanded, ai_offered = ai_offered}, heaps)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
774

775
776
777
instance substitute CaseType
where
	substitute {ct_pattern_type, ct_result_type, ct_cons_types} heaps 
778
779
780
781
		# (ct_pattern_type, heaps) = substitute ct_pattern_type heaps
		  (ct_result_type, heaps) = substitute ct_result_type heaps
		  (ct_cons_types, heaps) = substitute ct_cons_types heaps
		= ({ct_pattern_type = ct_pattern_type, ct_result_type = ct_result_type, 
Martin Wierich's avatar
Martin Wierich committed
782
								ct_cons_types = ct_cons_types}, heaps)
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

class removeAnnotations a :: !a  -> (!Bool, !a)

instance removeAnnotations (a,b) | removeAnnotations a & removeAnnotations b
where
	removeAnnotations t=:(x,y)
		# (rem_x, x) = removeAnnotations x
		  (rem_y, y) = removeAnnotations y
		| rem_x || rem_y
			= (True, (x,y))
			= (False, t)
	
instance removeAnnotations [a] | removeAnnotations a
where
	removeAnnotations l=:[x:xs]
		# (rem_x, x) = removeAnnotations x
		  (rem_xs, xs) = removeAnnotations xs
		| rem_x || rem_xs
			= (True, [x:xs])
			= (False, l)
	removeAnnotations el
		= (False, el)

instance removeAnnotations Type
where
	removeAnnotations t=:(arg_type --> res_type)
		# (rem, (arg_type, res_type)) = removeAnnotations (arg_type, res_type)
		| rem 
			= (True, arg_type --> res_type)
			= (False, t)
813
814
815
816
817
818
819
//AA..
	removeAnnotations t=:(TArrow1 arg_type)
		# (rem, arg_type) = removeAnnotations arg_type
		| rem 
			= (True, TArrow1 arg_type)
			= (False, t)
//..AA			
820
821
822
823
824
	removeAnnotations t=:(TA cons_id cons_args)
		# (rem, cons_args) = removeAnnotations cons_args
		| rem 
			= (True, TA cons_id cons_args)
			= (False, t)
825
826
827
828
829
	removeAnnotations t=:(TAS cons_id cons_args _)
		# (rem, cons_args) = removeAnnotations cons_args
		| rem 
			= (True, TA cons_id cons_args)
			= (False, t)
830
831
832
833
834
835
836
837
838
839
840
	removeAnnotations t=:(cv :@: types)
		# (rem, types) = removeAnnotations types
		| rem 
			= (True, cv :@: types)
			= (False, t)
	removeAnnotations type
		= (False, type)


instance removeAnnotations AType
where
841
	removeAnnotations atype=:{at_type}
842
843
		# (rem, at_type) = removeAnnotations at_type
		| rem
844
			= (True, { atype & at_type = at_type })
845
846
847
848
			= (False, atype)

instance removeAnnotations SymbolType
where
849
	removeAnnotations st=:{st_args,st_result,st_args_strictness}
850
851
		# (rem, (st_args,st_result)) = removeAnnotations (st_args,st_result)
		| rem
852
853
			= (True, { st & st_args = st_args, st_args_strictness=NotStrict, st_result = st_result })
		| is_not_strict st_args_strictness
854
			= (False, st)
855
			= (True, { st & st_args_strictness=NotStrict })
856

857
/*
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
858
859
expandTypeApplication :: ![ATypeVar] !TypeAttribute !Type ![AType] !TypeAttribute !*TypeHeaps -> (!Type, !*TypeHeaps)
expandTypeApplication type_args form_attr type_rhs arg_types act_attr type_heaps=:{th_attrs}
860
	# type_heaps = bindTypeVarsAndAttributes form_attr act_attr type_args arg_types type_heaps 
Martin Wierich's avatar
Martin Wierich committed
861
	  (_, exp_type, type_heaps) = substitute type_rhs type_heaps
862
	= (exp_type, clearBindingsOfTypeVarsAndAttributes form_attr type_args type_heaps)
863
*/
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878

VarIdTable :: {# String}
VarIdTable =: { "a", "b", "c", "d", "e", "f", "g", "h", "i", "j" }

newIdent id_name
	:== { id_name = id_name, id_info = nilPtr }
	
NewVarId var_store
	| var_store < size VarIdTable
		= newIdent VarIdTable.[var_store]
		= newIdent ("v" +++ toString var_store)
 
AttrVarIdTable :: {# String}
AttrVarIdTable =: { "u", "v", "w", "x", "y", "z" }

879
NewAttrVarId :: !Int -> Ident
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
NewAttrVarId attr_var_store
	| attr_var_store < size AttrVarIdTable
 		= newIdent AttrVarIdTable.[attr_var_store]
		= newIdent ("u" +++ toString attr_var_store)

class equiv a :: !a !a !*TypeHeaps -> (!Bool, !*TypeHeaps)

instance equiv AType
where
	equiv atype1 atype2 heaps=:{th_attrs}
		# (ok, th_attrs) = equi_attrs atype1.at_attribute atype2.at_attribute th_attrs
		| ok
			= equiv atype1.at_type atype2.at_type { heaps & th_attrs = th_attrs }
			= (False, { heaps & th_attrs = th_attrs })

	where
		equi_attrs attr=:(TA_Var {av_info_ptr}) (TA_TempVar av_number) attr_var_heap
897
			# (av_info, attr_var_heap) = readPtr av_info_ptr attr_var_heap
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
898
899
900
901
902
			= case av_info of
				AVI_Forward forw_var_number
					-> (forw_var_number == av_number, attr_var_heap)
				_
					-> (True, writePtr av_info_ptr (AVI_Forward av_number) attr_var_heap)
903
904
905
906
		equi_attrs (TA_Var _) (TA_Var _) attr_var_heap
			= (True, attr_var_heap)
		equi_attrs attr1 attr2 attr_var_heap
			= (attr1 == attr2, attr_var_heap)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
907

908
909
910
equivTypeVars :: !TypeVar !TempVarId !*TypeVarHeap -> (!Bool, !*TypeVarHeap)
equivTypeVars {tv_info_ptr} var_number type_var_heap
	# (tv_info, type_var_heap) = readPtr tv_info_ptr type_var_heap
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
911
912
	= case tv_info of
		TVI_Forward forw_var_number
913
			-> (forw_var_number == var_number, type_var_heap)
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
914
		_
915
			-> (True, type_var_heap <:= (tv_info_ptr, TVI_Forward var_number))
Ronny Wichers Schreur's avatar
Ronny Wichers Schreur committed
916
917
918
919
	

instance equiv Type
where
920
921
922
	equiv (TV tv) (TempV var_number) heaps=:{th_vars}
		# (equiv, th_vars) = equivTypeVars tv var_number th_vars
		= (equiv, { heaps & th_vars = th_vars })
923
924
	equiv (TV tv1) (TV tv2) heaps