Update test expectations

Wasm-DSL · May 30, 2024 · f27e5d0 · f27e5d0
1 parent 8fb06d0
commit f27e5d0
Show file tree

Hide file tree

Showing 4 changed files with 173 additions and 74 deletions.
diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md
@@ -5778,26 +5778,26 @@ syntax pth =
 syntax T = nat
 
 ;; C-conventions.watsup
-relation Premise: `%`(nat)
+relation NotationTypingPremise: `%`(nat)
 
 ;; C-conventions.watsup
-relation Premisedots: `...`
+relation NotationTypingPremisedots: `...`
 
 ;; C-conventions.watsup
-relation Scheme: `%`(nat)
+relation NotationTypingScheme: `%`(nat)
   ;; C-conventions.watsup
   rule _{conclusion : nat, premise_1 : nat, premise_2 : nat, premise_n : nat}:
     `%`(conclusion)
-    -- Premise: `%`(premise_1)
-    -- Premise: `%`(premise_2)
-    -- Premisedots: `...`
-    -- Premise: `%`(premise_n)
+    -- NotationTypingPremise: `%`(premise_1)
+    -- NotationTypingPremise: `%`(premise_2)
+    -- NotationTypingPremisedots: `...`
+    -- NotationTypingPremise: `%`(premise_n)
 
 ;; C-conventions.watsup
 rec {
 
-;; C-conventions.watsup:38.1-38.68
-relation InstrScheme: `%|-%:%`(context, instr*, functype)
+;; C-conventions.watsup:38.1-38.82
+relation NotationTypingInstrScheme: `%|-%:%`(context, instr*, functype)
   ;; C-conventions.watsup:40.1-41.38
   rule i32.add{C : context}:
     `%|-%:%`(C, [BINOP_instr(I32_numtype, ADD_binop_)], `%->%`_functype(`%`_resulttype([I32_valtype I32_valtype]), `%`_resulttype([I32_valtype])))
@@ -5807,13 +5807,27 @@ relation InstrScheme: `%|-%:%`(context, instr*, functype)
     `%|-%:%`(C, [GLOBAL.GET_instr(x)], `%->%`_functype(`%`_resulttype([]), `%`_resulttype([t])))
     -- if (C.GLOBALS_context[x!`%`_idx.0] = `%%`_globaltype(mut, t))
 
-  ;; C-conventions.watsup:47.1-50.60
+  ;; C-conventions.watsup:47.1-50.74
   rule block{C : context, blocktype : blocktype, instr* : instr*, t_1* : valtype*, t_2* : valtype*}:
     `%|-%:%`(C, [BLOCK_instr(blocktype, instr*{instr : instr})], `%->%`_functype(`%`_resulttype(t_1*{t_1 : valtype}), `%`_resulttype(t_2*{t_2 : valtype})))
     -- Blocktype_ok: `%|-%:%`(C, blocktype, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 : valtype}), [], `%`_resulttype(t_2*{t_2 : valtype})))
-    -- InstrScheme: `%|-%:%`(C ++ {TYPES [], RECS [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [`%`_resulttype(t_2*{t_2 : valtype})], RETURN ?()}, instr*{instr : instr}, `%->%`_functype(`%`_resulttype(t_1*{t_1 : valtype}), `%`_resulttype(t_2*{t_2 : valtype})))
+    -- NotationTypingInstrScheme: `%|-%:%`(C ++ {TYPES [], RECS [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [`%`_resulttype(t_2*{t_2 : valtype})], RETURN ?()}, instr*{instr : instr}, `%->%`_functype(`%`_resulttype(t_1*{t_1 : valtype}), `%`_resulttype(t_2*{t_2 : valtype})))
 }
 
+;; C-conventions.watsup
+relation NotationReduct: `~>%`(instr*)
+  ;; C-conventions.watsup
+  rule 2{q_1 : num_(F64_numtype), q_4 : num_(F64_numtype), q_3 : num_(F64_numtype)}:
+    `~>%`([CONST_instr(F64_numtype, q_1) CONST_instr(F64_numtype, q_4) CONST_instr(F64_numtype, q_3) BINOP_instr(F64_numtype, ADD_binop_) BINOP_instr(F64_numtype, MUL_binop_)])
+
+  ;; C-conventions.watsup
+  rule 3{q_1 : num_(F64_numtype), q_5 : num_(F64_numtype)}:
+    `~>%`([CONST_instr(F64_numtype, q_1) CONST_instr(F64_numtype, q_5) BINOP_instr(F64_numtype, MUL_binop_)])
+
+  ;; C-conventions.watsup
+  rule 4{q_6 : num_(F64_numtype)}:
+    `~>%`([CONST_instr(F64_numtype, q_6)])
+
 == IL Validation...
 == Complete.
 ```
diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md
@@ -8915,7 +8915,7 @@ $$
 {\mathit{premise}}_n
 }{
 {\mathit{conclusion}}
-} \, {[\textsc{\scriptsize Scheme}]}
+} \, {[\textsc{\scriptsize NotationTypingScheme}]}
 \qquad
 \end{array}
 $$
@@ -8927,7 +8927,7 @@ $$
 \frac{
 }{
 C \vdash \mathsf{i{\scriptstyle 32}} {.} \mathsf{add} : \mathsf{i{\scriptstyle 32}}~\mathsf{i{\scriptstyle 32}} \rightarrow \mathsf{i{\scriptstyle 32}}
-} \, {[\textsc{\scriptsize InstrScheme{-}i32.add}]}
+} \, {[\textsc{\scriptsize NotationTypingInstrScheme{-}i32.add}]}
 \qquad
 \end{array}
 $$
@@ -8938,7 +8938,7 @@ $$
 C{.}\mathsf{globals}{}[x] = {\mathsf{mut}^?}~t
 }{
 C \vdash \mathsf{global.get}~x : \epsilon \rightarrow t
-} \, {[\textsc{\scriptsize InstrScheme{-}global.get}]}
+} \, {[\textsc{\scriptsize NotationTypingInstrScheme{-}global.get}]}
 \qquad
 \end{array}
 $$
@@ -8951,10 +8951,22 @@ C \vdash {\mathit{blocktype}} : {t_1^\ast} \rightarrow {t_2^\ast}
 C, \mathsf{labels}~({t_2^\ast}) \vdash {{\mathit{instr}}^\ast} : {t_1^\ast} \rightarrow {t_2^\ast}
 }{
 C \vdash \mathsf{block}~{\mathit{blocktype}}~{{\mathit{instr}}^\ast} : {t_1^\ast} \rightarrow {t_2^\ast}
-} \, {[\textsc{\scriptsize InstrScheme{-}block}]}
+} \, {[\textsc{\scriptsize NotationTypingInstrScheme{-}block}]}
 \qquad
 \end{array}
 $$
 
+\vspace{1ex}
+
+$\boxed{{ \hookrightarrow }\;{{\mathit{instr}}^\ast}}$
+
+$$
+\begin{array}{@{}l@{}rcl@{}l@{}}
+{[\textsc{\scriptsize NotationReduct{-}2}]} \quad &  &\hookrightarrow& (\mathsf{f{\scriptstyle 64}}{.}\mathsf{const}~q_1)~(\mathsf{f{\scriptstyle 64}}{.}\mathsf{const}~q_4)~(\mathsf{f{\scriptstyle 64}}{.}\mathsf{const}~q_3)~\mathsf{f{\scriptstyle 64}} {.} \mathsf{add}~\mathsf{f{\scriptstyle 64}} {.} \mathsf{mul} \\
+{[\textsc{\scriptsize NotationReduct{-}3}]} \quad &  &\hookrightarrow& (\mathsf{f{\scriptstyle 64}}{.}\mathsf{const}~q_1)~(\mathsf{f{\scriptstyle 64}}{.}\mathsf{const}~q_5)~\mathsf{f{\scriptstyle 64}} {.} \mathsf{mul} \\
+{[\textsc{\scriptsize NotationReduct{-}4}]} \quad &  &\hookrightarrow& (\mathsf{f{\scriptstyle 64}}{.}\mathsf{const}~q_6) \\
+\end{array}
+$$
+
 
 ```