julia
2816a6f0 - effects: make `:terminates_globally` functional on recursive functions (#44210)

Commit
3 years ago
effects: make `:terminates_globally` functional on recursive functions (#44210) As with loop, it's hard to prove termination of recursive call automatically. But with this commit we can manually specify termination at least. ```julia Base.@assume_effects :terminates_globally function recur_termination1(x) x == 1 && return 1 1 < x < 20 || throw("bad") return x * recur_termination1(x-1) end @test fully_eliminated() do recur_termination1(12) end Base.@assume_effects :terminates_globally function recur_termination2(x) x == 1 && return 1 1 < x < 20 || throw("bad") return _recur_termination2(x) end _recur_termination2(x) = x * recur_termination2(x-1) @test fully_eliminated() do recur_termination2(12) end ```
Author
Parents
Loading