Lasse Letager Hansen
Lasse Letager Hansen
Part of #28. Need use statements #73 , early returns #15.
There are still some issues, and the library is not fully implemented, however this should be enough for now, we can always add more as we go.
We can add a phase that unrolls (guarded) matches, e.g. ```rust match foo { Foo { a, .. } if a > 10 => 1, Foo { b, .. }...
From what I can see `MachineIntergers.v` file is not directly part of CompCert library, so we do need it here.
> > From what I can see `MachineIntergers.v` file is not directly part of CompCert library, so we do need it here. > > Interesting. So, where does it come...
Yes, but I would like to add some testing, and structure the library a bit, but I guess those can be follow up PRs.
We have been using CompCert integers for the Coq backend, I was just updating them, to remove the weird extra file (MachineIntegers.v). If there is a better or more standard...
Closed in favor of #987 and annotated core lib.
This issue is related to #375 as the graph is not getting an edge, since the concrete idents are not equal.
I have a solution in a higher level language compiled to Piet (https://github.com/cmester0/Piet/blob/main/Rust/tests/advc/primes.advc), I can generate the Piet solution if you would like it.