Initial import

git-svn-id: https://svn.cs.ru.nl/repos/clean-compiler/trunk@2 1f8540f1-abd5-4d5b-9d24-4c5ce8603e2d

1 files changed, 795 insertions, 0 deletions

diff --git a/frontend/unitype.icl b/frontend/unitype.icl
new file mode 100644
index 0000000..dce6a68
--- /dev/null
+++ b/frontend/unitype.icl
@@ -0,0 +1,795 @@
+implementation module unitype
+
+import StdEnv
+
+import syntax, analunitypes, type, utilities
+
+::	CoercionPosition =
+	{	cp_expression	:: !Expression
+	}
+
+AttrUni			:== 0
+AttrMulti		:== 1
+FirstAttrVar	:== 2
+
+::	CoercionTree	= CT_Node !Int !CoercionTree !CoercionTree | CT_Empty | CT_Unique | CT_NonUnique /* | CT_Existential !Int */
+
+::	Coercions		= { coer_demanded :: !.{! .CoercionTree}, coer_offered :: !.{! .CoercionTree }}
+
+::	AttributePartition :== {# Int}
+
+::	PartitioningInfo = 
+	{	pi_marks :: 		!.AttributePartition
+	,	pi_next_num ::		!Int
+	,	pi_groups ::		![[Int]]
+	,	pi_deps ::			![Int]
+	}
+
+uniquenessError :: !CoercionPosition !String !*ErrorAdmin -> *ErrorAdmin
+uniquenessError position mess err=:{ea_file,ea_loc}
+	# ea_file = ea_file <<< "Uniqueness error " <<< hd ea_loc <<< ": \"" <<<  position <<< '\"' <<< mess <<< '\n'
+	= { err & ea_file = ea_file, ea_ok = False}
+
+::	BOOLVECT :== Int
+
+BITINDEX temp_var_id :== temp_var_id >> 5
+BITNUMBER temp_var_id :== temp_var_id bitand 31
+
+isPositive :: !TempVarId !{# BOOLVECT } -> Bool
+isPositive var_id cons_vars
+	= cons_vars.[BITINDEX var_id] bitand (1 << BITNUMBER var_id) <> 0
+
+determineAttributeCoercions :: !AType !AType !Bool !CoercionPosition !u:{! Type} !*Coercions !{# CommonDefs } 
+	!{# BOOLVECT } !*TypeDefInfos !*TypeHeaps !*ErrorAdmin
+		-> (!u:{! Type}, !*Coercions, !*TypeDefInfos, !*TypeHeaps, !*ErrorAdmin) 
+determineAttributeCoercions off_type dem_type coercible position subst coercions defs cons_vars td_infos type_heaps error
+	# (exp_off_type, es) = expandType defs cons_vars off_type (subst, { es_type_heaps = type_heaps, es_td_infos = td_infos})
+	  (exp_dem_type, (subst, {es_td_infos,es_type_heaps})) = expandType defs cons_vars dem_type es
+	  (ok, {crc_type_heaps, crc_coercions, crc_td_infos}) = coerce defs cons_vars exp_off_type exp_dem_type (if coercible PositiveSign TopSign)
+	  		 { crc_type_heaps = es_type_heaps, crc_coercions = coercions, crc_td_infos = es_td_infos}
+	| ok
+		= (subst, crc_coercions, crc_td_infos, crc_type_heaps, error)
+//					---> ("OK", off_type, exp_off_type, dem_type, exp_dem_type)
+		= (subst, crc_coercions, crc_td_infos, crc_type_heaps, uniquenessError position " invalid coercion" error)
+					---> (off_type, exp_off_type, dem_type, exp_dem_type)
+
+NotChecked :== -1	
+DummyAttrNumber :== -1
+::	AttributeGroups	:== {! [Int]}
+
+partitionateAttributes :: !{! CoercionTree} !{! *CoercionTree} -> (!AttributePartition, !{! CoercionTree})
+partitionateAttributes coer_offered coer_demanded
+	#! max_attr_nr = size coer_offered
+	# partitioning_info = { pi_marks = createArray max_attr_nr NotChecked, pi_deps = [], pi_next_num = 0, pi_groups = [] }
+	# {pi_marks,pi_groups} = partitionate_attributes FirstAttrVar max_attr_nr coer_offered partitioning_info
+	  (nr_of_groups, groups) = reverse_and_length pi_groups 0 []
+	  partition = build_partition 0 groups pi_marks
+	# demanded = { CT_Empty \\ i <- [0 .. nr_of_groups - 1] }
+	= (partition, adjust_coercions 0 groups partition coer_offered coer_demanded demanded)
+where
+	visit_attributes :: !CoercionTree !Int !Int !{! CoercionTree} !*PartitioningInfo -> *(!Int, !*PartitioningInfo)
+	visit_attributes (CT_Node attr left right) max_attr_nr min_dep coer_offered pi=:{pi_marks}
+		#! mark = pi_marks.[attr]
+		| mark == NotChecked
+			# (mark, pi) = partitionate_attribute attr max_attr_nr coer_offered pi
+			  (min_dep, pi) = visit_attributes left max_attr_nr (min min_dep mark)  coer_offered pi
+			= visit_attributes right max_attr_nr min_dep coer_offered pi
+		# (min_dep, pi) = visit_attributes left max_attr_nr (min min_dep mark) coer_offered pi
+		= visit_attributes right max_attr_nr min_dep coer_offered pi
+	visit_attributes tree max_attr_nr min_dep coer_offered pi
+		= (min_dep, pi)
+	
+	reverse_and_length :: ![a] !Int ![a] -> (!Int, ![a])
+	reverse_and_length [] length list = (length, list)
+	reverse_and_length [ x : xs ] length list = reverse_and_length xs (inc length) [x : list]
+	
+ 	partitionate_attributes :: !Int !Int !{!CoercionTree} !*PartitioningInfo -> *PartitioningInfo
+	partitionate_attributes from_index max_attr_nr coer_offered pi=:{pi_marks}
+		| from_index == max_attr_nr
+			= pi
+		| pi_marks.[from_index] == NotChecked
+			# (_, pi) = partitionate_attribute from_index max_attr_nr coer_offered pi
+			= partitionate_attributes (inc from_index) max_attr_nr coer_offered pi
+		= partitionate_attributes (inc from_index) max_attr_nr coer_offered pi
+
+	partitionate_attribute :: !Int !Int !{!CoercionTree} !*PartitioningInfo -> *(!Int, !*PartitioningInfo)
+	partitionate_attribute attr max_attr_nr coer_offered=:{ [attr] = off_attributes } pi=:{pi_next_num}
+		# (min_dep, pi) = visit_attributes off_attributes max_attr_nr max_attr_nr coer_offered (push_on_dep_stack attr pi)
+		= try_to_close_group attr pi_next_num min_dep max_attr_nr pi
+	where		
+		push_on_dep_stack attr pi=:{pi_deps,pi_marks,pi_next_num}
+			= { pi & pi_deps = [attr : pi_deps], pi_marks = { pi_marks & [attr] = pi_next_num }, pi_next_num = inc pi_next_num}
+
+		try_to_close_group attr attr_nr min_dep max_attr_nr pi=:{pi_marks, pi_deps, pi_groups}
+			| attr_nr <= min_dep
+				# (pi_deps, pi_marks, group) = close_group attr pi_deps pi_marks [] max_attr_nr
+				= (max_attr_nr, { pi & pi_deps = pi_deps, pi_marks = pi_marks, pi_groups = [group : pi_groups] })
+				= (min_dep, pi)
+		where
+			close_group attr [d:ds] marks group max_attr_nr
+				# marks = { marks & [d] = max_attr_nr }
+				| d == attr
+					= (ds, marks, [d : group])
+					= close_group attr ds marks [d : group] max_attr_nr
+
+	build_partition group_nr [] partition
+		= partition
+	build_partition group_nr [group : groups] partition
+		= build_partition (inc group_nr) groups (build_partition_of_group group_nr group partition)
+	where
+		build_partition_of_group group_nr [attr : attrs] partition
+			= build_partition_of_group group_nr attrs { partition & [attr] = group_nr }
+		build_partition_of_group group_nr [] partition
+			= partition
+
+	adjust_coercions group_index [group : groups] partition coer_offered coer_demanded demanded
+		# (combined_tree, coer_demanded) = combine_coercion_trees group_index group partition CT_Empty coer_offered coer_demanded
+		= adjust_coercions (inc group_index) groups partition coer_offered coer_demanded { demanded & [ group_index ] = combined_tree }
+	adjust_coercions group_index [] partition coer_offered coer_demanded demanded
+		= demanded
+
+	combine_coercion_trees group_index [ attr : attrs ] partition merged_tree coer_offered coer_demanded
+		| isNonUnique coer_offered.[attr]
+			= (CT_NonUnique, coer_demanded)
+/*		| isExistential coer_offered.[attr]
+			= (CT_Existential DummyAttrNumber, coer_demanded)
+*/		# (next_tree, coer_demanded) = replace coer_demanded attr CT_Empty
+		| isUnique next_tree
+			= (CT_Unique, coer_demanded)
+			# merged_tree = rebuild_tree group_index partition next_tree merged_tree
+			= combine_coercion_trees group_index attrs partition merged_tree coer_offered coer_demanded
+	combine_coercion_trees group_index [ ] partition merged_tree coer_offered coer_demanded
+		= (merged_tree, coer_demanded)
+		
+
+	rebuild_tree :: !Index !AttributePartition !*CoercionTree !*CoercionTree -> *CoercionTree
+	rebuild_tree group_index partition (CT_Node attr left right) tree
+		# tree = rebuild_tree group_index partition left tree
+		  tree = rebuild_tree group_index partition right tree
+		#! attr_nr = partition.[attr]
+		| attr_nr == group_index
+			= tree
+		# { tree } = insert partition.[attr] tree
+		= tree	
+	where
+		insert ::  !Int !*CoercionTree -> *CoercionTreeRecord
+		insert new_attr CT_Empty
+			=  { tree = CT_Node new_attr CT_Empty CT_Empty }
+		insert new_attr (CT_Node this_attr ct_less ct_greater)
+			| new_attr < this_attr
+				# { tree } = insert new_attr ct_less
+				= { tree = CT_Node this_attr tree ct_greater }
+			| new_attr > this_attr
+				# { tree } = insert new_attr ct_greater
+				= { tree = CT_Node this_attr ct_less tree }
+				= { tree = CT_Node this_attr ct_less ct_greater }
+	rebuild_tree group_index partition empty_tree tree
+		= tree
+
+::	CoercionTreeRecord = { tree :: !.CoercionTree }
+
+
+liftSubstitution :: !*{! Type} !{# CommonDefs } !Int !*TypeVarHeap !*TypeDefInfos -> (*{! Type}, !Int, !*TypeVarHeap, !*TypeDefInfos)
+liftSubstitution subst modules attr_store type_var_heap td_infos 
+	# ls = { ls_next_attr = attr_store, ls_td_infos = td_infos, ls_type_var_heap = type_var_heap}
+	= lift_substitution 0 modules subst ls
+where
+	lift_substitution var_index modules subst ls
+		| var_index < size subst
+			#! type = subst.[var_index]
+			# (type, _, _, subst, ls) = lift modules type subst ls
+			= lift_substitution (inc var_index) modules { subst & [var_index] = type } ls
+			= (subst, ls.ls_next_attr, ls.ls_type_var_heap, ls.ls_td_infos)
+
+adjustSignClass :: !SignClassification !Int -> SignClassification
+adjustSignClass {sc_pos_vect,sc_neg_vect} arity
+	= { sc_pos_vect = sc_pos_vect >> arity, sc_neg_vect = sc_neg_vect >> arity }
+
+// adjustPropClass :: !PropClassification !Int -> PropClassification
+adjustPropClass prop_class arity :== prop_class >> arity
+
+::	LiftState = 
+	{	ls_next_attr		:: !Int
+	,	ls_type_var_heap	:: !.TypeVarHeap
+	,	ls_td_infos			:: !.TypeDefInfos
+	}
+
+
+liftTempTypeVariable :: !{# CommonDefs } !TempVarId !*{! Type} !*LiftState
+	-> (!Type, !SignClassification, !PropClassification, !*{! Type}, !*LiftState)
+liftTempTypeVariable modules tv_number subst ls
+	#! type = subst.[tv_number]
+	= case type of
+		TE	-> (TempV tv_number, TopSignClass, PropClass, subst, ls)
+		_	-> lift modules type subst ls
+
+class lift a :: !{# CommonDefs } !a !*{! Type} !*LiftState
+	-> (!a, !SignClassification, !PropClassification, !*{! Type}, !*LiftState)
+
+
+instance lift Type
+where
+	lift modules (TempV tv_number) subst ls
+		= liftTempTypeVariable modules tv_number subst ls
+	lift modules (arg_type --> res_type) subst ls
+		# (arg_type, _, _, subst, ls) = lift modules arg_type subst ls
+		  (res_type, _, _, subst, ls) = lift modules res_type subst ls
+		= (arg_type --> res_type, BottomSignClass, NoPropClass, subst, ls)
+	lift modules (TA cons_id=:{type_index={glob_object,glob_module},type_arity} cons_args) subst ls
+		# (cons_args, sign_classes, prop_classes, subst, ls) = lift_list modules cons_args subst ls
+		  (type_prop, ls_type_var_heap, ls_td_infos) = typeProperties glob_object glob_module sign_classes prop_classes modules ls.ls_type_var_heap ls.ls_td_infos
+		= (TA  { cons_id & type_prop = type_prop } cons_args,
+					adjustSignClass type_prop.tsp_sign type_arity, adjustPropClass type_prop.tsp_propagation type_arity,
+			subst, { ls & ls_td_infos = ls_td_infos, ls_type_var_heap = ls_type_var_heap})
+	lift modules (TempCV temp_var :@: types) subst ls
+		# (type, sign_class, prop_class, subst, ls) = liftTempTypeVariable modules temp_var subst ls
+		  (types, _, _, subst, ls) = lift_list modules types subst ls
+		= case type of
+			TA type_cons cons_args
+				# nr_of_new_args = length types
+				-> (TA { type_cons & type_arity = type_cons.type_arity + nr_of_new_args } (cons_args ++ types),
+						adjustSignClass sign_class nr_of_new_args, adjustPropClass prop_class nr_of_new_args, subst, ls)
+			TempV tv_number
+				-> (TempCV tv_number :@: types, TopSignClass, PropClass, subst, ls)
+			cons_var :@: cv_types
+				-> (cons_var :@: (cv_types ++ types), TopSignClass, PropClass, subst, ls)
+	lift modules type subst ls
+		= (type, BottomSignClass, NoPropClass,  subst, ls)
+	
+instance lift AType
+where
+	lift modules attr_type=:{at_attribute,at_type} subst ls
+		# (at_type, sign_class, prop_class, subst, ls) = lift modules at_type subst ls
+		| type_is_non_coercible at_type
+			= ({attr_type & at_type = at_type}, sign_class, prop_class, subst, ls)
+			= ({attr_type & at_attribute = TA_TempVar ls.ls_next_attr, at_type = at_type},
+					sign_class, prop_class, subst, {ls & ls_next_attr = inc ls.ls_next_attr})
+	where
+		type_is_non_coercible (TempV _)
+			= True
+		type_is_non_coercible (TempQV _)
+			= True
+		type_is_non_coercible (_ --> _)
+			= True
+		type_is_non_coercible (_ :@: _)
+			= True
+		type_is_non_coercible _
+			= False
+
+
+lift_list :: !{#CommonDefs} ![a] !*{!Type} !*LiftState
+	-> (![a], ![SignClassification], ![PropClassification], !*{!Type}, !*LiftState) | lift a
+lift_list modules [] subst ls
+	= ([], [], [], subst, ls)
+lift_list modules [t:ts] subst ls
+	# (t, sign_class, prop_class, subst, ls) = lift modules t subst ls
+	  (ts, sign_classes, prop_classes, subst, ls) = lift_list modules ts subst ls
+	= ([t:ts], [sign_class : sign_classes], [prop_class : prop_classes], subst, ls)
+
+::	ExpansionState = 
+	{	es_type_heaps	:: !.TypeHeaps
+	,	es_td_infos		:: !.TypeDefInfos
+	}
+
+class expandType a :: !{# CommonDefs } !{# BOOLVECT } !a !*(!u:{! Type}, !*ExpansionState) -> (!a, !*(!u:{! Type}, !*ExpansionState))
+
+instance expandType AType
+where
+	expandType modules cons_vars attr_type=:{at_type, at_attribute} (subst, es=:{es_type_heaps})
+		# (at_attribute, th_attrs) = expand_attribute at_attribute es_type_heaps.th_attrs
+		  (at_type, subst_and_es) = expandType modules cons_vars at_type (subst, {es & es_type_heaps = { es_type_heaps & th_attrs = th_attrs }})
+		= ({ attr_type & at_type = at_type, at_attribute = at_attribute }, subst_and_es)
+	where
+		expand_attribute (TA_Var {av_info_ptr}) attr_var_heap
+			# (AVI_Attr attr, attr_var_heap) = readPtr av_info_ptr attr_var_heap
+			= (attr, attr_var_heap)
+		expand_attribute attr attr_var_heap
+			= (attr, attr_var_heap)
+	
+expandTempTypeVariable :: !TempVarId !*(!u:{! Type}, !*ExpansionState) -> (!Type, !*(!u:{! Type}, !*ExpansionState))
+expandTempTypeVariable tv_number (subst, es)
+	#! type = subst.[tv_number]
+	= case type of
+		TE	-> (TempV tv_number, (subst, es))
+		_	-> (type, (subst, es))
+
+instance expandType Type
+where
+	expandType modules cons_vars (TempV tv_number) es
+		= expandTempTypeVariable tv_number es
+	expandType modules cons_vars (TV {tv_info_ptr}) (subst, es=:{es_type_heaps})
+		# (TVI_Type type, th_vars) = readPtr tv_info_ptr es_type_heaps.th_vars
+		= (type, (subst, {es & es_type_heaps = { es_type_heaps & th_vars = th_vars }}))
+	expandType modules cons_vars (arg_type --> res_type) es
+		# (arg_type, es) = expandType modules cons_vars arg_type es
+		  (res_type, es) = expandType modules cons_vars res_type es
+		= (arg_type --> res_type, es)
+	expandType modules cons_vars (TA cons_id=:{type_index={glob_object,glob_module}} cons_args) es
+		# (cons_args, sign_classes, prop_classes, (subst,es=:{es_td_infos,es_type_heaps})) = expand_type_list modules cons_vars cons_args es
+		  (type_prop, th_vars, es_td_infos)
+		  			= typeProperties glob_object glob_module sign_classes prop_classes modules es_type_heaps.th_vars es_td_infos
+		= (TA { cons_id & type_prop = type_prop } cons_args,
+				(subst, { es & es_td_infos = es_td_infos, es_type_heaps = { es_type_heaps & th_vars = th_vars }}))
+	where
+		expand_type_list ::  !{#CommonDefs} !{# BOOLVECT } ![AType] !*(!u:{!Type}, !*ExpansionState)
+			-> (![AType], ![SignClassification], ![PropClassification], !*(!u:{!Type}, !*ExpansionState))
+		expand_type_list modules cons_vars [] es
+			= ([], [], [], es)
+		expand_type_list modules cons_vars [t:ts]  es
+			# (t, es) = expandType modules cons_vars t es
+			  (ts, sign_classes, prop_classes, es) = expand_type_list modules cons_vars ts es
+			= case t.at_type of 
+				TA {type_arity,type_prop} _
+					-> ([t:ts], [adjustSignClass type_prop.tsp_sign type_arity : sign_classes],
+								[adjustPropClass type_prop.tsp_propagation type_arity : prop_classes], es)
+				TempV tmp_var_id
+					| isPositive tmp_var_id cons_vars
+						-> ([t:ts], [PosSignClass : sign_classes], [PropClass : prop_classes], es)
+						-> ([t:ts], [TopSignClass : sign_classes], [NoPropClass : prop_classes], es)
+				_
+					-> ([t:ts], [TopSignClass : sign_classes], [PropClass : prop_classes], es)
+					
+	expandType modules cons_vars (TempCV temp_var :@: types) es
+		# (type, es) = expandTempTypeVariable temp_var es
+		  (types, es) = expandType modules cons_vars types es
+		= case type of
+			TA type_cons=:{type_arity} cons_args
+				# nr_of_new_args = length types
+				-> (TA { type_cons & type_arity = type_arity + nr_of_new_args } (cons_args ++ types), es)
+			TempV tv_number
+				-> (TempCV tv_number :@: types, es)
+			cons_var :@: cv_types
+				-> (cons_var :@: (cv_types ++ types), es)
+	expandType modules cons_vars type es
+		= (type, es)
+
+instance expandType [a] | expandType a
+where
+	expandType modules cons_vars l es = mapSt (expandType modules cons_vars) l es
+	
+instance toInt TypeAttribute
+where
+	 toInt TA_Unique 				= AttrUni
+	 toInt (TA_TempVar av_number)	= av_number
+//	 toInt (TA_TempExVar av_number)	= av_number
+	 toInt TA_Multi 				= AttrMulti
+	 toInt TA_None 					= AttrMulti
+
+
+instance * Bool
+where
+	(*) b1 b2 = b1 && b2 || not b1 && not b2
+
+instance * Sign
+where
+	(*) sign1 sign2
+		= {	pos_sign = sign1.pos_sign * sign2.pos_sign || sign1.neg_sign * sign2.neg_sign,
+			neg_sign = sign1.pos_sign * sign2.neg_sign || sign1.neg_sign * sign2.pos_sign }
+		
+::	CoercionState =
+	{	crc_type_heaps	:: !.TypeHeaps
+	,	crc_coercions	:: !.Coercions
+	,	crc_td_infos	:: !.TypeDefInfos
+	}
+
+
+class coerce a :: !{# CommonDefs} !{# BOOLVECT} !a !a !Sign !*CoercionState -> (!Bool, !*CoercionState)
+
+/*
+
+'coerceAttributes offered_attribute offered_attribute sign coercions' coerce offered_attribute to
+offered_attribute according to sign. Failure is indicated by returning False as a result.
+
+*/
+
+coerceAttributes TA_Unique dem_attr {neg_sign} coercions
+	| not neg_sign
+		= (True, coercions)
+coerceAttributes off_attr TA_Unique {pos_sign} coercions
+	| not pos_sign
+		= (True, coercions)
+coerceAttributes (TA_TempVar av_number) dem_attr {neg_sign} coercions=:{coer_demanded}
+	| not neg_sign && isUnique coer_demanded.[av_number]
+		= (True, coercions)
+coerceAttributes off_attr (TA_TempVar av_number) {pos_sign} coercions=:{coer_demanded}
+	| not pos_sign && isUnique coer_demanded.[av_number]
+		= (True, coercions)
+/*
+coerceAttributes off_attr TA_Multi {neg_sign} coercions
+	| not neg_sign
+		= (True, coercions)
+coerceAttributes TA_Multi dem_attr {pos_sign} coercions
+	| not pos_sign
+		= (True, coercions)
+*/
+coerceAttributes (TA_TempVar av_number1) (TA_TempVar av_number2) {pos_sign,neg_sign} coercions
+	| av_number1 == av_number2
+		= (True, coercions)
+	| pos_sign
+		| neg_sign
+			# (ok, coercions) = new_inequality av_number1 av_number2 coercions
+			| ok
+				= new_inequality av_number2 av_number1 coercions
+				= (False, coercions)
+			= new_inequality av_number1 av_number2 coercions
+	| neg_sign
+		= new_inequality av_number2 av_number1 coercions
+		= (True, coercions)
+where
+	new_inequality :: !Int !Int !*Coercions  -> (!Bool, !*Coercions)
+	new_inequality off_attr dem_attr coercions=:{coer_demanded, coer_offered}
+/*		| isExistential coer_offered.[off_attr]
+			#! off_attr_tree = coer_offered.[off_attr]
+			= coerce_to_existential_attribute off_attr_tree dem_attr coercions
+		| isExistential coer_demanded.[dem_attr]
+			#! dem_attr_tree = coer_demanded.[off_attr]
+			= coerce_to_existential_attribute dem_attr_tree off_attr coercions
+*/		| isNonUnique coer_offered.[off_attr]
+			| isUnique coer_demanded.[dem_attr]
+				= (False, coercions)
+				= (True, makeNonUnique dem_attr coercions)
+		| isUnique coer_demanded.[dem_attr]
+			= (True, makeUnique off_attr coercions)
+		| isNonUnique coer_offered.[dem_attr] || isUnique coer_demanded.[off_attr]
+			= (True, coercions)
+			= (True, newInequality off_attr dem_attr coercions)
+/*	
+	coerce_to_existential_attribute (CT_Existential exi_number) attr_number coercions
+		= coerceToExistentialAttribute exi_number attr_number coercions
+*/
+					
+coerceAttributes TA_Unique (TA_TempVar av_number) {neg_sign} coercions=:{coer_offered}
+	| isNonUnique coer_offered.[av_number]
+		= (False, coercions)
+		= (True, makeUnique av_number coercions)// ---> "*** 1 ***"
+coerceAttributes (TA_TempVar av_number) TA_Unique {pos_sign} coercions=:{coer_offered}
+	| isNonUnique coer_offered.[av_number]
+		= (False, coercions)
+		= (True, makeUnique av_number coercions)// ---> "*** 2 ***"
+coerceAttributes TA_Multi (TA_TempVar av_number) {pos_sign} coercions=:{coer_demanded}
+	| pos_sign
+		| isUnique coer_demanded.[av_number]
+			= (False, coercions)
+			= (True, makeNonUnique av_number coercions)
+		= (True, coercions)
+coerceAttributes (TA_TempVar av_number) TA_Multi {neg_sign} coercions=:{coer_demanded}
+	| neg_sign
+		| isUnique coer_demanded.[av_number]
+			= (False, coercions)
+			= (True, makeNonUnique av_number coercions)
+		= (True, coercions)
+coerceAttributes TA_Unique TA_Multi _ coercions
+	= (False, coercions)
+coerceAttributes off_attr dem_attr {pos_sign,neg_sign} coercions
+/*
+	| pos_sign || neg_sign // ---> ("coerceAttributes", off_attr, dem_attr)
+		= case off_attr of
+			TA_TempExVar eav_number
+				-> case dem_attr of
+					TA_TempVar av_number
+						-> coerceToExistentialAttribute eav_number av_number coercions
+					TA_TempExVar eav_number2
+						-> (eav_number == eav_number2, coercions)
+					_
+						-> (False, coercions)
+				
+			TA_TempVar av_number
+				-> case dem_attr of
+					TA_TempExVar eav_number
+						-> coerceToExistentialAttribute eav_number av_number coercions
+					_
+						-> (True, coercions)
+			_
+				-> case dem_attr of
+					TA_TempExVar eav_number
+						-> (False, coercions)
+					_
+						-> (True, coercions)
+*/
+		= (True, coercions)
+
+/*
+coerceToExistentialAttribute exi_attr_number attr_number coercions=:{coer_demanded, coer_offered}
+	#! dem_attr_tree = coer_demanded.[attr_number]
+	   off_attr_tree = coer_offered.[attr_number]
+	= case dem_attr_tree ---> ("coerceToExistentialAttribute", exi_attr_number, attr_number, dem_attr_tree, off_attr_tree) of
+		CT_Unique
+			-> (False, coercions)
+		CT_Existential exi_attr_number2
+			-> (exi_attr_number == exi_attr_number2, coercions)
+		_
+			-> case off_attr_tree of
+				CT_NonUnique
+					-> (False, coercions)
+				_
+					-> (True, make_attr_existential attr_number exi_attr_number coercions)
+	
+where
+	make_attr_existential :: !Int  !Int !*Coercions -> *Coercions
+	make_attr_existential attr exi_attr {coer_demanded, coer_offered}
+		# (dem_heaps_and_coercions, coer_demanded) = replace coer_demanded attr (CT_Existential exi_attr)
+		  (off_heaps_and_coercions, coer_offered) = replace coer_offered attr (CT_Existential exi_attr)
+		= make_existential off_heaps_and_coercions exi_attr (
+			make_existential dem_heaps_and_coercions exi_attr {coer_offered = coer_offered, coer_demanded = coer_demanded})
+
+	make_existential (CT_Node this_attr ct_less ct_greater) exi_attr coercions
+		# coercions = make_attr_existential this_attr exi_attr coercions
+		  coercions = make_existential ct_less exi_attr coercions
+		  coercions = make_existential ct_greater exi_attr coercions
+		= coercions
+	make_existential tree exi_attr coercions
+		= coercions
+*/
+newInequality :: !Int !Int !*Coercions -> *Coercions 
+newInequality off_attr dem_attr coercions=:{coer_demanded, coer_offered}
+	# (dem_coercions, coer_demanded) = replace coer_demanded off_attr CT_Empty
+	  (succ, dem_coercions) = insert dem_attr dem_coercions
+	  coer_demanded = { coer_demanded & [off_attr] = dem_coercions }
+	| succ
+		# (off_coercions, coer_offered) = replace coer_offered dem_attr CT_Empty
+	  	  (succ, off_coercions) = insert off_attr off_coercions
+	 	  coer_offered = { coer_offered & [dem_attr] = off_coercions }
+		= {coer_demanded = coer_demanded, coer_offered = coer_offered}
+		= {coer_demanded = coer_demanded, coer_offered = coer_offered}
+where
+
+	insert ::  !Int !*CoercionTree -> (!Bool, !*CoercionTree)
+	insert new_attr CT_Empty
+		=  (True, CT_Node new_attr CT_Empty CT_Empty)
+	insert new_attr (CT_Node this_attr ct_less ct_greater)
+		| new_attr < this_attr
+			# (succ, ct_less) = insert new_attr ct_less
+			= (succ, CT_Node this_attr ct_less ct_greater)
+		| new_attr > this_attr
+			# (succ, ct_greater) = insert new_attr ct_greater
+			= (succ, CT_Node this_attr ct_less ct_greater)
+			= (False, CT_Node this_attr ct_less ct_greater)
+	
+isNonUnique :: !CoercionTree -> Bool
+isNonUnique CT_NonUnique	= True
+isNonUnique _ 				= False
+
+isUnique  :: !CoercionTree -> Bool
+isUnique CT_Unique			= True
+isUnique _					= False
+
+/*
+isExistential  :: !CoercionTree -> Bool
+isExistential (CT_Existential exi_number)	= True
+isExistential attr_tree						= False
+*/
+		
+makeUnique :: !Int !*Coercions -> *Coercions
+makeUnique attr {coer_demanded, coer_offered}
+	# (off_coercions, coer_offered) = replace coer_offered attr CT_Empty
+	  coer_demanded = { coer_demanded & [attr] = CT_Unique }
+	= make_unique off_coercions {coer_offered = coer_offered, coer_demanded = coer_demanded}// ---> ("makeUnique :", attr)
+where
+	make_unique (CT_Node this_attr ct_less ct_greater) coercions
+		# coercions = makeUnique this_attr coercions
+		  coercions = make_unique ct_less coercions
+		  coercions = make_unique ct_greater coercions
+		= coercions
+	make_unique tree coercions
+		= coercions
+
+tryToMakeUnique :: !Int !*Coercions -> (!Bool, !*Coercions)
+tryToMakeUnique attr coercions=:{coer_offered}
+	| isNonUnique coer_offered.[attr] // || isExistential coer_offered.[attr]
+		= (False, coercions)
+		= (True, makeUnique attr coercions)
+
+makeNonUnique :: !Int !*Coercions -> *Coercions
+makeNonUnique attr {coer_demanded, coer_offered}
+	# (dem_coercions, coer_demanded) = replace coer_demanded attr CT_Empty
+	  coer_offered = { coer_offered & [attr] = CT_NonUnique }
+	= make_non_unique dem_coercions {coer_offered = coer_offered, coer_demanded = coer_demanded}
+where
+	make_non_unique (CT_Node this_attr ct_less ct_greater) coercions
+		# coercions = makeNonUnique this_attr coercions
+		  coercions = make_non_unique ct_less coercions
+		  coercions = make_non_unique ct_greater coercions
+		= coercions
+	make_non_unique tree coercions
+		= coercions
+
+tryToMakeNonUnique :: !Int !*Coercions -> (!Bool, !*Coercions)
+tryToMakeNonUnique attr coercions=:{coer_demanded}
+	| isUnique coer_demanded.[attr] // || isExistential coer_demanded.[attr]
+		= (False, coercions)
+		= (True, makeNonUnique attr coercions)
+//				---> ("tryToMakeNonUnique", attr)
+
+instance coerce AType
+where
+	coerce defs cons_vars at1=:{at_attribute=attr1,at_type=type1} at2=:{at_attribute=attr2,at_type=type2} sign cs=:{crc_coercions}
+		# sign = adjust_sign sign type1 cons_vars
+		  (succ, crc_coercions) = coerceAttributes attr1 attr2 sign crc_coercions
+		| succ
+			# (succ, cs) = coerce defs cons_vars type1 type2 sign { cs & crc_coercions = crc_coercions }
+			| succ
+				# (succ1, crc_coercions) = add_propagation_inequalities attr1 type1 cs.crc_coercions
+				  (succ2, crc_coercions) = add_propagation_inequalities attr2 type2 crc_coercions
+				= (succ1 && succ2, { cs & crc_coercions = crc_coercions })
+				= (False, cs)
+			= (False, { cs & crc_coercions = crc_coercions })
+				// ---> ("coerceAttributes", attr1, attr2, sign)
+
+	where		
+
+		adjust_sign :: !Sign !Type {# BOOLVECT} -> Sign
+		adjust_sign sign (TempV _) cons_vars
+			= TopSign
+		adjust_sign sign (TempQV _) cons_vars
+			= TopSign
+		adjust_sign sign (_ --> _) cons_vars
+			= TopSign
+		adjust_sign sign (TempCV tmp_var_id :@: _) cons_vars
+			| isPositive tmp_var_id cons_vars
+				= sign
+				= TopSign
+		adjust_sign sign (_ :@: _) cons_vars
+			= TopSign
+		adjust_sign sign (TA {type_name, type_prop={tsp_coercible}} _) cons_vars
+			| tsp_coercible
+				= sign
+				= TopSign
+//					---> ("adjust_sign to top", type_name)
+		adjust_sign sign _ cons_vars
+			= sign
+
+		add_propagation_inequalities attr (TA {type_prop={tsp_propagation}} cons_args) coercions
+			= add_inequalities tsp_propagation attr cons_args coercions
+		where
+			add_inequalities prop_class attr _ coercions
+				= (True, coercions)
+
+			add_inequalities prop_class attr [] coercions
+				= (True, coercions)
+			add_inequalities prop_class attr [{at_attribute} : args] coercions
+				| (prop_class bitand 1) == 0 //  || is_existential_attribute at_attribute coercions
+					= add_inequalities (prop_class >> 1) attr args coercions
+				# (succ, coercions) = coerceAttributes attr at_attribute PositiveSign coercions
+				| succ
+					= add_inequalities (prop_class >> 1) attr args coercions
+					= (False, coercions)
+							---> ("add_propagation_inequalities", attr, at_attribute)
+/*
+			is_existential_attribute (TA_TempExVar eav_number) coercions
+				= True
+			is_existential_attribute (TA_TempVar eav_number) {coer_offered}
+				= isExistential coer_offered.[eav_number]
+			is_existential_attribute _ {coer_offered}
+				= False
+*/ 
+		add_propagation_inequalities attr type coercions
+			= (True, coercions)
+	
+coercionsOfTypeList defs cons_vars [t1 : ts1] [t2 : ts2] sign_class type_index sign cs
+	# arg_sign = sign * signClassToSign sign_class type_index
+	  (ok, cs) = coerce defs cons_vars t1 t2 arg_sign cs
+	| ok
+		= coercionsOfTypeList defs cons_vars ts1 ts2 sign_class (inc type_index) sign cs
+		= (False, cs)
+coercionsOfTypeList defs cons_vars [] [] _ _ _ cs
+	= (True, cs)
+
+isSynonymType (SynType _)
+	= True
+isSynonymType type_rhs
+	= False
+	
+tryToExpandTypeSyn defs cons_vars cons_id=:{type_index={glob_object,glob_module}} type_args type_heaps td_infos
+	# {td_rhs,td_args} = defs.[glob_module].com_type_defs.[glob_object]
+	| isSynonymType td_rhs
+		# (SynType {at_type}) = td_rhs
+		  type_heaps = fold2St bind_type_and_attr td_args type_args type_heaps
+		  (expanded_type, (_, {es_type_heaps, es_td_infos}))
+		  		= expandType defs cons_vars at_type ({}, { es_type_heaps = type_heaps, es_td_infos = td_infos })
+		= (True, expanded_type, es_type_heaps, es_td_infos)
+		= (False, TA cons_id type_args, type_heaps, td_infos)
+where
+	bind_type_and_attr {atv_attribute = TA_Var {av_info_ptr}, atv_variable={tv_info_ptr}} {at_attribute,at_type} {th_vars,th_attrs}
+		= { th_vars = th_vars <:= (tv_info_ptr, TVI_Type at_type), th_attrs = th_attrs <:= (av_info_ptr, AVI_Attr at_attribute) }
+	bind_type_and_attr {atv_variable={tv_info_ptr}} {at_type} type_heaps=:{th_vars}
+		= { type_heaps & th_vars = th_vars <:= (tv_info_ptr, TVI_Type at_type) }
+	
+	
+instance coerce Type
+where
+	coerce defs cons_vars (TA dem_cons dem_args) (TA off_cons off_args) sign cs=:{crc_type_heaps, crc_td_infos}
+		| dem_cons == off_cons
+			= coercionsOfTypeList defs cons_vars dem_args off_args dem_cons.type_prop.tsp_sign 0 sign cs
+			# (_, dem_type, crc_type_heaps, crc_td_infos) = tryToExpandTypeSyn defs cons_vars dem_cons dem_args crc_type_heaps crc_td_infos
+			  (_, off_type, crc_type_heaps, crc_td_infos) = tryToExpandTypeSyn defs cons_vars off_cons off_args crc_type_heaps crc_td_infos
+			= coerce defs cons_vars dem_type off_type sign { cs & crc_type_heaps = crc_type_heaps, crc_td_infos = crc_td_infos }
+	coerce defs cons_vars (TA dem_cons dem_args) off_type sign cs=:{crc_type_heaps, crc_td_infos}
+		# (succ, dem_type, crc_type_heaps, crc_td_infos) = tryToExpandTypeSyn defs cons_vars dem_cons dem_args crc_type_heaps crc_td_infos
+		| succ
+			= coerce defs cons_vars dem_type off_type sign { cs & crc_type_heaps = crc_type_heaps, crc_td_infos = crc_td_infos }
+			= (True, { cs & crc_type_heaps = crc_type_heaps, crc_td_infos = crc_td_infos })
+	coerce defs cons_vars dem_type (TA off_cons off_args) sign cs=:{crc_type_heaps, crc_td_infos}
+		# (succ, off_type, crc_type_heaps, crc_td_infos) = tryToExpandTypeSyn defs cons_vars off_cons off_args crc_type_heaps crc_td_infos
+		| succ
+			= coerce defs cons_vars dem_type off_type sign { cs & crc_type_heaps = crc_type_heaps, crc_td_infos = crc_td_infos }
+			= (True, { cs & crc_type_heaps = crc_type_heaps, crc_td_infos = crc_td_infos })
+	coerce defs cons_vars (arg_type1 --> res_type1) (arg_type2 --> res_type2) sign cs
+		# (ok, cs) = coerce defs cons_vars arg_type1 arg_type2 (NegativeSign * sign) cs
+		| ok
+			= coerce defs cons_vars res_type1 res_type2 sign cs
+			= (False, cs)
+	coerce defs cons_vars (cons_var :@: types1) (_ :@: types2) sign cs
+		= coercions_of_type_list defs cons_vars (determine_sign_of_arg_types cons_var cons_vars) types1 types2 cs
+	where
+		determine_sign_of_arg_types (TempCV tmp_var_id) cons_vars
+			| isPositive tmp_var_id cons_vars
+				= PositiveSign
+				= TopSign
+		determine_sign_of_arg_types _ cons_vars
+				= TopSign
+			
+		coercions_of_type_list :: !{# CommonDefs} !{# BOOLVECT} !Sign ![a] ![a] !*CoercionState -> (!Bool,!*CoercionState) | coerce a
+		coercions_of_type_list defs cons_vars sign [t1 : ts1] [t2 : ts2] cs
+			# (ok, cs) = coerce defs cons_vars t1 t2 sign cs
+			| ok
+				= coercions_of_type_list defs cons_vars sign ts1 ts2 cs
+				= (False, cs)
+		coercions_of_type_list defs cons_vars sign [] [] cs
+			= (True, cs)
+	coerce defs cons_vars _ _ sign cs
+		= (True, cs)
+
+AttrRestricted :== 0
+
+instance <<< CoercionTree
+where
+	(<<<) file (CT_Node attr left right) = file <<< left <<< ' ' <<< attr <<< ' ' <<< right
+	(<<<) file CT_Unique = file <<< "CT_Unique"
+	(<<<) file CT_NonUnique = file <<< "CT_NonUnique"
+//	(<<<) file (CT_Existential int) = file <<< "CT_Existential:" <<< int
+	(<<<) file CT_Empty = file <<< "##"
+
+instance <<< CoercionPosition
+where
+	(<<<) file {cp_expression} = show_expression file cp_expression
+
+	where
+		show_expression file (Var {var_name})
+			= file <<< var_name
+		show_expression file (FreeVar {fv_name})
+			= file <<< fv_name
+		show_expression file (App {app_symb={symb_name}})
+			= file <<< symb_name
+		show_expression file (fun @ fun_args)
+			= show_expression file fun
+		show_expression file (Case {case_ident})
+			= case case_ident of
+				Yes {id_name}
+					# (line, pos) = get_line_and_col "_c" id_name
+					-> file <<< "case [" <<< line <<< ',' <<< pos <<< ']'
+				No
+					-> file <<< "(case ... )"
+		show_expression file (Selection _ expr selectors)
+			= file <<< "selection"
+		show_expression file (Update expr1 selectors expr2)
+			= file <<< "update"
+		show_expression file (TupleSelect {ds_arity} elem_nr expr)
+			= file <<< "argument" <<< (elem_nr + 1) <<< " of " <<< ds_arity <<< "-tuple"
+		show_expression file (BasicExpr bv _)
+			= file <<< bv
+		show_expression file (MatchExpr _ _ expr)
+			= file <<< "match expression"
+		show_expression file _
+			= file
+
+		
+		get_line_and_col prefix ident
+			# ident = ident % (0, size prefix - 1)
+			  del_pos = find_delimiter '_' 0 ident
+			= (toInt (ident % (0, del_pos - 1)), toInt (ident % (del_pos + 1, size ident - 1)))
+		where
+			find_delimiter del_char del_pos ident
+				| del_char == ident.[del_pos]
+					= del_pos
+					= find_delimiter del_char (inc del_pos) ident
+