Some renaming

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

@@ -127,8 +127,8 @@ syntax resulttype hint(desc "result type") =
 
 ;; Packed types
 
-syntax packedtype hint(des "packed type") = | I8 | I16
-syntax lanetype hint(desc "lane type") = | numtype | packedtype
+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
@@ -167,7 +167,7 @@ var ft : functype
 var gt : globaltype
 var mt : memtype
 var nt : numtype
-var pt : packedtype
+var pt : packtype
 var rt : reftype
 var tt : tabletype
 var vt : vectype
@@ -181,20 +181,20 @@ var xt : externtype
 ;; Constants
 
 def $size(valtype) : nat      hint(partial) hint(show |%|)
-def $psize(packedtype) : nat  hint(show |%|)
+def $psize(packtype) : nat    hint(show |%|)
 def $lsize(lanetype) : nat    hint(show |%|)
 def $lanetype(shape) : lanetype
 
 syntax num_(numtype)
 syntax num_(inn) = iN($size(inn))
 syntax num_(fnn) = fN($size(fnn))
 
-syntax pnum_(pnn) = iN($psize(pnn))
+syntax pack_(pnn) = iN($psize(pnn))
 
-syntax lnum_(lanetype)
-syntax lnum_(numtype) = num_(numtype)
-syntax lnum_(packedtype) = pnum_(packedtype)
-syntax lnum_(imm) = iN($lsize(imm))  ;; HACK
+syntax lane_(lanetype)
+syntax lane_(numtype) = num_(numtype)
+syntax lane_(packtype) = pack_(packtype)
+syntax lane_(imm) = iN($lsize(imm))  ;; HACK
 
 syntax vec_(vnn) = vN($size(vnn))
 

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

@@ -18,7 +18,7 @@ def $concat_bytes((b*) (b'*)*) = b* $concat_bytes((b'*)*)
 ;; def |I n| = |F n| = |V n| = n        ;; ????
 
 ;;def $size(valtype) : nat      hint(partial) hint(show |%|)
-;;def $psize(packedtype) : nat  hint(show |%|)
+;;def $psize(packtype) : nat    hint(show |%|)
 ;;def $lsize(lanetype) : nat    hint(show |%|)
 
 def $size(I32) = 32
@@ -31,14 +31,14 @@ def $psize(I8) = 8
 def $psize(I16) = 16
 
 def $lsize(numtype) = $size(numtype)
-def $lsize(packedtype) = $psize(packedtype)
+def $lsize(packtype) = $psize(packtype)
 
 
 ;; Unpacking
 
 def $unpack(lanetype) : numtype
 def $unpack(numtype) = numtype
-def $unpack(packedtype) = I32
+def $unpack(packtype) = I32
 
 
 ;; Shapes

spectec/spec/wasm-2.0/3-numerics.watsup

@@ -58,23 +58,23 @@ def $narrow(M, N, sx, iN(M)) : iN(N)    hint(show $narrow_((%,%))^(%)#(%))
 
 ;; Packed values
 
-def $packnum(lanetype, num_($unpack(lanetype))) : lnum_(lanetype)
+def $packnum(lanetype, num_($unpack(lanetype))) : lane_(lanetype)
     hint(show $pack_(%,%))
 def $packnum(numtype, c) = c
-def $packnum(packedtype, c) = $wrap($size($unpack(packedtype)), $psize(packedtype), c)
+def $packnum(packtype, c) = $wrap($size($unpack(packtype)), $psize(packtype), c)
 
-def $unpacknum(lanetype, lnum_(lanetype)) : num_($unpack(lanetype))
+def $unpacknum(lanetype, lane_(lanetype)) : num_($unpack(lanetype))
     hint(show $unpack_(%,%))
 def $unpacknum(numtype, c) = c
-def $unpacknum(packedtype, c) = $ext($psize(packedtype), $size($unpack(packedtype)), U, c)
+def $unpacknum(packtype, c) = $ext($psize(packtype), $size($unpack(packtype)), U, c)
 
 
 ;; Vectors
 
-def $lanes_(shape, vec_(V128)) : lnum_($lanetype(shape))*
+def $lanes_(shape, vec_(V128)) : lane_($lanetype(shape))*
     hint(show $lanes_(%,%))
 
-def $invlanes_(shape, lnum_($lanetype(shape))*) : vec_(V128)
+def $invlanes_(shape, lane_($lanetype(shape))*) : vec_(V128)
     hint(show $lanes^(-1)#_%#(%,%))
 def $invlanes_(sh, c*) = vc  -- if c* = $lanes_(sh, vc)
 
@@ -98,7 +98,7 @@ def $vbinop(shape, vbinop_(shape), vec_(V128), vec_(V128)) : vec_(V128)*
 def $vrelop(shape, vrelop_(shape), vec_(V128), vec_(V128)) : vec_(V128)
     hint(show %2#_%1#(%3, %4))
 
-def $vcvtop(shape_1, shape_2, vcvtop, sx?, lnum_($lanetype(shape_1))) : lnum_($lanetype(shape_2))
+def $vcvtop(shape_1, shape_2, vcvtop, sx?, lane_($lanetype(shape_1))) : lane_($lanetype(shape_2))
     hint(show %3#$_((%1,%2))^(%5)#((%6)))
 
 def $vextunop(ishape_1, ishape_2, vextunop_(ishape_1, ishape_2), sx, vec_(V128)) : vec_(V128)
@@ -107,5 +107,5 @@ def $vextbinop(ishape_1, ishape_2, vextbinop_(ishape_1, ishape_2), sx, vec_(V128
     hint(show %3#$_((%1,%2))^(%5)#((%6,%7)))
 
 ;; TODO: refactor for consistency?
-def $vishiftop(ishape, vshiftop_(ishape), lnum_($lanetype(ishape)), u32) : lnum_($lanetype(ishape))
+def $vishiftop(ishape, vshiftop_(ishape), lane_($lanetype(ishape)), u32) : lane_($lanetype(ishape))
     hint(show %2#_%1#(%3, %4))

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

@@ -143,9 +143,9 @@ syntax resulttype hint(desc "result type") =
 
 ;; Packed types
 
-syntax packedtype hint(des "packed type") = | I8 | I16
-syntax lanetype hint(desc "lane type") = | numtype | packedtype
-syntax storagetype hint(desc "storage type") = | valtype | packedtype
+syntax packtype hint(desc "packed type") = | I8 | I16
+syntax lanetype hint(desc "lane type") = | numtype | packtype
+syntax storagetype hint(desc "storage type") = | valtype | packtype
 
 syntax pnn hint(show I#n) = | I8 | I16
 syntax lnn hint(show I#n) = | numtype | pnn
@@ -224,7 +224,7 @@ var ht : heaptype
 ;; var lt : localtype  ;; defined in typing
 var mt : memtype
 var nt : numtype
-var pt : packedtype
+var pt : packtype
 var qt : rectype       ;; TODO: better choice?
 var rt : reftype
 var st : subtype
@@ -242,7 +242,7 @@ var zt : storagetype
 ;; Constants
 
 def $size(valtype) : nat       hint(partial) hint(show |%|)
-def $psize(packedtype) : nat   hint(show |%|)
+def $psize(packtype) : nat   hint(show |%|)
 def $lsize(lanetype) : nat     hint(show |%|)
 def $zsize(storagetype) : nat  hint(show |%|)
 def $lanetype(shape) : lanetype
@@ -251,19 +251,19 @@ syntax num_(numtype)
 syntax num_(inn) = iN($size(inn))
 syntax num_(fnn) = fN($size(fnn))
 
-syntax pnum_(pnn) = iN($psize(pnn))
+syntax pack_(pnn) = iN($psize(pnn))
 
-syntax lnum_(lanetype)
-syntax lnum_(numtype) = num_(numtype)
-syntax lnum_(packedtype) = pnum_(packedtype)
-syntax lnum_(imm) = iN($lsize(imm))  ;; HACK
+syntax lane_(lanetype)
+syntax lane_(numtype) = num_(numtype)
+syntax lane_(packtype) = pack_(packtype)
+syntax lane_(imm) = iN($lsize(imm))  ;; HACK
 
 syntax vec_(vnn) = vN($size(vnn))
 
 syntax zval_(storagetype)
 syntax zval_(numtype) = num_(numtype)
 syntax zval_(vectype) = vec_(vectype)
-syntax zval_(packedtype) = pnum_(packedtype)
+syntax zval_(packtype) = pack_(packtype)
 
 
 ;; Numeric operators

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

@@ -46,7 +46,7 @@ def $free_dataidx_funcs(func func'*) = $free_dataidx_func(func) $free_dataidx_fu
 ;; def |I n| = |F n| = |V n| = n        ;; ????
 
 ;;def $size(valtype) : nat       hint(partial) hint(show |%|)
-;;def $psize(packedtype) : nat   hint(show |%|)
+;;def $psize(packtype) : nat     hint(show |%|)
 ;;def $lsize(lanetype) : nat     hint(show |%|)
 ;;def $zsize(storagetype) : nat  hint(show |%|)
 
@@ -60,32 +60,32 @@ def $psize(I8) = 8
 def $psize(I16) = 16
 
 def $lsize(numtype) = $size(numtype)
-def $lsize(packedtype) = $psize(packedtype)
+def $lsize(packtype) = $psize(packtype)
 
 def $zsize(valtype) = $size(valtype)
-def $zsize(packedtype) = $psize(packedtype)
+def $zsize(packtype) = $psize(packtype)
 
 
 ;; Unpacking
 
 def $lunpack(lanetype) : numtype  hint(show $unpack(%))
 def $lunpack(numtype) = numtype
-def $lunpack(packedtype) = I32
+def $lunpack(packtype) = I32
 
 def $unpack(storagetype) : valtype  hint(show $unpack(%))
 def $unpack(valtype) = valtype
-def $unpack(packedtype) = I32
+def $unpack(packtype) = I32
 
 def $nunpack(storagetype) : numtype  hint(show $unpack(%)) hint(partial)
 def $nunpack(numtype) = numtype
-def $nunpack(packedtype) = I32
+def $nunpack(packtype) = I32
 
 def $vunpack(storagetype) : vectype  hint(show $unpack(%)) hint(partial)
 def $vunpack(vectype) = vectype
 
 def $sxfield(storagetype) : sx?  hint(show $sx(%))
 def $sxfield(valtype) = eps
-def $sxfield(packedtype) = S
+def $sxfield(packtype) = S
 
 
 ;; Shapes
@@ -127,7 +127,7 @@ def $subst_heaptype(heaptype, typevar*, heaptype*) : heaptype          hint(show
 def $subst_reftype(reftype, typevar*, heaptype*) : reftype             hint(show %#`[%:=%])
 def $subst_valtype(valtype, typevar*, heaptype*) : valtype             hint(show %#`[%:=%])
 
-def $subst_packedtype(packedtype, typevar*, heaptype*) : packedtype    hint(show %#`[%:=%])
+def $subst_packtype(packtype, typevar*, heaptype*) : packtype          hint(show %#`[%:=%])
 def $subst_storagetype(storagetype, typevar*, heaptype*) : storagetype hint(show %#`[%:=%])
 def $subst_fieldtype(fieldtype, typevar*, heaptype*) : fieldtype       hint(show %#`[%:=%])
 
@@ -162,10 +162,10 @@ def $subst_valtype(vt, xx*, ht*) = $subst_vectype(vt, xx*, ht*)
 def $subst_valtype(rt, xx*, ht*) = $subst_reftype(rt, xx*, ht*)
 def $subst_valtype(BOT, xx*, ht*) = BOT
 
-def $subst_packedtype(pt, xx*, ht*) = pt
+def $subst_packtype(pt, xx*, ht*) = pt
 
 def $subst_storagetype(t, xx*, ht*) = $subst_valtype(t, xx*, ht*)
-def $subst_storagetype(pt, xx*, ht*) = $subst_packedtype(pt, xx*, ht*)
+def $subst_storagetype(pt, xx*, ht*) = $subst_packtype(pt, xx*, ht*)
 
 def $subst_fieldtype((mut zt), xx*, ht*) = mut $subst_storagetype(zt, xx*, ht*)
 

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

@@ -59,23 +59,23 @@ def $narrow(M, N, sx, iN(M)) : iN(N)    hint(show $narrow_((%,%))^(%)#(%))
 
 ;; Packed values
 
-def $packnum(lanetype, num_($lunpack(lanetype))) : lnum_(lanetype)
+def $packnum(lanetype, num_($lunpack(lanetype))) : lane_(lanetype)
     hint(show $pack_(%,%))
 def $packnum(numtype, c) = c
-def $packnum(packedtype, c) = $wrap($size($lunpack(packedtype)), $psize(packedtype), c)
+def $packnum(packtype, c) = $wrap($size($lunpack(packtype)), $psize(packtype), c)
 
-def $unpacknum(lanetype, lnum_(lanetype)) : num_($lunpack(lanetype))
+def $unpacknum(lanetype, lane_(lanetype)) : num_($lunpack(lanetype))
     hint(show $unpack_(%,%))
 def $unpacknum(numtype, c) = c
-def $unpacknum(packedtype, c) = $ext($psize(packedtype), $size($lunpack(packedtype)), U, c)
+def $unpacknum(packtype, c) = $ext($psize(packtype), $size($lunpack(packtype)), U, c)
 
 
 ;; Vectors
 
-def $lanes_(shape, vec_(V128)) : lnum_($lanetype(shape))*
+def $lanes_(shape, vec_(V128)) : lane_($lanetype(shape))*
     hint(show $lanes_(%,%))
 
-def $invlanes_(shape, lnum_($lanetype(shape))*) : vec_(V128)
+def $invlanes_(shape, lane_($lanetype(shape))*) : vec_(V128)
     hint(show $lanes^(-1)#_%#(%,%))
 def $invlanes_(sh, c*) = vc  -- if c* = $lanes_(sh, vc)
 
@@ -99,7 +99,7 @@ def $vbinop(shape, vbinop_(shape), vec_(V128), vec_(V128)) : vec_(V128)*
 def $vrelop(shape, vrelop_(shape), vec_(V128), vec_(V128)) : vec_(V128)
     hint(show %2#_%1#(%3, %4))
 
-def $vcvtop(shape_1, shape_2, vcvtop, sx?, lnum_($lanetype(shape_1))) : lnum_($lanetype(shape_2))
+def $vcvtop(shape_1, shape_2, vcvtop, sx?, lane_($lanetype(shape_1))) : lane_($lanetype(shape_2))
     hint(show %3#$_((%1,%2))^(%5)#((%6)))
 
 def $vextunop(ishape_1, ishape_2, vextunop_(ishape_1, ishape_2), sx, vec_(V128)) : vec_(V128)
@@ -108,5 +108,5 @@ def $vextbinop(ishape_1, ishape_2, vextbinop_(ishape_1, ishape_2), sx, vec_(V128
     hint(show %3#$_((%1,%2))^(%5)#((%6,%7)))
 
 ;; TODO: refactor for consistency?
-def $vishiftop(ishape, vshiftop_(ishape), lnum_($lanetype(ishape)), u32) : lnum_($lanetype(ishape))
+def $vishiftop(ishape, vshiftop_(ishape), lane_($lanetype(ishape)), u32) : lane_($lanetype(ishape))
     hint(show %2#_%1#(%3, %4))

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

@@ -91,10 +91,10 @@ syntax exportinst hint(desc "export instance") =
   { NAME name,
     VALUE externval }
 
-syntax packedval hint(desc "packed value") =
-  | PACK packedtype pnum_(packedtype)    hint(show %.PACK %)
+syntax packval hint(desc "packed value") =
+  | PACK packtype pack_(packtype)    hint(show %.PACK %)
 syntax fieldval hint(desc "field value") =
-  | val | packedval
+  | val | packval
 syntax structinst hint(desc "structure instance") =
   { TYPE deftype,
     FIELD fieldval* }
@@ -124,7 +124,7 @@ var xi : exportinst
 var si : structinst
 var ai : arrayinst
 var fv : fieldval
-var pv : packedval
+var pv : packval
 
 
 ;; Configurations proper

spectec/spec/wasm-3.0/6-typing.watsup

@@ -109,7 +109,7 @@ rule Instrtype_ok:
 syntax oktypeidx hint(show OK#((typeidx)))    = | OK typeidx      hint(show OK#(%))
 syntax oktypeidxnat hint(show OK#(typeidx,n)) = | OK typeidx nat  hint(show OK#(%, %))
 
-relation Packedtype_ok: context |- packedtype : OK    hint(show "K-packed")
+relation Packtype_ok: context |- packtype : OK        hint(show "K-pack")
 relation Fieldtype_ok: context |- fieldtype : OK      hint(show "K-field")
 relation Storagetype_ok: context |- storagetype : OK  hint(show "K-storage")
 relation Comptype_ok: context |- comptype : OK        hint(show "K-comp")
@@ -125,16 +125,16 @@ relation Comptype_sub: context |- comptype <: comptype  hint(show "S-comp")
 relation Deftype_sub: context |- deftype <: deftype     hint(show "S-def")
 
 
-rule Packedtype_ok:
-  C |- packedtype : OK
+rule Packtype_ok:
+  C |- packtype : OK
 
 rule Storagetype_ok/val:
   C |- valtype : OK
   -- Valtype_ok: C |- valtype : OK
 
-rule Storagetype_ok/packed:
-  C |- packedtype : OK
-  -- Packedtype_ok: C |- packedtype : OK
+rule Storagetype_ok/pack:
+  C |- packtype : OK
+  -- Packtype_ok: C |- packtype : OK
 
 rule Fieldtype_ok:
   C |- mut zt : OK
@@ -388,24 +388,24 @@ rule Instrtype_sub:
 
 ;; Type definitions
 
-relation Packedtype_sub: context |- packedtype <: packedtype         hint(show "S-packed")
+relation Packtype_sub: context |- packtype <: packtype               hint(show "S-pack")
 relation Storagetype_sub: context |- storagetype <: storagetype      hint(show "S-storage")
 relation Fieldtype_sub: context |- fieldtype <: fieldtype            hint(show "S-field")
 ;;relation Comptype_sub: context |- comptype <: comptype             hint(show "S-comp")
 relation Functype_sub: context |- functype <: functype               hint(show "S-func")
 ;;relation Deftype_sub: context |- deftype <: deftype                hint(show "S-def")
 
-rule Packedtype_sub:
-  C |- packedtype <: packedtype
+rule Packtype_sub:
+  C |- packtype <: packtype
 
 
 rule Storagetype_sub/val:
   C |- valtype_1 <: valtype_2
   -- Valtype_sub: C |- valtype_1 <: valtype_2
 
-rule Storagetype_sub/packed:
-  C |- packedtype_1 <: packedtype_2
-  -- Packedtype_sub: C |- packedtype_1 <: packedtype_2
+rule Storagetype_sub/pack:
+  C |- packtype_1 <: packtype_2
+  -- Packtype_sub: C |- packtype_1 <: packtype_2
 
 
 rule Fieldtype_sub/const:

spectec/spec/wasm-3.0/A-binary.watsup

@@ -128,13 +128,13 @@ grammar Bmut : mut =
   | 0x00 => eps
   | 0x01 => MUT
 
-grammar Bpackedtype : packedtype =
+grammar Bpacktype : packtype =
   | 0x78 => I8
   | 0x77 => I16
 
 grammar Bstoragetype : storagetype =
   | t:Bvaltype => t
-  | pt:Bpackedtype => pt
+  | pt:Bpacktype => pt
 
 grammar Bfieldtype : fieldtype =
   | zt:Bstoragetype mut:Bmut => mut zt