More minor corrections, notation readability, "control" prose in block contexts.

Switching to "S ⊢ ..." notation for premises of typing rules for
administrative instructions, to match the spec document.

Readability: Changing quotes to number indices, and removing
unnecessary explicit exponent variables.

Suggesting prose for the new constructs in block contexts, connoting the
new structured administrative instructions with control frame opcodes.

Author: ioannad

proposals/exception-handling/Exceptions-formal-overview.md

@@ -74,12 +74,12 @@ C ⊢ rethrow l : [t1*]→[t2*]
 
 
 C ⊢ bt : [t1*]→[t2*]
-C, labels [t2*] ⊢ instr* : [t1*]→[t2*]
+C, labels [t2*] ⊢ instr1* : [t1*]→[t2*]
 (C.tags[x] = [t*]→[] ∧
- C, labels (catch [t2*]) ⊢ instr'* : [t*]→[t2*])*
-(C, labels (catch [t2*]) ⊢ instr''* : []→[t2*])?
+ C, labels (catch [t2*]) ⊢ instr2* : [t*]→[t2*])*
+(C, labels (catch [t2*]) ⊢ instr3* : []→[t2*])?
 -----------------------------------------------------------------------------
-C ⊢ try bt instr* (catch x instr'*)* (catch_all instr''*)? end : [t1*]→[t2*]
+C ⊢ try bt instr1* (catch x instr2*)* (catch_all instr3*)? end : [t1*]→[t2*]
 
 
 C ⊢ bt : [t1*]→[t2*]
@@ -130,6 +130,8 @@ C^k ::= 'catch'{ tagaddr? instr* }* B^k 'end'
       | 'delegate'{ labelidx } B^k 'end'
 ```
 
+Note the `C` in `C^k` above stands for `control`, because the related administrative instructions are in some ways modelling [control frame opcodes](https://webassembly.github.io/spec/core/appendix/algorithm.html?highlight=control#data-structures) "on the stack".
+
 #### Throw Contexts
 
 Throw contexts don't skip over handlers (administrative `catch` or `delegate` instructions).
@@ -152,34 +154,34 @@ An absent tag address in a `catch` administrative instruction (i.e., `a? = ε`)
 ```
 F; throw x  ↪  F; throw a  (if F.module.tagaddrs[x]=a)
 
-caught{a val^n} B^l[rethrow l] end
-  ↪ caught{a val^n} B^l[val^n (throw a)] end
+caught{a val*} B^l[rethrow l] end
+  ↪ caught{a val*} B^l[val* (throw a)] end
 
-caught{a val^n} val^m end  ↪  val^m
+caught{a val0*} val* end  ↪  val*
 
 
-F; val^n (try bt instr* (catch x instr'*)* (catch_all instr''*)? end)
-  ↪  F; label_m{} (catch{a instr'*}*{ε instr''*}? val^n instr* end) end
+F; val^n (try bt instr1* (catch x instr2*)* (catch_all instr3*)? end)
+  ↪  F; label_m{} (catch{a instr2*}*{ε instr3*}? val^n instr1* end) end
   (if expand_F(bt) = [t1^n]→[t2^m] ∧ (F.module.tagaddrs[x]=a)*)
 
-catch{a? instr*}* val^m end ↪ val^m
+catch{a? instr*}* val* end ↪ val*
 
-S; F; catch{a1? instr*}{a'? instr'*}* T[val^n (throw a)] end
-  ↪  S; F; caught{a val^n} (val^n)? instr* end
+S; F; catch{a1? instr1*}{a0? instr0*}* T[val^n (throw a)] end
+  ↪  S; F; caught{a val^n} (val^n)? instr1* end
   (if (a1? = ε ∨ a1? = a) ∧ S.tags(a).type = [t^n]→[])
 
-catch{a1? instr*}{a'? instr'*}* T[val^n (throw a)] end
-  ↪ catch{a'? instr'*}* T[val^n (throw a)] end
+catch{a1? instr*}{a0? instr0*}* T[val^n (throw a)] end
+  ↪ catch{a0? instr0*}* T[val^n (throw a)] end
   (if a1? ≠ ε ∧ a1? ≠ a)
 
-catch T[val^n (throw a)] end ↪  val^n (throw a)
+catch T[val* (throw a)] end ↪  val* (throw a)
 
 
 F; val^n (try bt instr* delegate l)
   ↪ F; label_m{} (delegate{l} val^n instr* end) end
-  (if expand_F(bt) = [t^n]→[t^m])
+  (if expand_F(bt) = [t1^n]→[t2^m])
 
-delegate{l} val^n end ↪ val^n
+delegate{l} val* end ↪ val*
 
 label_m{} B^l[ delegate{l} T[val^n (throw a)] end ] end
   ↪ val^n (throw a)
@@ -194,24 +196,25 @@ There is a subtle difference though. The instruction `br l` searches for the `l+
 
 ### Typing Rules for Administrative Instructions
 
+
 ```
-S.tags[a].type = [t*]→[]
---------------------------------
+S ⊢ tag a : tag [t*]→[]
+-------------------------------
 S;C ⊢ throw a : [t1* t*]→[t2*]
 
-((S.tags[a].type = [t'*]→[])?
- S;C, labels (catch [t*]) ⊢ instr'* : [t'*?]→[t*])*
-S;C, labels [t*] ⊢ instr* : []→[t*]
+((S ⊢ tag a : tag [t*]→[])?
+ S;C, labels (catch [t2*]) ⊢ instr2* : [t1*?]→[t2*])*
+S;C, labels [t2*] ⊢ instr1* : []→[t2*]
 -----------------------------------------------------------
-S;C, labels [t*] ⊢ catch{a? instr'*}* instr* end : []→[t*]
+S;C, labels [t2*] ⊢ catch{a? instr2*}* instr1* end : []→[t2*]
 
 S;C, labels [t*] ⊢ instr* : []→[t*]
-C.labels[l] = [t'*]
+C.labels[l] = [t0*]
 ------------------------------------------------------
 S;C, labels [t*] ⊢ delegate{l} instr* end : []→[t*]
 
-S.tags[a].type = [t'*]→[]
-(val:t')*
+S ⊢ tag a : tag [t0*]→[]
+(val:t0)*
 S;C, labels (catch [t*]) ⊢ instr* : []→[t*]
 ----------------------------------------------------------
 S;C, labels [t*] ⊢ caught{a val^n} instr* end : []→[t*]