Labels for blocks, loops, & switches #99
Conversation
|
So in both this and #98, I'm wondering if it's a good idea to desugar ops into other ops in Alternatively, there is another strategy that has already been on my mind: since there is already some collapsing going on where many "ops" (that have different names in AstSemantics.md) are given a single ML constructor in |
|
Yes, it's a good point, and has been bothering me as well. I'll give it a
try to introduce a "sugared ast" and move the current desugaring out of the
parser.
|
|
Great! |
|
One question of course is what to do with the use and resolution of symbolic names. I think it would be inadequate to have those appear inside |
|
Agreed. |
|
Could this also get rid of I also think it's less confusing to call |
|
It's only surface syntactic sugar for I'd be fine with |
I mean that you could get rid of the |
|
Ah, I see. Well, then it wouldn't be a desugaring any more, but a proper
translation. I think it's better to keep the input syntax a superset of the
core syntax, and allow access to desugared constructs directly. If for
nothing else, then for writing specific tests of malformed code.
|
|
Superseded by #117 |
Adding new spec tests
This PR adds the dependency to multi-value to the exception handling proposal text and to the README. I wrote an explanation of this dependency on the proposal text, but it's easier to see this once the verification and execution steps of `br_on_exn` and of `try` blocks are written out, as done [here](WebAssembly/exception-handling#87 (comment)) by @rossberg : Validation: ``` ft = t1* -> t2* C, label t2* |- e1* : t1* -> t2* C, label t2* |- e2* : exnref -> t2* ----------------------------------- C |- try ft e1* catch e2* end : ft C_label(l) = C_exn(x) = t* ------------------------------------- C |- br_on_exn l x : exnref -> exnref ``` Execution: ``` v^n (try ft e1* catch e2* end) --> catch_m{e2*} (label_m{} v^n e1* end) end) (iff ft = t1^n -> t2^m) S; F; catch_m{e*} T[v^n (throw a)] end --> S; F; label_m{} (exn a v^n) e* end (iff S_exn(a) = {typ t^n}) F; (exn a v*) (br_on_exn l x) --> F; v* (br l) (iff F_exn(x) = a) ``` Concerning the functionality of `try`-`catch` blocks, note especially the passing of `v^n` values into a `label_m{}`. Concerning the functionality of `br_on_exn`, note especially the execution step resulting in a `br` instruction.
…bAssembly#115) This reverts commit 10d6c6c. This reverts WebAssembly#96, which squashed all upstream commits into one, which was not the recommended way in https://github.com/WebAssembly/proposals/blob/master/howto.md#syncing-with-upstream-changes. This leaves README.md untouched because WebAssembly#99 made significant changes on top of the merged version already.
Interpreter: - Fixed evaluation of v128 load/store instructions to work with i64 - Reworked bulk operation execution to still reduce to well-typed instructions for i32 - Added missing size check to table allocation - Various minor refactorings and clean-ups Tests: - Added tests for size check in i64 table and memory type limits Split out from #1839
* Fix validation of `switch`. The validation of `switch` was not working as intended when the "switcher" and "switchee" had different continuation type immediates. The fix is to replace the current continuation from the argument list with the switched-to continuation. The previous thing happened to be working when the "switcher" and "switchee" used the same continuation type immediate. I also noticed a bug in the testsuite runner. It was not running the stack switching tests since commit WebAssembly/stack-switching@70086b9. I have added the "stack-switching" subdirectory to the test script runner such that the tests are now being run again by `make test`. Resolves WebAssembly#98. * Update interpreter/valid/valid.ml Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org> --------- Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>
Inspired by Dan's larger patch (#98), this one introduces sugar to define a label directly as part of a
block,loop, orswitch. Aloopallows up to two labels, one to exit, the other to continue the loop.The patch also redefines
returnas sugar for abreak, slightly simplifying the spec, and making the core language compositional (you can now substitute function bodies, up to variable renaming).