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

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)

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}`

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

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>`.

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}
 
 

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}}

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}
 
 

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
  }{

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::

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

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

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

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])

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
 

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) }

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)