Merge reference-types/master

Update to reference-types/master

Author: aheejin

.travis.yml

@@ -6,15 +6,21 @@ dist: bionic
 addons:
   apt:
     sources:
+      - sourceline: 'ppa:avsm/ppa'
       - sourceline: 'deb https://dl.yarnpkg.com/debian/ stable main'
         key_url: 'https://dl.yarnpkg.com/debian/pubkey.gpg'
+    update: true
     packages:
-      - ocaml
-      - ocamlbuild
+      - opam
       - texlive-full
       - yarn
 
 install:
+  - opam init --auto-setup --compiler=4.07.1
+  - eval $(opam env)
+  - opam --version
+  - ocaml --version
+  - opam install --yes ocamlbuild.0.14.0
   - pip install Sphinx==2.4.4
   - git clone https://github.com/tabatkins/bikeshed.git
   - pip install --editable $PWD/bikeshed

README.md

@@ -22,15 +22,18 @@ specification language.
 It also holds the WebAssembly testsuite, which tests numerous aspects of
 conformance to the spec.
 
-View the work-in-progress spec at
-[webassembly.github.io/spec](https://webassembly.github.io/spec/).
+View the work-in-progress spec at [webassembly.github.io/spec](https://webassembly.github.io/spec/).
 
 At this time, the contents of this repository are under development and known
 to be "incomplet and inkorrect".
 
 Participation is welcome. Discussions about new features, significant semantic
 changes, or any specification change likely to generate substantial discussion
-should take place in [the WebAssembly design
-repository](https://github.com/WebAssembly/design) first, so that this spec
-repository can remain focused. And please follow the [guidelines for
-contributing](Contributing.md).
+should take place in
+[the WebAssembly design repository](https://github.com/WebAssembly/design)
+first, so that this spec repository can remain focused. And please follow the
+[guidelines for contributing](Contributing.md).
+
+# citing
+
+For citing WebAssembly in LaTeX, use [this bibtex file](wasm-specs.bib).

document/README.md

@@ -21,3 +21,98 @@ To build everything and update [webassembly.github.io/spec](https://webassembly.
 make publish
 ```
 Please make sure to only use that once a change has approval.
+
+## Step by step guide to building the spec
+
+### Prerequisites
+
+You will need `python3.7`, and `pip`. `pip` should come with Python, if not follow [these installation instructions for `pip`](https://pip.pypa.io/en/stable/installing/), or check your system package manager for `pip3`.
+
+> Important: you will need the version of pip that works with `python3.7`.
+
+
+Use something like [`pipenv`](https://pipenv.pypa.io/) to keep your system installation of Python clean.
+
+```
+pip install pipenv
+pipenv --python 3.7
+pipenv shell
+```
+
+Install Python dependencies:
+
+```
+pip install Sphinx==2.4.4
+```
+
+### Checking out the repository
+
+Make sure this repository was cloned with `--recursive`:
+
+```
+git clone --recursive https://github.com/WebAssembly/spec
+```
+
+If you have already cloned but without `--recursive`, you can delete and re-clone, or `cd` into `spec` and run:
+
+```
+git submodule update --init --recursive
+```
+
+The rest of these instructions assume you are in the directory where is README is:
+
+```
+cd spec/document
+```
+
+### Building the multi-page HTML document
+
+You can now build the [multi-page html document](https://webassembly.github.io/spec/core/):
+
+```
+make -C core html
+```
+
+### Building the single-page HTML document
+
+To build the [single-page W3C version](https://webassembly.github.io/spec/core/bikeshed/), there are more dependencies to install. First, get [Bikeshed](https://github.com/tabatkins/bikeshed):
+
+```
+# cd back to root of git directory
+git clone https://github.com/tabatkins/bikeshed.git
+pip install --editable bikeshed
+bikeshed update
+```
+
+You will also need `npm` and `yarn` for all the LaTeX goodness. `npm` might already be available on your system, you can also use something like [`nvm`](https://github.com/nvm-sh/nvm) to prevent messing with system packages:
+
+```
+npm install -g yarn
+cd document
+make -C core bikeshed
+```
+
+### Building the PDF
+
+To build the [PDF](https://webassembly.github.io/spec/core/_download/WebAssembly.pdf), you will need `texlive-full`, install it using your system package manager:
+
+```
+apt install texlive-full
+make -C core pdf
+```
+
+### Building the JavaScript Embedding API
+
+To build the [JavaScript Embedding API](https://webassembly.github.io/spec/js-api/index.html), you will need `bikeshed` as describe in the section [Building the single-page HTML document](#building-the-single-page-html-document):
+
+```
+make -C js-api
+```
+
+### Building the Web Embedding API
+
+To build the [Web Embedding API](https://webassembly.github.io/spec/web-api/index.html), you will need `bikeshed` as describe in the section [Building the single-page HTML document](#building-the-single-page-html-document):
+
+```
+make -C web-api
+```

document/core/Makefile

@@ -89,8 +89,12 @@ bikeshed-keep:
 	  echo Downloaded Bikeshed.
 
 
+.PHONY: index
+index:
+	(cd appendix; ./gen-index-instructions.py)
+
 .PHONY: pdf
-pdf:	latexpdf
+pdf:	index latexpdf
 	mkdir -p $(BUILDDIR)/html/$(DOWNLOADDIR)
 	ln -f $(BUILDDIR)/latex/$(NAME).pdf $(BUILDDIR)/html/$(DOWNLOADDIR)/$(NAME).pdf
 
@@ -101,7 +105,7 @@ clean:
 	rm -rf $(STATICDIR)
 
 .PHONY: html
-html:
+html: index
 	$(SPHINXBUILD) -b html $(ALLSPHINXOPTS) $(BUILDDIR)/html
 	for file in `ls $(BUILDDIR)/html/*.html`; \
 	do \

document/core/appendix/algorithm.rst

@@ -27,11 +27,11 @@ Types are representable as an enumeration.
 
    type val_type = I32 | I64 | F32 | F64 | Funcref | Exnref | Externref
 
-   func is_num(t : val_type) : bool =
-     return t = I32 || t = I64 || t = F32 || t = F64
+   func is_num(t : val_type | Unknown) : bool =
+     return t = I32 || t = I64 || t = F32 || t = F64 || t = Unknown
 
-   func is_ref(t : val_type) : bool =
-     return t = Funcref || t = Exnref || t = Externref
+   func is_ref(t : val_type | Unknown) : bool =
+     return t = Funcref || t = Exnref || t = Externref || t = Unknown
 
 The algorithm uses two separate stacks: the *value stack* and the *control stack*.
 The former tracks the :ref:`types <syntax-valtype>` of operand values on the :ref:`stack <stack>`,
@@ -52,7 +52,6 @@ the latter surrounding :ref:`structured control instructions <syntax-instr-contr
 
 For each value, the value stack records its :ref:`value type <syntax-valtype>`, or :code:`Unknown` when the type is not known.
 
-
 For each entered block, the control stack records a *control frame* with the originating opcode, the types on the top of the operand stack at the start and end of the block (used to check its result as well as branches), the height of the operand stack at the start of the block (used to check that operands do not underflow the current block), and a flag recording whether the remainder of the block is unreachable (used to handle :ref:`stack-polymorphic <polymorphism>` typing after branches).
 
 For the purpose of presenting the algorithm, the operand and control stacks are simply maintained as global variables:
@@ -231,13 +230,17 @@ Other instructions are checked in a similar manner.
          push_vals(label_types(ctrls[n]))
 
        case (br_table n* m)
+         pop_val(I32)
          error_if(ctrls.size() < m)
+         let arity = label_types(ctrls[m]).size()
          foreach (n in n*)
-           error_if(ctrls.size() < n || label_types(ctrls[n]) =/= label_types(ctrls[m]))
-         pop_val(I32)
-         pop_vals(label_types(ctrls[m]))
+           error_if(ctrls.size() < n)
+           error_if(label_types(ctrls[n]).size() =/= arity)
+           push_vals(pop_vals(label_types(ctrls[n])))
+         pop_vals(label_types(ctrls[m]))
          unreachable()
 
+
 .. note::
    It is an invariant under the current WebAssembly instruction set that an operand of :code:`Unknown` type is never duplicated on the stack.
    This would change if the language were extended with stack instructions like :code:`dup`.