Merge pull request #82 from Wasm-DSL/mixcase

Unify syntax of Case and Notation
Wasm-DSL · Mar 1, 2024 · 49e0819 · 49e0819
2 parents c27aa4b + e6bfb2b
commit 49e0819
Show file tree

Hide file tree

Showing 15 changed files with 2,915 additions and 2,805 deletions.
diff --git a/spectec/spec/wasm-1.0/1-syntax.watsup b/spectec/spec/wasm-1.0/1-syntax.watsup
@@ -104,8 +104,8 @@ var l : labelidx
 syntax valtype hint(desc "number type") =
   | I32 | I64 | F32 | F64
 
-syntax inn hint(show I#n) = | I32 | I64
-syntax fnn hint(show F#n) = | F32 | F64
+syntax inn hint(show I#n) = I32 | I64
+syntax fnn hint(show F#n) = F32 | F64
 
 var t : valtype
 
@@ -146,11 +146,11 @@ syntax val_(fnn) = fN($size(fnn))
 
 ;; Operators
 
-syntax sx hint(desc "signedness") = | U | S
+syntax sx hint(desc "signedness") = U | S
 
 syntax unop_(valtype)
-syntax unop_(inn) = | CLZ | CTZ | POPCNT
-syntax unop_(fnn) = | ABS | NEG | SQRT | CEIL | FLOOR | TRUNC | NEAREST
+syntax unop_(inn) = CLZ | CTZ | POPCNT
+syntax unop_(fnn) = ABS | NEG | SQRT | CEIL | FLOOR | TRUNC | NEAREST
 
 syntax binop_(valtype)
 syntax binop_(inn) =
@@ -160,7 +160,7 @@ syntax binop_(fnn) =
   | ADD | SUB | MUL | DIV | MIN | MAX | COPYSIGN
 
 syntax testop_(valtype)
-syntax testop_(inn) = | EQZ
+syntax testop_(inn) = EQZ
 ;; syntax testop_(fnn) = |      ;; uninhabited
 
 syntax relop_(valtype)
@@ -171,7 +171,7 @@ syntax relop_(inn) =
 syntax relop_(fnn) =
   | EQ | NE | LT | GT | LE | GE
 
-syntax cvtop = | CONVERT | REINTERPRET
+syntax cvtop = CONVERT | REINTERPRET
 
 
 syntax memop hint(desc "memory operator") = {ALIGN u32, OFFSET u32}

diff --git a/spectec/spec/wasm-1.0/A-binary.watsup b/spectec/spec/wasm-1.0/A-binary.watsup
@@ -15,7 +15,7 @@ grammar Bvec(grammar BX : el) : el* =
 
 ;; Numbers
 
-grammar Bbyte : byte = | b:0x00 | ... | b:0xFF => b
+grammar Bbyte : byte = b:0x00 | ... | b:0xFF => b
 
 grammar BuN(N) : uN(N) hint(show Bu#%) =
   | n:Bbyte                 => n                       -- if $(n < 2^7 /\ n < 2^N)
@@ -34,11 +34,11 @@ grammar BfN(N) : fN(N) hint(show Bf#%) =
   | b*:Bbyte^(N/8)  => $invfbytes(N, b*)
 
 
-grammar Bu32 : u32 = | n:BuN(32) => n
-grammar Bu64 : u64 = | n:BuN(64) => n
+grammar Bu32 : u32 = n:BuN(32) => n
+grammar Bu64 : u64 = n:BuN(64) => n
 
-grammar Bf32 : f32 = | p:BfN(32) => p
-grammar Bf64 : f64 = | p:BfN(64) => p
+grammar Bf32 : f32 = p:BfN(32) => p
+grammar Bf64 : f64 = p:BfN(64) => p
 
 
 ;; Names
@@ -58,13 +58,13 @@ grammar Bname : name =
 
 ;; Indices
 
-grammar Btypeidx : typeidx = | x:Bu32 => x
-grammar Bfuncidx : funcidx = | x:Bu32 => x
-grammar Bglobalidx : globalidx = | x:Bu32 => x
-grammar Btableidx : tableidx = | x:Bu32 => x
-grammar Bmemidx : memidx = | x:Bu32 => x
-grammar Blocalidx : localidx = | x:Bu32 => x
-grammar Blabelidx : labelidx = | x:Bu32 => x
+grammar Btypeidx : typeidx = x:Bu32 => x
+grammar Bfuncidx : funcidx = x:Bu32 => x
+grammar Bglobalidx : globalidx = x:Bu32 => x
+grammar Btableidx : tableidx = x:Bu32 => x
+grammar Bmemidx : memidx = x:Bu32 => x
+grammar Blocalidx : localidx = x:Bu32 => x
+grammar Blabelidx : labelidx = x:Bu32 => x
 
 grammar Bexternidx : externidx =
   | 0x00 x:Bfuncidx => FUNC x

diff --git a/spectec/spec/wasm-2.0/1-syntax.watsup b/spectec/spec/wasm-2.0/1-syntax.watsup
@@ -132,9 +132,9 @@ syntax reftype hint(desc "reference type") =
 syntax valtype hint(desc "value type") =
   | numtype | vectype | reftype | BOT
 
-syntax inn hint(show I#n) = | I32 | I64
-syntax fnn hint(show F#n) = | F32 | F64
-syntax vnn hint(show V#n) = | V128
+syntax inn hint(show I#n) = I32 | I64
+syntax fnn hint(show F#n) = F32 | F64
+syntax vnn hint(show V#n) = V128
 
 
 syntax resulttype hint(desc "result type") =
@@ -143,12 +143,12 @@ syntax resulttype hint(desc "result type") =
 
 ;; Packed types
 
-syntax packtype hint(desc "packed type") = | I8 | I16
-syntax lanetype hint(desc "lane type") = | numtype | packtype
+syntax packtype hint(desc "packed type") = I8 | I16
+syntax lanetype hint(desc "lane type") = numtype | packtype
 
-syntax pnn hint(show I#n) = | I8 | I16
-syntax lnn hint(show I#n) = | numtype | pnn
-syntax imm hint(show I#n) = | inn | pnn
+syntax pnn hint(show I#n) = I8 | I16
+syntax lnn hint(show I#n) = numtype | pnn
+syntax imm hint(show I#n) = inn | pnn
 
 
 ;; External types
@@ -221,11 +221,11 @@ def $zero(fnn) = $fzero($size(fnn))
 
 ;; Numeric operators
 
-syntax sx hint(desc "signedness") = | U | S
+syntax sx hint(desc "signedness") = U | S
 
 syntax unop_(numtype)
-syntax unop_(inn) = | CLZ | CTZ | POPCNT | EXTEND n
-syntax unop_(fnn) = | ABS | NEG | SQRT | CEIL | FLOOR | TRUNC | NEAREST
+syntax unop_(inn) = CLZ | CTZ | POPCNT | EXTEND n
+syntax unop_(fnn) = ABS | NEG | SQRT | CEIL | FLOOR | TRUNC | NEAREST
 
 syntax binop_(numtype)
 syntax binop_(inn) =
@@ -235,7 +235,7 @@ syntax binop_(fnn) =
   | ADD | SUB | MUL | DIV | MIN | MAX | COPYSIGN
 
 syntax testop_(numtype)
-syntax testop_(inn) = | EQZ
+syntax testop_(inn) = EQZ
 ;; syntax testop_(fnn) = |      ;; uninhabited
 
 syntax relop_(numtype)
@@ -246,7 +246,7 @@ syntax relop_(inn) =
 syntax relop_(fnn) =
   | EQ | NE | LT | GT | LE | GE
 
-syntax cvtop = | CONVERT | CONVERT_SAT | REINTERPRET
+syntax cvtop = CONVERT | CONVERT_SAT | REINTERPRET
 
 
 ;; Vector operators
@@ -260,14 +260,14 @@ syntax pshape hint(desc "shape") = pnn X dim      ;; TODO: hint(show %#X#%)
 def $dim(shape) : dim
 def $shsize(shape) : nat  hint(show |%|)
 
-syntax vvunop = | NOT
-syntax vvbinop = | AND | ANDNOT | OR | XOR
-syntax vvternop = | BITSELECT
-syntax vvtestop = | ANY_TRUE
+syntax vvunop = NOT
+syntax vvbinop = AND | ANDNOT | OR | XOR
+syntax vvternop = BITSELECT
+syntax vvtestop = ANY_TRUE
 
 syntax vunop_(shape)
-syntax vunop_(imm X N) = | ABS | NEG | POPCNT -- if imm = I8
-syntax vunop_(fnn X N) = | ABS | NEG | SQRT | CEIL | FLOOR | TRUNC | NEAREST
+syntax vunop_(imm X N) = ABS | NEG | POPCNT -- if imm = I8
+syntax vunop_(fnn X N) = ABS | NEG | SQRT | CEIL | FLOOR | TRUNC | NEAREST
 
 syntax vbinop_(shape)
 syntax vbinop_(imm X N) =
@@ -280,17 +280,17 @@ syntax vbinop_(imm X N) =
   | Q15MULR_SAT_S                          -- if $lsize(imm) = 16
   | MIN sx hint(show MIN#_#sx)             -- if $lsize(imm) <= 32
   | MAX sx hint(show MAX#_#sx)             -- if $lsize(imm) <= 32
-syntax vbinop_(fnn X N) = | ADD | SUB | MUL | DIV | MIN | MAX | PMIN | PMAX
+syntax vbinop_(fnn X N) = ADD | SUB | MUL | DIV | MIN | MAX | PMIN | PMAX
 
 syntax vtestop_(shape)
-syntax vtestop_(imm X N) = | ALL_TRUE
+syntax vtestop_(imm X N) = ALL_TRUE
 ;; syntax vtestop_(fnn X N) = |           ;; uninhabited
 
 syntax vrelop_(shape)
-syntax vrelop_(imm X N) = | EQ | NE | LT sx | GT sx | LE sx | GE sx
-syntax vrelop_(fnn X N) = | EQ | NE | LT | GT | LE | GE
+syntax vrelop_(imm X N) = EQ | NE | LT sx | GT sx | LE sx | GE sx
+syntax vrelop_(fnn X N) = EQ | NE | LT | GT | LE | GE
 
-syntax vcvtop = | EXTEND | TRUNC_SAT | CONVERT | DEMOTE | PROMOTE
+syntax vcvtop = EXTEND | TRUNC_SAT | CONVERT | DEMOTE | PROMOTE
 ;; TODO: analogous to cvtop, this could just universally be CONVERT.
 ;; Otherwise, it needs to be indexed by 2 shapes.
 ;; TODO: the following syntactic constraints apply:
@@ -302,7 +302,7 @@ syntax vcvtop = | EXTEND | TRUNC_SAT | CONVERT | DEMOTE | PROMOTE
 ;; fNxM <- fN'xM'  N > N'  PROMOTE LOW
 
 syntax vshiftop_(ishape)
-syntax vshiftop_(imm X N) = | SHL | SHR sx
+syntax vshiftop_(imm X N) = SHL | SHR sx
 
 syntax vextunop_(ishape_1, ishape_2)  hint(show vextunop_((%,%)))
 syntax vextunop_(imm_1 X N_1, imm_2 X N_2) =
@@ -361,7 +361,7 @@ syntax instr/num hint(desc "numeric instruction") = ...
   | EXTEND numtype N                 hint(show %.EXTEND#%#_S)
   | ...
 
-syntax half hint(desc "lane part") = | LOW | HIGH
+syntax half hint(desc "lane part") = LOW | HIGH
 syntax zero = ZERO?
 
 syntax instr/vec hint(desc "vector instruction") = ...
@@ -449,8 +449,8 @@ var e : expr
 ;; Modules
 ;;
 
-syntax elemmode = | ACTIVE tableidx expr | PASSIVE | DECLARE
-syntax datamode = | ACTIVE memidx expr | PASSIVE
+syntax elemmode = ACTIVE tableidx expr | PASSIVE | DECLARE
+syntax datamode = ACTIVE memidx expr | PASSIVE
 
 syntax type hint(desc "type") =
   TYPE functype

diff --git a/spectec/spec/wasm-2.0/A-binary.watsup b/spectec/spec/wasm-2.0/A-binary.watsup
@@ -15,7 +15,7 @@ grammar Bvec(grammar BX : el) : el* =
 
 ;; Numbers
 
-grammar Bbyte : byte = | b:0x00 | ... | b:0xFF => b
+grammar Bbyte : byte = b:0x00 | ... | b:0xFF => b
 
 grammar BuN(N) : uN(N) hint(show Bu#%) =
   | n:Bbyte                 => n                       -- if $(n < 2^7 /\ n < 2^N)
@@ -34,12 +34,12 @@ grammar BfN(N) : fN(N) hint(show Bf#%) =
   | b*:Bbyte^(N/8)  => $invfbytes(N, b*)
 
 
-grammar Bu32 : u32 = | n:BuN(32) => n
-grammar Bu64 : u64 = | n:BuN(64) => n
-grammar Bs33 : s33 = | i:BsN(33) => i
+grammar Bu32 : u32 = n:BuN(32) => n
+grammar Bu64 : u64 = n:BuN(64) => n
+grammar Bs33 : s33 = i:BsN(33) => i
 
-grammar Bf32 : f32 = | p:BfN(32) => p
-grammar Bf64 : f64 = | p:BfN(64) => p
+grammar Bf32 : f32 = p:BfN(32) => p
+grammar Bf64 : f64 = p:BfN(64) => p
 
 
 ;; Names
@@ -59,15 +59,15 @@ grammar Bname : name =
 
 ;; Indices
 
-grammar Btypeidx : typeidx = | x:Bu32 => x
-grammar Bfuncidx : funcidx = | x:Bu32 => x
-grammar Bglobalidx : globalidx = | x:Bu32 => x
-grammar Btableidx : tableidx = | x:Bu32 => x
-grammar Bmemidx : memidx = | x:Bu32 => x
-grammar Belemidx : elemidx = | x:Bu32 => x
-grammar Bdataidx : dataidx = | x:Bu32 => x
-grammar Blocalidx : localidx = | x:Bu32 => x
-grammar Blabelidx : labelidx = | x:Bu32 => x
+grammar Btypeidx : typeidx = x:Bu32 => x
+grammar Bfuncidx : funcidx = x:Bu32 => x
+grammar Bglobalidx : globalidx = x:Bu32 => x
+grammar Btableidx : tableidx = x:Bu32 => x
+grammar Bmemidx : memidx = x:Bu32 => x
+grammar Belemidx : elemidx = x:Bu32 => x
+grammar Bdataidx : dataidx = x:Bu32 => x
+grammar Blocalidx : localidx = x:Bu32 => x
+grammar Blabelidx : labelidx = x:Bu32 => x
 
 grammar Bexternidx : externidx =
   | 0x00 x:Bfuncidx => FUNC x