-
Notifications
You must be signed in to change notification settings - Fork 20
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(engine) Rewrite control flow inside loops. #988
Conversation
Code generation should be almost stable. The remaining part is to write the specific folds as part of the fstar |
384b180
to
e39a345
Compare
0233971
to
5fd14ea
Compare
@W95Psp still testing but you can start to review. |
5fd14ea
to
239cf75
Compare
05a1ee6
to
782b9f2
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks! I have a first set of comments!
@W95Psp I think I fixed everything according to your feedback! |
Great, looking at it. Next PR can you resolve discussions that you think are handled? |
Closes #393.
Loops are already translated as folds. This PR wraps their accumulators to add control flow information (in case of
break
return
orcontinue
). Some specific fold operators are also added to handle these wrapped accumulators.This PR puts
LocalMutation
beforeRewriteControlFlow
. InRewriteControlFlow
, we now deal with the body of loops (to push control flow in return position, like this phase already does forreturn
s outside loops). We also wrap loops that have areturn
inside a pattern matching over the result (to propagate a returned value), and apply the phase to inline what comes after in the branches of the pattern matching. PhaseDropNeedlessReturns
is nowDropREturnBreakContinue
. Inside loops it replacesreturn
,break
andcontinue
by their encoding in theControlFlow
enum. It treats a value in return position of a loop body like acontinue
. PhaseFunctionalizeLoops
selects the correctfold
operator (each fold should now come in 3 versions: the normal one, the one supportingbreak
andcontinue
, and the one supporting all type of control flow).