Add definition of defaultable types (WebAssembly#62)

No rules for locals yet, since those are still being discussed.

Author: rossberg

document/core/exec/runtime.rst

@@ -58,7 +58,7 @@ it is the respective value :math:`0` for :ref:`number types <syntax-numtype>`, :
    \begin{array}{lcl@{\qquad}l}
    \default_t &=& t{.}\CONST~0 & (\iff t = \numtype) \\
    \default_t &=& t{.}\CONST~0 & (\iff t = \vectype) \\
-   \default_t &=& \REFNULL~t & (\iff t = \reftype) \\
+   \default_t &=& \REFNULL~t & (\iff t = (\REF~\NULL~\heaptype)) \\
    \end{array}
 
 

document/core/syntax/types.rst

@@ -99,6 +99,7 @@ A *concrete* heap type consists of a :ref:`type index <syntax-typeidx>` and clas
    pair: abstract syntax; reference type
    pair: reference; type
 .. _syntax-reftype:
+.. _syntax-nullable:
 
 Reference Types
 ~~~~~~~~~~~~~~~

document/core/util/macros.def

@@ -878,6 +878,7 @@
 .. Notation
 
 .. |ok| mathdef:: \mathrel{\mbox{ok}}
+.. |defaultable| mathdef:: \xref{valid/types}{valid-defaultable}{\mathrel{\mbox{defaultable}}}
 .. |const| mathdef:: \xref{valid/instructions}{valid-constant}{\mathrel{\mbox{const}}}
 
 .. |matchesnumtype| mathdef:: \xref{valid/matching}{match-numtype}{\leq}
@@ -924,6 +925,9 @@
 .. |vdashglobaltype| mathdef:: \xref{valid/types}{valid-globaltype}{\vdash}
 .. |vdashexterntype| mathdef:: \xref{valid/types}{valid-externtype}{\vdash}
 
+.. |vdashvaltypedefaultable| mathdef:: \xref{valid/types}{valid-defaultable}{\vdash}
+.. |vdashtabletypedefaultable| mathdef:: \xref{valid/types}{valid-defaultable}{\vdash}
+
 .. |vdashnumtypematch| mathdef:: \xref{valid/matching}{match-numtype}{\vdash}
 .. |vdashheaptypematch| mathdef:: \xref{valid/matching}{match-heaptype}{\vdash}
 .. |vdashreftypematch| mathdef:: \xref{valid/matching}{match-reftype}{\vdash}

document/core/valid/modules.rst

@@ -48,7 +48,7 @@ Functions :math:`\func` are classified by :ref:`function types <syntax-functype>
    }
 
 
-.. index:: table, table type
+.. index:: table, table type, defaultable
    pair: validation; table
    single: abstract syntax; table
 .. _valid-table:
@@ -68,6 +68,8 @@ Tables :math:`\table` are classified by :ref:`table types <syntax-tabletype>`.
 .. math::
    \frac{
      C \vdashtabletype \tabletype \ok
+     \qquad
+     C \vdashtabletypedefaultable \tabletype \defaultable
    }{
      C \vdashtable \{ \TTYPE~\tabletype \} : \tabletype
    }

document/core/valid/types.rst

@@ -397,3 +397,58 @@ External Types
    }{
      C \vdashexterntype \ETGLOBAL~\globaltype \ok
    }
+
+
+.. index:: value type, ! defaultable, number type, vector type, reference type, table type
+.. _valid-defaultable:
+
+Defaultable Types
+~~~~~~~~~~~~~~~~~
+
+A type is *defaultable* if it has a :ref:`default value <default-val>` for initialization.
+
+Value Types
+...........
+
+* A defaultable :ref:`value type <syntax-valtype>` :math:`t` must be:
+
+  - either a :ref:`number type <syntax-numtype>`,
+
+  - or a :ref:`vector type <syntax-vectype>`,
+
+  - or a :ref:`nullable reference type <syntax-numtype>`.
+
+
+.. math::
+   \frac{
+   }{
+     C \vdashvaltypedefaultable \numtype \defaultable
+   }
+
+.. math::
+   \frac{
+   }{
+     C \vdashvaltypedefaultable \vectype \defaultable
+   }
+
+.. math::
+   \frac{
+   }{
+     C \vdashvaltypedefaultable (\REF~\NULL~\heaptype) \defaultable
+   }
+
+
+Table Types
+...........
+
+* A defaultable :ref:`table type <syntax-tabletype>` must be:
+
+  - of the form :math:`\limits~t`, where `t` is a :ref:`defaultable <valid-defaultable>` :ref:`reference type <syntax-numtype>`.
+
+
+.. math::
+   \frac{
+     C \vdashvaltypedefaultable \reftype \defaultable
+   }{
+     C \vdashtabletypedefaultable \limits~\reftype \defaultable
+   }