Skip to content
This repository was archived by the owner on Apr 25, 2025. It is now read-only.

Add prose for typing rule of try-delegate. #237

Merged
merged 2 commits into from
Nov 17, 2022

Conversation

ioannad
Copy link
Collaborator

@ioannad ioannad commented Sep 16, 2022

Also slightly adjusted notation to match the formal overview.

Why WIP:

The prose is finished, but while trying to add explanatory notes, I couldn't find a reference in the spec to the validation label that the frame pushes to the context.

EDIT:
WIP is no longer necessary after addressing review comments.

Also slightly adjusted notation to match the formal overview.

Why WIP:

The prose is finished, but while trying to add explanatory notes,
I couldn't find a reference in the spec to the validation label that the frame
pushes to the context.
@ioannad ioannad requested a review from rossberg September 16, 2022 12:40
The :ref:`label index <syntax-labelidx>` after |DELEGATE| refers to a label surrounding the :ref:`try-delegate <syntax-try-delegate>` instruction. The furthest label it can refer to is the label inserted by the frame. For example, :math:`\TRY~\dots~\DELEGATE~0` may appear without any explicitly surrounding block, in which case the label 0 refers to the label of the frame.

.. todo::
Add references/links to "the label of the frame": Where is this label introduced?
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Frames represent calls and are unrelated to labels. A function body implicitly is a block, that's why it has an outermost label.

But in fact, I'd remove this entire note. It basically just explains again how labels and functions work, which is not specific to delegate. If we did that here, then we would have to do that for every br instruction.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

done.

}{
C \vdashinstrseq \TRY~\blocktype~\instr^\ast~\DELEGATE~l : [t_1^\ast]\to[t_2^\ast]
}

.. note::
The :ref:`notation <notation-extend>` :math:`C,\CLABELS\, [t^\ast]` inserts the new label type at index :math:`0`, shifting all others.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can we reuse the wording used for br and friends?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, switching to the wording of br.
FWIW I had copy pasted this from the note under if-else.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

done.

@ioannad ioannad changed the title WIP: Add prose for typing rule of try-delegate. Add prose for typing rule of try-delegate. Oct 13, 2022
@ioannad
Copy link
Collaborator Author

ioannad commented Oct 13, 2022

This should be now ready for merging, pending approval.

@ioannad ioannad merged commit 9fdb00b into WebAssembly:main Nov 17, 2022
@ioannad ioannad deleted the spec-prose-valid-try-delegate branch November 17, 2022 21:09
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants