metamath / metamath-knife

Metamath-knife can rapidly verify Metamath proofs, providing strong confidence that the proofs are correct.
Apache License 2.0
25 stars 10 forks source link

Statement range iteration #61

Closed digama0 closed 2 years ago

digama0 commented 2 years ago

The main breaking changes are:

The main new feature is the addition of db.statements_range() which takes a range expression like label1..label2 or ..label or label.. or (Bound::Excluded(label1), Bound::Unbounded), and yields a double ended iterator. This can be used to find the next/previous statement from a given one, or iterate over statements in a range.

tirix commented 2 years ago

I see you have taken care to apply the SegmentId's special order in SegmentOrder::range(), and that a SegmentIter indeed iterates over slices of the ordered SegmentId's, so the obvious pitfall I could think of has been taken care of. I also see how both SegmentIter and StatementIter implement a double ended iterator and can be used to go back along statement addresses, while taking care of the special segment ordering. And I see how both are linked by flat_map in the statement_range_address API.

So this looks good to me! Sorry I have taken time to review this one.