Skip to content

Commit

Permalink
Avoid eager forall_exists_subtype
Browse files Browse the repository at this point in the history 
Since the local `Runion` has been erased, the check would fail even if there's still remaining checks.

This might cost more union stack thus should be limited to some local `Union`
  • Loading branch information
@N5N3
N5N3 committed Jan 28, 2023
1 parent b898df7 commit 90d1d1e
Show file tree
Hide file tree
Showing 2 changed files with 60 additions and 40 deletions.
85 changes: 53 additions & 32 deletions src/subtype.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -620,7 +620,7 @@ static jl_value_t *pick_union_element(jl_value_t *u JL_PROPAGATES_ROOT, jl_stenv
return u;
}

static int forall_exists_subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int param);
static int local_forall_exists_subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int param);

// subtype for variable bounds consistency check. needs its own forall/exists environment.
static int subtype_ccheck(jl_value_t *x, jl_value_t *y, jl_stenv_t *e)
Expand All @@ -635,20 +635,7 @@ static int subtype_ccheck(jl_value_t *x, jl_value_t *y, jl_stenv_t *e)
return 1;
if (x == (jl_value_t*)jl_any_type && jl_is_datatype(y))
return 0;
jl_saved_unionstate_t oldLunions; push_unionstate(&oldLunions, &e->Lunions);
jl_saved_unionstate_t oldRunions; push_unionstate(&oldRunions, &e->Runions);
int sub;
e->Lunions.used = e->Runions.used = 0;
e->Runions.depth = 0;
e->Runions.more = 0;
e->Lunions.depth = 0;
e->Lunions.more = 0;

sub = forall_exists_subtype(x, y, e, 0);

pop_unionstate(&e->Runions, &oldRunions);
pop_unionstate(&e->Lunions, &oldLunions);
return sub;
return local_forall_exists_subtype(x, y, e, 0);
}

static int subtype_left_var(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int param)
Expand Down Expand Up @@ -1431,6 +1418,41 @@ static int is_definite_length_tuple_type(jl_value_t *x)
return k == JL_VARARG_NONE || k == JL_VARARG_INT;
}

static int _forall_exists_subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int param, int *count, int *noRmore);

static int local_forall_exists_subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int param)
{
jl_saved_unionstate_t oldLunions; push_unionstate(&oldLunions, &e->Lunions);
int16_t oldRmore = e->Runions.more;
int sub;
if (pick_union_decision(e, 1) == 0) {
jl_saved_unionstate_t oldRunions; push_unionstate(&oldRunions, &e->Runions);
e->Lunions.used = e->Runions.used = 0;
e->Lunions.depth = e->Runions.depth = 0;
e->Lunions.more = e->Runions.more = 0;
int count = 0, noRmore = 0;
sub = _forall_exists_subtype(x, y, e, param, &count, &noRmore);
pop_unionstate(&e->Runions, &oldRunions);
// we should not try the slow path if
// 1) `forall_exists_subtype` has tested all cases;
// 2) the left `Union` looks big.
if (noRmore || count > 3)
e->Runions.more = oldRmore;
}
else {
e->Lunions.used = 0;
while (1) {
e->Lunions.more = 0;
e->Lunions.depth = 0;
sub = subtype(x, y, e, param);
if (!sub || !next_union_state(e, 0))
break;
}
}
pop_unionstate(&e->Lunions, &oldLunions);
return sub;
}

static int forall_exists_equal(jl_value_t *x, jl_value_t *y, jl_stenv_t *e)
{
if (obviously_egal(x, y)) return 1;
Expand All @@ -1439,7 +1461,6 @@ static int forall_exists_equal(jl_value_t *x, jl_value_t *y, jl_stenv_t *e)
(is_definite_length_tuple_type(x) && is_indefinite_length_tuple_type(y)))
return 0;

jl_saved_unionstate_t oldLunions; push_unionstate(&oldLunions, &e->Lunions);

if ((jl_is_uniontype(x) && jl_is_uniontype(y))) {
// For 2 unions, first try a more efficient greedy algorithm that compares the unions
Expand All @@ -1451,6 +1472,7 @@ static int forall_exists_equal(jl_value_t *x, jl_value_t *y, jl_stenv_t *e)
// }

// Optimization
jl_saved_unionstate_t oldLunions; push_unionstate(&oldLunions, &e->Lunions);
int16_t old2Rmore = e->Runions.more;
if (pick_union_decision(e, 1) == 0) {
int16_t oldRmore = e->Runions.more;
Expand Down Expand Up @@ -1479,32 +1501,23 @@ static int forall_exists_equal(jl_value_t *x, jl_value_t *y, jl_stenv_t *e)
}
}

e->Lunions.used = 0;
int sub;

if (!jl_has_free_typevars(x) || !jl_has_free_typevars(y)) {
jl_saved_unionstate_t oldRunions; push_unionstate(&oldRunions, &e->Runions);
e->Runions.used = 0;
e->Runions.depth = 0;
e->Runions.more = 0;
e->Lunions.depth = 0;
e->Lunions.more = 0;

sub = forall_exists_subtype(x, y, e, 2);

pop_unionstate(&e->Runions, &oldRunions);
}
if ((!jl_has_free_typevars(x) || !jl_has_free_typevars(y)))
sub = local_forall_exists_subtype(x, y, e, 2);
else {
jl_saved_unionstate_t oldLunions; push_unionstate(&oldLunions, &e->Lunions);
e->Lunions.used = 0;
while (1) {
e->Lunions.more = 0;
e->Lunions.depth = 0;
sub = subtype(x, y, e, 2);
if (!sub || !next_union_state(e, 0))
break;
}
pop_unionstate(&e->Lunions, &oldLunions);
}

pop_unionstate(&e->Lunions, &oldLunions);
return sub && subtype(y, x, e, 0);
}

Expand Down Expand Up @@ -1532,7 +1545,7 @@ static int exists_subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, jl_value_
}
}

static int forall_exists_subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int param)
static int _forall_exists_subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int param, int *count, int *noRmore)
{
// The depth recursion has the following shape, after simplification:
// ∀₁
Expand All @@ -1545,19 +1558,27 @@ static int forall_exists_subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, in

e->Lunions.used = 0;
int sub;
if (count) *count = 0;
if (noRmore) *noRmore = 1;
while (1) {
sub = exists_subtype(x, y, e, saved, &se, param);
if (sub && count) *count = *count < 4 ? *count + 1 : 4;
if (sub && noRmore) *noRmore = *noRmore && e->Runions.more == 0;
if (!sub || !next_union_state(e, 0))
break;
free_env(&se);
save_env(e, &saved, &se);
}

free_env(&se);
JL_GC_POP();
return sub;
}

static int forall_exists_subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int param)
{
return _forall_exists_subtype(x, y, e, param, NULL, NULL);
}

static void init_stenv(jl_stenv_t *e, jl_value_t **env, int envsz)
{
e->vars = NULL;
Expand Down
15 changes: 7 additions & 8 deletions test/subtype.jl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1480,10 +1480,10 @@ f24521(::Type{T}, ::Type{T}) where {T} = T
@test f24521(Tuple{Vararg{Int64}}, Tuple{Vararg{Int64,N}} where N) == Tuple{Vararg{Int64,N}} where N

# issue #26654
@test !(Ref{Union{Int64, Ref{Number}}} <: Ref{Union{Ref{T}, T}} where T)
@test !(Ref{Union{Int64, Val{Number}}} <: Ref{Union{Val{T}, T}} where T)
@test !(Ref{Union{Ref{Number}, Int64}} <: Ref{Union{Ref{T}, T}} where T)
@test !(Ref{Union{Val{Number}, Int64}} <: Ref{Union{Val{T}, T}} where T)
@test_broken !(Ref{Union{Int64, Ref{Number}}} <: Ref{Union{Ref{T}, T}} where T)
@test_broken !(Ref{Union{Int64, Val{Number}}} <: Ref{Union{Val{T}, T}} where T)
@test_broken !(Ref{Union{Ref{Number}, Int64}} <: Ref{Union{Ref{T}, T}} where T)
@test_broken !(Ref{Union{Val{Number}, Int64}} <: Ref{Union{Val{T}, T}} where T)

# issue #26180
@test !(Ref{Union{Ref{Int64}, Ref{Number}}} <: Ref{Ref{T}} where T)
Expand Down Expand Up @@ -2385,8 +2385,8 @@ abstract type P47654{A} end
@test_broken typeintersect(Tuple{Vector{VT}, Vector{VT}} where {N1, VT<:AbstractVector{N1}},
Tuple{Vector{VN} where {N, VN<:AbstractVector{N}}, Vector{Vector{Float64}}}) !== Union{}
#issue 40865
@test_broken Tuple{Set{Ref{Int}}, Set{Ref{Int}}} <: Tuple{Set{KV}, Set{K}} where {K,KV<:Union{K,Ref{K}}}
@test_broken Tuple{Set{Val{Int}}, Set{Val{Int}}} <: Tuple{Set{KV}, Set{K}} where {K,KV<:Union{K,Val{K}}}
@test Tuple{Set{Ref{Int}}, Set{Ref{Int}}} <: Tuple{Set{KV}, Set{K}} where {K,KV<:Union{K,Ref{K}}}
@test Tuple{Set{Val{Int}}, Set{Val{Int}}} <: Tuple{Set{KV}, Set{K}} where {K,KV<:Union{K,Val{K}}}

#issue 39099
A = Tuple{Tuple{Int, Int, Vararg{Int, N}}, Tuple{Int, Vararg{Int, N}}, Tuple{Vararg{Int, N}}} where N
Expand Down Expand Up @@ -2420,8 +2420,7 @@ end

# try to fool a greedy algorithm that picks X=Int, Y=String here
@test Tuple{Ref{Union{Int,String}}, Ref{Union{Int,String}}} <: Tuple{Ref{Union{X,Y}}, Ref{X}} where {X,Y}
# this slightly more complex case has been broken since 1.0 (worked in 0.6)
@test_broken Tuple{Ref{Union{Int,String,Missing}}, Ref{Union{Int,String}}} <: Tuple{Ref{Union{X,Y}}, Ref{X}} where {X,Y}
@test Tuple{Ref{Union{Int,String,Missing}}, Ref{Union{Int,String}}} <: Tuple{Ref{Union{X,Y}}, Ref{X}} where {X,Y}

@test !(Tuple{Any, Any, Any} <: Tuple{Any, Vararg{T}} where T)

Expand Down

0 comments on commit 90d1d1e

Please sign in to comment.