Restrict shape sizes

Wasm-DSL · Oct 15, 2024 · d3f35fa · d3f35fa
1 parent 7ce6064
commit d3f35fa
Show file tree

Hide file tree

Showing 9 changed files with 31 additions and 109 deletions.
diff --git a/spectec/spec/wasm-3.0/1-syntax.watsup b/spectec/spec/wasm-3.0/1-syntax.watsup
@@ -448,12 +448,12 @@ syntax cvtop__(Fnn_1, Fnn_2) =
 
 ;; Vector shapes
 
-;; TODO(1, rossberg): restrict size to 128
 syntax dim hint(desc "dimension") = `1 | `2 | `4 | `8 | `16
+
 syntax shape hint(desc "shape") = lanetype X dim  hint(show %0#X#%2) hint(macro "%shape")
+  -- if $($lsize(lanetype) * dim = 128)
 syntax ishape hint(desc "shape") = Jnn X dim      hint(show %0#X#%2) hint(macro "%shape")
-syntax fshape hint(desc "shape") = Fnn X dim      hint(show %0#X#%2) hint(macro "%shape")
-syntax pshape hint(desc "shape") = Pnn X dim      hint(show %0#X#%2) hint(macro "%shape")
+  -- if $($lsizenn(Jnn) * dim = 128)
 
 
 def $lanetype(shape) : lanetype hint(macro "shlanetype")
@@ -462,9 +462,6 @@ def $lanetype(Lnn X N) = Lnn
 def $dim(shape) : dim     hint(macro "shdim")
 def $dim(Lnn X N) = N
 
-def $shsize(shape) : nat  hint(show |%|)
-def $shsize(Lnn X N) = $($lsize(Lnn) * N)
-
 def $unpackshape(shape) : numtype  hint(show $unpack(%))
 def $unpackshape(Lnn X N) = $lunpack(Lnn)
 

diff --git a/spectec/spec/wasm-3.0/4-numerics.watsup b/spectec/spec/wasm-3.0/4-numerics.watsup
@@ -422,7 +422,6 @@ def $fvbinop_(shape, def $f_(N, fN(N), fN(N)) : fN(N)*, vec_(V128), vec_(V128))
 def $ivternopnd_(shape, def $f_(N, iN(N), iN(N), iN(N)) : iN(N)*, vec_(V128), vec_(V128), vec_(V128)) : vec_(V128)*
 def $fvternop_(shape, def $f_(N, fN(N), fN(N), fN(N)) : fN(N)*, vec_(V128), vec_(V128), vec_(V128)) : vec_(V128)*
 
-;; TODO(1, rossberg): this is not lane-wise, lump with shape shifters
 def $ivtestop_(shape, def $f_(N, iN(N)) : u32, vec_(V128)) : u32
 def $fvtestop_(shape, def $f_(N, fN(N)) : u32, vec_(V128)) : u32
 

diff --git a/spectec/src/frontend/eval.ml b/spectec/src/frontend/eval.ml
@@ -759,20 +759,21 @@ and sub_typ env t1 t2 =
   match t1.it, t2.it with
   | NumT t1', NumT t2' -> t1' <= t2'
   | StrT tfs1, StrT tfs2 ->
-    El.Convert.forall_nl_list (fun (atom, (t2, prems2), _) ->
+    El.Convert.forall_nl_list (fun (atom, (t2, _prems2), _) ->
       match find_field tfs1 atom with
-      | Some (t1, prems1) ->
-        equiv_typ env t1 t2 && Eq.eq_nl_list Eq.eq_prem prems1 prems2
+      | Some (t1, _prems1) ->
+        equiv_typ env t1 t2 (*&& Eq.eq_nl_list Eq.eq_prem prems1 prems2*)
       | None -> false
     ) tfs2
   | CaseT (NoDots, [], tcs1, NoDots), CaseT (NoDots, [], tcs2, NoDots) ->
-    El.Convert.forall_nl_list (fun (atom, (t1, prems1), _) ->
+    El.Convert.forall_nl_list (fun (atom, (t1, _prems1), _) ->
       match find_case tcs2 atom with
-      | Some (t2, prems2) ->
-        equiv_typ env t1 t2 && Eq.eq_nl_list Eq.eq_prem prems1 prems2
+      | Some (t2, _prems2) ->
+        equiv_typ env t1 t2 (*&& Eq.eq_nl_list Eq.eq_prem prems1 prems2*)
       | None -> false
     ) tcs1
-  | ConT ((t11, _), _), ConT ((t21, _), _) -> sub_typ env t11 t21
+  | ConT ((t11, _prems1), _), ConT ((t21, _prems2), _) ->
+    sub_typ env t11 t21 (*&& Eq.eq_nl_list Eq.eq_prem prems1 prems2*)
 (*
   | ConT ((t11, _), _), _ -> sub_typ env t11 t2
   | _, ConT ((t21, _), _) -> sub_typ env t1 t21

diff --git a/spectec/src/il/eval.ml b/spectec/src/il/eval.ml
@@ -841,6 +841,7 @@ and equiv_iter env iter1 iter2 =
     equiv_exp env e1 e2 && Option.equal (fun id1 id2 -> id1.it = id2.it) ido1 ido2
   | _, _ -> iter1 = iter2
 
+(*
 and equiv_prem env pr1 pr2 =
   match pr1.it, pr2.it with
   | RulePr (id1, mixop1, e1), RulePr (id2, mixop2, e2) ->
@@ -851,6 +852,7 @@ and equiv_prem env pr1 pr2 =
   | IterPr (pr11, iter1), IterPr (pr21, iter2) ->
     equiv_prem env pr11 pr21 && equiv_iter env (fst iter1) (fst iter2)
   | pr1', pr2' -> pr1' = pr2'
+*)
 
 and equiv_exp env e1 e2 =
   Debug.(log "il.equiv_exp"
@@ -916,17 +918,17 @@ and sub_typ env t1 t2 =
   | VarT _, VarT _ ->
     (match (reduce_typdef env t1').it, (reduce_typdef env t2').it with
     | StructT tfs1, StructT tfs2 ->
-      List.for_all (fun (atom, (_binds2, t2, prems2), _) ->
+      List.for_all (fun (atom, (_binds2, t2, _prems2), _) ->
         match find_field tfs1 atom with
-        | Some (_binds1, t1, prems1) ->
-          sub_typ env t1 t2 && equiv_list equiv_prem env prems1 prems2
+        | Some (_binds1, t1, _prems1) ->
+          sub_typ env t1 t2 (*&& equiv_list equiv_prem env prems1 prems2*)
         | None -> false
       ) tfs2
     | VariantT tcs1, VariantT tcs2 ->
-      List.for_all (fun (mixop, (_binds1, t1, prems1), _) ->
+      List.for_all (fun (mixop, (_binds1, t1, _prems1), _) ->
         match find_case tcs2 mixop with
-        | Some (_binds2, t2, prems2) ->
-          sub_typ env t1 t2 && equiv_list equiv_prem env prems1 prems2
+        | Some (_binds2, t2, _prems2) ->
+          sub_typ env t1 t2 (*&& equiv_list equiv_prem env prems1 prems2*)
         | None -> false
       ) tcs1
     | _, _ -> false

diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md
@@ -962,18 +962,12 @@ syntax dim =
 ;; 1-syntax.watsup
 syntax shape =
   | `%X%`{lanetype : lanetype, dim : dim}(lanetype : lanetype, dim : dim)
+    -- if (($lsize(lanetype) * dim!`%`_dim.0) = 128)
 
 ;; 1-syntax.watsup
 syntax ishape =
   | `%X%`{Jnn : Jnn, dim : dim}(Jnn : Jnn, dim : dim)
-
-;; 1-syntax.watsup
-syntax fshape =
-  | `%X%`{Fnn : Fnn, dim : dim}(Fnn : Fnn, dim : dim)
-
-;; 1-syntax.watsup
-syntax pshape =
-  | `%X%`{Pnn : Pnn, dim : dim}(Pnn : Pnn, dim : dim)
+    -- if (($lsizenn((Jnn : Jnn <: lanetype)) * dim!`%`_dim.0) = 128)
 
 ;; 1-syntax.watsup
 def $lanetype(shape : shape) : lanetype
@@ -985,11 +979,6 @@ def $dim(shape : shape) : dim
   ;; 1-syntax.watsup
   def $dim{Lnn : Lnn, N : N}(`%X%`_shape(Lnn, `%`_dim(N))) = `%`_dim(N)
 
-;; 1-syntax.watsup
-def $shsize(shape : shape) : nat
-  ;; 1-syntax.watsup
-  def $shsize{Lnn : Lnn, N : N}(`%X%`_shape(Lnn, `%`_dim(N))) = ($lsize(Lnn) * N)
-
 ;; 1-syntax.watsup
 def $unpackshape(shape : shape) : numtype
   ;; 1-syntax.watsup

diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md
@@ -2831,10 +2831,8 @@ $$
 $$
 \begin{array}[t]{@{}lrrl@{}l@{}}
 \mbox{(dimension)} & {\mathit{dim}} & ::= & \mathsf{{\scriptstyle 1}} ~|~ \mathsf{{\scriptstyle 2}} ~|~ \mathsf{{\scriptstyle 4}} ~|~ \mathsf{{\scriptstyle 8}} ~|~ \mathsf{{\scriptstyle 16}} \\
-\mbox{(shape)} & {\mathit{shape}} & ::= & {{\mathit{lanetype}}}{\mathsf{x}}{{\mathit{dim}}} \\
-\mbox{(shape)} & {\mathit{ishape}} & ::= & {{\mathsf{i}}{N}}{\mathsf{x}}{{\mathit{dim}}} \\
-\mbox{(shape)} & {\mathit{fshape}} & ::= & {{\mathsf{f}}{N}}{\mathsf{x}}{{\mathit{dim}}} \\
-\mbox{(shape)} & {\mathit{pshape}} & ::= & {{\mathsf{i}}{N}}{\mathsf{x}}{{\mathit{dim}}} \\
+\mbox{(shape)} & {\mathit{shape}} & ::= & {{\mathit{lanetype}}}{\mathsf{x}}{{\mathit{dim}}} & \quad \mbox{if}~ {|{\mathit{lanetype}}|} \cdot {\mathit{dim}} = 128 \\
+\mbox{(shape)} & {\mathit{ishape}} & ::= & {{\mathsf{i}}{N}}{\mathsf{x}}{{\mathit{dim}}} & \quad \mbox{if}~ N \cdot {\mathit{dim}} = 128 \\
 \end{array}
 $$
 
@@ -2852,12 +2850,6 @@ $$
 \end{array}
 $$
 
-$$
-\begin{array}[t]{@{}lcl@{}l@{}}
-{|{{\mathsf{i}}{N}}{\mathsf{x}}{N}|} & = & {|{\mathsf{i}}{N}|} \cdot N \\
-\end{array}
-$$
-
 $$
 \begin{array}[t]{@{}lcl@{}l@{}}
 {\mathrm{unpack}}({{\mathsf{i}}{N}}{\mathsf{x}}{N}) & = & {\mathrm{unpack}}({\mathsf{i}}{N}) \\

diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md
@@ -952,18 +952,12 @@ syntax dim =
 ;; 1-syntax.watsup
 syntax shape =
   | `%X%`{lanetype : lanetype, dim : dim}(lanetype : lanetype, dim : dim)
+    -- if (($lsize(lanetype) * dim!`%`_dim.0) = 128)
 
 ;; 1-syntax.watsup
 syntax ishape =
   | `%X%`{Jnn : Jnn, dim : dim}(Jnn : Jnn, dim : dim)
-
-;; 1-syntax.watsup
-syntax fshape =
-  | `%X%`{Fnn : Fnn, dim : dim}(Fnn : Fnn, dim : dim)
-
-;; 1-syntax.watsup
-syntax pshape =
-  | `%X%`{Pnn : Pnn, dim : dim}(Pnn : Pnn, dim : dim)
+    -- if (($lsizenn((Jnn : Jnn <: lanetype)) * dim!`%`_dim.0) = 128)
 
 ;; 1-syntax.watsup
 def $lanetype(shape : shape) : lanetype
@@ -975,11 +969,6 @@ def $dim(shape : shape) : dim
   ;; 1-syntax.watsup
   def $dim{Lnn : Lnn, N : N}(`%X%`_shape(Lnn, `%`_dim(N))) = `%`_dim(N)
 
-;; 1-syntax.watsup
-def $shsize(shape : shape) : nat
-  ;; 1-syntax.watsup
-  def $shsize{Lnn : Lnn, N : N}(`%X%`_shape(Lnn, `%`_dim(N))) = ($lsize(Lnn) * N)
-
 ;; 1-syntax.watsup
 def $unpackshape(shape : shape) : numtype
   ;; 1-syntax.watsup
@@ -9749,18 +9738,12 @@ syntax dim =
 ;; 1-syntax.watsup
 syntax shape =
   | `%X%`{lanetype : lanetype, dim : dim}(lanetype : lanetype, dim : dim)
+    -- if (($lsize(lanetype) * dim!`%`_dim.0) = 128)
 
 ;; 1-syntax.watsup
 syntax ishape =
   | `%X%`{Jnn : Jnn, dim : dim}(Jnn : Jnn, dim : dim)
-
-;; 1-syntax.watsup
-syntax fshape =
-  | `%X%`{Fnn : Fnn, dim : dim}(Fnn : Fnn, dim : dim)
-
-;; 1-syntax.watsup
-syntax pshape =
-  | `%X%`{Pnn : Pnn, dim : dim}(Pnn : Pnn, dim : dim)
+    -- if (($lsizenn((Jnn : Jnn <: lanetype)) * dim!`%`_dim.0) = 128)
 
 ;; 1-syntax.watsup
 def $lanetype(shape : shape) : lanetype
@@ -9772,11 +9755,6 @@ def $dim(shape : shape) : dim
   ;; 1-syntax.watsup
   def $dim{Lnn : Lnn, N : N}(`%X%`_shape(Lnn, `%`_dim(N))) = `%`_dim(N)
 
-;; 1-syntax.watsup
-def $shsize(shape : shape) : nat
-  ;; 1-syntax.watsup
-  def $shsize{Lnn : Lnn, N : N}(`%X%`_shape(Lnn, `%`_dim(N))) = ($lsize(Lnn) * N)
-
 ;; 1-syntax.watsup
 def $unpackshape(shape : shape) : numtype
   ;; 1-syntax.watsup
@@ -18548,18 +18526,12 @@ syntax dim =
 ;; 1-syntax.watsup
 syntax shape =
   | `%X%`{lanetype : lanetype, dim : dim}(lanetype : lanetype, dim : dim)
+    -- if (($lsize(lanetype) * dim!`%`_dim.0) = 128)
 
 ;; 1-syntax.watsup
 syntax ishape =
   | `%X%`{Jnn : Jnn, dim : dim}(Jnn : Jnn, dim : dim)
-
-;; 1-syntax.watsup
-syntax fshape =
-  | `%X%`{Fnn : Fnn, dim : dim}(Fnn : Fnn, dim : dim)
-
-;; 1-syntax.watsup
-syntax pshape =
-  | `%X%`{Pnn : Pnn, dim : dim}(Pnn : Pnn, dim : dim)
+    -- if (($lsizenn((Jnn : Jnn <: lanetype)) * dim!`%`_dim.0) = 128)
 
 ;; 1-syntax.watsup
 def $lanetype(shape : shape) : lanetype
@@ -18571,11 +18543,6 @@ def $dim(shape : shape) : dim
   ;; 1-syntax.watsup
   def $dim{Lnn : Lnn, N : N}(`%X%`_shape(Lnn, `%`_dim(N))) = `%`_dim(N)
 
-;; 1-syntax.watsup
-def $shsize(shape : shape) : nat
-  ;; 1-syntax.watsup
-  def $shsize{Lnn : Lnn, N : N}(`%X%`_shape(Lnn, `%`_dim(N))) = ($lsize(Lnn) * N)
-
 ;; 1-syntax.watsup
 def $unpackshape(shape : shape) : numtype
   ;; 1-syntax.watsup
@@ -27347,18 +27314,12 @@ syntax dim =
 ;; 1-syntax.watsup
 syntax shape =
   | `%X%`{lanetype : lanetype, dim : dim}(lanetype : lanetype, dim : dim)
+    -- if (($lsize(lanetype) * dim!`%`_dim.0) = 128)
 
 ;; 1-syntax.watsup
 syntax ishape =
   | `%X%`{Jnn : Jnn, dim : dim}(Jnn : Jnn, dim : dim)
-
-;; 1-syntax.watsup
-syntax fshape =
-  | `%X%`{Fnn : Fnn, dim : dim}(Fnn : Fnn, dim : dim)
-
-;; 1-syntax.watsup
-syntax pshape =
-  | `%X%`{Pnn : Pnn, dim : dim}(Pnn : Pnn, dim : dim)
+    -- if (($lsizenn((Jnn : Jnn <: lanetype)) * dim!`%`_dim.0) = 128)
 
 ;; 1-syntax.watsup
 def $lanetype(shape : shape) : lanetype
@@ -27370,11 +27331,6 @@ def $dim(shape : shape) : dim
   ;; 1-syntax.watsup
   def $dim{Lnn : Lnn, N : N}(`%X%`_shape(Lnn, `%`_dim(N))) = `%`_dim(N)
 
-;; 1-syntax.watsup
-def $shsize(shape : shape) : nat
-  ;; 1-syntax.watsup
-  def $shsize{Lnn : Lnn, N : N}(`%X%`_shape(Lnn, `%`_dim(N))) = ($lsize(Lnn) * N)
-
 ;; 1-syntax.watsup
 def $unpackshape(shape : shape) : numtype
   ;; 1-syntax.watsup

diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md
@@ -17081,13 +17081,6 @@ watsup 0.4 generator
 1. Return :math:`N`.
 
 
-:math:`{|({{\mathsf{i}}{N}}{\mathsf{x}}{N})|}`
-..............................................
-
-
-1. Return :math:`{|{\mathsf{i}}{N}|} \cdot N`.
-
-
 :math:`{\mathrm{unpack}}(({{\mathsf{i}}{N}}{\mathsf{x}}{N}))`
 .............................................................
 
@@ -24800,9 +24793,6 @@ lanetype (Lnn X N)
 dim (Lnn X N)
 1. Return N.
 
-shsize (Lnn X N)
-1. Return ($lsize(Lnn) · N).
-
 unpackshape (Lnn X N)
 1. Return $lunpack(Lnn).
 

diff --git a/spectec/test-splice/TEST.md b/spectec/test-splice/TEST.md
@@ -347,7 +347,6 @@ warning: syntax `fieldval` was never spliced
 warning: syntax `fin` was never spliced
 warning: syntax `frame` was never spliced
 warning: syntax `free` was never spliced
-warning: syntax `fshape` was never spliced
 warning: syntax `func` was never spliced
 warning: syntax `funcaddr` was never spliced
 warning: syntax `funccode` was never spliced
@@ -427,7 +426,6 @@ warning: syntax `oktypeidxnat` was never spliced
 warning: syntax `pack_` was never spliced
 warning: syntax `packtype` was never spliced
 warning: syntax `packval` was never spliced
-warning: syntax `pshape` was never spliced
 warning: syntax `pth` was never spliced
 warning: syntax `record` was never spliced
 warning: syntax `recorddots` was never spliced
@@ -1482,7 +1480,6 @@ warning: definition `setproduct1_` was never spliced
 warning: definition `setproduct2_` was never spliced
 warning: definition `setproduct_` was never spliced
 warning: definition `shift_labelidxs` was never spliced
-warning: definition `shsize` was never spliced
 warning: definition `signed_` was never spliced
 warning: definition `signif` was never spliced
 warning: definition `sizenn` was never spliced
@@ -2096,7 +2093,6 @@ warning: definition prose `setproduct1_` was never spliced
 warning: definition prose `setproduct2_` was never spliced
 warning: definition prose `setproduct_` was never spliced
 warning: definition prose `shift_labelidxs` was never spliced
-warning: definition prose `shsize` was never spliced
 warning: definition prose `signed_` was never spliced
 warning: definition prose `signif` was never spliced
 warning: definition prose `size` was never spliced