Integrate some code review comments

Support module substitution of rewrite strategies.

Fixes coq#18463

doc/tools/docgram/common.edit_mlg

@@ -2244,14 +2244,14 @@ as_or_and_ipat: [
 | "as" or_and_intropattern
 ]
 
-rewstrategy2: [
+rewstrategy1_list: [
 | DELETE rewstrategy1
-| REPLACE rewstrategy2 ";" rewstrategy1
+| REPLACE rewstrategy1_list ";" rewstrategy1
 | WITH LIST1 rewstrategy1 SEP ";"
 ]
 
 SPLICE: [
-| rewstrategy2
+| rewstrategy1_list
 | clause
 | noedit_mode
 | match_list

doc/tools/docgram/fullGrammar

@@ -2279,11 +2279,11 @@ glob_constr_with_bindings: [
 
 rewstrategy: [
 | "fix" identref ":=" rewstrategy1
-| rewstrategy2
+| rewstrategy1_list
 ]
 
-rewstrategy2: [
-| rewstrategy2 ";" rewstrategy1
+rewstrategy1_list: [
+| rewstrategy1_list ";" rewstrategy1
 | rewstrategy1
 ]
 

plugins/ltac/g_rewrite.mlg

@@ -66,8 +66,20 @@ END
 
 {
 
-(** XXX this seems incorrect? *)
-let subst_strategy s str = str
+let rec subst_strategy sub = function
+| Rewrite.StratVar _
+| StratId | StratFail | StratRefl
+| StratHints _
+  as str -> str
+| StratConstr (c, b) -> StratConstr (Tacsubst.subst_glob_constr_and_expr sub c, b)
+| StratFix (x, s) -> StratFix (x, subst_strategy sub s)
+| StratUnary (s, str) -> StratUnary (s, subst_strategy sub str)
+| StratBinary (s, str, str') -> StratBinary (s, subst_strategy sub str, subst_strategy sub str')
+| StratNAry (s, strs) -> StratNAry (s, List.map (subst_strategy sub) strs)
+| StratTerms l -> StratTerms (List.map (Tacsubst.subst_glob_constr_and_expr sub) l)
+| StratEval r -> StratEval (Tacsubst.subst_redexp sub r)
+| StratFold c -> StratFold (Tacsubst.subst_glob_constr_and_expr sub c)
+
 
 let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>"
 let pr_raw_strategy env sigma prc prlc _ (s : Tacexpr.raw_strategy) =
@@ -97,9 +109,9 @@ GRAMMAR EXTEND Gram
   rewstrategy:
     [ NONA
       [ IDENT "fix"; id = identref; ":="; s = rewstrategy1 -> { StratFix (id, s) }
-      | h = rewstrategy2 -> { h } ] ]
+      | h = rewstrategy1_list -> { h } ] ]
   ;
-  rewstrategy2:
+  rewstrategy1_list:
     [ LEFTA
       [ h = SELF; ";"; h' = rewstrategy1 -> { StratBinary (Compose, h, h') }
       | h = rewstrategy1 -> { h } ] ]

plugins/ltac/tacintern.ml

@@ -760,16 +760,19 @@ let glob_tactic_env l env x =
 let intern_strategy ist s =
   let rec aux stratvars = function
     | Rewrite.StratVar x ->
+      (* We could make this whole branch assert false, since it's
+         unreachable except from plugins. But maybe it's useful if any
+         plug-in wants to craft a strategy by hand. *)
       if Id.Set.mem x.v stratvars then Rewrite.StratVar x.v
       else CErrors.user_err ?loc:x.loc Pp.(str "Unbound strategy" ++ spc() ++ Id.print x.v)
     | StratConstr ({ v = CRef (qid, None) }, true) when idset_mem_qualid qid stratvars ->
       let (_, x) = repr_qualid qid in Rewrite.StratVar x
+    | StratConstr (c, b) -> StratConstr (intern_constr ist c, b)
     | StratFix (x, s) -> StratFix (x.v, aux (Id.Set.add x.v stratvars) s)
     | StratId | StratFail | StratRefl as s -> s
     | StratUnary (s, str) -> StratUnary (s, aux stratvars str)
     | StratBinary (s, str, str') -> StratBinary (s, aux stratvars str, aux stratvars str')
     | StratNAry (s, strs) -> StratNAry (s, List.map (aux stratvars) strs)
-    | StratConstr (c, b) -> StratConstr (intern_constr ist c, b)
     | StratTerms l -> StratTerms (List.map (intern_constr ist) l)
     | StratHints (b, id) -> StratHints (b, id)
     | StratEval r -> StratEval (intern_red_expr ist r)

plugins/ltac/tacsubst.mli

@@ -31,3 +31,5 @@ val subst_glob_constr_and_expr :
 val subst_glob_with_bindings : substitution ->
   glob_constr_and_expr with_bindings ->
   glob_constr_and_expr with_bindings
+
+val subst_redexp : substitution -> Genredexpr.glob_red_expr -> Genredexpr.glob_red_expr

tactics/redexpr.mli

@@ -54,6 +54,10 @@ val set_strategy :
 (** call by value normalisation function using the virtual machine *)
 val cbv_vm : reduction_function
 
+(** [subst_red_expr sub c] performs the substitution [sub] on all kernel
+   names appearing in [c] *)
+val subst_red_expr : Mod_subst.substitution -> red_expr -> red_expr
+
 open Constrexpr
 open Libnames
 

test-suite/bugs/bug_18463.v

@@ -0,0 +1,38 @@
+From Coq Require Import Setoid.
+
+Module Type Nop. End Nop.
+Module nop. End nop.
+
+Module RewriteStratSubstTestF (Nop : Nop).
+  Axiom X : Set.
+
+  Axiom f : X -> X.
+  Axiom g : X -> X -> X.
+  Axiom h : nat -> X -> X.
+
+  Axiom lem0 : forall x, f (f x) = f x.
+  Axiom lem1 : forall x, g x x = f x.
+  Axiom lem2 : forall n x, h (S n) x = g (h n x) (h n x).
+  Axiom lem3 : forall x, h 0 x = x.
+  Definition idnat := @id nat.
+
+  Ltac rs1 := rewrite_strat topdown lem2.
+  Ltac rs2 := rewrite_strat try fold idnat.
+  Ltac rs3 := rewrite_strat try subterms lem2.
+  Ltac rs4 := rewrite_strat eval cbv delta [idnat].
+End RewriteStratSubstTestF.
+
+Module RewriteStratSubstTest := RewriteStratSubstTestF nop.
+
+Goal forall x, RewriteStratSubstTest.h 6 x = RewriteStratSubstTest.f x /\ RewriteStratSubstTest.idnat 5 = id 5.
+  intros.
+  Print Ltac RewriteStratSubstTest.rs1. (* Ltac RewriteStratSubstTest.rs1 := Coq.Init.Ltac.rewrite_strat_#_521927FC _ (* Generic printer *) *)
+  RewriteStratSubstTest.rs1. (* Error: Anomaly "Constant rewrite_strat.RewriteStratSubstTestF.lem2 does not appear in the environment."
+Please report at http://coq.inria.fr/bugs/. *)
+Undo 1.
+  RewriteStratSubstTest.rs2.
+Undo 1.
+  RewriteStratSubstTest.rs3.
+Undo 1.
+  RewriteStratSubstTest.rs4.
+Admitted.