Add (sub open ...) and make it mandatory

tlively · tlively · commit 06cd5bb62491 · 2023-09-11T14:36:18.000-07:00
Instead of using final? in the syntax, use ext ::= open | final. Implements the design discussed in #413. Update the interpreter, the abstract syntax, the binary and text formats, and MVP.md.
diff --git a/document/core/appendix/algorithm.rst b/document/core/appendix/algorithm.rst
@@ -57,8 +57,9 @@ Similarly, :ref:`defined types <syntax-deftype>` :code:`def_type` can be represe
    type array_type = Array(fields : field_type)
    type func_type = Func(params : list(val_type), results : list(val_type))
    type comp_type = struct_type | array_type | func_type
+   type ext_type = Open | Final
 
-   type sub_type = Sub(super : list(def_type), body : comp_type, final : bool)
+   type sub_type = Sub(super : list(def_type), body : comp_type, ext : ext_type)
    type rec_type = Rec(types : list(sub_type))
 
    type def_type = Def(rec : rec_type, proj : int32)
diff --git a/document/core/appendix/index-types.rst b/document/core/appendix/index-types.rst
@@ -35,7 +35,7 @@ Category                                  Constructor
 :ref:`Composite type <syntax-comptype>`   :math:`\TSTRUCT~\fieldtype^\ast`                    :math:`\hex{5F}` (-33 as |Bs7|)
 :ref:`Composite type <syntax-comptype>`   :math:`\TARRAY~\fieldtype`                          :math:`\hex{5E}` (-34 as |Bs7|)
 (reserved)                                                                                    :math:`\hex{5D}` .. :math:`\hex{51}`
-:ref:`Sub type <syntax-subtype>`          :math:`\TSUB~\typeidx^\ast~\comptype`               :math:`\hex{50}` (-48 as |Bs7|)
+:ref:`Sub type <syntax-subtype>`          :math:`\TSUB~\TOPEN~\typeidx^\ast~\comptype`               :math:`\hex{50}` (-48 as |Bs7|)
 :ref:`Sub type <syntax-subtype>`          :math:`\TSUB~\TFINAL~\typeidx^\ast~\comptype`       :math:`\hex{4F}` (-49 as |Bs7|)
 :ref:`Recursive type <syntax-rectype>`    :math:`\TREC~\subtype^\ast`                         :math:`\hex{4E}` (-50 as |Bs7|)
 (reserved)                                                                                    :math:`\hex{4D}` .. :math:`\hex{41}`
diff --git a/document/core/binary/types.rst b/document/core/binary/types.rst
@@ -223,7 +223,7 @@ Recursive Types
 ~~~~~~~~~~~~~~~
 
 :ref:`Recursive types <syntax-rectype>` are encoded by the byte :math:`\hex{31}` followed by a :ref:`vector <binary-vec>` of :ref:`sub types <syntax-subtype>`.
-Additional shorthands are recognized for unary recursions and sub types without super types.
+Additional shorthands are recognized for unary recursions and final sub types without super types.
 
 .. math::
    \begin{array}{llclll@{\qquad\qquad}l}
@@ -234,7 +234,7 @@ Additional shorthands are recognized for unary recursions and sub types without
        &\Rightarrow& \TREC~\X{st} \\
    \production{sub type} & \Bsubtype &::=&
      \hex{50}~~x^\ast{:\,}\Bvec(\Btypeidx)~~\X{ct}{:}\Bcomptype
-       &\Rightarrow& \TSUB~x^\ast~\X{ct} \\ &&|&
+       &\Rightarrow& \TSUB~\TOPEN~x^\ast~\X{ct} \\ &&|&
      \hex{4E}~~x^\ast{:\,}\Bvec(\Btypeidx)~~\X{ct}{:}\Bcomptype
        &\Rightarrow& \TSUB~\TFINAL~x^\ast~\X{ct} \\ &&|&
      \X{ct}{:}\Bcomptype
diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst
@@ -291,25 +291,27 @@ including :ref:`function types <syntax-functype>` and :ref:`aggregate types <syn
    \end{array}
 
 
-.. index:: ! recursive type, ! sub type, composite type, ! final, subtyping, ! roll, ! unroll, recursive type index
+.. index:: ! recursive type, ! sub type, composite type, ! open, ! final, subtyping, ! roll, ! unroll, recursive type index
    pair: abstract syntax; recursive type
    pair: abstract syntax; sub type
 .. _syntax-rectype:
 .. _syntax-subtype:
+.. _syntax-ext:
 
 Recursive Types
 ~~~~~~~~~~~~~~~
 
 *Recursive types* denote a group of mutually recursive :ref:`composite types <syntax-comptype>`, each of which can optionally declare a list of :ref:`type indices <syntax-typeidx>` of supertypes that it :ref:`matches <match-comptype>`.
-Each type can also be declared *final*, preventing further subtyping.
-.
+Each type can also be declared *open*, in which case they may have further subtypes, or *final*, preventing further subtyping.
 
 .. math::
    \begin{array}{llrl}
    \production{recursive type} & \rectype &::=&
      \TREC~\subtype^\ast \\
    \production{sub types} & \subtype &::=&
-     \TSUB~\TFINAL^?~\typeidx^\ast~\comptype \\
+     \TSUB~\ext~\typeidx^\ast~\comptype \\
+   \production{extension type} & \ext &::=&
+     \TOPEN ~|~ \TFINAL \\
    \end{array}
 
 In a :ref:`module <syntax-module>`, each member of a recursive type is assigned a separate :ref:`type index <syntax-typeidx>`.
diff --git a/document/core/text/types.rst b/document/core/text/types.rst
@@ -242,6 +242,7 @@ Composite Types
 .. _text-rectype:
 .. _text-subtype:
 .. _text-deftype:
+.. _text-exttype:
 
 Recursive Types
 ~~~~~~~~~~~~~~~
@@ -255,8 +256,11 @@ Recursive Types
      \text{(}~\text{type}~~\Tid^?~~\X{st}{:}\Tsubtype_I~\text{)}
        &\Rightarrow& \X{st} \\
    \production{sub type} & \Tsubtype_I &::=&
-     \text{(}~\text{sub}~~\text{final}^?~~x^\ast{:\,}\Tvec(\Ttypeidx_I)~~\X{ct}{:}\Tcomptype_I~\text{)}
-       &\Rightarrow& \TSUB~\TFINAL^?~x^\ast~\X{ct} \\
+     \text{(}~\text{sub}~~\X{ext}{:}\Texttype~~x^\ast{:\,}\Tvec(\Ttypeidx_I)~~\X{ct}{:}\Tcomptype_I~\text{)}
+       &\Rightarrow& \TSUB~\X{ext}~x^\ast~\X{ct} \\
+   \production{extension type} & \Texttype &::=&
+     \text{open} &\Rightarrow& \TOPEN \\ &&|&
+     \text{final} &\Rightarrow& \TFINAL \\
    \end{array}
 
 
diff --git a/document/core/util/macros.def b/document/core/util/macros.def
@@ -234,6 +234,7 @@
 .. |TARRAY| mathdef:: \xref{syntax/types}{syntax-comptype}{\K{array}}
 .. |TSUB| mathdef:: \xref{syntax/types}{syntax-subtype}{\K{sub}}
 .. |TREC| mathdef:: \xref{syntax/types}{syntax-rectype}{\K{rec}}
+.. |TOPEN| mathdef:: \xref{syntax/types}{syntax-subtype}{\K{open}}
 .. |TFINAL| mathdef:: \xref{syntax/types}{syntax-subtype}{\K{final}}
 
 .. |MVAR| mathdef:: \xref{syntax/types}{syntax-mut}{\K{var}}
@@ -270,6 +271,7 @@
 .. |subtype| mathdef:: \xref{syntax/types}{syntax-subtype}{\X{subtype}}
 .. |rectype| mathdef:: \xref{syntax/types}{syntax-rectype}{\X{rectype}}
 .. |deftype| mathdef:: \xref{valid/conventions}{syntax-deftype}{\X{deftype}}
+.. |ext| mathdef:: \xref{syntax/types}{syntax-ext}{\X{ext}}
 
 .. |globaltype| mathdef:: \xref{syntax/types}{syntax-globaltype}{\X{globaltype}}
 .. |tabletype| mathdef:: \xref{syntax/types}{syntax-tabletype}{\X{tabletype}}
@@ -906,6 +908,7 @@
 .. |Tstoragetype| mathdef:: \xref{text/types}{text-storagetype}{\T{storagetype}}
 .. |Tpackedtype| mathdef:: \xref{text/types}{text-packedtype}{\T{packedtype}}
 .. |Tcomptype| mathdef:: \xref{text/types}{text-comptype}{\T{comptype}}
+.. |Texttype| mathdef:: \xref{text/types}{text-exttype}{\T{exttype}}
 .. |Tsubtype| mathdef:: \xref{text/types}{text-subtype}{\T{subtype}}
 .. |Tdeftype| mathdef:: \xref{text/types}{text-deftype}{\T{deftype}}
 .. |Trectype| mathdef:: \xref{text/types}{text-rectype}{\T{rectype}}
diff --git a/document/core/valid/conventions.rst b/document/core/valid/conventions.rst
@@ -52,7 +52,7 @@ they only occur during :ref:`validation <valid>` or :ref:`execution <exec>`.
    \production{heap type} & \heaptype &::=&
      \dots ~|~ \deftype ~|~ \REC~i \\
    \production{sub types} & \subtype &::=&
-     \TSUB~\TFINAL^?~\heaptype^\ast~\comptype \\
+     \TSUB~\ext~\heaptype^\ast~\comptype \\
    \end{array}
 
 The unique :ref:`value type <syntax-valtype>` |BOT| is a *bottom type* that :ref:`matches <match-heaptype>` all value types.
@@ -180,7 +180,7 @@ In addition, the following auxiliary function denotes the *expansion* of a :ref:
 
 .. math::
    \begin{array}{@{}llll@{}}
-   \expanddt(\deftype) &=& \comptype & (\iff \unrolldt(\deftype) = \TSUB~\TFINAL^?~\X{ht}^?~\comptype) \\
+   \expanddt(\deftype) &=& \comptype & (\iff \unrolldt(\deftype) = \TSUB~\ext~\X{ht}^?~\comptype) \\
    \end{array}
 
 
diff --git a/document/core/valid/matching.rst b/document/core/valid/matching.rst
@@ -431,7 +431,7 @@ A :ref:`defined type <syntax-deftype>` :math:`\deftype_1` matches a type :math:`
 
 * Or:
 
-  * Let the :ref:`sub type <syntax-subtype>` :math:`\TSUB~\TFINAL^?~\heaptype^\ast~\comptype` be the result of :ref:`unrolling <aux-unroll-deftype>` :math:`\deftype_1`.
+  * Let the :ref:`sub type <syntax-subtype>` :math:`\TSUB~\ext~\heaptype^\ast~\comptype` be the result of :ref:`unrolling <aux-unroll-deftype>` :math:`\deftype_1`.
 
   * Then there must exist a :ref:`heap type <syntax-heaptype>` :math:`\heaptype_i` in :math:`\heaptype^\ast` that :ref:`matches <match-heaptype>` :math:`\deftype_2`.
 
@@ -446,7 +446,7 @@ A :ref:`defined type <syntax-deftype>` :math:`\deftype_1` matches a type :math:`
 .. math::
    ~\\[-1ex]
    \frac{
-     \unrolldt(\deftype_1) = \TSUB~\TFINAL^?~\heaptype^\ast~\comptype
+     \unrolldt(\deftype_1) = \TSUB~\ext~\heaptype^\ast~\comptype
      \qquad
      C \vdashheaptypematch \heaptype^\ast[i] \matchesheaptype \deftype_2
    }{
diff --git a/document/core/valid/types.rst b/document/core/valid/types.rst
@@ -405,7 +405,7 @@ Recursive Types
      C \vdashrectype \TREC~\subtype~{\subtype'}^\ast ~{\ok}(x)
    }
 
-:math:`\TSUB~\TFINAL^?~y^\ast~\comptype`
+:math:`\TSUB~\ext~y^\ast~\comptype`
 ........................................
 
 * The :ref:`composite type <syntax-comptype>` :math:`\comptype` must be :ref:`valid <valid-comptype>`.
@@ -420,7 +420,7 @@ Recursive Types
 
   * Let :math:`\subtype_i` be the :ref:`unrolling <aux-unroll-deftype>` of the :ref:`defined type <syntax-deftype>` :math:`C.\CTYPES[y_i]`.
 
-  * The :ref:`sub type <syntax-subtype>` :math:`\subtype_i` must not contain :math:`\TFINAL`.
+  * The :ref:`sub type <syntax-subtype>` :math:`\subtype_i` must contain :math:`\TOPEN`.
 
   * Let :math:`\comptype'_i` be the :ref:`expansion <aux-expand-deftype>` of the :ref:`defined type <syntax-deftype>` :math:`C.\CTYPES[y_i]`.
 
@@ -435,14 +435,14 @@ Recursive Types
      \qquad
      (y < x)^\ast
      \qquad
-     (\unrolldt(C.\CTYPES[y]) = \TSUB~{y'}^\ast~\comptype')^\ast
+     (\unrolldt(C.\CTYPES[y]) = \TSUB~\TOPEN~{y'}^\ast~\comptype')^\ast
      \\
      C \vdashcomptype \comptype \ok
      \qquad
      (C \vdashcomptypematch \comptype \matchescomptype \comptype')^\ast
      \end{array}
    }{
-     C \vdashsubtype \TSUB~\TFINAL^?~y^\ast~\comptype ~{\ok}(x)
+     C \vdashsubtype \TSUB~\ext~y^\ast~\comptype ~{\ok}(x)
    }
 
 .. note::
diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml
@@ -258,7 +258,7 @@ let sub_type s =
   | Some i when i = -0x30 land 0x7f ->
     skip 1 s;
     let xs = vec (var_type u32) s in
-    SubT (NoFinal, List.map (fun x -> VarHT x) xs, str_type s)
+    SubT (Open, List.map (fun x -> VarHT x) xs, str_type s)
   | Some i when i = -0x31 land 0x7f ->
     skip 1 s;
     let xs = vec (var_type u32) s in
diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml
@@ -181,7 +181,7 @@ struct
   let sub_type = function
     | SubT (Final, [], st) -> str_type st
     | SubT (Final, hts, st) -> s7 (-0x31); vec var_heap_type hts; str_type st
-    | SubT (NoFinal, hts, st) -> s7 (-0x30); vec var_heap_type hts; str_type st
+    | SubT (Open, hts, st) -> s7 (-0x30); vec var_heap_type hts; str_type st
 
   let rec_type = function
     | RecT [st] -> sub_type st
diff --git a/interpreter/syntax/types.ml b/interpreter/syntax/types.ml
@@ -7,7 +7,7 @@ type name = Utf8.unicode
 type null = NoNull | Null
 type mut = Cons | Var
 type init = Set | Unset
-type final = NoFinal | Final
+type ext = Open | Final
 type 'a limits = {min : 'a; max : 'a option}
 
 type var = StatX of type_idx | RecX of int32
@@ -39,7 +39,7 @@ and str_type =
   | DefArrayT of array_type
   | DefFuncT of func_type
 
-and sub_type = SubT of final * heap_type list * str_type
+and sub_type = SubT of ext * heap_type list * str_type
 and rec_type = RecT of sub_type list
 and def_type = DefT of rec_type * int32
 
@@ -307,9 +307,9 @@ let string_of_null = function
   | NoNull -> ""
   | Null -> "null "
 
-let string_of_final = function
-  | NoFinal -> ""
-  | Final -> " final"
+let string_of_ext = function
+  | Open -> "open"
+  | Final -> "final"
 
 let string_of_mut s = function
   | Cons -> s
@@ -379,9 +379,9 @@ and string_of_str_type = function
 
 and string_of_sub_type = function
   | SubT (Final, [], st) -> string_of_str_type st
-  | SubT (fin, hts, st) ->
+  | SubT (ext, hts, st) ->
     String.concat " "
-      (("sub" ^ string_of_final fin) :: List.map string_of_heap_type hts) ^
+      (("sub " ^ string_of_ext ext) :: List.map string_of_heap_type hts) ^
     " (" ^ string_of_str_type st ^ ")"
 
 and string_of_rec_type = function
diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml
@@ -77,9 +77,9 @@ let heap_type t = string_of_heap_type t
 let val_type t = string_of_val_type t
 let storage_type t = string_of_storage_type t
 
-let final = function
-  | NoFinal -> ""
-  | Final -> " final"
+let extendability = function
+  | Open -> "open"
+  | Final -> "final"
 
 let decls kind ts = tab kind (atom val_type) ts
 
@@ -103,9 +103,9 @@ let str_type st =
 
 let sub_type = function
   | SubT (Final, [], st) -> str_type st
-  | SubT (fin, xs, st) ->
+  | SubT (ext, xs, st) ->
     Node (String.concat " "
-      (("sub" ^ final fin ):: List.map heap_type xs), [str_type st])
+      (("sub " ^ extendability ext):: List.map heap_type xs), [str_type st])
 
 let rec_type i j st =
   Node ("type $" ^ nat (i + j), [sub_type st])
diff --git a/interpreter/text/lexer.mll b/interpreter/text/lexer.mll
@@ -82,7 +82,7 @@ let character =
     [^'"''\\''\x00'-'\x1f''\x7f'-'\xff']
   | utf8enc
   | '\\'escape
-  | '\\'hexdigit hexdigit 
+  | '\\'hexdigit hexdigit
   | "\\u{" hexnum '}'
 
 let nat = num | "0x" hexnum
@@ -175,6 +175,7 @@ rule token = parse
       | "field" -> FIELD
       | "mut" -> MUT
       | "sub" -> SUB
+      | "open" -> OPEN
       | "final" -> FINAL
       | "rec" -> REC
 
diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly
@@ -257,7 +257,7 @@ let inline_func_type_explicit (c : context) x ft at =
 %token ANYREF NULLREF EQREF I31REF STRUCTREF ARRAYREF
 %token FUNCREF NULLFUNCREF EXTERNREF NULLEXTERNREF
 %token ANY NONE EQ I31 REF NOFUNC EXTERN NOEXTERN NULL
-%token MUT FIELD STRUCT ARRAY SUB FINAL REC
+%token MUT FIELD STRUCT ARRAY SUB OPEN FINAL REC
 %token UNREACHABLE NOP DROP SELECT
 %token BLOCK END IF THEN ELSE LOOP
 %token BR BR_IF BR_TABLE
@@ -413,9 +413,9 @@ str_type :
 
 sub_type :
   | str_type { fun c x -> SubT (Final, [], $1 c x) }
-  | LPAR SUB var_list str_type RPAR
-    { fun c x -> SubT (NoFinal,
-        List.map (fun y -> VarHT (StatX y.it)) ($3 c type_), $4 c x) }
+  | LPAR SUB OPEN var_list str_type RPAR
+    { fun c x -> SubT (Open,
+        List.map (fun y -> VarHT (StatX y.it)) ($4 c type_), $5 c x) }
   | LPAR SUB FINAL var_list str_type RPAR
     { fun c x -> SubT (Final,
         List.map (fun y -> VarHT (StatX y.it)) ($4 c type_), $5 c x) }
diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml
@@ -174,13 +174,13 @@ let check_sub_type (c : context) (sut : sub_type) at =
   check_str_type c st at
 
 let check_sub_type_sub (c : context) (sut : sub_type) x at =
-  let SubT (_fin, hts, st) = sut in
+  let SubT (_ext, hts, st) = sut in
   List.iter (fun hti ->
     let xi = match hti with VarHT (StatX xi) -> xi | _ -> assert false in
-    let SubT (fini, _, sti) = unroll_def_type (type_ c (xi @@ at)) in
+    let SubT (ext, _, sti) = unroll_def_type (type_ c (xi @@ at)) in
     require (xi < x) at ("forward use of type " ^ I32.to_string_u xi ^
       " in sub type definition");
-    require (fini = NoFinal) at ("sub type " ^ I32.to_string_u x ^
+    require (ext = Open) at ("sub type " ^ I32.to_string_u x ^
       " has final super type " ^ I32.to_string_u xi);
     require (match_str_type c.types st sti) at ("sub type " ^ I32.to_string_u x ^
       " does not match super type " ^ I32.to_string_u xi)
diff --git a/proposals/gc/MVP.md b/proposals/gc/MVP.md
diff --git a/test/core/gc/br_on_cast.wast b/test/core/gc/br_on_cast.wast
diff --git a/test/core/gc/br_on_cast_fail.wast b/test/core/gc/br_on_cast_fail.wast
diff --git a/test/core/gc/ref_cast.wast b/test/core/gc/ref_cast.wast
diff --git a/test/core/gc/ref_eq.wast b/test/core/gc/ref_eq.wast
diff --git a/test/core/gc/ref_test.wast b/test/core/gc/ref_test.wast
diff --git a/test/core/gc/type-subtyping.wast b/test/core/gc/type-subtyping.wast
