[spec] specify host functions in spectec#2210
Conversation
|
@rossberg We talked about upstreaming this part, and here we go. It should be a good starting point, but there're still TODOs. |
rossberg
left a comment
There was a problem hiding this comment.
Thanks, this looks good so far.
|
|
||
| def $lift_result(result) : instr* hint(show %) | ||
| def $lift_result(_VALS val*) = val* | ||
| def $lift_result(`(REF.EXN_ADDR a) THROW_REF) = (REF.EXN_ADDR a) THROW_REF |
There was a problem hiding this comment.
Note that the representation of exception results changes in #2189.
| rule Step/call_ref-hostfunc-res: | ||
| s; f; val^n (REF.FUNC_ADDR a) (CALL_REF yy) ~> s'; f; $lift_result(result) | ||
| ---- | ||
| -- if $funcinst((s; f))[a] = fi |
There was a problem hiding this comment.
Does it not work to use pattern matching here, like in the hand-written version?
There was a problem hiding this comment.
I think the reason was that there's a MODULE field in the record as well, so it has to appear in the pattern. But otherwise I don't see any problems. I can do it if it's preferred.
There was a problem hiding this comment.
Ah, right. In that case leave it as is.
There was a problem hiding this comment.
I was wondering why I needed the parens around (s; f) in the $funcinst call. Maybe the reason is in the latex generation:
-\mbox{if}~ (s ; f){.}\mathsf{funcs}{}[a] = {\mathit{fi}} \\
+\mbox{if}~ s ; f{.}\mathsf{funcs}{}[a] = {\mathit{fi}} \\
There was a problem hiding this comment.
Yes, exactly. Or more precisely, the show hint for $funcinst removes the call parens..
|
Quick reminder: please never, ever force-push to a PR branch, since that breaks half of GitHub's review work flow. ;) |
It breaks the prose backend.
The official spec still needs to splice the relevant additions from spectec.