feat: Add Rewrite Rules to TemplateMonad

First hacky attempt, basically parsing the whole
`Rewrite Rule` vernac command. More robust solution
would probably require updating Rocq's API.

Author: TDiazT

template-rocq/src/plugin_core.ml

@@ -93,6 +93,36 @@ let tmDefinition (nm : ident) ?poly:(poly=false) ?opaque:(opaque=false) (typ : t
     let evm = Evd.from_env env in
     success ~st env evm (Names.Constant.canonical (Globnames.destConstRef n))
 
+let tmRewriteRule (id : ident) (rules : (string option * string * string) list) : unit tm =
+  fun ~st env evm success _fail ->
+    let one_rule (udecl, lhs, rhs) =
+      "| " ^
+      (match udecl with
+       | None -> ""
+       | Some u -> u ^ " |- ") ^
+      lhs ^ " => " ^ rhs
+    in
+    let cmd =
+      "Rewrite Rule " ^ Names.Id.to_string id ^ " :=\n" ^
+      String.concat "\n" (List.map one_rule rules) ^
+      "."
+    in
+    let parsed =
+      Procq.parse_string (Procq.eoi_entry (Pvernac.main_entry None)) cmd
+    in
+    let parsed =
+      match parsed with
+      | Some x -> x
+      | None -> CErrors.user_err (Pp.str "Empty command while parsing tmRewriteRule")
+    in
+    let vst = Vernacstate.freeze_full_state () in
+    let _vst' =
+      Vernacinterp.interp ~intern:Vernacinterp.fs_intern ~verbosely:false ~st:vst parsed
+    in
+    let env = Global.env () in
+    let evm = Evd.from_env env in
+    success ~st env evm ()
+
 let tmAxiom (nm : ident) ?poly:(poly=false) (typ : term) : kername tm =
   fun ~st env evm success _fail ->
     let univs = Evd.univ_entry ~poly evm in

template-rocq/src/plugin_core.mli

@@ -48,6 +48,7 @@ val reduce : Environ.env -> Evd.evar_map -> reduction_strategy -> term -> Evd.ev
 val tmEval : reduction_strategy -> term -> term tm
 
 val tmDefinition : ident -> ?poly:bool -> ?opaque:bool -> term option -> term -> kername tm
+val tmRewriteRule : ident -> (string option * string * string) list -> unit tm
 val tmAxiom : ident -> ?poly:bool -> term -> kername tm
 val tmLemma : ident -> ?poly:bool -> term -> kername tm
 

template-rocq/src/run_template_monad.ml

@@ -67,6 +67,14 @@ let unquote_map_option f trm =
 
 let unquote_option = unquote_map_option (fun x -> x)
 
+let unquote_rewrite_rule trm : string option * string * string =
+  let lhsrhs, rhs = unquote_pair trm in
+  let udecl, lhs = unquote_pair lhsrhs in
+  let udecl = unquote_map_option unquote_string udecl in
+  let lhs = unquote_string lhs in
+  let rhs = unquote_string rhs in
+  (udecl, lhs, rhs)
+
 let rec unquote_pos trm : int =
   let (h,args) = app_full trm [] in
   match args with
@@ -408,6 +416,15 @@ let rec run_template_program_rec ~poly ?(intactic=false) (k : Constr.t Plugin_co
       Plugin_core.run ~st
         (Plugin_core.tmDefinition name ~poly ~opaque typ body) env evm
         (fun ~st env evm res -> k ~st env evm (quote_kn res))
+  | TmRewriteRule (name, rules) ->
+    if intactic
+    then not_in_tactic "tmRewriteRule"
+    else
+      let name = unquote_ident (reduce_all env evm name) in
+      let rules = List.map unquote_rewrite_rule (unquote_list (reduce_all env evm rules)) in
+      Plugin_core.run ~st
+        (Plugin_core.tmRewriteRule name rules) env evm
+        (fun ~st env evm _ -> k ~st env evm (Lazy.force unit_tt))
   | TmLemmaTerm (name, typ) ->
     let ident = unquote_ident (reduce_all env evm name) in
     let evm,typ = denote_term env evm (reduce_all env evm typ) in

template-rocq/src/template_monad.ml

@@ -20,6 +20,7 @@ let (ptmReturn,
 
      ptmLemma,
      ptmDefinitionRed,
+     ptmRewriteRule,
      ptmAxiomRed,
      ptmMkDefinition,
      ptmMkInductive,
@@ -64,6 +65,7 @@ let (ptmReturn,
 
    r_template_monad_prop_p "tmLemma",
    r_template_monad_prop_p "tmDefinitionRed_",
+   r_template_monad_prop_p "tmRewriteRule_",
    r_template_monad_prop_p "tmAxiomRed",
    r_template_monad_prop_p "tmMkDefinition",
    r_template_monad_prop_p "tmMkInductive",
@@ -174,6 +176,7 @@ type template_monad =
 
     (* creating definitions *)
   | TmDefinition of Constr.t * Constr.t * Constr.t * Constr.t * Constr.t
+  | TmRewriteRule of Constr.t * Constr.t
   | TmDefinitionTerm of Constr.t * Constr.t * Constr.t * Constr.t
   | TmLemma of Constr.t * Constr.t
   | TmLemmaTerm of Constr.t * Constr.t
@@ -283,6 +286,11 @@ let next_action env evd (pgm : constr) : template_monad * _ =
     | opaque::name::s::typ::body::[] ->
       (TmDefinition (opaque, name, s, typ, body), universes)
     | _ -> monad_failure "tmDefinitionRed" 4
+  else if eq_gr ptmRewriteRule then
+    match args with
+    | name::rules::[] ->
+      (TmRewriteRule (name, rules), universes)
+    | _ -> monad_failure "tmRewriteRule" 2
   else if eq_gr ttmDefinition then
     match args with
     | opaque::name::typ::body::[] ->

template-rocq/src/template_monad.mli

@@ -23,6 +23,7 @@ type template_monad =
 
     (* creating definitions *)
   | TmDefinition of Constr.t * Constr.t * Constr.t * Constr.t * Constr.t
+  | TmRewriteRule of Constr.t * Constr.t
   | TmDefinitionTerm of Constr.t * Constr.t * Constr.t * Constr.t
   | TmLemma of Constr.t * Constr.t
   | TmLemmaTerm of Constr.t * Constr.t

template-rocq/theories/Constants.v

@@ -254,6 +254,7 @@ Register MetaRocq.Template.TemplateMonad.Core.tmVariable as metarocq.templatemon
 Register MetaRocq.Template.TemplateMonad.Core.tmSymbol as metarocq.templatemonad.prop.tmSymbol.
 Register MetaRocq.Template.TemplateMonad.Core.tmLemma as metarocq.templatemonad.prop.tmLemma.
 Register MetaRocq.Template.TemplateMonad.Core.tmDefinitionRed_ as metarocq.templatemonad.prop.tmDefinitionRed_.
+Register MetaRocq.Template.TemplateMonad.Core.tmRewriteRule_ as metarocq.templatemonad.prop.tmRewriteRule_.
 Register MetaRocq.Template.TemplateMonad.Core.tmAxiomRed as metarocq.templatemonad.prop.tmAxiomRed.
 Register MetaRocq.Template.TemplateMonad.Core.tmMkDefinition as metarocq.templatemonad.prop.tmMkDefinition.
 Register MetaRocq.Template.TemplateMonad.Core.tmMkInductive as metarocq.templatemonad.prop.tmMkInductive.

template-rocq/theories/TemplateMonad/Core.v

@@ -31,6 +31,7 @@ Cumulative Inductive TemplateMonad@{t u} : Type@{t} -> Prop :=
 (* Return the defined constant *)
 | tmLemma : ident -> forall A : Type@{t}, TemplateMonad A
 | tmDefinitionRed_ : forall (opaque : bool), ident -> option reductionStrategy -> forall {A:Type@{t}}, A -> TemplateMonad A
+| tmRewriteRule_ : ident -> list (option string * string * string) -> TemplateMonad unit
 | tmAxiomRed : ident -> option reductionStrategy -> forall A : Type@{t}, TemplateMonad A
 | tmVariable : ident -> Type@{t} -> TemplateMonad unit
 | tmSymbol : ident -> Type@{t} -> TemplateMonad unit
@@ -121,6 +122,14 @@ Definition tmMkInductive' (mind : mutual_inductive_body) : TemplateMonad unit
 
 Definition tmAxiom id := tmAxiomRed id None.
 Definition tmDefinition id {A} t := @tmDefinitionRed_ false id None A t.
+Definition tmRewriteRule (id : ident) (rules : list (string * string)) : TemplateMonad unit :=
+  tmRewriteRule_ id
+    (List.map (fun x =>
+                 let '(lhs, rhs) := x in
+                 (None, lhs, rhs))
+              rules).
+Definition tmRewriteRuleU (id : ident) (rules : list (option string * string * string)) : TemplateMonad unit :=
+  tmRewriteRule_ id rules.
 
 (** We keep the original behaviour of [tmQuoteRec]: it quotes all the dependencies regardless of the opaqueness settings *)
 Definition tmQuoteRec {A} (a : A) := tmQuoteRecTransp a true.

test-suite/_RocqProject.in

@@ -51,9 +51,9 @@ tmFix.v
 tmFreshName.v
 tmInferInstance.v
 tmQuoteModule.v
+tmRewriteRule.v
 tmVariable.v
 unfold.v
 univ.v
 vs.v
 ind_fresh_univ.v
-

test-suite/tmRewriteRule.v

@@ -0,0 +1,68 @@
+From MetaRocq.Utils Require Import utils.
+From MetaRocq.Template Require Import All.
+From Stdlib Require Import List.
+Import ListNotations.
+Import MRMonadNotation.
+
+
+(* Rewrite Rule pplus_rewrite :=
+| ?n ++ 0 => ?n
+| ?n ++ S ?m => S (?n ++ ?m)
+| 0 ++ ?n => ?n
+| S ?n ++ ?m => S (?n ++ ?m). *)
+
+MetaRocq Run (
+  tmSymbol "f_rr" (nat -> nat -> nat) ;;
+  tmRewriteRule "pplus_n_0_rewrite_tm"
+    [ ("f_rr ?n 0", "?n") ]).
+
+About f_rr.    
+Infix "++" := f_rr.
+
+Eval cbn in 1 ++ 0.
+(* Doesn't reduce *)
+Eval cbn in 0 ++ 1.
+
+MetaRocq Run (tmRewriteRule "pplus_rewrite"
+    [ ("?n ++ S ?m", "S (?n ++ ?m)");
+      ("S ?n ++ ?m", "S (?n ++ ?m)"); 
+      ("0 ++ ?n", "?n") ]).
+      
+Eval cbn in 0 ++ 1.    
+Eval cbn in 1 ++ 3.   
+Eval cbn in 3 ++ 1.
+
+Set Universe Polymorphism.
+#[universes(polymorphic=no)]
+Sort Exc.
+
+#[unfold_fix]
+Symbol (raise : forall (A : Type@{Exc; Set}), A).
+
+Inductive nat : Type@{Exc; Set} :=
+ | O : nat 
+ | S : nat -> nat.
+
+Inductive bool : Type@{Exc; Set} :=
+ | true
+ | false.
+ 
+Rewrite Rule raise_nat_match :=
+| match raise nat as t0 return ?P with 
+  | O => _
+  | _ => _ 
+  end => raise (?P@{t0 := raise nat}).
+  
+Eval cbn in match raise nat with | O => O | S n => S n end.
+Eval cbn in match raise nat with | O => true | S n => false end.
+
+Eval cbn in match raise bool with | true => O | false => S O end.
+  
+MetaRocq Run (tmRewriteRule "raise_bool_match"
+    [ ("match raise bool as t0 return ?P with | true => _ | _ => _ end", "raise (?P@{t0 := raise bool})")]).
+    
+Eval cbn in match raise bool with | true => O | false => S O end.
+    
+
+  
+