Reduction semantics

proposals/stack-switching/Explainer.md

@@ -808,8 +808,8 @@ This abbreviation will be formalised with an auxiliary function or other means i
 
 - `suspend <tagidx>`
   - Use a control tag to suspend the current computation.
-  - `suspend $t : [t1*] -> [t2*]`
-    - iff `C.tags[$t] = tag $ft`
+  - `suspend $e : [t1*] -> [t2*]`
+    - iff `C.tags[$e] = tag $ft`
     - and `C.types[$ft] ~~ func [t1*] -> [t2*]`
 
 - `switch <typeidx> <tagidx>`
@@ -833,6 +833,147 @@ events and only `(on $e switch)` handlers can handle `switch`
 events. The handler search continues past handlers for the wrong kind
 of event, even if they use the correct tag.
 
+#### Store extensions
+
+* New store component `conts` for allocated continuations
+  - `S ::= {..., conts <cont>?*}`
+
+* A continuation is a context annotated with its hole's arity
+  - `cont ::= (E : n)`
+
+
+#### Administrative instructions
+
+* `(ref.cont a)` represents a continuation value, where `a` is a *continuation address* indexing into the store's `conts` component
+  - `ref.cont a : [] -> [(ref $ct)]`
+    - iff `S.conts[a] = epsilon \/ S.conts[a] = (E : n)`
+      + iff `E[val^n] : t2*`
+      + and `(val : t1)^n`
+    - and `$ct ~~ cont $ft`
+    - and `$ft ~~ [t1^n] -> [t2*]`
+
+* `(suspend.addr ea)` represents a `(suspend $e)` instruction where the tag index `$e` has been replaced with the physical address `ea` of the tag.
+  - `suspend.addr ea : [t1*] -> [t2*]`
+    - iff `S.tags[ea].type ~~ [t1*] -> [t2*]`
+
+* `(switch.addr $ct ea)` represents a `(switch $ct $e)` instruction where the tag index `$e` has been replaced with the physical address `ea` of the tag.
+  - `switch.addr $ct ea : [t1* (ref null $ct1)] -> [t2*]`
+    - iff `S.tags[$e].type ~~ [] -> [t*]`
+    - and `C.types[$ct] ~~ cont [t1* (ref null? $ct2)] -> [te1*]`
+    - and `te1* <: t*`
+    - and `C.types[$ct2] ~~ cont [t2*] -> [te2*]`
+    - and `t* <: te2*` 
+
+* `(prompt{<hdl>*} <instr>* end)` represents an active handler
+  - `(prompt{hdl*}? instr* end) : [] -> [t*]`
+    - iff `instr* : [] -> [t*]` in the empty context
+    - and `(hdl : [t*])*`
+
+The administrative structure `hdl` is defined as
+```
+hdl ::= (<tagaddr> $l) | (<tagaddr> switch)
+```
+
+where
+
+* `(a $l)` represents a tag-label association
+ - `(a $l) : [t2*]`
+    - iff `(S.tags[a].type ~~ [te1*] -> [te2*])*`
+    - and `(label $l : [te1'* (ref null? $ct')])*`
+    - and `([te1*] <: [te1'*])*`
+    - and `($ct' ~~ cont $ft')*`
+    - and `([te2*] -> [t2*] <: $ft')*`
+
+* `(a switch)` represents a tag-switch association
+ - `(a switch) : [t2*]`
+      - iff `(S.tags[b].type ~~ [] -> [te2*])*`
+
+
+#### Handler contexts
+
+```
+H^ea ::=
+  _
+  val* H^ea instr*
+  label_n{instr*} H^ea end
+  frame_n{F} H^ea end
+  catch{...} H^ea end
+  prompt{hdl*} H^ea end   (iff ea notin hdl*)
+```
+
+
+#### Reduction
+
+* `S; F; (ref.null t) (cont.new $ct)  -->  S; F; trap`
+
+* `S; F; (ref.func fa) (cont.new $ct)  -->  S'; F; (ref.cont |S.conts|)`
+  - iff `S' = S with conts += (E : n)`
+  - and `E = _ (invoke fa)`
+  - and `$ct ~~ cont $ft`
+  - and `$ft ~~ [t1^n] -> [t2*]`
+
+* `S; F; (ref.null t) (cont.bind $ct $ct')  -->  S; F; trap`
+
+* `S; F; (ref.cont ca) (cont.bind $ct $ct')  -->  S; F; trap`
+  - iff `S.conts[ca] = epsilon`
+
+* `S; F; v^n (ref.cont ca) (cont.bind $ct $ct')  -->  S'; F; (ref.cont |S.conts|)`
+  - iff `S.conts[ca] = (E' : n')`
+  - and `$ct' ~~ cont $ft'`
+  - and `$ft' ~~ [t1'*] -> [t2'*]`
+  - and `n = n' - |t1'*|`
+  - and `S' = S with conts[ca] = epsilon with conts += (E : |t1'*|)`
+  - and `E = E'[v^n _]`
+
+* `S; F; (ref.null t) (resume $ct hdl*)  -->  S; F; trap`
+
+* `S; F; (ref.cont ca) (resume $ct hdl*)  -->  S; F; trap`
+  - iff `S.conts[ca] = epsilon`
+
+* `S; F; v^n (ref.cont ca) (resume $ct hdl*)  -->  S'; F; prompt{hdl'*} E[v^n] end`
+  - iff `S.conts[ca] = (E : n)`
+  - and `S' = S with conts[ca] = epsilon`
+  - and `hdl'*` is obtained by translating the `<tagidx>` from `hdl*` into `<tagaddr>` using `F.tag`:
+       - if `on $a $l` is in `hdl*` and `F.tags[$e]=ea`, then `ea $l` is in `hdl'*`
+       - if `on $a switch` is in `hdl'*` and `F.tags[$e]=ea`, then `ea switch` is in `hdl'*`
+
+* `S; F; (ref.null t) (resume_throw $ct $e hdl*)  -->  S; F; trap`
+
+* `S; F; (ref.cont ca) (resume_throw $ct $e hdl*)  -->  S; F; trap`
+  - iff `S.conts[ca] = epsilon`
+
+* `S; F; v^m (ref.cont ca) (resume_throw $ct $e hdl*)  -->  S'; F; prompt{hdl'*} E[v^m (throw $e)] end`
+  - iff `S.conts[ca] = (E : n)`
+  - and `S.tags[F.tags[$e]].type ~~ [t1^m] -> [t2*]`
+  - and `S' = S with conts[ca] = epsilon`
+  - and `hdl'*` is obtained by translating the `<tagidx>` from `hdl*` into `<tagaddr>` using `F.tag`:
+       - if `on $a $l` is in `hdl*` and `F.tags[$e]=ea`, then `ea $l` is in `hdl'*`
+       - if `on $a switch` is in `hdl'*` and `F.tags[$e]=ea`, then `ea switch` is in `hdl'*`
+
+* `S; F; (prompt{hdl*} v* end)  -->  S; F; v*`
+
+* `S; F; (suspend $e) --> S; F; (suspend.addr ea)`
+  - iff `ea = F.tags[$e]`
+
+* `S; F; (prompt{hdl1* (ea $l) hdl2*} H^ea[v^n (suspend.addr ea)] end)  --> S'; F; v^n (ref.cont |S.conts|) (br $l)`
+  - iff `ea notin tagaddr(hdl1*)`
+  - and `S.tags[ea].type ~~ [t1^n] -> [t2^m]`
+  - and `S' = S with conts += (H^ea : m)`
+
+* `S; F; (switch $ct $e) --> S; F; (switch.addr $ct ea)`
+  - iff `ea = F.tags[$e]`
+
+* `S; F; (prompt{hdl1* (ea switch) hdl2*} H^ea[v^n (ref.cont ca) (switch.addr $ct ea)] end) --> S''; F; prompt{hdl1* (ea switch) hdl2*} E[v^n (ref.cont |S.conts|)] end`
+  - iff  `S.conts[ca] = (E : n')`
+  - and `n' = 1 + n`
+  - and `ea notin tagaddr(hdl1*)`
+  - and `$ct ~~ cont $ft`
+  - and `$ft ~~ [t1* (ref $ct2)] -> [t2*]`
+  - and `$ct2 ~~ cont $ft2`
+  - and `$ft2 ~~ [t1'^m] -> [t2'*]`
+  - and `S' = S with conts[ca] = epsilon`
+  - and `S'' = S' with conts += (H^ea : m)`
+
 ### Binary format
 
 We extend the binary format of composite types, heap types, and instructions.
@@ -856,7 +997,7 @@ The opcode for heap types is encoded as an `s33`.
 
 #### Instructions
 
-We use the use the opcode space `0xe0-0xe5` for the seven new instructions.
+We use the use the opcode space `0xe0-0xe5` for the six new instructions.
 
 | Opcode | Instruction              | Immediates |
 | ------ | ------------------------ | ---------- |