From aafc185d37527f72e663768375ec25864d72ec5a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 16 Dec 2021 17:28:17 +0100 Subject: [PATCH] "rewrite_strat strat with db" syntax --- doc/sphinx/addendum/generalized-rewriting.rst | 5 +++++ doc/tools/docgram/fullGrammar | 1 + doc/tools/docgram/orderedGrammar | 1 + plugins/ltac/g_rewrite.mlg | 1 + tactics/rewrite.ml | 21 ++++++++++--------- tactics/rewrite.mli | 2 +- 6 files changed, 20 insertions(+), 11 deletions(-) diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 96617cfca8aa..957dded199f3 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -795,6 +795,11 @@ Usage :tacn:`setoid_rewrite` :n:`@one_term` is basically equivalent to :n:`rewrite_strat outermost @one_term`. +.. tacn:: rewrite_strat @rewstrategy with @ident + + Equivalent to :tacn:`rewrite_strat` but the hint database + :n:`@ident` is used in typeclass inference instead of + `typeclasses_db`. .. tacn:: rewrite_db @ident__1 {? in @ident__2 } diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 06bd1cb77212..249784671322 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1727,6 +1727,7 @@ simple_tactic: [ | "compare" constr constr | "rewrite_strat" rewstrategy "in" hyp | "rewrite_strat" rewstrategy +| "rewrite_strat" rewstrategy "with" preident | "rewrite_db" preident "in" hyp | "rewrite_db" preident | "substitute" orient glob_constr_with_bindings diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index cd07e0666724..cc96aa31cbd4 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1475,6 +1475,7 @@ simple_tactic: [ | "is_ground" one_term | "autoapply" one_term "with" ident | "rewrite_strat" rewstrategy OPT ( "in" ident ) +| "rewrite_strat" rewstrategy "with" ident | "rewrite_db" ident OPT ( "in" ident ) | "substitute" OPT [ "->" | "<-" ] one_term_with_bindings | "setoid_rewrite" OPT [ "->" | "<-" ] one_term_with_bindings OPT ( "at" rewrite_occs ) OPT ( "in" ident ) diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index ddd344d8fed2..735f7a4972c1 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -155,6 +155,7 @@ let cl_rewrite_clause (ist, c) b occ cl = TACTIC EXTEND rewrite_strat | [ "rewrite_strat" rewstrategy(s) "in" hyp(id) ] -> { cl_rewrite_clause_strat s (Some id) } | [ "rewrite_strat" rewstrategy(s) ] -> { cl_rewrite_clause_strat s None } +| [ "rewrite_strat" rewstrategy(s) "with" preident(db) ] -> { cl_rewrite_clause_strat ~db s None } | [ "rewrite_db" preident(db) "in" hyp(id) ] -> { cl_rewrite_clause_db ist db (Some id) } | [ "rewrite_db" preident(db) ] -> { cl_rewrite_clause_db ist db None } END diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 7ce214879dc5..08e9b9dea3ef 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1481,7 +1481,7 @@ let () = CErrors.register_handler begin function | _ -> None end -let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : result = +let cl_rewrite_clause_aux ?(abs=None) ~db strat env avoid sigma concl is_hyp : result = let sigma, sort = Typing.sort_of env sigma concl in let evdref = ref sigma in let evars = (!evdref, Evar.Set.empty) in @@ -1502,7 +1502,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul | Identity -> Some None | Success res -> let (_, cstrs) = res.rew_evars in - let evars = solve_constraints ~db:TC.typeclasses_db env res.rew_evars in + let evars = solve_constraints ~db env res.rew_evars in let iter ev = if not (Evd.is_defined evars ev) then raise (UnsolvedConstraints (env, evars, ev)) in let () = Evar.Set.iter iter cstrs in let newt = res.rew_to in @@ -1532,7 +1532,7 @@ let newfail n s = let info = Exninfo.reify () in Proofview.tclZERO ~info (Tacticals.FailError (n, lazy s)) -let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = +let cl_rewrite_clause_newtac ?abs ?origsigma ~db ~progress strat clause = let open Proofview.Notations in (* For compatibility *) let beta = Tactics.reduct_in_concl ~cast:false ~check:false @@ -1597,7 +1597,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = in try let res = - cl_rewrite_clause_aux ?abs strat env Id.Set.empty sigma ty clause + cl_rewrite_clause_aux ?abs ~db strat env Id.Set.empty sigma ty clause in let sigma = match origsigma with None -> sigma | Some sigma -> sigma in treat sigma res state <*> @@ -1614,11 +1614,12 @@ let tactic_init_setoid () = let _, info = Exninfo.capture e in Tacticals.tclFAIL ~info (str"Setoid library not loaded") -let cl_rewrite_clause_strat progress strat clause = +let cl_rewrite_clause_strat ~db progress strat clause = + let db = Option.default TC.typeclasses_db db in tactic_init_setoid () <*> (if progress then Proofview.tclPROGRESS else fun x -> x) (Proofview.tclOR - (cl_rewrite_clause_newtac ~progress strat clause) + (cl_rewrite_clause_newtac ~db ~progress strat clause) (fun (e, info) -> match e with | Tacticals.FailError (n, pp) -> tclFAILn ~info n (str"setoid rewrite failed: " ++ Lazy.force pp) @@ -1628,11 +1629,11 @@ let cl_rewrite_clause_strat progress strat clause = (** Setoid rewriting when called with "setoid_rewrite" *) let cl_rewrite_clause l left2right occs clause = let strat = rewrite_with left2right (general_rewrite_unif_flags ()) l occs in - cl_rewrite_clause_strat true strat clause + cl_rewrite_clause_strat ~db:None true strat clause (** Setoid rewriting when called with "rewrite_strat" *) -let cl_rewrite_clause_strat strat clause = - cl_rewrite_clause_strat false strat clause +let cl_rewrite_clause_strat ?db strat clause = + cl_rewrite_clause_strat ~db false strat clause let apply_glob_constr ((_, c) : _ * EConstr.t delayed_open) l2r occs = (); fun ({ state = () ; env = env } as input) -> let c sigma = @@ -1877,7 +1878,7 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals = (tclPROGRESS (tclTHEN (Proofview.Unsafe.tclEVARS evd) - (cl_rewrite_clause_newtac ~progress:true ~abs:(Some abs) ~origsigma strat cl))) + (cl_rewrite_clause_newtac ~db:TC.typeclasses_db ~progress:true ~abs:(Some abs) ~origsigma strat cl))) (fun (e, info) -> match e with | e -> Proofview.tclZERO ~info e) end diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli index affa33182f7b..c0af2de0454d 100644 --- a/tactics/rewrite.mli +++ b/tactics/rewrite.mli @@ -69,7 +69,7 @@ val pr_strategy : ('a -> Pp.t) -> ('b -> Pp.t) -> ('a, 'b) strategy_ast -> Pp.t (** Entry point for user-level "rewrite_strat" *) -val cl_rewrite_clause_strat : strategy -> Id.t option -> unit Proofview.tactic +val cl_rewrite_clause_strat : ?db:string -> strategy -> Id.t option -> unit Proofview.tactic (** Entry point for user-level "setoid_rewrite" *) val cl_rewrite_clause :