Browse Source

[abstracts] code style changes for abstract unify functions (#9704)

Dmitrii Maganov 5 years ago
parent
commit
05740e5277
3 changed files with 105 additions and 99 deletions
  1. 5 6
      src/context/abstractCast.ml
  2. 29 28
      src/core/abstract.ml
  3. 71 65
      src/core/tUnification.ml

+ 5 - 6
src/context/abstractCast.ml

@@ -40,8 +40,7 @@ and do_check_cast ctx uctx tleft eright p =
 		if cf == ctx.curfield || rec_stack_memq cf cast_stack then error "Recursive implicit cast" p;
 		if cf == ctx.curfield || rec_stack_memq cf cast_stack then error "Recursive implicit cast" p;
 		rec_stack_loop cast_stack cf f ()
 		rec_stack_loop cast_stack cf f ()
 	in
 	in
-	let find a tl f =
-		let tcf,cf = f() in
+	let make (a,tl,(tcf,cf)) =
 		if (Meta.has Meta.MultiType a.a_meta) then
 		if (Meta.has Meta.MultiType a.a_meta) then
 			mk_cast eright tleft p
 			mk_cast eright tleft p
 		else match a.a_impl with
 		else match a.a_impl with
@@ -61,9 +60,9 @@ and do_check_cast ctx uctx tleft eright p =
 				let stack = (tleft,tright) :: stack in
 				let stack = (tleft,tright) :: stack in
 				match follow tleft,follow tright with
 				match follow tleft,follow tright with
 				| TAbstract(a1,tl1),TAbstract(a2,tl2) ->
 				| TAbstract(a1,tl1),TAbstract(a2,tl2) ->
-					Abstract.find_to_from uctx find a1 tl1 a2 tl2 tleft eright.etype
+					make (Abstract.find_to_from uctx eright.etype tleft a2 tl2 a1 tl1)
 				| TAbstract(a,tl),_ ->
 				| TAbstract(a,tl),_ ->
-					begin try find a tl (fun () -> Abstract.find_from uctx a tl eright.etype tleft)
+					begin try make (a,tl,Abstract.find_from uctx eright.etype a tl)
 					with Not_found ->
 					with Not_found ->
 						let rec loop2 tcl = match tcl with
 						let rec loop2 tcl = match tcl with
 							| tc :: tcl ->
 							| tc :: tcl ->
@@ -74,7 +73,7 @@ and do_check_cast ctx uctx tleft eright p =
 						loop2 a.a_from
 						loop2 a.a_from
 					end
 					end
 				| _,TAbstract(a,tl) ->
 				| _,TAbstract(a,tl) ->
-					begin try find a tl (fun () -> Abstract.find_to uctx a tl tleft)
+					begin try make (a,tl,Abstract.find_to uctx tleft a tl)
 					with Not_found ->
 					with Not_found ->
 						let rec loop2 tcl = match tcl with
 						let rec loop2 tcl = match tcl with
 							| tc :: tcl ->
 							| tc :: tcl ->
@@ -213,7 +212,7 @@ let find_multitype_specialization com a pl p =
 	in
 	in
 	let _,cf =
 	let _,cf =
 		try
 		try
-			Abstract.find_to uctx a tl m
+			Abstract.find_to uctx m a tl
 		with Not_found ->
 		with Not_found ->
 			let at = apply_params a.a_params pl a.a_this in
 			let at = apply_params a.a_params pl a.a_this in
 			let st = s_type (print_context()) at in
 			let st = s_type (print_context()) at in

+ 29 - 28
src/core/abstract.ml

@@ -9,46 +9,47 @@ let build_abstract a = match a.a_impl with
 	| Some c -> ignore(c.cl_build())
 	| Some c -> ignore(c.cl_build())
 	| None -> ()
 	| None -> ()
 
 
-let has_direct_to uctx ab pl b =
-	List.exists (unify_to {uctx with allow_transitive_cast = false} ab pl b) ab.a_to
+let has_direct_from uctx a b ab tl =
+	unifies_from {uctx with allow_transitive_cast = false} a b ab tl
 
 
-let has_direct_from uctx ab pl a b =
-	List.exists (unify_from {uctx with allow_transitive_cast = false} ab pl a b) ab.a_from
+let has_direct_to uctx a b ab tl =
+	unifies_to {uctx with allow_transitive_cast = false} a b ab tl
 
 
-let find_field_to uctx ab pl b =
-	build_abstract ab;
-	List.find (unify_to_field uctx ab pl b) ab.a_to_field
+let find_field_from uctx a b ab tl =
+	List.find (unifies_from_field uctx a b ab tl) ab.a_from_field
 
 
-let find_field_from uctx ab pl a b =
-	build_abstract ab;
-	List.find (unify_from_field uctx ab pl a b) ab.a_from_field
+let find_field_to uctx a b ab tl =
+	List.find (unifies_to_field uctx a b ab tl) ab.a_to_field
 
 
-let find_to_from uctx f ab_left tl_left ab_right tl_right tleft tright =
-	build_abstract ab_left;
-	build_abstract ab_right;
-	if has_direct_to uctx ab_right tl_right tleft || has_direct_from uctx ab_left tl_left tright tleft then
+let find_to_from uctx a b a1 tl1 a2 tl2 =
+	build_abstract a1;
+	build_abstract a2;
+	if has_direct_to uctx a b a1 tl1 || has_direct_from uctx a b a2 tl2 then
 		raise Not_found
 		raise Not_found
-	else
-		try f ab_right tl_right (fun () -> find_field_to uctx ab_right tl_right tleft)
-		with Not_found -> f ab_left tl_left (fun () -> find_field_from uctx ab_left tl_left tright tleft)
+	else try
+		(a1,tl1,find_field_to uctx a b a1 tl1)
+	with Not_found ->
+		(a2,tl2,find_field_from uctx a b a2 tl2)
 
 
-let find_to uctx ab pl b =
+let find_from uctx a ab tl =
+	let b = TAbstract(ab,tl) in
 	build_abstract ab;
 	build_abstract ab;
-	if follow b == t_dynamic then
-		List.find (fun (t,_) -> follow t == t_dynamic) ab.a_to_field
-	else if has_direct_to uctx ab pl b then
+	if follow a == t_dynamic then
+		List.find (fun (t,_) -> follow t == t_dynamic) ab.a_from_field
+	else if has_direct_from uctx a b ab tl then
 		raise Not_found (* legacy compatibility *)
 		raise Not_found (* legacy compatibility *)
 	else
 	else
-		find_field_to uctx ab pl b
+		find_field_from uctx a b ab tl
 
 
-let find_from uctx ab pl a b =
+let find_to uctx b ab tl =
+	let a = TAbstract(ab,tl) in
 	build_abstract ab;
 	build_abstract ab;
-	if follow a == t_dynamic then
-		List.find (fun (t,_) -> follow t == t_dynamic) ab.a_from_field
-	else if has_direct_from uctx ab pl a b then
+	if follow b == t_dynamic then
+		List.find (fun (t,_) -> follow t == t_dynamic) ab.a_to_field
+	else if has_direct_to uctx a b ab tl then
 		raise Not_found (* legacy compatibility *)
 		raise Not_found (* legacy compatibility *)
 	else
 	else
-		find_field_from uctx ab pl a b
+		find_field_to uctx a b ab tl
 
 
 let underlying_type_stack = new_rec_stack()
 let underlying_type_stack = new_rec_stack()
 
 
@@ -90,7 +91,7 @@ let rec get_underlying_type ?(return_first=false) a pl =
 			`find_to` is probably needed for `@:multiType`
 			`find_to` is probably needed for `@:multiType`
 		*)
 		*)
 		let m = mk_mono() in
 		let m = mk_mono() in
-		let _ = find_to default_unification_context a pl m in
+		let _ = find_to default_unification_context m a pl in
 		maybe_recurse (follow m)
 		maybe_recurse (follow m)
 	with Not_found ->
 	with Not_found ->
 		if Meta.has Meta.CoreType a.a_meta then
 		if Meta.has Meta.CoreType a.a_meta then

+ 71 - 65
src/core/tUnification.ml

@@ -648,7 +648,7 @@ let rec unify (uctx : unification_context) a b =
 			| KTypeParameter pl -> List.exists (fun t ->
 			| KTypeParameter pl -> List.exists (fun t ->
 				match follow t with
 				match follow t with
 				| TInst (cs,tls) -> loop cs (List.map (apply_params c.cl_params tl) tls)
 				| TInst (cs,tls) -> loop cs (List.map (apply_params c.cl_params tl) tls)
-				| TAbstract(aa,tl) -> List.exists (unify_to uctx aa tl b) aa.a_to
+				| TAbstract(aa,tl) -> unifies_to uctx a b aa tl
 				| _ -> false
 				| _ -> false
 			) pl
 			) pl
 			| _ -> false)
 			| _ -> false)
@@ -794,8 +794,8 @@ let rec unify (uctx : unification_context) a b =
 					type_eq {uctx with equality_kind = EqRightDynamic} t t2
 					type_eq {uctx with equality_kind = EqRightDynamic} t t2
 				with
 				with
 					Unify_error l -> error (cannot_unify a b :: l));
 					Unify_error l -> error (cannot_unify a b :: l));
-		| TAbstract(bb,tl) when (List.exists (unify_from uctx bb tl a b) bb.a_from) ->
-			()
+		| TAbstract(bb,tl) ->
+			unify_from uctx a b bb tl
 		| _ ->
 		| _ ->
 			error [cannot_unify a b])
 			error [cannot_unify a b])
 	| _ , TDynamic t ->
 	| _ , TDynamic t ->
@@ -821,33 +821,23 @@ let rec unify (uctx : unification_context) a b =
 				) an.a_fields
 				) an.a_fields
 			with Unify_error l ->
 			with Unify_error l ->
 				error (cannot_unify a b :: l))
 				error (cannot_unify a b :: l))
-		| TAbstract(aa,tl) when (List.exists (unify_to uctx aa tl b) aa.a_to) ->
-			()
+		| TAbstract(aa,tl) ->
+			unify_to uctx a b aa tl
 		| _ ->
 		| _ ->
 			error [cannot_unify a b])
 			error [cannot_unify a b])
 	| TAbstract (aa,tl), _  ->
 	| TAbstract (aa,tl), _  ->
-		if not (List.exists (unify_to uctx aa tl b) aa.a_to) then error [cannot_unify a b];
+		unify_to uctx a b aa tl
 	| TInst ({ cl_kind = KTypeParameter ctl } as c,pl), TAbstract (bb,tl) ->
 	| TInst ({ cl_kind = KTypeParameter ctl } as c,pl), TAbstract (bb,tl) ->
 		(* one of the constraints must satisfy the abstract *)
 		(* one of the constraints must satisfy the abstract *)
 		if not (List.exists (fun t ->
 		if not (List.exists (fun t ->
 			let t = apply_params c.cl_params pl t in
 			let t = apply_params c.cl_params pl t in
 			try unify uctx t b; true with Unify_error _ -> false
 			try unify uctx t b; true with Unify_error _ -> false
-		) ctl) && not (List.exists (unify_from uctx bb tl a b) bb.a_from) then error [cannot_unify a b];
+		) ctl) then unify_from uctx a b bb tl
 	| _, TAbstract (bb,tl) ->
 	| _, TAbstract (bb,tl) ->
-		if not (List.exists (unify_from uctx bb tl a b) bb.a_from) then error [cannot_unify a b]
+		unify_from uctx a b bb tl
 	| _ , _ ->
 	| _ , _ ->
 		error [cannot_unify a b]
 		error [cannot_unify a b]
 
 
-and unify_abstracts uctx a b a1 tl1 a2 tl2 =
-	let uctx_no_transitive_casts = {uctx with allow_transitive_cast = false} in
-	if (List.exists (unify_to uctx_no_transitive_casts a1 tl1 b) a1.a_to)
-	|| (List.exists (unify_from uctx_no_transitive_casts a2 tl2 a b) a2.a_from)
-	|| (((Meta.has Meta.CoreType a1.a_meta) || (Meta.has Meta.CoreType a2.a_meta))
-		&& ((List.exists (unify_to uctx a1 tl1 b) a1.a_to) || (List.exists (unify_from uctx a2 tl2 a b) a2.a_from))) then
-		()
-	else
-		error [cannot_unify a b]
-
 and unify_anons uctx a b a1 a2 =
 and unify_anons uctx a b a1 a2 =
 	(try
 	(try
 		PMap.iter (fun n f2 ->
 		PMap.iter (fun n f2 ->
@@ -883,54 +873,70 @@ and unify_anons uctx a b a1 a2 =
 	with
 	with
 		Unify_error l -> error (cannot_unify a b :: l))
 		Unify_error l -> error (cannot_unify a b :: l))
 
 
-and unify_from uctx ab tl a b t =
-	rec_stack_bool abstract_cast_stack (a,b)
-		(fun (a2,b2) -> fast_eq a a2 && fast_eq b b2)
-		(fun() ->
-			let t = apply_params ab.a_params tl t in
-			let unify_func = if uctx.allow_transitive_cast then unify uctx else type_eq {uctx with equality_kind = EqRightDynamic} in
-			unify_func a t)
-
-and unify_to uctx ab tl b t =
-	let t = apply_params ab.a_params tl t in
-	let unify_func = if uctx.allow_transitive_cast then unify uctx else type_eq {uctx with equality_kind = EqStrict} in
-	try
-		unify_func t b;
-		true
-	with Unify_error _ ->
-		false
+and get_abstract_unify_func uctx equality_kind =
+	if uctx.allow_transitive_cast then unify uctx else type_eq {uctx with equality_kind = equality_kind}
 
 
-and unify_from_field uctx ab tl a b (t,cf) =
-	rec_stack_bool abstract_cast_stack (a,b)
-		(fun (a2,b2) -> fast_eq a a2 && fast_eq b b2)
-		(fun() ->
-			let unify_func = if uctx.allow_transitive_cast then unify uctx else type_eq {uctx with equality_kind = EqStrict} in
-			match follow cf.cf_type with
-			| TFun(_,r) ->
-				let map = apply_params ab.a_params tl in
-				let monos = Monomorph.spawn_constrained_monos map cf.cf_params in
-				let map t = map (apply_params cf.cf_params monos t) in
-				unify_func a (map t);
-				unify_func (map r) b;
-				true
-			| _ -> die "" __LOC__)
-
-and unify_to_field uctx ab tl b (t,cf) =
-	let a = TAbstract(ab,tl) in
-	rec_stack_bool abstract_cast_stack (b,a)
-		(fun (b2,a2) -> fast_eq a a2 && fast_eq b b2)
-		(fun() ->
-			let unify_func = if uctx.allow_transitive_cast then unify uctx else type_eq {uctx with equality_kind = EqStrict} in
-			match follow cf.cf_type with
-			| TFun((_,_,ta) :: _,_) ->
-				let map = apply_params ab.a_params tl in
-				let monos = Monomorph.spawn_constrained_monos map cf.cf_params in
-				let map t = map (apply_params cf.cf_params monos t) in
-				let athis = map ab.a_this in
-				(* we cannot allow implicit casts when the this type is not completely known yet *)
-				with_variance uctx (type_eq {uctx with equality_kind = EqStrict}) athis (map ta);
-				unify_func (map t) b;
-			| _ -> die "" __LOC__)
+and rec_stack_abstract_unifies a b frun =
+	rec_stack_bool abstract_cast_stack (a,b) (fun (a',b') -> fast_eq a a' && fast_eq b b') frun
+
+and unify_abstracts uctx a b a1 tl1 a2 tl2 =
+	if not (unifies_abstracts uctx a b a1 tl1 a2 tl2) then error [cannot_unify a b]
+
+and unify_from uctx a b ab tl =
+	if not (unifies_from uctx a b ab tl) then error [cannot_unify a b]
+
+and unify_to uctx a b ab tl =
+	if not (unifies_to uctx a b ab tl) then error [cannot_unify a b]
+
+and unifies_abstracts uctx a b a1 tl1 a2 tl2 =
+	let uctx_no_transitive_casts = {uctx with allow_transitive_cast = false} in
+	(unifies_to uctx_no_transitive_casts a b a1 tl1) || (unifies_from uctx_no_transitive_casts a b a2 tl2)
+	|| (((Meta.has Meta.CoreType a1.a_meta) || (Meta.has Meta.CoreType a2.a_meta))
+		&& ((unifies_to uctx a b a1 tl1) || (unifies_from uctx a b a2 tl2)))
+
+and unifies_from uctx a b ab tl =
+	List.exists (unifies_from_direct uctx a b ab tl) ab.a_from
+
+and unifies_to uctx a b ab tl =
+	List.exists (unifies_to_direct uctx a b ab tl) ab.a_to
+
+and unifies_from_direct uctx a b ab tl t =
+	rec_stack_abstract_unifies a b (fun() ->
+		let t = apply_params ab.a_params tl t in
+		let unify_func = get_abstract_unify_func uctx EqRightDynamic in
+		unify_func a t)
+
+and unifies_to_direct uctx a b ab tl t =
+	rec_stack_abstract_unifies a b (fun() ->
+		let t = apply_params ab.a_params tl t in
+		let unify_func = get_abstract_unify_func uctx EqStrict in
+		unify_func t b)
+
+and unifies_from_field uctx a b ab tl (t,cf) =
+	rec_stack_abstract_unifies a b (fun() ->
+		match follow cf.cf_type with
+		| TFun(_,r) ->
+			let map = apply_params ab.a_params tl in
+			let monos = Monomorph.spawn_constrained_monos map cf.cf_params in
+			let map t = map (apply_params cf.cf_params monos t) in
+			let unify_func = get_abstract_unify_func uctx EqStrict in
+			unify_func a (map t);
+			unify_func (map r) b;
+		| _ -> die "" __LOC__)
+
+and unifies_to_field uctx a b ab tl (t,cf) =
+	rec_stack_abstract_unifies a b (fun() ->
+		match follow cf.cf_type with
+		| TFun((_,_,ta) :: _,_) ->
+			let map = apply_params ab.a_params tl in
+			let monos = Monomorph.spawn_constrained_monos map cf.cf_params in
+			let map t = map (apply_params cf.cf_params monos t) in
+			let unify_func = get_abstract_unify_func uctx EqStrict in
+			let athis = map ab.a_this in
+			(* we cannot allow implicit casts when the this type is not completely known yet *)
+			with_variance uctx (type_eq {uctx with equality_kind = EqStrict}) athis (map ta);
+			unify_func (map t) b;
+		| _ -> die "" __LOC__)
 
 
 and unify_with_variance uctx f t1 t2 =
 and unify_with_variance uctx f t1 t2 =
 	let allows_variance_to t tf = type_iseq uctx tf t in
 	let allows_variance_to t tf = type_iseq uctx tf t in