Idris2
Idris2 copied to clipboard
[ performance ] More stack safety in the Prelude
This PR adds transform rules for making map, mapMaybe, and filter for List and SnocList plus some other utilities tail recursive.
A note about mapImpl: The following transform rule is ignored during compilation:
%transform "tailRecMap" map {f = List} = List.mapTR
I checked this with several different variations including the follow, where all arguments are given explicitly, and none of them worked:
%transform "tailRecMap" map {b} {a} {f = List} f xs = List.mapTR f xs
I therefore extracted map for List and SnocList to utility functions mapImpl, and applied the transform rules to those, which works nicely as shown in the adjusted test case for the node backend.
This is strange. Any idea why the windows test fails?
Actually, I forgot the correctness proof for SnocLists tail recursive append, and indeed, the implementation was wrong. :-)