Type construction functions

Wasm-DSL · Jun 29, 2024 · f9adc39 · f9adc39
1 parent e73fc48
commit f9adc39
Show file tree

Hide file tree

Showing 7 changed files with 1,427 additions and 1,335 deletions.
diff --git a/spectec/spec/wasm-3.0/1-syntax.watsup b/spectec/spec/wasm-3.0/1-syntax.watsup
@@ -419,7 +419,6 @@ syntax vrelop_(Fnn X M) = EQ | NE | LT | GT | LE | GE
 syntax vcvtop_(shape_1, shape_2) hint(show vcvtop_((%,%))) hint(macro "%" "V%")
 syntax vcvtop_(Jnn_1 X M_1, Jnn_2 X M_2) =
   | EXTEND    -- if $lsizenn2(Jnn_2) = $(2 * $lsizenn1(Jnn_1))
-  ;; TODO(1, rossberg): turn back into VEXTEND
 syntax vcvtop_(Jnn_1 X M_1, Fnn_2 X M_2) =
   | CONVERT   -- if $sizenn2(Fnn_2) >= $lsizenn1(Jnn_1) = `32
 syntax vcvtop_(Fnn_1 X M_1, Jnn_2 X M_2) =

diff --git a/spectec/spec/wasm-3.0/2-syntax-aux.watsup b/spectec/spec/wasm-3.0/2-syntax-aux.watsup
@@ -48,14 +48,20 @@ def $zsize(numtype) = $size(numtype)
 def $zsize(vectype) = $vsize(vectype)
 def $zsize(packtype) = $psize(packtype)
 
-def $IN(N) : numtype  hint(show I#%) hint(macro "INX")
+def $IN(N) : Inn  hint(show I#%) hint(macro "INX")
 def $IN(32) = I32
 def $IN(64) = I64
 
-def $FN(N) : numtype  hint(show F#%) hint(macro "FNX")
+def $FN(N) : Fnn  hint(show F#%) hint(macro "FNX")
 def $FN(32) = F32
 def $FN(64) = F64
 
+def $JN(N) : Jnn  hint(show I#%) hint(macro "INX")
+def $JN(8) = I8
+def $JN(16) = I16
+def $JN(32) = I32
+def $JN(64) = I64
+
 
 ;; Unpacking
 

diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md
diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md
@@ -2085,6 +2085,15 @@ $$
 \end{array}
 $$
 
+$$
+\begin{array}{@{}lcl@{}l@{}}
+{\mathsf{i}}{8} &=& \mathsf{i{\scriptstyle 8}} \\
+{\mathsf{i}}{16} &=& \mathsf{i{\scriptstyle 16}} \\
+{\mathsf{i}}{32} &=& \mathsf{i{\scriptstyle 32}} \\
+{\mathsf{i}}{64} &=& \mathsf{i{\scriptstyle 64}} \\
+\end{array}
+$$
+
 \vspace{1ex}
 
 $$

diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md
diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md
@@ -4380,6 +4380,16 @@ FN N_u0
 2. Assert: Due to validation, (N_u0 is 64).
 3. Return F64.
 
+JN N_u0
+1. If (N_u0 is 8), then:
+  a. Return I8.
+2. If (N_u0 is 16), then:
+  a. Return I16.
+3. If (N_u0 is 32), then:
+  a. Return I32.
+4. Assert: Due to validation, (N_u0 is 64).
+5. Return I64.
+
 lunpack lanet_u0
 1. If the type of lanet_u0 is numtype, then:
   a. Let numtype be lanet_u0.

diff --git a/spectec/test-splice/TEST.md b/spectec/test-splice/TEST.md
@@ -1141,6 +1141,7 @@ warning: definition `FN` was never spliced
 warning: definition `FUNCREF` was never spliced
 warning: definition `I31REF` was never spliced
 warning: definition `IN` was never spliced
+warning: definition `JN` was never spliced
 warning: definition `Ki` was never spliced
 warning: definition `M` was never spliced
 warning: definition `NULLEXTERNREF` was never spliced
@@ -1667,6 +1668,7 @@ warning: definition prose `FN` was never spliced
 warning: definition prose `FUNCREF` was never spliced
 warning: definition prose `I31REF` was never spliced
 warning: definition prose `IN` was never spliced
+warning: definition prose `JN` was never spliced
 warning: definition prose `Ki` was never spliced
 warning: definition prose `M` was never spliced
 warning: definition prose `NULLEXTERNREF` was never spliced