Commit d72d21bd authored by Sjaak Smetsers's avatar Sjaak Smetsers
Browse files

bug fix: Improved unification algoritm for kinds

Universally quantified types (parsing and inference)
parent bb0d225f
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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)"
......
......@@ -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
......
......@@ -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
......
......@@ -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)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment