Introduce bshape

document/core/syntax/instructions.rst

@@ -117,7 +117,8 @@ Vector Instructions
 
 Vector instructions (also known as *SIMD* instructions, *single instruction multiple data*) provide basic operations over :ref:`values <syntax-value>` of :ref:`vector type <syntax-vectype>`.
 
-$${syntax: {lanetype dim shape ishape} half__ zero__ laneidx instr/vec}
+$${syntax: {lanetype dim shape ishape bshape} half__ zero__ laneidx instr/vec}
+$${syntax-ignore: J8}
 
 $${syntax:
   vvunop vvbinop vvternop vvtestop

document/core/util/macros.def

@@ -752,9 +752,9 @@
 .. |frelop| mathdef:: \xref{syntax/instructions}{syntax-relop}{\X{frelop}}
 
 .. |dim| mathdef:: \xref{syntax/instructions}{syntax-dim}{\X{dim}}
-.. |ishape| mathdef:: \xref{syntax/instructions}{syntax-shape}{\X{ishape}}
-.. |fshape| mathdef:: \xref{syntax/instructions}{syntax-shape}{\X{fshape}}
 .. |shape| mathdef:: \xref{syntax/instructions}{syntax-shape}{\X{shape}}
+.. |ishape| mathdef:: \xref{syntax/instructions}{syntax-shape}{\X{ishape}}
+.. |bshape| mathdef:: \xref{syntax/instructions}{syntax-shape}{\X{bshape}}
 
 .. |vvunop| mathdef:: \xref{syntax/instructions}{syntax-vvunop}{\X{vvunop}}
 .. |vvbinop| mathdef:: \xref{syntax/instructions}{syntax-vvbinop}{\X{vvbinop}}

spectec/spec/wasm-3.0/1-syntax.watsup

@@ -449,23 +449,24 @@ syntax cvtop__(Fnn_1, Fnn_2) =
 ;; Vector shapes
 
 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")
-  -- if $($lsizenn(Jnn) * dim = 128)
-
 
-def $lanetype(shape) : lanetype hint(macro "shlanetype")
-def $lanetype(Lnn X N) = Lnn
 
-def $dim(shape) : dim     hint(macro "shdim")
+def $dim(shape) : dim  hint(macro "shdim")
 def $dim(Lnn X N) = N
 
+def $lanetype(shape) : lanetype  hint(macro "shlanetype")
+def $lanetype(Lnn X N) = Lnn
+
 def $unpackshape(shape) : numtype  hint(show $unpack(%))
 def $unpackshape(Lnn X N) = $lunpack(Lnn)
 
 
+syntax ishape hint(desc "integer shape") = shape -- if $lanetype(shape) = Jnn
+syntax bshape hint(desc "byte shape") = shape    -- if $lanetype(shape) = I8
+
+
 ;; Vector operators
 
 syntax half__(shape_1, shape_2)
@@ -515,27 +516,10 @@ syntax vrelop_(Jnn X M) = EQ | NE
   | GE sx hint(show GE#_#%)  -- if $lsizenn(Jnn) =/= `64 \/ sx = S
 syntax vrelop_(Fnn X M) = EQ | NE | LT | GT | LE | GE
 
-;; TODO(2, rossberg): internalise half and zero
-syntax vcvtop__(shape_1, shape_2) hint(macro "%" "V%")
-syntax vcvtop__(Jnn_1 X M_1, Jnn_2 X M_2) =
-  | EXTEND sx hint(show EXTEND#_#%)
-    -- if $lsizenn2(Jnn_2) = $(2 * $lsizenn1(Jnn_1))
-syntax vcvtop__(Jnn_1 X M_1, Fnn_2 X M_2) =
-  | CONVERT sx hint(show CONVERT#_#%)
-    -- if $sizenn2(Fnn_2) >= $lsizenn1(Jnn_1) = `32
-syntax vcvtop__(Fnn_1 X M_1, Jnn_2 X M_2) =
-  | TRUNC_SAT sx hint(show TRUNC_SAT#_#%)
-    -- if $sizenn1(Fnn_1) >= $lsizenn2(Jnn_2) = `32
-  | RELAXED_TRUNC sx hint(show RELAXED_TRUNC#_#%)
-    -- if $sizenn1(Fnn_1) >= $lsizenn2(Jnn_2) = `32
-syntax vcvtop__(Fnn_1 X M_1, Fnn_2 X M_2) =
-  | DEMOTE    -- if $sizenn1(Fnn_1) > $sizenn2(Fnn_2)
-  | PROMOTE   -- if $sizenn1(Fnn_1) < $sizenn2(Fnn_2)
-
 syntax vshiftop_(ishape) hint(macro "%" "V%")
 syntax vshiftop_(Jnn X M) = SHL | SHR sx hint(show SHR#_#%)
 
-syntax vswizzlop_(ishape) hint(macro "%" "V%")
+syntax vswizzlop_(bshape) hint(macro "%" "V%")
 syntax vswizzlop_(I8 X M) = SWIZZLE | RELAXED_SWIZZLE
 
 syntax vextunop__(ishape_1, ishape_2) hint(macro "%" "V%")
@@ -557,6 +541,23 @@ syntax vextternop__(Jnn_1 X M_1, Jnn_2 X M_2) =
   | RELAXED_DOT_ADD S hint(show RELAXED_DOT_ADD#_#%)
     -- if $(4 * $lsizenn1(Jnn_1)) = $lsizenn2(Jnn_2) = `32
 
+;; TODO(2, rossberg): internalise half and zero
+syntax vcvtop__(shape_1, shape_2) hint(macro "%" "V%")
+syntax vcvtop__(Jnn_1 X M_1, Jnn_2 X M_2) =
+  | EXTEND sx hint(show EXTEND#_#%)
+    -- if $lsizenn2(Jnn_2) = $(2 * $lsizenn1(Jnn_1))
+syntax vcvtop__(Jnn_1 X M_1, Fnn_2 X M_2) =
+  | CONVERT sx hint(show CONVERT#_#%)
+    -- if $sizenn2(Fnn_2) >= $lsizenn1(Jnn_1) = `32
+syntax vcvtop__(Fnn_1 X M_1, Jnn_2 X M_2) =
+  | TRUNC_SAT sx hint(show TRUNC_SAT#_#%)
+    -- if $sizenn1(Fnn_1) >= $lsizenn2(Jnn_2) = `32
+  | RELAXED_TRUNC sx hint(show RELAXED_TRUNC#_#%)
+    -- if $sizenn1(Fnn_1) >= $lsizenn2(Jnn_2) = `32
+syntax vcvtop__(Fnn_1 X M_1, Fnn_2 X M_2) =
+  | DEMOTE    -- if $sizenn1(Fnn_1) > $sizenn2(Fnn_2)
+  | PROMOTE   -- if $sizenn1(Fnn_1) < $sizenn2(Fnn_2)
+
 
 ;; Memory operators
 
@@ -658,10 +659,9 @@ syntax instr/vec hint(desc "vector instruction") = ...
   | VRELOP shape vrelop_(shape)         hint(show ##%.##%)
   | VSHIFTOP ishape vshiftop_(ishape)   hint(show ##%.##%)
   | VBITMASK ishape                     hint(show ##%.BITMASK)   hint(macro "VBITMASK")
-  | VSWIZZLOP ishape vswizzlop_(ishape) hint(show ##%.##%)
-  | VSHUFFLE ishape laneidx*            hint(show ##%.SHUFFLE %) hint(macro "VSHUFFLE")
-    -- if ishape = I8 X `16 /\ |laneidx*| = `16
-    ;; TODO(3, rossberg): enable ^16 in type
+  | VSWIZZLOP bshape vswizzlop_(bshape) hint(show ##%.##%)
+  | VSHUFFLE bshape laneidx*            hint(show ##%.SHUFFLE %) hint(macro "VSHUFFLE")
+    -- if |laneidx*| = $dim(bshape)
   | VEXTUNOP ishape_1 ishape_2 vextunop__(ishape_2, ishape_1)
     hint(show ##%1.##%3#_# ##%2)
   | VEXTBINOP ishape_1 ishape_2 vextbinop__(ishape_2, ishape_1)

spectec/spec/wasm-3.0/2-syntax-aux.watsup

@@ -470,8 +470,8 @@ def $free_instr(VTESTOP shape vtestop) = $free_shape(shape)
 def $free_instr(VRELOP shape vrelop) = $free_shape(shape)
 def $free_instr(VSHIFTOP ishape vshiftop) = $free_shape(ishape)
 def $free_instr(VBITMASK ishape) = $free_shape(ishape)
-def $free_instr(VSWIZZLOP ishape vswizzlop) = $free_shape(ishape)
-def $free_instr(VSHUFFLE ishape laneidx*) = $free_shape(ishape)
+def $free_instr(VSWIZZLOP bshape vswizzlop) = $free_shape(bshape)
+def $free_instr(VSHUFFLE bshape laneidx*) = $free_shape(bshape)
 def $free_instr(VEXTUNOP ishape_1 ishape_2 vextunop) =
   $free_shape(ishape_1) ++ $free_shape(ishape_2)
 def $free_instr(VEXTBINOP ishape_1 ishape_2 vextbinop) =

spectec/spec/wasm-3.0/4-numerics.watsup

@@ -561,9 +561,9 @@ def $vshiftop_(ishape, vshiftop_(ishape), vec_(V128), u32) : vec_(V128)
     hint(show %2#$_(%1)#(%3, %4))
 def $vbitmaskop_(ishape, vec_(V128)) : u32
     hint(show VBITMASK#$_(%1,%2))
-def $vswizzlop_(ishape, vswizzlop_(ishape), vec_(V128), vec_(V128)) : vec_(V128)
+def $vswizzlop_(bshape, vswizzlop_(bshape), vec_(V128), vec_(V128)) : vec_(V128)
     hint(show %2#$_(%1,%3,%4))
-def $vshufflop_(ishape, laneidx*, vec_(V128), vec_(V128)) : vec_(V128)
+def $vshufflop_(bshape, laneidx*, vec_(V128), vec_(V128)) : vec_(V128)
     hint(show VSHUFFLE#$_(%1,%2,%3,%4))
 
 def $vnarrowop__(shape_1, shape_2, sx, vec_(V128), vec_(V128)) : vec_(V128)

spectec/src/el/debug.ml

@@ -10,11 +10,15 @@ let el_typfield = string_of_typfield
 let el_exp = string_of_exp
 let el_expfield = string_of_expfield
 let el_sym = string_of_sym
+let el_prem = string_of_prem
 let el_arg = string_of_arg
 let el_param = string_of_param
 let el_args = list el_arg
 let el_params = list el_param
 let el_def = string_of_def
+
+let nl_list f xs = list f (Convert.filter_nl xs)
+
 let el_free s = String.concat " "
   Free.[
     set s.typid;

spectec/src/frontend/elab.ml

@@ -1507,15 +1507,29 @@ and cast_exp' phrase env e' t1 t2 : Il.exp' =
   | TupT [], SeqT [] ->
     e'.it
   | ConT ((t11, _), _), ConT ((t21, _), _) ->
-    let mixop1, ts1', ts1 = elab_typ_notation env (expand_id env t1) t11 in
-    let mixop2, _ts2', ts2 = elab_typ_notation env (expand_id env t2) t21 in
-    if mixop1 <> mixop2 then
-      error_typ2 env e'.at phrase t1 t2 "";
-    let e'' = Il.UncaseE (e', mixop1) $$ e'.at % tup_typ' ts1' e'.at in
-    let es' = List.mapi (fun i t1I' -> Il.ProjE (e'', i) $$ e''.at % t1I') ts1' in
-    let es'' = List.map2 (fun eI' (t1I, t2I) ->
-      cast_exp phrase env eI' t1I t2I) es' (List.combine ts1 ts2) in
-    Il.CaseE (mixop2, tup_exp_bind' es'' e'.at)
+    (try
+      let mixop1, ts1', ts1 = elab_typ_notation env (expand_id env t1) t11 in
+      let mixop2, _ts2', ts2 = elab_typ_notation env (expand_id env t2) t21 in
+      if mixop1 <> mixop2 then
+        error_typ2 env e'.at phrase t1 t2 "";
+      let e'' = Il.UncaseE (e', mixop1) $$ e'.at % tup_typ' ts1' e'.at in
+      let es' = List.mapi (fun i t1I' -> Il.ProjE (e'', i) $$ e''.at % t1I') ts1' in
+      let es'' = List.map2 (fun eI' (t1I, t2I) ->
+        cast_exp phrase env eI' t1I t2I) es' (List.combine ts1 ts2) in
+      Il.CaseE (mixop2, tup_exp_bind' es'' e'.at)
+    with Error _ ->  (* backtrack *)
+      Debug.(log_in_at "el.cast_exp" e'.at
+        (fun _ -> fmt "%s <: %s  >>  (%s) <: (%s) = (%s) # backtrack 1" (el_typ t1) (el_typ t2)
+          (el_typ (expand_def env t1 $ t1.at)) (el_typ (expand_def env t2 $ t2.at))
+          (el_typ (expand_nondef env t2))
+        )
+      );
+      let mixop, ts', ts = elab_typ_notation env (expand_id env t1) t11 in
+      let t111, t111' = match ts, ts' with [t111], [t111'] -> t111, t111' | _ ->
+        error_typ2 env e'.at phrase t1 t2 "" in
+      let e'' = Il.UncaseE (e', mixop) $$ e'.at % tup_typ' ts' e'.at in
+      cast_exp' phrase env (Il.ProjE (e'', 0) $$ e'.at % t111') t111 t2
+    )
   | ConT ((t11, _), _), t2' ->
     (try
       let env' = local_env env in
@@ -1531,7 +1545,7 @@ and cast_exp' phrase env e' t1 t2 : Il.exp' =
       e'
     with Error _ ->  (* backtrack *)
       Debug.(log_in_at "el.cast_exp" e'.at
-        (fun _ -> fmt "%s <: %s  >>  (%s) <: (%s) = (%s) # backtrack 1" (el_typ t1) (el_typ t2)
+        (fun _ -> fmt "%s <: %s  >>  (%s) <: (%s) = (%s) # backtrack 2" (el_typ t1) (el_typ t2)
           (el_typ (expand_def env t1 $ t1.at)) (el_typ (expand_def env t2 $ t2.at))
           (el_typ (expand_nondef env t2))
         )
@@ -1562,7 +1576,7 @@ and cast_exp' phrase env e' t1 t2 : Il.exp' =
       e'
     with Error _ ->  (* backtrack *)
       Debug.(log_in_at "el.cast_exp" e'.at
-        (fun _ -> fmt "%s <: %s  >>  (%s) <: (%s) = (%s) # backtrack 2" (el_typ t1) (el_typ t2)
+        (fun _ -> fmt "%s <: %s  >>  (%s) <: (%s) = (%s) # backtrack 3" (el_typ t1) (el_typ t2)
           (el_typ (expand_def env t1 $ t1.at)) (el_typ (expand_def env t2 $ t2.at))
           (el_typ (expand_nondef env t2))
         )

spectec/src/frontend/eval.ml

@@ -750,6 +750,14 @@ and equiv_params env ps1 ps2 =
 
 (* Subtyping *)
 
+and sub_prems _env prems1 prems2 =
+  Debug.(log "el.sub_prems"
+    (fun _ -> fmt "%s <: %s" (nl_list el_prem prems1) (nl_list el_prem prems2))
+    Bool.to_string
+  ) @@ fun _ ->
+  let open Convert in
+  forall_nl_list (fun prem2 -> exists_nl_list (Eq.eq_prem prem2) prems1) prems2
+
 and sub_typ env t1 t2 =
   Debug.(log "el.sub_typ"
     (fun _ -> fmt "%s <: %s" (el_typ t1) (el_typ t2)) Bool.to_string
@@ -759,21 +767,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 && sub_prems env 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 && sub_prems env prems1 prems2
       | None -> false
     ) tcs1
-  | ConT ((t11, _prems1), _), ConT ((t21, _prems2), _) ->
-    sub_typ env t11 t21 (*&& Eq.eq_nl_list Eq.eq_prem prems1 prems2*)
+  | ConT ((t11, prems1), _), ConT ((t21, prems2), _) ->
+    sub_typ env t11 t21 && sub_prems env prems1 prems2
 (*
   | ConT ((t11, _), _), _ -> sub_typ env t11 t2
   | _, ConT ((t21, _), _) -> sub_typ env t1 t21

spectec/src/il/eval.ml

@@ -905,6 +905,9 @@ and equiv_params env ps1 ps2 =
 
 (* Subtyping *)
 
+and sub_prems _env prems1 prems2 =
+  List.for_all (fun prem2 -> List.exists (Eq.eq_prem prem2) prems1) prems2
+
 and sub_typ env t1 t2 =
   Debug.(log "il.sub_typ"
     (fun _ -> fmt "%s <: %s" (il_typ t1) (il_typ t2)) Bool.to_string
@@ -918,17 +921,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 && sub_prems 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 && sub_prems env prems1 prems2
         | None -> false
       ) tcs1
     | _, _ -> false