Drop noreturn

Author: rossberg

document/core/util/macros.def

@@ -717,8 +717,6 @@
 .. |CLABELS| mathdef:: \xref{valid/conventions}{context}{\K{labels}}
 .. |CRETURN| mathdef:: \xref{valid/conventions}{context}{\K{return}}
 
-.. |NORETURN| mathdef:: \xref{valid/conventions}{context}{\K{noreturn}}
-
 
 .. Judgments
 

document/core/valid/conventions.rst

@@ -40,7 +40,7 @@ which collects relevant information about the surrounding :ref:`module <syntax-m
 * *Globals*: the list of globals declared in the current module, represented by their global type.
 * *Locals*: the list of locals declared in the current function (including parameters), represented by their value type.
 * *Labels*: the stack of labels accessible from the current position, represented by their result type.
-* *Return*: the return type of the current function, represented as a result type, or a special marker |NORETURN| indicating that no return is allowed, as in free-standing expressions.
+* *Return*: the return type of the current function, represented as an optional result type that is absent when no return is allowed, as in free-standing expressions.
 
 In other words, a context contains a sequence of suitable :ref:`types <syntax-type>` for each :ref:`index space <syntax-index>`,
 describing each defined entry in that space.
@@ -60,14 +60,13 @@ More concretely, contexts are defined as :ref:`records <notation-record>` :math:
         & \CGLOBALS & \globaltype^\ast, \\
         & \CLOCALS & \valtype^\ast, \\
         & \CLABELS & \resulttype^\ast, \\
-        & \CRETURN & (\resulttype ~|~ \NORETURN) ~\} \\
+        & \CRETURN & \resulttype^? ~\} \\
      \end{array}
    \end{array}
 
 In addition to field access written :math:`C.\K{field}` the following notation is adopted for manipulating contexts:
 
 * When spelling out a context, empty fields are omitted.
-  Likewise, the |CRETURN| field may be omitted when it is |NORETURN|.
 
 * The notation :math:`\K{field}\,A^\ast, C` denotes the same context as :math:`C` but with the elements :math:`A^\ast` prepended to its :math:`\K{field}` component sequence.
 

document/core/valid/instructions.rst

@@ -616,7 +616,7 @@ Control Instructions
 :math:`\RETURN`
 ...............
 
-* The return type :math:`C.\CRETURN` must not be |NORETURN| in the context.
+* The return type :math:`C.\CRETURN` must not be absent in the context.
 
 * Let :math:`[t^?]` be the :ref:`result type <syntax-resulttype>` of :math:`C.\CRETURN`.
 
@@ -632,7 +632,9 @@ Control Instructions
 .. note::
    The |RETURN| instruction is :ref:`stack-polymorphic <polymorphism>`.
 
-   :math:`C.\CRETURN` is |NORETURN| when validating an :ref:`expression <valid-expr>` that is not a function body.
+   :math:`C.\CRETURN` is absent (set to :math:`\epsilon`) when validating an :ref:`expression <valid-expr>` that is not a function body.
+   This differs from it being set to the empty result type (:math:`[\epsilon]`),
+   which is the case for functions not returning anything.
 
 
 .. _valid-call:

document/core/valid/modules.rst

@@ -469,9 +469,9 @@ Instead, the context :math:`C` for validation of the module's content is constru
 
   * :math:`C.\CLABELS` is empty,
 
-  * :math:`C.\CRETURN` is |NORETURN|.
+  * :math:`C.\CRETURN` is empty.
 
-* Let :math:`C'` be the :ref:`context <context>` where :math:`C'.\CGLOBALS` is the sequence :math:`\etglobals(\externtype_i^\ast)`, :math:`C.\CRETURN` is |NORETURN| and all other fields are empty.
+* Let :math:`C'` be the :ref:`context <context>` where :math:`C'.\CGLOBALS` is the sequence :math:`\etglobals(\externtype_i^\ast)` and all other fields are empty.
 
 * Under the context :math:`C`: