Merge pull request WebAssembly#11 from dhil/wasmfx-merge

Merge with WebAssembly/spec and WebAssembly/gc

Author: dhil

.github/workflows/ci-interpreter.yml

@@ -23,7 +23,7 @@ jobs:
         with:
           ocaml-compiler: 4.14.x
       - name: Setup OCaml tools
-        run: opam install --yes ocamlbuild.0.14.0 ocamlfind.1.9.5 js_of_ocaml.4.0.0 js_of_ocaml-ppx.4.0.0
+        run: opam install --yes ocamlfind.1.9.5 js_of_ocaml.4.0.0 js_of_ocaml-ppx.4.0.0
       - name: Setup Node.js
         uses: actions/setup-node@v2
         with:

document/core/appendix/changes.rst

@@ -188,9 +188,9 @@ Added managed reference types [#proposal-gc]_.
 
 * New :ref:`reference instructions <syntax-instr-ref>` for :ref:`array types <syntax-structtype>`: |ARRAYNEW|, |ARRAYNEWDEFAULT|, |ARRAYNEWFIXED|, |ARRAYNEWDATA|, |ARRAYNEWELEM|, :math:`\ARRAYGET\K{\_}\sx^?`, |ARRAYSET|, |ARRAYLEN|, |ARRAYFILL|, |ARRAYCOPY|, |ARRAYINITDATA|, |ARRAYINITELEM|
 
-* New :ref:`reference instructions <syntax-instr-ref>` for converting :ref:`host types <syntax-externtype>`: |EXTERNINTERNALIZE|, |EXTERNEXTERNALIZE|
+* New :ref:`reference instructions <syntax-instr-ref>` for converting :ref:`host types <syntax-externtype>`: |ANYCONVERTEXTERN|, |EXTERNCONVERTANY|
 
-* Extended set of :ref:`constant instructions <valid-const>` with |REFI31|, |STRUCTNEW|, |STRUCTNEWDEFAULT|, |ARRAYNEW|, |ARRAYNEWDEFAULT|, |ARRAYNEWFIXED|, |EXTERNINTERNALIZE|, |EXTERNEXTERNALIZE|, and |GLOBALGET| for any previously declared immutable :ref:`global <syntax-global>`
+* Extended set of :ref:`constant instructions <valid-const>` with |REFI31|, |STRUCTNEW|, |STRUCTNEWDEFAULT|, |ARRAYNEW|, |ARRAYNEWDEFAULT|, |ARRAYNEWFIXED|, |ANYCONVERTEXTERN|, |EXTERNCONVERTANY|, and |GLOBALGET| for any previously declared immutable :ref:`global <syntax-global>`
 
 
 .. [#proposal-signext]

document/core/appendix/index-instructions.py

@@ -279,7 +279,7 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
     Instruction(None, r'\hex{CF}'),
     Instruction(r'\REFNULL~\X{ht}', r'\hex{D0}', r'[] \to [(\REF~\NULL~\X{ht})]', r'valid-ref.null', r'exec-ref.null'),
     Instruction(r'\REFISNULL', r'\hex{D1}', r'[(\REF~\NULL~\X{ht})] \to [\I32]', r'valid-ref.is_null', r'exec-ref.is_null'),
-    Instruction(r'\REFFUNC~x', r'\hex{D2}', r'[] \to [\FUNCREF]', r'valid-ref.func', r'exec-ref.func'),
+    Instruction(r'\REFFUNC~x', r'\hex{D2}', r'[] \to [\REF~\X{ht}]', r'valid-ref.func', r'exec-ref.func'),
     Instruction(r'\REFEQ', r'\hex{D3}', r'[\EQREF~\EQREF] \to [\I32]', r'valid-ref.eq', r'exec-ref.eq'),
     Instruction(r'\REFASNONNULL', r'\hex{D4}', r'[(\REF~\NULL~\X{ht})] \to [(\REF~\X{ht})]', r'valid-ref.as_non_null', r'exec-ref.as_non_null'),
     Instruction(r'\BRONNULL~l', r'\hex{D5}', r'[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast~(\REF~\X{ht})]', r'valid-br_on_null', r'exec-br_on_null'),
@@ -327,15 +327,15 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
     Instruction(r'\STRUCTGETU~x~y', r'\hex{FB}~\hex{04}', r'[(\REF~\NULL~x)] \to [\I32]', r'valid-struct.get', r'exec-struct.get'),
     Instruction(r'\STRUCTSET~x~y', r'\hex{FB}~\hex{05}', r'[(\REF~\NULL~x)~t] \to []', r'valid-struct.set', r'exec-struct.set'),
     Instruction(r'\ARRAYNEW~x', r'\hex{FB}~\hex{06}', r'[t] \to [(\REF~x)]', r'valid-array.new', r'exec-array.new'),
-    Instruction(r'\ARRAYNEWDEFAULT~x', r'\hex{FB}~\hex{07}', r'[] \to [(\REF~x)]', r'valid-array.new', r'exec-array.new'),
+    Instruction(r'\ARRAYNEWDEFAULT~x', r'\hex{FB}~\hex{07}', r'[\I32] \to [(\REF~x)]', r'valid-array.new', r'exec-array.new'),
     Instruction(r'\ARRAYNEWFIXED~x~n', r'\hex{FB}~\hex{08}', r'[t^n] \to [(\REF~x)]', r'valid-array.new_fixed', r'exec-array.new_fixed'),
     Instruction(r'\ARRAYNEWDATA~x~y', r'\hex{FB}~\hex{09}', r'[\I32~\I32] \to [(\REF~x)]', r'valid-array.new_data', r'exec-array.new_data'),
     Instruction(r'\ARRAYNEWELEM~x~y', r'\hex{FB}~\hex{0A}', r'[\I32~\I32] \to [(\REF~x)]', r'valid-array.new_elem', r'exec-array.new_elem'),
     Instruction(r'\ARRAYGET~x', r'\hex{FB}~\hex{0B}', r'[(\REF~\NULL~x)~\I32] \to [t]', r'valid-array.get', r'exec-array.get'),
     Instruction(r'\ARRAYGETS~x', r'\hex{FB}~\hex{0C}', r'[(\REF~\NULL~x)~\I32] \to [\I32]', r'valid-array.get', r'exec-array.get'),
     Instruction(r'\ARRAYGETU~x', r'\hex{FB}~\hex{0D}', r'[(\REF~\NULL~x)~\I32] \to [\I32]', r'valid-array.get', r'exec-array.get'),
     Instruction(r'\ARRAYSET~x', r'\hex{FB}~\hex{0E}', r'[(\REF~\NULL~x)~\I32~t] \to []', r'valid-array.set', r'exec-array.set'),
-    Instruction(r'\ARRAYLEN', r'\hex{FB}~\hex{0F}', r'[\ARRAYREF] \to []', r'valid-array.len', r'exec-array.len'),
+    Instruction(r'\ARRAYLEN', r'\hex{FB}~\hex{0F}', r'[(\REF~\NULL~\ARRAY)] \to [\I32]', r'valid-array.len', r'exec-array.len'),
     Instruction(r'\ARRAYFILL~x', r'\hex{FB}~\hex{10}', r'[(\REF~\NULL~x)~\I32~t~\I32] \to []', r'valid-array.fill', r'exec-array.fill'),
     Instruction(r'\ARRAYCOPY~x~y', r'\hex{FB}~\hex{11}', r'[(\REF~\NULL~x)~\I32~(\REF~\NULL~y)~\I32~\I32] \to []', r'valid-array.copy', r'exec-array.copy'),
     Instruction(r'\ARRAYINITDATA~x~y', r'\hex{FB}~\hex{12}', r'[(\REF~\NULL~x)~\I32~\I32~\I32] \to []', r'valid-array.init_data', r'exec-array.init_data'),
@@ -346,8 +346,8 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
     Instruction(r'\REFCAST~(\REF~\NULL~t)', r'\hex{FB}~\hex{17}', r"[(\REF~\NULL~t')] \to [(\REF~\NULL~t)]", r'valid-ref.cast', r'exec-ref.cast'),
     Instruction(r'\BRONCAST~t_1~t_2', r'\hex{FB}~\hex{18}', r'[t_1] \to [t_1\reftypediff t_2]', r'valid-br_on_cast', r'exec-br_on_cast'),
     Instruction(r'\BRONCASTFAIL~t_1~t_2', r'\hex{FB}~\hex{19}', r'[t_1] \to [t_2]', r'valid-br_on_cast_fail', r'exec-br_on_cast_fail'),
-    Instruction(r'\EXTERNINTERNALIZE', r'\hex{FB}~\hex{1A}', r'[\EXTERNREF] \to [\ANYREF]', r'valid-extern.internalize', r'exec-extern.internalize'),
-    Instruction(r'\EXTERNEXTERNALIZE', r'\hex{FB}~\hex{1B}', r'[\ANYREF] \to [\EXTERNREF]', r'valid-extern.externalize', r'exec-extern.externalize'),
+    Instruction(r'\ANYCONVERTEXTERN', r'\hex{FB}~\hex{1A}', r'[(\REF~\NULL~\EXTERN)] \to [(\REF~\NULL~\ANY)]', r'valid-any.convert_extern', r'exec-any.convert_extern'),
+    Instruction(r'\EXTERNCONVERTANY', r'\hex{FB}~\hex{1B}', r'[(\REF~\NULL~\ANY)] \to [(\REF~\NULL~\EXTERN)]', r'valid-extern.convert_any', r'exec-extern.convert_any'),
     Instruction(r'\REFI31', r'\hex{FB}~\hex{1C}', r'[\I32] \to [\I31REF]', r'valid-ref.i31', r'exec-ref.i31'),
     Instruction(r'\I31GETS', r'\hex{FB}~\hex{1D}', r'[\I31REF] \to [\I32]', r'valid-i31.get_sx', r'exec-i31.get_sx'),
     Instruction(r'\I31GETU', r'\hex{FB}~\hex{1E}', r'[\I31REF] \to [\I32]', r'valid-i31.get_sx', r'exec-i31.get_sx'),

document/core/binary/instructions.rst

@@ -44,6 +44,7 @@ Control Instructions
 .. _binary-call_ref:
 .. _binary-call_indirect:
 .. _binary-return_call:
+.. _binary-return_call_ref:
 .. _binary-return_call_indirect:
 
 .. math::
@@ -131,8 +132,8 @@ Generic :ref:`reference instructions <syntax-instr-ref>` are represented by sing
 .. _binary-i31.get_u:
 .. _binary-ref.test:
 .. _binary-ref.cast:
-.. _binary-extern.internalize:
-.. _binary-extern.externalize:
+.. _binary-any.convert_extern:
+.. _binary-extern.convert_any:
 
 .. math::
    \begin{array}{llclll}
@@ -166,8 +167,8 @@ Generic :ref:`reference instructions <syntax-instr-ref>` are represented by sing
      \hex{FB}~~21{:}\Bu32~~\X{ht}{:}\Bheaptype &\Rightarrow& \REFTEST~(\REF~\NULL~\X{ht}) \\ &&|&
      \hex{FB}~~22{:}\Bu32~~\X{ht}{:}\Bheaptype &\Rightarrow& \REFCAST~(\REF~\X{ht}) \\ &&|&
      \hex{FB}~~23{:}\Bu32~~\X{ht}{:}\Bheaptype &\Rightarrow& \REFCAST~(\REF~\NULL~\X{ht}) \\ &&|&
-     \hex{FB}~~26{:}\Bu32 &\Rightarrow& \EXTERNINTERNALIZE \\ &&|&
-     \hex{FB}~~27{:}\Bu32 &\Rightarrow& \EXTERNEXTERNALIZE \\ &&|&
+     \hex{FB}~~26{:}\Bu32 &\Rightarrow& \ANYCONVERTEXTERN \\ &&|&
+     \hex{FB}~~27{:}\Bu32 &\Rightarrow& \EXTERNCONVERTANY \\ &&|&
      \hex{FB}~~28{:}\Bu32 &\Rightarrow& \REFI31 \\ &&|&
      \hex{FB}~~29{:}\Bu32 &\Rightarrow& \I31GETS \\ &&|&
      \hex{FB}~~30{:}\Bu32 &\Rightarrow& \I31GETU \\

document/core/binary/modules.rst

@@ -341,7 +341,7 @@ It decodes into a vector of :ref:`element segments <syntax-elem>` that represent
    \production{element segment} & \Belem &::=&
      0{:}\Bu32~~e{:}\Bexpr~~y^\ast{:}\Bvec(\Bfuncidx)
        &\Rightarrow& \\&&&\quad
-       \{ \ETYPE~\FUNCREF, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|&
+       \{ \ETYPE~(\REF~\NULL~\FUNC), \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|&
      1{:}\Bu32~~\X{et}:\Belemkind~~y^\ast{:}\Bvec(\Bfuncidx)
        &\Rightarrow& \\&&&\quad
        \{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EPASSIVE \} \\ &&|&
@@ -353,7 +353,7 @@ It decodes into a vector of :ref:`element segments <syntax-elem>` that represent
        \{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EDECLARATIVE \} \\ &&|&
      4{:}\Bu32~~e{:}\Bexpr~~\X{el}^\ast{:}\Bvec(\Bexpr)
        &\Rightarrow& \\&&&\quad
-       \{ \ETYPE~\FUNCREF, \EINIT~\X{el}^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|&
+       \{ \ETYPE~(\REF~\NULL~\FUNC), \EINIT~\X{el}^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|&
      5{:}\Bu32~~\X{et}:\Breftype~~\X{el}^\ast{:}\Bvec(\Bexpr)
        &\Rightarrow& \\&&&\quad
        \{ \ETYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EPASSIVE \} \\ &&|&

document/core/exec/instructions.rst

@@ -1475,43 +1475,57 @@ Where:
    \end{array}
 
 
-.. _exec-extern.externalize:
+.. _exec-any.convert_extern:
 
-:math:`\EXTERNEXTERNALIZE`
-..........................
+:math:`\ANYCONVERTEXTERN`
+.........................
 
-1. Assert: due to :ref:`validation <valid-extern.externalize>`, a :ref:`reference value <syntax-ref>` is on the top of the stack.
+1. Assert: due to :ref:`validation <valid-any.convert_extern>`, a :ref:`reference value <syntax-ref>` is on the top of the stack.
 
 2. Pop the value :math:`\reff` from the stack.
 
-3. Let :math:`\reff'` be the reference value :math:`(\REFEXTERN~\reff)`.
+3. If :math:`\reff` is :math:`\REFNULL~\X{ht}`, then:
+
+   a. Push the reference value :math:`(\REFNULL~\ANY)` to the stack.
+
+4. Else:
+
+   a. Assert: due to :ref:`validation <valid-any.convert_extern>`, a :math:`\reff` is an :ref:`external reference <syntax-ref.extern>`.
 
-5. Push the reference value :math:`\reff'` to the stack.
+   b. Let :math:`\REFEXTERN~\reff'` be the reference value :math:`\reff`.
+
+   c. Push the reference value :math:`\reff'` to the stack.
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
-   \reff~\EXTERNEXTERNALIZE &\stepto& (\REFEXTERN~\reff)
+   (\REFNULL \X{ht})~\ANYCONVERTEXTERN &\stepto& (\REFNULL~\ANY) \\
+   (\REFEXTERN~\reff)~\ANYCONVERTEXTERN &\stepto& \reff \\
    \end{array}
 
 
-.. _exec-extern.internalize:
+.. _exec-extern.convert_any:
 
-:math:`\EXTERNINTERNALIZE`
-..........................
+:math:`\EXTERNCONVERTANY`
+.........................
 
-1. Assert: due to :ref:`validation <valid-extern.internalize>`, a :ref:`reference value <syntax-ref>` is on the top of the stack.
+1. Assert: due to :ref:`validation <valid-extern.convert_any>`, a :ref:`reference value <syntax-ref>` is on the top of the stack.
 
 2. Pop the value :math:`\reff` from the stack.
 
-3. Assert: due to :ref:`validation <valid-extern.internalize>`, a :math:`\reff` is an :ref:`external reference <syntax-ref.extern>`.
+3. If :math:`\reff` is :math:`\REFNULL~\X{ht}`, then:
+
+   a. Push the reference value :math:`(\REFNULL~\EXTERN)` to the stack.
+
+4. Else:
 
-4. Let :math:`\REFEXTERN~\reff'` be the reference value :math:`\reff`.
+   a. Let :math:`\reff'` be the reference value :math:`(\REFEXTERN~\reff)`.
 
-5. Push the reference value :math:`\reff'` to the stack.
+   b. Push the reference value :math:`\reff'` to the stack.
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
-   (\REFEXTERN~\reff)~\EXTERNINTERNALIZE &\stepto& \reff
+   (\REFNULL \X{ht})~\EXTERNCONVERTANY &\stepto& (\REFNULL~\EXTERN) \\
+   \reff~\EXTERNCONVERTANY &\stepto& (\REFEXTERN~\reff) & (\iff \reff \neq (\REFNULL \X{ht})) \\
    \end{array}
 
 
@@ -4125,7 +4139,7 @@ Control Instructions
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
-   S; \reff~(\BRONCAST~l~\X{rt}_1~X{rt}_2) &\stepto& (\BR~l)
+   S; \reff~(\BRONCAST~l~\X{rt}_1~X{rt}_2) &\stepto& \reff~(\BR~l)
      & (\iff S \vdashval \reff : \X{rt}
         \land \vdashreftypematch \X{rt} \matchesreftype \insttype_{F.\AMODULE}(\X{rt}_2)) \\
    S; \reff~(\BRONCAST~l~\X{rt}_1~\X{rt}_2) &\stepto& \reff
@@ -4163,7 +4177,7 @@ Control Instructions
    S; \reff~(\BRONCASTFAIL~l~\X{rt}_1~X{rt}_2) &\stepto& \reff
      & (\iff S \vdashval \reff : \X{rt}
         \land \vdashreftypematch \X{rt} \matchesreftype \insttype_{F.\AMODULE}(\X{rt}_2)) \\
-   S; \reff~(\BRONCASTFAIL~l~\X{rt}_1~\X{rt}_2) &\stepto& (\BR~l)
+   S; \reff~(\BRONCASTFAIL~l~\X{rt}_1~\X{rt}_2) &\stepto& \reff~(\BR~l)
      & (\otherwise) \\
    \end{array}
 

document/core/exec/modules.rst

@@ -715,6 +715,10 @@ Once the function has returned, the following steps are executed:
 
 2. Pop :math:`\val_{\F{res}}^m` from the stack.
 
+3. Assert: due to :ref:`validation <valid-module>`, the frame :math:`F` is now on the top of the stack.
+
+4. Pop the frame :math:`F` from the stack.
+
 The values :math:`\val_{\F{res}}^m` are returned as the results of the invocation.
 
 .. math::

document/core/syntax/instructions.rst

@@ -485,8 +485,8 @@ while the latter performs a downcast and :ref:`traps <trap>` if the operand's ty
 .. _syntax-ref.i31:
 .. _syntax-i31.get_s:
 .. _syntax-i31.get_u:
-.. _syntax-extern.internalize:
-.. _syntax-extern.externalize:
+.. _syntax-any.convert_extern:
+.. _syntax-extern.convert_any:
 .. _syntax-instr-struct:
 .. _syntax-instr-array:
 .. _syntax-instr-i31:
@@ -521,8 +521,8 @@ Instructions in this group are concerned with creating and accessing :ref:`refer
      \ARRAYINITELEM~\typeidx~\elemidx \\&&|&
      \REFI31 \\&&|&
      \I31GET\K{\_}\sx \\&&|&
-     \EXTERNINTERNALIZE \\&&|&
-     \EXTERNEXTERNALIZE \\
+     \ANYCONVERTEXTERN \\&&|&
+     \EXTERNCONVERTANY \\
    \end{array}
 
 The instructions |STRUCTNEW| and |STRUCTNEWDEFAULT| allocate a new :ref:`structure <syntax-structtype>`, initializing them either with operands or with default values.
@@ -539,7 +539,7 @@ again allowing for different sign extension modes in the case of a :ref:`packed
 
 The instructions |REFI31| and :math:`\I31GET\K{\_}\sx` convert between type |I31| and an unboxed :ref:`scalar <syntax-i31>`.
 
-The instructions |EXTERNINTERNALIZE| and |EXTERNEXTERNALIZE| allow lossless conversion between references represented as type :math:`(\REF~\NULL~\EXTERN)`| and as :math:`(\REF~\NULL~\ANY)`.
+The instructions |ANYCONVERTEXTERN| and |EXTERNCONVERTANY| allow lossless conversion between references represented as type :math:`(\REF~\NULL~\EXTERN)`| and as :math:`(\REF~\NULL~\ANY)`.
 
 .. index:: ! parametric instruction, value type
    pair: abstract syntax; instruction

document/core/syntax/types.rst

@@ -93,7 +93,7 @@ There are three disjoint hierarchies of heap types:
 - *aggregate types* classify dynamically allocated *managed* data, such as *structures*, *arrays*, or *unboxed scalars*,
 - *external types* classify *external* references possibly owned by the :ref:`embedder <embedder>`.
 
-The values from the latter two hierarchies are interconvertible by ways of the |EXTERNINTERNALIZE| and |EXTERNEXTERNALIZE| instructions.
+The values from the latter two hierarchies are interconvertible by ways of the |EXTERNCONVERTANY| and |ANYCONVERTEXTERN| instructions.
 That is, both type hierarchies are inhabited by an isomorphic set of values, but may have different, incompatible representations in practice.
 
 .. math::
@@ -168,6 +168,29 @@ Other references are *non-null*.
 Reference types are *opaque*, meaning that neither their size nor their bit pattern can be observed.
 Values of reference type can be stored in :ref:`tables <syntax-table>`.
 
+Conventions
+...........
+
+* The reference type |ANYREF| is an abbreviation for :math:`\REF~\NULL~\ANY`.
+
+* The reference type |EQREF| is an abbreviation for :math:`\REF~\NULL~\EQT`.
+
+* The reference type |I31REF| is an abbreviation for :math:`\REF~\NULL~\I31`.
+
+* The reference type |STRUCTREF| is an abbreviation for :math:`\REF~\NULL~\STRUCT`.
+
+* The reference type |ARRAYREF| is an abbreviation for :math:`\REF~\NULL~\ARRAY`.
+
+* The reference type |FUNCREF| is an abbreviation for :math:`\REF~\NULL~\FUNC`.
+
+* The reference type |EXTERNREF| is an abbreviation for :math:`\REF~\NULL~\EXTERN`.
+
+* The reference type |NULLREF| is an abbreviation for :math:`\REF~\NULL~\NONE`.
+
+* The reference type |NULLFUNCREF| is an abbreviation for :math:`\REF~\NULL~\NOFUNC`.
+
+* The reference type |NULLEXTERNREF| is an abbreviation for :math:`\REF~\NULL~\NOEXTERN`.
+
 
 .. index:: ! value type, number type, vector type, reference type
    pair: abstract syntax; value type

document/core/text/instructions.rst

@@ -204,8 +204,8 @@ Reference Instructions
 .. _text-i31.get_u:
 .. _text-ref.test:
 .. _text-ref.cast:
-.. _text-extern.internalize:
-.. _text-extern.externalize:
+.. _text-any.convert_extern:
+.. _text-extern.convert_any:
 
 .. math::
    \begin{array}{llclll}
@@ -240,8 +240,8 @@ Reference Instructions
      \text{ref.i31} &\Rightarrow& \REFI31 \\ &&|&
      \text{i31.get\_u} &\Rightarrow& \I31GETU \\ &&|&
      \text{i31.get\_s} &\Rightarrow& \I31GETS \\ &&|&
-     \text{extern.internalize} &\Rightarrow& \EXTERNINTERNALIZE \\ &&|&
-     \text{extern.externalize} &\Rightarrow& \EXTERNEXTERNALIZE \\
+     \text{any.convert_extern} &\Rightarrow& \ANYCONVERTEXTERN \\ &&|&
+     \text{extern.convert_any} &\Rightarrow& \EXTERNCONVERTANY \\
    \end{array}