Rewrite control flow inside loops.

Open maximebuyse opened this issue 1 year ago • 1 comments

Closes #393.

Loops are already translated as folds. This PR wraps their accumulators to add control flow information (in case of break return or continue). Some specific fold operators are also added to handle these wrapped accumulators.

Oct 10 '24 15:10 maximebuyse

Code generation should be almost stable. The remaining part is to write the specific folds as part of the fstar Rust_primitives

Oct 10 '24 15:10 maximebuyse

@W95Psp still testing but you can start to review.

Oct 21 '24 14:10 maximebuyse

@W95Psp I think I fixed everything according to your feedback!

Oct 23 '24 16:10 maximebuyse

Great, looking at it. Next PR can you resolve discussions that you think are handled?

Oct 24 '24 07:10 W95Psp