Merge pull request #79 from Wasm-DSL/ConT

Enable "refinement" types

document/core/syntax/types.rst

@@ -36,8 +36,10 @@ Values of number type can be stored in :ref:`memories <syntax-mem>`.
 Conventions
 ...........
 
-* The notation ${:|t|}` denotes the *bit width* of a number type ${:t}.
-  That is, ${:|I32| = |F32| = 32} and ${:|I64| = |F64| = 64}.
+* The notation ${:$size(t)}` denotes the *bit width* of a number type ${:t}.
+  That is, ${:$size(I32) = $size(F32) = 32} and ${:$size(I64) = $size(F64) = 64}.
+
+$${definition-ignore: size}
 
 
 .. index:: ! vector type, integer, floating-point, IEEE 754, bit width, memory, SIMD
@@ -64,8 +66,9 @@ Values of vector type can be stored in :ref:`memories <syntax-mem>`.
 Conventions
 ...........
 
-* The notation ${:|t|} for :ref:`bit width <bitwidth-numtype>` extends to vector types as well, that is, ${:|V128| = 128}.
+* The notation ${:$vsize(t)} for :ref:`bit width <bitwidth-numtype>` extends to vector types as well, that is, ${:$vsize(V128) = 128}.
 
+$${definition-ignore: vsize}
 
 
 .. index:: ! heap type, store, type index, ! abstract type, ! concrete type, ! unboxed scalar
@@ -85,7 +88,7 @@ There are three disjoint hierarchies of heap types:
 - *aggregate types* classify dynamically allocated *managed* data, such as *structures*, *arrays*, or *unboxed scalars*,
 - *external types* classify *external* references possibly owned by the :ref:`embedder <embedder>`.
 
-The values from the latter two hierarchies are interconvertible by ways of the |EXTERNCONVERTANY| and |ANYCONVERTEXTERN| instructions.
+The values from the latter two hierarchies are interconvertible by ways of the ${instr: EXTERN.CONVERT_ANY} and ${instr: ANY.CONVERT_EXTERN} instructions.
 That is, both type hierarchies are inhabited by an isomorphic set of values, but may have different, incompatible representations in practice.
 
 $${syntax: {absheaptype/syn heaptype/syn}}
@@ -250,7 +253,9 @@ $${syntax: {structtype arraytype fieldtype storagetype packtype}}
 Conventions
 ...........
 
-* The notation ${:|t|} for :ref:`bit width <bitwidth-valtype>` extends to packed types as well, that is, ${:|I8| = 8} and ${:|I16| = 16}.
+* The notation ${:$psize(t)} for :ref:`bit width <bitwidth-valtype>` extends to packed types as well, that is, ${:$psize(I8) = 8} and ${:$psize(I16) = 16}.
+
+$${definition-ignore: psize}
 
 
 .. index:: ! composite type, function type, aggreagate type, structure type, array type

document/core/syntax/values.rst

@@ -134,7 +134,7 @@ Vectors
 ~~~~~~~
 
 *Numeric vectors* are 128-bit values that are processed by vector instructions (also known as *SIMD* instructions, single instruction multiple data).
-They are represented in the abstract syntax using |i128|. The interpretation of lane types (:ref:`integer <syntax-int>` or :ref:`floating-point <syntax-float>` numbers) and lane sizes are determined by the specific instruction operating on them.
+They are represented in the abstract syntax using ${:i128}. The interpretation of lane types (:ref:`integer <syntax-int>` or :ref:`floating-point <syntax-float>` numbers) and lane sizes are determined by the specific instruction operating on them.
 
 
 .. index:: ! name, byte, Unicode, UTF-8, character, binary format

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

@@ -2,20 +2,8 @@
 ;; Lists
 ;;
 
-;; TODO: make alias
-syntax list(syntax A) = | _LIST A*  -- if |A*| < $(2^32)
-
-
-;;
-;; Names
-;;
-
-syntax char hint(desc "character") = U+0000 | ... | U+D7FF | U+E000 | ... | U+10FFFF
-
-;; TODO: enable side condition
-syntax name hint(desc "name") = char*  ;; -- if |$utf8(char*)| < $(2^32)
-
-var nm : name
+;; TODO: enable writing X^n
+syntax list(syntax X) = X*  -- if |X*| < $(2^32)
 
 
 ;;
@@ -79,6 +67,19 @@ def $canon_(N) : nat
 def $canon_(N) = $(2^($signif(N)-1))
 
 
+;;
+;; Names
+;;
+
+syntax char hint(desc "character") = U+0000 | ... | U+D7FF | U+E000 | ... | U+10FFFF
+
+def $utf8(char*) : byte*
+
+syntax name hint(desc "name") = char*  -- if |$utf8(char*)| < $(2^32)
+
+var nm : name
+
+
 ;;
 ;; Indices
 ;;

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

@@ -43,9 +43,9 @@ grammar Bf64 : f64 = | p:BfN(64) => p
 
 ;; Names
 
-var ch : nat
+var ch : char
 
-def $utf8(name) : byte*
+;; def $utf8(char*) : byte*
 def $utf8(ch) = b  -- if ch < U+0080 /\ ch = b
 def $utf8(ch) = b_1 b_2  -- if U+0080 <= ch < U+0800 /\ ch = $(2^6*(b_1 - 0xC0) + (b_2 - 0x80))
 def $utf8(ch) = b_1 b_2 b_3  -- if (U+0800 <= ch < U+D800 \/ U+E000 <= ch < U+10000) /\ ch = $(2^12*(b_1 - 0xE0) + 2^6*(b_2 - 0x80) + (b_3 - 0x80))

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

@@ -2,20 +2,8 @@
 ;; Lists
 ;;
 
-;; TODO: make alias
-syntax list(syntax A) = | _LIST A*  -- if |A*| < $(2^32)
-
-
-;;
-;; Names
-;;
-
-syntax char hint(desc "character") = U+0000 | ... | U+D7FF | U+E000 | ... | U+10FFFF
-
-;; TODO: enable side condition
-syntax name hint(desc "name") = char*  ;; -- if |$utf8(char*)| < $(2^32)
-
-var nm : name
+;; TODO: enable writing X^n
+syntax list(syntax X) = X*  -- if |X*| < $(2^32)
 
 
 ;;
@@ -90,6 +78,19 @@ syntax vN(N) hint(desc "vector") hint(show v#%) =
   iN(N)
 
 
+;;
+;; Names
+;;
+
+syntax char hint(desc "character") = U+0000 | ... | U+D7FF | U+E000 | ... | U+10FFFF
+
+def $utf8(char*) : byte*
+
+syntax name hint(desc "name") = char*  -- if |$utf8(char*)| < $(2^32)
+
+var nm : name
+
+
 ;;
 ;; Indices
 ;;
@@ -268,13 +269,13 @@ syntax vbinop_(shape)
 syntax vbinop_(imm X N) =
   | ADD
   | SUB
-  | ADD_SAT sx     -- if $lsize(imm) <= 16
-  | SUB_SAT sx     -- if $lsize(imm) <= 16
-  | MUL            -- if $lsize(imm) >= 16
-  | AVGR_U         -- if $lsize(imm) <= 16
-  | Q15MULR_SAT_S  -- if $lsize(imm) = 16
-  | MIN sx         -- if $lsize(imm) <= 32
-  | MAX sx         -- if $lsize(imm) <= 32
+  | ADD_SAT sx hint(show ADD_SAT#_#sx)     -- if $lsize(imm) <= 16
+  | SUB_SAT sx hint(show SUB_SAT#_#sx)     -- if $lsize(imm) <= 16
+  | MUL                                    -- if $lsize(imm) >= 16
+  | AVGR_U                                 -- if $lsize(imm) <= 16
+  | 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 vtestop_(shape)

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

@@ -44,9 +44,9 @@ grammar Bf64 : f64 = | p:BfN(64) => p
 
 ;; Names
 
-var ch : nat
+var ch : char
 
-def $utf8(name) : byte*
+;; def $utf8(char*) : byte*
 def $utf8(ch) = b  -- if ch < U+0080 /\ ch = b
 def $utf8(ch) = b_1 b_2  -- if U+0080 <= ch < U+0800 /\ ch = $(2^6*(b_1 - 0xC0) + (b_2 - 0x80))
 def $utf8(ch) = b_1 b_2 b_3  -- if (U+0800 <= ch < U+D800 \/ U+E000 <= ch < U+10000) /\ ch = $(2^12*(b_1 - 0xE0) + 2^6*(b_2 - 0x80) + (b_3 - 0x80))

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

@@ -2,20 +2,8 @@
 ;; Lists
 ;;
 
-;; TODO: enable side condition
-syntax list(syntax X) = X*  ;; -- if |X*| < $(2^32)
-
-
-;;
-;; Names
-;;
-
-syntax char hint(desc "character") = U+0000 | ... | U+D7FF | U+E000 | ... | U+10FFFF
-
-;; TODO: enable side condition
-syntax name hint(desc "name") = char*  ;; -- if |$utf8(char*)| < $(2^32)
-
-var nm : name
+;; TODO: enable writing X^n
+syntax list(syntax X) = X*  -- if |X*| < $(2^32)
 
 
 ;;
@@ -90,6 +78,19 @@ syntax vN(N) hint(desc "vector") hint(show v#%) =
   iN(N)
 
 
+;;
+;; Names
+;;
+
+syntax char hint(desc "character") = U+0000 | ... | U+D7FF | U+E000 | ... | U+10FFFF
+
+def $utf8(char*) : byte*
+
+syntax name hint(desc "name") = char*  -- if |$utf8(char*)| < $(2^32)
+
+var nm : name
+
+
 ;;
 ;; Indices
 ;;
@@ -252,14 +253,15 @@ var zt : storagetype
 
 ;; Constants
 
-def $size(valtype) : nat       hint(partial) hint(show |%|)
+def $size(numtype) : nat       hint(show |%|)
+def $vsize(vectype) : 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
 
-def $sizenn(valtype) : nat   hint(show n)
-def $sizenn(t) = $size(t)
+def $sizenn(numtype) : nat     hint(show n)
+def $sizenn(nt) = $size(nt)
 
 syntax num_(numtype)
 syntax num_(inn) = iN($sizenn(inn))
@@ -272,7 +274,7 @@ syntax lane_(numtype) = num_(numtype)
 syntax lane_(packtype) = pack_(packtype)
 syntax lane_(imm) = iN($lsize(imm))  ;; HACK
 
-syntax vec_(vnn) = vN($size(vnn))
+syntax vec_(vnn) = vN($vsize(vnn))
 
 syntax zval_(storagetype)
 syntax zval_(numtype) = num_(numtype)
@@ -334,13 +336,13 @@ syntax vbinop_(shape)
 syntax vbinop_(imm X N) =
   | ADD
   | SUB
-  | ADD_SAT sx     -- if $lsize(imm) <= 16
-  | SUB_SAT sx     -- if $lsize(imm) <= 16
-  | MUL            -- if $lsize(imm) >= 16
-  | AVGR_U         -- if $lsize(imm) <= 16
-  | Q15MULR_SAT_S  -- if $lsize(imm) = 16
-  | MIN sx         -- if $lsize(imm) <= 32
-  | MAX sx         -- if $lsize(imm) <= 32
+  | ADD_SAT sx hint(show ADD_SAT#_#sx)     -- if $lsize(imm) <= 16
+  | SUB_SAT sx hint(show SUB_SAT#_#sx)     -- if $lsize(imm) <= 16
+  | MUL                                    -- if $lsize(imm) >= 16
+  | AVGR_U                                 -- if $lsize(imm) <= 16
+  | 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 vtestop_(shape)

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

@@ -45,24 +45,27 @@ 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 $size(numtype) : nat       hint(show |%|)
+;;def $vsize(vectype) : nat      hint(show |%|)
 ;;def $psize(packtype) : nat     hint(show |%|)
 ;;def $lsize(lanetype) : nat     hint(show |%|)
-;;def $zsize(storagetype) : nat  hint(show |%|)
+;;def $zsize(storagetype) : nat  hint(show |%|) hint(partial)
 
 def $size(I32) = 32
 def $size(I64) = 64
 def $size(F32) = 32
 def $size(F64) = 64
-def $size(V128) = 128
+
+def $vsize(V128) = 128
 
 def $psize(I8) = 8
 def $psize(I16) = 16
 
 def $lsize(numtype) = $size(numtype)
 def $lsize(packtype) = $psize(packtype)
 
-def $zsize(valtype) = $size(valtype)
+def $zsize(numtype) = $size(numtype)
+def $zsize(vectype) = $vsize(vectype)
 def $zsize(packtype) = $psize(packtype)
 
 
@@ -196,8 +199,8 @@ def $subst_externtype((MEM mt), xx*, ht*) = MEM $subst_memtype(mt, xx*, ht*)
 def $subst_all_reftype(reftype, heaptype*) : reftype  hint(show %#`[:=%])
 def $subst_all_deftype(deftype, heaptype*) : deftype  hint(show %#`[:=%])
 
-def $subst_all_reftype(rt, ht^n) = $subst_reftype(rt, $idx(x)^(x<n), ht^n)
-def $subst_all_deftype(dt, ht^n) = $subst_deftype(dt, $idx(x)^(x<n), ht^n)
+def $subst_all_reftype(rt, ht^n) = $subst_reftype(rt, $idx(i)^(i<n), ht^n)
+def $subst_all_deftype(dt, ht^n) = $subst_deftype(dt, $idx(i)^(i<n), ht^n)
 
 def $subst_all_deftypes(deftype*, heaptype*) : deftype*  hint(show %#`[:=%])
 

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

@@ -208,12 +208,12 @@ def $vvbinop(vectype, vvbinop, vec_(vectype), vec_(vectype)) : vec_(vectype)
 def $vvternop(vectype, vvternop, vec_(vectype), vec_(vectype), vec_(vectype)) : vec_(vectype)
     hint(show %2#_%1#(%3, %4, %5))
 
-def $vvunop(V128, NOT, v128) = $inot($size(V128), v128)
-def $vvbinop(V128, AND, v128_1, v128_2) = $iand($size(V128), v128_1, v128_2)
-def $vvbinop(V128, ANDNOT, v128_1, v128_2) = $iandnot($size(V128), v128_1, v128_2)
-def $vvbinop(V128, OR, v128_1, v128_2) = $ior($size(V128), v128_1, v128_2)
-def $vvbinop(V128, XOR, v128_1, v128_2) = $ixor($size(V128), v128_1, v128_2)
-def $vvternop(V128, BITSELECT, v128_1, v128_2, v128_3) = $ibitselect($size(V128), v128_1, v128_2, v128_3)
+def $vvunop(V128, NOT, v128) = $inot($vsize(V128), v128)
+def $vvbinop(V128, AND, v128_1, v128_2) = $iand($vsize(V128), v128_1, v128_2)
+def $vvbinop(V128, ANDNOT, v128_1, v128_2) = $iandnot($vsize(V128), v128_1, v128_2)
+def $vvbinop(V128, OR, v128_1, v128_2) = $ior($vsize(V128), v128_1, v128_2)
+def $vvbinop(V128, XOR, v128_1, v128_2) = $ixor($vsize(V128), v128_1, v128_2)
+def $vvternop(V128, BITSELECT, v128_1, v128_2, v128_3) = $ibitselect($vsize(V128), v128_1, v128_2, v128_3)
 
 ;; TODO: rename these to mapunop etc?
 def $vunop(shape, vunop_(shape), vec_(V128)) : vec_(V128)

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

@@ -185,7 +185,7 @@ rule Rectype_ok/empty:
   C |- REC eps : OK(x)
 
 rule Rectype_ok/cons:
-  C |- REC st_1 st* : OK(x)
+  C |- REC (st_1 st*) : OK(x)
   -- Subtype_ok: C |- st_1 : OK(x)
   -- Rectype_ok: C |- REC st* : OK($(x+1))
 
@@ -197,7 +197,7 @@ rule Rectype_ok2/empty:
   C |- REC eps : OK x i
 
 rule Rectype_ok2/cons:
-  C |- REC st_1 st* : OK x i
+  C |- REC (st_1 st*) : OK x i
   -- Subtype_ok2: C |- st_1 : OK x i
   -- Rectype_ok2: C |- REC st* : OK $(x+1) $(i+1)
 
@@ -419,7 +419,7 @@ rule Fieldtype_sub/var:
 
 
 rule Comptype_sub/struct:
-  C |- STRUCT yt_1* yt'_1 <: STRUCT yt_2*
+  C |- STRUCT (yt_1* yt'_1) <: STRUCT yt_2*
   -- (Fieldtype_sub: C |- yt_1 <: yt_2)*
 
 rule Comptype_sub/array:
@@ -1046,7 +1046,7 @@ rule Instr_ok/vload_lane:
 rule Instr_ok/vstore:
   C |- VSTORE x {ALIGN n_A, OFFSET n_O} : I32 V128 -> eps
   -- if C.MEM[x] = mt
-  -- if $(2^(n_A) <= $size(V128)/8)
+  -- if $(2^(n_A) <= $vsize(V128)/8)
 
 rule Instr_ok/vstore_lane:
   C |- VSTORE_LANE n x {ALIGN n_A, OFFSET n_O} laneidx : I32 V128 -> eps