|
@@ -269,10 +269,17 @@ type eq_kind =
|
|
|
| EqDoNotFollowNull (* like EqStrict, but does not follow Null<T> *)
|
|
|
|
|
|
type unification_context = {
|
|
|
- allow_transitive_cast : bool
|
|
|
+ allow_transitive_cast : bool;
|
|
|
+ equality_kind : eq_kind;
|
|
|
}
|
|
|
|
|
|
-let rec type_eq param a b =
|
|
|
+let default_unification_context = {
|
|
|
+ allow_transitive_cast = true;
|
|
|
+ equality_kind = EqStrict;
|
|
|
+}
|
|
|
+
|
|
|
+let rec type_eq uctx a b =
|
|
|
+ let param = uctx.equality_kind in
|
|
|
let can_follow t = match param with
|
|
|
| EqCoreType -> false
|
|
|
| EqDoNotFollowNull -> not (is_explicit_null t)
|
|
@@ -281,45 +288,45 @@ let rec type_eq param a b =
|
|
|
if a == b then
|
|
|
()
|
|
|
else match a , b with
|
|
|
- | TLazy f , _ -> type_eq param (lazy_type f) b
|
|
|
- | _ , TLazy f -> type_eq param a (lazy_type f)
|
|
|
+ | TLazy f , _ -> type_eq uctx (lazy_type f) b
|
|
|
+ | _ , TLazy f -> type_eq uctx a (lazy_type f)
|
|
|
| TMono t , _ ->
|
|
|
(match t.tm_type with
|
|
|
| None -> if param = EqCoreType || not (link t a b) then error [cannot_unify a b]
|
|
|
- | Some t -> type_eq param t b)
|
|
|
+ | Some t -> type_eq uctx t b)
|
|
|
| _ , TMono t ->
|
|
|
(match t.tm_type with
|
|
|
| None -> if param = EqCoreType || not (link t b a) then error [cannot_unify a b]
|
|
|
- | Some t -> type_eq param a t)
|
|
|
+ | Some t -> type_eq uctx a t)
|
|
|
| TAbstract ({a_path=[],"Null"},[t1]),TAbstract ({a_path=[],"Null"},[t2]) ->
|
|
|
- type_eq param t1 t2
|
|
|
+ type_eq uctx t1 t2
|
|
|
| TAbstract ({a_path=[],"Null"},[t]),_ when param <> EqDoNotFollowNull ->
|
|
|
- type_eq param t b
|
|
|
+ type_eq uctx t b
|
|
|
| _,TAbstract ({a_path=[],"Null"},[t]) when param <> EqDoNotFollowNull ->
|
|
|
- type_eq param a t
|
|
|
+ type_eq uctx a t
|
|
|
| TType (t1,tl1), TType (t2,tl2) when (t1 == t2 || (param = EqCoreType && t1.t_path = t2.t_path)) && List.length tl1 = List.length tl2 ->
|
|
|
- type_eq_params param a b tl1 tl2
|
|
|
+ type_eq_params uctx a b tl1 tl2
|
|
|
| TType (t,tl) , _ when can_follow a ->
|
|
|
- type_eq param (apply_params t.t_params tl t.t_type) b
|
|
|
+ type_eq uctx (apply_params t.t_params tl t.t_type) b
|
|
|
| _ , TType (t,tl) when can_follow b ->
|
|
|
rec_stack eq_stack (a,b)
|
|
|
(fun (a2,b2) -> fast_eq a a2 && fast_eq b b2)
|
|
|
- (fun() -> type_eq param a (apply_params t.t_params tl t.t_type))
|
|
|
+ (fun() -> type_eq uctx a (apply_params t.t_params tl t.t_type))
|
|
|
(fun l -> error (cannot_unify a b :: l))
|
|
|
| TEnum (e1,tl1) , TEnum (e2,tl2) ->
|
|
|
if e1 != e2 && not (param = EqCoreType && e1.e_path = e2.e_path) then error [cannot_unify a b];
|
|
|
- type_eq_params param a b tl1 tl2
|
|
|
+ type_eq_params uctx a b tl1 tl2
|
|
|
| TInst (c1,tl1) , TInst (c2,tl2) ->
|
|
|
if c1 != c2 && not (param = EqCoreType && c1.cl_path = c2.cl_path) && (match c1.cl_kind, c2.cl_kind with KExpr _, KExpr _ -> false | _ -> true) then error [cannot_unify a b];
|
|
|
- type_eq_params param a b tl1 tl2
|
|
|
+ type_eq_params uctx a b tl1 tl2
|
|
|
| TFun (l1,r1) , TFun (l2,r2) when List.length l1 = List.length l2 ->
|
|
|
let i = ref 0 in
|
|
|
(try
|
|
|
- type_eq param r1 r2;
|
|
|
+ type_eq uctx r1 r2;
|
|
|
List.iter2 (fun (n,o1,t1) (_,o2,t2) ->
|
|
|
incr i;
|
|
|
if o1 <> o2 then error [Not_matching_optional n];
|
|
|
- type_eq param t1 t2
|
|
|
+ type_eq uctx t1 t2
|
|
|
) l1 l2
|
|
|
with
|
|
|
Unify_error l ->
|
|
@@ -327,10 +334,10 @@ let rec type_eq param a b =
|
|
|
error (cannot_unify a b :: msg :: l)
|
|
|
)
|
|
|
| TDynamic a , TDynamic b ->
|
|
|
- type_eq param a b
|
|
|
+ type_eq uctx a b
|
|
|
| TAbstract (a1,tl1) , TAbstract (a2,tl2) ->
|
|
|
if a1 != a2 && not (param = EqCoreType && a1.a_path = a2.a_path) then error [cannot_unify a b];
|
|
|
- type_eq_params param a b tl1 tl2
|
|
|
+ type_eq_params uctx a b tl1 tl2
|
|
|
| TAnon a1, TAnon a2 ->
|
|
|
(try
|
|
|
(match !(a2.a_status) with
|
|
@@ -345,7 +352,7 @@ let rec type_eq param a b =
|
|
|
let f2 = PMap.find n a2.a_fields in
|
|
|
if f1.cf_kind <> f2.cf_kind && (param = EqStrict || param = EqCoreType || not (unify_kind f1.cf_kind f2.cf_kind)) then error [invalid_kind n f1.cf_kind f2.cf_kind];
|
|
|
let a = f1.cf_type and b = f2.cf_type in
|
|
|
- (try type_eq param a b with Unify_error l -> error (invalid_field n :: l));
|
|
|
+ (try type_eq uctx a b with Unify_error l -> error (invalid_field n :: l));
|
|
|
if (has_class_field_flag f1 CfPublic) != (has_class_field_flag f2 CfPublic) then error [invalid_visibility n];
|
|
|
with
|
|
|
Not_found ->
|
|
@@ -370,12 +377,12 @@ let rec type_eq param a b =
|
|
|
else
|
|
|
error [cannot_unify a b]
|
|
|
|
|
|
-and type_eq_params param a b tl1 tl2 =
|
|
|
+and type_eq_params uctx a b tl1 tl2 =
|
|
|
let i = ref 0 in
|
|
|
List.iter2 (fun t1 t2 ->
|
|
|
incr i;
|
|
|
try
|
|
|
- type_eq param t1 t2
|
|
|
+ type_eq uctx t1 t2
|
|
|
with Unify_error l ->
|
|
|
let err = cannot_unify a b in
|
|
|
error (err :: (Invariant_parameter !i) :: l)
|
|
@@ -383,14 +390,14 @@ and type_eq_params param a b tl1 tl2 =
|
|
|
|
|
|
let type_iseq a b =
|
|
|
try
|
|
|
- type_eq EqStrict a b;
|
|
|
+ type_eq default_unification_context a b;
|
|
|
true
|
|
|
with
|
|
|
Unify_error _ -> false
|
|
|
|
|
|
let type_iseq_strict a b =
|
|
|
try
|
|
|
- type_eq EqDoNotFollowNull a b;
|
|
|
+ type_eq {default_unification_context with equality_kind = EqDoNotFollowNull} a b;
|
|
|
true
|
|
|
with Unify_error _ ->
|
|
|
false
|
|
@@ -409,10 +416,6 @@ let print_stacks() =
|
|
|
print_endline "abstract_cast_stack";
|
|
|
List.iter (fun (a,b) -> Printf.printf "\t%s , %s\n" (st a) (st b)) abstract_cast_stack.rec_stack
|
|
|
|
|
|
-let default_unification_context = {
|
|
|
- allow_transitive_cast = true
|
|
|
-}
|
|
|
-
|
|
|
let rec unify (uctx : unification_context) a b =
|
|
|
if a == b then
|
|
|
()
|
|
@@ -625,7 +628,7 @@ let rec unify (uctx : unification_context) a b =
|
|
|
| TDynamic t2 ->
|
|
|
if t2 != b then
|
|
|
(try
|
|
|
- type_eq EqRightDynamic t t2
|
|
|
+ type_eq {uctx with equality_kind = EqRightDynamic} t t2
|
|
|
with
|
|
|
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) ->
|
|
@@ -639,7 +642,7 @@ let rec unify (uctx : unification_context) a b =
|
|
|
| TDynamic t2 ->
|
|
|
if t2 != a then
|
|
|
(try
|
|
|
- type_eq EqRightDynamic t t2
|
|
|
+ type_eq {uctx with equality_kind = EqRightDynamic} t t2
|
|
|
with
|
|
|
Unify_error l -> error (cannot_unify a b :: l));
|
|
|
| TAnon an ->
|
|
@@ -650,7 +653,7 @@ let rec unify (uctx : unification_context) a b =
|
|
|
| _ -> ());
|
|
|
PMap.iter (fun _ f ->
|
|
|
try
|
|
|
- type_eq EqStrict (field_type f) t
|
|
|
+ type_eq uctx (field_type f) t
|
|
|
with Unify_error l ->
|
|
|
error (invalid_field f.cf_name :: l)
|
|
|
) an.a_fields
|
|
@@ -737,12 +740,12 @@ and unify_from uctx ab tl a b t =
|
|
|
(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 EqRightDynamic 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 EqStrict 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
|
|
@@ -753,7 +756,7 @@ 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 EqStrict in
|
|
|
+ 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 monos = List.map (fun _ -> mk_mono()) cf.cf_params in
|
|
@@ -773,7 +776,7 @@ and unify_to_field uctx ab tl b (t,cf) =
|
|
|
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 EqStrict in
|
|
|
+ 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 monos = List.map (fun _ -> mk_mono()) cf.cf_params in
|
|
@@ -781,7 +784,7 @@ and unify_to_field uctx ab tl b (t,cf) =
|
|
|
let athis = map ab.a_this in
|
|
|
(* we cannot allow implicit casts when the this type is not completely known yet *)
|
|
|
(* if has_mono athis then raise (Unify_error []); *)
|
|
|
- with_variance uctx (type_eq EqStrict) athis (map ta);
|
|
|
+ with_variance uctx (type_eq {uctx with equality_kind = EqStrict}) athis (map ta);
|
|
|
(* immediate constraints checking is ok here because we know there are no monomorphs *)
|
|
|
List.iter2 (fun m (name,t) -> match follow t with
|
|
|
| TInst ({ cl_kind = KTypeParameter constr },_) when constr <> [] ->
|
|
@@ -804,15 +807,15 @@ and unify_with_variance uctx f t1 t2 =
|
|
|
if (Meta.has Meta.CoreType a1.a_meta) && (Meta.has Meta.CoreType a2.a_meta) then begin
|
|
|
let ta1 = apply_params a1.a_params pl1 a1.a_this in
|
|
|
let ta2 = apply_params a2.a_params pl2 a2.a_this in
|
|
|
- type_eq EqStrict ta1 ta2;
|
|
|
+ type_eq {uctx with equality_kind = EqStrict} ta1 ta2;
|
|
|
end;
|
|
|
if not (List.exists (allows_variance_to t2) a1.a_to) && not (List.exists (allows_variance_to t1) a2.a_from) then
|
|
|
error [cannot_unify t1 t2]
|
|
|
| TAbstract(a,pl),t ->
|
|
|
- type_eq EqBothDynamic (apply_params a.a_params pl a.a_this) t;
|
|
|
+ type_eq {uctx with equality_kind = EqBothDynamic} (apply_params a.a_params pl a.a_this) t;
|
|
|
if not (List.exists (fun t2 -> allows_variance_to t (apply_params a.a_params pl t2)) a.a_to) then error [cannot_unify t1 t2]
|
|
|
| t,TAbstract(a,pl) ->
|
|
|
- type_eq EqBothDynamic t (apply_params a.a_params pl a.a_this);
|
|
|
+ type_eq {uctx with equality_kind = EqBothDynamic} t (apply_params a.a_params pl a.a_this);
|
|
|
if not (List.exists (fun t2 -> allows_variance_to t (apply_params a.a_params pl t2)) a.a_from) then error [cannot_unify t1 t2]
|
|
|
| (TAnon a1 as t1), (TAnon a2 as t2) ->
|
|
|
rec_stack unify_stack (t1,t2)
|
|
@@ -827,7 +830,7 @@ and unify_type_params uctx a b tl1 tl2 =
|
|
|
List.iter2 (fun t1 t2 ->
|
|
|
incr i;
|
|
|
try
|
|
|
- with_variance uctx (type_eq EqRightDynamic) t1 t2
|
|
|
+ with_variance uctx (type_eq {uctx with equality_kind = EqRightDynamic}) t1 t2
|
|
|
with Unify_error l ->
|
|
|
let err = cannot_unify a b in
|
|
|
error (err :: (Invariant_parameter !i) :: l)
|
|
@@ -850,7 +853,7 @@ and unify_with_access uctx f1 t1 f2 =
|
|
|
if (has_class_field_flag f1 CfFinal) <> (has_class_field_flag f2 CfFinal) then raise (Unify_error [FinalInvariance]);
|
|
|
unify uctx t1 f2.cf_type
|
|
|
(* read/write *)
|
|
|
- | _ -> with_variance uctx (type_eq EqBothDynamic) t1 f2.cf_type
|
|
|
+ | _ -> with_variance uctx (type_eq {uctx with equality_kind = EqBothDynamic}) t1 f2.cf_type
|
|
|
|
|
|
let does_unify a b =
|
|
|
try
|
|
@@ -860,4 +863,7 @@ let does_unify a b =
|
|
|
false
|
|
|
|
|
|
let unify_custom = unify
|
|
|
-let unify = unify default_unification_context
|
|
|
+let unify = unify default_unification_context
|
|
|
+
|
|
|
+let type_eq_custom = type_eq
|
|
|
+let type_eq param = type_eq {default_unification_context with equality_kind = param}
|