feat: tail-recursive and short-circuiting version of List.any/all #392
Conversation
semorrison
added
the
awaiting-review
Co-authored-by: François G. Dorais <fgdorais@gmail.com>
| def anyTR (xs : List α) (p : α → Bool) : Bool := | ||
| go false xs | ||
| where | ||
| /-- Auxiliary for `anyTR`. -/ | ||
| go : Bool → List α → Bool | ||
| | true, _ => true | ||
| | false, [] => false | ||
| | false, h :: t => go (p h) t |
There was a problem hiding this comment.
How about the following?
| def anyTR (xs : List α) (p : α → Bool) : Bool := | |
| go false xs | |
| where | |
| /-- Auxiliary for `anyTR`. -/ | |
| go : Bool → List α → Bool | |
| | true, _ => true | |
| | false, [] => false | |
| | false, h :: t => go (p h) t | |
| def anyTR : List α -> (α → Bool) -> Bool | |
| | [], _ => false | |
| | h :: t, p => p h || anyTR t p |
There was a problem hiding this comment.
Neat! That is indeed tail recursive! Makes me wonder if it's intentional that List.any in core is not short-circuiting?
There was a problem hiding this comment.
After inspecting the C code in stage0, it seems that List.or, which is the specialization of List.any where p=id, compiles as short-circuiting tail-recursive code. I'm not sure about List.any though since it has a lot more C crud.
I wonder if the short-circuiting tail-recursive version should actually be in core?
There was a problem hiding this comment.
💡 Interesting. I wish we had an annotation to require / check tail-recursiveness...
There was a problem hiding this comment.
@fgdorais my tail recursion detector says that List.any/List.all is not tail-recursive, but List.or/List.and is, which is a bit mysterious.
There was a problem hiding this comment.
I'm ok with merging anyTR/allTR if that would unblock something, but making the change to core seems preferable.
| def allTR (xs : List α) (p : α → Bool) : Bool := | ||
| go true xs | ||
| where | ||
| /-- Auxiliary for `allTR`. -/ | ||
| go : Bool → List α → Bool | ||
| | false, _ => false | ||
| | true, [] => true | ||
| | true, h :: t => go (p h) t |
There was a problem hiding this comment.
| def allTR (xs : List α) (p : α → Bool) : Bool := | |
| go true xs | |
| where | |
| /-- Auxiliary for `allTR`. -/ | |
| go : Bool → List α → Bool | |
| | false, _ => false | |
| | true, [] => true | |
| | true, h :: t => go (p h) t | |
| def allTR : List α -> (α → Bool) -> Bool | |
| | [], _ => true | |
| | h :: t, p => p h && allTR t p |
|
I'll close this in favour of leanprover/lean4#2972. Reviews there welcome. |
Changes the implementation of `List.all` and `List.any` so they short-circuit. The implementations are tail-recursive. This replaces leanprover-community/batteries#392, which was going to do this with `@[csimp]`.
No description provided.