Abhiroop / okasaki

A Haskell Collections library. [WIP]
BSD 3-Clause "New" or "Revised" License
14 stars 3 forks source link

Fuse pattern in red black tree #2

Open tijsvd opened 8 months ago

tijsvd commented 8 months ago

Hi, looking at your code as a base for my own tree, as your nice pen drawings are all over google.

Just to let you know, I'm running into proptest failures in fuse. But my code is not in Haskell, I wouldn't know how to check yours.

In the red-red and black-black cases, the intermediate fuse may be empty, but there's no pattern for that case (RedBlackTree.hs lines 103 and 108) -- the catch pattern in your code describes a black node.

Red-red failure case: *insert 5, 3, 1, 2, 4

Black-black failure case:

Thanks

Abhiroop commented 7 months ago

Hey @tijsvd

Thanks for reporting! I plan to formally verify parts of this library soon, including the red-black tree deletion. Hopefully, that will catch any existing bugs.