Skip to content

Commit

Permalink
Remove $idx (#122)
Browse files Browse the repository at this point in the history
  • Loading branch information
@ShinWonho
ShinWonho authored Sep 6, 2024
1 parent 177d014 commit a2240b2
Show file tree
Hide file tree
Showing 10 changed files with 1,356 additions and 1,410 deletions.
15 changes: 6 additions & 9 deletions spectec/spec/wasm-3.0/2-syntax-aux.watsup
View file
Original file line number Diff line number Diff line change
Expand Up @@ -103,14 +103,11 @@ def $diffrt((REF nul1 ht_1), (REF ht_2)) = (REF nul1 ht_1)

;; Injection

syntax typevar = _IDX typeidx | REC nat
syntax typevar = _IDX typeidx hint(show %) | REC nat
var tv : typevar
var yy : typeuse hint(show y)
var tu : typeuse

def $idx(typeidx) : typevar hint(show %)
def $idx(x) = _IDX x


;; Free indices

Expand Down Expand Up @@ -616,10 +613,10 @@ def $subst_all_reftype(reftype, heaptype*) : reftype hint(show %#`[:=%]) hint(m
def $subst_all_deftype(deftype, heaptype*) : deftype hint(show %#`[:=%]) hint(macro "%subst")
def $subst_all_moduletype(moduletype, heaptype*) : moduletype hint(show %#`[:=%]) hint(macro "%subst")

def $subst_all_valtype(t, tu^n) = $subst_valtype(t, $idx(i)^(i<n), tu^n)
def $subst_all_reftype(rt, tu^n) = $subst_reftype(rt, $idx(i)^(i<n), tu^n)
def $subst_all_deftype(dt, tu^n) = $subst_deftype(dt, $idx(i)^(i<n), tu^n)
def $subst_all_moduletype(mmt, tu^n) = $subst_moduletype(mmt, $idx(i)^(i<n), tu^n)
def $subst_all_valtype(t, tu^n) = $subst_valtype(t, (_IDX i)^(i<n), tu^n)
def $subst_all_reftype(rt, tu^n) = $subst_reftype(rt, (_IDX i)^(i<n), tu^n)
def $subst_all_deftype(dt, tu^n) = $subst_deftype(dt, (_IDX i)^(i<n), tu^n)
def $subst_all_moduletype(mmt, tu^n) = $subst_moduletype(mmt, (_IDX i)^(i<n), tu^n)

def $subst_all_deftypes(deftype*, heaptype*) : deftype* hint(show %#`[:=%]) hint(macro "%subst")
def $subst_all_deftypes(eps, tu*) = eps
Expand All @@ -637,7 +634,7 @@ def $expanddt(deftype) : comptype hint(show $expand(%)) hint(macro "e
;; TODO(3, rossberg): in general, multi-dimensional use of dimensioned vars is ambiguous;
;; for example, x** with dimension x* could be x1 x2 x1 x2 or x1 x1 x2 x2.
;; For now, we avoid to reuse the dimension var in exact same form
def $rollrt(x, rectype) = REC ($subst_subtype(subtype, ($idx($(x + i)))^(i<n), (REC i)^(i<n)))^n
def $rollrt(x, rectype) = REC ($subst_subtype(subtype, ((_IDX $(x + i)))^(i<n), (REC i)^(i<n)))^n
-- if rectype = REC subtype^n
def $unrollrt(rectype) = REC ($subst_subtype(subtype, (REC i)^(i<n), (DEF rectype i)^(i<n)))^n
-- if rectype = REC subtype^n
Expand Down
42 changes: 21 additions & 21 deletions spectec/spec/wasm-3.0/6-typing.watsup
View file
Original file line number Diff line number Diff line change
Expand Up @@ -171,10 +171,10 @@ rule Comptype_ok/func:


rule Subtype_ok:
C |- SUB FINAL? $idx(x)* comptype : OK(x_0)
C |- SUB FINAL? (_IDX x)* comptype : OK(x_0)
-- if |x*| <= 1
-- (if x < x_0)*
-- (if $unrolldt(C.TYPES[x]) = SUB $idx(x')* comptype')*
-- (if $unrolldt(C.TYPES[x]) = SUB (_IDX x')* comptype')*
----
-- Comptype_ok: C |- comptype : OK
-- (Comptype_sub: C |- comptype <: comptype')*
Expand Down Expand Up @@ -682,11 +682,11 @@ rule Instr_ok/call:
-- Expand: C.FUNCS[x] ~~ FUNC (t_1* -> t_2*)

rule Instr_ok/call_ref:
C |- CALL_REF $idx(x) : t_1* (REF NULL $idx(x)) -> t_2*
C |- CALL_REF (_IDX x) : t_1* (REF NULL (_IDX x)) -> t_2*
-- Expand: C.TYPES[x] ~~ FUNC (t_1* -> t_2*)

rule Instr_ok/call_indirect:
C |- CALL_INDIRECT x $idx(y) : t_1* I32 -> t_2*
C |- CALL_INDIRECT x (_IDX y) : t_1* I32 -> t_2*
-- if C.TABLES[x] = lim rt
-- Reftype_sub: C |- rt <: (REF NULL FUNC)
-- Expand: C.TYPES[y] ~~ FUNC (t_1* -> t_2*)
Expand All @@ -706,15 +706,15 @@ rule Instr_ok/return_call:

;; TODO(3, rossberg): enable t_2* <: C.RETURN
rule Instr_ok/return_call_ref:
C |- RETURN_CALL_REF $idx(x) : t_3* t_1* (REF NULL $idx(x)) -> t_4*
C |- RETURN_CALL_REF (_IDX x) : t_3* t_1* (REF NULL (_IDX x)) -> t_4*
-- Expand: C.TYPES[x] ~~ FUNC (t_1* -> t_2*)
-- if C.RETURN = (t'_2*)
-- Resulttype_sub: C |- t_2* <: t'_2*
-- Instrtype_ok: C |- t_3* -> t_4* : OK

;; TODO(3, rossberg): enable t_2* <: C.RETURN
rule Instr_ok/return_call_indirect:
C |- RETURN_CALL_INDIRECT x $idx(y) : t_3* t_1* I32 -> t_4*
C |- RETURN_CALL_INDIRECT x (_IDX y) : t_3* t_1* I32 -> t_4*
-- if C.TABLES[x] = lim rt
-- Reftype_sub: C |- rt <: (REF NULL FUNC)
----
Expand Down Expand Up @@ -830,82 +830,82 @@ rule Instr_ok/i31.get:
;; Structure instructions

rule Instr_ok/struct.new:
C |- STRUCT.NEW x : $unpack(zt)* -> (REF $idx(x))
C |- STRUCT.NEW x : $unpack(zt)* -> (REF (_IDX x))
-- Expand: C.TYPES[x] ~~ STRUCT (mut zt)*

rule Instr_ok/struct.new_default:
C |- STRUCT.NEW_DEFAULT x : eps -> (REF $idx(x))
C |- STRUCT.NEW_DEFAULT x : eps -> (REF (_IDX x))
-- Expand: C.TYPES[x] ~~ STRUCT (mut zt)*
-- (if $default_($unpack(zt)) = val)*

rule Instr_ok/struct.get:
C |- STRUCT.GET sx? x i : (REF NULL $idx(x)) -> $unpack(zt)
C |- STRUCT.GET sx? x i : (REF NULL (_IDX x)) -> $unpack(zt)
-- Expand: C.TYPES[x] ~~ STRUCT yt*
-- if yt*[i] = mut zt
-- if sx? = eps <=> zt = $unpack(zt)

rule Instr_ok/struct.set:
C |- STRUCT.SET x i : (REF NULL $idx(x)) $unpack(zt) -> eps
C |- STRUCT.SET x i : (REF NULL (_IDX x)) $unpack(zt) -> eps
-- Expand: C.TYPES[x] ~~ STRUCT yt*
-- if yt*[i] = MUT zt


;; Array instructions

rule Instr_ok/array.new:
C |- ARRAY.NEW x : $unpack(zt) I32 -> (REF $idx(x))
C |- ARRAY.NEW x : $unpack(zt) I32 -> (REF (_IDX x))
-- Expand: C.TYPES[x] ~~ ARRAY (mut zt)

rule Instr_ok/array.new_default:
C |- ARRAY.NEW_DEFAULT x : I32 -> (REF $idx(x))
C |- ARRAY.NEW_DEFAULT x : I32 -> (REF (_IDX x))
-- Expand: C.TYPES[x] ~~ ARRAY (mut zt)
-- if $default_($unpack(zt)) = val

rule Instr_ok/array.new_fixed:
C |- ARRAY.NEW_FIXED x n : $unpack(zt)^n -> (REF $idx(x))
C |- ARRAY.NEW_FIXED x n : $unpack(zt)^n -> (REF (_IDX x))
-- Expand: C.TYPES[x] ~~ ARRAY (mut zt)

rule Instr_ok/array.new_elem:
C |- ARRAY.NEW_ELEM x y : I32 I32 -> (REF $idx(x))
C |- ARRAY.NEW_ELEM x y : I32 I32 -> (REF (_IDX x))
-- Expand: C.TYPES[x] ~~ ARRAY (mut rt)
-- Reftype_sub: C |- C.ELEMS[y] <: rt

rule Instr_ok/array.new_data:
C |- ARRAY.NEW_DATA x y : I32 I32 -> (REF $idx(x))
C |- ARRAY.NEW_DATA x y : I32 I32 -> (REF (_IDX x))
-- Expand: C.TYPES[x] ~~ ARRAY (mut zt)
-- if $unpack(zt) = numtype \/ $unpack(zt) = vectype
-- if C.DATAS[y] = OK

rule Instr_ok/array.get:
C |- ARRAY.GET sx? x : (REF NULL $idx(x)) I32 -> $unpack(zt)
C |- ARRAY.GET sx? x : (REF NULL (_IDX x)) I32 -> $unpack(zt)
-- Expand: C.TYPES[x] ~~ ARRAY (mut zt)
-- if sx? = eps <=> zt = $unpack(zt)

rule Instr_ok/array.set:
C |- ARRAY.SET x : (REF NULL $idx(x)) I32 $unpack(zt) -> eps
C |- ARRAY.SET x : (REF NULL (_IDX x)) I32 $unpack(zt) -> eps
-- Expand: C.TYPES[x] ~~ ARRAY (MUT zt)

rule Instr_ok/array.len:
C |- ARRAY.LEN : (REF NULL ARRAY) -> I32
-- Expand: C.TYPES[x] ~~ ARRAY (MUT zt)

rule Instr_ok/array.fill:
C |- ARRAY.FILL x : (REF NULL $idx(x)) I32 $unpack(zt) I32 -> eps
C |- ARRAY.FILL x : (REF NULL (_IDX x)) I32 $unpack(zt) I32 -> eps
-- Expand: C.TYPES[x] ~~ ARRAY (MUT zt)

rule Instr_ok/array.copy:
C |- ARRAY.COPY x_1 x_2 : (REF NULL $idx(x_1)) I32 (REF NULL $idx(x_2)) I32 I32 -> eps
C |- ARRAY.COPY x_1 x_2 : (REF NULL (_IDX x_1)) I32 (REF NULL (_IDX x_2)) I32 I32 -> eps
-- Expand: C.TYPES[x_1] ~~ ARRAY (MUT zt_1)
-- Expand: C.TYPES[x_2] ~~ ARRAY (mut zt_2)
-- Storagetype_sub: C |- zt_2 <: zt_1

rule Instr_ok/array.init_elem:
C |- ARRAY.INIT_ELEM x y : (REF NULL $idx(x)) I32 I32 I32 -> eps
C |- ARRAY.INIT_ELEM x y : (REF NULL (_IDX x)) I32 I32 I32 -> eps
-- Expand: C.TYPES[x] ~~ ARRAY (MUT zt)
-- Storagetype_sub: C |- C.ELEMS[y] <: zt

rule Instr_ok/array.init_data:
C |- ARRAY.INIT_DATA x y : (REF NULL $idx(x)) I32 I32 I32 -> eps
C |- ARRAY.INIT_DATA x y : (REF NULL (_IDX x)) I32 I32 I32 -> eps
-- Expand: C.TYPES[x] ~~ ARRAY (MUT zt)
-- if $unpack(zt) = numtype \/ $unpack(zt) = vectype
-- if C.DATAS[y] = OK
Expand Down
2 changes: 1 addition & 1 deletion spectec/spec/wasm-3.0/8-reduction.watsup
View file
Original file line number Diff line number Diff line change
Expand Up @@ -335,7 +335,7 @@ rule Step_pure/cvtop-trap:
;; Reference instructions

rule Step_read/ref.null-idx:
z; (REF.NULL $idx(x)) ~> (REF.NULL $type(z, x))
z; (REF.NULL (_IDX x)) ~> (REF.NULL $type(z, x))

rule Step_read/ref.func:
z; (REF.FUNC x) ~> (REF.FUNC_ADDR $moduleinst(z).FUNCS[x])
Expand Down
12 changes: 6 additions & 6 deletions spectec/spec/wasm-3.0/A-binary.watsup
View file
Original file line number Diff line number Diff line change
Expand Up @@ -160,8 +160,8 @@ grammar Bcomptype : comptype =
| 0x60 t_1*:Bresulttype t_2*:Bresulttype => FUNC (t_1* -> t_2*)

grammar Bsubtype : subtype =
| 0x4F x*:Blist(Btypeidx) ct:Bcomptype => SUB FINAL $idx(x)* ct
| 0x50 x*:Blist(Btypeidx) ct:Bcomptype => SUB $idx(x)* ct
| 0x4F x*:Blist(Btypeidx) ct:Bcomptype => SUB FINAL (_IDX x)* ct
| 0x50 x*:Blist(Btypeidx) ct:Bcomptype => SUB (_IDX x)* ct
| ct:Bcomptype => SUB FINAL eps ct

grammar Brectype : rectype =
Expand Down Expand Up @@ -189,11 +189,11 @@ grammar Btagtype : typeidx =


grammar Bexterntype : externtype =
| 0x00 x:Btypeidx => FUNC $idx(x)
| 0x00 x:Btypeidx => FUNC (_IDX x)
| 0x01 tt:Btabletype => TABLE tt
| 0x02 mt:Bmemtype => MEM mt
| 0x03 gt:Bglobaltype => GLOBAL gt
| 0x04 x:Btagtype => TAG $idx(x)
| 0x04 x:Btagtype => TAG (_IDX x)


;;
Expand Down Expand Up @@ -228,9 +228,9 @@ grammar Binstr/control : instr =
| 0x0E l*:Blist(Blabelidx) l_n:Blabelidx => BR_TABLE l* l_n
| 0x0F => RETURN
| 0x10 x:Bfuncidx => CALL x
| 0x11 y:Btypeidx x:Btableidx => CALL_INDIRECT x $idx(y)
| 0x11 y:Btypeidx x:Btableidx => CALL_INDIRECT x (_IDX y)
| 0x12 x:Bfuncidx => RETURN_CALL x
| 0x13 y:Btypeidx x:Btableidx => RETURN_CALL_INDIRECT x $idx(y)
| 0x13 y:Btypeidx x:Btableidx => RETURN_CALL_INDIRECT x (_IDX y)
| 0x1F bt:Bblocktype c*:Blist(Bcatch) (in:Binstr)* 0x0B =>
TRY_TABLE bt c* in*
| ...
Expand Down
Loading

0 comments on commit a2240b2

Please sign in to comment.