From 262d51793c450b526ea1e35c801b138b8c8de762 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 28 May 2024 10:53:50 +0200 Subject: [PATCH] Math for valid modules --- document/core/syntax/modules.rst | 7 +- document/core/syntax/types.rst | 1 - document/core/util/macros.def | 8 +- document/core/valid/modules.rst | 375 +++------------------- document/core/valid/types.rst | 2 - spectec/spec/wasm-2.0/6-typing.watsup | 4 +- spectec/spec/wasm-3.0/6-typing.watsup | 52 ++-- spectec/test-frontend/TEST.md | 84 ++--- spectec/test-latex/TEST.md | 58 ++-- spectec/test-middlend/TEST.md | 430 ++++++++++++++------------ spectec/test-splice/TEST.md | 1 + 11 files changed, 403 insertions(+), 619 deletions(-) diff --git a/document/core/syntax/modules.rst b/document/core/syntax/modules.rst index 7bc1372ffb..b62ee0962e 100644 --- a/document/core/syntax/modules.rst +++ b/document/core/syntax/modules.rst @@ -96,13 +96,16 @@ Conventions .. index:: ! type definition, type index, function type, aggregate type pair: abstract syntax; type definition +.. _syntax-type: .. _syntax-typedef: Types ~~~~~ -The ${:type} section of a module defines a list of :ref:`recursive types `, each of consisting of a list of :ref:`sub types ` referenced by individual :ref:`type indices `. -All :ref:`function ` or :ref:`aggregate ` types used in a module must be defined in this component. +The ${:type} section of a module defines a list of :ref:`recursive types `, each consisting of a list of :ref:`sub types ` referenced by individual :ref:`type indices `. +All :ref:`function ` or :ref:`aggregate ` types used in a module must be defined in this section. + +$${syntax: type} .. index:: ! function, ! local, function index, local index, type index, value type, expression, import diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst index 345991a9c3..c3b45998b2 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -1,6 +1,5 @@ .. index:: ! type, validation, instantiation, execution pair: abstract syntax; type -.. _syntax-type: Types ----- diff --git a/document/core/util/macros.def b/document/core/util/macros.def index dde511be04..39106636d6 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -184,6 +184,7 @@ .. |toF| mathdef:: \xref{syntax/types}{syntax-functype}{\rightarrow} .. |to| mathdef:: \mathrel{\xref{valid/conventions}{syntax-instrtype}{\rightarrow}} +.. |toM| mathdef:: \mathrel{\xref{valid/modules}{syntax-moduletype}{\rightarrow}} .. |BOTH| mathdef:: \xref{valid/conventions}{syntax-heaptype-ext}{\K{bot}} .. |BOT| mathdef:: \xref{valid/conventions}{syntax-valtype-ext}{\K{bot}} @@ -297,6 +298,7 @@ .. |instrtype| mathdef:: \xref{valid/conventions}{syntax-instrtype}{\X{instrtype}} .. |localtype| mathdef:: \xref{valid/conventions}{syntax-localtype}{\X{localtype}} .. |externtype| mathdef:: \xref{syntax/types}{syntax-externtype}{\X{externtype}} +.. |moduletype| mathdef:: \xref{syntax/types}{syntax-moduletype}{\X{moduletype}} .. Types, meta functions @@ -367,8 +369,9 @@ .. |MELEMS| mathdef:: \xref{syntax/modules}{syntax-module}{\K{elems}} .. |MSTART| mathdef:: \xref{syntax/modules}{syntax-module}{\K{start}} +.. |TYPE| mathdef:: \xref{syntax/modules}{syntax-type}{\K{type}} .. |FUNC| mathdef:: \xref{syntax/modules}{syntax-func}{\K{func}} -.. |LOCAL| mathdef:: \xref{syntax/modules}{syntax-func}{\K{local}} +.. |LOCAL| mathdef:: \xref{syntax/modules}{syntax-local}{\K{local}} .. |FTYPE| mathdef:: \xref{syntax/modules}{syntax-func}{\K{type}} .. |FLOCALS| mathdef:: \xref{syntax/modules}{syntax-func}{\K{locals}} .. |FBODY| mathdef:: \xref{syntax/modules}{syntax-func}{\K{body}} @@ -1214,6 +1217,9 @@ .. |CONSTexprconst| mathdef:: \xref{valid/instructions}{valid-const}{\K{const}} .. |CONSTexprokconst| mathdef:: \xref{valid/instructions}{valid-const}{\K{const}} +.. |vdashexternidx| mathdef:: \xref{valid/modules}{valid-exxternidx}{\vdash} + +.. |vdashtype| mathdef:: \xref{valid/modules}{valid-type}{\vdash} .. |vdashtypes| mathdef:: \xref{valid/modules}{valid-types}{\vdash} .. |vdashfunc| mathdef:: \xref{valid/modules}{valid-func}{\vdash} .. |vdashlocal| mathdef:: \xref{valid/modules}{valid-local}{\vdash} diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 05a8b4f028..ae1a0f7335 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -8,12 +8,19 @@ Furthermore, most definitions are themselves classified with a suitable type. .. index:: type, type index, defined type, recursive type pair: abstract syntax; type single: abstract syntax; type +.. _valid-type: .. _valid-types: Types ~~~~~ -The sequence of :ref:`types ` defined in a module is validated incrementally, yielding a suitable :ref:`context `. +The sequence of :ref:`types ` defined in a module is validated incrementally, yielding a sequence of :ref:`defined types ` representing them individually. + +:math:`\type` +............. + +$${rule: Type_ok} + :math:`\type^\ast` .................. @@ -40,37 +47,18 @@ The sequence of :ref:`types ` defined in a module is validated incr * Then the type sequence is valid. -.. math:: - \frac{ - }{ - \{\} \vdashtypes \epsilon : \OKtypes - } - -.. math:: - \frac{ - C' \vdashtypes \type^\ast : \OKtypes - \qquad - C = C' \with \CTYPES = C'.\CTYPES~\rolldt_{|C'.\CTYPES|}^\ast(\rectype) - \qquad - C \vdashrectype \rectype : {\OKrectype}(|C'.\CTYPES|) - }{ - C \vdashtypes \type^\ast~\rectype : \OKtypes - } - -.. note:: - Despite the appearance, the context :math:`C` is effectively an _output_ of this judgement. +$${rule: Types_ok/*} .. index:: function, local, function index, local index, type index, function type, value type, local type, expression, import pair: abstract syntax; function single: abstract syntax; function -.. _valid-local: .. _valid-func: Functions ~~~~~~~~~ -Functions :math:`\func` are classified by :ref:`defined types ` that :ref:`expand ` to :ref:`function types ` of the form :math:`\TFUNC~[t_1^\ast] \toF [t_2^\ast]`. +Functions ${:func} are classified by :ref:`defined types ` that :ref:`expand ` to :ref:`function types ` of the form ${comptype: FUNC (t_1* -> t_2*)}. :math:`\{ \FTYPE~x, \FLOCALS~t^\ast, \FBODY~\expr \}` @@ -82,7 +70,7 @@ Functions :math:`\func` are classified by :ref:`defined types ` * For each local declared by a :ref:`value type ` :math:`t` in :math:`t^\ast`: - * The local for type :math:`t` must be :ref:`valid ` with :ref:`local type ` :math:`\localtype_i`. + * The local for type :math:`t` must be :ref:`valid ` with :ref:`local type ` :math:`\localtype_i`. * Let :math:`\localtype^\ast` be the concatenation of all :math:`\localtype_i`. @@ -100,27 +88,18 @@ Functions :math:`\func` are classified by :ref:`defined types ` * Then the function definition is valid with type :math:`C.\CTYPES[x]`. -.. math:: - \frac{ - \expanddt(C.\CTYPES[x]) = \TFUNC~[t_1^\ast] \toF [t_2^\ast] - \qquad - (C \vdashlocal \{\LTYPE~t\} : \init~t)^\ast - \qquad - C,\CLOCALS\,(\SET~t_1)^\ast~(\init~t)^\ast,\CLABELS~[t_2^\ast],\CRETURN~[t_2^\ast] \vdashexpr \expr : [t_2^\ast] - }{ - C \vdashfunc \{ \FTYPE~x, \FLOCALS~\{\LTYPE~t\}^\ast, \FBODY~\expr \} : C.\CTYPES[x] - } +$${rule: Func_ok Local_ok} .. index:: local, local type, value type pair: validation; local single: abstract syntax; local -.. _valid-localtype: +.. _valid-local: Locals ~~~~~~ -:ref:`Locals ` are classified with :ref:`local types `. +Locals ${:local} are classified with :ref:`local types `. :math:`\{ \LTYPE~\valtype \}` ............................. @@ -135,21 +114,7 @@ Locals * The local is valid with :ref:`local type ` :math:`\UNSET~\valtype`. -.. math:: - \frac{ - C \vdashvaltype t : \OKvaltype - \qquad - C \vdashvaltype t \mathrel{\mbox{defaultable}} - }{ - C \vdashlocal \{ \LTYPE~t \} : \SET~t - } - -.. math:: - \frac{ - C \vdashvaltype t : \OKvaltype - }{ - C \vdashlocal \{ \LTYPE~t \} : \UNSET~t - } +$${rule: Local_ok/*} .. note:: For cases where both rules are applicable, the former yields the more permissable type. @@ -163,7 +128,7 @@ Locals Tables ~~~~~~ -Tables :math:`\table` are classified by :ref:`table types `. +Tables ${:table} are classified by :ref:`table types `. :math:`\{ \TTYPE~\tabletype, \TINIT~\expr \}` ............................................. @@ -178,18 +143,7 @@ Tables :math:`\table` are classified by :ref:`table types `. * Then the table definition is valid with type :math:`\tabletype`. -.. math:: - \frac{ - C \vdashtabletype \tabletype : \OKtabletype - \qquad - \tabletype = \limits~t - \qquad - C \vdashexpr \expr : [t] - \qquad - C \vdashexprconst \expr \CONSTexprconst - }{ - C \vdashtable \{ \TTYPE~\tabletype, \TINIT~\expr \} : \tabletype - } +$${rule: Table_ok} .. index:: memory, memory type @@ -200,7 +154,7 @@ Tables :math:`\table` are classified by :ref:`table types `. Memories ~~~~~~~~ -Memories :math:`\mem` are classified by :ref:`memory types `. +Memories ${:mem} are classified by :ref:`memory types `. :math:`\{ \MTYPE~\memtype \}` ............................. @@ -209,12 +163,7 @@ Memories :math:`\mem` are classified by :ref:`memory types `. * Then the memory definition is valid with type :math:`\memtype`. -.. math:: - \frac{ - C \vdashmemtype \memtype : \OKmemtype - }{ - C \vdashmem \{ \MTYPE~\memtype \} : \memtype - } +$${rule: Mem_ok} .. index:: global, global type, expression, constant @@ -226,7 +175,7 @@ Memories :math:`\mem` are classified by :ref:`memory types `. Globals ~~~~~~~ -Globals :math:`\global` are classified by :ref:`global types ` of the form :math:`\mut~t`. +Globals ${:global} are classified by :ref:`global types `. Sequences of globals are handled incrementally, such that each definition has access to previous definitions. @@ -242,16 +191,7 @@ Sequences of globals are handled incrementally, such that each definition has ac * Then the global definition is valid with type :math:`\mut~t`. -.. math:: - \frac{ - C \vdashglobaltype \mut~t : \OKglobaltype - \qquad - C \vdashexpr \expr : [t] - \qquad - C \vdashexprconst \expr \CONSTexprconst - }{ - C \vdashglobal \{ \GTYPE~\mut~t, \GINIT~\expr \} : \mut~t - } +$${rule: Global_ok} :math:`\global^\ast` @@ -269,21 +209,7 @@ Sequences of globals are handled incrementally, such that each definition has ac * Then the sequence is valid with the sequence of :ref:`global types ` consisting of :math:`\X{gt}_1` prepended to :math:`\X{gt}^\ast`. -.. math:: - ~\\ - \frac{ - }{ - C \vdashglobals \epsilon : \epsilon - } - \qquad - \frac{ - C \vdashglobal \global_1 : \X{gt}_1 - \qquad - C \compose \{\CGLOBALS~\X{gt}_1\} \vdashglobals \global^\ast : \X{gt}^\ast - }{ - C \vdashglobals \global_1~\global^\ast : \X{gt}_1~\X{gt}^\ast - } - +$${rule: Globals_ok/*} .. index:: element, table, table index, expression, constant, function index @@ -296,7 +222,7 @@ Sequences of globals are handled incrementally, such that each definition has ac Element Segments ~~~~~~~~~~~~~~~~ -Element segments :math:`\elem` are classified by the :ref:`reference type ` of their elements. +Element segments ${:elem} are classified by the :ref:`reference type ` of their elements. :math:`\{ \ETYPE~t, \EINIT~e^\ast, \EMODE~\elemmode \}` ....................................................... @@ -315,21 +241,7 @@ Element segments :math:`\elem` are classified by the :ref:`reference type ` :math:`t`. - -.. math:: - \frac{ - C \vdashreftype t : \OKreftype - \qquad - (C \vdashexpr e : [t])^\ast - \qquad - (C \vdashexprconst e \CONSTexprconst)^\ast - \qquad - C \vdashelemmode \elemmode : t' - \qquad - C \vdashreftypematch t \subreftypematch t' - }{ - C \vdashelem \{ \ETYPE~t, \EINIT~e^\ast, \EMODE~\elemmode \} : t - } +$${rule: Elem_ok} .. _valid-elemmode: @@ -339,12 +251,7 @@ Element segments :math:`\elem` are classified by the :ref:`reference type ` :ref:`reference type `. -.. math:: - \frac{ - C \vdashreftype \reftype : \OKreftype - }{ - C \vdashelemmode \EPASSIVE : \reftype - } +$${rule: Elemmode_ok/passive} :math:`\EACTIVE~\{ \ETABLE~x, \EOFFSET~\expr \}` @@ -360,31 +267,14 @@ Element segments :math:`\elem` are classified by the :ref:`reference type ` :math:`t`. -.. math:: - \frac{ - \begin{array}{@{}c@{}} - C.\CTABLES[x] = \limits~t - \\ - C \vdashexpr \expr : [\I32] - \qquad - C \vdashexprconst \expr \CONSTexprconst - \end{array} - }{ - C \vdashelemmode \EACTIVE~\{ \ETABLE~x, \EOFFSET~\expr \} : t - } +$${rule: Elemmode_ok/active} :math:`\EDECLARE` ................. * The element mode is valid with any :ref:`valid ` :ref:`reference type `. -.. math:: - \frac{ - C \vdashreftype \reftype : \OKreftype - }{ - C \vdashelemmode \EDECLARE : \reftype - } - +$${rule: Elemmode_ok/declare} .. index:: data, memory, memory index, expression, constant, byte @@ -398,7 +288,7 @@ Element segments :math:`\elem` are classified by the :ref:`reference type `. +Exports ${:export} are classified by their :ref:`external type `. :math:`\{ \ENAME~\name, \EDESC~\exportdesc \}` @@ -499,12 +366,7 @@ Exports :math:`\export` and export descriptions :math:`\exportdesc` are classifi * Then the export is valid with :ref:`external type ` :math:`\externtype`. -.. math:: - \frac{ - C \vdashexportdesc \exportdesc : \externtype - }{ - C \vdashexport \{ \ENAME~\name, \EDESC~\exportdesc \} : \externtype - } +$${rule: Export_ok} :math:`\EDFUNC~x` @@ -516,12 +378,7 @@ Exports :math:`\export` and export descriptions :math:`\exportdesc` are classifi * Then the export description is valid with :ref:`external type ` :math:`\ETFUNC~\X{dt}`. -.. math:: - \frac{ - C.\CFUNCS[x] = \X{dt} - }{ - C \vdashexportdesc \EDFUNC~x : \ETFUNC~\X{dt} - } +$${rule: Externidx_ok/func} :math:`\EDTABLE~x` @@ -531,12 +388,7 @@ Exports :math:`\export` and export descriptions :math:`\exportdesc` are classifi * Then the export description is valid with :ref:`external type ` :math:`\ETTABLE~C.\CTABLES[x]`. -.. math:: - \frac{ - C.\CTABLES[x] = \tabletype - }{ - C \vdashexportdesc \EDTABLE~x : \ETTABLE~\tabletype - } +$${rule: Externidx_ok/table} :math:`\EDMEM~x` @@ -546,12 +398,7 @@ Exports :math:`\export` and export descriptions :math:`\exportdesc` are classifi * Then the export description is valid with :ref:`external type ` :math:`\ETMEM~C.\CMEMS[x]`. -.. math:: - \frac{ - C.\CMEMS[x] = \memtype - }{ - C \vdashexportdesc \EDMEM~x : \ETMEM~\memtype - } +$${rule: Externidx_ok/mem} :math:`\EDGLOBAL~x` @@ -561,12 +408,8 @@ Exports :math:`\export` and export descriptions :math:`\exportdesc` are classifi * Then the export description is valid with :ref:`external type ` :math:`\ETGLOBAL~C.\CGLOBALS[x]`. -.. math:: - \frac{ - C.\CGLOBALS[x] = \globaltype - }{ - C \vdashexportdesc \EDGLOBAL~x : \ETGLOBAL~\globaltype - } +$${rule: Externidx_ok/global} + .. index:: import, name, function type, table type, memory type, global type @@ -578,7 +421,7 @@ Exports :math:`\export` and export descriptions :math:`\exportdesc` are classifi Imports ~~~~~~~ -Imports :math:`\import` and import descriptions :math:`\importdesc` are classified by :ref:`external types `. +Imports ${:import} are classified by :ref:`external types `. :math:`\{ \IMODULE~\name_1, \INAME~\name_2, \IDESC~\importdesc \}` @@ -588,72 +431,7 @@ Imports :math:`\import` and import descriptions :math:`\importdesc` are classifi * Then the import is valid with type :math:`\externtype`. -.. math:: - \frac{ - C \vdashimportdesc \importdesc : \externtype - }{ - C \vdashimport \{ \IMODULE~\name_1, \INAME~\name_2, \IDESC~\importdesc \} : \externtype - } - - -:math:`\IDFUNC~x` -................. - -* The :ref:`defined type ` :math:`C.\CTYPES[x]` must be a :ref:`function type `. - -* Then the import description is valid with type :math:`\ETFUNC~C.\CTYPES[x]`. - -.. math:: - \frac{ - \expanddt(C.\CTYPES[x]) = \TFUNC~\functype - }{ - C \vdashimportdesc \IDFUNC~x : \ETFUNC~C.\CTYPES[x] - } - - -:math:`\IDTABLE~\tabletype` -........................... - -* The table type :math:`\tabletype` must be :ref:`valid `. - -* Then the import description is valid with type :math:`\ETTABLE~\tabletype`. - -.. math:: - \frac{ - C \vdashtable \tabletype : \OKtabletype - }{ - C \vdashimportdesc \IDTABLE~\tabletype : \ETTABLE~\tabletype - } - - -:math:`\IDMEM~\memtype` -....................... - -* The memory type :math:`\memtype` must be :ref:`valid `. - -* Then the import description is valid with type :math:`\ETMEM~\memtype`. - -.. math:: - \frac{ - C \vdashmemtype \memtype : \OKmemtype - }{ - C \vdashimportdesc \IDMEM~\memtype : \ETMEM~\memtype - } - - -:math:`\IDGLOBAL~\globaltype` -............................. - -* The global type :math:`\globaltype` must be :ref:`valid `. - -* Then the import description is valid with type :math:`\ETGLOBAL~\globaltype`. - -.. math:: - \frac{ - C \vdashglobaltype \globaltype : \OKglobaltype - }{ - C \vdashimportdesc \IDGLOBAL~\globaltype : \ETGLOBAL~\globaltype - } +$${rule: Import_ok} .. index:: module, type definition, function type, function, table, memory, global, element, data, start function, import, export, context @@ -669,7 +447,7 @@ Modules are classified by their mapping from the :ref:`external types ` is required. -Instead, the context :math:`C` for validation of the module's content is constructed from the definitions in the module. +Instead, the :ref:`context ` ${:C} for validation of the module's content is constructed from the definitions in the module. The :ref:`external types ` classifying a module may contain free :ref:`type indices ` that refer to types defined within the module. @@ -772,70 +550,17 @@ The :ref:`external types ` classifying a module may contain f * Then the module is valid with :ref:`external types ` :math:`\X{it}^\ast \to \X{et}^\ast`. -.. math:: - \frac{ - \begin{array}{@{}c@{}} - C_0 \vdashtypes \type^\ast : \OKtypes - \quad - C' \vdashglobals \global^\ast : \X{gt}^\ast - \quad - (C' \vdashtable \table : \X{tt})^\ast - \quad - (C' \vdashmem \mem : \X{mt})^\ast - \quad - (C \vdashfunc \func : \X{dt})^\ast - \\ - (C \vdashelem \elem : \X{rt})^\ast - \quad - (C \vdashdata \data : \X{ok})^\ast - \quad - (C \vdashstart \start : \OKstart)^? - \quad - (C \vdashimport \import : \X{it})^\ast - \quad - (C \vdashexport \export : \X{et})^\ast - \\ - \X{idt}^\ast = \funcsxt(\X{it}^\ast) - \qquad - \X{itt}^\ast = \tablesxt(\X{it}^\ast) - \qquad - \X{imt}^\ast = \memsxt(\X{it}^\ast) - \qquad - \X{igt}^\ast = \globalsxt(\X{it}^\ast) - \\ - x^\ast = \freefuncidx(\module \with \MFUNCS = \epsilon \with \MSTART = \epsilon) - \\ - C = \{ \CTYPES~C_0.\CTYPES, \CFUNCS~\X{idt}^\ast\,\X{dt}^\ast, \CTABLES~\X{itt}^\ast\,\X{tt}^\ast, \CMEMS~\X{imt}^\ast\,\X{mt}^\ast, \CGLOBALS~\X{igt}^\ast\,\X{gt}^\ast, \CELEMS~\X{rt}^\ast, \CDATAS~\X{ok}^\ast, \CREFS~x^\ast \} - \\ - C' = \{ \CTYPES~C_0.\CTYPES, \CGLOBALS~\X{igt}^\ast, \CFUNCS~(C.\CFUNCS), \CREFS~(C.\CREFS) \} - \qquad - (\export.\ENAME)^\ast ~\F{disjoint} - \\ - \module = \{ - \begin{array}[t]{@{}l@{}} - \MTYPES~\type^\ast, - \MFUNCS~\func^\ast, - \MTABLES~\table^\ast, - \MMEMS~\mem^\ast, - \MGLOBALS~\global^\ast, \\ - \MELEMS~\elem^\ast, - \MDATAS~\data^n, - \MSTART~\start^?, - \MIMPORTS~\import^\ast, - \MEXPORTS~\export^\ast \} - \end{array} - \end{array} - }{ - \vdashmodule \module : \X{it}^\ast \to \X{et}^\ast - } +$${rule: Module_ok} + +.. todo:: Check refs; check export names .. note:: All functions in a module are mutually recursive. - Consequently, the definition of the :ref:`context ` :math:`C` in this rule is recursive: + Consequently, the definition of the :ref:`context ` ${:C} in this rule is recursive: it depends on the outcome of validation of the function, table, memory, and global definitions contained in the module, - which itself depends on :math:`C`. + which itself depends on ${:C}. However, this recursion is just a specification device. - All types needed to construct :math:`C` can easily be determined from a simple pre-pass over the module that does not perform any actual validation. + All types needed to construct ${:C} can easily be determined from a simple pre-pass over the module that does not perform any actual validation. Globals, however, are not recursive but evaluated sequentially, such that each :ref:`constant expressions ` only has access to imported or previously defined globals. diff --git a/document/core/valid/types.rst b/document/core/valid/types.rst index be17706bc7..2e3f9c7dac 100644 --- a/document/core/valid/types.rst +++ b/document/core/valid/types.rst @@ -1,5 +1,3 @@ -.. _valid-type: - Types ----- diff --git a/spectec/spec/wasm-2.0/6-typing.watsup b/spectec/spec/wasm-2.0/6-typing.watsup index 48f3a02caa..4cd09c88cf 100644 --- a/spectec/spec/wasm-2.0/6-typing.watsup +++ b/spectec/spec/wasm-2.0/6-typing.watsup @@ -582,7 +582,7 @@ rule Data_ok: rule Elemmode_ok/active: C |- ACTIVE x expr : rt -- if C.TABLES[x] = lim rt - -- (Expr_ok_const: C |- expr : I32 CONST)* + -- Expr_ok_const: C |- expr : I32 CONST rule Elemmode_ok/passive: C |- PASSIVE : rt @@ -593,7 +593,7 @@ rule Elemmode_ok/declare: rule Datamode_ok/active: C |- ACTIVE 0 expr : OK -- if C.MEMS[0] = mt - -- (Expr_ok_const: C |- expr : I32 CONST)* + -- Expr_ok_const: C |- expr : I32 CONST rule Datamode_ok/passive: C |- PASSIVE : OK diff --git a/spectec/spec/wasm-3.0/6-typing.watsup b/spectec/spec/wasm-3.0/6-typing.watsup index e83d1b608d..1978e25a95 100644 --- a/spectec/spec/wasm-3.0/6-typing.watsup +++ b/spectec/spec/wasm-3.0/6-typing.watsup @@ -1211,25 +1211,26 @@ rule Func_ok: -- Expr_ok: C, LOCALS (SET t_1)* lct*, LABELS (t_2*), RETURN (t_2*) |- expr : t_2* rule Global_ok: - C |- GLOBAL gt expr : gt + C |- GLOBAL globaltype expr : globaltype -- Globaltype_ok: C |- gt : OK - -- if gt = mut t + -- if globaltype = mut t -- Expr_ok_const: C |- expr : t CONST rule Table_ok: - C |- TABLE tt expr : tt + C |- TABLE tabletype expr : tabletype -- Tabletype_ok: C |- tt : OK - -- if tt = limits rt + -- if tabletype = lim rt -- Expr_ok_const: C |- expr : rt CONST rule Mem_ok: - C |- MEMORY mt : mt - -- Memtype_ok: C |- mt : OK + C |- MEMORY memtype : memtype + -- Memtype_ok: C |- memtype : OK rule Elem_ok: - C |- ELEM rt expr* elemmode : rt - -- (Expr_ok_const: C |- expr : rt CONST)* - -- Elemmode_ok: C |- elemmode : rt + C |- ELEM reftype expr* elemmode : reftype + -- Reftype_ok: C |- reftype : OK + -- (Expr_ok_const: C |- expr : reftype CONST)* + -- Elemmode_ok: C |- elemmode : reftype rule Data_ok: C |- DATA b* datamode : OK @@ -1237,8 +1238,9 @@ rule Data_ok: rule Elemmode_ok/active: C |- ACTIVE x expr : rt - -- if C.TABLES[x] = lim rt - -- (Expr_ok_const: C |- expr : I32 CONST)* + -- if C.TABLES[x] = lim rt' + -- Reftype_sub: C |- rt <: rt' + -- Expr_ok_const: C |- expr : I32 CONST rule Elemmode_ok/passive: C |- PASSIVE : rt @@ -1249,7 +1251,7 @@ rule Elemmode_ok/declare: rule Datamode_ok/active: C |- ACTIVE x expr : OK -- if C.MEMS[x] = mt - -- (Expr_ok_const: C |- expr : I32 CONST)* + -- Expr_ok_const: C |- expr : I32 CONST rule Datamode_ok/passive: C |- PASSIVE : OK @@ -1293,15 +1295,17 @@ rule Externidx_ok/mem: ;; Modules proper -relation Module_ok: |- module : OK hint(show "T-module") hint(macro "%module") +syntax moduletype hint(desc "module type") = externtype* -> externtype* hint(macro "toM") + +relation Module_ok: |- module : moduletype hint(show "T-module") hint(macro "%module") relation Types_ok: context |- type* : deftype* hint(show "T-types") hint(macro "%types") relation Globals_ok: context |- global* : globaltype* hint(show "T-globals") hint(macro "%globals") ;; TODO: refs rule Module_ok: - |- MODULE type* import* func* global* table* mem* elem* data^n start? export* : OK + |- MODULE type* import* func* global* table* mem* elem* data* start? export* : xt_I* -> xt_E* -- Types_ok: {} |- type* : dt'* - -- (Import_ok: {TYPES dt'*} |- import : ixt)* + -- (Import_ok: {TYPES dt'*} |- import : xt_I)* ---- -- Globals_ok: C' |- global* : gt* -- (Table_ok: C' |- table : tt)* @@ -1309,19 +1313,19 @@ rule Module_ok: -- (Func_ok: C |- func : dt)* ---- -- (Elem_ok: C |- elem : rt)* - -- (Data_ok: C |- data : OK)^n + -- (Data_ok: C |- data : ok)* -- (Start_ok: C |- start : OK)? - -- (Export_ok: C |- export : xt)* + -- (Export_ok: C |- export : xt_E)* ;; -- TODO: disjoint export names ---- - -- if C = {TYPES dt'*, FUNCS idt* dt*, GLOBALS igt* gt*, TABLES itt* tt*, MEMS imt* mt*, ELEMS rt*, DATAS OK^n} + -- if C = {TYPES dt'*, FUNCS dt_I* dt*, GLOBALS gt_I* gt*, TABLES tt_I* tt*, MEMS mt_I* mt*, ELEMS rt*, DATAS ok*} ---- - -- if C' = {TYPES dt'*, FUNCS idt* dt*, GLOBALS igt*} + -- if C' = {TYPES dt'*, FUNCS dt_I* dt*, GLOBALS gt_I*} ---- - -- if idt* = $funcsxt(ixt*) - -- if igt* = $globalsxt(ixt*) - -- if itt* = $tablesxt(ixt*) - -- if imt* = $memsxt(ixt*) + -- if dt_I* = $funcsxt(xt_I*) + -- if gt_I* = $globalsxt(xt_I*) + -- if tt_I* = $tablesxt(xt_I*) + -- if mt_I* = $memsxt(xt_I*) rule Types_ok/empty: @@ -1329,7 +1333,7 @@ rule Types_ok/empty: rule Types_ok/cons: C |- type_1 type* : dt_1* dt* - -- Type_ok: C |- type_1 : dt_1 + -- Type_ok: C |- type_1 : dt_1* -- Types_ok: C[.TYPES =.. dt_1*] |- type* : dt* rule Globals_ok/empty: diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index 2fd9c92987..e2c1be0fc9 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -4269,35 +4269,36 @@ relation Func_ok: `%|-%:%`(context, func, deftype) ;; 6-typing.watsup relation Global_ok: `%|-%:%`(context, global, globaltype) ;; 6-typing.watsup - rule _{C : context, gt : globaltype, expr : expr, mut : mut, t : valtype}: - `%|-%:%`(C, GLOBAL_global(gt, expr), gt) + rule _{C : context, globaltype : globaltype, expr : expr, gt : globaltype, mut : mut, t : valtype}: + `%|-%:%`(C, GLOBAL_global(globaltype, expr), globaltype) -- Globaltype_ok: `%|-%:OK`(C, gt) - -- if (gt = `%%`_globaltype(mut, t)) + -- if (globaltype = `%%`_globaltype(mut, t)) -- Expr_ok_const: `%|-%:%CONST`(C, expr, t) ;; 6-typing.watsup relation Table_ok: `%|-%:%`(context, table, tabletype) ;; 6-typing.watsup - rule _{C : context, tt : tabletype, expr : expr, limits : limits, rt : reftype}: - `%|-%:%`(C, TABLE_table(tt, expr), tt) + rule _{C : context, tabletype : tabletype, expr : expr, tt : tabletype, lim : limits, rt : reftype}: + `%|-%:%`(C, TABLE_table(tabletype, expr), tabletype) -- Tabletype_ok: `%|-%:OK`(C, tt) - -- if (tt = `%%`_tabletype(limits, rt)) + -- if (tabletype = `%%`_tabletype(lim, rt)) -- Expr_ok_const: `%|-%:%CONST`(C, expr, (rt : reftype <: valtype)) ;; 6-typing.watsup relation Mem_ok: `%|-%:%`(context, mem, memtype) ;; 6-typing.watsup - rule _{C : context, mt : memtype}: - `%|-%:%`(C, MEMORY_mem(mt), mt) - -- Memtype_ok: `%|-%:OK`(C, mt) + rule _{C : context, memtype : memtype}: + `%|-%:%`(C, MEMORY_mem(memtype), memtype) + -- Memtype_ok: `%|-%:OK`(C, memtype) ;; 6-typing.watsup relation Elemmode_ok: `%|-%:%`(context, elemmode, reftype) ;; 6-typing.watsup - rule active{C : context, x : idx, expr : expr, rt : reftype, lim : limits}: + rule active{C : context, x : idx, expr : expr, rt : reftype, lim : limits, rt' : reftype}: `%|-%:%`(C, ACTIVE_elemmode(x, expr), rt) - -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - -- (Expr_ok_const: `%|-%:%CONST`(C, expr, I32_valtype))*{} + -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt')) + -- Reftype_sub: `%|-%<:%`(C, rt, rt') + -- Expr_ok_const: `%|-%:%CONST`(C, expr, I32_valtype) ;; 6-typing.watsup rule passive{C : context, rt : reftype}: @@ -4310,10 +4311,11 @@ relation Elemmode_ok: `%|-%:%`(context, elemmode, reftype) ;; 6-typing.watsup relation Elem_ok: `%|-%:%`(context, elem, reftype) ;; 6-typing.watsup - rule _{C : context, rt : reftype, expr* : expr*, elemmode : elemmode}: - `%|-%:%`(C, ELEM_elem(rt, expr*{expr : expr}, elemmode), rt) - -- (Expr_ok_const: `%|-%:%CONST`(C, expr, (rt : reftype <: valtype)))*{expr : expr} - -- Elemmode_ok: `%|-%:%`(C, elemmode, rt) + rule _{C : context, reftype : reftype, expr* : expr*, elemmode : elemmode}: + `%|-%:%`(C, ELEM_elem(reftype, expr*{expr : expr}, elemmode), reftype) + -- Reftype_ok: `%|-%:OK`(C, reftype) + -- (Expr_ok_const: `%|-%:%CONST`(C, expr, (reftype : reftype <: valtype)))*{expr : expr} + -- Elemmode_ok: `%|-%:%`(C, elemmode, reftype) ;; 6-typing.watsup relation Datamode_ok: `%|-%:OK`(context, datamode) @@ -4321,7 +4323,7 @@ relation Datamode_ok: `%|-%:OK`(context, datamode) rule active{C : context, x : idx, expr : expr, mt : memtype}: `%|-%:OK`(C, ACTIVE_datamode(x, expr)) -- if (C.MEMS_context[x!`%`_idx.0] = mt) - -- (Expr_ok_const: `%|-%:%CONST`(C, expr, I32_valtype))*{} + -- Expr_ok_const: `%|-%:%CONST`(C, expr, I32_valtype) ;; 6-typing.watsup rule passive{C : context}: @@ -4377,16 +4379,20 @@ relation Export_ok: `%|-%:%`(context, export, externtype) `%|-%:%`(C, EXPORT_export(name, externidx), xt) -- Externidx_ok: `%|-%:%`(C, externidx, xt) +;; 6-typing.watsup +syntax moduletype = + | `%->%`{externtype* : externtype*}(externtype*{externtype : externtype} : externtype*, externtype*) + ;; 6-typing.watsup rec { -;; 6-typing.watsup:1298.1-1298.100 +;; 6-typing.watsup:1302.1-1302.100 relation Globals_ok: `%|-%:%`(context, global*, globaltype*) - ;; 6-typing.watsup:1335.1-1336.17 + ;; 6-typing.watsup:1339.1-1340.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1338.1-1341.55 + ;; 6-typing.watsup:1342.1-1345.55 rule cons{C : context, global_1 : global, global : global, gt_1 : globaltype, gt* : globaltype*}: `%|-%:%`(C, [global_1] :: global*{}, [gt_1] :: gt*{gt : globaltype}) -- Global_ok: `%|-%:%`(C, global, gt_1) @@ -4396,40 +4402,40 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*) ;; 6-typing.watsup rec { -;; 6-typing.watsup:1297.1-1297.98 +;; 6-typing.watsup:1301.1-1301.98 relation Types_ok: `%|-%:%`(context, type*, deftype*) - ;; 6-typing.watsup:1327.1-1328.17 + ;; 6-typing.watsup:1331.1-1332.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1330.1-1333.50 - rule cons{C : context, type_1 : type, type* : type*, dt_1 : deftype, dt* : deftype*}: - `%|-%:%`(C, [type_1] :: type*{type : type}, dt_1*{} :: dt*{dt : deftype}) - -- Type_ok: `%|-%:%`(C, type_1, [dt_1]) - -- Types_ok: `%|-%:%`(C[TYPES_context =.. dt_1*{}], type*{type : type}, dt*{dt : deftype}) + ;; 6-typing.watsup:1334.1-1337.50 + rule cons{C : context, type_1 : type, type* : type*, dt_1* : deftype*, dt* : deftype*}: + `%|-%:%`(C, [type_1] :: type*{type : type}, dt_1*{dt_1 : deftype} :: dt*{dt : deftype}) + -- Type_ok: `%|-%:%`(C, type_1, dt_1*{dt_1 : deftype}) + -- Types_ok: `%|-%:%`(C[TYPES_context =.. dt_1*{dt_1 : deftype}], type*{type : type}, dt*{dt : deftype}) } ;; 6-typing.watsup -relation Module_ok: `|-%:OK`(module) +relation Module_ok: `|-%:%`(module, moduletype) ;; 6-typing.watsup - rule _{type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data^n : data^n, n : n, start? : start?, export* : export*, dt'* : deftype*, ixt* : externtype*, C' : context, gt* : globaltype*, tt* : tabletype*, mt* : memtype*, C : context, dt* : deftype*, rt* : reftype*, xt* : externtype*, idt* : deftype*, igt* : globaltype*, itt* : tabletype*, imt* : memtype*}: - `|-%:OK`(MODULE_module(type*{type : type}, import*{import : import}, func*{func : func}, global*{global : global}, table*{table : table}, mem*{mem : mem}, elem*{elem : elem}, data^n{data : data}, start?{start : start}, export*{export : export})) + rule _{type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data* : data*, start? : start?, export* : export*, xt_I* : externtype*, xt_E* : externtype*, dt'* : deftype*, C' : context, gt* : globaltype*, tt* : tabletype*, mt* : memtype*, C : context, dt* : deftype*, rt* : reftype*, ok* : datatype*, dt_I* : deftype*, gt_I* : globaltype*, tt_I* : tabletype*, mt_I* : memtype*}: + `|-%:%`(MODULE_module(type*{type : type}, import*{import : import}, func*{func : func}, global*{global : global}, table*{table : table}, mem*{mem : mem}, elem*{elem : elem}, data*{data : data}, start?{start : start}, export*{export : export}), `%->%`_moduletype(xt_I*{xt_I : externtype}, xt_E*{xt_E : externtype})) -- Types_ok: `%|-%:%`({TYPES [], RECS [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}, type*{type : type}, dt'*{dt' : deftype}) - -- (Import_ok: `%|-%:%`({TYPES dt'*{dt' : deftype}, RECS [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}, import, ixt))*{import : import, ixt : externtype} + -- (Import_ok: `%|-%:%`({TYPES dt'*{dt' : deftype}, RECS [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}, import, xt_I))*{import : import, xt_I : externtype} -- Globals_ok: `%|-%:%`(C', global*{global : global}, gt*{gt : globaltype}) -- (Table_ok: `%|-%:%`(C', table, tt))*{table : table, tt : tabletype} -- (Mem_ok: `%|-%:%`(C', mem, mt))*{mem : mem, mt : memtype} -- (Func_ok: `%|-%:%`(C, func, dt))*{dt : deftype, func : func} -- (Elem_ok: `%|-%:%`(C, elem, rt))*{elem : elem, rt : reftype} - -- (Data_ok: `%|-%:%`(C, data, OK_datatype))^n{data : data} + -- (Data_ok: `%|-%:%`(C, data, ok))*{data : data, ok : datatype} -- (Start_ok: `%|-%:OK`(C, start))?{start : start} - -- (Export_ok: `%|-%:%`(C, export, xt))*{export : export, xt : externtype} - -- if (C = {TYPES dt'*{dt' : deftype}, RECS [], FUNCS idt*{idt : deftype} :: dt*{dt : deftype}, GLOBALS igt*{igt : globaltype} :: gt*{gt : globaltype}, TABLES itt*{itt : tabletype} :: tt*{tt : tabletype}, MEMS imt*{imt : memtype} :: mt*{mt : memtype}, ELEMS rt*{rt : reftype}, DATAS OK_datatype^n{}, LOCALS [], LABELS [], RETURN ?()}) - -- if (C' = {TYPES dt'*{dt' : deftype}, RECS [], FUNCS idt*{idt : deftype} :: dt*{dt : deftype}, GLOBALS igt*{igt : globaltype}, TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}) - -- if (idt*{idt : deftype} = $funcsxt(ixt*{ixt : externtype})) - -- if (igt*{igt : globaltype} = $globalsxt(ixt*{ixt : externtype})) - -- if (itt*{itt : tabletype} = $tablesxt(ixt*{ixt : externtype})) - -- if (imt*{imt : memtype} = $memsxt(ixt*{ixt : externtype})) + -- (Export_ok: `%|-%:%`(C, export, xt_E))*{export : export, xt_E : externtype} + -- if (C = {TYPES dt'*{dt' : deftype}, RECS [], FUNCS dt_I*{dt_I : deftype} :: dt*{dt : deftype}, GLOBALS gt_I*{gt_I : globaltype} :: gt*{gt : globaltype}, TABLES tt_I*{tt_I : tabletype} :: tt*{tt : tabletype}, MEMS mt_I*{mt_I : memtype} :: mt*{mt : memtype}, ELEMS rt*{rt : reftype}, DATAS ok*{ok : datatype}, LOCALS [], LABELS [], RETURN ?()}) + -- if (C' = {TYPES dt'*{dt' : deftype}, RECS [], FUNCS dt_I*{dt_I : deftype} :: dt*{dt : deftype}, GLOBALS gt_I*{gt_I : globaltype}, TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}) + -- if (dt_I*{dt_I : deftype} = $funcsxt(xt_I*{xt_I : externtype})) + -- if (gt_I*{gt_I : globaltype} = $globalsxt(xt_I*{xt_I : externtype})) + -- if (tt_I*{tt_I : tabletype} = $tablesxt(xt_I*{xt_I : externtype})) + -- if (mt_I*{mt_I : memtype} = $memsxt(xt_I*{xt_I : externtype})) ;; 7-runtime-typing.watsup relation Ref_ok: `%|-%:%`(store, ref, reftype) diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md index 144b419066..f8c19b8afd 100644 --- a/spectec/test-latex/TEST.md +++ b/spectec/test-latex/TEST.md @@ -6229,11 +6229,11 @@ $$ \frac{ C \vdash {\mathit{gt}} : \mathsf{ok} \qquad -{\mathit{gt}} = {\mathsf{mut}^?}~t +{\mathit{globaltype}} = {\mathsf{mut}^?}~t \qquad C \vdash {\mathit{expr}} : t~\mathsf{const} }{ -C \vdash \mathsf{global}~{\mathit{gt}}~{\mathit{expr}} : {\mathit{gt}} +C \vdash \mathsf{global}~{\mathit{globaltype}}~{\mathit{expr}} : {\mathit{globaltype}} } \, {[\textsc{\scriptsize T{-}global}]} \qquad \end{array} @@ -6244,11 +6244,11 @@ $$ \frac{ C \vdash {\mathit{tt}} : \mathsf{ok} \qquad -{\mathit{tt}} = {\mathit{limits}}~{\mathit{rt}} +{\mathit{tabletype}} = {\mathit{lim}}~{\mathit{rt}} \qquad C \vdash {\mathit{expr}} : {\mathit{rt}}~\mathsf{const} }{ -C \vdash \mathsf{table}~{\mathit{tt}}~{\mathit{expr}} : {\mathit{tt}} +C \vdash \mathsf{table}~{\mathit{tabletype}}~{\mathit{expr}} : {\mathit{tabletype}} } \, {[\textsc{\scriptsize T{-}table}]} \qquad \end{array} @@ -6257,9 +6257,9 @@ $$ $$ \begin{array}{@{}c@{}}\displaystyle \frac{ -C \vdash {\mathit{mt}} : \mathsf{ok} +C \vdash {\mathit{memtype}} : \mathsf{ok} }{ -C \vdash \mathsf{memory}~{\mathit{mt}} : {\mathit{mt}} +C \vdash \mathsf{memory}~{\mathit{memtype}} : {\mathit{memtype}} } \, {[\textsc{\scriptsize T{-}mem}]} \qquad \end{array} @@ -6268,11 +6268,13 @@ $$ $$ \begin{array}{@{}c@{}}\displaystyle \frac{ -(C \vdash {\mathit{expr}} : {\mathit{rt}}~\mathsf{const})^\ast +C \vdash {\mathit{reftype}} : \mathsf{ok} + \qquad +(C \vdash {\mathit{expr}} : {\mathit{reftype}}~\mathsf{const})^\ast \qquad -C \vdash {\mathit{elemmode}} : {\mathit{rt}} +C \vdash {\mathit{elemmode}} : {\mathit{reftype}} }{ -C \vdash \mathsf{elem}~{\mathit{rt}}~{{\mathit{expr}}^\ast}~{\mathit{elemmode}} : {\mathit{rt}} +C \vdash \mathsf{elem}~{\mathit{reftype}}~{{\mathit{expr}}^\ast}~{\mathit{elemmode}} : {\mathit{reftype}} } \, {[\textsc{\scriptsize T{-}elem}]} \qquad \end{array} @@ -6292,9 +6294,11 @@ $$ $$ \begin{array}{@{}c@{}}\displaystyle \frac{ -C{.}\mathsf{tables}{}[x] = {\mathit{lim}}~{\mathit{rt}} +C{.}\mathsf{tables}{}[x] = {\mathit{lim}}~{\mathit{rt}'} + \qquad +C \vdash {\mathit{rt}} \leq {\mathit{rt}'} \qquad -(C \vdash {\mathit{expr}} : \mathsf{i{\scriptstyle 32}}~\mathsf{const})^\ast +C \vdash {\mathit{expr}} : \mathsf{i{\scriptstyle 32}}~\mathsf{const} }{ C \vdash \mathsf{active}~x~{\mathit{expr}} : {\mathit{rt}} } \, {[\textsc{\scriptsize T{-}elemmode{-}active}]} @@ -6327,7 +6331,7 @@ $$ \frac{ C{.}\mathsf{mems}{}[x] = {\mathit{mt}} \qquad -(C \vdash {\mathit{expr}} : \mathsf{i{\scriptstyle 32}}~\mathsf{const})^\ast +C \vdash {\mathit{expr}} : \mathsf{i{\scriptstyle 32}}~\mathsf{const} }{ C \vdash \mathsf{active}~x~{\mathit{expr}} : \mathsf{ok} } \, {[\textsc{\scriptsize T{-}datamode{-}active}]} @@ -6434,7 +6438,13 @@ $$ \vspace{1ex} -$\boxed{{ \vdash }\;{\mathit{module}} : \mathsf{ok}}$ +$$ +\begin{array}{@{}lrrl@{}l@{}} +\mbox{(module type)} & {\mathit{moduletype}} &::=& {{\mathit{externtype}}^\ast} \rightarrow {{\mathit{externtype}}^\ast} \\ +\end{array} +$$ + +$\boxed{{ \vdash }\;{\mathit{module}} : {\mathit{moduletype}}}$ $\boxed{{\mathit{context}} \vdash {{\mathit{type}}^\ast} : {{\mathit{deftype}}^\ast}}$ @@ -6448,7 +6458,7 @@ $$ \}\end{array} \vdash {{\mathit{type}}^\ast} : {{\mathit{dt}'}^\ast} \qquad (\{ \begin{array}[t]{@{}l@{}} -\mathsf{types}~{{\mathit{dt}'}^\ast} \}\end{array} \vdash {\mathit{import}} : {\mathit{ixt}})^\ast +\mathsf{types}~{{\mathit{dt}'}^\ast} \}\end{array} \vdash {\mathit{import}} : {\mathit{xt}}_{\mathsf{i}})^\ast \\ {C'} \vdash {{\mathit{global}}^\ast} : {{\mathit{gt}}^\ast} \qquad @@ -6460,28 +6470,28 @@ $$ \\ (C \vdash {\mathit{elem}} : {\mathit{rt}})^\ast \qquad -(C \vdash {\mathit{data}} : \mathsf{ok})^{n} +(C \vdash {\mathit{data}} : {\mathit{ok}})^\ast \qquad (C \vdash {\mathit{start}} : \mathsf{ok})^? \qquad -(C \vdash {\mathit{export}} : {\mathit{xt}})^\ast +(C \vdash {\mathit{export}} : {\mathit{xt}}_{\mathsf{e}})^\ast \\ C = \{ \begin{array}[t]{@{}l@{}} -\mathsf{types}~{{\mathit{dt}'}^\ast},\; \mathsf{funcs}~{{\mathit{idt}}^\ast}~{{\mathit{dt}}^\ast},\; \mathsf{globals}~{{\mathit{igt}}^\ast}~{{\mathit{gt}}^\ast},\; \mathsf{tables}~{{\mathit{itt}}^\ast}~{{\mathit{tt}}^\ast},\; \mathsf{mems}~{{\mathit{imt}}^\ast}~{{\mathit{mt}}^\ast},\; \mathsf{elems}~{{\mathit{rt}}^\ast},\; \mathsf{datas}~{\mathsf{ok}^{n}} \}\end{array} +\mathsf{types}~{{\mathit{dt}'}^\ast},\; \mathsf{funcs}~{{\mathit{dt}}_{\mathsf{i}}^\ast}~{{\mathit{dt}}^\ast},\; \mathsf{globals}~{{\mathit{gt}}_{\mathsf{i}}^\ast}~{{\mathit{gt}}^\ast},\; \mathsf{tables}~{{\mathit{tt}}_{\mathsf{i}}^\ast}~{{\mathit{tt}}^\ast},\; \mathsf{mems}~{{\mathit{mt}}_{\mathsf{i}}^\ast}~{{\mathit{mt}}^\ast},\; \mathsf{elems}~{{\mathit{rt}}^\ast},\; \mathsf{datas}~{{\mathit{ok}}^\ast} \}\end{array} \\ {C'} = \{ \begin{array}[t]{@{}l@{}} -\mathsf{types}~{{\mathit{dt}'}^\ast},\; \mathsf{funcs}~{{\mathit{idt}}^\ast}~{{\mathit{dt}}^\ast},\; \mathsf{globals}~{{\mathit{igt}}^\ast} \}\end{array} +\mathsf{types}~{{\mathit{dt}'}^\ast},\; \mathsf{funcs}~{{\mathit{dt}}_{\mathsf{i}}^\ast}~{{\mathit{dt}}^\ast},\; \mathsf{globals}~{{\mathit{gt}}_{\mathsf{i}}^\ast} \}\end{array} \\ -{{\mathit{idt}}^\ast} = {\mathrm{funcs}}({{\mathit{ixt}}^\ast}) +{{\mathit{dt}}_{\mathsf{i}}^\ast} = {\mathrm{funcs}}({{\mathit{xt}}_{\mathsf{i}}^\ast}) \qquad -{{\mathit{igt}}^\ast} = {\mathrm{globals}}({{\mathit{ixt}}^\ast}) +{{\mathit{gt}}_{\mathsf{i}}^\ast} = {\mathrm{globals}}({{\mathit{xt}}_{\mathsf{i}}^\ast}) \qquad -{{\mathit{itt}}^\ast} = {\mathrm{tables}}({{\mathit{ixt}}^\ast}) +{{\mathit{tt}}_{\mathsf{i}}^\ast} = {\mathrm{tables}}({{\mathit{xt}}_{\mathsf{i}}^\ast}) \qquad -{{\mathit{imt}}^\ast} = {\mathrm{mems}}({{\mathit{ixt}}^\ast}) +{{\mathit{mt}}_{\mathsf{i}}^\ast} = {\mathrm{mems}}({{\mathit{xt}}_{\mathsf{i}}^\ast}) \end{array} }{ -{ \vdash }\;\mathsf{module}~{{\mathit{type}}^\ast}~{{\mathit{import}}^\ast}~{{\mathit{func}}^\ast}~{{\mathit{global}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{data}}^{n}}~{{\mathit{start}}^?}~{{\mathit{export}}^\ast} : \mathsf{ok} +{ \vdash }\;\mathsf{module}~{{\mathit{type}}^\ast}~{{\mathit{import}}^\ast}~{{\mathit{func}}^\ast}~{{\mathit{global}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{data}}^\ast}~{{\mathit{start}}^?}~{{\mathit{export}}^\ast} : {{\mathit{xt}}_{\mathsf{i}}^\ast} \rightarrow {{\mathit{xt}}_{\mathsf{e}}^\ast} } \, {[\textsc{\scriptsize T{-}module}]} \qquad \end{array} @@ -6502,7 +6512,7 @@ $$ $$ \begin{array}{@{}c@{}}\displaystyle \frac{ -C \vdash {\mathit{type}}_1 : {\mathit{dt}}_1 +C \vdash {\mathit{type}}_1 : {{\mathit{dt}}_1^\ast} \qquad C{}[{.}\mathsf{types} = ..{{\mathit{dt}}_1^\ast}] \vdash {{\mathit{type}}^\ast} : {{\mathit{dt}}^\ast} }{ diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md index 62cbb14e56..83afc6cd1c 100644 --- a/spectec/test-middlend/TEST.md +++ b/spectec/test-middlend/TEST.md @@ -4259,35 +4259,36 @@ relation Func_ok: `%|-%:%`(context, func, deftype) ;; 6-typing.watsup relation Global_ok: `%|-%:%`(context, global, globaltype) ;; 6-typing.watsup - rule _{C : context, gt : globaltype, expr : expr, mut : mut, t : valtype}: - `%|-%:%`(C, GLOBAL_global(gt, expr), gt) + rule _{C : context, globaltype : globaltype, expr : expr, gt : globaltype, mut : mut, t : valtype}: + `%|-%:%`(C, GLOBAL_global(globaltype, expr), globaltype) -- Globaltype_ok: `%|-%:OK`(C, gt) - -- if (gt = `%%`_globaltype(mut, t)) + -- if (globaltype = `%%`_globaltype(mut, t)) -- Expr_ok_const: `%|-%:%CONST`(C, expr, t) ;; 6-typing.watsup relation Table_ok: `%|-%:%`(context, table, tabletype) ;; 6-typing.watsup - rule _{C : context, tt : tabletype, expr : expr, limits : limits, rt : reftype}: - `%|-%:%`(C, TABLE_table(tt, expr), tt) + rule _{C : context, tabletype : tabletype, expr : expr, tt : tabletype, lim : limits, rt : reftype}: + `%|-%:%`(C, TABLE_table(tabletype, expr), tabletype) -- Tabletype_ok: `%|-%:OK`(C, tt) - -- if (tt = `%%`_tabletype(limits, rt)) + -- if (tabletype = `%%`_tabletype(lim, rt)) -- Expr_ok_const: `%|-%:%CONST`(C, expr, (rt : reftype <: valtype)) ;; 6-typing.watsup relation Mem_ok: `%|-%:%`(context, mem, memtype) ;; 6-typing.watsup - rule _{C : context, mt : memtype}: - `%|-%:%`(C, MEMORY_mem(mt), mt) - -- Memtype_ok: `%|-%:OK`(C, mt) + rule _{C : context, memtype : memtype}: + `%|-%:%`(C, MEMORY_mem(memtype), memtype) + -- Memtype_ok: `%|-%:OK`(C, memtype) ;; 6-typing.watsup relation Elemmode_ok: `%|-%:%`(context, elemmode, reftype) ;; 6-typing.watsup - rule active{C : context, x : idx, expr : expr, rt : reftype, lim : limits}: + rule active{C : context, x : idx, expr : expr, rt : reftype, lim : limits, rt' : reftype}: `%|-%:%`(C, ACTIVE_elemmode(x, expr), rt) - -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - -- (Expr_ok_const: `%|-%:%CONST`(C, expr, I32_valtype))*{} + -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt')) + -- Reftype_sub: `%|-%<:%`(C, rt, rt') + -- Expr_ok_const: `%|-%:%CONST`(C, expr, I32_valtype) ;; 6-typing.watsup rule passive{C : context, rt : reftype}: @@ -4300,10 +4301,11 @@ relation Elemmode_ok: `%|-%:%`(context, elemmode, reftype) ;; 6-typing.watsup relation Elem_ok: `%|-%:%`(context, elem, reftype) ;; 6-typing.watsup - rule _{C : context, rt : reftype, expr* : expr*, elemmode : elemmode}: - `%|-%:%`(C, ELEM_elem(rt, expr*{expr : expr}, elemmode), rt) - -- (Expr_ok_const: `%|-%:%CONST`(C, expr, (rt : reftype <: valtype)))*{expr : expr} - -- Elemmode_ok: `%|-%:%`(C, elemmode, rt) + rule _{C : context, reftype : reftype, expr* : expr*, elemmode : elemmode}: + `%|-%:%`(C, ELEM_elem(reftype, expr*{expr : expr}, elemmode), reftype) + -- Reftype_ok: `%|-%:OK`(C, reftype) + -- (Expr_ok_const: `%|-%:%CONST`(C, expr, (reftype : reftype <: valtype)))*{expr : expr} + -- Elemmode_ok: `%|-%:%`(C, elemmode, reftype) ;; 6-typing.watsup relation Datamode_ok: `%|-%:OK`(context, datamode) @@ -4311,7 +4313,7 @@ relation Datamode_ok: `%|-%:OK`(context, datamode) rule active{C : context, x : idx, expr : expr, mt : memtype}: `%|-%:OK`(C, ACTIVE_datamode(x, expr)) -- if (C.MEMS_context[x!`%`_idx.0] = mt) - -- (Expr_ok_const: `%|-%:%CONST`(C, expr, I32_valtype))*{} + -- Expr_ok_const: `%|-%:%CONST`(C, expr, I32_valtype) ;; 6-typing.watsup rule passive{C : context}: @@ -4367,16 +4369,20 @@ relation Export_ok: `%|-%:%`(context, export, externtype) `%|-%:%`(C, EXPORT_export(name, externidx), xt) -- Externidx_ok: `%|-%:%`(C, externidx, xt) +;; 6-typing.watsup +syntax moduletype = + | `%->%`{externtype* : externtype*}(externtype*{externtype : externtype} : externtype*, externtype*) + ;; 6-typing.watsup rec { -;; 6-typing.watsup:1298.1-1298.100 +;; 6-typing.watsup:1302.1-1302.100 relation Globals_ok: `%|-%:%`(context, global*, globaltype*) - ;; 6-typing.watsup:1335.1-1336.17 + ;; 6-typing.watsup:1339.1-1340.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1338.1-1341.55 + ;; 6-typing.watsup:1342.1-1345.55 rule cons{C : context, global_1 : global, global : global, gt_1 : globaltype, gt* : globaltype*}: `%|-%:%`(C, [global_1] :: global*{}, [gt_1] :: gt*{gt : globaltype}) -- Global_ok: `%|-%:%`(C, global, gt_1) @@ -4386,40 +4392,40 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*) ;; 6-typing.watsup rec { -;; 6-typing.watsup:1297.1-1297.98 +;; 6-typing.watsup:1301.1-1301.98 relation Types_ok: `%|-%:%`(context, type*, deftype*) - ;; 6-typing.watsup:1327.1-1328.17 + ;; 6-typing.watsup:1331.1-1332.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1330.1-1333.50 - rule cons{C : context, type_1 : type, type* : type*, dt_1 : deftype, dt* : deftype*}: - `%|-%:%`(C, [type_1] :: type*{type : type}, dt_1*{} :: dt*{dt : deftype}) - -- Type_ok: `%|-%:%`(C, type_1, [dt_1]) - -- Types_ok: `%|-%:%`(C[TYPES_context =.. dt_1*{}], type*{type : type}, dt*{dt : deftype}) + ;; 6-typing.watsup:1334.1-1337.50 + rule cons{C : context, type_1 : type, type* : type*, dt_1* : deftype*, dt* : deftype*}: + `%|-%:%`(C, [type_1] :: type*{type : type}, dt_1*{dt_1 : deftype} :: dt*{dt : deftype}) + -- Type_ok: `%|-%:%`(C, type_1, dt_1*{dt_1 : deftype}) + -- Types_ok: `%|-%:%`(C[TYPES_context =.. dt_1*{dt_1 : deftype}], type*{type : type}, dt*{dt : deftype}) } ;; 6-typing.watsup -relation Module_ok: `|-%:OK`(module) +relation Module_ok: `|-%:%`(module, moduletype) ;; 6-typing.watsup - rule _{type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data^n : data^n, n : n, start? : start?, export* : export*, dt'* : deftype*, ixt* : externtype*, C' : context, gt* : globaltype*, tt* : tabletype*, mt* : memtype*, C : context, dt* : deftype*, rt* : reftype*, xt* : externtype*, idt* : deftype*, igt* : globaltype*, itt* : tabletype*, imt* : memtype*}: - `|-%:OK`(MODULE_module(type*{type : type}, import*{import : import}, func*{func : func}, global*{global : global}, table*{table : table}, mem*{mem : mem}, elem*{elem : elem}, data^n{data : data}, start?{start : start}, export*{export : export})) + rule _{type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data* : data*, start? : start?, export* : export*, xt_I* : externtype*, xt_E* : externtype*, dt'* : deftype*, C' : context, gt* : globaltype*, tt* : tabletype*, mt* : memtype*, C : context, dt* : deftype*, rt* : reftype*, ok* : datatype*, dt_I* : deftype*, gt_I* : globaltype*, tt_I* : tabletype*, mt_I* : memtype*}: + `|-%:%`(MODULE_module(type*{type : type}, import*{import : import}, func*{func : func}, global*{global : global}, table*{table : table}, mem*{mem : mem}, elem*{elem : elem}, data*{data : data}, start?{start : start}, export*{export : export}), `%->%`_moduletype(xt_I*{xt_I : externtype}, xt_E*{xt_E : externtype})) -- Types_ok: `%|-%:%`({TYPES [], RECS [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}, type*{type : type}, dt'*{dt' : deftype}) - -- (Import_ok: `%|-%:%`({TYPES dt'*{dt' : deftype}, RECS [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}, import, ixt))*{import : import, ixt : externtype} + -- (Import_ok: `%|-%:%`({TYPES dt'*{dt' : deftype}, RECS [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}, import, xt_I))*{import : import, xt_I : externtype} -- Globals_ok: `%|-%:%`(C', global*{global : global}, gt*{gt : globaltype}) -- (Table_ok: `%|-%:%`(C', table, tt))*{table : table, tt : tabletype} -- (Mem_ok: `%|-%:%`(C', mem, mt))*{mem : mem, mt : memtype} -- (Func_ok: `%|-%:%`(C, func, dt))*{dt : deftype, func : func} -- (Elem_ok: `%|-%:%`(C, elem, rt))*{elem : elem, rt : reftype} - -- (Data_ok: `%|-%:%`(C, data, OK_datatype))^n{data : data} + -- (Data_ok: `%|-%:%`(C, data, ok))*{data : data, ok : datatype} -- (Start_ok: `%|-%:OK`(C, start))?{start : start} - -- (Export_ok: `%|-%:%`(C, export, xt))*{export : export, xt : externtype} - -- if (C = {TYPES dt'*{dt' : deftype}, RECS [], FUNCS idt*{idt : deftype} :: dt*{dt : deftype}, GLOBALS igt*{igt : globaltype} :: gt*{gt : globaltype}, TABLES itt*{itt : tabletype} :: tt*{tt : tabletype}, MEMS imt*{imt : memtype} :: mt*{mt : memtype}, ELEMS rt*{rt : reftype}, DATAS OK_datatype^n{}, LOCALS [], LABELS [], RETURN ?()}) - -- if (C' = {TYPES dt'*{dt' : deftype}, RECS [], FUNCS idt*{idt : deftype} :: dt*{dt : deftype}, GLOBALS igt*{igt : globaltype}, TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}) - -- if (idt*{idt : deftype} = $funcsxt(ixt*{ixt : externtype})) - -- if (igt*{igt : globaltype} = $globalsxt(ixt*{ixt : externtype})) - -- if (itt*{itt : tabletype} = $tablesxt(ixt*{ixt : externtype})) - -- if (imt*{imt : memtype} = $memsxt(ixt*{ixt : externtype})) + -- (Export_ok: `%|-%:%`(C, export, xt_E))*{export : export, xt_E : externtype} + -- if (C = {TYPES dt'*{dt' : deftype}, RECS [], FUNCS dt_I*{dt_I : deftype} :: dt*{dt : deftype}, GLOBALS gt_I*{gt_I : globaltype} :: gt*{gt : globaltype}, TABLES tt_I*{tt_I : tabletype} :: tt*{tt : tabletype}, MEMS mt_I*{mt_I : memtype} :: mt*{mt : memtype}, ELEMS rt*{rt : reftype}, DATAS ok*{ok : datatype}, LOCALS [], LABELS [], RETURN ?()}) + -- if (C' = {TYPES dt'*{dt' : deftype}, RECS [], FUNCS dt_I*{dt_I : deftype} :: dt*{dt : deftype}, GLOBALS gt_I*{gt_I : globaltype}, TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}) + -- if (dt_I*{dt_I : deftype} = $funcsxt(xt_I*{xt_I : externtype})) + -- if (gt_I*{gt_I : globaltype} = $globalsxt(xt_I*{xt_I : externtype})) + -- if (tt_I*{tt_I : tabletype} = $tablesxt(xt_I*{xt_I : externtype})) + -- if (mt_I*{mt_I : memtype} = $memsxt(xt_I*{xt_I : externtype})) ;; 7-runtime-typing.watsup relation Ref_ok: `%|-%:%`(store, ref, reftype) @@ -10050,35 +10056,36 @@ relation Func_ok: `%|-%:%`(context, func, deftype) ;; 6-typing.watsup relation Global_ok: `%|-%:%`(context, global, globaltype) ;; 6-typing.watsup - rule _{C : context, gt : globaltype, expr : expr, mut : mut, t : valtype}: - `%|-%:%`(C, GLOBAL_global(gt, expr), gt) + rule _{C : context, globaltype : globaltype, expr : expr, gt : globaltype, mut : mut, t : valtype}: + `%|-%:%`(C, GLOBAL_global(globaltype, expr), globaltype) -- Globaltype_ok: `%|-%:OK`(C, gt) - -- if (gt = `%%`_globaltype(mut, t)) + -- if (globaltype = `%%`_globaltype(mut, t)) -- Expr_ok_const: `%|-%:%CONST`(C, expr, t) ;; 6-typing.watsup relation Table_ok: `%|-%:%`(context, table, tabletype) ;; 6-typing.watsup - rule _{C : context, tt : tabletype, expr : expr, limits : limits, rt : reftype}: - `%|-%:%`(C, TABLE_table(tt, expr), tt) + rule _{C : context, tabletype : tabletype, expr : expr, tt : tabletype, lim : limits, rt : reftype}: + `%|-%:%`(C, TABLE_table(tabletype, expr), tabletype) -- Tabletype_ok: `%|-%:OK`(C, tt) - -- if (tt = `%%`_tabletype(limits, rt)) + -- if (tabletype = `%%`_tabletype(lim, rt)) -- Expr_ok_const: `%|-%:%CONST`(C, expr, (rt : reftype <: valtype)) ;; 6-typing.watsup relation Mem_ok: `%|-%:%`(context, mem, memtype) ;; 6-typing.watsup - rule _{C : context, mt : memtype}: - `%|-%:%`(C, MEMORY_mem(mt), mt) - -- Memtype_ok: `%|-%:OK`(C, mt) + rule _{C : context, memtype : memtype}: + `%|-%:%`(C, MEMORY_mem(memtype), memtype) + -- Memtype_ok: `%|-%:OK`(C, memtype) ;; 6-typing.watsup relation Elemmode_ok: `%|-%:%`(context, elemmode, reftype) ;; 6-typing.watsup - rule active{C : context, x : idx, expr : expr, rt : reftype, lim : limits}: + rule active{C : context, x : idx, expr : expr, rt : reftype, lim : limits, rt' : reftype}: `%|-%:%`(C, ACTIVE_elemmode(x, expr), rt) - -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - -- (Expr_ok_const: `%|-%:%CONST`(C, expr, I32_valtype))*{} + -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt')) + -- Reftype_sub: `%|-%<:%`(C, rt, rt') + -- Expr_ok_const: `%|-%:%CONST`(C, expr, I32_valtype) ;; 6-typing.watsup rule passive{C : context, rt : reftype}: @@ -10091,10 +10098,11 @@ relation Elemmode_ok: `%|-%:%`(context, elemmode, reftype) ;; 6-typing.watsup relation Elem_ok: `%|-%:%`(context, elem, reftype) ;; 6-typing.watsup - rule _{C : context, rt : reftype, expr* : expr*, elemmode : elemmode}: - `%|-%:%`(C, ELEM_elem(rt, expr*{expr : expr}, elemmode), rt) - -- (Expr_ok_const: `%|-%:%CONST`(C, expr, (rt : reftype <: valtype)))*{expr : expr} - -- Elemmode_ok: `%|-%:%`(C, elemmode, rt) + rule _{C : context, reftype : reftype, expr* : expr*, elemmode : elemmode}: + `%|-%:%`(C, ELEM_elem(reftype, expr*{expr : expr}, elemmode), reftype) + -- Reftype_ok: `%|-%:OK`(C, reftype) + -- (Expr_ok_const: `%|-%:%CONST`(C, expr, (reftype : reftype <: valtype)))*{expr : expr} + -- Elemmode_ok: `%|-%:%`(C, elemmode, reftype) ;; 6-typing.watsup relation Datamode_ok: `%|-%:OK`(context, datamode) @@ -10102,7 +10110,7 @@ relation Datamode_ok: `%|-%:OK`(context, datamode) rule active{C : context, x : idx, expr : expr, mt : memtype}: `%|-%:OK`(C, ACTIVE_datamode(x, expr)) -- if (C.MEMS_context[x!`%`_idx.0] = mt) - -- (Expr_ok_const: `%|-%:%CONST`(C, expr, I32_valtype))*{} + -- Expr_ok_const: `%|-%:%CONST`(C, expr, I32_valtype) ;; 6-typing.watsup rule passive{C : context}: @@ -10158,16 +10166,20 @@ relation Export_ok: `%|-%:%`(context, export, externtype) `%|-%:%`(C, EXPORT_export(name, externidx), xt) -- Externidx_ok: `%|-%:%`(C, externidx, xt) +;; 6-typing.watsup +syntax moduletype = + | `%->%`{externtype* : externtype*}(externtype*{externtype : externtype} : externtype*, externtype*) + ;; 6-typing.watsup rec { -;; 6-typing.watsup:1298.1-1298.100 +;; 6-typing.watsup:1302.1-1302.100 relation Globals_ok: `%|-%:%`(context, global*, globaltype*) - ;; 6-typing.watsup:1335.1-1336.17 + ;; 6-typing.watsup:1339.1-1340.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1338.1-1341.55 + ;; 6-typing.watsup:1342.1-1345.55 rule cons{C : context, global_1 : global, global : global, gt_1 : globaltype, gt* : globaltype*}: `%|-%:%`(C, [global_1] :: global*{}, [gt_1] :: gt*{gt : globaltype}) -- Global_ok: `%|-%:%`(C, global, gt_1) @@ -10177,40 +10189,40 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*) ;; 6-typing.watsup rec { -;; 6-typing.watsup:1297.1-1297.98 +;; 6-typing.watsup:1301.1-1301.98 relation Types_ok: `%|-%:%`(context, type*, deftype*) - ;; 6-typing.watsup:1327.1-1328.17 + ;; 6-typing.watsup:1331.1-1332.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1330.1-1333.50 - rule cons{C : context, type_1 : type, type* : type*, dt_1 : deftype, dt* : deftype*}: - `%|-%:%`(C, [type_1] :: type*{type : type}, dt_1*{} :: dt*{dt : deftype}) - -- Type_ok: `%|-%:%`(C, type_1, [dt_1]) - -- Types_ok: `%|-%:%`(C[TYPES_context =.. dt_1*{}], type*{type : type}, dt*{dt : deftype}) + ;; 6-typing.watsup:1334.1-1337.50 + rule cons{C : context, type_1 : type, type* : type*, dt_1* : deftype*, dt* : deftype*}: + `%|-%:%`(C, [type_1] :: type*{type : type}, dt_1*{dt_1 : deftype} :: dt*{dt : deftype}) + -- Type_ok: `%|-%:%`(C, type_1, dt_1*{dt_1 : deftype}) + -- Types_ok: `%|-%:%`(C[TYPES_context =.. dt_1*{dt_1 : deftype}], type*{type : type}, dt*{dt : deftype}) } ;; 6-typing.watsup -relation Module_ok: `|-%:OK`(module) +relation Module_ok: `|-%:%`(module, moduletype) ;; 6-typing.watsup - rule _{type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data^n : data^n, n : n, start? : start?, export* : export*, dt'* : deftype*, ixt* : externtype*, C' : context, gt* : globaltype*, tt* : tabletype*, mt* : memtype*, C : context, dt* : deftype*, rt* : reftype*, xt* : externtype*, idt* : deftype*, igt* : globaltype*, itt* : tabletype*, imt* : memtype*}: - `|-%:OK`(MODULE_module(type*{type : type}, import*{import : import}, func*{func : func}, global*{global : global}, table*{table : table}, mem*{mem : mem}, elem*{elem : elem}, data^n{data : data}, start?{start : start}, export*{export : export})) + rule _{type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data* : data*, start? : start?, export* : export*, xt_I* : externtype*, xt_E* : externtype*, dt'* : deftype*, C' : context, gt* : globaltype*, tt* : tabletype*, mt* : memtype*, C : context, dt* : deftype*, rt* : reftype*, ok* : datatype*, dt_I* : deftype*, gt_I* : globaltype*, tt_I* : tabletype*, mt_I* : memtype*}: + `|-%:%`(MODULE_module(type*{type : type}, import*{import : import}, func*{func : func}, global*{global : global}, table*{table : table}, mem*{mem : mem}, elem*{elem : elem}, data*{data : data}, start?{start : start}, export*{export : export}), `%->%`_moduletype(xt_I*{xt_I : externtype}, xt_E*{xt_E : externtype})) -- Types_ok: `%|-%:%`({TYPES [], RECS [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}, type*{type : type}, dt'*{dt' : deftype}) - -- (Import_ok: `%|-%:%`({TYPES dt'*{dt' : deftype}, RECS [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}, import, ixt))*{import : import, ixt : externtype} + -- (Import_ok: `%|-%:%`({TYPES dt'*{dt' : deftype}, RECS [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}, import, xt_I))*{import : import, xt_I : externtype} -- Globals_ok: `%|-%:%`(C', global*{global : global}, gt*{gt : globaltype}) -- (Table_ok: `%|-%:%`(C', table, tt))*{table : table, tt : tabletype} -- (Mem_ok: `%|-%:%`(C', mem, mt))*{mem : mem, mt : memtype} -- (Func_ok: `%|-%:%`(C, func, dt))*{dt : deftype, func : func} -- (Elem_ok: `%|-%:%`(C, elem, rt))*{elem : elem, rt : reftype} - -- (Data_ok: `%|-%:%`(C, data, OK_datatype))^n{data : data} + -- (Data_ok: `%|-%:%`(C, data, ok))*{data : data, ok : datatype} -- (Start_ok: `%|-%:OK`(C, start))?{start : start} - -- (Export_ok: `%|-%:%`(C, export, xt))*{export : export, xt : externtype} - -- if (C = {TYPES dt'*{dt' : deftype}, RECS [], FUNCS idt*{idt : deftype} :: dt*{dt : deftype}, GLOBALS igt*{igt : globaltype} :: gt*{gt : globaltype}, TABLES itt*{itt : tabletype} :: tt*{tt : tabletype}, MEMS imt*{imt : memtype} :: mt*{mt : memtype}, ELEMS rt*{rt : reftype}, DATAS OK_datatype^n{}, LOCALS [], LABELS [], RETURN ?()}) - -- if (C' = {TYPES dt'*{dt' : deftype}, RECS [], FUNCS idt*{idt : deftype} :: dt*{dt : deftype}, GLOBALS igt*{igt : globaltype}, TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}) - -- if (idt*{idt : deftype} = $funcsxt(ixt*{ixt : externtype})) - -- if (igt*{igt : globaltype} = $globalsxt(ixt*{ixt : externtype})) - -- if (itt*{itt : tabletype} = $tablesxt(ixt*{ixt : externtype})) - -- if (imt*{imt : memtype} = $memsxt(ixt*{ixt : externtype})) + -- (Export_ok: `%|-%:%`(C, export, xt_E))*{export : export, xt_E : externtype} + -- if (C = {TYPES dt'*{dt' : deftype}, RECS [], FUNCS dt_I*{dt_I : deftype} :: dt*{dt : deftype}, GLOBALS gt_I*{gt_I : globaltype} :: gt*{gt : globaltype}, TABLES tt_I*{tt_I : tabletype} :: tt*{tt : tabletype}, MEMS mt_I*{mt_I : memtype} :: mt*{mt : memtype}, ELEMS rt*{rt : reftype}, DATAS ok*{ok : datatype}, LOCALS [], LABELS [], RETURN ?()}) + -- if (C' = {TYPES dt'*{dt' : deftype}, RECS [], FUNCS dt_I*{dt_I : deftype} :: dt*{dt : deftype}, GLOBALS gt_I*{gt_I : globaltype}, TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}) + -- if (dt_I*{dt_I : deftype} = $funcsxt(xt_I*{xt_I : externtype})) + -- if (gt_I*{gt_I : globaltype} = $globalsxt(xt_I*{xt_I : externtype})) + -- if (tt_I*{tt_I : tabletype} = $tablesxt(xt_I*{xt_I : externtype})) + -- if (mt_I*{mt_I : memtype} = $memsxt(xt_I*{xt_I : externtype})) ;; 7-runtime-typing.watsup relation Ref_ok: `%|-%:%`(store, ref, reftype) @@ -15841,35 +15853,36 @@ relation Func_ok: `%|-%:%`(context, func, deftype) ;; 6-typing.watsup relation Global_ok: `%|-%:%`(context, global, globaltype) ;; 6-typing.watsup - rule _{C : context, gt : globaltype, expr : expr, mut : mut, t : valtype}: - `%|-%:%`(C, GLOBAL_global(gt, expr), gt) + rule _{C : context, globaltype : globaltype, expr : expr, gt : globaltype, mut : mut, t : valtype}: + `%|-%:%`(C, GLOBAL_global(globaltype, expr), globaltype) -- Globaltype_ok: `%|-%:OK`(C, gt) - -- if (gt = `%%`_globaltype(mut, t)) + -- if (globaltype = `%%`_globaltype(mut, t)) -- Expr_ok_const: `%|-%:%CONST`(C, expr, t) ;; 6-typing.watsup relation Table_ok: `%|-%:%`(context, table, tabletype) ;; 6-typing.watsup - rule _{C : context, tt : tabletype, expr : expr, limits : limits, rt : reftype}: - `%|-%:%`(C, TABLE_table(tt, expr), tt) + rule _{C : context, tabletype : tabletype, expr : expr, tt : tabletype, lim : limits, rt : reftype}: + `%|-%:%`(C, TABLE_table(tabletype, expr), tabletype) -- Tabletype_ok: `%|-%:OK`(C, tt) - -- if (tt = `%%`_tabletype(limits, rt)) + -- if (tabletype = `%%`_tabletype(lim, rt)) -- Expr_ok_const: `%|-%:%CONST`(C, expr, (rt : reftype <: valtype)) ;; 6-typing.watsup relation Mem_ok: `%|-%:%`(context, mem, memtype) ;; 6-typing.watsup - rule _{C : context, mt : memtype}: - `%|-%:%`(C, MEMORY_mem(mt), mt) - -- Memtype_ok: `%|-%:OK`(C, mt) + rule _{C : context, memtype : memtype}: + `%|-%:%`(C, MEMORY_mem(memtype), memtype) + -- Memtype_ok: `%|-%:OK`(C, memtype) ;; 6-typing.watsup relation Elemmode_ok: `%|-%:%`(context, elemmode, reftype) ;; 6-typing.watsup - rule active{C : context, x : idx, expr : expr, rt : reftype, lim : limits}: + rule active{C : context, x : idx, expr : expr, rt : reftype, lim : limits, rt' : reftype}: `%|-%:%`(C, ACTIVE_elemmode(x, expr), rt) - -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - -- (Expr_ok_const: `%|-%:%CONST`(C, expr, I32_valtype))*{} + -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt')) + -- Reftype_sub: `%|-%<:%`(C, rt, rt') + -- Expr_ok_const: `%|-%:%CONST`(C, expr, I32_valtype) ;; 6-typing.watsup rule passive{C : context, rt : reftype}: @@ -15882,10 +15895,11 @@ relation Elemmode_ok: `%|-%:%`(context, elemmode, reftype) ;; 6-typing.watsup relation Elem_ok: `%|-%:%`(context, elem, reftype) ;; 6-typing.watsup - rule _{C : context, rt : reftype, expr* : expr*, elemmode : elemmode}: - `%|-%:%`(C, ELEM_elem(rt, expr*{expr : expr}, elemmode), rt) - -- (Expr_ok_const: `%|-%:%CONST`(C, expr, (rt : reftype <: valtype)))*{expr : expr} - -- Elemmode_ok: `%|-%:%`(C, elemmode, rt) + rule _{C : context, reftype : reftype, expr* : expr*, elemmode : elemmode}: + `%|-%:%`(C, ELEM_elem(reftype, expr*{expr : expr}, elemmode), reftype) + -- Reftype_ok: `%|-%:OK`(C, reftype) + -- (Expr_ok_const: `%|-%:%CONST`(C, expr, (reftype : reftype <: valtype)))*{expr : expr} + -- Elemmode_ok: `%|-%:%`(C, elemmode, reftype) ;; 6-typing.watsup relation Datamode_ok: `%|-%:OK`(context, datamode) @@ -15893,7 +15907,7 @@ relation Datamode_ok: `%|-%:OK`(context, datamode) rule active{C : context, x : idx, expr : expr, mt : memtype}: `%|-%:OK`(C, ACTIVE_datamode(x, expr)) -- if (C.MEMS_context[x!`%`_idx.0] = mt) - -- (Expr_ok_const: `%|-%:%CONST`(C, expr, I32_valtype))*{} + -- Expr_ok_const: `%|-%:%CONST`(C, expr, I32_valtype) ;; 6-typing.watsup rule passive{C : context}: @@ -15949,16 +15963,20 @@ relation Export_ok: `%|-%:%`(context, export, externtype) `%|-%:%`(C, EXPORT_export(name, externidx), xt) -- Externidx_ok: `%|-%:%`(C, externidx, xt) +;; 6-typing.watsup +syntax moduletype = + | `%->%`{externtype* : externtype*}(externtype*{externtype : externtype} : externtype*, externtype*) + ;; 6-typing.watsup rec { -;; 6-typing.watsup:1298.1-1298.100 +;; 6-typing.watsup:1302.1-1302.100 relation Globals_ok: `%|-%:%`(context, global*, globaltype*) - ;; 6-typing.watsup:1335.1-1336.17 + ;; 6-typing.watsup:1339.1-1340.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1338.1-1341.55 + ;; 6-typing.watsup:1342.1-1345.55 rule cons{C : context, global_1 : global, global : global, gt_1 : globaltype, gt* : globaltype*}: `%|-%:%`(C, [global_1] :: global*{}, [gt_1] :: gt*{gt : globaltype}) -- Global_ok: `%|-%:%`(C, global, gt_1) @@ -15968,40 +15986,40 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*) ;; 6-typing.watsup rec { -;; 6-typing.watsup:1297.1-1297.98 +;; 6-typing.watsup:1301.1-1301.98 relation Types_ok: `%|-%:%`(context, type*, deftype*) - ;; 6-typing.watsup:1327.1-1328.17 + ;; 6-typing.watsup:1331.1-1332.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1330.1-1333.50 - rule cons{C : context, type_1 : type, type* : type*, dt_1 : deftype, dt* : deftype*}: - `%|-%:%`(C, [type_1] :: type*{type : type}, dt_1*{} :: dt*{dt : deftype}) - -- Type_ok: `%|-%:%`(C, type_1, [dt_1]) - -- Types_ok: `%|-%:%`(C[TYPES_context =.. dt_1*{}], type*{type : type}, dt*{dt : deftype}) + ;; 6-typing.watsup:1334.1-1337.50 + rule cons{C : context, type_1 : type, type* : type*, dt_1* : deftype*, dt* : deftype*}: + `%|-%:%`(C, [type_1] :: type*{type : type}, dt_1*{dt_1 : deftype} :: dt*{dt : deftype}) + -- Type_ok: `%|-%:%`(C, type_1, dt_1*{dt_1 : deftype}) + -- Types_ok: `%|-%:%`(C[TYPES_context =.. dt_1*{dt_1 : deftype}], type*{type : type}, dt*{dt : deftype}) } ;; 6-typing.watsup -relation Module_ok: `|-%:OK`(module) +relation Module_ok: `|-%:%`(module, moduletype) ;; 6-typing.watsup - rule _{type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data^n : data^n, n : n, start? : start?, export* : export*, dt'* : deftype*, ixt* : externtype*, C' : context, gt* : globaltype*, tt* : tabletype*, mt* : memtype*, C : context, dt* : deftype*, rt* : reftype*, xt* : externtype*, idt* : deftype*, igt* : globaltype*, itt* : tabletype*, imt* : memtype*}: - `|-%:OK`(MODULE_module(type*{type : type}, import*{import : import}, func*{func : func}, global*{global : global}, table*{table : table}, mem*{mem : mem}, elem*{elem : elem}, data^n{data : data}, start?{start : start}, export*{export : export})) + rule _{type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data* : data*, start? : start?, export* : export*, xt_I* : externtype*, xt_E* : externtype*, dt'* : deftype*, C' : context, gt* : globaltype*, tt* : tabletype*, mt* : memtype*, C : context, dt* : deftype*, rt* : reftype*, ok* : datatype*, dt_I* : deftype*, gt_I* : globaltype*, tt_I* : tabletype*, mt_I* : memtype*}: + `|-%:%`(MODULE_module(type*{type : type}, import*{import : import}, func*{func : func}, global*{global : global}, table*{table : table}, mem*{mem : mem}, elem*{elem : elem}, data*{data : data}, start?{start : start}, export*{export : export}), `%->%`_moduletype(xt_I*{xt_I : externtype}, xt_E*{xt_E : externtype})) -- Types_ok: `%|-%:%`({TYPES [], RECS [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}, type*{type : type}, dt'*{dt' : deftype}) - -- (Import_ok: `%|-%:%`({TYPES dt'*{dt' : deftype}, RECS [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}, import, ixt))*{import : import, ixt : externtype} + -- (Import_ok: `%|-%:%`({TYPES dt'*{dt' : deftype}, RECS [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}, import, xt_I))*{import : import, xt_I : externtype} -- Globals_ok: `%|-%:%`(C', global*{global : global}, gt*{gt : globaltype}) -- (Table_ok: `%|-%:%`(C', table, tt))*{table : table, tt : tabletype} -- (Mem_ok: `%|-%:%`(C', mem, mt))*{mem : mem, mt : memtype} -- (Func_ok: `%|-%:%`(C, func, dt))*{dt : deftype, func : func} -- (Elem_ok: `%|-%:%`(C, elem, rt))*{elem : elem, rt : reftype} - -- (Data_ok: `%|-%:%`(C, data, OK_datatype))^n{data : data} + -- (Data_ok: `%|-%:%`(C, data, ok))*{data : data, ok : datatype} -- (Start_ok: `%|-%:OK`(C, start))?{start : start} - -- (Export_ok: `%|-%:%`(C, export, xt))*{export : export, xt : externtype} - -- if (C = {TYPES dt'*{dt' : deftype}, RECS [], FUNCS idt*{idt : deftype} :: dt*{dt : deftype}, GLOBALS igt*{igt : globaltype} :: gt*{gt : globaltype}, TABLES itt*{itt : tabletype} :: tt*{tt : tabletype}, MEMS imt*{imt : memtype} :: mt*{mt : memtype}, ELEMS rt*{rt : reftype}, DATAS OK_datatype^n{}, LOCALS [], LABELS [], RETURN ?()}) - -- if (C' = {TYPES dt'*{dt' : deftype}, RECS [], FUNCS idt*{idt : deftype} :: dt*{dt : deftype}, GLOBALS igt*{igt : globaltype}, TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}) - -- if (idt*{idt : deftype} = $funcsxt(ixt*{ixt : externtype})) - -- if (igt*{igt : globaltype} = $globalsxt(ixt*{ixt : externtype})) - -- if (itt*{itt : tabletype} = $tablesxt(ixt*{ixt : externtype})) - -- if (imt*{imt : memtype} = $memsxt(ixt*{ixt : externtype})) + -- (Export_ok: `%|-%:%`(C, export, xt_E))*{export : export, xt_E : externtype} + -- if (C = {TYPES dt'*{dt' : deftype}, RECS [], FUNCS dt_I*{dt_I : deftype} :: dt*{dt : deftype}, GLOBALS gt_I*{gt_I : globaltype} :: gt*{gt : globaltype}, TABLES tt_I*{tt_I : tabletype} :: tt*{tt : tabletype}, MEMS mt_I*{mt_I : memtype} :: mt*{mt : memtype}, ELEMS rt*{rt : reftype}, DATAS ok*{ok : datatype}, LOCALS [], LABELS [], RETURN ?()}) + -- if (C' = {TYPES dt'*{dt' : deftype}, RECS [], FUNCS dt_I*{dt_I : deftype} :: dt*{dt : deftype}, GLOBALS gt_I*{gt_I : globaltype}, TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}) + -- if (dt_I*{dt_I : deftype} = $funcsxt(xt_I*{xt_I : externtype})) + -- if (gt_I*{gt_I : globaltype} = $globalsxt(xt_I*{xt_I : externtype})) + -- if (tt_I*{tt_I : tabletype} = $tablesxt(xt_I*{xt_I : externtype})) + -- if (mt_I*{mt_I : memtype} = $memsxt(xt_I*{xt_I : externtype})) ;; 7-runtime-typing.watsup relation Ref_ok: `%|-%:%`(store, ref, reftype) @@ -21732,36 +21750,37 @@ relation Func_ok: `%|-%:%`(context, func, deftype) ;; 6-typing.watsup relation Global_ok: `%|-%:%`(context, global, globaltype) ;; 6-typing.watsup - rule _{C : context, gt : globaltype, expr : expr, mut : mut, t : valtype}: - `%|-%:%`(C, GLOBAL_global(gt, expr), gt) + rule _{C : context, globaltype : globaltype, expr : expr, gt : globaltype, mut : mut, t : valtype}: + `%|-%:%`(C, GLOBAL_global(globaltype, expr), globaltype) -- Globaltype_ok: `%|-%:OK`(C, gt) - -- if (gt = `%%`_globaltype(mut, t)) + -- if (globaltype = `%%`_globaltype(mut, t)) -- Expr_ok_const: `%|-%:%CONST`(C, expr, t) ;; 6-typing.watsup relation Table_ok: `%|-%:%`(context, table, tabletype) ;; 6-typing.watsup - rule _{C : context, tt : tabletype, expr : expr, limits : limits, rt : reftype}: - `%|-%:%`(C, TABLE_table(tt, expr), tt) + rule _{C : context, tabletype : tabletype, expr : expr, tt : tabletype, lim : limits, rt : reftype}: + `%|-%:%`(C, TABLE_table(tabletype, expr), tabletype) -- Tabletype_ok: `%|-%:OK`(C, tt) - -- if (tt = `%%`_tabletype(limits, rt)) + -- if (tabletype = `%%`_tabletype(lim, rt)) -- Expr_ok_const: `%|-%:%CONST`(C, expr, (rt : reftype <: valtype)) ;; 6-typing.watsup relation Mem_ok: `%|-%:%`(context, mem, memtype) ;; 6-typing.watsup - rule _{C : context, mt : memtype}: - `%|-%:%`(C, MEMORY_mem(mt), mt) - -- Memtype_ok: `%|-%:OK`(C, mt) + rule _{C : context, memtype : memtype}: + `%|-%:%`(C, MEMORY_mem(memtype), memtype) + -- Memtype_ok: `%|-%:OK`(C, memtype) ;; 6-typing.watsup relation Elemmode_ok: `%|-%:%`(context, elemmode, reftype) ;; 6-typing.watsup - rule active{C : context, x : idx, expr : expr, rt : reftype, lim : limits}: + rule active{C : context, x : idx, expr : expr, rt : reftype, lim : limits, rt' : reftype}: `%|-%:%`(C, ACTIVE_elemmode(x, expr), rt) -- if (x!`%`_idx.0 < |C.TABLES_context|) - -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - -- (Expr_ok_const: `%|-%:%CONST`(C, expr, I32_valtype))*{} + -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt')) + -- Reftype_sub: `%|-%<:%`(C, rt, rt') + -- Expr_ok_const: `%|-%:%CONST`(C, expr, I32_valtype) ;; 6-typing.watsup rule passive{C : context, rt : reftype}: @@ -21774,10 +21793,11 @@ relation Elemmode_ok: `%|-%:%`(context, elemmode, reftype) ;; 6-typing.watsup relation Elem_ok: `%|-%:%`(context, elem, reftype) ;; 6-typing.watsup - rule _{C : context, rt : reftype, expr* : expr*, elemmode : elemmode}: - `%|-%:%`(C, ELEM_elem(rt, expr*{expr : expr}, elemmode), rt) - -- (Expr_ok_const: `%|-%:%CONST`(C, expr, (rt : reftype <: valtype)))*{expr : expr} - -- Elemmode_ok: `%|-%:%`(C, elemmode, rt) + rule _{C : context, reftype : reftype, expr* : expr*, elemmode : elemmode}: + `%|-%:%`(C, ELEM_elem(reftype, expr*{expr : expr}, elemmode), reftype) + -- Reftype_ok: `%|-%:OK`(C, reftype) + -- (Expr_ok_const: `%|-%:%CONST`(C, expr, (reftype : reftype <: valtype)))*{expr : expr} + -- Elemmode_ok: `%|-%:%`(C, elemmode, reftype) ;; 6-typing.watsup relation Datamode_ok: `%|-%:OK`(context, datamode) @@ -21786,7 +21806,7 @@ relation Datamode_ok: `%|-%:OK`(context, datamode) `%|-%:OK`(C, ACTIVE_datamode(x, expr)) -- if (x!`%`_idx.0 < |C.MEMS_context|) -- if (C.MEMS_context[x!`%`_idx.0] = mt) - -- (Expr_ok_const: `%|-%:%CONST`(C, expr, I32_valtype))*{} + -- Expr_ok_const: `%|-%:%CONST`(C, expr, I32_valtype) ;; 6-typing.watsup rule passive{C : context}: @@ -21847,16 +21867,20 @@ relation Export_ok: `%|-%:%`(context, export, externtype) `%|-%:%`(C, EXPORT_export(name, externidx), xt) -- Externidx_ok: `%|-%:%`(C, externidx, xt) +;; 6-typing.watsup +syntax moduletype = + | `%->%`{externtype* : externtype*}(externtype*{externtype : externtype} : externtype*, externtype*) + ;; 6-typing.watsup rec { -;; 6-typing.watsup:1298.1-1298.100 +;; 6-typing.watsup:1302.1-1302.100 relation Globals_ok: `%|-%:%`(context, global*, globaltype*) - ;; 6-typing.watsup:1335.1-1336.17 + ;; 6-typing.watsup:1339.1-1340.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1338.1-1341.55 + ;; 6-typing.watsup:1342.1-1345.55 rule cons{C : context, global_1 : global, global : global, gt_1 : globaltype, gt* : globaltype*}: `%|-%:%`(C, [global_1] :: global*{}, [gt_1] :: gt*{gt : globaltype}) -- Global_ok: `%|-%:%`(C, global, gt_1) @@ -21866,46 +21890,47 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*) ;; 6-typing.watsup rec { -;; 6-typing.watsup:1297.1-1297.98 +;; 6-typing.watsup:1301.1-1301.98 relation Types_ok: `%|-%:%`(context, type*, deftype*) - ;; 6-typing.watsup:1327.1-1328.17 + ;; 6-typing.watsup:1331.1-1332.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1330.1-1333.50 - rule cons{C : context, type_1 : type, type* : type*, dt_1 : deftype, dt* : deftype*}: - `%|-%:%`(C, [type_1] :: type*{type : type}, dt_1*{} :: dt*{dt : deftype}) - -- Type_ok: `%|-%:%`(C, type_1, [dt_1]) - -- Types_ok: `%|-%:%`(C[TYPES_context =.. dt_1*{}], type*{type : type}, dt*{dt : deftype}) + ;; 6-typing.watsup:1334.1-1337.50 + rule cons{C : context, type_1 : type, type* : type*, dt_1* : deftype*, dt* : deftype*}: + `%|-%:%`(C, [type_1] :: type*{type : type}, dt_1*{dt_1 : deftype} :: dt*{dt : deftype}) + -- Type_ok: `%|-%:%`(C, type_1, dt_1*{dt_1 : deftype}) + -- Types_ok: `%|-%:%`(C[TYPES_context =.. dt_1*{dt_1 : deftype}], type*{type : type}, dt*{dt : deftype}) } ;; 6-typing.watsup -relation Module_ok: `|-%:OK`(module) +relation Module_ok: `|-%:%`(module, moduletype) ;; 6-typing.watsup - rule _{type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data^n : data^n, n : n, start? : start?, export* : export*, dt'* : deftype*, ixt* : externtype*, C' : context, gt* : globaltype*, tt* : tabletype*, mt* : memtype*, C : context, dt* : deftype*, rt* : reftype*, xt* : externtype*, idt* : deftype*, igt* : globaltype*, itt* : tabletype*, imt* : memtype*}: - `|-%:OK`(MODULE_module(type*{type : type}, import*{import : import}, func*{func : func}, global*{global : global}, table*{table : table}, mem*{mem : mem}, elem*{elem : elem}, data^n{data : data}, start?{start : start}, export*{export : export})) - -- if (|import*{import : import}| = |ixt*{ixt : externtype}|) + rule _{type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data* : data*, start? : start?, export* : export*, xt_I* : externtype*, xt_E* : externtype*, dt'* : deftype*, C' : context, gt* : globaltype*, tt* : tabletype*, mt* : memtype*, C : context, dt* : deftype*, rt* : reftype*, ok* : datatype*, dt_I* : deftype*, gt_I* : globaltype*, tt_I* : tabletype*, mt_I* : memtype*}: + `|-%:%`(MODULE_module(type*{type : type}, import*{import : import}, func*{func : func}, global*{global : global}, table*{table : table}, mem*{mem : mem}, elem*{elem : elem}, data*{data : data}, start?{start : start}, export*{export : export}), `%->%`_moduletype(xt_I*{xt_I : externtype}, xt_E*{xt_E : externtype})) + -- if (|import*{import : import}| = |xt_I*{xt_I : externtype}|) -- if (|table*{table : table}| = |tt*{tt : tabletype}|) -- if (|mem*{mem : mem}| = |mt*{mt : memtype}|) -- if (|dt*{dt : deftype}| = |func*{func : func}|) -- if (|elem*{elem : elem}| = |rt*{rt : reftype}|) - -- if (|export*{export : export}| = |xt*{xt : externtype}|) + -- if (|data*{data : data}| = |ok*{ok : datatype}|) + -- if (|export*{export : export}| = |xt_E*{xt_E : externtype}|) -- Types_ok: `%|-%:%`({TYPES [], RECS [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}, type*{type : type}, dt'*{dt' : deftype}) - -- (Import_ok: `%|-%:%`({TYPES dt'*{dt' : deftype}, RECS [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}, import, ixt))*{import : import, ixt : externtype} + -- (Import_ok: `%|-%:%`({TYPES dt'*{dt' : deftype}, RECS [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}, import, xt_I))*{import : import, xt_I : externtype} -- Globals_ok: `%|-%:%`(C', global*{global : global}, gt*{gt : globaltype}) -- (Table_ok: `%|-%:%`(C', table, tt))*{table : table, tt : tabletype} -- (Mem_ok: `%|-%:%`(C', mem, mt))*{mem : mem, mt : memtype} -- (Func_ok: `%|-%:%`(C, func, dt))*{dt : deftype, func : func} -- (Elem_ok: `%|-%:%`(C, elem, rt))*{elem : elem, rt : reftype} - -- (Data_ok: `%|-%:%`(C, data, OK_datatype))^n{data : data} + -- (Data_ok: `%|-%:%`(C, data, ok))*{data : data, ok : datatype} -- (Start_ok: `%|-%:OK`(C, start))?{start : start} - -- (Export_ok: `%|-%:%`(C, export, xt))*{export : export, xt : externtype} - -- if (C = {TYPES dt'*{dt' : deftype}, RECS [], FUNCS idt*{idt : deftype} :: dt*{dt : deftype}, GLOBALS igt*{igt : globaltype} :: gt*{gt : globaltype}, TABLES itt*{itt : tabletype} :: tt*{tt : tabletype}, MEMS imt*{imt : memtype} :: mt*{mt : memtype}, ELEMS rt*{rt : reftype}, DATAS OK_datatype^n{}, LOCALS [], LABELS [], RETURN ?()}) - -- if (C' = {TYPES dt'*{dt' : deftype}, RECS [], FUNCS idt*{idt : deftype} :: dt*{dt : deftype}, GLOBALS igt*{igt : globaltype}, TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}) - -- if (idt*{idt : deftype} = $funcsxt(ixt*{ixt : externtype})) - -- if (igt*{igt : globaltype} = $globalsxt(ixt*{ixt : externtype})) - -- if (itt*{itt : tabletype} = $tablesxt(ixt*{ixt : externtype})) - -- if (imt*{imt : memtype} = $memsxt(ixt*{ixt : externtype})) + -- (Export_ok: `%|-%:%`(C, export, xt_E))*{export : export, xt_E : externtype} + -- if (C = {TYPES dt'*{dt' : deftype}, RECS [], FUNCS dt_I*{dt_I : deftype} :: dt*{dt : deftype}, GLOBALS gt_I*{gt_I : globaltype} :: gt*{gt : globaltype}, TABLES tt_I*{tt_I : tabletype} :: tt*{tt : tabletype}, MEMS mt_I*{mt_I : memtype} :: mt*{mt : memtype}, ELEMS rt*{rt : reftype}, DATAS ok*{ok : datatype}, LOCALS [], LABELS [], RETURN ?()}) + -- if (C' = {TYPES dt'*{dt' : deftype}, RECS [], FUNCS dt_I*{dt_I : deftype} :: dt*{dt : deftype}, GLOBALS gt_I*{gt_I : globaltype}, TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}) + -- if (dt_I*{dt_I : deftype} = $funcsxt(xt_I*{xt_I : externtype})) + -- if (gt_I*{gt_I : globaltype} = $globalsxt(xt_I*{xt_I : externtype})) + -- if (tt_I*{tt_I : tabletype} = $tablesxt(xt_I*{xt_I : externtype})) + -- if (mt_I*{mt_I : memtype} = $memsxt(xt_I*{xt_I : externtype})) ;; 7-runtime-typing.watsup relation Ref_ok: `%|-%:%`(store, ref, reftype) @@ -27712,36 +27737,37 @@ relation Func_ok: `%|-%:%`(context, func, deftype) ;; 6-typing.watsup relation Global_ok: `%|-%:%`(context, global, globaltype) ;; 6-typing.watsup - rule _{C : context, gt : globaltype, expr : expr, mut : mut, t : valtype}: - `%|-%:%`(C, GLOBAL_global(gt, expr), gt) + rule _{C : context, globaltype : globaltype, expr : expr, gt : globaltype, mut : mut, t : valtype}: + `%|-%:%`(C, GLOBAL_global(globaltype, expr), globaltype) -- Globaltype_ok: `%|-%:OK`(C, gt) - -- where `%%`_globaltype(mut, t) = gt + -- where `%%`_globaltype(mut, t) = globaltype -- Expr_ok_const: `%|-%:%CONST`(C, expr, t) ;; 6-typing.watsup relation Table_ok: `%|-%:%`(context, table, tabletype) ;; 6-typing.watsup - rule _{C : context, tt : tabletype, expr : expr, limits : limits, rt : reftype}: - `%|-%:%`(C, TABLE_table(tt, expr), tt) + rule _{C : context, tabletype : tabletype, expr : expr, tt : tabletype, lim : limits, rt : reftype}: + `%|-%:%`(C, TABLE_table(tabletype, expr), tabletype) -- Tabletype_ok: `%|-%:OK`(C, tt) - -- where `%%`_tabletype(limits, rt) = tt + -- where `%%`_tabletype(lim, rt) = tabletype -- Expr_ok_const: `%|-%:%CONST`(C, expr, (rt : reftype <: valtype)) ;; 6-typing.watsup relation Mem_ok: `%|-%:%`(context, mem, memtype) ;; 6-typing.watsup - rule _{C : context, mt : memtype}: - `%|-%:%`(C, MEMORY_mem(mt), mt) - -- Memtype_ok: `%|-%:OK`(C, mt) + rule _{C : context, memtype : memtype}: + `%|-%:%`(C, MEMORY_mem(memtype), memtype) + -- Memtype_ok: `%|-%:OK`(C, memtype) ;; 6-typing.watsup relation Elemmode_ok: `%|-%:%`(context, elemmode, reftype) ;; 6-typing.watsup - rule active{C : context, x : idx, expr : expr, rt : reftype, lim : limits}: + rule active{C : context, x : idx, expr : expr, rt : reftype, lim : limits, rt' : reftype}: `%|-%:%`(C, ACTIVE_elemmode(x, expr), rt) -- if (x!`%`_idx.0 < |C.TABLES_context|) - -- (Expr_ok_const: `%|-%:%CONST`(C, expr, I32_valtype))*{} - -- where `%%`_tabletype(lim, rt) = C.TABLES_context[x!`%`_idx.0] + -- Expr_ok_const: `%|-%:%CONST`(C, expr, I32_valtype) + -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt')) + -- Reftype_sub: `%|-%<:%`(C, rt, rt') ;; 6-typing.watsup rule passive{C : context, rt : reftype}: @@ -27754,10 +27780,11 @@ relation Elemmode_ok: `%|-%:%`(context, elemmode, reftype) ;; 6-typing.watsup relation Elem_ok: `%|-%:%`(context, elem, reftype) ;; 6-typing.watsup - rule _{C : context, rt : reftype, expr* : expr*, elemmode : elemmode}: - `%|-%:%`(C, ELEM_elem(rt, expr*{expr : expr}, elemmode), rt) - -- (Expr_ok_const: `%|-%:%CONST`(C, expr, (rt : reftype <: valtype)))*{expr : expr} - -- Elemmode_ok: `%|-%:%`(C, elemmode, rt) + rule _{C : context, reftype : reftype, expr* : expr*, elemmode : elemmode}: + `%|-%:%`(C, ELEM_elem(reftype, expr*{expr : expr}, elemmode), reftype) + -- Reftype_ok: `%|-%:OK`(C, reftype) + -- (Expr_ok_const: `%|-%:%CONST`(C, expr, (reftype : reftype <: valtype)))*{expr : expr} + -- Elemmode_ok: `%|-%:%`(C, elemmode, reftype) ;; 6-typing.watsup relation Datamode_ok: `%|-%:OK`(context, datamode) @@ -27766,7 +27793,7 @@ relation Datamode_ok: `%|-%:OK`(context, datamode) `%|-%:OK`(C, ACTIVE_datamode(x, expr)) -- if (x!`%`_idx.0 < |C.MEMS_context|) -- if (C.MEMS_context[x!`%`_idx.0] = mt) - -- (Expr_ok_const: `%|-%:%CONST`(C, expr, I32_valtype))*{} + -- Expr_ok_const: `%|-%:%CONST`(C, expr, I32_valtype) ;; 6-typing.watsup rule passive{C : context}: @@ -27827,16 +27854,20 @@ relation Export_ok: `%|-%:%`(context, export, externtype) `%|-%:%`(C, EXPORT_export(name, externidx), xt) -- Externidx_ok: `%|-%:%`(C, externidx, xt) +;; 6-typing.watsup +syntax moduletype = + | `%->%`{externtype* : externtype*}(externtype*{externtype : externtype} : externtype*, externtype*) + ;; 6-typing.watsup rec { -;; 6-typing.watsup:1298.1-1298.100 +;; 6-typing.watsup:1302.1-1302.100 relation Globals_ok: `%|-%:%`(context, global*, globaltype*) - ;; 6-typing.watsup:1335.1-1336.17 + ;; 6-typing.watsup:1339.1-1340.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1338.1-1341.55 + ;; 6-typing.watsup:1342.1-1345.55 rule cons{C : context, global_1 : global, global : global, gt_1 : globaltype, gt* : globaltype*}: `%|-%:%`(C, [global_1] :: global*{}, [gt_1] :: gt*{gt : globaltype}) -- Global_ok: `%|-%:%`(C, global, gt_1) @@ -27846,46 +27877,47 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*) ;; 6-typing.watsup rec { -;; 6-typing.watsup:1297.1-1297.98 +;; 6-typing.watsup:1301.1-1301.98 relation Types_ok: `%|-%:%`(context, type*, deftype*) - ;; 6-typing.watsup:1327.1-1328.17 + ;; 6-typing.watsup:1331.1-1332.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1330.1-1333.50 - rule cons{C : context, type_1 : type, type* : type*, dt_1 : deftype, dt* : deftype*}: - `%|-%:%`(C, [type_1] :: type*{type : type}, dt_1*{} :: dt*{dt : deftype}) - -- Type_ok: `%|-%:%`(C, type_1, [dt_1]) - -- Types_ok: `%|-%:%`(C[TYPES_context =.. dt_1*{}], type*{type : type}, dt*{dt : deftype}) + ;; 6-typing.watsup:1334.1-1337.50 + rule cons{C : context, type_1 : type, type* : type*, dt_1* : deftype*, dt* : deftype*}: + `%|-%:%`(C, [type_1] :: type*{type : type}, dt_1*{dt_1 : deftype} :: dt*{dt : deftype}) + -- Type_ok: `%|-%:%`(C, type_1, dt_1*{dt_1 : deftype}) + -- Types_ok: `%|-%:%`(C[TYPES_context =.. dt_1*{dt_1 : deftype}], type*{type : type}, dt*{dt : deftype}) } ;; 6-typing.watsup -relation Module_ok: `|-%:OK`(module) +relation Module_ok: `|-%:%`(module, moduletype) ;; 6-typing.watsup - rule _{type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data^n : data^n, n : n, start? : start?, export* : export*, dt'* : deftype*, ixt* : externtype*, C' : context, gt* : globaltype*, tt* : tabletype*, mt* : memtype*, C : context, dt* : deftype*, rt* : reftype*, xt* : externtype*, idt* : deftype*, igt* : globaltype*, itt* : tabletype*, imt* : memtype*}: - `|-%:OK`(MODULE_module(type*{type : type}, import*{import : import}, func*{func : func}, global*{global : global}, table*{table : table}, mem*{mem : mem}, elem*{elem : elem}, data^n{data : data}, start?{start : start}, export*{export : export})) - -- if (|import*{import : import}| = |ixt*{ixt : externtype}|) + rule _{type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data* : data*, start? : start?, export* : export*, xt_I* : externtype*, xt_E* : externtype*, dt'* : deftype*, C' : context, gt* : globaltype*, tt* : tabletype*, mt* : memtype*, C : context, dt* : deftype*, rt* : reftype*, ok* : datatype*, dt_I* : deftype*, gt_I* : globaltype*, tt_I* : tabletype*, mt_I* : memtype*}: + `|-%:%`(MODULE_module(type*{type : type}, import*{import : import}, func*{func : func}, global*{global : global}, table*{table : table}, mem*{mem : mem}, elem*{elem : elem}, data*{data : data}, start?{start : start}, export*{export : export}), `%->%`_moduletype(xt_I*{xt_I : externtype}, xt_E*{xt_E : externtype})) + -- if (|import*{import : import}| = |xt_I*{xt_I : externtype}|) -- if (|table*{table : table}| = |tt*{tt : tabletype}|) -- if (|mem*{mem : mem}| = |mt*{mt : memtype}|) -- if (|dt*{dt : deftype}| = |func*{func : func}|) -- if (|elem*{elem : elem}| = |rt*{rt : reftype}|) - -- if (|export*{export : export}| = |xt*{xt : externtype}|) + -- if (|data*{data : data}| = |ok*{ok : datatype}|) + -- if (|export*{export : export}| = |xt_E*{xt_E : externtype}|) -- Types_ok: `%|-%:%`({TYPES [], RECS [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}, type*{type : type}, dt'*{dt' : deftype}) - -- (Import_ok: `%|-%:%`({TYPES dt'*{dt' : deftype}, RECS [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}, import, ixt))*{import : import, ixt : externtype} + -- (Import_ok: `%|-%:%`({TYPES dt'*{dt' : deftype}, RECS [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}, import, xt_I))*{import : import, xt_I : externtype} -- Globals_ok: `%|-%:%`(C', global*{global : global}, gt*{gt : globaltype}) -- (Table_ok: `%|-%:%`(C', table, tt))*{table : table, tt : tabletype} -- (Mem_ok: `%|-%:%`(C', mem, mt))*{mem : mem, mt : memtype} -- (Func_ok: `%|-%:%`(C, func, dt))*{dt : deftype, func : func} -- (Elem_ok: `%|-%:%`(C, elem, rt))*{elem : elem, rt : reftype} - -- (Data_ok: `%|-%:%`(C, data, OK_datatype))^n{data : data} + -- (Data_ok: `%|-%:%`(C, data, ok))*{data : data, ok : datatype} -- (Start_ok: `%|-%:OK`(C, start))?{start : start} - -- (Export_ok: `%|-%:%`(C, export, xt))*{export : export, xt : externtype} - -- if (C = {TYPES dt'*{dt' : deftype}, RECS [], FUNCS idt*{idt : deftype} :: dt*{dt : deftype}, GLOBALS igt*{igt : globaltype} :: gt*{gt : globaltype}, TABLES itt*{itt : tabletype} :: tt*{tt : tabletype}, MEMS imt*{imt : memtype} :: mt*{mt : memtype}, ELEMS rt*{rt : reftype}, DATAS OK_datatype^n{}, LOCALS [], LABELS [], RETURN ?()}) - -- if (C' = {TYPES dt'*{dt' : deftype}, RECS [], FUNCS idt*{idt : deftype} :: dt*{dt : deftype}, GLOBALS igt*{igt : globaltype}, TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}) - -- if (idt*{idt : deftype} = $funcsxt(ixt*{ixt : externtype})) - -- if (igt*{igt : globaltype} = $globalsxt(ixt*{ixt : externtype})) - -- if (itt*{itt : tabletype} = $tablesxt(ixt*{ixt : externtype})) - -- if (imt*{imt : memtype} = $memsxt(ixt*{ixt : externtype})) + -- (Export_ok: `%|-%:%`(C, export, xt_E))*{export : export, xt_E : externtype} + -- if (C = {TYPES dt'*{dt' : deftype}, RECS [], FUNCS dt_I*{dt_I : deftype} :: dt*{dt : deftype}, GLOBALS gt_I*{gt_I : globaltype} :: gt*{gt : globaltype}, TABLES tt_I*{tt_I : tabletype} :: tt*{tt : tabletype}, MEMS mt_I*{mt_I : memtype} :: mt*{mt : memtype}, ELEMS rt*{rt : reftype}, DATAS ok*{ok : datatype}, LOCALS [], LABELS [], RETURN ?()}) + -- if (C' = {TYPES dt'*{dt' : deftype}, RECS [], FUNCS dt_I*{dt_I : deftype} :: dt*{dt : deftype}, GLOBALS gt_I*{gt_I : globaltype}, TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], RETURN ?()}) + -- if (dt_I*{dt_I : deftype} = $funcsxt(xt_I*{xt_I : externtype})) + -- if (gt_I*{gt_I : globaltype} = $globalsxt(xt_I*{xt_I : externtype})) + -- if (tt_I*{tt_I : tabletype} = $tablesxt(xt_I*{xt_I : externtype})) + -- if (mt_I*{mt_I : memtype} = $memsxt(xt_I*{xt_I : externtype})) ;; 7-runtime-typing.watsup relation Ref_ok: `%|-%:%`(store, ref, reftype) diff --git a/spectec/test-splice/TEST.md b/spectec/test-splice/TEST.md index 59aaac33f6..0f860e40e2 100644 --- a/spectec/test-splice/TEST.md +++ b/spectec/test-splice/TEST.md @@ -427,6 +427,7 @@ warning: syntax `memidxop` was never spliced warning: syntax `meminst` was never spliced warning: syntax `module` was never spliced warning: syntax `moduleinst` was never spliced +warning: syntax `moduletype` was never spliced warning: syntax `mut` was never spliced warning: syntax `n` was never spliced warning: syntax `name` was never spliced