Skip to content

Commit 76075ca

Browse files
coqbot-app[bot]ejgallego
coqbot-app[bot]
and
ejgallego
authored
Merge PR #15767: Move the rewrite implementation out of Ltac.
Reviewed-by: ejgallego Ack-by: JasonGross Ack-by: Alizter Co-authored-by: ejgallego <[email protected]>
2 parents 3539569 + 8e7fa46 commit 76075ca

File tree

6 files changed

+377
-278
lines changed

6 files changed

+377
-278
lines changed

‎plugins/ltac/comRewrite.ml

Lines changed: 258 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,258 @@
1+
(************************************************************************)
2+
(* * The Coq Proof Assistant / The Coq Development Team *)
3+
(* v * Copyright INRIA, CNRS and contributors *)
4+
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
5+
(* \VV/ **************************************************************)
6+
(* // * This file is distributed under the terms of the *)
7+
(* * GNU Lesser General Public License Version 2.1 *)
8+
(* * (see LICENSE file for the text of the license) *)
9+
(************************************************************************)
10+
11+
open Util
12+
open Names
13+
open Nameops
14+
open Constr
15+
open Constrexpr
16+
open EConstr
17+
open Libnames
18+
19+
let () = CErrors.register_handler begin function
20+
| Rewrite.RewriteFailure (env, sigma, e) ->
21+
let e = Himsg.explain_pretype_error env sigma e in
22+
Some Pp.(str"setoid rewrite failed: " ++ e)
23+
| _ -> None
24+
end
25+
26+
module TC = Typeclasses
27+
28+
let classes_dirpath =
29+
Names.DirPath.make (List.map Id.of_string ["Classes";"Coq"])
30+
31+
let init_setoid () =
32+
if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
33+
else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"]
34+
35+
type rewrite_attributes = { polymorphic : bool; global : bool }
36+
37+
let rewrite_attributes =
38+
let open Attributes.Notations in
39+
Attributes.(polymorphic ++ program ++ locality) >>= fun ((polymorphic, program), locality) ->
40+
let global = not (Locality.make_section_locality locality) in
41+
Attributes.Notations.return { polymorphic; global }
42+
43+
(** Utility functions *)
44+
45+
let find_reference dir s =
46+
Coqlib.find_reference "generalized rewriting" dir s
47+
[@@warning "-3"]
48+
49+
let lazy_find_reference dir s =
50+
let gr = lazy (find_reference dir s) in
51+
fun () -> Lazy.force gr
52+
53+
module PropGlobal = struct
54+
55+
let morphisms = ["Coq"; "Classes"; "Morphisms"]
56+
57+
let respectful_ref = lazy_find_reference morphisms "respectful"
58+
59+
let proper_class =
60+
let r = lazy (find_reference morphisms "Proper") in
61+
fun env sigma -> TC.class_info env sigma (Lazy.force r)
62+
63+
let proper_proj env sigma =
64+
mkConst (Option.get (List.hd (proper_class env sigma).TC.cl_projs).TC.meth_const)
65+
66+
67+
end
68+
69+
(* By default the strategy for "rewrite_db" is top-down *)
70+
71+
let mkappc s l = CAst.make @@ CAppExpl ((qualid_of_ident (Id.of_string s),None),l)
72+
73+
let declare_an_instance n s args =
74+
(((CAst.make @@ Name n),None),
75+
CAst.make @@ CAppExpl ((qualid_of_string s,None), args))
76+
77+
let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
78+
79+
let get_locality b = if b then Hints.SuperGlobal else Hints.Local
80+
81+
let anew_instance atts binders (name,t) fields =
82+
let locality = get_locality atts.global in
83+
let _id = Classes.new_instance ~poly:atts.polymorphic
84+
name binders t (true, CAst.make @@ CRecord (fields))
85+
~locality Hints.empty_hint_info
86+
in
87+
()
88+
89+
let declare_instance_refl atts binders a aeq n lemma =
90+
let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
91+
in anew_instance atts binders instance
92+
[(qualid_of_ident (Id.of_string "reflexivity"),lemma)]
93+
94+
let declare_instance_sym atts binders a aeq n lemma =
95+
let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric"
96+
in anew_instance atts binders instance
97+
[(qualid_of_ident (Id.of_string "symmetry"),lemma)]
98+
99+
let declare_instance_trans atts binders a aeq n lemma =
100+
let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive"
101+
in anew_instance atts binders instance
102+
[(qualid_of_ident (Id.of_string "transitivity"),lemma)]
103+
104+
let declare_relation atts ?(binders=[]) a aeq n refl symm trans =
105+
init_setoid ();
106+
let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation" in
107+
let () = anew_instance atts binders instance [] in
108+
match (refl,symm,trans) with
109+
(None, None, None) -> ()
110+
| (Some lemma1, None, None) ->
111+
declare_instance_refl atts binders a aeq n lemma1
112+
| (None, Some lemma2, None) ->
113+
declare_instance_sym atts binders a aeq n lemma2
114+
| (None, None, Some lemma3) ->
115+
declare_instance_trans atts binders a aeq n lemma3
116+
| (Some lemma1, Some lemma2, None) ->
117+
let () = declare_instance_refl atts binders a aeq n lemma1 in
118+
declare_instance_sym atts binders a aeq n lemma2
119+
| (Some lemma1, None, Some lemma3) ->
120+
let () = declare_instance_refl atts binders a aeq n lemma1 in
121+
let () = declare_instance_trans atts binders a aeq n lemma3 in
122+
let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in
123+
anew_instance atts binders instance
124+
[(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1);
125+
(qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)]
126+
| (None, Some lemma2, Some lemma3) ->
127+
let () = declare_instance_sym atts binders a aeq n lemma2 in
128+
let () = declare_instance_trans atts binders a aeq n lemma3 in
129+
let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in
130+
anew_instance atts binders instance
131+
[(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2);
132+
(qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)]
133+
| (Some lemma1, Some lemma2, Some lemma3) ->
134+
let () = declare_instance_refl atts binders a aeq n lemma1 in
135+
let () = declare_instance_sym atts binders a aeq n lemma2 in
136+
let () = declare_instance_trans atts binders a aeq n lemma3 in
137+
let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in
138+
anew_instance atts binders instance
139+
[(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1);
140+
(qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2);
141+
(qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)]
142+
143+
let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None)
144+
145+
let proper_projection env sigma r ty =
146+
let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) in
147+
let ctx, inst = decompose_prod_assum sigma ty in
148+
let mor, args = destApp sigma inst in
149+
let instarg = mkApp (r, rel_vect 0 (List.length ctx)) in
150+
let app = mkApp (PropGlobal.proper_proj env sigma,
151+
Array.append args [| instarg |]) in
152+
it_mkLambda_or_LetIn app ctx
153+
154+
let declare_projection name instance_id r =
155+
let env = Global.env () in
156+
let poly = Environ.is_polymorphic env r in
157+
let sigma = Evd.from_env env in
158+
let sigma,c = Evd.fresh_global env sigma r in
159+
let ty = Retyping.get_type_of env sigma c in
160+
let body = proper_projection env sigma c ty in
161+
let sigma, typ = Typing.type_of env sigma body in
162+
let ctx, typ = decompose_prod_assum sigma typ in
163+
let typ =
164+
let n =
165+
let rec aux t =
166+
match EConstr.kind sigma t with
167+
| App (f, [| a ; a' ; rel; rel' |])
168+
when isRefX sigma (PropGlobal.respectful_ref ()) f ->
169+
succ (aux rel')
170+
| _ -> 0
171+
in
172+
let init =
173+
match EConstr.kind sigma typ with
174+
App (f, args) when isRefX sigma (PropGlobal.respectful_ref ()) f ->
175+
mkApp (f, fst (Array.chop (Array.length args - 2) args))
176+
| _ -> typ
177+
in aux init
178+
in
179+
let ctx,ccl = Reductionops.splay_prod_n env sigma (3 * n) typ
180+
in it_mkProd_or_LetIn ccl ctx
181+
in
182+
let types = Some (it_mkProd_or_LetIn typ ctx) in
183+
let kind = Decls.(IsDefinition Definition) in
184+
let impargs, udecl = [], UState.default_univ_decl in
185+
let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types () in
186+
let info = Declare.Info.make ~kind ~udecl ~poly () in
187+
let _r : GlobRef.t =
188+
Declare.declare_definition ~cinfo ~info ~opaque:false ~body sigma
189+
in ()
190+
191+
let add_setoid atts binders a aeq t n =
192+
init_setoid ();
193+
let () = declare_instance_refl atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in
194+
let () = declare_instance_sym atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
195+
let () = declare_instance_trans atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in
196+
let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
197+
in
198+
anew_instance atts binders instance
199+
[(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
200+
(qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
201+
(qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]
202+
203+
let add_morphism_as_parameter atts m n : unit =
204+
init_setoid ();
205+
let instance_id = add_suffix n "_Proper" in
206+
let env = Global.env () in
207+
let evd = Evd.from_env env in
208+
let poly = atts.polymorphic in
209+
let kind = Decls.(IsAssumption Logical) in
210+
let impargs, udecl = [], UState.default_univ_decl in
211+
let evd, types = Rewrite.Internal.build_morphism_signature env evd m in
212+
let evd, pe = Declare.prepare_parameter ~poly ~udecl ~types evd in
213+
let cst = Declare.declare_constant ~name:instance_id ~kind (Declare.ParameterEntry pe) in
214+
let cst = GlobRef.ConstRef cst in
215+
Classes.Internal.add_instance
216+
(PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global cst;
217+
declare_projection n instance_id cst
218+
219+
let add_morphism_interactive atts ~tactic m n : Declare.Proof.t =
220+
init_setoid ();
221+
let instance_id = add_suffix n "_Proper" in
222+
let env = Global.env () in
223+
let evd = Evd.from_env env in
224+
let evd, morph = Rewrite.Internal.build_morphism_signature env evd m in
225+
let poly = atts.polymorphic in
226+
let kind = Decls.(IsDefinition Instance) in
227+
let hook { Declare.Hook.S.dref; _ } = dref |> function
228+
| GlobRef.ConstRef cst ->
229+
Classes.Internal.add_instance (PropGlobal.proper_class env evd) Hints.empty_hint_info
230+
atts.global (GlobRef.ConstRef cst);
231+
declare_projection n instance_id (GlobRef.ConstRef cst)
232+
| _ -> assert false
233+
in
234+
let hook = Declare.Hook.make hook in
235+
Flags.silently
236+
(fun () ->
237+
let cinfo = Declare.CInfo.make ~name:instance_id ~typ:morph () in
238+
let info = Declare.Info.make ~poly ~hook ~kind () in
239+
let lemma = Declare.Proof.start ~cinfo ~info evd in
240+
fst (Declare.Proof.by tactic lemma)) ()
241+
242+
let add_morphism atts ~tactic binders m s n =
243+
init_setoid ();
244+
let instance_id = add_suffix n "_Proper" in
245+
let instance_name = (CAst.make @@ Name instance_id),None in
246+
let instance_t =
247+
CAst.make @@ CAppExpl
248+
((Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper",None),
249+
[cHole; s; m])
250+
in
251+
let locality = get_locality atts.global in
252+
let _id, lemma = Classes.new_instance_interactive
253+
~locality ~poly:atts.polymorphic
254+
instance_name binders instance_t
255+
~tac:tactic ~hook:(declare_projection n instance_id)
256+
Hints.empty_hint_info None
257+
in
258+
lemma (* no instance body -> always open proof *)

‎plugins/ltac/comRewrite.mli

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
(************************************************************************)
2+
(* * The Coq Proof Assistant / The Coq Development Team *)
3+
(* v * Copyright INRIA, CNRS and contributors *)
4+
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
5+
(* \VV/ **************************************************************)
6+
(* // * This file is distributed under the terms of the *)
7+
(* * GNU Lesser General Public License Version 2.1 *)
8+
(* * (see LICENSE file for the text of the license) *)
9+
(************************************************************************)
10+
11+
open Names
12+
open Constrexpr
13+
14+
type rewrite_attributes
15+
val rewrite_attributes : rewrite_attributes Attributes.attribute
16+
17+
val declare_relation
18+
: rewrite_attributes
19+
-> ?binders:local_binder_expr list
20+
-> constr_expr
21+
-> constr_expr
22+
-> Id.t
23+
-> constr_expr option
24+
-> constr_expr option
25+
-> constr_expr option
26+
-> unit
27+
28+
val add_setoid
29+
: rewrite_attributes
30+
-> local_binder_expr list
31+
-> constr_expr
32+
-> constr_expr
33+
-> constr_expr
34+
-> Id.t
35+
-> unit
36+
37+
val add_morphism_interactive : rewrite_attributes ->
38+
tactic:unit Proofview.tactic -> constr_expr -> Id.t -> Declare.Proof.t
39+
val add_morphism_as_parameter : rewrite_attributes -> constr_expr -> Id.t -> unit
40+
41+
val add_morphism
42+
: rewrite_attributes
43+
-> tactic:unit Proofview.tactic
44+
-> local_binder_expr list
45+
-> constr_expr
46+
-> constr_expr
47+
-> Id.t
48+
-> Declare.Proof.t

‎plugins/ltac/g_rewrite.mlg

Lines changed: 21 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ open Genintern
2020
open Geninterp
2121
open Extraargs
2222
open Rewrite
23+
open ComRewrite
2324
open Stdarg
2425
open Tactypes
2526
open Pcoq.Prim
@@ -69,7 +70,11 @@ type raw_strategy = (constr_expr, Tacexpr.raw_red_expr) strategy_ast
6970
type glob_strategy = (glob_constr_and_expr, Tacexpr.glob_red_expr) strategy_ast
7071

7172
let interp_strategy ist env sigma s =
72-
strategy_of_ast ist s
73+
let interp_redexpr r = fun env sigma -> Tacinterp.interp_red_expr ist env sigma r in
74+
let interp_constr c = (fst c, fun env sigma -> Tacinterp.interp_open_constr ist env sigma c) in
75+
let s = map_strategy interp_constr interp_redexpr s in
76+
strategy_of_ast s
77+
7378
let glob_strategy ist s = map_strategy (Tacintern.intern_constr ist) (Tacintern.intern_red_expr ist) s
7479
let subst_strategy s str = str
7580

@@ -125,7 +130,11 @@ END
125130
{
126131

127132
let db_strat db = StratUnary (Topdown, StratHints (false, db))
128-
let cl_rewrite_clause_db ist db = cl_rewrite_clause_strat (strategy_of_ast ist (db_strat db))
133+
let cl_rewrite_clause_db ist db = cl_rewrite_clause_strat (strategy_of_ast (db_strat db))
134+
135+
let cl_rewrite_clause (ist, c) b occ cl =
136+
let c env sigma = Tacinterp.interp_open_constr_with_bindings ist env sigma c in
137+
cl_rewrite_clause c b occ cl
129138

130139
}
131140

@@ -272,6 +281,13 @@ END
272281
let add_setoid atts binders a aeq t n =
273282
add_setoid atts binders a aeq t n.CAst.v
274283

284+
let morphism_tactic =
285+
let open Tacexpr in
286+
let name = "Coq.Classes.SetoidTactics.add_morphism_tactic" in
287+
let tacqid = Libnames.qualid_of_string name in
288+
let tac = CAst.make @@ TacArg (TacCall (CAst.make (tacqid, []))) in
289+
Tacinterp.interp tac
290+
275291
}
276292

277293
VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
@@ -287,17 +303,17 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
287303
=> { VtStartProof(GuaranteesOpacity, [n.CAst.v]) }
288304
-> { if Lib.is_modtype () then
289305
CErrors.user_err Pp.(str "Add Morphism cannot be used in a module type. Use Parameter Morphism instead.");
290-
add_morphism_interactive atts m n.CAst.v }
306+
add_morphism_interactive atts ~tactic:morphism_tactic m n.CAst.v }
291307
| #[ atts = rewrite_attributes; ] [ "Declare" "Morphism" constr(m) ":" identref(n) ]
292308
=> { VtSideff([n.CAst.v], VtLater) }
293309
-> { add_morphism_as_parameter atts m n.CAst.v }
294310
| #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" identref(n) ]
295311
=> { VtStartProof(GuaranteesOpacity,[n.CAst.v]) }
296-
-> { add_morphism atts [] m s n.CAst.v }
312+
-> { add_morphism atts ~tactic:morphism_tactic [] m s n.CAst.v }
297313
| #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
298314
"with" "signature" lconstr(s) "as" identref(n) ]
299315
=> { VtStartProof(GuaranteesOpacity,[n.CAst.v]) }
300-
-> { add_morphism atts binders m s n.CAst.v }
316+
-> { add_morphism atts ~tactic:morphism_tactic binders m s n.CAst.v }
301317
END
302318

303319
TACTIC EXTEND setoid_symmetry

0 commit comments

Comments
 (0)