Make relation xrefs work

document/core/util/macros.def

@@ -240,6 +240,10 @@
 .. |SET| mathdef:: \xref{valid/conventions}{syntax-init}{\K{set}}
 .. |UNSET| mathdef:: \xref{valid/conventions}{syntax-init}{\K{unset}}
 
+.. |Llbrack| mathdef:: \xref{syntax/types}{syntax-limits}{\[}
+.. |Lrbrack| mathdef:: \xref{syntax/types}{syntax-limits}{\]}
+.. |Ldotdot| mathdef:: \xref{syntax/types}{syntax-limits}{\,{..}\,}
+.. TODO: remove
 .. |LMIN| mathdef:: \xref{syntax/types}{syntax-limits}{\K{min}}
 .. |LMAX| mathdef:: \xref{syntax/types}{syntax-limits}{\K{max}}
 
@@ -1316,6 +1320,7 @@
 
 .. |ZSTORE| mathdef:: \xref{exec/runtime}{syntax-store}{\K{store}}
 .. |ZFRAME| mathdef:: \xref{exec/runtime}{syntax-store}{\K{frame}}
+.. |ZMODULE| mathdef:: \xref{exec/runtime}{syntax-store}{\K{module}}
 .. |ZTYPES| mathdef:: \xref{exec/runtime}{syntax-store}{\K{types}}
 .. |ZFUNCS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{funcs}}
 .. |ZGLOBALS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{globals}}

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

@@ -228,7 +228,7 @@ syntax rectype hint(desc "recursive type") hint(macro "%" "T%") =
 
 ;; External types
 
-syntax limits hint(desc "limits") =
+syntax limits hint(desc "limits") hint(macro "%" "L%") =
   `[u32 .. u32]
 
 syntax globaltype hint(desc "global type") =
@@ -519,23 +519,23 @@ syntax instr/vec hint(desc "vector instruction") = ...
   | VTESTOP shape vtestop_(shape)       hint(show %.%)
   | VRELOP shape vrelop_(shape)         hint(show %.%)
   | VSHIFTOP ishape vshiftop_(ishape)   hint(show %.%)
-  | VBITMASK ishape                     hint(show %.BITMASK)
-  | VSWIZZLE ishape                     hint(show %.SWIZZLE)
+  | VBITMASK ishape                     hint(show %.BITMASK)   hint(macro "VBITMASK")
+  | VSWIZZLE ishape                     hint(show %.SWIZZLE)   hint(macro "VSWIZZLE")
     -- if ishape = I8 X `16
-  | VSHUFFLE ishape laneidx*            hint(show %.SHUFFLE %)
+  | VSHUFFLE ishape laneidx*            hint(show %.SHUFFLE %) hint(macro "VSHUFFLE")
     -- if ishape = I8 X `16 /\ |laneidx*| = 16
-  | VSPLAT shape                        hint(show %.SPLAT)
-  | VEXTRACT_LANE shape sx? laneidx     hint(show %.EXTRACT_LANE#_#% %)
+  | VSPLAT shape                        hint(show %.SPLAT)     hint(macro "VSPLAT")
+  | VEXTRACT_LANE shape sx? laneidx     hint(show %.EXTRACT_LANE#_#% %) hint(macro "VEXTRACT_LANE")
     -- if $lanetype(shape) = numtype <=> sx? = eps
-  | VREPLACE_LANE shape laneidx         hint(show %.REPLACE_LANE %)
+  | VREPLACE_LANE shape laneidx         hint(show %.REPLACE_LANE %)     hint(macro "VREPLACE_LANE")
   | VEXTUNOP ishape_1 ishape_2 vextunop_(ishape_1) sx
     hint(show %1.%3#_#%2#_#%4)
     -- if $($lsize($lanetype(ishape_1)) = 2*$lsize($lanetype(ishape_2)))
   | VEXTBINOP ishape_1 ishape_2 vextbinop_(ishape_1) sx
     hint(show %1.%3#_#%2#_#%4)
     -- if $($lsize($lanetype(ishape_1)) = 2*$lsize($lanetype(ishape_2)))
     ;; TODO: /\ (vextbinop =/= DOT \/ sx = S)
-  | VNARROW ishape_1 ishape_2 sx        hint(show %.NARROW#_#%#_#%)
+  | VNARROW ishape_1 ishape_2 sx        hint(show %.NARROW#_#%#_#%) hint(macro "VNARROW")
     -- if $($lsize($lanetype(ishape_2)) = 2*$lsize($lanetype(ishape_1)) <= 32)
   | VCVTOP shape_1 shape_2 vcvtop_(shape_2, shape_1) half_(shape_2, shape_1)? sx? zero_(shape_2, shape_1)?
     hint(show %1.%3#_#%4#_#%2#_#%5#_#%6)

spectec/spec/wasm-3.0/5-runtime-aux.watsup

@@ -75,10 +75,7 @@ def $frame(state) : frame             hint(show %.FRAME) hint(macro "Z%")
 def $store((s; f)) = s
 def $frame((s; f)) = f
 
-
-def $funcaddr(state) : funcaddr*      hint(show %.MODULE.FUNCS) hint(macro "Z%")
-def $funcaddr((s; f)) = f.MODULE.FUNCS
-
+def $moduleinst(state) : moduleinst   hint(show %.MODULE)  hint(macro "Z%")
 def $funcinst(state) : funcinst*      hint(show %.FUNCS)   hint(macro "Z%")
 def $globalinst(state) : globalinst*  hint(show %.GLOBALS) hint(macro "Z%")
 def $tableinst(state) : tableinst*    hint(show %.TABLES)  hint(macro "Z%")
@@ -87,8 +84,8 @@ def $eleminst(state) : eleminst*      hint(show %.ELEMS)   hint(macro "Z%")
 def $datainst(state) : datainst*      hint(show %.DATAS)   hint(macro "Z%")
 def $structinst(state) : structinst*  hint(show %.STRUCTS) hint(macro "Z%")
 def $arrayinst(state) : arrayinst*    hint(show %.ARRAYS)  hint(macro "Z%")
-def $moduleinst(state) : moduleinst   hint(show %.MODULE)  hint(macro "Z%")
 
+def $moduleinst((s; f)) = f.MODULE
 def $funcinst((s; f)) = s.FUNCS
 def $globalinst((s; f)) = s.GLOBALS
 def $tableinst((s; f)) = s.TABLES
@@ -97,7 +94,6 @@ def $eleminst((s; f)) = s.ELEMS
 def $datainst((s; f)) = s.DATAS
 def $structinst((s; f)) = s.STRUCTS
 def $arrayinst((s; f)) = s.ARRAYS
-def $moduleinst((s; f)) = f.MODULE
 
 def $type(state, typeidx) : deftype         hint(show %.TYPES[%])   hint(macro "Z%")
 def $func(state, funcidx) : funcinst        hint(show %.FUNCS[%])   hint(macro "Z%")

spectec/spec/wasm-3.0/8-reduction.watsup

@@ -158,7 +158,7 @@ rule Step_read/br_on_cast_fail-fail:
 
 rule Step_read/call:
   z; (CALL x)  ~>  (REF.FUNC_ADDR a) (CALL_REF $funcinst(z)[a].TYPE)
-  -- if $funcaddr(z)[x] = a
+  -- if $moduleinst(z).FUNCS[x] = a
 
 rule Step_read/call_ref-null:
   z; (REF.NULL ht) (CALL_REF yy)  ~>  TRAP
@@ -174,7 +174,7 @@ rule Step_read/call_ref-func:
 
 rule Step_read/return_call:
   z; (RETURN_CALL x)  ~>  (REF.FUNC_ADDR a) (RETURN_CALL_REF $funcinst(z)[a].TYPE)
-  -- if $funcaddr(z)[x] = a
+  -- if $moduleinst(z).FUNCS[x] = a
 
 
 rule Step_read/return_call_ref-label:
@@ -250,7 +250,7 @@ rule Step_read/ref.null-idx:
   z; (REF.NULL $idx(x))  ~>  (REF.NULL $type(z, x))
 
 rule Step_read/ref.func:
-  z; (REF.FUNC x)  ~>  (REF.FUNC_ADDR $funcaddr(z)[x])
+  z; (REF.FUNC x)  ~>  (REF.FUNC_ADDR $moduleinst(z).FUNCS[x])
 
 rule Step_pure/ref.i31:
   (CONST I32 i) REF.I31  ~>  (REF.I31_NUM $wrap(32, 31, i))