Source file autorewrite.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
open Equality
open Names
open Pp
open Constr
open CErrors
open Util
open Mod_subst
open Locus
type rew_rule = { rew_id : KerName.t;
rew_lemma : constr;
rew_type: types;
rew_pat: constr;
rew_ctx: Univ.ContextSet.t;
rew_l2r: bool;
rew_tac: Genarg.glob_generic_argument option }
module RewRule =
struct
type t = rew_rule
let rew_lemma r = (r.rew_ctx, r.rew_lemma)
let rew_l2r r = r.rew_l2r
let rew_tac r = r.rew_tac
end
module HintIdent =
struct
type t = rew_rule
let compare r1 r2 = KerName.compare r1.rew_id r2.rew_id
let constr_of t = t.rew_pat
end
module DTerm =
struct
type 't t =
| DRel
| DSort
| DRef of GlobRef.t
| DProd
| DLet
| DLambda
| DApp
| DCase of case_info
| DFix of int array * int
| DCoFix of int
| DInt of Uint63.t
| DFloat of Float64.t
| DArray
let compare_ci ci1 ci2 =
let c = Ind.CanOrd.compare ci1.ci_ind ci2.ci_ind in
if c = 0 then
let c = Int.compare ci1.ci_npar ci2.ci_npar in
if c = 0 then
let c = Array.compare Int.compare ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls in
if c = 0 then
Array.compare Int.compare ci1.ci_cstr_nargs ci2.ci_cstr_nargs
else c
else c
else c
let compare t1 t2 = match t1, t2 with
| DRel, DRel -> 0
| DRel, _ -> -1 | _, DRel -> 1
| DSort, DSort -> 0
| DSort, _ -> -1 | _, DSort -> 1
| DRef gr1, DRef gr2 -> GlobRef.CanOrd.compare gr1 gr2
| DRef _, _ -> -1 | _, DRef _ -> 1
| DProd, DProd -> 0
| DProd, _ -> -1 | _, DProd -> 1
| DLet, DLet -> 0
| DLet, _ -> -1 | _, DLet -> 1
| DLambda, DLambda
| DApp, DApp -> 0
| DLambda, _ -> -1 | _, DLambda -> 1
| DApp, _ -> -1 | _, DApp -> 1
| DCase ci1, DCase ci2 ->
compare_ci ci1 ci2
| DCase _, _ -> -1 | _, DCase _ -> 1
| DFix (i1, j1), DFix (i2, j2) ->
let c = Int.compare j1 j2 in
if c = 0 then
Array.compare Int.compare i1 i2
else c
| DFix _, _ -> -1 | _, DFix _ -> 1
| DCoFix i1, DCoFix i2 ->
Int.compare i1 i2
| DCoFix _, _ -> -1 | _, DCoFix _ -> 1
| DInt i1, DInt i2 -> Uint63.compare i1 i2
| DInt _, _ -> -1 | _, DInt _ -> 1
| DFloat f1, DFloat f2 -> Float64.total_compare f1 f2
| DFloat _, _ -> -1 | _, DFloat _ -> 1
| DArray, DArray -> 1
end
module HintDN :
sig
type t
type ident = HintIdent.t
val empty : t
(** [add c i dn] adds the binding [(c,i)] to [dn]. [c] can be a
closed term or a pattern (with untyped Evars). No Metas accepted *)
val add : constr -> ident -> t -> t
(** [search_pattern dn c] returns all terms/patterns in dn
matching/matched by c *)
val search_pattern : Environ.env -> t -> constr -> ident list
(** [find_all dn] returns all idents contained in dn *)
val find_all : t -> ident list
end
=
struct
module Ident = HintIdent
module PTerm =
struct
type t = unit DTerm.t
let compare = DTerm.compare
end
module TDnet = Dn.Make(PTerm)(Ident)
type t = TDnet.t
type ident = HintIdent.t
open DTerm
open TDnet
let pat_of_constr c : (unit DTerm.t * Constr.t list) option =
let open GlobRef in
let rec pat_of_constr c = match Constr.kind c with
| Rel _ -> Some (DRel, [])
| Sort _ -> Some (DSort, [])
| Var i -> Some (DRef (VarRef i), [])
| Const (c,u) -> Some (DRef (ConstRef c), [])
| Ind (i,u) -> Some (DRef (IndRef i), [])
| Construct (c,u)-> Some (DRef (ConstructRef c), [])
| Meta _ -> assert false
| Evar (i,_) -> None
| Case (ci,u1,pms1,(c1,_),_iv,c2,ca) ->
let f_ctx (_, p) = p in
Some (DCase(ci), [f_ctx c1; c2] @ Array.map_to_list f_ctx ca)
| Fix ((ia,i),(_,ta,ca)) ->
Some (DFix(ia,i), Array.to_list ta @ Array.to_list ca)
| CoFix (i,(_,ta,ca)) ->
Some (DCoFix(i), Array.to_list ta @ Array.to_list ca)
| Cast (c,_,_) -> pat_of_constr c
| Lambda (_,t,c) -> Some (DLambda, [t; c])
| Prod (_, t, u) -> Some (DProd, [t; u])
| LetIn (_, c, t, u) -> Some (DLet, [c; t; u])
| App (f,ca) ->
let len = Array.length ca in
let a = ca.(len - 1) in
let ca = Array.sub ca 0 (len - 1) in
Some (DApp, [mkApp (f, ca); a])
| Proj (p,_,c) ->
pat_of_constr (mkApp (UnsafeMonomorphic.mkConst (Projection.constant p), [|c|]))
| Int i -> Some (DInt i, [])
| Float f -> Some (DFloat f, [])
| Array (_u,t,def,ty) ->
Some (DArray, Array.to_list t @ [def ; ty])
in
pat_of_constr c
let empty = TDnet.empty
let add (c:constr) (id:Ident.t) (dn:t) =
let (ctx, c) = Term.decompose_prod_decls c in
let c = TDnet.pattern pat_of_constr c in
TDnet.add dn c id
let split_app sigma c = match EConstr.kind sigma c with
App(c,l) ->
let len = Array.length l in
if Int.equal len 0 then ([],c) else
let last = Array.get l (len-1) in
let prev = Array.sub l 0 (len-1) in
c::(Array.to_list prev), last
| _ -> assert false
exception CannotFilter
let filtering env sigma ctx cv_pb c1 c2 =
let open EConstr in
let open Vars in
let evm = ref Evar.Map.empty in
let define cv_pb e1 ev c1 =
try let (e2,c2) = Evar.Map.find ev !evm in
let shift = e1 - e2 in
if Termops.constr_cmp env sigma cv_pb c1 (lift shift c2) then () else raise CannotFilter
with Not_found ->
evm := Evar.Map.add ev (e1,c1) !evm
in
let rec aux ctx cv_pb c1 c2 =
match EConstr.kind sigma c1, EConstr.kind sigma c2 with
| App _, App _ ->
let ((p1,l1),(p2,l2)) = (split_app sigma c1),(split_app sigma c2) in
let () = aux ctx cv_pb l1 l2 in
begin match p1, p2 with
| [], [] -> ()
| (h1 :: p1), (h2 :: p2) ->
aux ctx cv_pb (applist (h1, p1)) (applist (h2, p2))
| _ -> assert false
end
| Prod (n,t1,c1), Prod (_,t2,c2) ->
aux ctx cv_pb t1 t2;
aux (ctx + 1) cv_pb c1 c2
| _, Evar (ev,_) -> define cv_pb ctx ev c1
| Evar (ev,_), _ -> define cv_pb ctx ev c2
| _ ->
if Termops.compare_constr_univ env sigma
(fun pb c1 c2 -> aux ctx pb c1 c2; true) cv_pb c1 c2 then ()
else raise CannotFilter
in
try let () = aux ctx cv_pb c1 c2 in true with CannotFilter -> false
let align_prod_letin sigma c a =
let (lc,_) = EConstr.decompose_prod_decls sigma c in
let (l,a) = EConstr.decompose_prod_decls sigma a in
let lc = List.length lc in
let n = List.length l in
if n < lc then invalid_arg "align_prod_letin";
let l1 = CList.firstn lc l in
n - lc, EConstr.it_mkProd_or_LetIn a l1
let decomp pat = match pat_of_constr pat with
| None -> Dn.Everything
| Some (lbl, args) -> Dn.Label (lbl, args)
let search_pattern env dn cpat =
let _dctx, dpat = Term.decompose_prod_decls cpat in
let whole_c = EConstr.of_constr cpat in
List.fold_left
(fun acc id ->
let c_id = EConstr.of_constr @@ Ident.constr_of id in
let (ctx,wc) =
try align_prod_letin Evd.empty whole_c c_id
with Invalid_argument _ -> 0, c_id in
if filtering env Evd.empty ctx Conversion.CUMUL whole_c wc then id :: acc
else acc
) (TDnet.lookup dn decomp dpat) []
let find_all dn = TDnet.lookup dn (fun () -> Everything) ()
end
type rewrite_db = {
rdb_hintdn : HintDN.t;
rdb_order : int KNmap.t;
rdb_maxuid : int;
}
let empty_rewrite_db = {
rdb_hintdn = HintDN.empty;
rdb_order = KNmap.empty;
rdb_maxuid = 0;
}
let rewtab =
Summary.ref (String.Map.empty : rewrite_db String.Map.t) ~name:"autorewrite"
let raw_find_base bas = String.Map.find bas !rewtab
let find_base bas =
try raw_find_base bas
with Not_found ->
user_err
(str "Rewriting base " ++ str bas ++ str " does not exist.")
let find_rewrites bas =
let db = find_base bas in
let sort r1 r2 = Int.compare (KNmap.find r2.rew_id db.rdb_order) (KNmap.find r1.rew_id db.rdb_order) in
List.sort sort (HintDN.find_all db.rdb_hintdn)
let find_matches env bas pat =
let base = find_base bas in
let res = HintDN.search_pattern env base.rdb_hintdn pat in
let sort r1 r2 = Int.compare (KNmap.find r2.rew_id base.rdb_order) (KNmap.find r1.rew_id base.rdb_order) in
List.sort sort res
let print_rewrite_hintdb bas =
let env = Global.env () in
let sigma = Evd.from_env env in
(str "Database " ++ str bas ++ fnl () ++
prlist_with_sep fnl
(fun h ->
str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++
Printer.pr_lconstr_env env sigma h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr_env env sigma h.rew_type ++
Option.cata (fun tac -> str " then use tactic " ++
Pputils.pr_glb_generic env sigma tac) (mt ()) h.rew_tac)
(find_rewrites bas))
type raw_rew_rule = (constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option) CAst.t
let tclMAP_rev f args =
List.fold_left (fun accu arg -> Tacticals.tclTHEN accu (f arg)) (Proofview.tclUNIT ()) args
let one_base where conds tac_main bas =
let lrul = find_rewrites bas in
let rewrite dir c tac =
let c = (EConstr.of_constr c, Tactypes.NoBindings) in
general_rewrite ~where ~l2r:dir AllOccurrences ~freeze:true ~dep:false ~with_evars:false ~tac:(tac, conds) c
in
let try_rewrite h tc =
Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let subst, ctx' = UnivGen.fresh_universe_context_set_instance h.rew_ctx in
let subst = Sorts.QVar.Map.empty, subst in
let c' = Vars.subst_univs_level_constr subst h.rew_lemma in
let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx' in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (rewrite h.rew_l2r c' tc)
end in
let open Proofview.Notations in
Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
let eval h =
let tac = match h.rew_tac with
| None -> Proofview.tclUNIT ()
| Some (Genarg.GenArg (Genarg.Glbwit wit, tac)) ->
let ist = { Geninterp.lfun = Id.Map.empty
; poly
; extra = Geninterp.TacStore.empty } in
Ftactic.run (Geninterp.interp wit ist tac) (fun _ -> Proofview.tclUNIT ())
in
Tacticals.tclREPEAT_MAIN (Tacticals.tclTHENFIRST (try_rewrite h tac) tac_main)
in
let lrul = tclMAP_rev eval lrul in
Tacticals.tclREPEAT_MAIN (Proofview.tclPROGRESS lrul)
let autorewrite ?(conds=Naive) tac_main lbas =
Tacticals.tclREPEAT_MAIN (Proofview.tclPROGRESS
(tclMAP_rev (fun bas -> (one_base None conds tac_main bas)) lbas))
let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas =
Proofview.Goal.enter begin fun gl ->
let _ = List.map (fun id -> Tacmach.pf_get_hyp id gl) idl in
Tacticals.tclMAP (fun id ->
Tacticals.tclREPEAT_MAIN (Proofview.tclPROGRESS
(tclMAP_rev (fun bas -> (one_base (Some id) conds tac_main bas)) lbas)))
idl
end
let autorewrite_in ?(conds=Naive) id = autorewrite_multi_in ~conds [id]
let gen_auto_multi_rewrite conds tac_main lbas cl =
let try_do_hyps treat_id l =
autorewrite_multi_in ~conds (List.map treat_id l) tac_main lbas
in
let concl_tac = (if cl.concl_occs != NoOccurrences then autorewrite ~conds tac_main lbas else Proofview.tclUNIT ()) in
if not (Locusops.is_all_occurrences cl.concl_occs) &&
cl.concl_occs != NoOccurrences
then
let info = Exninfo.reify () in
Tacticals.tclZEROMSG ~info (str"The \"at\" syntax isn't available yet for the autorewrite tactic.")
else
match cl.onhyps with
| Some [] -> concl_tac
| Some l -> Tacticals.tclTHENFIRST concl_tac (try_do_hyps (fun ((_,id),_) -> id) l)
| None ->
let hyp_tac =
Proofview.Goal.enter begin fun gl ->
let ids = Tacmach.pf_ids_of_hyps gl in
try_do_hyps (fun id -> id) ids
end
in
Tacticals.tclTHENFIRST concl_tac hyp_tac
let auto_multi_rewrite ?(conds=Naive) lems cl =
Proofview.wrap_exceptions (fun () -> gen_auto_multi_rewrite conds (Proofview.tclUNIT()) lems cl)
let fresh_key =
let id = Summary.ref ~name:"REWHINT-COUNTER" 0 in
fun () ->
let cur = incr id; !id in
let lbl = Id.of_string ("_" ^ string_of_int cur) in
let kn = Lib.make_kn lbl in
let (mp, _) = KerName.repr kn in
let lbl = Id.of_string_soft (Printf.sprintf "%s#%i"
(ModPath.to_string mp) cur)
in
KerName.make mp (Label.of_id lbl)
let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl =
let onconcl = match cl.Locus.concl_occs with NoOccurrences -> false | _ -> true in
match onconcl,cl.Locus.onhyps with
| false,Some [_] | true,Some [] | false,Some [] ->
Proofview.wrap_exceptions (fun () -> gen_auto_multi_rewrite conds tac_main lbas cl)
| _ ->
let info = Exninfo.reify () in
Tacticals.tclZEROMSG ~info
(strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.")
let cache_hintrewrite (rbase,lrl) =
let base = try raw_find_base rbase with Not_found -> empty_rewrite_db in
let fold accu r = {
rdb_hintdn = HintDN.add r.rew_pat r accu.rdb_hintdn;
rdb_order = KNmap.add r.rew_id accu.rdb_maxuid accu.rdb_order;
rdb_maxuid = accu.rdb_maxuid + 1;
} in
let base = List.fold_left fold base lrl in
rewtab := String.Map.add rbase base !rewtab
let subst_hintrewrite (subst,(rbase,list as node)) =
let subst_hint subst hint =
let id' = subst_kn subst hint.rew_id in
let cst' = subst_mps subst hint.rew_lemma in
let typ' = subst_mps subst hint.rew_type in
let pat' = subst_mps subst hint.rew_pat in
let t' = Option.Smart.map (Gensubst.generic_substitute subst) hint.rew_tac in
if hint.rew_id == id' && hint.rew_lemma == cst' && hint.rew_type == typ' &&
hint.rew_tac == t' && hint.rew_pat == pat' then hint else
{ hint with
rew_lemma = cst'; rew_type = typ';
rew_pat = pat'; rew_tac = t' }
in
let list' = List.Smart.map (fun h -> subst_hint subst h) list in
if list' == list then node else
(rbase,list')
let inGlobalHintRewrite : string * rew_rule list -> Libobject.obj =
let open Libobject in
declare_object @@ superglobal_object_nodischarge "HINT_REWRITE_GLOBAL"
~cache:cache_hintrewrite
~subst:(Some subst_hintrewrite)
let inExportHintRewrite : string * rew_rule list -> Libobject.obj =
let open Libobject in
declare_object @@ global_object_nodischarge ~cat:Hints.hint_cat "HINT_REWRITE_EXPORT"
~cache:cache_hintrewrite
~subst:(Some subst_hintrewrite)
type hypinfo = {
hyp_ty : EConstr.types;
hyp_pat : EConstr.constr;
}
let decompose_applied_relation env sigma c ctype left2right =
let find_rel ty =
let sigma, ty = EClause.make_evar_clause env sigma ty in
let (_, args) = EConstr.decompose_app sigma ty.EClause.cl_concl in
let len = Array.length args in
if 2 <= len then
let c1 = args.(len - 2) in
let c2 = args.(len - 1) in
Some (if left2right then c1 else c2)
else None
in
match find_rel ctype with
| Some c -> Some { hyp_pat = c; hyp_ty = ctype }
| None ->
let ctx,t' = Reductionops.whd_decompose_prod_decls env sigma ctype in
let ctype = EConstr.it_mkProd_or_LetIn t' ctx in
match find_rel ctype with
| Some c -> Some { hyp_pat = c; hyp_ty = ctype }
| None -> None
let find_applied_relation ?loc env sigma c left2right =
let ctype = Retyping.get_type_of env sigma (EConstr.of_constr c) in
match decompose_applied_relation env sigma c ctype left2right with
| Some c -> c
| None ->
user_err ?loc
(str"The type" ++ spc () ++ Printer.pr_econstr_env env sigma ctype ++
spc () ++ str"of this term does not end with an applied relation.")
let default_hint_rewrite_locality () =
if Lib.sections_are_opened () then Hints.Local
else Hints.Export
let add_rew_rules ~locality base lrul =
let env = Global.env () in
let sigma = Evd.from_env env in
let ist = Genintern.empty_glob_sign ~strict:true (Global.env ()) in
let intern tac = snd (Genintern.generic_intern ist tac) in
let map {CAst.loc;v=((c,ctx),b,t)} =
let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in
let info = find_applied_relation ?loc env sigma c b in
let pat = EConstr.Unsafe.to_constr info.hyp_pat in
let uid = fresh_key () in
{ rew_id = uid; rew_lemma = c; rew_type = EConstr.Unsafe.to_constr info.hyp_ty;
rew_pat = pat; rew_ctx = ctx; rew_l2r = b;
rew_tac = Option.map intern t }
in
let lrul = List.map map lrul in
let open Hints in
match locality with
| Local -> cache_hintrewrite (base,lrul)
| SuperGlobal ->
let () =
if Lib.sections_are_opened () then
CErrors.user_err Pp.(str
"This command does not support the global attribute in sections.");
in
Lib.add_leaf (inGlobalHintRewrite (base,lrul))
| Export ->
let () =
if Lib.sections_are_opened () then
CErrors.user_err Pp.(str
"This command does not support the export attribute in sections.");
in
Lib.add_leaf (inExportHintRewrite (base,lrul))