[spectec] Support hints on rules

Author: rossberg

spectec/doc/example/output/NanoWasm.pdf

@@ -232,6 +232,8 @@ let env_hintdef env hd =
     env_hints "show" env.show_rel id hints;
     env_hints "name" env.name_rel id hints;
     env_hints "tabular" env.tab_rel id hints
+  | RuleH (_id1, _id2, _hints) ->
+    ()
   | VarH (id, hints) ->
     env_hints "macro" env.macro_var id hints;
     env_hints "show" env.show_var id hints
@@ -1768,7 +1770,7 @@ let render_gramdef env d : row list =
 
 let render_ruledef_infer env d =
   match d.it with
-  | RuleD (id1, _ps, id2, e, prems) ->
+  | RuleD (id1, _ps, id2, e, prems, _hints) ->
     let prems' = filter_nl_list (function {it = VarPr _; _} -> false | _ -> true) prems in
     "\\frac{\n" ^
       (if has_nl prems then "\\begin{array}{@{}c@{}}\n" else "") ^
@@ -1782,7 +1784,7 @@ let render_ruledef_infer env d =
 
 let render_ruledef env d : row list =
   match d.it with
-  | RuleD (id1, _ps, id2, e, prems) ->
+  | RuleD (id1, _ps, id2, e, prems, _hints) ->
     let e1, op, e2 =
       match e.it with
       | InfixE (e1, op, ({it = SeqE (e21::es22); _} as e2)) when Atom.is_sub op ->
@@ -1848,7 +1850,7 @@ let rec render_defs env = function
     | RelD (_, _ps, t, _) ->
       "\\boxed{" ^ render_typ env t ^ "}" ^
       (if ds' = [] then "" else " \\; " ^ render_defs env ds')
-    | RuleD (id1, _, _, _, _) ->
+    | RuleD (id1, _, _, _, _, _) ->
       if Map.mem id1.it !(env.tab_rel) then
         (* Columns: decorator & lhs & op & rhs & premise *)
         let sp_deco = if env.deco_rule then sp else "@{}" in
@@ -1892,7 +1894,7 @@ let rec split_tabdefs id tabdefs = function
   | [] -> List.rev tabdefs, []
   | d::ds ->
     match d.it with
-    | RuleD (id1, _, _, _, _) when id1.it = id ->
+    | RuleD (id1, _, _, _, _, _) when id1.it = id ->
       split_tabdefs id (d::tabdefs) ds
     | _ -> List.rev tabdefs, d::ds
 
@@ -1918,7 +1920,7 @@ let rec render_script env = function
     | RelD _ ->
       "$" ^ render_def env d ^ "$\n\n" ^
       render_script env ds
-    | RuleD (id1, _, _, _, _) ->
+    | 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" ^

spectec/src/backend-latex/render.ml

@@ -87,7 +87,7 @@ let env_def env def =
     env.gram <- Map.add id1.it {grammar with gfragments} env.gram
   | RelD (id, _, _, _) ->
     env.rel <- Map.add id.it {rdef = def; rules = []} env.rel
-  | RuleD (id1, _, id2, _, _) ->
+  | RuleD (id1, _, id2, _, _, _) ->
     let relation = Map.find id1.it env.rel in
     let rules = relation.rules @ [(id2.it, def, ref 0)] in
     env.rel <- Map.add id1.it {relation with rules} env.rel

spectec/src/backend-splice/splice.ml

@@ -174,7 +174,7 @@ and def' =
   | TypD of id * id * arg list * typ * hint list   (* `syntax` typid args hint* `=` typ *)
   | GramD of id * id * param list * typ * gram * hint list (* `grammar` gramid params hint* `:` type `=` gram *)
   | RelD of id * param list * typ * hint list              (* `relation` relid params `:` typ hint* *)
-  | RuleD of id * param list * id * exp * prem nl_list     (* `rule` relid params ruleid? `:` exp (`--` prem)* *)
+  | RuleD of id * param list * id * exp * prem nl_list * hint list (* `rule` relid params ruleid? `:` exp (`--` prem)* *)
   | VarD of id * typ * hint list                   (* `var` varid `:` typ *)
   | DecD of id * param list * typ * hint list      (* `def` `$` defid params `:` typ hint* *)
   | DefD of id * arg list * exp * prem nl_list     (* `def` `$` defid args `=` exp (`--` prem)* *)
@@ -195,6 +195,7 @@ and hintdef' =
   | TypH of id * id * hint list
   | GramH of id * id * hint list
   | RelH of id * hint list
+  | RuleH of id * id * hint list
   | VarH of id * hint list
   | DecH of id * hint list
 

spectec/src/el/ast.ml

@@ -173,7 +173,7 @@ let free_def d =
   | VarD (_id, t, _hints) -> free_typ t
   | SepD -> empty
   | RelD (_id, ps, t, _hints) -> free_typ t -- bound_params ps
-  | RuleD (id1, ps, _id2, e, prems) ->
+  | RuleD (id1, ps, _id2, e, prems, _hints) ->
     free_relid id1 ++ (free_exp e ++ free_prems prems -- bound_params ps)
   | DecD (_id, ps, t, _hints) ->
     free_params ps ++ free_typ t -- bound_params ps

spectec/src/el/free.ml

@@ -225,6 +225,7 @@ let hintdef d =
   | TypH (x1, x2, hs) -> typid x1; ruleid x2; hints hs
   | GramH (x1, x2, hs) -> gramid x1; ruleid x2; hints hs
   | RelH (x, hs) -> relid x; hints hs
+  | RuleH (x1, x2, hs) -> relid x1; ruleid x2; hints hs
   | VarH (x, hs) -> varid x; hints hs
   | DecH (x, hs) -> defid x; hints hs
 
@@ -237,7 +238,7 @@ let def d =
   | VarD (x, t, hs) -> varid x; typ t; hints hs
   | SepD -> ()
   | RelD (x, ps, t, hs) -> relid x; params ps; typ t; hints hs
-  | RuleD (x1, ps, x2, e, prs) -> relid x1; params ps; ruleid x2; exp e; prems prs
+  | RuleD (x1, ps, x2, e, prs, hs) -> relid x1; params ps; ruleid x2; exp e; prems prs; hints hs
   | DecD (x, ps, t, hs) -> defid x; params ps; typ t; hints hs
   | DefD (x, as_, e, prs) -> defid x; args as_; exp e; prems prs
   | HintD hd -> hintdef hd
@@ -389,6 +390,7 @@ let clone_hintdef d =
   | TypH (x1, x2, hs) -> TypH (x1, x2, List.map clone_hint hs)
   | GramH (x1, x2, hs) -> GramH (x1, x2, List.map clone_hint hs)
   | RelH (x, hs) -> RelH (x, List.map clone_hint hs)
+  | RuleH (x1, x2, hs) -> RuleH (x1, x2, List.map clone_hint hs)
   | VarH (x, hs) -> VarH (x, List.map clone_hint hs)
   | DecH (x, hs) -> DecH (x, List.map clone_hint hs)
   ) $ d.at
@@ -401,7 +403,7 @@ let clone_def d =
   | VarD (x, t, hs) -> VarD (x, clone_typ t, List.map clone_hint hs)
   | SepD -> SepD
   | RelD (x, ps, t, hs) -> RelD (x, List.map clone_param ps, clone_typ t, List.map clone_hint hs)
-  | RuleD (x1, ps, x2, e, prs) -> RuleD (x1, List.map clone_param ps, x2, clone_exp e, Convert.map_nl_list clone_prem prs)
+  | RuleD (x1, ps, x2, e, prs, hs) -> RuleD (x1, List.map clone_param ps, x2, clone_exp e, Convert.map_nl_list clone_prem prs, List.map clone_hint hs)
   | DecD (x, ps, t, hs) -> DecD (x, List.map clone_param ps, clone_typ t, List.map clone_hint hs)
   | DefD (x, as_, e, prs) -> DefD (x, List.map clone_arg as_, clone_exp e, Convert.map_nl_list clone_prem prs)
   | HintD hd -> HintD (clone_hintdef hd)

spectec/src/el/iter.ml

@@ -310,7 +310,7 @@ let string_of_def d =
       string_of_typ t ^ " = " ^ string_of_gram gram
   | RelD (id, ps, t, _hints) ->
     "relation " ^ string_of_relid id ^ string_of_params ps ^ ": " ^ string_of_typ t
-  | RuleD (id1, ps, id2, e, prems) ->
+  | RuleD (id1, ps, id2, e, prems, _hints) ->
     "rule " ^ string_of_relid id1 ^ string_of_params ps ^ string_of_ruleid id2 ^ ":\n  " ^
       string_of_exp e ^
       string_of_nl_list "" "" (prefix "\n  -- " string_of_prem) prems

spectec/src/el/print.ml

@@ -264,7 +264,7 @@ let subst_def s d =
   | VarD (x, t, hs) -> VarD (x, subst_typ s t, hs)
   | SepD -> SepD
   | RelD (x, ps, t, hs) -> RelD (x, List.map (subst_param s) ps, subst_typ s t, hs)
-  | RuleD (x1, ps, x2, e, prs) -> RuleD (x1, List.map (subst_param s) ps, x2, subst_exp s e, Convert.map_nl_list (subst_prem s) prs)
+  | RuleD (x1, ps, x2, e, prs, hs) -> RuleD (x1, List.map (subst_param s) ps, x2, subst_exp s e, Convert.map_nl_list (subst_prem s) prs, hs)
   | DecD (x, ps, t, hs) -> DecD (x, List.map (subst_param s) ps, subst_typ s t, hs)
   | DefD (x, as_, e, prs) -> DefD (x, List.map (subst_arg s) as_, subst_exp s e, Convert.map_nl_list (subst_prem s) prs)
   | HintD hd -> HintD hd

spectec/src/el/subst.ml

@@ -2470,7 +2470,13 @@ let elab_hintdef _env (hd : hintdef) : Il.def list =
     [Il.HintD (Il.DecH (id, elab_hints id "" hints) $ hd.at) $ hd.at]
   | AtomH (id, atom, _hints) ->
     let _ = elab_atom atom id in []
-  | GramH _ | VarH _ ->
+  | GramH (id1, _id2, hints) ->
+    if hints = [] then [] else
+    [Il.HintD (Il.GramH (id1, elab_hints id1 "" hints) $ hd.at) $ hd.at]
+  | RuleH (id1, id2, hints) ->
+    if hints = [] then [] else
+    [Il.HintD (Il.RuleH (id1, id2, elab_hints id1 "" hints) $ hd.at) $ hd.at]
+  | VarH _ ->
     []
 
 
@@ -2624,7 +2630,7 @@ let rec elab_def_pass2 env (d : def) : Il.def list =
 
   | RelD _ -> []
 
-  | RuleD (x1, ps, x2, e, prems) ->
+  | RuleD (x1, ps, x2, e, prems, hints) ->
     let ps', t', rules', mixop, not' = find "relation" env.rels x1 in
     if List.exists (fun (x, _) -> x.it = x2.it) rules' then
       error d.at ("duplicate rule name `" ^ x1.it ^
@@ -2642,7 +2648,8 @@ let rec elab_def_pass2 env (d : def) : Il.def list =
     let qs = infer_quants env env' dims det [] [] [] es' [] prems' d.at in
     let rule' = Il.RuleD (x2, qs, mixop, e', prems') $ d.at in
     env.rels <- rebind "relation" env.rels x1 (ps', t', rules' @ [x2, rule'], mixop, not');
-    if not env'.pm then [] else elab_def_pass2 env Subst.(subst_def pm_snd (Iter.clone_def d))
+    (if not env'.pm then [] else elab_def_pass2 env Subst.(subst_def pm_snd (Iter.clone_def d)))
+      @ elab_hintdef env (RuleH (x1, x2, hints) $ d.at)
 
   | VarD _ -> []
 
@@ -2694,6 +2701,7 @@ let populate_hint env (hd' : Il.hintdef) =
   | Il.RelH (x, _) -> ignore (find "relation" env.rels x)
   | Il.DecH (x, _) -> ignore (find "definition" env.defs x)
   | Il.GramH (x, _) -> ignore (find "grammar" env.grams x)
+  | Il.RuleH (x, _, _) -> ignore (find "relation" env.rels x)
 
 let populate_def env (d' : Il.def) : Il.def =
   Debug.(log_in "el.populate_def" dline);

spectec/src/frontend/elab.ml

@@ -1088,12 +1088,12 @@ def_ :
     { RelD ($2, [], $4, $5) }
   | RELATION relid LPAREN comma_list(param) RPAREN COLON nottyp hint*
     { RelD ($2, $4, $7, $8) }
-  | RULE relid ruleid_list COLON exp prem_list
+  | RULE relid ruleid_list COLON exp prem_list hint*
     { let id = if $3 = "" then "" else String.sub $3 1 (String.length $3 - 1) in
-      RuleD ($2, [], id $ $loc($3), $5, $6) }
-  | RULE relid LPAREN comma_list(param) RPAREN ruleid_list COLON exp prem_list
+      RuleD ($2, [], id $ $loc($3), $5, $6, $7) }
+  | RULE relid LPAREN comma_list(param) RPAREN ruleid_list COLON exp prem_list hint*
     { let id = if $6 = "" then "" else String.sub $6 1 (String.length $6 - 1) in
-      RuleD ($2, $4, id $ $loc($6), $8, $9) }
+      RuleD ($2, $4, id $ $loc($6), $8, $9, $10) }
   | VAR varid_bind COLON typ hint*
     { VarD ($2, $4, $5) }
   | DEF DOLLAR defid COLON typ hint*
@@ -1122,6 +1122,9 @@ def_ :
       HintD (GramH ($2, id $ $loc($3), $4) $ $sloc) }
   | RELATION relid hint*
     { HintD (RelH ($2, $3) $ $sloc) }
+  | RULE relid ruleid_list hint*
+    { let id = if $3 = "" then "" else String.sub $3 1 (String.length $3 - 1) in
+      HintD (RuleH ($2, id $ $loc($3), $4) $ $sloc) }
   | VAR varid_bind hint*
     { HintD (VarH ($2, $3) $ $sloc) }
   | DEF DOLLAR defid hint*