Skip to content

Commit

Permalink
Convert exec/types
Browse files Browse the repository at this point in the history
  • Loading branch information
@rossberg
rossberg committed Jun 1, 2024
1 parent 3e65eb8 commit c29d540
Show file tree
Hide file tree
Showing 7 changed files with 172 additions and 116 deletions.
7 changes: 5 additions & 2 deletions document/core/exec/types.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
Types
-----

Execution has to check and compare :ref:`types <syntax-type>` in a few places, such as :ref:`executing <exec-call_indirect>` |CALLINDIRECT| or :ref:`instantiating <exec-instantiation>` :ref:`modules <syntax-module>`.
Execution has to check and compare :ref:`types <syntax-type>` in a few places, such as :ref:`executing <exec-call_indirect>` ${:CALL_INDIRECT} or :ref:`instantiating <exec-instantiation>` :ref:`modules <syntax-module>`.

It is an invariant of the semantics that all types occurring during execution are :ref:`closed <type-closed>`.

Expand All @@ -20,7 +20,10 @@ It is an invariant of the semantics that all types occurring during execution ar
Instantiation
~~~~~~~~~~~~~

Any form of :ref:`type <syntax-type>` can be *instantiated* into a :ref:`closed <type-closed>` type inside a :ref:`module instance <syntax-moduleinst>` by :ref:`substituting <notation-subst>` each :ref:`type index <syntax-typeidx>` :math:`x` occurring in it with the corresponding :ref:`defined type <syntax-deftype>` :math:`\moduleinst.\MITYPES[x]`.
Any form of :ref:`type <syntax-type>` can be *instantiated* into a :ref:`closed <type-closed>` type inside a :ref:`module instance <syntax-moduleinst>` by :ref:`substituting <notation-subst>` each :ref:`type index <syntax-typeidx>` ${:x} occurring in it with the corresponding :ref:`defined type <syntax-deftype>` ${deftype: moduleinst.TYPES[x]}.

$${definition: inst_valtype}
$${definition-ignore: inst_reftype}

.. math::
\insttype_{\moduleinst}(t) = t[\subst \moduleinst.\MITYPES]
Expand Down
8 changes: 6 additions & 2 deletions spectec/spec/wasm-3.0/5-runtime-aux.watsup
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,10 +4,14 @@

;; Instantiation

def $inst_valtype(moduleinst, valtype) : valtype hint(show $inst_(%,%)) hint(macro "insttype")
def $inst_reftype(moduleinst, reftype) : reftype hint(show $inst_(%,%)) hint(macro "insttype")

def $inst_reftype(mm, rt) = $subst_all_reftype(rt, dt*)
-- if dt* = mm.TYPES
;; TODO: make inlining moduleinst.TYPES work
def $inst_valtype(moduleinst, t) = $subst_all_valtype(t, dt*)
-- if dt* = moduleinst.TYPES
def $inst_reftype(moduleinst, rt) = $subst_all_reftype(rt, dt*)
-- if dt* = moduleinst.TYPES


;;
Expand Down
42 changes: 24 additions & 18 deletions spectec/test-frontend/TEST.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2548,11 +2548,17 @@ syntax state =
syntax config =
| `%;%`{state : state, instr* : instr*}(state : state, instr*{instr : instr} : instr*)

;; 5-runtime-aux.watsup
def $inst_valtype(moduleinst : moduleinst, valtype : valtype) : valtype
;; 5-runtime-aux.watsup
def $inst_valtype{moduleinst : moduleinst, t : valtype, dt* : deftype*}(moduleinst, t) = $subst_all_valtype(t, (dt : deftype <: heaptype)*{dt : deftype})
-- if (dt*{dt : deftype} = moduleinst.TYPES_moduleinst)

;; 5-runtime-aux.watsup
def $inst_reftype(moduleinst : moduleinst, reftype : reftype) : reftype
;; 5-runtime-aux.watsup
def $inst_reftype{mm : moduleinst, rt : reftype, dt* : deftype*}(mm, rt) = $subst_all_reftype(rt, (dt : deftype <: heaptype)*{dt : deftype})
-- if (dt*{dt : deftype} = mm.TYPES_moduleinst)
def $inst_reftype{moduleinst : moduleinst, rt : reftype, dt* : deftype*}(moduleinst, rt) = $subst_all_reftype(rt, (dt : deftype <: heaptype)*{dt : deftype})
-- if (dt*{dt : deftype} = moduleinst.TYPES_moduleinst)

;; 5-runtime-aux.watsup
def $default_(valtype : valtype) : val?
Expand Down Expand Up @@ -2584,55 +2590,55 @@ def $unpackfield(storagetype : storagetype, sx?, fieldval : fieldval) : val
;; 5-runtime-aux.watsup
rec {

;; 5-runtime-aux.watsup:42.1-42.86
;; 5-runtime-aux.watsup:46.1-46.86
def $funcsxv(externval*) : funcaddr*
;; 5-runtime-aux.watsup:47.1-47.24
;; 5-runtime-aux.watsup:51.1-51.24
def $funcsxv([]) = []
;; 5-runtime-aux.watsup:48.1-48.47
;; 5-runtime-aux.watsup:52.1-52.47
def $funcsxv{fa : funcaddr, xv* : externval*}([FUNC_externval(fa)] :: xv*{xv : externval}) = [fa] :: $funcsxv(xv*{xv : externval})
;; 5-runtime-aux.watsup:49.1-49.58
;; 5-runtime-aux.watsup:53.1-53.58
def $funcsxv{externval : externval, xv* : externval*}([externval] :: xv*{xv : externval}) = $funcsxv(xv*{xv : externval})
-- otherwise
}

;; 5-runtime-aux.watsup
rec {

;; 5-runtime-aux.watsup:43.1-43.88
;; 5-runtime-aux.watsup:47.1-47.88
def $globalsxv(externval*) : globaladdr*
;; 5-runtime-aux.watsup:51.1-51.26
;; 5-runtime-aux.watsup:55.1-55.26
def $globalsxv([]) = []
;; 5-runtime-aux.watsup:52.1-52.53
;; 5-runtime-aux.watsup:56.1-56.53
def $globalsxv{ga : globaladdr, xv* : externval*}([GLOBAL_externval(ga)] :: xv*{xv : externval}) = [ga] :: $globalsxv(xv*{xv : externval})
;; 5-runtime-aux.watsup:53.1-53.62
;; 5-runtime-aux.watsup:57.1-57.62
def $globalsxv{externval : externval, xv* : externval*}([externval] :: xv*{xv : externval}) = $globalsxv(xv*{xv : externval})
-- otherwise
}

;; 5-runtime-aux.watsup
rec {

;; 5-runtime-aux.watsup:44.1-44.87
;; 5-runtime-aux.watsup:48.1-48.87
def $tablesxv(externval*) : tableaddr*
;; 5-runtime-aux.watsup:55.1-55.25
;; 5-runtime-aux.watsup:59.1-59.25
def $tablesxv([]) = []
;; 5-runtime-aux.watsup:56.1-56.50
;; 5-runtime-aux.watsup:60.1-60.50
def $tablesxv{ta : tableaddr, xv* : externval*}([TABLE_externval(ta)] :: xv*{xv : externval}) = [ta] :: $tablesxv(xv*{xv : externval})
;; 5-runtime-aux.watsup:57.1-57.60
;; 5-runtime-aux.watsup:61.1-61.60
def $tablesxv{externval : externval, xv* : externval*}([externval] :: xv*{xv : externval}) = $tablesxv(xv*{xv : externval})
-- otherwise
}

;; 5-runtime-aux.watsup
rec {

;; 5-runtime-aux.watsup:45.1-45.85
;; 5-runtime-aux.watsup:49.1-49.85
def $memsxv(externval*) : memaddr*
;; 5-runtime-aux.watsup:59.1-59.23
;; 5-runtime-aux.watsup:63.1-63.23
def $memsxv([]) = []
;; 5-runtime-aux.watsup:60.1-60.44
;; 5-runtime-aux.watsup:64.1-64.44
def $memsxv{ma : memaddr, xv* : externval*}([MEM_externval(ma)] :: xv*{xv : externval}) = [ma] :: $memsxv(xv*{xv : externval})
;; 5-runtime-aux.watsup:61.1-61.56
;; 5-runtime-aux.watsup:65.1-65.56
def $memsxv{externval : externval, xv* : externval*}([externval] :: xv*{xv : externval}) = $memsxv(xv*{xv : externval})
-- otherwise
}
Expand Down
11 changes: 9 additions & 2 deletions spectec/test-latex/TEST.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3079,8 +3079,15 @@ $$

$$
\begin{array}{@{}lcl@{}l@{}}
{{\mathrm{inst}}}_{{\mathit{mm}}}({\mathit{rt}}) &=& {{\mathit{rt}}}{{}[ { := }\;{{\mathit{dt}}^\ast} ]}
&\qquad \mbox{if}~{{\mathit{dt}}^\ast} = {\mathit{mm}}{.}\mathsf{types} \\
{{\mathrm{inst}}}_{{\mathit{moduleinst}}}(t) &=& {t}{{}[ { := }\;{{\mathit{dt}}^\ast} ]}
&\qquad \mbox{if}~{{\mathit{dt}}^\ast} = {\mathit{moduleinst}}{.}\mathsf{types} \\
\end{array}
$$

$$
\begin{array}{@{}lcl@{}l@{}}
{{\mathrm{inst}}}_{{\mathit{moduleinst}}}({\mathit{rt}}) &=& {{\mathit{rt}}}{{}[ { := }\;{{\mathit{dt}}^\ast} ]}
&\qquad \mbox{if}~{{\mathit{dt}}^\ast} = {\mathit{moduleinst}}{.}\mathsf{types} \\
\end{array}
$$

Expand Down
Loading

0 comments on commit c29d540

Please sign in to comment.