@@ -1565,37 +1565,12 @@ static int is_definite_length_tuple_type(jl_value_t *x)
1565
1565
return k == JL_VARARG_NONE || k == JL_VARARG_INT ;
1566
1566
}
1567
1567
1568
- static int _forall_exists_subtype (jl_value_t * x , jl_value_t * y , jl_stenv_t * e , int param , int * count , int * noRmore );
1569
-
1570
- static int may_contain_union_decision (jl_value_t * x , jl_stenv_t * e , jl_typeenv_t * log ) JL_NOTSAFEPOINT
1568
+ static int is_exists_typevar (jl_value_t * x , jl_stenv_t * e )
1571
1569
{
1572
- if (x == NULL || x == (jl_value_t * )jl_any_type || x == jl_bottom_type )
1573
- return 0 ;
1574
- if (jl_is_unionall (x ))
1575
- return may_contain_union_decision (((jl_unionall_t * )x )-> body , e , log );
1576
- if (jl_is_datatype (x )) {
1577
- jl_datatype_t * xd = (jl_datatype_t * )x ;
1578
- for (int i = 0 ; i < jl_nparams (xd ); i ++ ) {
1579
- jl_value_t * param = jl_tparam (xd , i );
1580
- if (jl_is_vararg (param ))
1581
- param = jl_unwrap_vararg (param );
1582
- if (may_contain_union_decision (param , e , log ))
1583
- return 1 ;
1584
- }
1585
- return 0 ;
1586
- }
1587
1570
if (!jl_is_typevar (x ))
1588
- return jl_is_type (x );
1589
- jl_typeenv_t * t = log ;
1590
- while (t != NULL ) {
1591
- if (x == (jl_value_t * )t -> var )
1592
- return 1 ;
1593
- t = t -> prev ;
1594
- }
1595
- jl_typeenv_t newlog = { (jl_tvar_t * )x , NULL , log };
1596
- jl_varbinding_t * xb = lookup (e , (jl_tvar_t * )x );
1597
- return may_contain_union_decision (xb ? xb -> lb : ((jl_tvar_t * )x )-> lb , e , & newlog ) ||
1598
- may_contain_union_decision (xb ? xb -> ub : ((jl_tvar_t * )x )-> ub , e , & newlog );
1571
+ return 0 ;
1572
+ jl_varbinding_t * vb = lookup (e , (jl_tvar_t * )x );
1573
+ return vb && vb -> right ;
1599
1574
}
1600
1575
1601
1576
static int has_exists_typevar (jl_value_t * x , jl_stenv_t * e ) JL_NOTSAFEPOINT
@@ -1626,31 +1601,9 @@ static int local_forall_exists_subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t
1626
1601
int kindy = !jl_has_free_typevars (y );
1627
1602
if (kindx && kindy )
1628
1603
return jl_subtype (x , y );
1629
- if (may_contain_union_decision (y , e , NULL ) && pick_union_decision (e , 1 ) == 0 ) {
1630
- jl_saved_unionstate_t oldRunions ; push_unionstate (& oldRunions , & e -> Runions );
1631
- e -> Lunions .used = e -> Runions .used = 0 ;
1632
- e -> Lunions .depth = e -> Runions .depth = 0 ;
1633
- e -> Lunions .more = e -> Runions .more = 0 ;
1634
- int count = 0 , noRmore = 0 ;
1635
- sub = _forall_exists_subtype (x , y , e , param , & count , & noRmore );
1636
- pop_unionstate (& e -> Runions , & oldRunions );
1637
- // We could skip the slow path safely if
1638
- // 1) `_∀_∃_subtype` has tested all cases
1639
- // 2) `_∀_∃_subtype` returns 1 && `x` and `y` contain no ∃ typevar
1640
- // Once `limit_slow == 1`, also skip it if
1641
- // 1) `_∀_∃_subtype` returns 0
1642
- // 2) the left `Union` looks big
1643
- // TODO: `limit_slow` ignores complexity from inner `local_∀_exists_subtype`.
1644
- if (limit_slow == -1 )
1645
- limit_slow = kindx || kindy ;
1646
- int skip = noRmore || (limit_slow && (count > 3 || !sub )) ||
1647
- (sub && (kindx || !has_exists_typevar (x , e )) &&
1648
- (kindy || !has_exists_typevar (y , e )));
1649
- if (skip )
1650
- e -> Runions .more = oldRmore ;
1651
- }
1652
- else {
1653
- // slow path
1604
+ int has_exists = (!kindx && has_exists_typevar (x , e )) ||
1605
+ (!kindy && has_exists_typevar (y , e ));
1606
+ if (has_exists && (is_exists_typevar (x , e ) != is_exists_typevar (y , e ))) {
1654
1607
e -> Lunions .used = 0 ;
1655
1608
while (1 ) {
1656
1609
e -> Lunions .more = 0 ;
@@ -1659,7 +1612,51 @@ static int local_forall_exists_subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t
1659
1612
if (!sub || !next_union_state (e , 0 ))
1660
1613
break ;
1661
1614
}
1615
+ return sub ;
1662
1616
}
1617
+ if (limit_slow == -1 )
1618
+ limit_slow = kindx || kindy ;
1619
+ jl_savedenv_t se ;
1620
+ save_env (e , & se , has_exists );
1621
+ int count , limited = 0 , ini_count = 0 ;
1622
+ jl_saved_unionstate_t latestLunions = {0 , 0 , 0 , NULL };
1623
+ while (1 ) {
1624
+ count = ini_count ;
1625
+ if (ini_count == 0 )
1626
+ e -> Lunions .used = 0 ;
1627
+ else
1628
+ pop_unionstate (& e -> Lunions , & latestLunions );
1629
+ while (1 ) {
1630
+ e -> Lunions .more = 0 ;
1631
+ e -> Lunions .depth = 0 ;
1632
+ if (count < 4 ) count ++ ;
1633
+ sub = subtype (x , y , e , param );
1634
+ if (limit_slow && count == 4 )
1635
+ limited = 1 ;
1636
+ if (!sub || !next_union_state (e , 0 ))
1637
+ break ;
1638
+ if (limited || !has_exists || e -> Runions .more == oldRmore ) {
1639
+ // re-save env and freeze the ∃decision for previous ∀Union
1640
+ // Note: We could ignore the rest `∃Union` decisions if `x` and `y`
1641
+ // contain no ∃ typevar, as they have no effect on env.
1642
+ ini_count = count ;
1643
+ push_unionstate (& latestLunions , & e -> Lunions );
1644
+ re_save_env (e , & se , has_exists );
1645
+ e -> Runions .more = oldRmore ;
1646
+ }
1647
+ }
1648
+ if (sub || e -> Runions .more == oldRmore )
1649
+ break ;
1650
+ assert (e -> Runions .more > oldRmore );
1651
+ next_union_state (e , 1 );
1652
+ restore_env (e , & se , has_exists ); // also restore Rdepth here
1653
+ e -> Runions .more = oldRmore ;
1654
+ }
1655
+ if (!sub )
1656
+ assert (e -> Runions .more == oldRmore );
1657
+ else if (limited || !has_exists )
1658
+ e -> Runions .more = oldRmore ;
1659
+ free_env (& se );
1663
1660
return sub ;
1664
1661
}
1665
1662
@@ -1729,7 +1726,7 @@ static int exists_subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, jl_savede
1729
1726
}
1730
1727
}
1731
1728
1732
- static int _forall_exists_subtype (jl_value_t * x , jl_value_t * y , jl_stenv_t * e , int param , int * count , int * noRmore )
1729
+ static int forall_exists_subtype (jl_value_t * x , jl_value_t * y , jl_stenv_t * e , int param )
1733
1730
{
1734
1731
// The depth recursion has the following shape, after simplification:
1735
1732
// ∀₁
@@ -1741,12 +1738,8 @@ static int _forall_exists_subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, i
1741
1738
1742
1739
e -> Lunions .used = 0 ;
1743
1740
int sub ;
1744
- if (count ) * count = 0 ;
1745
- if (noRmore ) * noRmore = 1 ;
1746
1741
while (1 ) {
1747
1742
sub = exists_subtype (x , y , e , & se , param );
1748
- if (count ) * count = (* count < 4 ) ? * count + 1 : 4 ;
1749
- if (noRmore ) * noRmore = * noRmore && e -> Runions .more == 0 ;
1750
1743
if (!sub || !next_union_state (e , 0 ))
1751
1744
break ;
1752
1745
re_save_env (e , & se , 1 );
@@ -1756,11 +1749,6 @@ static int _forall_exists_subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, i
1756
1749
return sub ;
1757
1750
}
1758
1751
1759
- static int forall_exists_subtype (jl_value_t * x , jl_value_t * y , jl_stenv_t * e , int param )
1760
- {
1761
- return _forall_exists_subtype (x , y , e , param , NULL , NULL );
1762
- }
1763
-
1764
1752
static void init_stenv (jl_stenv_t * e , jl_value_t * * env , int envsz )
1765
1753
{
1766
1754
e -> vars = NULL ;
0 commit comments