Jonathan Protzenko
Jonathan Protzenko
Can @mamonet investigate? Thanks for pinpointing this!
Yes it works now that I uninstalled the brew-provided cargo. Feel free to turn this into "warn against using system cargo", or "make sure cargo comes from rustup", or just...
Excellent. Thanks for minimizing!
Ok I worked around it by normalizing (t) to t everywhere.
Standard desugaring of lazy boolean operators to make sure the right hand side isn't eagerly evaluated? ``` if (e1 && e2) { e3 } else { e4 ``` becomes ```...
initially spotted by @franziskuskiefer
And maybe explain that the grammar won't backtrack (past N tokens, I presume) -- with backtracking one could possibly parse this expression, but it would be expensive.
``` jonathan@absinthe:~/Code/eurydice (protz/preserve_const) $ make -Bn test/fn_higher_order.llbc # --mir elaborated --add-drop-bounds /Users/jonathan/Code/charon/bin/charon rustc --preset=eurydice --dest-file "test/fn_higher_order.llbc" -- test/fn_higher_order.rs ``` (sorry in a rush)
Why are we parsing floats as floats? We should preserve them as strings, just like we do for machine integer literals, otherwise we're going to go through IEEE-754 rounding, possibly...
Yes. Also, it may be the case the in .NET lingo `float` means IEEE-754 simple precision. (That would explain your behavior.)