Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Use open instead of final in the text format #413

Closed
wants to merge 2 commits into from
Closed

Use open instead of final in the text format #413

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
5d13b53
Update text format spec to use `open` instead of `final`
bvisness Jul 28, 2023
21f85de
Update interpreter and tests to use `open`
bvisness Jul 28, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 13 additions & 10 deletions document/core/text/types.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,8 +85,8 @@ Abbreviations
There are shorthands for references to abstract heap types.

.. math::
\begin{array}{llclll}
\production{reference type} &
\begin{array}{lcl}
\production{reference type}
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is also unrelated to my work, but this table was jank, and now it is not.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, the production name needs its own column, in case its used. The correct fix here is to add &'s below, i.e., change each \\ to \\& (perhaps except the last). You can simplify the column scheme to {llcl}.

\text{anyref} &\equiv& \text{(}~\text{ref}~~\text{null}~~\text{any}~\text{)} \\
\text{eqref} &\equiv& \text{(}~\text{ref}~~\text{null}~~\text{eq}~\text{)} \\
\text{i31ref} &\equiv& \text{(}~\text{ref}~~\text{null}~~\text{i31}~\text{)} \\
Expand Down Expand Up @@ -255,30 +255,33 @@ 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{)}
\text{(}~\text{sub}~~\text{open}^?~~x^\ast{:\,}\Tvec(\Ttypeidx_I)~~\X{ct}{:}\Tcomptype_I~\text{)}
&\Rightarrow& \TSUB~\TFINAL^?~x^\ast~\X{ct} \\
\end{array}

.. note::
A subtype is :ref:`final <syntax-subtype>` if the :math:`\text{open}` keyword is not present, and vice versa.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

See above, this comment shouldn't be needed if the text format is consistent with the AST.



Abbreviations
.............

Singular recursive types can omit the |Trec| keyword:
Singular recursive types can omit the :math:`\text{rec}` keyword:
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why this change?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Because it refers to a keyword of the text format, not a structural element of a wasm module. The primary difference is in how they render, but suppose the structural element were named "recgrp" instead of "rec" - if that were the case, the sentence would make no sense, as recgrp is not a text format keyword.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It may be useful to note that macros.def does not define Trec, so I think it is parsing as |TREC|, which does link to the abstract syntax rather than the textual keyword.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, good points.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done as a standalone fix in #426.


.. math::
\begin{array}{llclll}
\begin{array}{lcl}
\production{recursive type} &
\Tsubtype &\equiv&
\text{(}~~\text{rec}~~\Tsubtype~~\text{)} \\
\Tdeftype &\equiv&
\text{(}~~\text{rec}~~\Tdeftype~~\text{)} \\
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is not related to my work, but I believe it to be a bug in the spec that is easy to fix.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No, I think this was correct before.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't see how it could be correct before. According to the grammar above, recursion groups contain deftypes ((rec vec(deftype))), and deftypes contain subtypes ((type subtype)). The production subtype = (rec subtype) therefore doesn't make sense, as it implies that it expands to something like (rec (sub (struct))), which violates the main grammar.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@bvisness's fix here looks right to me. We don't want to allow (sub (struct)), a subtype, to appear on its own, but we do want to allow (type (sub (struct))), a deftype, to appear on its own.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, you are right, I was confused by the impedance mismatch with the abstract syntax, where deftype is something else. We should probably not be naming this one in the text format deftype, but rather something else (typedef?).

\end{array}

Similarly, final sub types with no super-types can omit the |Tsub| keyword and arguments:
Similarly, final sub types with no super-types can omit the :math:`\text{sub}` keyword:

.. math::
\begin{array}{llclll}
\begin{array}{lcl}
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this needs to be at least llcl, otherwise Latex will barf.

\production{sub type} &
\Tcomptype &\equiv&
\text{(}~~\text{sub}~~\text{final}~~\epsilon~~\Tcomptype~~\text{)} \\
\text{(}~~\text{sub}~~\Tcomptype~~\text{)} \\
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's not clear to me why the epsilon was in here, but I can add it back if it was actually necessary.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It probably represented the empty vector of supertypes. I think it would make sense to put it and the "and arguments" language back.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What @tlively said, this was intentional.

\end{array}


Expand Down
4 changes: 2 additions & 2 deletions interpreter/syntax/types.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -308,8 +308,8 @@ let string_of_null = function
| Null -> "null "

let string_of_final = function
| NoFinal -> ""
| Final -> " final"
| NoFinal -> " open"
| Final -> ""

let string_of_mut s = function
| Cons -> s
Expand Down
4 changes: 2 additions & 2 deletions interpreter/text/arrange.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -78,8 +78,8 @@ let val_type t = string_of_val_type t
let storage_type t = string_of_storage_type t

let final = function
| NoFinal -> ""
| Final -> " final"
| NoFinal -> " open"
| Final -> ""

let decls kind ts = tab kind (atom val_type) ts

Expand Down
2 changes: 1 addition & 1 deletion interpreter/text/lexer.mll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -175,7 +175,7 @@ rule token = parse
| "field" -> FIELD
| "mut" -> MUT
| "sub" -> SUB
| "final" -> FINAL
| "open" -> OPEN
| "rec" -> REC

| "nop" -> NOP
Expand Down
8 changes: 4 additions & 4 deletions interpreter/text/parser.mly
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 REC
%token UNREACHABLE NOP DROP SELECT
%token BLOCK END IF THEN ELSE LOOP
%token BR BR_IF BR_TABLE
Expand Down Expand Up @@ -414,10 +414,10 @@ 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 FINAL var_list str_type RPAR
{ fun c x -> SubT (Final,
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 (NoFinal,
List.map (fun y -> VarHT (StatX y.it)) ($4 c type_), $5 c x) }

table_type :
Expand Down
16 changes: 8 additions & 8 deletions test/core/gc/br_on_cast.wast
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -102,14 +102,14 @@
;; Concrete Types

(module
(type $t0 (sub (struct)))
(type $t1 (sub $t0 (struct (field i32))))
(type $t1' (sub $t0 (struct (field i32))))
(type $t2 (sub $t1 (struct (field i32 i32))))
(type $t2' (sub $t1' (struct (field i32 i32))))
(type $t3 (sub $t0 (struct (field i32 i32))))
(type $t0' (sub $t0 (struct)))
(type $t4 (sub $t0' (struct (field i32 i32))))
(type $t0 (sub open (struct)))
(type $t1 (sub open $t0 (struct (field i32))))
(type $t1' (sub open $t0 (struct (field i32))))
(type $t2 (sub open $t1 (struct (field i32 i32))))
(type $t2' (sub open $t1' (struct (field i32 i32))))
(type $t3 (sub open $t0 (struct (field i32 i32))))
(type $t0' (sub open $t0 (struct)))
(type $t4 (sub open $t0' (struct (field i32 i32))))

(table 20 structref)

Expand Down
16 changes: 8 additions & 8 deletions test/core/gc/br_on_cast_fail.wast
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -102,14 +102,14 @@
;; Concrete Types

(module
(type $t0 (sub (struct)))
(type $t1 (sub $t0 (struct (field i32))))
(type $t1' (sub $t0 (struct (field i32))))
(type $t2 (sub $t1 (struct (field i32 i32))))
(type $t2' (sub $t1' (struct (field i32 i32))))
(type $t3 (sub $t0 (struct (field i32 i32))))
(type $t0' (sub $t0 (struct)))
(type $t4 (sub $t0' (struct (field i32 i32))))
(type $t0 (sub open (struct)))
(type $t1 (sub open $t0 (struct (field i32))))
(type $t1' (sub open $t0 (struct (field i32))))
(type $t2 (sub open $t1 (struct (field i32 i32))))
(type $t2' (sub open $t1' (struct (field i32 i32))))
(type $t3 (sub open $t0 (struct (field i32 i32))))
(type $t0' (sub open $t0 (struct)))
(type $t4 (sub open $t0' (struct (field i32 i32))))

(table 20 structref)

Expand Down
16 changes: 8 additions & 8 deletions test/core/gc/ref_cast.wast
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,14 +97,14 @@
;; Concrete Types

(module
(type $t0 (sub (struct)))
(type $t1 (sub $t0 (struct (field i32))))
(type $t1' (sub $t0 (struct (field i32))))
(type $t2 (sub $t1 (struct (field i32 i32))))
(type $t2' (sub $t1' (struct (field i32 i32))))
(type $t3 (sub $t0 (struct (field i32 i32))))
(type $t0' (sub $t0 (struct)))
(type $t4 (sub $t0' (struct (field i32 i32))))
(type $t0 (sub open (struct)))
(type $t1 (sub open $t0 (struct (field i32))))
(type $t1' (sub open $t0 (struct (field i32))))
(type $t2 (sub open $t1 (struct (field i32 i32))))
(type $t2' (sub open $t1' (struct (field i32 i32))))
(type $t3 (sub open $t0 (struct (field i32 i32))))
(type $t0' (sub open $t0 (struct)))
(type $t4 (sub open $t0' (struct (field i32 i32))))

(table 20 (ref null struct))

Expand Down
4 changes: 2 additions & 2 deletions test/core/gc/ref_eq.wast
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
(module
(type $st (sub (struct)))
(type $st' (sub (struct (field i32))))
(type $st (sub open (struct)))
(type $st' (sub open (struct (field i32))))
(type $at (array i8))
(type $st-sub1 (sub $st (struct)))
(type $st-sub2 (sub $st (struct)))
Expand Down
16 changes: 8 additions & 8 deletions test/core/gc/ref_test.wast
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -180,14 +180,14 @@
;; Concrete Types

(module
(type $t0 (sub (struct)))
(type $t1 (sub $t0 (struct (field i32))))
(type $t1' (sub $t0 (struct (field i32))))
(type $t2 (sub $t1 (struct (field i32 i32))))
(type $t2' (sub $t1' (struct (field i32 i32))))
(type $t3 (sub $t0 (struct (field i32 i32))))
(type $t0' (sub $t0 (struct)))
(type $t4 (sub $t0' (struct (field i32 i32))))
(type $t0 (sub open (struct)))
(type $t1 (sub open $t0 (struct (field i32))))
(type $t1' (sub open $t0 (struct (field i32))))
(type $t2 (sub open $t1 (struct (field i32 i32))))
(type $t2' (sub open $t1' (struct (field i32 i32))))
(type $t3 (sub open $t0 (struct (field i32 i32))))
(type $t0' (sub open $t0 (struct)))
(type $t4 (sub open $t0' (struct (field i32 i32))))

(table 20 (ref null struct))

Expand Down
Loading