Merge pull request #105 from Wasm-DSL/cvtop

Refine cvtop

document/core/valid/instructions.rst

@@ -195,7 +195,7 @@ $${rule: Instr_ok/relop}
 
 * The instruction is valid with type :math:`[t_1] \to [t_2]`.
 
-$${rule: Instr_ok/cvtop-*}
+$${rule: Instr_ok/cvtop}
 
 
 .. index:: reference instructions, reference type

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

@@ -171,7 +171,8 @@ syntax relop_(Inn) =
 syntax relop_(Fnn) =
   | EQ | NE | LT | GT | LE | GE
 
-syntax cvtop = CONVERT | REINTERPRET
+syntax cvtop =
+  | EXTEND sx | WRAP | CONVERT sx | TRUNC sx | PROMOTE | DEMOTE | REINTERPRET
 
 
 syntax memarg hint(desc "memory argument") = {ALIGN u32, OFFSET u32}
@@ -216,7 +217,7 @@ syntax instr/num hint(desc "numeric instruction") = ...
   | BINOP valtype binop_(valtype)    hint(show %.%)
   | TESTOP valtype testop_(valtype)  hint(show %.%)
   | RELOP valtype relop_(valtype)    hint(show %.%)
-  | CVTOP valtype_1 valtype_2 cvtop sx?  hint(show %1.%3#_#%2#_#%4) hint(show %1.%3#_#%2)
+  | CVTOP valtype_1 valtype_2 cvtop  hint(show %1.%3#_#%2)
     -- if valtype_1 =/= valtype_2
   | ...
 

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

@@ -22,8 +22,8 @@ def $testop(valtype, testop_(valtype), val_(valtype)) : val_(I32)
     hint(show %2#$_(%1)#((%3)))
 def $relop(valtype, relop_(valtype), val_(valtype), val_(valtype)) : val_(I32)
     hint(show %2#$_(%1)#(%3, %4))
-def $cvtop(valtype_1, valtype_2, cvtop, sx?, val_(valtype_1)) : val_(valtype_2)*
-    hint(show %3#$_((%1,%2))^(%4)#((%5)))
+def $cvtop(valtype_1, valtype_2, cvtop, val_(valtype_1)) : val_(valtype_2)*
+    hint(show %3#$_((%1,%2))#((%4)))
 
 def $wrap(M, N, iN(M)) : iN(N)                      hint(show $wrap_((%,%))#((%)))
 def $ext(M, N, sx, iN(M)) : iN(N)                   hint(show $ext_((%,%))^(%)#((%)))
@@ -136,11 +136,11 @@ def $relop(Fnn, GT, fN_1, fN_2) = $fgt($size(Fnn), fN_1, fN_2)
 def $relop(Fnn, LE, fN_1, fN_2) = $fle($size(Fnn), fN_1, fN_2)
 def $relop(Fnn, GE, fN_1, fN_2) = $fge($size(Fnn), fN_1, fN_2)
 
-def $cvtop(I32, I64, CONVERT, sx, iN) = $ext(32, 64, sx, iN)
-def $cvtop(I64, I32, CONVERT, sx?, iN) = $wrap(64, 32, iN)
-def $cvtop(Fnn, Inn, CONVERT, sx, fN) = $trunc($size(Fnn), $size(Inn), sx, fN)
-def $cvtop(F32, F64, CONVERT, sx?, fN) = $promote(32, 64, fN)
-def $cvtop(F64, F32, CONVERT, sx?, fN) = $demote(64, 32, fN)
-def $cvtop(Inn, Fnn, CONVERT, sx, iN) = $convert($size(Inn), $size(Fnn), sx, iN)
-def $cvtop(Inn, Fnn, REINTERPRET, sx?, iN) = $reinterpret(Inn, Fnn, iN) -- if $size(Inn) = $size(Fnn)
-def $cvtop(Fnn, Inn, REINTERPRET, sx?, fN) = $reinterpret(Fnn, Inn, fN) -- if $size(Inn) = $size(Fnn)
+def $cvtop(I32, I64, EXTEND sx, iN) = $ext(32, 64, sx, iN)
+def $cvtop(I64, I32, WRAP, iN) = $wrap(64, 32, iN)
+def $cvtop(Fnn, Inn, TRUNC sx, fN) = $trunc($size(Fnn), $size(Inn), sx, fN)
+def $cvtop(F32, F64, PROMOTE, fN) = $promote(32, 64, fN)
+def $cvtop(F64, F32, DEMOTE, fN) = $demote(64, 32, fN)
+def $cvtop(Inn, Fnn, CONVERT sx, iN) = $convert($size(Inn), $size(Fnn), sx, iN)
+def $cvtop(Inn, Fnn, REINTERPRET, iN) = $reinterpret(Inn, Fnn, iN) -- if $size(Inn) = $size(Fnn)
+def $cvtop(Fnn, Inn, REINTERPRET, fN) = $reinterpret(Fnn, Inn, fN) -- if $size(Inn) = $size(Fnn)

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

@@ -229,8 +229,7 @@ rule Instr_ok/cvtop-reinterpret:
   -- if $size(nt_1) = $size(nt_2)
 
 rule Instr_ok/cvtop-convert:
-  C |- CVTOP nt_1 nt_2 CONVERT sx? : nt_2 -> nt_1
-  -- if sx? = eps <=> nt_1 = Inn_1 /\ nt_2 = Inn_2 /\ $size(nt_1) > $size(nt_2) \/ nt_1 = Fnn_1 /\ nt_2 = Fnn_2
+  C |- CVTOP nt_1 nt_2 cvtop : nt_2 -> nt_1
 
 
 ;; Local instructions

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

@@ -193,12 +193,12 @@ rule Step_pure/relop:
 
 
 rule Step_pure/cvtop-val:
-  (CONST t_1 c_1) (CVTOP t_2 t_1 cvtop sx?)  ~>  (CONST t_2 c)
-  -- if $cvtop(t_1, t_2, cvtop, sx?, c_1) = c  ;; TODO
+  (CONST t_1 c_1) (CVTOP t_2 t_1 cvtop)  ~>  (CONST t_2 c)
+  -- if $cvtop(t_1, t_2, cvtop, c_1) = c  ;; TODO
 
 rule Step_pure/cvtop-trap:
-  (CONST t_1 c_1) (CVTOP t_2 t_1 cvtop sx?)  ~>  TRAP
-  -- if $cvtop(t_1, t_2, cvtop, sx?, c_1) = eps  ;; TODO
+  (CONST t_1 c_1) (CVTOP t_2 t_1 cvtop)  ~>  TRAP
+  -- if $cvtop(t_1, t_2, cvtop, c_1) = eps  ;; TODO
 
 
 ;; Local instructions

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

@@ -355,29 +355,28 @@ grammar Binstr/numeric-bin-f64 : instr = ...
   | 0xA6 => BINOP F64 COPYSIGN
   | ...
 
-
 grammar Binstr/numeric-cvt : instr = ...
-  | 0xA7 => CVTOP I32 I64 CONVERT
-  | 0xA8 => CVTOP I32 F32 CONVERT S
-  | 0xA9 => CVTOP I32 F32 CONVERT U
-  | 0xAA => CVTOP I32 F64 CONVERT S
-  | 0xAB => CVTOP I32 F64 CONVERT U
-  | 0xAC => CVTOP I64 I32 CONVERT S
-  | 0xAD => CVTOP I64 I32 CONVERT U
-  | 0xAE => CVTOP I64 F32 CONVERT S
-  | 0xAF => CVTOP I64 F32 CONVERT U
-  | 0xB0 => CVTOP I64 F64 CONVERT S
-  | 0xB1 => CVTOP I64 F64 CONVERT U
-  | 0xB2 => CVTOP F32 I32 CONVERT S
-  | 0xB3 => CVTOP F32 I32 CONVERT U
-  | 0xB4 => CVTOP F32 I64 CONVERT S
-  | 0xB5 => CVTOP F32 I64 CONVERT U
-  | 0xB6 => CVTOP F32 F64 CONVERT
-  | 0xB7 => CVTOP F64 I32 CONVERT S
-  | 0xB8 => CVTOP F64 I32 CONVERT U
-  | 0xB9 => CVTOP F64 I64 CONVERT S
-  | 0xBA => CVTOP F64 I64 CONVERT U
-  | 0xBB => CVTOP F64 F32 CONVERT
+  | 0xA7 => CVTOP I32 I64 WRAP
+  | 0xA8 => CVTOP I32 F32 (TRUNC S)
+  | 0xA9 => CVTOP I32 F32 (TRUNC U)
+  | 0xAA => CVTOP I32 F64 (TRUNC S)
+  | 0xAB => CVTOP I32 F64 (TRUNC U)
+  | 0xAC => CVTOP I64 I32 (EXTEND S)
+  | 0xAD => CVTOP I64 I32 (EXTEND U)
+  | 0xAE => CVTOP I64 F32 (TRUNC S)
+  | 0xAF => CVTOP I64 F32 (TRUNC U)
+  | 0xB0 => CVTOP I64 F64 (TRUNC S)
+  | 0xB1 => CVTOP I64 F64 (TRUNC U)
+  | 0xB2 => CVTOP F32 I32 (CONVERT S)
+  | 0xB3 => CVTOP F32 I32 (CONVERT U)
+  | 0xB4 => CVTOP F32 I64 (CONVERT S)
+  | 0xB5 => CVTOP F32 I64 (CONVERT U)
+  | 0xB6 => CVTOP F32 F64 DEMOTE
+  | 0xB7 => CVTOP F64 I32 (CONVERT S)
+  | 0xB8 => CVTOP F64 I32 (CONVERT U)
+  | 0xB9 => CVTOP F64 I64 (CONVERT S)
+  | 0xBA => CVTOP F64 I64 (CONVERT U)
+  | 0xBB => CVTOP F32 F64 PROMOTE
   | 0xBC => CVTOP I32 F32 REINTERPRET
   | 0xBD => CVTOP I64 F64 REINTERPRET
   | 0xBE => CVTOP F32 I32 REINTERPRET

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

@@ -257,7 +257,15 @@ syntax relop_(Inn) =
 syntax relop_(Fnn) =
   | EQ | NE | LT | GT | LE | GE
 
-syntax cvtop = CONVERT | CONVERT_SAT | REINTERPRET
+syntax cvtop =
+  | EXTEND sx
+  | WRAP
+  | CONVERT sx
+  | TRUNC sx
+  | TRUNC_SAT sx
+  | PROMOTE
+  | DEMOTE
+  | REINTERPRET
 
 
 ;; Vector operators
@@ -382,7 +390,7 @@ syntax instr/num hint(desc "numeric instruction") = ...
   | BINOP numtype binop_(numtype)    hint(show %.%)
   | TESTOP numtype testop_(numtype)  hint(show %.%)
   | RELOP numtype relop_(numtype)    hint(show %.%)
-  | CVTOP numtype_1 numtype_2 cvtop sx?  hint(show %1.%3#_#%2#_#%4) hint(show %1.%3#_#%2)
+  | CVTOP numtype_1 numtype_2 cvtop  hint(show %1.%3#_#%2)
     -- if numtype_1 =/= numtype_2
   | EXTEND numtype n                 hint(show %.EXTEND#%#_#S)
   | ...

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

@@ -27,8 +27,8 @@ def $testop(numtype, testop_(numtype), num_(numtype)) : num_(I32)
     hint(show %2#$_(%1)#((%3)))
 def $relop(numtype, relop_(numtype), num_(numtype), num_(numtype)) : num_(I32)
     hint(show %2#$_(%1)#(%3, %4))
-def $cvtop(numtype_1, numtype_2, cvtop, sx?, num_(numtype_1)) : num_(numtype_2)*
-    hint(show %3#$_((%1,%2))^(%4)#((%5)))
+def $cvtop(numtype_1, numtype_2, cvtop, num_(numtype_1)) : num_(numtype_2)*
+    hint(show %3#$_((%1,%2))#((%4)))
 
 def $wrap(M, N, iN(M)) : iN(N)                      hint(show $wrap_((%,%))#((%)))
 def $ext(M, N, sx, iN(M)) : iN(N)                   hint(show $ext_((%,%))^(%)#((%)))
@@ -162,15 +162,15 @@ def $relop(Fnn, GT, fN_1, fN_2) = $fgt($size(Fnn), fN_1, fN_2)
 def $relop(Fnn, LE, fN_1, fN_2) = $fle($size(Fnn), fN_1, fN_2)
 def $relop(Fnn, GE, fN_1, fN_2) = $fge($size(Fnn), fN_1, fN_2)
 
-def $cvtop(I32, I64, CONVERT, sx, iN) = $ext(32, 64, sx, iN)
-def $cvtop(I64, I32, CONVERT, sx?, iN) = $wrap(64, 32, iN)
-def $cvtop(Fnn, Inn, CONVERT, sx, fN) = $trunc($size(Fnn), $size(Inn), sx, fN)
-def $cvtop(Fnn, Inn, CONVERT_SAT, sx, fN) = $trunc_sat($size(Fnn), $size(Inn), sx, fN)
-def $cvtop(F32, F64, CONVERT, sx?, fN) = $promote(32, 64, fN)
-def $cvtop(F64, F32, CONVERT, sx?, fN) = $demote(64, 32, fN)
-def $cvtop(Inn, Fnn, CONVERT, sx, iN) = $convert($size(Inn), $size(Fnn), sx, iN)
-def $cvtop(Inn, Fnn, CONVERT, sx?, iN) = $reinterpret(Inn, Fnn, iN) -- if $size(Inn) = $size(Fnn)
-def $cvtop(Fnn, Inn, CONVERT, sx?, fN) = $reinterpret(Fnn, Inn, fN) -- if $size(Inn) = $size(Fnn)
+def $cvtop(I32, I64, EXTEND sx, iN) = $ext(32, 64, sx, iN)
+def $cvtop(I64, I32, WRAP, iN) = $wrap(64, 32, iN)
+def $cvtop(Fnn, Inn, TRUNC sx, fN) = $trunc($size(Fnn), $size(Inn), sx, fN)
+def $cvtop(Fnn, Inn, TRUNC_SAT sx, fN) = $trunc_sat($size(Fnn), $size(Inn), sx, fN)
+def $cvtop(F32, F64, PROMOTE, fN) = $promote(32, 64, fN)
+def $cvtop(F64, F32, DEMOTE, fN) = $demote(64, 32, fN)
+def $cvtop(Inn, Fnn, CONVERT sx, iN) = $convert($size(Inn), $size(Fnn), sx, iN)
+def $cvtop(Inn, Fnn, REINTERPRET, iN) = $reinterpret(Inn, Fnn, iN) -- if $size(Inn) = $size(Fnn)
+def $cvtop(Fnn, Inn, REINTERPRET, fN) = $reinterpret(Fnn, Inn, fN) -- if $size(Inn) = $size(Fnn)
 
 
 ;; Packed values

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

@@ -273,8 +273,7 @@ rule Instr_ok/cvtop-reinterpret:
   -- if $size(nt_1) = $size(nt_2)
 
 rule Instr_ok/cvtop-convert:
-  C |- CVTOP nt_1 nt_2 CONVERT sx? : nt_2 -> nt_1
-  -- if sx? = eps <=> nt_1 = Inn_1 /\ nt_2 = Inn_2 /\ $size(nt_1) > $size(nt_2) \/ nt_1 = Fnn_1 /\ nt_2 = Fnn_2
+  C |- CVTOP nt_1 nt_2 cvtop : nt_2 -> nt_1
 
 
 ;; Reference instructions

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

@@ -199,12 +199,12 @@ rule Step_pure/relop:
 
 
 rule Step_pure/cvtop-val:
-  (CONST nt_1 c_1) (CVTOP nt_2 nt_1 cvtop sx?)  ~>  (CONST nt_2 c)
-  -- if $cvtop(nt_1, nt_2, cvtop, sx?, c_1) = c  ;; TODO
+  (CONST nt_1 c_1) (CVTOP nt_2 nt_1 cvtop)  ~>  (CONST nt_2 c)
+  -- if $cvtop(nt_1, nt_2, cvtop, c_1) = c  ;; TODO
 
 rule Step_pure/cvtop-trap:
-  (CONST nt_1 c_1) (CVTOP nt_2 nt_1 cvtop sx?)  ~>  TRAP
-  -- if $cvtop(nt_1, nt_2, cvtop, sx?, c_1) = eps  ;; TODO
+  (CONST nt_1 c_1) (CVTOP nt_2 nt_1 cvtop)  ~>  TRAP
+  -- if $cvtop(nt_1, nt_2, cvtop, c_1) = eps  ;; TODO
 
 
 ;; Reference instructions

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

@@ -399,35 +399,45 @@ grammar Binstr/numeric-bin-f64 : instr = ...
   | 0xA6 => BINOP F64 COPYSIGN
   | ...
 
-
 grammar Binstr/numeric-cvt : instr = ...
-  | 0xA7 => CVTOP I32 I64 CONVERT
-  | 0xA8 => CVTOP I32 F32 CONVERT S
-  | 0xA9 => CVTOP I32 F32 CONVERT U
-  | 0xAA => CVTOP I32 F64 CONVERT S
-  | 0xAB => CVTOP I32 F64 CONVERT U
-  | 0xAC => CVTOP I64 I32 CONVERT S
-  | 0xAD => CVTOP I64 I32 CONVERT U
-  | 0xAE => CVTOP I64 F32 CONVERT S
-  | 0xAF => CVTOP I64 F32 CONVERT U
-  | 0xB0 => CVTOP I64 F64 CONVERT S
-  | 0xB1 => CVTOP I64 F64 CONVERT U
-  | 0xB2 => CVTOP F32 I32 CONVERT S
-  | 0xB3 => CVTOP F32 I32 CONVERT U
-  | 0xB4 => CVTOP F32 I64 CONVERT S
-  | 0xB5 => CVTOP F32 I64 CONVERT U
-  | 0xB6 => CVTOP F32 F64 CONVERT
-  | 0xB7 => CVTOP F64 I32 CONVERT S
-  | 0xB8 => CVTOP F64 I32 CONVERT U
-  | 0xB9 => CVTOP F64 I64 CONVERT S
-  | 0xBA => CVTOP F64 I64 CONVERT U
-  | 0xBB => CVTOP F64 F32 CONVERT
+  | 0xA7 => CVTOP I32 I64 WRAP
+  | 0xA8 => CVTOP I32 F32 (TRUNC S)
+  | 0xA9 => CVTOP I32 F32 (TRUNC U)
+  | 0xAA => CVTOP I32 F64 (TRUNC S)
+  | 0xAB => CVTOP I32 F64 (TRUNC U)
+  | 0xAC => CVTOP I64 I32 (EXTEND S)
+  | 0xAD => CVTOP I64 I32 (EXTEND U)
+  | 0xAE => CVTOP I64 F32 (TRUNC S)
+  | 0xAF => CVTOP I64 F32 (TRUNC U)
+  | 0xB0 => CVTOP I64 F64 (TRUNC S)
+  | 0xB1 => CVTOP I64 F64 (TRUNC U)
+  | 0xB2 => CVTOP F32 I32 (CONVERT S)
+  | 0xB3 => CVTOP F32 I32 (CONVERT U)
+  | 0xB4 => CVTOP F32 I64 (CONVERT S)
+  | 0xB5 => CVTOP F32 I64 (CONVERT U)
+  | 0xB6 => CVTOP F32 F64 DEMOTE
+  | 0xB7 => CVTOP F64 I32 (CONVERT S)
+  | 0xB8 => CVTOP F64 I32 (CONVERT U)
+  | 0xB9 => CVTOP F64 I64 (CONVERT S)
+  | 0xBA => CVTOP F64 I64 (CONVERT U)
+  | 0xBB => CVTOP F32 F64 PROMOTE
   | 0xBC => CVTOP I32 F32 REINTERPRET
   | 0xBD => CVTOP I64 F64 REINTERPRET
   | 0xBE => CVTOP F32 I32 REINTERPRET
   | 0xBF => CVTOP F64 I64 REINTERPRET
   | ...
 
+grammar Binstr/numeric-cvt-sat : instr = ...
+  | 0xFC 0:Bu32 => CVTOP I32 F32 (TRUNC_SAT S)
+  | 0xFC 1:Bu32 => CVTOP I32 F32 (TRUNC_SAT U)
+  | 0xFC 2:Bu32 => CVTOP I32 F64 (TRUNC_SAT S)
+  | 0xFC 3:Bu32 => CVTOP I32 F64 (TRUNC_SAT U)
+  | 0xFC 4:Bu32 => CVTOP I64 F32 (TRUNC_SAT S)
+  | 0xFC 5:Bu32 => CVTOP I64 F32 (TRUNC_SAT U)
+  | 0xFC 6:Bu32 => CVTOP I64 F64 (TRUNC_SAT S)
+  | 0xFC 7:Bu32 => CVTOP I64 F64 (TRUNC_SAT U)
+  | ...
+
 grammar Binstr/numeric-extend : instr = ...
   | 0xC0 => UNOP I32 (EXTEND 8)
   | 0xC1 => UNOP I32 (EXTEND 16)

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

@@ -365,10 +365,19 @@ syntax relop_(Fnn) =
   | EQ | NE | LT | GT | LE | GE
 
 syntax cvtop_(numtype_1, numtype_2) hint(show cvtop_((%,%)))
-syntax cvtop_(nt_1, nt_2) =
-  | CONVERT
-  | CONVERT_SAT  -- if nt_1 = Inn /\ nt_2 = Fnn
-  | REINTERPRET  -- if $size(nt_1) = $size(nt_2)
+syntax cvtop_(Inn_1, Inn_2) =
+  | EXTEND sx hint(show %0#_#%1)  -- if $sizenn1(Inn_1) < $sizenn2(Inn_2)
+  | WRAP         -- if $sizenn1(Inn_1) > $sizenn2(Inn_2)
+syntax cvtop_(Inn_1, Fnn_2) =
+  | CONVERT sx hint(show %0#_#%1)
+  | REINTERPRET  -- if $sizenn1(Inn_1) = $sizenn2(Fnn_2)
+syntax cvtop_(Fnn_1, Inn_2) =
+  | TRUNC sx hint(show %0#_#%1)
+  | TRUNC_SAT sx hint(show %0#_#%1)
+  | REINTERPRET  -- if $sizenn1(Fnn_1) = $sizenn2(Inn_2)
+syntax cvtop_(Fnn_1, Fnn_2) =
+  | PROMOTE      -- if $sizenn1(Fnn_1) < $sizenn2(Fnn_2)
+  | DEMOTE       -- if $sizenn1(Fnn_1) > $sizenn2(Fnn_2)
 
 
 ;; Vector operators
@@ -514,9 +523,7 @@ syntax instr/num hint(desc "numeric instruction") = ...
   | BINOP numtype binop_(numtype)    hint(show %.##%)
   | TESTOP numtype testop_(numtype)  hint(show %.##%)
   | RELOP numtype relop_(numtype)    hint(show %.##%)
-  | CVTOP numtype_1 numtype_2 cvtop_(numtype_2, numtype_1) sx?  hint(show %1.%3#_#%2) hint(show %1.%3#_#%2#_#%4)
-    -- if numtype_1 =/= numtype_2
-    ;; TODO(1, rossberg): constrain sx? or move it into cvtop
+  | CVTOP numtype_1 numtype_2 cvtop_(numtype_2, numtype_1)  hint(show %1.##%3#_#%2)
   | ...
 
 syntax instr/vec hint(desc "vector instruction") = ...

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

@@ -357,7 +357,7 @@ def $free_instr(UNOP numtype unop) = $free_numtype(numtype)
 def $free_instr(BINOP numtype binop) = $free_numtype(numtype)
 def $free_instr(TESTOP numtype testop) = $free_numtype(numtype)
 def $free_instr(RELOP numtype relop) = $free_numtype(numtype)
-def $free_instr(CVTOP numtype_1 numtype_2 cvtop sx?) =
+def $free_instr(CVTOP numtype_1 numtype_2 cvtop) =
   $free_numtype(numtype_1) ++ $free_numtype(numtype_2)
 
 def $free_instr(VCONST vectype veclit) = $free_vectype(vectype)

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

@@ -19,6 +19,7 @@ def $invsigned(N, i) = j        -- if $signed(N, j) = i
 
 ;; TODO(3, all): implement numerics internally
 
+;; TODO(2, rossberg): show as function ids, not var ids
 def $unop(numtype, unop_(numtype), num_(numtype)) : num_(numtype)*
     hint(show %2#$_(%1)#((%3)))
 def $binop(numtype, binop_(numtype), num_(numtype), num_(numtype)) : num_(numtype)*
@@ -27,8 +28,8 @@ def $testop(numtype, testop_(numtype), num_(numtype)) : num_(I32)
     hint(show %2#$_(%1)#((%3)))
 def $relop(numtype, relop_(numtype), num_(numtype), num_(numtype)) : num_(I32)
     hint(show %2#$_(%1)#(%3, %4))
-def $cvtop(numtype_1, numtype_2, cvtop_(numtype_1, numtype_2), sx?, num_(numtype_1)) : num_(numtype_2)*
-    hint(show %3#$_((%1,%2))^(%4)#((%5)))
+def $cvtop(numtype_1, numtype_2, cvtop_(numtype_1, numtype_2), num_(numtype_1)) : num_(numtype_2)*
+    hint(show %3#$_((%1,%2))#((%4)))
 
 def $wrap(M, N, iN(M)) : iN(N)                      hint(show $wrap_((%,%))#((%)))
 def $ext(M, N, sx, iN(M)) : iN(N)                   hint(show $ext_((%,%))^(%)#((%)))
@@ -166,15 +167,15 @@ def $relop(Fnn, GT, fN_1, fN_2) = $fgt($size(Fnn), fN_1, fN_2)
 def $relop(Fnn, LE, fN_1, fN_2) = $fle($size(Fnn), fN_1, fN_2)
 def $relop(Fnn, GE, fN_1, fN_2) = $fge($size(Fnn), fN_1, fN_2)
 
-def $cvtop(I32, I64, CONVERT, sx, iN) = $ext(32, 64, sx, iN)
-def $cvtop(I64, I32, CONVERT, sx?, iN) = $wrap(64, 32, iN)
-def $cvtop(Fnn, Inn, CONVERT, sx, fN) = $trunc($size(Fnn), $size(Inn), sx, fN)
-def $cvtop(Fnn, Inn, CONVERT_SAT, sx, fN) = $trunc_sat($size(Fnn), $size(Inn), sx, fN)
-def $cvtop(F32, F64, CONVERT, sx?, fN) = $promote(32, 64, fN)
-def $cvtop(F64, F32, CONVERT, sx?, fN) = $demote(64, 32, fN)
-def $cvtop(Inn, Fnn, CONVERT, sx, iN) = $convert($size(Inn), $size(Fnn), sx, iN)
-def $cvtop(Inn, Fnn, REINTERPRET, sx?, iN) = $reinterpret(Inn, Fnn, iN) -- if $size(Inn) = $size(Fnn)
-def $cvtop(Fnn, Inn, REINTERPRET, sx?, fN) = $reinterpret(Fnn, Inn, fN) -- if $size(Inn) = $size(Fnn)
+def $cvtop(Inn_1, Inn_2, EXTEND sx, iN_1) = $ext($sizenn1(Inn_1), $sizenn2(Inn_2), sx, iN_1)
+def $cvtop(Inn_1, Inn_2, WRAP, iN_1) = $wrap($sizenn1(Inn_1), $sizenn2(Inn_2), iN_1)
+def $cvtop(Fnn_1, Inn_2, TRUNC sx, fN_1) = $trunc($sizenn1(Fnn_1), $sizenn2(Inn_2), sx, fN_1)
+def $cvtop(Fnn_1, Inn_2, TRUNC_SAT sx, fN_1) = $trunc_sat($sizenn1(Fnn_1), $sizenn2(Inn_2), sx, fN_1)
+def $cvtop(Inn_1, Fnn_2, CONVERT sx, iN_1) = $convert($sizenn1(Inn_1), $sizenn2(Fnn_2), sx, iN_1)
+def $cvtop(Fnn_1, Fnn_2, PROMOTE, fN_1) = $promote($sizenn1(Fnn_1), $sizenn2(Fnn_2), fN_1)
+def $cvtop(Fnn_1, Fnn_2, DEMOTE, fN_1) = $demote($sizenn1(Fnn_1), $sizenn2(Fnn_2), fN_1)
+def $cvtop(Inn_1, Fnn_2, REINTERPRET, iN_1) = $reinterpret(Inn_1, Fnn_2, iN_1) -- if $sizenn1(Inn_1) = $sizenn2(Fnn_2)
+def $cvtop(Fnn_1, Inn_2, REINTERPRET, fN_1) = $reinterpret(Fnn_1, Inn_2, fN_1) -- if $sizenn1(Inn_1) = $sizenn2(Fnn_2)
 
 
 ;; Packed numbers