bug fix: Improved unification algoritm for kinds

Universally quantified types (parsing and inference)


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

7 files changed, 106 insertions, 50 deletions

diff --git a/frontend/analtypes.icl b/frontend/analtypes.icl
index f68e216..664c21d 100644
--- a/frontend/analtypes.icl
+++ b/frontend/analtypes.icl
@@ -13,6 +13,65 @@ AS_NotChecked :== -1
 kindError kind1 kind2 error
 	= checkError "conflicting kinds: " (toString kind1 +++ " and " +++ toString kind2) error
 
+skipIndirections (KI_Var kind_info_ptr) kind_heap
+	# (kind, kind_heap) = readPtr kind_info_ptr kind_heap
+	= skip_indirections kind_info_ptr kind kind_heap
+where
+	skip_indirections this_info_ptr kind=:(KI_Var kind_info_ptr) kind_heap
+		| this_info_ptr == kind_info_ptr
+			= (kind, kind_heap)
+			# (kind, kind_heap) = readPtr kind_info_ptr kind_heap
+			= skip_indirections kind_info_ptr kind kind_heap
+	skip_indirections this_info_ptr kind kind_heap
+		= (kind, kind_heap)
+skipIndirections kind kind_heap
+	= (kind, kind_heap)
+
+unifyKinds  :: !KindInfo !KindInfo !*UnifyKindsInfo -> *UnifyKindsInfo
+unifyKinds kind1 kind2 uni_info=:{uki_kind_heap}
+	# (kind1, uki_kind_heap) = skipIndirections kind1 uki_kind_heap
+	# (kind2, uki_kind_heap) = skipIndirections kind2 uki_kind_heap
+	= unify_kinds kind1 kind2 { uni_info & uki_kind_heap = uki_kind_heap }
+where	
+	unify_kinds kind1=:(KI_Var info_ptr1) kind2 uni_info
+		= case kind2 of
+			KI_Var info_ptr2
+				| info_ptr1 == info_ptr2
+					-> uni_info
+					-> { uni_info & uki_kind_heap = uni_info.uki_kind_heap <:= (info_ptr1, kind2) }
+			_
+				# (found, uki_kind_heap) = contains_kind_ptr info_ptr1 kind2 uni_info.uki_kind_heap
+				| found
+					-> { uni_info & uki_kind_heap = uki_kind_heap, uki_error = kindError kind1 kind2 uni_info.uki_error }
+					-> { uni_info & uki_kind_heap = uki_kind_heap <:= (info_ptr1, kind2)  }
+		where
+			contains_kind_ptr info_ptr (KI_Arrow kinds) kind_heap
+				= kinds_contains_kind_ptr info_ptr kinds kind_heap
+			contains_kind_ptr info_ptr (KI_Var kind_info_ptr) kind_heap
+				= (info_ptr == kind_info_ptr, kind_heap)
+			contains_kind_ptr info_ptr (KI_Const) kind_heap
+				= (False, kind_heap)
+
+			kinds_contains_kind_ptr info_ptr [ kind : kinds ] kind_heap
+				# (kind, kind_heap) = skipIndirections kind kind_heap
+				  (found, kind_heap) = contains_kind_ptr info_ptr kind kind_heap
+				| found
+					= (True, kind_heap)
+					= kinds_contains_kind_ptr info_ptr kinds kind_heap
+			kinds_contains_kind_ptr info_ptr [] kind_heap
+				= (False, kind_heap)
+	unify_kinds kind k1=:(KI_Var info_ptr1) uni_info
+		= unify_kinds k1 kind  uni_info
+	unify_kinds kind1=:(KI_Arrow kinds1) kind2=:(KI_Arrow kinds2) uni_info=:{uki_error}
+		| length kinds1 == length kinds2
+			= fold2St unifyKinds kinds1 kinds2 uni_info
+			= { uni_info & uki_error = kindError kind1 kind2 uki_error }
+	unify_kinds KI_Const KI_Const uni_info
+		= uni_info
+	unify_kinds kind1 kind2 uni_info=:{uki_error}
+		= { uni_info & uki_error = kindError kind1 kind2 uki_error }
+
+/*
 unifyKinds  :: !KindInfo !KindInfo !*UnifyKindsInfo -> *UnifyKindsInfo
 unifyKinds (KI_Indirection kind1) kind2 uni_info=:{uki_kind_heap}
 	= unifyKinds kind1 kind2 uni_info
@@ -35,7 +94,6 @@ where
 		= info_ptr1 == kind_info_ptr
 	contains_kind_ptr info_ptr uki_kind_heap (KI_Const)
 		= False
-
 unifyKinds kind k1=:(KI_Var info_ptr1) uni_info
 	= unifyKinds k1 kind  uni_info
 unifyKinds kind1=:(KI_Arrow kinds1) kind2=:(KI_Arrow kinds2) uni_info=:{uki_error}
@@ -46,6 +104,7 @@ unifyKinds KI_Const KI_Const uni_info
 	= uni_info
 unifyKinds kind1 kind2 uni_info=:{uki_error}
 	= { uni_info & uki_error = kindError kind1 kind2 uki_error }
+*/
 
 class toKindInfo a :: !a -> KindInfo
 
@@ -114,16 +173,11 @@ where
 	analTypes has_root_attr modules form_tvs {tv_info_ptr}  (conds=:{con_var_binds}, as=:{as_heaps, as_kind_heap})
 		# (TVI_TypeKind kind_info_ptr, th_vars) = readPtr tv_info_ptr as_heaps.th_vars
 		  (kind_info, as_kind_heap) = readPtr kind_info_ptr as_kind_heap
-		  kind_info = skip_indirections kind_info
+		  (kind_info, as_kind_heap) = skipIndirections kind_info as_kind_heap
 		| isEmpty form_tvs
 			= (cMAXINT, kind_info, cIsHyperStrict, (conds, { as & as_heaps = { as_heaps & th_vars = th_vars }, as_kind_heap = as_kind_heap }))
 			= (cMAXINT, kind_info, cIsHyperStrict, ({ conds & con_var_binds = [{vb_var = kind_info_ptr, vb_vars = form_tvs } : con_var_binds] },
 						 { as & as_heaps = { as_heaps & th_vars = th_vars }, as_kind_heap = as_kind_heap }))
-	where
-		skip_indirections (KI_Indirection kind)
-			= skip_indirections kind
-		skip_indirections kind
-			= kind
 
 instance analTypes Type
 where
@@ -365,15 +419,16 @@ where
 				
 		retrieve_kind (KindVar kind_info_ptr) kind_heap
 			# (kind_info, kind_heap) = readPtr kind_info_ptr kind_heap
-			= (determine_kind kind_info, kind_heap)
+			= determine_kind kind_info kind_heap
 		where
-			determine_kind (KI_Indirection kind) 
-				= determine_kind kind
-			determine_kind (KI_Arrow kinds)
-				//AA: = KindArrow (length kinds)
-				= KindArrow [determine_kind k \\ k <- kinds]
-			determine_kind kind
-				= KindConst
+			determine_kind kind kind_heap
+				# (kind, kind_heap) = skipIndirections kind kind_heap
+				= case kind of
+					KI_Arrow kinds
+						# (kinds, kind_heap) = mapSt determine_kind kinds kind_heap
+						-> (KindArrow kinds, kind_heap)
+					_
+						-> (KindConst, kind_heap)
 			   
 	unify_var_binds :: ![VarBind] !*KindHeap -> *KindHeap
 	unify_var_binds binds kind_heap
diff --git a/frontend/checktypes.icl b/frontend/checktypes.icl
index 847f8fa..ea81616 100644
--- a/frontend/checktypes.icl
+++ b/frontend/checktypes.icl
@@ -267,7 +267,7 @@ checkTypeDef :: !Index !Index !*TypeSymbols !*TypeInfo !*CheckState -> (!*TypeSy
 checkTypeDef type_index module_index ts=:{ts_type_defs} ti=:{ti_type_heaps} cs=:{cs_error}
 	# (type_def, ts_type_defs) = ts_type_defs![type_index]
 	# {td_name,td_pos,td_args,td_attribute} = type_def
-	  position = newPosition td_name td_pos
+	# position = newPosition td_name td_pos
 	  cs_error = pushErrorAdmin position cs_error
 	  (td_attribute, attr_vars, th_attrs) = determine_root_attribute td_attribute td_name.id_name ti_type_heaps.th_attrs
 	  (type_vars, (attr_vars, ti_type_heaps, cs))
@@ -287,6 +287,7 @@ where
 	determine_root_attribute TA_Unique name attr_var_heap
 		= (TA_Unique, [], attr_var_heap)
 
+
 CS_Checked	:== 1
 CS_Checking	:== 0
 
diff --git a/frontend/parse.icl b/frontend/parse.icl
index a8ca287..567aae1 100644
--- a/frontend/parse.icl
+++ b/frontend/parse.icl
@@ -1765,9 +1765,12 @@ tryAType tryAA annot attr pState
 		| isEmpty vars
 			= ( True, atype, pState)
 			= ( True, { atype & at_type = TFA vars atype.at_type }, pState)
-	// otherwise
-		# pState	= tokenBack pState
-		= tryApplicationType types annot attr pState
+	// otherwise (not that types is non-empty)
+// Sjaak	
+	# (atype, pState) = convertAAType types annot attr (tokenBack pState)
+	| isEmpty vars
+		= (True, atype, pState)
+		= (True, { atype & at_type = TFA vars atype.at_type }, pState)
 /* PK
 tryFunctionType :: ![AType] !Annotation !TypeAttribute !ParseState -> (!Bool,!AType,!ParseState)
 tryFunctionType types annot attr pState
@@ -1784,22 +1787,17 @@ where
 		= {at_annotation = annot, at_attribute = attr, at_type = t1 --> make_curry_type AN_None TA_None tr res_type}
 	make_curry_type _ _ _ _ = abort "make_curry_type: wrong assumption"
 
-tryApplicationType :: ![AType] !Annotation !TypeAttribute !ParseState -> (!Bool,!AType,!ParseState)
-tryApplicationType [type1:types_rest] annot attr pState
-	#	(annot, pState)	= determAnnot annot type1.at_annotation pState
-		type			= type1.at_type
-		(attr, pState)	= determAttr attr type1.at_attribute type pState
-	| isEmpty types_rest
-		= ( True
-		  , {at_annotation = annot, at_attribute = attr, at_type = type}
-		  , pState
-		  )
+// Sjaak ...
+convertAAType :: ![AType] !Annotation !TypeAttribute !ParseState -> (!AType,!ParseState)
+convertAAType [atype:atypes] annot attr pState
+	#	(annot, pState)	= determAnnot annot atype.at_annotation pState
+		type			= atype.at_type
+		(attr, pState)	= determAttr attr atype.at_attribute type pState
+	| isEmpty atypes
+		= ( {at_annotation = annot, at_attribute = attr, at_type = type}, pState)
 	// otherwise // type application
-		# (type, pState)	= convert_list_of_types type1.at_type types_rest pState
-		= ( True
-		  , {at_annotation = annot, at_attribute = attr, at_type = type}
-		  , pState
-		  )
+		# (type, pState)	= convert_list_of_types atype.at_type atypes pState
+		= ({at_annotation = annot, at_attribute = attr, at_type = type}, pState)
 where
 	convert_list_of_types (TA sym []) types pState
 		= (TA { sym & type_arity = length types } types, pState)
@@ -1815,9 +1813,11 @@ where
 //..AA
 	convert_list_of_types _ types pState
 		= (TE, parseError "Type" No "ordinary type variable" pState)
+// ... Sjaak
+/*
 tryApplicationType _ annot attr pState
 	= (False, {at_annotation = annot, at_attribute = attr, at_type = TE}, pState)
-
+*/
 tryBrackType :: !ParseState -> (!Bool, Type, !ParseState)
 tryBrackType pState
 	# (succ, atype, pState) 	= trySimpleType AN_None TA_None pState
diff --git a/frontend/refmark.icl b/frontend/refmark.icl
index 477242f..6ed1d44 100644
--- a/frontend/refmark.icl
+++ b/frontend/refmark.icl
@@ -579,7 +579,7 @@ where
 				
 		has_observing_base_type (VI_Type {at_type} _) type_def_infos subst
 			= has_observing_type at_type type_def_infos subst
-		has_observing_base_type (VI_FAType _ {at_type}) type_def_infos subst
+		has_observing_base_type (VI_FAType _ {at_type} _) type_def_infos subst
 			= has_observing_type at_type type_def_infos subst
 		has_observing_base_type _ type_def_infos subst
 			= abort "has_observing_base_type (refmark.icl)"
diff --git a/frontend/syntax.dcl b/frontend/syntax.dcl
index f92b7d5..1a3a345 100644
--- a/frontend/syntax.dcl
+++ b/frontend/syntax.dcl
@@ -519,7 +519,8 @@ cIsALocalVar	:== False
 
 :: AP_Kind = APK_Constructor !Index | APK_Macro
 
-::	VarInfo  =	VI_Empty | VI_Type !AType !(Optional CoercionPosition) | VI_FAType ![ATypeVar] !AType | VI_Occurrence !Occurrence | VI_UsedVar !Ident |
+::	VarInfo  =	VI_Empty | VI_Type !AType !(Optional CoercionPosition) | VI_FAType ![ATypeVar] !AType !(Optional CoercionPosition) |
+				VI_Occurrence !Occurrence | VI_UsedVar !Ident |
 				VI_Expression !Expression | VI_Variable !Ident !VarInfoPtr | VI_LiftedVariable !VarInfoPtr |
 				VI_Count !Int /* the reference count of a variable */ !Bool /* true if the variable is global, false otherwise */ |
 				VI_AccVar !ConsClass !ArgumentPosition /* used during fusion to determine accumulating parameters of functions */ |
@@ -854,7 +855,6 @@ cNonRecursiveAppl	:== False
 ::	KindInfoPtr	:== Ptr KindInfo
 
 ::	KindInfo	= KI_Var !KindInfoPtr
-				| KI_Indirection !KindInfo
 				| KI_Arrow ![KindInfo]
 				| KI_Const
 				
diff --git a/frontend/syntax.icl b/frontend/syntax.icl
index 83c26a3..5660068 100644
--- a/frontend/syntax.icl
+++ b/frontend/syntax.icl
@@ -504,7 +504,8 @@ cIsALocalVar	:== False
 
 :: AP_Kind = APK_Constructor !Index | APK_Macro
 
-::	VarInfo  =	VI_Empty | VI_Type !AType !(Optional CoercionPosition) | VI_FAType ![ATypeVar] !AType | VI_Occurrence !Occurrence | VI_UsedVar !Ident |
+::	VarInfo  =	VI_Empty | VI_Type !AType !(Optional CoercionPosition) | VI_FAType ![ATypeVar] !AType !(Optional CoercionPosition) |
+				VI_Occurrence !Occurrence | VI_UsedVar !Ident |
 				VI_Expression !Expression | VI_Variable !Ident !VarInfoPtr | VI_LiftedVariable !VarInfoPtr |
 				VI_Count !Int /* the reference count of a variable */ !Bool /* true if the variable is global, false otherwise */ |
 				VI_AccVar !ConsClass !ArgumentPosition /* used during fusion to determine accumulating parameters of functions */ |
@@ -827,7 +828,6 @@ cNotVarNumber :== -1
 ::	KindInfoPtr	:== Ptr KindInfo
 
 ::	KindInfo	= KI_Var !KindInfoPtr
-				| KI_Indirection !KindInfo
 				| KI_Arrow ![KindInfo]
 				| KI_Const
 				
diff --git a/frontend/type.icl b/frontend/type.icl
index ab4ca6b..0f551bb 100644
--- a/frontend/type.icl
+++ b/frontend/type.icl
@@ -1132,7 +1132,7 @@ where
 		= case var_info of
 			VI_Type type _
 				-> (type, Yes var_expr_ptr, (reqs, ts))
-			VI_FAType vars type
+			VI_FAType vars type _
 				# ts = foldSt bind_var_and_attr vars ts
 		  		  (fresh_type, ts_type_heaps) = freshCopy type ts.ts_type_heaps
 		  		-> (fresh_type, Yes var_expr_ptr, (reqs, { ts & ts_type_heaps = ts_type_heaps }))
@@ -1594,8 +1594,8 @@ makeBase fun_or_cons_ident arg_nr [{fv_name, fv_info_ptr} : vars] [type : types]
 		= makeBase fun_or_cons_ident (arg_nr+1) vars types (addToBase fv_info_ptr type (Yes (CP_FunArg fun_or_cons_ident arg_nr)) ts_var_heap)
 		= makeBase fun_or_cons_ident (arg_nr+1) vars types (addToBase fv_info_ptr type No ts_var_heap)
 
-addToBase info_ptr atype=:{at_type = TFA atvs type} _ ts_var_heap 
-	= ts_var_heap  <:= (info_ptr, VI_FAType atvs { atype & at_type = type})
+addToBase info_ptr atype=:{at_type = TFA atvs type} optional_position ts_var_heap 
+	= ts_var_heap  <:= (info_ptr, VI_FAType atvs { atype & at_type = type} optional_position)
 addToBase info_ptr type optional_position ts_var_heap
 	= ts_var_heap  <:= (info_ptr, VI_Type type optional_position)
 	
@@ -2487,13 +2487,13 @@ is_rare_name {id_name}
 	= id_name.[0]=='_'
 
 getPositionOfExpr expr=:(Var {var_info_ptr}) var_heap
-	# (VI_Type _ opt_position, var_heap) = readPtr var_info_ptr var_heap
-	= (case opt_position of
-		Yes position
-			-> position
-		No
-			-> CP_Expression expr,
-	   var_heap)
+	= case readPtr var_info_ptr var_heap of
+		(VI_Type _ (Yes position), var_heap)
+			-> (position, var_heap)
+		(VI_FAType _ _ (Yes position), var_heap)
+			-> (position, var_heap)
+		(_, var_heap)
+			-> (CP_Expression expr, var_heap)
 getPositionOfExpr expr var_heap
 	= (CP_Expression expr, var_heap)