maximebuyse
maximebuyse
So if I understand well, to complete this issue we need this `RewriteControlFlow` phase that would come before `DropNeedlessReturn` and essentially deal with `return`s inside `if`s (potentially duplicating some code)....
We also need another phase (or a second visitor inside drop_needless_returns) to rewrite ``` let a = return b; c ``` as ``` return b ``` As they can be...
> I thought #907 is only partially implementing this? We have a lot of issues around this. My understanding is that #907 implements this one. But it is only a...
I am designing the part about loops. First attempt: - Apply the current `RewriteControlFlow` phase inside loops bodies but treat `break` and `continue` like `return`. After that, all of them...
> I am designing the part about loops. First attempt: > > * Apply the current `RewriteControlFlow` phase inside loops bodies but treat `break` and `continue` like `return`. After that,...
Here is an example of the rewriting: ``` fn f (v: &[i32]) -> i32 { let mut sum = 0; for i in v { if *i < 0 {...
> We wanted to work on that together in CC, but that will not happen this week (I thought I could do CC today, but after being awake for a...
Still relevant
I had an issue that seems to be related. The equality constraints inside a trait type argument are not translated to f*: https://hax-playground.cryspen.com/#fstar/3b38e61b99/gist=cc40e5e2c6579d215293f9378b9e871f
I tried the current implementation. Here is a list of what doesn't work: ### Situation A The bundle is created but both functions are named `f` in it. And they...