Add prose for typing rule of CAUGHTadm #229
Conversation
Fixes related .. todo:: section. Also slightly adjusted notation to match the one in the [formal overview document](https://github.com/WebAssembly/exception-handling/blob/main/proposals/exception-handling/Exceptions-formal-overview.md).
| Add prose. | ||
| * The :ref:`external tag value <syntax-externval>` :math:`\EVTAG~\tagaddr` must be :ref:`valid <valid-externval-tag>` with some :ref:`external tag type <syntax-externtype>` :math:`\ETTAG~[t_0^\ast] \to []`. | ||
|
|
||
| * The :ref:`values <syntax-val>` :math:`\val^\ast` must be of type :math:`[t_0^\ast]`. |
There was a problem hiding this comment.
I think this isn't defined as written, and requires a loop over the individual values.
|
|
||
| * The :ref:`values <syntax-val>` :math:`\val^\ast` must be of type :math:`[t_0^\ast]`. | ||
|
|
||
| * Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the label :math:`(\LCATCH~[t^\ast])` prepended to the |CLABELS| vector. |
There was a problem hiding this comment.
This seems wrong. Note that the typing rule requires that there already is a labeltype t* at the front of the labels (which you need to check!), and this is just adjusting it.
|
|
||
| * Let :math:`C''` be the same :ref:`context <context>` as :math:`C`, but with the label :math:`[t^\ast]` prepended to the |CLABELS| vector. | ||
|
|
||
| * Then the compound instruction is valid under context :math:`C''` with type :math:`[] \to [t^\ast]`. |
There was a problem hiding this comment.
Ah, I see, what you are trying. But the context C is an input, you cannot construct another one here. If there are constraints on it, those have to be checked.
There was a problem hiding this comment.
@rossberg, looking for past review comments I had forgotten I found this, which was the reason for the (still misplaced) change you found in PR#241. How should this prose and rule look like after all?
There was a problem hiding this comment.
The prose needs to first check the topmost entry of its input context C, and then construct C' from it by updating that, and check the body under that C'.
Fixes the typing rule of CAUGHTadm as suggested in: WebAssembly#229 (comment)
* Fixes the typing rule of CAUGHTadm as suggested in: #229 (comment) * Applying suggestion from PR #241 https://github.com/WebAssembly/exception-handling/pull/241/files/201ff276be6c458e7a819662eb2862bd475f2fcd..f97c9d108a999c3c3fd30f25554a113822bed1b8#r1030097793 * Applied suggestions from code review, fixed notation, also adding the missing _n to CAUGHTadm. The subscript is introduced by the changes in PR #226
Fixes related .. todo:: section.
Also slightly adjusted notation to match the one in the formal overview document.