More syntax

Wasm-DSL · Mar 4, 2024 · bc69c3f · bc69c3f
1 parent 6e73ee3
commit bc69c3f
Show file tree

Hide file tree

Showing 19 changed files with 2,476 additions and 2,302 deletions.
diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst
diff --git a/spectec/spec/wasm-1.0/1-syntax.watsup b/spectec/spec/wasm-1.0/1-syntax.watsup
@@ -188,19 +188,25 @@ var bt : blocktype
 syntax instr/control hint(desc "control instruction") =
   | UNREACHABLE
   | NOP
-  | DROP
-  | SELECT (valtype*)?
   | BLOCK blocktype instr*
   | LOOP blocktype instr*
   | IF blocktype instr* ELSE instr*
   | BR labelidx
   | BR_IF labelidx
   | BR_TABLE labelidx* labelidx
+  | ...
+
+syntax instr/call hint(desc "call instruction") = ...
   | CALL funcidx
   | CALL_INDIRECT typeidx
   | RETURN
   | ...
 
+syntax instr/parametric hint(desc "parametric instruction") = ...
+  | DROP
+  | SELECT
+  | ...
+
 syntax instr/num hint(desc "numeric instruction") = ...
   | CONST valtype val_(valtype)      hint(show %.CONST %)
   | UNOP valtype unop_(valtype)      hint(show %.%)
@@ -221,11 +227,16 @@ syntax instr/global hint(desc "global instruction") = ...
   | GLOBAL.SET globalidx
   | ...
 
+syntax packsize hint(desc "pack size") = 8 | 16 | 32
+syntax ww hint(show w) = packsize
+
 syntax instr/memory hint(desc "memory instruction") = ...
+  | LOAD valtype (ww _ sx)? memop  hint(show %.LOAD % %)    hint(show %.LOAD#% % %)
+    -- (if valtype = inn /\ ww < $size(inn))?  ;; TODO: take size implicitly
+  | STORE valtype ww? memop        hint(show %.STORE % %)   hint(show %.STORE#% % %)
+    -- (if valtype = inn /\ ww < $size(inn))?  ;; TODO: take size implicitly
   | MEMORY.SIZE
   | MEMORY.GROW
-  | LOAD valtype (n _ sx)? memop  hint(show %.LOAD % %)  hint(show %.LOAD#% %)
-  | STORE valtype n? memop        hint(show %.STORE % %) hint(show %.STORE#% %)
 
 syntax expr hint(desc "expression") =
   instr*

diff --git a/spectec/spec/wasm-1.0/8-reduction.watsup b/spectec/spec/wasm-1.0/8-reduction.watsup
@@ -50,11 +50,11 @@ rule Step_pure/drop:
 
 
 rule Step_pure/select-true:
-  val_1 val_2 (CONST I32 c) (SELECT t*?)  ~>  val_1
+  val_1 val_2 (CONST I32 c) SELECT  ~>  val_1
   -- if c =/= 0
 
 rule Step_pure/select-false:
-  val_1 val_2 (CONST I32 c) (SELECT t*?)  ~>  val_2
+  val_1 val_2 (CONST I32 c) SELECT  ~>  val_2
   -- if c = 0
 
 

diff --git a/spectec/spec/wasm-1.0/A-binary.watsup b/spectec/spec/wasm-1.0/A-binary.watsup
@@ -382,7 +382,6 @@ grammar Binstr/numeric-cvt : instr = ...
   | 0xBD => CVTOP I64 REINTERPRET F64
   | 0xBE => CVTOP F32 REINTERPRET I32
   | 0xBF => CVTOP F64 REINTERPRET I64
-  | ...
 
 
 ;; Expressions

diff --git a/spectec/spec/wasm-2.0/1-syntax.watsup b/spectec/spec/wasm-2.0/1-syntax.watsup
@@ -181,6 +181,7 @@ var lim : limits
 var t : valtype
 var ft : functype
 var gt : globaltype
+var lt : lanetype
 var mt : memtype
 var nt : numtype
 var pt : packtype
@@ -219,6 +220,7 @@ def $zero(numtype) : num_(numtype)
 def $zero(inn) = 0
 def $zero(fnn) = $fzero($size(fnn))
 
+
 ;; Numeric operators
 
 syntax sx hint(desc "signedness") = U | S
@@ -336,21 +338,27 @@ syntax blocktype hint(desc "block type") =
 var bt : blocktype
 
 syntax instr/control hint(desc "control instruction") =
-  | UNREACHABLE
   | NOP
-  | DROP
-  | SELECT (valtype*)?
+  | UNREACHABLE
   | BLOCK blocktype instr*
   | LOOP blocktype instr*
   | IF blocktype instr* ELSE instr*
   | BR labelidx
   | BR_IF labelidx
   | BR_TABLE labelidx* labelidx
+  | ...
+
+syntax instr/call hint(desc "call instruction") = ...
   | CALL funcidx
   | CALL_INDIRECT tableidx typeidx
   | RETURN
   | ...
 
+syntax instr/parametric hint(desc "parametric instruction") = ...
+  | DROP
+  | SELECT (valtype*)?
+  | ...
+
 syntax instr/num hint(desc "numeric instruction") = ...
   | CONST numtype num_(numtype)      hint(show %.CONST %)
   | UNOP numtype unop_(numtype)      hint(show %.%)
@@ -418,23 +426,34 @@ syntax instr/table hint(desc "table instruction") = ...
   | TABLE.FILL tableidx
   | TABLE.COPY tableidx tableidx
   | TABLE.INIT tableidx elemidx
-  | ELEM.DROP elemidx
   | ...
 
+syntax instr/elem hint(desc "element instruction") = ...
+  | ELEM.DROP elemidx
+  | ...
+
+syntax packsize hint(desc "pack size") = 8 | 16 | 32 | 64
+syntax ww hint(show w) = packsize
 
 syntax instr/memory hint(desc "memory instruction") = ...
+  | LOAD numtype (ww _ sx)? memop  hint(show %.LOAD % %)    hint(show %.LOAD#% % %)
+    -- (if numtype = inn /\ ww < $size(inn))?  ;; TODO: take size implicitly
+  | STORE numtype ww? memop        hint(show %.STORE % %)   hint(show %.STORE#% % %)
+    -- (if numtype = inn /\ ww < $size(inn))?  ;; TODO: take size implicitly
+  | VLOAD vloadop? memop           hint(show V128.LOAD % %) hint(show V128.LOAD#% % %)
+  | VLOAD_LANE ww memop laneidx    hint(show V128.LOAD#%#_#LANE % % %)
+  | VSTORE memop                   hint(show V128.STORE % %)
+  | VSTORE_LANE ww memop laneidx   hint(show V128.STORE#%#_#LANE % % %)
   | MEMORY.SIZE
   | MEMORY.GROW
   | MEMORY.FILL
   | MEMORY.COPY
   | MEMORY.INIT dataidx
+  | ...
+
+syntax instr/data hint(desc "data instruction") = ...
   | DATA.DROP dataidx
-  | LOAD numtype (n _ sx)? memop  hint(show %.LOAD % %)  hint(show %.LOAD#% %)
-  | STORE numtype n? memop        hint(show %.STORE % %) hint(show %.STORE#% %)
-  | VLOAD vloadop? memop          hint(show V128.LOAD %) hint(show V128.LOAD#% %)
-  | VLOAD_LANE n memop laneidx    hint(show V128.LOAD#%#_#LANE % %)
-  | VSTORE memop                  hint(show V128.STORE %)
-  | VSTORE_LANE n memop laneidx   hint(show V128.STORE#%#_#LANE % %)
+
 
 syntax expr hint(desc "expression") =
   instr*

diff --git a/spectec/spec/wasm-2.0/A-binary.watsup b/spectec/spec/wasm-2.0/A-binary.watsup
@@ -736,7 +736,6 @@ grammar Binstr/vector-cvt : instr = ...
   | 0xFD 255:Bu32 => VCVTOP (F64 X 2) CONVERT LOW (I32 X 4) U
   | 0xFD 94:Bu32 => VCVTOP (F32 X 4) DEMOTE (F64 X 2) ZERO
   | 0xFD 95:Bu32 => VCVTOP (F64 X 2) PROMOTE LOW (F32 X 4)
-  | ...
 
 
 ;; Expressions

diff --git a/spectec/spec/wasm-3.0/1-syntax.watsup b/spectec/spec/wasm-3.0/1-syntax.watsup
@@ -232,7 +232,7 @@ var gt : globaltype
 var ht : heaptype
 ;; var it : instrtype  ;; defined in typing
 ;; kt : conttype       ;; future extension
-;; var lt : localtype  ;; defined in typing
+var lt : lanetype
 var mt : memtype
 var nt : numtype
 var pt : packtype
@@ -285,6 +285,7 @@ def $zero(numtype) : num_(numtype)
 def $zero(inn) = 0
 def $zero(fnn) = $fzero($size(fnn))
 
+
 ;; Numeric operators
 
 syntax sx hint(desc "signedness") = U | S
@@ -402,10 +403,8 @@ syntax blocktype hint(desc "block type") =
 var bt : blocktype
 
 syntax instr/control hint(desc "control instruction") =
-  | UNREACHABLE
   | NOP
-  | DROP
-  | SELECT (valtype*)?
+  | UNREACHABLE
   | BLOCK blocktype instr*
   | LOOP blocktype instr*
   | IF blocktype instr* ELSE instr*
@@ -416,6 +415,9 @@ syntax instr/control hint(desc "control instruction") =
   | BR_ON_NON_NULL labelidx
   | BR_ON_CAST labelidx reftype reftype
   | BR_ON_CAST_FAIL labelidx reftype reftype
+  | ...
+
+syntax instr/call hint(desc "call instruction") = ...
   | CALL funcidx
   | CALL_REF typeidx?
   | CALL_INDIRECT tableidx typeidx
@@ -425,6 +427,11 @@ syntax instr/control hint(desc "control instruction") =
   | RETURN_CALL_INDIRECT tableidx typeidx
   | ...
 
+syntax instr/parametric hint(desc "parametric instruction") = ...
+  | DROP
+  | SELECT (valtype*)?
+  | ...
+
 syntax instr/num hint(desc "numeric instruction") = ...
   | CONST numtype num_(numtype)      hint(show %.CONST %)
   | UNOP numtype unop_(numtype)      hint(show %.%)
@@ -469,24 +476,33 @@ syntax instr/vec hint(desc "vector instruction") = ...
 
 syntax instr/ref hint(desc "reference instruction") = ...
   | REF.NULL heaptype
-  | REF.I31
-  | REF.FUNC funcidx
   | REF.IS_NULL
   | REF.AS_NON_NULL
   | REF.EQ
   | REF.TEST reftype
   | REF.CAST reftype
   | ...
 
-syntax instr/heap hint(desc "heap instruction") = ...
+syntax instr/func hint(desc "function reference instruction") = ...
+  | REF.FUNC funcidx
+  | ...
+
+syntax instr/i31 hint(desc "scalar reference instruction") = ...
+  | REF.I31
   | I31.GET sx                      hint(show I31.GET#_#%)
+  | ...
+
+syntax instr/struct hint(desc "structure reference instruction") = ...
   | STRUCT.NEW typeidx
   | STRUCT.NEW_DEFAULT typeidx
   | STRUCT.GET sx? typeidx u32      hint(show STRUCT.GET#_#% % %)
   | STRUCT.SET typeidx u32
+  | ...
+
+syntax instr/array hint(desc "array reference instruction") = ...
   | ARRAY.NEW typeidx
   | ARRAY.NEW_DEFAULT typeidx
-  | ARRAY.NEW_FIXED typeidx nat
+  | ARRAY.NEW_FIXED typeidx u32
   | ARRAY.NEW_DATA typeidx dataidx
   | ARRAY.NEW_ELEM typeidx elemidx
   | ARRAY.GET sx? typeidx           hint(show ARRAY.GET#_#% %)
@@ -496,6 +512,9 @@ syntax instr/heap hint(desc "heap instruction") = ...
   | ARRAY.COPY typeidx typeidx
   | ARRAY.INIT_DATA typeidx dataidx
   | ARRAY.INIT_ELEM typeidx elemidx
+  | ...
+
+syntax instr/extern hint(desc "external reference instruction") = ...
   | EXTERN.CONVERT_ANY
   | ANY.CONVERT_EXTERN
   | ...
@@ -519,23 +538,34 @@ syntax instr/table hint(desc "table instruction") = ...
   | TABLE.FILL tableidx
   | TABLE.COPY tableidx tableidx
   | TABLE.INIT tableidx elemidx
+  | ...
+
+syntax instr/elem hint(desc "element instruction") = ...
   | ELEM.DROP elemidx
   | ...
 
+syntax packsize hint(desc "pack size") = 8 | 16 | 32 | 64
+syntax ww hint(show w) = packsize
 
 syntax instr/memory hint(desc "memory instruction") = ...
+  | LOAD numtype (ww _ sx)? memidx memop  hint(show %.LOAD % %)    hint(show %.LOAD#% % %)
+    -- (if numtype = inn /\ ww < $size(inn))?  ;; TODO: take size implicitly
+  | STORE numtype ww? memidx memop        hint(show %.STORE % %)   hint(show %.STORE#% % %)
+    -- (if numtype = inn /\ ww < $size(inn))?  ;; TODO: take size implicitly
+  | VLOAD vloadop? memidx memop           hint(show V128.LOAD % %) hint(show V128.LOAD#% % %)
+  | VLOAD_LANE ww memidx memop laneidx    hint(show V128.LOAD#%#_#LANE % % %)
+  | VSTORE memidx memop                   hint(show V128.STORE % %)
+  | VSTORE_LANE ww memidx memop laneidx   hint(show V128.STORE#%#_#LANE % % %)
   | MEMORY.SIZE memidx
   | MEMORY.GROW memidx
   | MEMORY.FILL memidx
   | MEMORY.COPY memidx memidx
   | MEMORY.INIT memidx dataidx
+  | ...
+
+syntax instr/data hint(desc "data instruction") = ...
   | DATA.DROP dataidx
-  | LOAD numtype (n _ sx)? memidx memop  hint(show %.LOAD % %)    hint(show %.LOAD#% % %)
-  | STORE numtype n? memidx memop        hint(show %.STORE % %)   hint(show %.STORE#% % %)
-  | VLOAD vloadop? memidx memop          hint(show V128.LOAD % %) hint(show V128.LOAD#% % %)
-  | VLOAD_LANE n memidx memop laneidx    hint(show V128.LOAD#%#_#LANE % % %)
-  | VSTORE memidx memop                  hint(show V128.STORE % %)
-  | VSTORE_LANE n memidx memop laneidx   hint(show V128.STORE#%#_#LANE % % %)
+
 
 syntax expr hint(desc "expression") =
   instr*

diff --git a/spectec/spec/wasm-3.0/6-typing.watsup b/spectec/spec/wasm-3.0/6-typing.watsup
@@ -19,14 +19,14 @@ syntax context hint(desc "context") =
     LOCAL localtype*, LABEL resulttype*, RETURN resulttype? }
 
 var C : context
-var lt : localtype
+var lct : localtype  hint(show lt)
 var it : instrtype
 
 
 def $with_locals(context, localidx*, localtype*) : context  hint(show %[.LOCAL[%]=%])
 
 def $with_locals(C, eps, eps) = C
-def $with_locals(C, x_1 x*, lt_1 lt*) = $with_locals(C[.LOCAL[x_1] = lt_1], x*, lt*)
+def $with_locals(C, x_1 x*, lct_1 lct*) = $with_locals(C[.LOCAL[x_1] = lct_1], x*, lct*)
 
 
 def $clostype(context, deftype) : deftype  hint(show $clos_%(%))
@@ -101,7 +101,7 @@ rule Instrtype_ok:
   C |- t_1* -> x* t_2* : OK
   -- Resulttype_ok: C |- t_1* : OK
   -- Resulttype_ok: C |- t_2* : OK
-  -- if (C.LOCAL[x] = lt)*
+  -- if (C.LOCAL[x] = lct)*
 
 
 ;; Type definitions
@@ -500,7 +500,9 @@ rule Externtype_sub/mem:
 ;; Instructions
 ;;
 
-relation Instr_ok: context |- instr : functype      hint(show "T")
+syntax finstrtype = resulttype -> resulttype  ;; TODO: HACK, shouldn't be needed
+
+relation Instr_ok: context |- instr : finstrtype    hint(show "T")
 relation Instrf_ok: context |- instr : instrtype    hint(show "T")
 relation Instrs_ok: context |- instr* : instrtype   hint(show "T-instr*")
 relation Expr_ok: context |- expr : resulttype      hint(show "T-expr")
@@ -1138,8 +1140,8 @@ rule Local_ok/unset:
 rule Func_ok:
   C |- FUNC x local* expr : C.TYPE[x]
   -- Expand: C.TYPE[x] ~~ FUNC (t_1* -> t_2*)
-  -- (Local_ok: C |- local : lt)*
-  -- Expr_ok: C, LOCAL (SET t_1)* lt*, LABEL (t_2*), RETURN (t_2*) |- expr : t_2*
+  -- (Local_ok: C |- local : lct)*
+  -- Expr_ok: C, LOCAL (SET t_1)* lct*, LABEL (t_2*), RETURN (t_2*) |- expr : t_2*
 
 rule Global_ok:
   C |- GLOBAL gt expr : gt

diff --git a/spectec/spec/wasm-3.0/A-binary.watsup b/spectec/spec/wasm-3.0/A-binary.watsup
@@ -828,7 +828,6 @@ grammar Binstr/vector-cvt : instr = ...
   | 0xFD 255:Bu32 => VCVTOP (F64 X 2) CONVERT LOW (I32 X 4) U
   | 0xFD 94:Bu32 => VCVTOP (F32 X 4) DEMOTE (F64 X 2) ZERO
   | 0xFD 95:Bu32 => VCVTOP (F64 X 2) PROMOTE LOW (F32 X 4)
-  | ...
 
 
 ;; Expressions

diff --git a/spectec/src/backend-interpreter/construct.ml b/spectec/src/backend-interpreter/construct.ml
@@ -768,7 +768,8 @@ and al_to_instr': value -> Ast.instr' = function
   | CaseV ("VREPLACE_LANE", vop) -> VecReplace (al_to_vreplaceop vop)
   | CaseV ("REF.IS_NULL", []) -> RefIsNull
   | CaseV ("REF.FUNC", [ idx ]) -> RefFunc (al_to_idx idx)
-  | CaseV ("SELECT", [ vtl_opt ]) -> Select (al_to_opt (al_to_list al_to_val_type) vtl_opt)
+  | CaseV ("SELECT", []) when !version = 1 -> Select None
+  | CaseV ("SELECT", [ vtl_opt ]) when !version <> 1 -> Select (al_to_opt (al_to_list al_to_val_type) vtl_opt)
   | CaseV ("LOCAL.GET", [ idx ]) -> LocalGet (al_to_idx idx)
   | CaseV ("LOCAL.SET", [ idx ]) -> LocalSet (al_to_idx idx)
   | CaseV ("LOCAL.TEE", [ idx ]) -> LocalTee (al_to_idx idx)
@@ -1722,6 +1723,7 @@ let rec al_of_instr instr =
   | VecReplace vop -> CaseV ("VREPLACE_LANE", al_of_vreplaceop vop)
   | RefIsNull -> nullary "REF.IS_NULL"
   | RefFunc idx -> CaseV ("REF.FUNC", [ al_of_idx idx ])
+  | Select vtl_opt when !version = 1 -> assert (vtl_opt = None); nullary "SELECT"
   | Select vtl_opt -> CaseV ("SELECT", [ al_of_opt (al_of_list al_of_val_type) vtl_opt ])
   | LocalGet idx -> CaseV ("LOCAL.GET", [ al_of_idx idx ])
   | LocalSet idx -> CaseV ("LOCAL.SET", [ al_of_idx idx ])

diff --git a/spectec/src/backend-latex/render.ml b/spectec/src/backend-latex/render.ml
@@ -680,7 +680,7 @@ and render_exp env e =
     (* Hack for printing t.LOADn_sx *)
     let e2' = as_paren_exp (fuse_exp e2 true) in
     "{" ^ render_exp env e1 ^ "}" ^ "{" ^ render_exp env e2' ^ "}"
-  | HoleE `None -> "{}"
+  | HoleE `None -> ""
   | HoleE _ -> error e.at "misplaced hole"
 
 and render_exps sep env es =