Tweak AL EnterI/ExitI instructions when being rendered

[jaehyun1ee]

This PR adds an additional pass on the generated prose (which is to be rendered, not interpreted), such that:

• PopI on the current context (label or frame) instead of ExitI, which says "Exit current context."
• EnterI on the context (label or frame) without mentioning the admin instruction LABEL_ or FRAME_.

The additional pass works by special-casing on the patterns of EnterI and ExitI instruction AST.

For example, for ExitI,

@@ -5971,11 +5981,11 @@ execution_of_RETURN
   b. Let n be the arity of F.
   c. Pop the values val^n from the stack.
   d. Pop all values val'* from the stack.
-  e. Exit current context.
+  e. Pop the current context from the stack.
   f. Push the values val^n to the stack.
 2. Else if the current context is LABEL_, then:
   a. Pop all values val* from the stack.
-  b. Exit current context.
+  b. Pop the current context from the stack.
   c. Push the values val* to the stack.
   d. Execute the instruction RETURN.

and for EnterI,

@@ -6285,8 +6295,7 @@ execution_of_BLOCK bt instr*
 3. Assert: Due to validation, there are at least m values on the top of the stack.
 4. Pop the values val^m from the stack.
 5. Let L be the label_n{[]}.
-6. Enter L with label instr* ++ [LABEL_]:
-  a. Push the values val^m to the stack.
+6. Enter val^m ++ instr* with label L.

[rossberg]

Thanks, this looks like a good improvement. Can we also somehow change "current context"? The spec does not define that – by "context" it only refers to typing or evaluation contexts. Instead of "the current context is X" it would say "X is on the top of the stack" and then "pop X".

[jaehyun1ee]

Can we also somehow change "current context"?

We need the phrase "current context", to distinguish what to do in the prose of RETURN and RETURN_CALL_REF. This all stems to our very choice to use bubbling-up semantics. For instance RETURN,

(* rule *)

rule Step_pure/return-frame:
  (FRAME_ n `{f} val'* val^n RETURN instr*)  ~>  val^n

rule Step_pure/return-label:
  (LABEL_ n `{instr'*} val* RETURN instr*)  ~>  val* RETURN

(* prose *)

execution_of_RETURN
1. If the current context is FRAME_, then:
  a. Let F be the current frame.
  b. Let n be the arity of F.
  c. Pop the values val^n from the stack.
  d. Pop all values val'* from the stack.
  e. Pop the current context from the stack.
  f. Push the values val^n to the stack.
2. Else if the current context is LABEL_, then:
  a. Pop all values val* from the stack.
  b. Pop the current context from the stack.
  c. Push the values val* to the stack.
  d. Execute the instruction RETURN.

The bubbling up semantics gives two rules for RETURN, which is returning n values if we were in the context of a frame, and simply discarding the LABEL if we were in the context of a label. Now, in the prose-generation point of view, we have to merge the two rules into one algorithm. Here, we can only distinguish the two different behaviors (steps 1a ~ 1f vs. 2a ~ 2d) by an IfI condition on, in which context we are in: a label or a frame.

[rossberg]

Yes, but that doesn't need a new notion. Manually I'd translate the rules to something like this:

execution_of_RETURN
1. Pop all values val* from the top of the stack.
2. If a frame is now on the top of the stack, then:
  a. Pop the frame F from the stack.
  b. Let n be the arity of F.
  c. Let val^n be the last n values of val*.
  d. Push the values val^n back to the stack.
3. Else if a label is now on the top of the stack, then:
  a. Pop the label from the stack.
  b. Push the values val* back to the stack.
  c. Execute the instruction RETURN.

If that doesn't work then the spec needs to introduce a term like "control entry" as the name for all non-value things on the stack, and the prose should say something like the "topmost control entry on the stack" instead of "current context".

Note also that it needs to say "pop all value from the top of the stack", because there can be more values on the stack below the frame or label entry, which are not affected.

[jaehyun1ee]

Thank you for the comment, I have modified the IL-to-AL translation logic such that we do not use the term "current context" (which corresponds to the GetCurContextE and ContextKindE AL AST) anymore in the generated AL.

Plus, I have also clarified "pop all values ... from the top of the stack".

execution_of_RETURN
-1. If the current context is FRAME_, then:
+1. Pop all values val* from the top of the stack.
+2. If a frame is now on the top of the stack, then:
   a. Let F be the current frame.
   b. Let n be the arity of F.
-  c. Pop the values val^n from the stack.
-  d. Pop all values val'* from the stack.
-  e. Pop the current context from the stack.
-  f. Push the values val^n to the stack.
-2. Else if the current context is LABEL_, then:
-  a. Pop all values val* from the stack.
-  b. Pop the current context from the stack.
-  c. Push the values val* to the stack.
-  d. Execute the instruction RETURN.
+  c. Pop the current frame from the stack.
+  d. Let val'* ++ val^n be val*.
+  e. Push the values val^n to the stack.
+3. Else if a label is now on the top of the stack, then:
+  a. Pop the current label from the stack.
+  b. Push the values val* to the stack.
+  c. Execute the instruction RETURN.