Remove hard-coded reduction rule rendering in favour of hint

Wasm-DSL · Sep 3, 2024 · 6c58671 · 6c58671
1 parent d44abbb
commit 6c58671
Show file tree

Hide file tree

Showing 9 changed files with 53 additions and 68 deletions.
diff --git a/spectec/spec/wasm-1.0/8-reduction.watsup b/spectec/spec/wasm-1.0/8-reduction.watsup
@@ -2,10 +2,10 @@
 ;; Configurations
 ;;
 
-relation Step: config ~> config                 hint(show "E")
-relation Step_pure: admininstr* ~> admininstr*  hint(show "E")
-relation Step_read: config ~> admininstr*       hint(show "E")
-relation Steps: config ~>* config               hint(show "E")
+relation Step: config ~> config                 hint(show "E") hint(tabular)
+relation Step_pure: admininstr* ~> admininstr*  hint(show "E") hint(tabular)
+relation Step_read: config ~> admininstr*       hint(show "E") hint(tabular)
+relation Steps: config ~>* config               hint(show "E") hint(tabular)
 
 rule Step/pure:
   z; instr*  ~>  z; instr'*
@@ -26,7 +26,7 @@ rule Steps/trans:
 
 ;; Expressions
 
-relation Eval_expr: state; expr ~>* state; val*  hint(show "E-expr")
+relation Eval_expr: state; expr ~>* state; val*  hint(show "E-expr") hint(tabular)
 
 rule Eval_expr:
   z; instr*  ~>*  z'; val*

diff --git a/spectec/spec/wasm-2.0/8-reduction.watsup b/spectec/spec/wasm-2.0/8-reduction.watsup
@@ -2,10 +2,10 @@
 ;; Configurations
 ;;
 
-relation Step: config ~> config                 hint(show "E")
-relation Step_pure: admininstr* ~> admininstr*  hint(show "E")
-relation Step_read: config ~> admininstr*       hint(show "E")
-relation Steps: config ~>* config               hint(show "E")
+relation Step: config ~> config                 hint(show "E") hint(tabular)
+relation Step_pure: admininstr* ~> admininstr*  hint(show "E") hint(tabular)
+relation Step_read: config ~> admininstr*       hint(show "E") hint(tabular)
+relation Steps: config ~>* config               hint(show "E") hint(tabular)
 
 rule Step/pure:
   z; instr*  ~>  z; instr'*
@@ -26,7 +26,7 @@ rule Steps/trans:
 
 ;; Expressions
 
-relation Eval_expr: state; expr ~>* state; val*  hint(show "E-expr")
+relation Eval_expr: state; expr ~>* state; val*  hint(show "E-expr") hint(tabular)
 
 rule Eval_expr:
   z; instr*  ~>*  z'; val*

diff --git a/spectec/spec/wasm-3.0/2-syntax-aux.watsup b/spectec/spec/wasm-3.0/2-syntax-aux.watsup
@@ -647,7 +647,7 @@ def $unrolldt(DEF rectype i) = subtype*[i]               -- if $unrollrt(rectype
 
 def $expanddt(deftype) = comptype              -- if $unrolldt(deftype) = SUB fin typeuse* comptype
 
-relation Expand: deftype ~~ comptype hint(macro "%expanddt")
+relation Expand: deftype ~~ comptype hint(macro "%expanddt") hint(tabular)
 rule Expand: deftype ~~ comptype               -- if $unrolldt(deftype) = SUB fin typeuse* comptype
 
 

diff --git a/spectec/spec/wasm-3.0/8-reduction.watsup b/spectec/spec/wasm-3.0/8-reduction.watsup
@@ -2,10 +2,10 @@
 ;; Configurations
 ;;
 
-relation Step: config ~> config       hint(show "E") hint(macro "stepto")
-relation Step_pure: instr* ~> instr*  hint(show "E") hint(macro "stepto")
-relation Step_read: config ~> instr*  hint(show "E") hint(macro "stepto")
-relation Steps: config ~>* config     hint(show "E") hint(macro "steptostar")
+relation Step: config ~> config       hint(show "E") hint(macro "stepto") hint(tabular)
+relation Step_pure: instr* ~> instr*  hint(show "E") hint(macro "stepto") hint(tabular)
+relation Step_read: config ~> instr*  hint(show "E") hint(macro "stepto") hint(tabular)
+relation Steps: config ~>* config     hint(show "E") hint(macro "steptostar") hint(tabular)
 
 rule Step/pure:
   z; instr*  ~>  z; instr'*
@@ -26,7 +26,7 @@ rule Steps/trans:
 
 ;; Expressions
 
-relation Eval_expr: state; expr ~>* state; val*  hint(show "E-expr") hint(macro "steptostar")
+relation Eval_expr: state; expr ~>* state; val*  hint(show "E-expr") hint(macro "steptostar") hint(tabular)
 
 rule Eval_expr:
   z; instr*  ~>*  z'; val*

diff --git a/spectec/spec/wasm-3.0/C-conventions.watsup b/spectec/spec/wasm-3.0/C-conventions.watsup
@@ -52,7 +52,7 @@ rule NotationTypingInstrScheme/block:
 
 ;; Execution notation
 
-relation NotationReduct: ~> instr*
+relation NotationReduct: ~> instr* hint(tabular)
 
 rule NotationReduct/2:
   ~> (CONST F64 q_1) (CONST F64 q_4) (CONST F64 q_3) $($(BINOP F64 ADD)) $($(BINOP F64 MUL))

diff --git a/spectec/src/backend-latex/render.ml b/spectec/src/backend-latex/render.ml
@@ -133,6 +133,7 @@ type env =
     desc_gram : hints ref;
     deco_typ : bool;
     deco_rule : bool;
+    tab_rel : hints ref;
   }
 
 let new_env config =
@@ -155,6 +156,7 @@ let new_env config =
     desc_gram = ref Map.empty;
     deco_typ = false;
     deco_rule = false;
+    tab_rel = ref Map.empty;
   }
 
 let config env : Config.t =
@@ -222,7 +224,8 @@ let env_hintdef env hd =
     env_hints "show" env.show_gram id1 hints
   | RelH (id, hints) ->
     env_hints "macro" env.macro_rel id hints;
-    env_hints "show" env.show_rel id hints
+    env_hints "show" env.show_rel id hints;
+    env_hints "tabular" env.tab_rel id hints
   | VarH (id, hints) ->
     env_hints "macro" env.macro_var id hints;
     env_hints "show" env.show_var id hints
@@ -1402,13 +1405,13 @@ let render_ruledef env d =
   | _ -> failwith "render_ruledef"
 
 
-let render_reddef env d =
+let render_ruledef_tabular env d =
   match d.it with
   | RuleD (id1, id2, e, prems) ->
     let e1, op, e2 =
       match e.it with
       | InfixE (e1, op, e2) -> e1, op, e2
-      | _ -> error e.at "unrecognized format for reduction rule"
+      | _ -> error e.at "unrecognized format for tabular rule, infix operator expected"
     in
     render_rule_deco env "" id1 id2 " \\quad " ^ "& " ^
       render_exp env e1 ^ " &" ^ render_atom env op ^ "& " ^
@@ -1417,7 +1420,7 @@ let render_reddef env d =
         else
           render_conditions env ("\\\\\n  & \\multicolumn{3}{@{}l@{}}{\\qquad " ^
             render_exp env e2 ^ " }") "&&&" prems
-  | _ -> failwith "render_reddef"
+  | _ -> failwith "render_ruledef_tabular"
 
 let render_funcdef env d =
   match d.it with
@@ -1433,20 +1436,6 @@ let rec render_sep_defs ?(sep = " \\\\\n") ?(br = " \\\\[0.8ex]\n") f = function
   | d::ds -> f d ^ sep ^ render_sep_defs ~sep ~br f ds
 
 
-type rel_sort = TypingRel | ReductionRel
-
-let rec classify_rel e : rel_sort option =
-  match e.it with
-  | InfixE (_, {it = Turnstile; _}, _) -> Some TypingRel
-  | InfixE (_, {it = SqArrow | SqArrowStar | Approx; _}, _) -> Some ReductionRel
-  | InfixE (e1, _, e2) ->
-    (match classify_rel e1 with
-    | None -> classify_rel e2
-    | some -> some
-    )
-  | _ -> None
-
-
 let rec render_defs env = function
   | [] -> ""
   | d::ds' as ds ->
@@ -1470,18 +1459,16 @@ let rec render_defs env = function
     | RelD (_, t, _) ->
       "\\boxed{" ^ render_typ env t ^ "}" ^
       (if ds' = [] then "" else " \\; " ^ render_defs env ds')
-    | RuleD (_, _, e, _) ->
-      (match classify_rel e with
-      | Some TypingRel | None ->
+    | RuleD (id1, _, _, _) ->
+      if Map.mem id1.it !(env.tab_rel) then
+        "\\begin{array}{@{}l@{}r" ^ sp ^ "c" ^ sp ^ "l@{}l@{}}\n" ^
+          render_sep_defs (render_ruledef_tabular env) ds ^
+        "\\end{array}"
+      else
         "\\begin{array}{@{}c@{}}\\displaystyle\n" ^
           render_sep_defs ~sep:"\n\\qquad\n" ~br:"\n\\\\[3ex]\\displaystyle\n"
             (render_ruledef env) ds ^
         "\\end{array}"
-      | Some ReductionRel ->
-        "\\begin{array}{@{}l@{}r" ^ sp ^ "c" ^ sp ^ "l@{}l@{}}\n" ^
-          render_sep_defs (render_reddef env) ds ^
-        "\\end{array}"
-      )
     | DefD _ ->
       "\\begin{array}{@{}l" ^ sp ^ "c" ^ sp ^ "l@{}l@{}}\n" ^
         render_sep_defs (render_funcdef env) ds ^
@@ -1511,13 +1498,13 @@ let rec split_gramdefs gramdefs = function
     | GramD _ -> split_gramdefs (d::gramdefs) ds
     | _ -> List.rev gramdefs, d::ds
 
-let rec split_reddefs id reddefs = function
-  | [] -> List.rev reddefs, []
+let rec split_tabdefs id tabdefs = function
+  | [] -> List.rev tabdefs, []
   | d::ds ->
     match d.it with
     | RuleD (id1, _, _, _) when id1.it = id ->
-      split_reddefs id (d::reddefs) ds
-    | _ -> List.rev reddefs, d::ds
+      split_tabdefs id (d::tabdefs) ds
+    | _ -> List.rev tabdefs, d::ds
 
 let rec split_funcdefs id funcdefs = function
   | [] -> List.rev funcdefs, []
@@ -1541,16 +1528,14 @@ let rec render_script env = function
     | RelD _ ->
       "$" ^ render_def env d ^ "$\n\n" ^
       render_script env ds
-    | RuleD (id1, _, e, _) ->
-      (match classify_rel e with
-      | Some TypingRel | None ->
+    | RuleD (id1, _, _, _) ->
+      if Map.mem id1.it !(env.tab_rel) then
+        let tabdefs, ds' = split_tabdefs id1.it [d] ds in
+        "$$\n" ^ render_defs env tabdefs ^ "\n$$\n\n" ^
+        render_script env ds'
+      else
         "$$\n" ^ render_def env d ^ "\n$$\n\n" ^
         render_script env ds
-      | Some ReductionRel ->
-        let reddefs, ds' = split_reddefs id1.it [d] ds in
-        "$$\n" ^ render_defs env reddefs ^ "\n$$\n\n" ^
-        render_script env ds'
-      )
     | DefD (id, _, _, _) ->
       let funcdefs, ds' = split_funcdefs id.it [d] ds in
       "$$\n" ^ render_defs env funcdefs ^ "\n$$\n\n" ^

diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md
@@ -6210,7 +6210,7 @@ relation Step_read: `%~>%`(config, instr*)
 ;; 8-reduction.watsup
 rec {
 
-;; 8-reduction.watsup:5.1-5.74
+;; 8-reduction.watsup:5.1-5.88
 relation Step: `%~>%`(config, config)
   ;; 8-reduction.watsup:10.1-12.34
   rule pure{z : state, instr* : instr*, instr'* : instr*}:
@@ -6365,7 +6365,7 @@ relation Step: `%~>%`(config, config)
 ;; 8-reduction.watsup
 rec {
 
-;; 8-reduction.watsup:8.1-8.78
+;; 8-reduction.watsup:8.1-8.92
 relation Steps: `%~>*%`(config, config)
   ;; 8-reduction.watsup:18.1-19.26
   rule refl{z : state, instr* : instr*}:

diff --git a/spectec/test-latex/test.watsup b/spectec/test-latex/test.watsup
@@ -488,23 +488,23 @@ syntax C = {}
 
 relation Rok: C |- parent : OK
 relation Rsub: C |- parent <: parent
-relation Reval: parent; child ~> parent; child
+relation Reval: parent; child ~> parent; child hint(tabular)
 
 rule Rok: C |- AA : OK
 rule Rsub: C |- parent <: AA
 rule Reval: parent; child ~> AA; BB
 
 relation Rok_macro: C |- parent : OK                  hint(macro "%ok")
 relation Rsub_macro: C |- parent <: parent            hint(macro "%sub")
-relation Reval_macro: parent; child ~> parent; child  hint(macro "%eval")
+relation Reval_macro: parent; child ~> parent; child  hint(macro "%eval") hint(tabular)
 
 rule Rok_macro: C |- AA : OK
 rule Rsub_macro: C |- parent <: AA
 rule Reval_macro: parent; child ~> AA; BB
 
 relation Rok_nomacro: C |- parent : OK                  hint(macro none)
 relation Rsub_nomacro: C |- parent <: parent            hint(macro none)
-relation Reval_nomacro: parent; child ~> parent; child  hint(macro none)
+relation Reval_nomacro: parent; child ~> parent; child  hint(macro none) hint(tabular)
 
 rule Rok_nomacro: C |- AA : OK
 rule Rsub_nomacro: C |- parent <: AA

diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md
@@ -6200,7 +6200,7 @@ relation Step_read: `%~>%`(config, instr*)
 ;; 8-reduction.watsup
 rec {
 
-;; 8-reduction.watsup:5.1-5.74
+;; 8-reduction.watsup:5.1-5.88
 relation Step: `%~>%`(config, config)
   ;; 8-reduction.watsup:10.1-12.34
   rule pure{z : state, instr* : instr*, instr'* : instr*}:
@@ -6355,7 +6355,7 @@ relation Step: `%~>%`(config, config)
 ;; 8-reduction.watsup
 rec {
 
-;; 8-reduction.watsup:8.1-8.78
+;; 8-reduction.watsup:8.1-8.92
 relation Steps: `%~>*%`(config, config)
   ;; 8-reduction.watsup:18.1-19.26
   rule refl{z : state, instr* : instr*}:
@@ -14510,7 +14510,7 @@ relation Step_read: `%~>%`(config, instr*)
 ;; 8-reduction.watsup
 rec {
 
-;; 8-reduction.watsup:5.1-5.74
+;; 8-reduction.watsup:5.1-5.88
 relation Step: `%~>%`(config, config)
   ;; 8-reduction.watsup:10.1-12.34
   rule pure{z : state, instr* : instr*, instr'* : instr*}:
@@ -14665,7 +14665,7 @@ relation Step: `%~>%`(config, config)
 ;; 8-reduction.watsup
 rec {
 
-;; 8-reduction.watsup:8.1-8.78
+;; 8-reduction.watsup:8.1-8.92
 relation Steps: `%~>*%`(config, config)
   ;; 8-reduction.watsup:18.1-19.26
   rule refl{z : state, instr* : instr*}:
@@ -22820,7 +22820,7 @@ relation Step_read: `%~>%`(config, instr*)
 ;; 8-reduction.watsup
 rec {
 
-;; 8-reduction.watsup:5.1-5.74
+;; 8-reduction.watsup:5.1-5.88
 relation Step: `%~>%`(config, config)
   ;; 8-reduction.watsup:10.1-12.34
   rule pure{z : state, instr* : instr*, instr'* : instr*}:
@@ -22975,7 +22975,7 @@ relation Step: `%~>%`(config, config)
 ;; 8-reduction.watsup
 rec {
 
-;; 8-reduction.watsup:8.1-8.78
+;; 8-reduction.watsup:8.1-8.92
 relation Steps: `%~>*%`(config, config)
   ;; 8-reduction.watsup:18.1-19.26
   rule refl{z : state, instr* : instr*}:
@@ -31316,7 +31316,7 @@ relation Step_read: `%~>%`(config, instr*)
 ;; 8-reduction.watsup
 rec {
 
-;; 8-reduction.watsup:5.1-5.74
+;; 8-reduction.watsup:5.1-5.88
 relation Step: `%~>%`(config, config)
   ;; 8-reduction.watsup:10.1-12.34
   rule pure{z : state, instr* : instr*, instr'* : instr*}:
@@ -31478,7 +31478,7 @@ relation Step: `%~>%`(config, config)
 ;; 8-reduction.watsup
 rec {
 
-;; 8-reduction.watsup:8.1-8.78
+;; 8-reduction.watsup:8.1-8.92
 relation Steps: `%~>*%`(config, config)
   ;; 8-reduction.watsup:18.1-19.26
   rule refl{z : state, instr* : instr*}: