Repository navigation
Commit e4867f4
committed
Short-circuit empty branches in function and list emptiness checks
Similar to #15619, avoid exploring branches whose result is already known.
In phi, a branch whose refined return type (ret ∧ return) or refined
argument (arg ∖ type) is empty is true, as empty types are never refined
back, so we return true without recursing over the remaining positives.
In list_line_empty?, subtype_seen?/3 already computes the difference
between the last types, so compute it once instead of computing it again
and re-checking its emptiness when the subtype check fails.
Timings per subtype?/2 call, before and after:
| Case | Before | After |
|---------------------------------------------|---------|--------|
| fun, 5 arrows with none() args (holds) | 114µs | 6.7µs |
| fun, 5 arrows with none() args (fails) | 58µs | 4.4µs |
| non_empty_list, 4 negatives cover the tail | 1.62µs | 1.49µs |
| non_empty_list, partial cover | 1.27µs | 1.13µs |
Assisted-by: Claude Code:claude-opus-5-51 parent 5313b1b commit e4867f4
1 file changed
Lines changed: 18 additions & 13 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1872 | 1872 | | |
1873 | 1873 | | |
1874 | 1874 | | |
1875 | | - | |
| 1875 | + | |
| 1876 | + | |
| 1877 | + | |
| 1878 | + | |
1876 | 1879 | | |
1877 | | - | |
| 1880 | + | |
| 1881 | + | |
| 1882 | + | |
1878 | 1883 | | |
1879 | 1884 | | |
1880 | 1885 | | |
| |||
1883 | 1888 | | |
1884 | 1889 | | |
1885 | 1890 | | |
| 1891 | + | |
| 1892 | + | |
| 1893 | + | |
1886 | 1894 | | |
1887 | | - | |
1888 | | - | |
1889 | | - | |
| 1895 | + | |
| 1896 | + | |
| 1897 | + | |
| 1898 | + | |
| 1899 | + | |
| 1900 | + | |
1890 | 1901 | | |
1891 | 1902 | | |
1892 | 1903 | | |
| |||
2474 | 2485 | | |
2475 | 2486 | | |
2476 | 2487 | | |
2477 | | - | |
2478 | | - | |
2479 | | - | |
2480 | | - | |
2481 | | - | |
2482 | | - | |
2483 | | - | |
2484 | | - | |
| 2488 | + | |
| 2489 | + | |
2485 | 2490 | | |
2486 | 2491 | | |
2487 | 2492 | | |
| |||
0 commit comments