Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit 8086956

Browse files
pl-semioticspl-semiotics
committedJan 10, 2023
Add draft of the specification of validation
1 parent 006b97c commit 8086956

25 files changed

+5455
-0
lines changed
 

Diff for: ‎.gitignore

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
docs/

Diff for: ‎LICENSE

+1
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ to that directory and its relative sub-directories.
44
The relevant directories and licenses are:
55

66
design/ - Apache License 2.0
7+
spec/document/ - W3C Software and Document Notice and License
78

89
(Other directories will be added when the [module-linking] repository merges.)
910

Diff for: ‎spec/document/.gitignore

+2
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
_build/
2+
util/__pycache__

Diff for: ‎spec/document/LICENSE

+50
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
W3C SOFTWARE AND DOCUMENT NOTICE AND LICENSE
2+
3+
This work is being provided by the copyright holders under the following
4+
license.
5+
6+
7+
LICENSE
8+
9+
By obtaining and/or copying this work, you (the licensee) agree that you have
10+
read, understood, and will comply with the following terms and conditions.
11+
12+
Permission to copy, modify, and distribute this work, with or without
13+
modification, for any purpose and without fee or royalty is hereby granted,
14+
provided that you include the following on ALL copies of the work or portions
15+
thereof, including modifications:
16+
17+
* The full text of this NOTICE in a location viewable to users of the
18+
redistributed or derivative work.
19+
20+
* Any pre-existing intellectual property disclaimers, notices, or terms and
21+
conditions. If none exist, the W3C Software and Document Short Notice
22+
(https://www.w3.org/Consortium/Legal/copyright-software-short-notice) should
23+
be included.
24+
25+
* Notice of any changes or modifications, through a copyright statement on the
26+
new code or document such as "This software or document includes material
27+
copied from or derived from [title and URI of the W3C document]. Copyright © [YEAR] W3C® (MIT, ERCIM, Keio, Beihang)."
28+
29+
30+
DISCLAIMERS
31+
32+
THIS WORK IS PROVIDED "AS IS," AND COPYRIGHT HOLDERS MAKE NO REPRESENTATIONS
33+
OR WARRANTIES, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO, WARRANTIES OF
34+
MERCHANTABILITY OR FITNESS FOR ANY PARTICULAR PURPOSE OR THAT THE USE OF THE
35+
SOFTWARE OR DOCUMENT WILL NOT INFRINGE ANY THIRD PARTY PATENTS, COPYRIGHTS,
36+
TRADEMARKS OR OTHER RIGHTS.
37+
38+
COPYRIGHT HOLDERS WILL NOT BE LIABLE FOR ANY DIRECT, INDIRECT, SPECIAL OR
39+
CONSEQUENTIAL DAMAGES ARISING OUT OF ANY USE OF THE SOFTWARE OR DOCUMENT.
40+
41+
The name and trademarks of copyright holders may NOT be used in advertising or
42+
publicity pertaining to the work without specific, written prior permission.
43+
Title to copyright in this work will at all times remain with copyright
44+
holders.
45+
46+
47+
NOTES
48+
49+
This version:
50+
http://www.w3.org/Consortium/Legal/2015/copyright-software-and-document

Diff for: ‎spec/document/Makefile

+50
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
# Minimal makefile for Sphinx documentation
2+
#
3+
4+
# You can set these variables from the command line, and also
5+
# from the environment for the first two.
6+
SPHINXOPTS ?= -d _build/.doctrees
7+
SPHINXBUILD ?= sphinx-build
8+
SOURCEDIR = .
9+
BUILDDIR = _build
10+
11+
SOURCE_DATE_EPOCH = $(shell date +"%s")
12+
13+
ALLSPHINXOPTS = -d $(BUILDDIR)/doctrees $(SPHINXOPTS) .
14+
15+
# Put it first so that "make" without argument is like "make help".
16+
help:
17+
@$(SPHINXBUILD) -M help "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)
18+
19+
.PHONY: help Makefile
20+
21+
# Catch-all target: route all unknown targets to Sphinx using the new
22+
# "make mode" option. $(O) is meant as a shortcut for $(SPHINXOPTS).
23+
%: Makefile
24+
@$(SPHINXBUILD) -M $@ "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)
25+
26+
.PHONY: html
27+
html:
28+
$(SPHINXBUILD) -b html $(ALLSPHINXOPTS) $(BUILDDIR)/html
29+
for file in `ls $(BUILDDIR)/html/*.html`; \
30+
do \
31+
sed s:BASEDIR:.:g <$$file >$$file.out; \
32+
mv -f $$file.out $$file; \
33+
done
34+
for file in `ls $(BUILDDIR)/html/*/*.html`; \
35+
do \
36+
sed s:BASEDIR:..:g <$$file >$$file.out; \
37+
mv -f $$file.out $$file; \
38+
done
39+
@echo
40+
@echo "Build finished. The HTML pages are in `pwd`/$(BUILDDIR)/html/."
41+
42+
NAME=webassemblycomponentmodel
43+
44+
.PHONY: docs
45+
docs: html latexpdf
46+
mkdir -p ../../docs/multihtml/
47+
cp -r $(BUILDDIR)/html/* ../../docs/multihtml/
48+
rm ../../docs/multihtml/objects.inv
49+
mkdir -p ../../docs/_download/
50+
cp $(BUILDDIR)/latex/$(NAME).pdf ../../docs/_download/

Diff for: ‎spec/document/appendix/index.rst

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
.. _appendix:
2+
3+
Appendix
4+
========

Diff for: ‎spec/document/binary/index.rst

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
.. _binary:
2+
3+
Binary Format
4+
=============
5+
6+
TODO: Formal write-up of the binary format.

Diff for: ‎spec/document/conf.py

+83
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
1+
# Configuration file for the Sphinx documentation builder.
2+
#
3+
# This file only contains a selection of the most common options. For a full
4+
# list see the documentation:
5+
# https://www.sphinx-doc.org/en/master/usage/configuration.html
6+
7+
# -- Path setup --------------------------------------------------------------
8+
9+
# If extensions (or modules to document with autodoc) are in another directory,
10+
# add these directories to sys.path here. If the directory is relative to the
11+
# documentation root, use os.path.abspath to make it absolute, like shown here.
12+
#
13+
import os
14+
import sys
15+
from datetime import date
16+
sys.path.insert(0, os.path.abspath('.'))
17+
18+
19+
# -- Project information -----------------------------------------------------
20+
21+
name = 'WebAssembly Component Model'
22+
project = 'WebAssembly Component Model'
23+
title = 'WebAssembly Component Model Specification'
24+
copyright = '2022 WebAssembly Community Group'
25+
author = 'Authors of the Webassembly Component Model Specification'
26+
27+
version = u'0.0'
28+
# The draft version string (clear out for release cuts)
29+
draft = ' (Draft ' + date.today().strftime("%Y-%m-%d") + ')'
30+
# The full version, including alpha/beta/rc tags.
31+
release = version + draft
32+
33+
mathjax_path='https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js'
34+
35+
# -- General configuration ---------------------------------------------------
36+
37+
# Add any Sphinx extension module names here, as strings. They can be
38+
# extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
39+
# ones.
40+
extensions = [
41+
'sphinx.ext.mathjax',
42+
'util.mathdef'
43+
]
44+
45+
# Add any paths that contain templates here, relative to this directory.
46+
templates_path = ['_templates']
47+
48+
# List of patterns, relative to source directory, that match files and
49+
# directories to ignore when looking for source files.
50+
# This pattern also affects html_static_path and html_extra_path.
51+
exclude_patterns = ['_build', 'Thumbs.db', '.DS_Store']
52+
53+
54+
# -- Options for HTML output -------------------------------------------------
55+
56+
# The theme to use for HTML and HTML Help pages. See the documentation for
57+
# a list of builtin themes.
58+
#
59+
html_theme = 'alabaster'
60+
html_theme_options = {
61+
'description': 'WebAssembly Component Model Specification',
62+
'fixed_sidebar': True,
63+
'sidebar_width': '260px',
64+
'sidebar_collapse': True,
65+
'show_powered_by': False,
66+
'extra_nav_links': {
67+
'Index': 'BASEDIR/genindex.html',
68+
'Download as PDF': 'BASEDIR/../_download/webassemblycomponentmodel.pdf'
69+
},
70+
}
71+
html_title = project +u' ' + release
72+
html_copy_source = False # At least for the one included in docs/ ...
73+
74+
# Add any paths that contain custom static files (such as style sheets) here,
75+
# relative to this directory. They are copied after the builtin static files,
76+
# so a file named "default.css" will overwrite the builtin "default.css".
77+
# html_static_path = ['_static']
78+
79+
pwd = os.path.abspath('.')
80+
rst_prolog = """
81+
.. include:: /""" + pwd + """/util/macros-core.def
82+
.. include:: /""" + pwd + """/util/macros.def
83+
"""

Diff for: ‎spec/document/exec/index.rst

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
.. _exec:
2+
3+
Execution
4+
=========
5+
6+
TODO: Describe the execution semantics of a component
7+
8+
.. toctree::
9+
:maxdepth: 2

Diff for: ‎spec/document/index.rst

+26
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
.. wasm components documentation master file, created by
2+
sphinx-quickstart on Wed Sep 22 14:51:32 2021.
3+
You can adapt this file completely to your liking, but it should at least
4+
contain the root `toctree` directive.
5+
6+
Welcome to the WebAssembly Component Model Specification
7+
========================================================
8+
9+
.. toctree::
10+
:maxdepth: 2
11+
:caption: Contents:
12+
13+
intro/index
14+
syntax/index
15+
valid/index
16+
exec/index
17+
binary/index
18+
text/index
19+
appendix/index
20+
21+
Indices and tables
22+
==================
23+
24+
* :ref:`genindex`
25+
* :ref:`modindex`
26+
* :ref:`search`

Diff for: ‎spec/document/intro/index.rst

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
.. _intro:
2+
3+
Introduction
4+
============
5+
6+
TODO: Introduction

Diff for: ‎spec/document/shell.nix

+5
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
{ nixpkgs ? import <nixpkgs> {} }: with nixpkgs;
2+
stdenv.mkDerivation {
3+
name = "wasm-components-spec";
4+
buildInputs = [ gnumake sphinx texlive.combined.scheme-full ];
5+
}

Diff for: ‎spec/document/syntax/components.rst

+224
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,224 @@
1+
Components
2+
----------
3+
4+
.. _syntax-coresort:
5+
.. _syntax-sort:
6+
7+
Sorts
8+
~~~~~
9+
10+
A component's definitions define objects, each of which is of one of
11+
the following *sort*\ s:
12+
13+
.. math::
14+
\begin{array}{llcl}
15+
\production{(coresort)} & \coresort &::=&
16+
\CSFUNC | \CSTABLE | \CSMEMORY | \CSGLOBAL | \CSTYPE | \CSMODULE | \CSINSTANCE\\
17+
\production{(sort)} & \sort &::=&
18+
\SCORE~\coresort\\&&|&
19+
\SFUNC | \SVALUE | \STYPE | \SCOMPONENT | \SINSTANCE
20+
\end{array}
21+
22+
.. _syntax-coremoduleidx:
23+
.. _syntax-componentidx:
24+
.. _syntax-instanceidx:
25+
.. _syntax-funcidx:
26+
.. _syntax-corefuncidx:
27+
.. _syntax-typeidx:
28+
.. _syntax-coretypeidx:
29+
.. _syntax-sortidx:
30+
.. _syntax-coresortidx:
31+
.. _syntax-coreinstanceidx:
32+
.. _syntax-valueidx:
33+
34+
Indices
35+
~~~~~~~
36+
37+
Each object defined by a component exists within an *index space* made
38+
up of all objects of the same sort. Unlike in Core WebAssembly, a
39+
component definition may only refer to objects that were defined prior
40+
to it in the current component. Future definitions refer to past
41+
definitions by means of an *index* into the appropriate index space:
42+
43+
.. math::
44+
\begin{array}{llll}
45+
\production{(coremoduleidx)} & \coremoduleidx &::=& \u32\\
46+
\production{(coreinstanceidx)} & \coreinstanceidx &::=& \u32\\
47+
\production{(componentidx)} & \componentidx &::=& \u32\\
48+
\production{(instanceidx)} & \instanceidx &::=& \u32\\
49+
\production{(funcidx)} & \funcidx &::=& \u32\\
50+
\production{(corefuncidx)} & \corefuncidx &::=& \u32\\
51+
\production{(valueidx)} & \valueidx &::=& \u32\\
52+
\production{(typeidx)} & \typeidx &::=& \u32\\
53+
\production{(coretypeidx)} & \coretypeidx &::=& \u32
54+
\end{array}
55+
56+
.. math::
57+
\begin{array}{llll}
58+
\production{(coresortidx)} & \coresortidx &::=& \{ \CSISORT~\coresort, \CSIIDX~\u32 \}\\
59+
\production{(sortidx)} & \sortidx &::=& \{ \SISORT~\sort, \SIIDX~\u32 \}
60+
\end{array}
61+
62+
.. _syntax-definition:
63+
64+
Definitions
65+
~~~~~~~~~~~
66+
67+
Each object within a component is defined by a *definition*, of which
68+
there are several kinds:
69+
70+
.. math::
71+
\begin{array}{llcl}
72+
\production{(definition)} & \definition &::=&
73+
\DCOREMODULE~\core:module\\&&|&
74+
\DCOREINSTANCE~\coreinstance\\&&|&
75+
\DCORETYPE~\coredeftype\\&&|&
76+
\DCOMPONENT~\component\\&&|&
77+
\DINSTANCE~\instance\\&&|&
78+
\DALIAS~\alias\\&&|&
79+
\DTYPE~\deftype\\&&|&
80+
\DCANON~\canon\\&&|&
81+
\DSTART~\start\\&&|&
82+
\DIMPORT~\import\\&&|&
83+
\DEXPORT~\export\\
84+
\end{array}
85+
86+
.. _syntax-coreinstance:
87+
.. _syntax-coreinstantiatearg:
88+
.. _syntax-coreexport:
89+
90+
Core instances
91+
~~~~~~~~~~~~~~
92+
93+
A core instance may be defined either by instantiating a core module
94+
with other core instances taking the place of its first-level imports,
95+
or by creating a core module from whole cloth by combining core
96+
definitions already present in our index space:
97+
98+
.. math::
99+
\begin{array}{llcl}
100+
\production{(coreinstance)} & \coreinstance &::=&
101+
\CIINSTANTIATE~\coremoduleidx~\coreinstantiatearg^{*}\\&&|&
102+
\CIEXPORTS~\coreexport^{*}\\
103+
\production{(coreinstantiatearg)} & \coreinstantiatearg &::=&
104+
\{ \CIANAME~\name, \CIAINSTANCE~\coreinstanceidx \}\\
105+
\production{(coreexport)} & \coreexport &::=& \{ \CENAME~\name, \CEDEF~\coresortidx \}\\
106+
\end{array}
107+
108+
.. _syntax-component:
109+
110+
Components
111+
~~~~~~~~~~
112+
113+
A component is merely a sequence of definitions:
114+
115+
.. math::
116+
\begin{array}{llll}
117+
\production{(component)} & \component &::=& \definition^{*}
118+
\end{array}
119+
120+
.. _syntax-instance:
121+
.. _syntax-instantiatearg:
122+
123+
Instances
124+
~~~~~~~~~
125+
126+
Component-level instance declarations are nearly identical to
127+
core-level instance declarations, with the caveat that more sorts of
128+
definitions may be supplied as imports:
129+
130+
.. math::
131+
\begin{array}{llcl}
132+
\production{(instance)} & \instance &::=&
133+
\IINSTANTIATE~\componentidx~\instantiatearg^{*}\\&&|&
134+
\IEXPORTS~\export^{*}\\
135+
\production{(instantiatearg)} & \instantiatearg &::=&
136+
\{ \IANAME~\name, \IAARG~\sortidx \}
137+
\end{array}
138+
139+
.. _syntax-alias:
140+
.. _syntax-aliastarget:
141+
142+
Aliases
143+
~~~~~~~
144+
145+
An alias definition copies a definition from some other module,
146+
component, or instance into an index space of the current component:
147+
148+
.. math::
149+
\begin{array}{llcl}
150+
\production{(alias)} & \alias &::=& \{ \ASORT~\sort, \ATARGET~\aliastarget \}\\
151+
\production{(aliastarget)} & \aliastarget &::=&
152+
\ATEXPORT~\instanceidx~\name\\&&|&
153+
\ATCOREEXPORT~\coreinstanceidx~\name\\&&|&
154+
\ATOUTER~\u32~\u32\\
155+
\end{array}
156+
157+
.. _syntax-canon:
158+
.. _syntax-canonopt:
159+
160+
Canonical definitions
161+
~~~~~~~~~~~~~~~~~~~~~
162+
163+
Canonical definitions are the only way to convert between Core
164+
WebAssembly functions and component-level shared-nothing functions
165+
which produce and consume values of type :math:`valtype`. A *canon
166+
lift* definition converts a core WebAssembly function into a
167+
component-level function which may be exported or used to satisfy the
168+
imports of another component; a *canon lower* definition converts an
169+
lifted function (often imported) into a core function.
170+
171+
.. math::
172+
\begin{array}{llcl}
173+
\production{(canon)} & \canon &::=&
174+
\CLIFT~\core:funcidx~\canonopt^{*}~\typeidx\\&&|&
175+
\CLOWER~\funcidx~\canonopt^{*}\\
176+
\production{(canonopt)} & \canonopt &::=&
177+
\COSTRINGENCODINGUTF8\\&&|&
178+
\COSTRINGENCODINGUTF16\\&&|&
179+
\COSTRINGENCODINGLATIN1UTF16\\&&|&
180+
\COMEMORY~\core:memidx\\&&|&
181+
\COREALLOC~\core:funcidx\\&&|&
182+
\COPOSTRETURN~\core:funcidx\\
183+
\end{array}
184+
185+
.. _syntax-start:
186+
187+
Start definitions
188+
~~~~~~~~~~~~~~~~~
189+
190+
A start definition specifies a component function which this component
191+
would like to see called at instantiation type in order to do some
192+
sort of initialization.
193+
194+
.. math::
195+
\begin{array}{llcl}
196+
\production{(start)} & \start &::=& \{ \FFUNC~\funcidx, \FARGS~\valueidx^{*} \}
197+
\end{array}
198+
199+
.. _syntax-import:
200+
201+
Imports
202+
~~~~~~~
203+
204+
Since an imported value is described entirely by its type, an actual
205+
import definition is effectively the same thing as an import
206+
declaration:
207+
208+
.. math::
209+
\begin{array}{llcl}
210+
\production{(import)} & \import &::=& \importdecl
211+
\end{array}
212+
213+
.. _syntax-export:
214+
215+
Exports
216+
~~~~~~~
217+
218+
An export definition is simply a name and a reference to another
219+
definition to export:
220+
221+
.. math::
222+
\begin{array}{llll}
223+
\production{(export)} & \export &::=& \{ \ENAME~\name, \EDEF~\sortidx \}
224+
\end{array}

Diff for: ‎spec/document/syntax/conventions.rst

+43
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
.. index:: ! abstract syntax
2+
3+
Conventions
4+
-----------
5+
6+
The WebAssembly component specification defines a language for
7+
specifying components, which, like the WebAssembly core language, may
8+
be represented by multiple complete representations (e.g. the
9+
:ref:`binary format <binary>` and the :ref:`text format <text>`). In
10+
order to avoid duplication, the static and dynamic semantics of the
11+
WebAssembly component model are instead defined over an abstract
12+
syntax.
13+
14+
.. index:: ! grammar notation, notation
15+
single: abstract syntax; grammar
16+
pair: abstract syntax; noatation
17+
.. _grammar:
18+
19+
The following conventions are adopted in defining grammar rules for abstract syntax.
20+
21+
* Terminal symbols (atoms) are written in sans-serif font: :math:`\K{i32}, \K{end}`.
22+
23+
* Nonterminal symbols are written in italic font: :math:`\X{valtype}, \X{instr}`.
24+
25+
* :math:`A^n` is a sequence of :math:`n\geq 0` iterations of :math:`A`.
26+
27+
* :math:`A^\ast` is a possibly empty sequence of iterations of :math:`A`.
28+
(This is a shorthand for :math:`A^n` used where :math:`n` is not relevant.)
29+
30+
* :math:`A^+` is a non-empty sequence of iterations of :math:`A`.
31+
(This is a shorthand for :math:`A^n` where :math:`n \geq 1`.)
32+
33+
* :math:`A^?` is an optional occurrence of :math:`A`.
34+
(This is a shorthand for :math:`A^n` where :math:`n \leq 1`.)
35+
36+
* Productions are written :math:`\X{sym} ::= A_1 ~|~ \dots ~|~ A_n`.
37+
38+
* Large productions may be split into multiple definitions, indicated by ending the first one with explicit ellipses, :math:`\X{sym} ::= A_1 ~|~ \dots`, and starting continuations with ellipses, :math:`\X{sym} ::= \dots ~|~ A_2`.
39+
40+
* Some productions are augmented with side conditions in parentheses, ":math:`(\iff \X{condition})`", that provide a shorthand for a combinatorial expansion of the production into many separate cases.
41+
42+
* If the same meta variable or non-terminal symbol appears multiple times in a production, then all those occurrences must have the same instantiation.
43+
(This is a shorthand for a side condition requiring multiple different variables to be equal.)

Diff for: ‎spec/document/syntax/index.rst

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
.. _syntax:
2+
3+
Structure
4+
=========
5+
6+
.. toctree::
7+
:maxdepth: 2
8+
9+
conventions
10+
types
11+
components

Diff for: ‎spec/document/syntax/types.rst

+210
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,210 @@
1+
.. _syntax-type:
2+
3+
Types
4+
-----
5+
6+
The component model introduces two new kinds of types: value types,
7+
which are used to classify shared-nothing interface values, and
8+
definition types, which are used to characterize the core and
9+
component modules, instances, and functions which form part of a a
10+
component's interface.
11+
12+
.. _syntax-recordfield:
13+
.. _syntax-variantcase:
14+
.. _syntax-primvaltype:
15+
.. _syntax-defvaltype:
16+
.. _syntax-valtype:
17+
18+
Value types
19+
~~~~~~~~~~~
20+
21+
A *value type* classifies a component-level abstract value. Unlike for
22+
Core WebAssembly values, no specified abstract syntax of component
23+
values exist; they serve simply to define the interface of lifted
24+
component functions (which currently may be produced only via
25+
canonical definitions).
26+
27+
Value types are further divided into primitive value types, which have
28+
a compact representation and can be found in most places where types
29+
are allowed, and defined value types, which must appear in a type
30+
definition before they can be used (via a :math:`\typeidx` into the
31+
type index space):
32+
33+
.. math::
34+
\begin{array}{llcl}
35+
\production{(primvaltype)} & \primvaltype &::=&
36+
\VTBOOL\\&&|&
37+
\VTS8 ~|~ \VTU8 ~|~ \VTS16 ~|~ \VTU16 ~|~ \VTS32 ~|~ \VTU32 ~|~ \VTS64 ~|~ \VTU64\\&&|&
38+
\VTFLOAT32 ~|~ \VTFLOAT64\\&&|&
39+
\VTCHAR ~|~ \VTSTRING\\&&|&\\
40+
\production{(defvaltype)} & \defvaltype &::=&
41+
\VTPRIM~\primvaltype\\&&|&
42+
\VTRECORD~\recordfield^{+}\\&&|&
43+
\VTVARIANT~\variantcase^{+}\\&&|&
44+
\VTLIST~\valtype\\&&|&
45+
\VTTUPLE~\valtype^{*}\\&&|&
46+
\VTFLAGS~\name^{*}\\&&|&
47+
\VTENUM~\name^{+}\\&&|&
48+
\VTUNION~\valtype^{+}\\&&|&
49+
\VTOPTION~\valtype\\&&|&
50+
\VTRESULT~\valtype^{?}~\valtype^{?}\\&&|&
51+
\VTOWN~\typeidx\\&&|&
52+
\VTBORROW~\typeidx\\
53+
\production{(valtype)} &\valtype &::=&
54+
\primvaltype ~|~ \typeidx
55+
\end{array}
56+
57+
.. math::
58+
\begin{array}{llll}
59+
\production{(recordfield)} & \recordfield &::=&
60+
\{ \RFNAME~\name, \RFTYPE~\valtype \}\\
61+
\production{(variantcase)} & \variantcase &::=&
62+
\{ \VCNAME~\name, \VCTYPE~\valtype, \VCREFINES~\u32^? \}
63+
\end{array}
64+
65+
.. _syntax-resourcetype:
66+
67+
Resource types
68+
~~~~~~~~~~~~~~
69+
70+
.. math::
71+
\begin{array}{llll}
72+
\production{(resourcetype)} & \resourcetype &::= &
73+
\{ \RTREP~\mathtt{i32}, \RTDTOR~\funcidx \}
74+
\end{array}
75+
76+
.. _syntax-functype:
77+
.. _syntax-funclist:
78+
79+
Function types
80+
~~~~~~~~~~~~~~
81+
82+
A component-level shared-nothing function is classified by the types
83+
of its parameters and return values. Such a function may take as
84+
parameters zero or more named values, and will return as results zero
85+
or more namde values. If a function takes a single parameter, or
86+
returns a single result, said parameter or result may be unnamed:
87+
88+
.. math::
89+
\begin{array}{llll}
90+
\production{(functype)} & \functype &::=&
91+
\resulttype \to \resulttype
92+
\end{array}
93+
94+
The input or output of a function is classified by a result type:
95+
96+
.. math::
97+
\begin{array}{llcl}
98+
\production{(resulttype)} & \resulttype &::=&
99+
\valtype\\&&|&
100+
\{ \RTNAME~\name, \RTTYPE~\valtype \}^{*}
101+
\end{array}
102+
103+
.. _syntax-instancetype:
104+
.. _syntax-instancedecl:
105+
.. _syntax-exportdecl:
106+
.. _syntax-typebound:
107+
108+
Instance types
109+
~~~~~~~~~~~~~~
110+
111+
A component instance is conceptually classified by the types of its
112+
exports. However, an instance's type is concretely represented as a
113+
series of *declarations* manipulating index spaces (particular to the
114+
instance type; these index spaces are entirely unrelated to both the
115+
index spaces of any instance which has this type and those of any
116+
instance importing or exporting something of this type). This allows
117+
for better type sharing and, in the future, uses of private types from
118+
parent components.
119+
120+
.. math::
121+
\begin{array}{llcl}
122+
\production{(instancetype)} & \instancetype &::=& \instancedecl^{*}\\
123+
\production{(instancedecl)} & \instancedecl &::=&
124+
\IDALIAS~\alias\\&&|&
125+
\IDCORETYPE~\core:type\\&&|&
126+
\IDTYPE~\deftype\\&&|&
127+
\IDEXPORT~\exportdecl\\
128+
\production{(externdesc)} & \externdesc &::=&
129+
\EDTYPE~\typebound\\&&|&
130+
\EDCOREMODULE~\core:typeidx\\&&|&
131+
\EDFUNC~\typeidx\\&&|&
132+
\EDVALUE~\valtype\\&&|&
133+
\EDINSTANCE~\typeidx\\&&|&
134+
\EDCOMPONENT~\typeidx\\
135+
\production{(typebound)} & \typebound &::=&
136+
\TBEQ~\typeidx\\&&|&
137+
\TBSUBR\\&&|&
138+
\dots\\
139+
\production{(exportdecl)} & \exportdecl &::=& \{ \EDNAME~\name, \EDDESC~\externdesc \}
140+
\end{array}
141+
142+
.. _syntax-componenttype:
143+
.. _syntax-componentdecl:
144+
.. _syntax-importdecl:
145+
.. _syntax-externdesc:
146+
147+
Component types
148+
~~~~~~~~~~~~~~~
149+
150+
A component is conceptually classified by the types of its imports and
151+
exports. However, like instances, this is concretely represented as a
152+
series of declarations; in particular, a similar set of declarations
153+
allowing also for imports.
154+
155+
.. math::
156+
\begin{array}{llcl}
157+
\production{(componenttype)} & \componenttype &::=& \componentdecl^{*}\\
158+
\production{(componentdecl)} & \componentdecl &::=&
159+
\instancedecl\\&&|&
160+
\CDIMPORT~\importdecl\\
161+
\production{(importdecl)} & \importdecl &::=& \{ \IDNAME~\name, \IDDESC~\externdesc \}\\
162+
\end{array}
163+
164+
.. _syntax-deftype:
165+
166+
Definition types
167+
~~~~~~~~~~~~~~~~
168+
169+
A type definition may name a value, resource, function, component, or instance type:
170+
171+
.. math::
172+
\begin{array}{llcl}
173+
\production{(deftype)} & \deftype &::=&
174+
\defvaltype\\&&|&
175+
\resourcetype\\&&|&
176+
\functype\\&&|&
177+
\componenttype\\&&|&
178+
\instancetype\\
179+
\end{array}
180+
.. _syntax-coredeftype:
181+
.. _syntax-coremoduletype:
182+
.. _syntax-coreimportdecl:
183+
.. _syntax-coreexportdecl:
184+
.. _syntax-corealias:
185+
.. _syntax-corealiastarget:
186+
.. _syntax-coremoduledecl:
187+
188+
Core definition types
189+
~~~~~~~~~~~~~~~~~~~~~
190+
191+
The component module specification also defines an expanded notion of
192+
what a core type is, which may eventually be subsumed by a core module
193+
linking extension.
194+
195+
.. math::
196+
\begin{array}{llcl}
197+
\production{(coredeftype)} & \coredeftype &::=&
198+
\core:functype\\&&|&
199+
\coremoduletype\\
200+
\production{(coremoduletype)} & \coremoduletype &::=& \coremoduledecl^{*}\\
201+
\production{(coremoduledecl)} & \coremoduledecl &::=&
202+
\coreimportdecl\\&&|&
203+
\coredeftype\\&&|&
204+
\corealias\\&&|&
205+
\coreexportdecl\\
206+
\production{(corealias)} & \corealias &::=& \{ \CASORT~\coresort, \CATARGET~\corealiastarget \}\\
207+
\production{(corealiastarget)} & \corealiastarget &::=& \CATOUTER~\u32~\u32\\
208+
\production{(coreimportdecl)} & \coreimportdecl &::=& \core:import\\
209+
\production{(coreexportdecl)} & \coreexportdecl &::=& \{ \CEDNAME~\name, \CEDDESC~\core:importdesc \}
210+
\end{array}

Diff for: ‎spec/document/text/index.rst

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
.. _text:
2+
3+
Text Format
4+
===========
5+
6+
TODO: Formal write-up of the text format.

Diff for: ‎spec/document/util/macros-core.def

+1,281
Large diffs are not rendered by default.

Diff for: ‎spec/document/util/macros.def

+388
Large diffs are not rendered by default.

Diff for: ‎spec/document/util/mathdef.py

+181
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,181 @@
1+
from sphinx.directives.patches import MathDirective
2+
from sphinx.util.texescape import tex_replace_map
3+
from sphinx.writers.html5 import HTML5Translator
4+
from sphinx.writers.latex import LaTeXTranslator
5+
from docutils import nodes
6+
from docutils.nodes import math
7+
from docutils.parsers.rst.directives.misc import Replace
8+
from six import text_type
9+
import re
10+
11+
12+
# Transform \xref in math nodes
13+
14+
xref_re = re.compile('\\\\(core:|)xref\{([^}]*)\}\{([^}]*)\}', re.M)
15+
16+
def munge_file(file):
17+
if file[0] == "!":
18+
fileparts = file.split("!")
19+
if fileparts[1] == "S":
20+
if fileparts[2] in fileparts[3]:
21+
return fileparts[4]
22+
else:
23+
return fileparts[5]
24+
return file
25+
26+
def html_hyperlink(is_core, file, id):
27+
sub = (munge_file(file), id.replace('_', '-').lower())
28+
if is_core:
29+
return '\\href{https://webassembly.github.io/spec/core/%s.html#%s}' % sub
30+
else:
31+
return '\\href{../%s.html#%s}' % sub
32+
33+
def html_transform_math_xref(node):
34+
new_text = xref_re.sub(lambda m: html_hyperlink(m.group(1), m.group(2), m.group(3)), node.astext())
35+
node.children[0] = nodes.Text(new_text)
36+
37+
# Mirrors sphinx/writers/latex
38+
def latex_hyperlink(is_core, file, id):
39+
if is_core:
40+
return '\\href{https://webassembly.github.io/spec/core/%s.html\\#%s}' \
41+
% (munge_file(file), id.replace('_', '-'))
42+
else:
43+
id = text_type(id).translate(tex_replace_map).\
44+
encode('ascii', 'backslashreplace').decode('ascii').\
45+
replace('_', '-').replace('\\', '_')
46+
return '\\hyperref[%s:%s]' % (munge_file(file), id)
47+
48+
def latex_transform_math_xref(node):
49+
new_text = xref_re.sub(lambda m: latex_hyperlink(m.group(1), m.group(2), m.group(3)), node.astext())
50+
node.children[0] = nodes.Text(new_text)
51+
52+
# Expand mathdef names in math roles and directives
53+
54+
def_re = re.compile('\\\\[A-Za-z][0-9A-Za-z:!]*', re.M)
55+
56+
auxcounter = 0
57+
58+
def corify_xrefs(str):
59+
corified = xref_re.sub(lambda m: '\\core:xref{%s}{%s}' % (m.group(2), m.group(3)), str)
60+
return corified
61+
62+
def lookup_mathdef(defs, name, is_core):
63+
split = name.split('!')
64+
name = split[0]
65+
if is_core:
66+
core_name = "\\core:" + name[1:]
67+
if core_name in defs:
68+
return lookup_mathdef(defs, core_name, False)
69+
if name in defs:
70+
[arity, s] = defs[name]
71+
if arity == 1 and name == "X":
72+
# stupid hack for reasons
73+
pass
74+
if arity > 0:
75+
global auxcounter
76+
auxcounter = auxcounter + 1
77+
name = "\\mathdef%d" % auxcounter
78+
s = "\\def%s#%d{%s}%s" % (name, arity, s, name)
79+
if arity < 0:
80+
for i in range(1, -arity+1):
81+
s = s.replace("#" + str(i), split[i])
82+
if name.startswith("\\core:"):
83+
s = corify_xrefs(s)
84+
return s
85+
return name
86+
87+
def replace_mathdefs(doc, s, is_core):
88+
if not hasattr(doc, 'mathdefs'):
89+
return s
90+
return def_re.sub(lambda m: lookup_mathdef(doc.mathdefs, m.group(0), is_core), s)
91+
92+
def ext_math_role(role, raw, text, line, inliner, options = {}, content = []):
93+
text = replace_mathdefs(inliner.document, raw.split('`')[1], False)
94+
return [math(raw, text)], []
95+
96+
class ExtMathDirective(MathDirective):
97+
def run(self):
98+
doc = self.state.document
99+
for i, s in enumerate(self.content):
100+
self.content[i] = replace_mathdefs(doc, s, False)
101+
for i, s in enumerate(self.arguments):
102+
self.arguments[i] = replace_mathdefs(doc, s, False)
103+
return super().run()
104+
105+
class MathdefDirective(Replace):
106+
def run(self):
107+
name = '\\' + self.state.parent.rawsource.split('|')[1]
108+
name = name.split('#')
109+
if len(name) > 1:
110+
arity = int(name[1])
111+
else:
112+
arity = 0
113+
name = name[0]
114+
doc = self.state.document
115+
if not hasattr(doc, 'mathdefs'):
116+
doc.mathdefs = {}
117+
# TODO: we don't ever hit the case where len(self.content) > 1
118+
for i, s in enumerate(self.content):
119+
self.content[i] = replace_mathdefs(doc, s, False)
120+
doc.mathdefs[name] = [arity, ''.join(self.content)]
121+
self.content[0] = ':math:`' + self.content[0]
122+
self.content[-1] = self.content[-1] + '`'
123+
return super().run()
124+
125+
class CoreMathdefDirective(Replace):
126+
def run(self):
127+
name = self.state.parent.rawsource.split('|')[1]
128+
name = '\\' + ("" if name.startswith("core:") else "core:") + name
129+
name = name.split('#')
130+
if len(name) > 1:
131+
arity = int(name[1])
132+
else:
133+
arity = 0
134+
name = name[0]
135+
doc = self.state.document
136+
if not hasattr(doc, 'mathdefs'):
137+
doc.mathdefs = {}
138+
# TODO: we don't ever hit the case where len(self.content) > 1
139+
for i, s in enumerate(self.content):
140+
self.content[i] = replace_mathdefs(doc, s, True)
141+
doc.mathdefs[name] = [arity, ''.join(self.content)]
142+
self.content[0] = ':math:`' + self.content[0]
143+
self.content[-1] = self.content[-1] + '`'
144+
return super().run()
145+
146+
class WebAssemblyHTML5Translator(HTML5Translator):
147+
"""
148+
Customize HTML5Translator.
149+
Convert xref in math and math block nodes to hrefs.
150+
"""
151+
def visit_math(self, node, math_env = ''):
152+
html_transform_math_xref(node)
153+
super().visit_math(node, math_env)
154+
155+
def visit_math_block(self, node, math_env = ''):
156+
html_transform_math_xref(node)
157+
super().visit_math_block(node, math_env)
158+
159+
class WebAssemblyLaTeXTranslator(LaTeXTranslator):
160+
"""
161+
Customize LaTeXTranslator.
162+
Convert xref in math and math block nodes to hyperrefs.
163+
"""
164+
def visit_math(self, node):
165+
latex_transform_math_xref(node)
166+
super().visit_math(node)
167+
168+
def visit_math_block(self, node):
169+
latex_transform_math_xref(node)
170+
super().visit_math_block(node)
171+
172+
# Setup
173+
174+
def setup(app):
175+
app.set_translator('html', WebAssemblyHTML5Translator)
176+
app.set_translator('singlehtml', WebAssemblyHTML5Translator)
177+
app.set_translator('latex', WebAssemblyLaTeXTranslator)
178+
app.add_role('math', ext_math_role)
179+
app.add_directive('math', ExtMathDirective, override = True)
180+
app.add_directive('mathdef', MathdefDirective)
181+
app.add_directive('coremathdef', CoreMathdefDirective)

Diff for: ‎spec/document/valid/components.rst

+807
Large diffs are not rendered by default.

Diff for: ‎spec/document/valid/conventions.rst

+69
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
Conventions
2+
-----------
3+
4+
As in Core WebAssembly, a *validation* stage checks that a component
5+
is well-formed, and only valid components may be instantiated.
6+
7+
Similarly to Core WebAssembly, a *type system* over the abstract
8+
syntax of a component is used to specify which modules are valid, and
9+
the rules governing the validity of a component are given in both
10+
prose and formal mathematical notation.
11+
12+
.. _syntax-tyctx:
13+
.. _syntax-coretyctx:
14+
15+
Contexts
16+
~~~~~~~~
17+
18+
Validation rules for individual definitions are interpreted within a
19+
particular *context*, which contains the information about the
20+
surrounding component and environment needed to validae a particular
21+
definition. The validation contexts used in the component model
22+
contain the types of every definition in every index space currently
23+
accessible (including the index spaces of parent components, which may
24+
be accessed via :math:`\ATOUTER` aliases).
25+
26+
Concretely, a validation context is defined as a record with the
27+
following abstract syntax:
28+
29+
.. math::
30+
\begin{array}{llcl}
31+
\production{(coretyctx)} & \coretyctx &::=&
32+
\{
33+
\begin{array}[t]{l@{~}ll}
34+
\CTCTYPES & \ecoredeftype^\ast, \\
35+
\CTCFUNCS & \core:functype^\ast, \\
36+
\CTCMODULES & \ecoremoduletype^\ast, \\
37+
\CTCINSTANCES & \ecoreinstancetype^\ast, \\
38+
\CTCTABLES & \core:tabletype^\ast, \\
39+
\CTCMEMS & \core:memtype^\ast, \\
40+
\CTCGLOBALS & \core:globaltype^\ast\} \\
41+
\end{array}\\
42+
\production{(tyctx)} & \tyctx &::=&
43+
\{
44+
\begin{array}[t]{l@{~}ll}
45+
\TCPARENT & \tyctx, \\
46+
\TCCORE & \coretyctx, \\
47+
\TCUVARS & \boundedtyvar^\ast, \\
48+
\TCEVARS & (\boundedtyvar, \edeftype)^\ast \\
49+
\TCRTYPES & \eresourcetype^\ast, \\
50+
\TCTYPES & \edeftype^\ast, \\
51+
\TCCOMPONENTS & \ecomponenttype^\ast, \\
52+
\TCINSTANCES & {\einstancetype^\dagger}^\ast, \\
53+
\TCFUNCS & \efunctype^\ast, \\
54+
\TCVALUES & \evaltypead^\ast, \} \\
55+
\end{array}\\
56+
\end{array}
57+
58+
Notation
59+
~~~~~~~~
60+
61+
Both the formal and prose notation share a number of constructs:
62+
63+
* When writing a value of the abstract syntax, any component of the
64+
abstract syntax which has the form :math:`\X{nonterminal}^n`,
65+
:math:`\X{nonterminal}^\ast`, :math:`\X{nonterminal}^{+}`, or
66+
:math:`\X{nonterminal}^{?}`, we may write
67+
:math:`\overline{\dots_i}^n` to mean that this position is filled by
68+
a series of :math:`n` abstract values, named :math:`\dots_1` to
69+
:math:`\dots_n`.

Diff for: ‎spec/document/valid/index.rst

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
.. _valid:
2+
3+
Validation
4+
==========
5+
6+
.. toctree::
7+
:maxdepth: 2
8+
9+
conventions
10+
types
11+
subtyping
12+
components

Diff for: ‎spec/document/valid/subtyping.rst

+332
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,332 @@
1+
Subtyping
2+
---------
3+
4+
Subtyping defines when a value of one type may be used when a value of
5+
another type is expected.
6+
7+
TODO: This is not complete, pending further discussion, especially in
8+
re the special treatment that may or may not be required or specialized value types.
9+
10+
Value types
11+
~~~~~~~~~~~
12+
13+
Reflexivity
14+
...........
15+
16+
* Any value type is a subtype of itself
17+
18+
.. math::
19+
\frac{
20+
}{
21+
\evaltype \subtypeof \evaltype
22+
}
23+
24+
Numeric types
25+
.............
26+
27+
* :math:`\EVTS8` is a subtype of :math:`\EVTS16`, :math:`\EVTS32`, and
28+
:math:`\EVTS64`.
29+
30+
* :math:`\EVTS16` is a subtype of :math:`\EVTS32` and :math:`\EVTS64`.
31+
32+
* :math:`\EVTS32` is a subtype of :math:`\EVTS64`.
33+
34+
* :math:`\EVTU8` is a subtype of :math:`\EVTU16`, :math:`\EVTU32`,
35+
:math:`\EVTU64`, :math:`\EVTS16`, :math:`\EVTS32`, and
36+
:math:`\EVTS64`.
37+
38+
* :math:`\EVTU16` is a subtype of :math:`\EVTU32`, :math:`\EVTU64`,
39+
:math:`\EVTS32`, and :math:`\EVTS64`.
40+
41+
* :math:`\EVTU32` is a subtype of :math:`\EVTU64` and :math:`\EVTS64`.
42+
43+
* :math:`\EVTFLOAT32` is a subtype of :math:`\EVTFLOAT64`.
44+
45+
.. math::
46+
\frac{
47+
m > n
48+
}{
49+
\K{s}n \subtypeof \K{s}m
50+
}
51+
52+
.. math::
53+
\frac{
54+
m > n
55+
}{
56+
\K{u}n \subtypeof \K{u}m
57+
}
58+
59+
.. math::
60+
\frac{
61+
m > n
62+
}{
63+
\K{u}n \subtypeof \K{s}m
64+
}
65+
66+
.. math::
67+
\frac{
68+
}{
69+
\EVTFLOAT32 \subtypeof \EVTFLOAT64
70+
}
71+
72+
Records
73+
.......
74+
75+
* A type :math:`\EVTRECORD~\overline{{\erecordfield}_i}` is a subtype
76+
of a type :math:`\EVTRECORD~\overline{{\erecordfield'}_j}` if, for
77+
each named field of the latter type, a field with the same name is
78+
present in the former, and the type of the field in the former is a
79+
subtype of the type of the field in the latter.
80+
81+
Todo: We may need to move despecialization later because of subtyping?
82+
83+
.. math::
84+
\frac{
85+
\begin{aligned}
86+
\forall j, \exists i,&{\erecordfield}_i.\ERFNAME = {\erecordfield'}_j.\ERFNAME\\ \land{}& {\erecordfield}_i.\ERFTYPE \subtypeof {\erecordfield}_j.\ERFTYPE
87+
\end{aligned}
88+
}{
89+
\EVTRECORD~\overline{{\erecordfield}_i} \subtypeof
90+
\EVTRECORD~\overline{{\erecordfield'}_j}
91+
}
92+
93+
Variants
94+
........
95+
96+
* A type :math:`\EVTVARIANT~\overline{{\evariantcase}_i}` is a subtype
97+
of a type :math:`\EVTVARIANT~\overline{{\evariantcase'}_j}` if, or
98+
each named case of the former type, either:
99+
100+
+ A case of the same name exists in the latter type, such that the
101+
type of the field in the former is a subtype of the type of the
102+
field in the latter; or
103+
104+
+ No case of the same name exists in the latter type, and the case
105+
in the former contains a :math:`\EVCREFINES`.
106+
107+
.. math::
108+
\frac{
109+
\begin{alignedat}{2}
110+
\forall i,&&(\exists j,&{\evariantcase'}_j.\EVCNAME = {\evariantcase}_i.\EVCNAME\\&& \land{}& {\evariantcase}_i \subtypeof {\evariantcase'}_j)\\
111+
\lor{}&&(\forall j,&{\evariantcase'}_j.\EVCNAME \neq {\evariantcase}_i.\EVCNAME\\&& \land{}&\exists \name, {\evariantcase}_i.\EVCREFINES = \name)
112+
\end{alignedat}
113+
}{
114+
\EVTVARIANT~\overline{{\evariantcase}_i} \subtypeof
115+
\EVTVARIANT~\overline{{\evariantcase'}_j}
116+
}
117+
118+
Lists
119+
.....
120+
121+
* A type :math:`\EVTLIST~\evaltype` is a subtype of a type
122+
:math:`\EVTLIST~\evaltype'` if :math:`\evaltype` is a subtype of
123+
:math:`\evaltype'`
124+
125+
.. math::
126+
\frac{
127+
\evaltype \subtypeof \evaltype'
128+
}{
129+
\EVTLIST~\evaltype \subtypeof \EVTLIST~\evaltype'
130+
}
131+
132+
Result types
133+
~~~~~~~~~~~~
134+
135+
* A result type of the form :math:`\evaltype` is a subtype of a result
136+
type of te form :math:`\evaltype'` if :math:`\evaltype` is a subtype
137+
of :math:`\evaltype'`.
138+
139+
.. math::
140+
\frac{
141+
\evaltype \subtypeof \evaltype'
142+
}{
143+
\evaltype \subtypeof \evaltype'
144+
}
145+
146+
* A result type of the form :math:`\overline{\{ \ERTNAME~\name_i,
147+
\ERTTYPE~{\evaltype}_i \}}` is a subtype of a result type of the form
148+
:math:`\overline{\{ \ERTNAME~\name'_j, \ERTTYPE~{\evaltype'}_j \}}`
149+
when:
150+
151+
+ For each :math:`\name'_j`, there is some :math:`i` such that
152+
:math:`\name'_j = \name_i` and :math:`{\evaltype}_i \subtypeof
153+
{\evaltype}'_j`.
154+
155+
.. math::
156+
\frac{
157+
\forall j, \exists i, \name_i = \name'_j \land {\evaltype}_i \subtypeof {\evaltype}'_j
158+
}{
159+
\overline{\{ \ERTNAME~\name_i, \ERTTYPE~{\evaltype}_i \}}
160+
\subtypeof
161+
\overline{\{ \ERTNAME~\name'_j, \ERTTYPE~{\evaltype'}_j \}}
162+
}
163+
164+
Function types
165+
~~~~~~~~~~~~~~
166+
167+
* A function type :math:`{\eresulttype}_1 \to {\eresulttype}_2` is a
168+
subtype of a function :math:`{\eresulttype'}_1 \to
169+
{\eresulttype'}_2` if :math:`{\eresulttype'}_1 \subtypeof
170+
{\eresulttype}_1` and :math:`{\eresulttype}_2 \subtypeof
171+
{\eresulttype'}_2`.
172+
173+
.. math::
174+
\frac{
175+
\begin{array}{@{}c@{}}
176+
{\eresulttype'}_1 \subtypeof {\eresulttype}_1\\
177+
{\eresulttype}_2 \subtypeof {\eresulttype'}_2
178+
\end{array}
179+
}{
180+
{\eresulttype}_1 \to {\eresulttype}_2
181+
\subtypeof
182+
{\eresulttype'}_1 \to {\eresulttype'}_2
183+
}
184+
185+
Type bound
186+
~~~~~~~~~~
187+
188+
:math:`\ETBEQ~\edeftype`
189+
........................
190+
191+
* A type bound :math:`\ETBEQ~\edeftype` is a subtype of
192+
:math:`\ETBEQ~\edeftype'` if :math:`\edeftype` is a subtype of
193+
:math:`\edeftype'`.
194+
195+
.. math::
196+
\frac{
197+
\edeftype \subtypeof \edeftype'
198+
}{
199+
\ETBEQ~\edeftype \subtypeof \ETBEQ~\edeftype'
200+
}
201+
202+
Extern descriptors
203+
~~~~~~~~~~~~~~~~~~
204+
205+
:math:`\EEMDCOREMODULE~\ecoremoduletype`
206+
........................................
207+
208+
* A extern descriptor :math:`\EEMDCOREMODULE~\ecoremoduletype` is a
209+
subtype of :math:`\EEMDCOREMODULE~\ecoremoduletype'` if
210+
:math:`\ecoremoduletype` is a subtype of :math:`\ecoremoduletype'`.
211+
212+
.. math::
213+
\frac{
214+
\ecoremoduletype' \subtypeof \coremoduletype'
215+
}{
216+
\EEMDCOREMODULE~\ecoremoduletype \subtypeof
217+
\EEMDCOREMODULE~\ecoremoduletype'
218+
}
219+
220+
:math:`\EEMDFUNC~\efunctype`
221+
............................
222+
223+
* An extern descriptor :math:`\EEMDFUNC~\efunctype` is a subtype of
224+
:math:`\EEMDFUNC~\efunctype'` if :math:`\efunctype` is a subtype of
225+
:math:`\efunctype'`.
226+
227+
.. math::
228+
\frac{
229+
\efunctype \subtypeof \efunctype'
230+
}{
231+
\EEMDFUNC~\efunctype \subtypeof \EEMDFUNC~\efunctype'
232+
}
233+
234+
:math:`\EEMDVALUE~\evaltype`
235+
............................
236+
237+
* An extern descriptor :math:`\EEMDVALUE~\evaltype` is a subtype of
238+
:math:`\EEMDVALUE~\evaltype'` if :math:`\evaltype` is a subtype of
239+
:math:`\evaltype'`.
240+
241+
.. math::
242+
\frac{
243+
\evaltype \subtypeof \evaltype'
244+
}{
245+
\EEMDVALUE~\evaltype \subtypeof \EEMDVALUE~\evaltype'
246+
}
247+
248+
:math:`\EEMDTYPE~\etypebound`
249+
.............................
250+
251+
* An extern descriptor :math:`\EEMDTYPE~\etypebound` is a subtype of
252+
:math:`\EEMDTYPE~\etypebound'` if :math:`\etypebound` is a subtype of
253+
:math:`\etypebound'`.
254+
255+
.. math::
256+
\frac{
257+
\etypebound \subtypeof \etypebound'
258+
}{
259+
\EEMDTYPE~\etypebound \subtypeof \EEMDTYPE~\etypebound'
260+
}
261+
262+
:math:`\EEMDINSTANCE~\einstancetype`
263+
....................................
264+
265+
* An extern descriptor :math:`\EEMDINSTANCE~\einstancetype` is a subtype of
266+
:math:`\EEMDINSTANCE~\einstancetype'` if :math:`\einstancetype` is a subtype of
267+
:math:`\einstancetype'`.
268+
269+
.. math::
270+
\frac{
271+
\einstancetype \subtypeof \einstancetype'
272+
}{
273+
\EEMDINSTANCE~\einstancetype \subtypeof \EEMDINSTANCE~\einstancetype'
274+
}
275+
276+
:math:`\EEMDCOMPONENT~\ecomponenttype`
277+
......................................
278+
279+
* An extern descriptor :math:`\EEMDCOMPONENT~\ecomponenttype` is a subtype of
280+
:math:`\EEMDCOMPONENT~\ecomponenttype'` if :math:`\ecomponenttype` is a subtype of
281+
:math:`\ecomponenttype'`.
282+
283+
.. math::
284+
\frac{
285+
\ecomponenttype \subtypeof \ecomponenttype'
286+
}{
287+
\EEMDCOMPONENT~\ecomponenttype \subtypeof \EEMDCOMPONENT~\ecomponenttype'
288+
}
289+
290+
291+
Instance types
292+
~~~~~~~~~~~~~~
293+
294+
* An instance type :math:`\overline{{\eexterndecl}_i}` is a subtype of
295+
an instance type :math:`\overline{{\eexterndecl'}_j}` if:
296+
297+
+ For each :math:`j`, there exists some :math:`i` such that
298+
:math:`{\eexterndecl}_i.\EEDNAME = {\eexterndecl'}_j.\EEDNAME` and
299+
:math:`{\eexterndecl}_i.\EEDDESC \subtypeof {\eexterndecl'}_j.\EEDDESC`.
300+
301+
.. math::
302+
\frac{
303+
\forall j, \exists i, {\eexterndecl}_i.\EEDNAME = {\eexterndecl'}_j.\EEDNAME \land {\eexterndecl}_i.\EEDDESC \subtypeof {\eexterndecl'}_j.\EEDDESC.
304+
}{
305+
\overline{{\eexterndecl}_i} \subtypeof \overline{{\eexterndecl'}_j}
306+
}
307+
308+
Component types
309+
~~~~~~~~~~~~~~~
310+
311+
* A component type :math:`\overline{{\eexterndecl}_i} \to
312+
\einstancetype` is a subtype of a
313+
:math:`\overline{{\eexterndecl'}_j} \to \einstancetype'` if:
314+
315+
+ For each :math:`i`, there exists some :math:`j`, such that
316+
:math:`{\eexterndecl'}_j.\EEDNAME = {\eexterndecl}_i.\EEDNAME` and
317+
:math:`{\eexterndecl'}_j.\EEDDESC \subtypeof {\eexterndecl}_i.\EEDDESC`;
318+
and
319+
320+
+ :math:`\einstancetype \subtypeof \einstancetype'`
321+
322+
.. math::
323+
\frac{
324+
\begin{array}{@{}c@{}}
325+
\forall i, \exists j, {\eexterndecl'}_j.\EEDNAME = {\eexterndecl}_i.\EEDNAME \land {\eexterndecl'}_j.\EEDDESC \subtypeof {\eexterndecl}_i.\EEDDESC\\
326+
\einstancetype \subtypeof \einstancetype'
327+
\end{array}
328+
}{
329+
\overline{{\eexterndecl}_i} \to \einstancetype
330+
\subtypeof
331+
\overline{{\eexterndecl'}_j} \to \einstancetype'
332+
}

Diff for: ‎spec/document/valid/types.rst

+1,648
Large diffs are not rendered by default.

0 commit comments

Comments
 (0)
Please sign in to comment.