Source file proof_diffs.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
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
open Pp_diff
let term_color = ref true
let write_color_enabled enabled =
term_color := enabled
let color_enabled () = !term_color
type diffOpt = DiffOff | DiffOn | DiffRemoved
let diffs_to_string = function
| DiffOff -> "off"
| DiffOn -> "on"
| DiffRemoved -> "removed"
let assert_color_enabled () =
if not (color_enabled ()) then
CErrors.user_err
Pp.(str "Enabling Diffs requires setting the \"-color\" command line argument to \"on\" or \"auto\".")
let string_to_diffs = function
| "off" -> DiffOff
| "on" -> assert_color_enabled (); DiffOn
| "removed" -> assert_color_enabled (); DiffRemoved
| _ -> CErrors.user_err Pp.(str "Diffs option only accepts the following values: \"off\", \"on\", \"removed\".")
let opt_name = ["Diffs"]
let { Goptions.get = diff_option } =
Goptions.declare_interpreted_string_option_and_ref
~key:opt_name
~value:DiffOff
string_to_diffs
diffs_to_string
()
let show_diffs () = match diff_option () with DiffOff -> false | _ -> true
let show_removed () = match diff_option () with DiffRemoved -> true | _ -> false
let cfprintf oc = Printf.(kfprintf (fun oc -> fprintf oc "") oc)
let log_out_ch = ref stdout
[@@@ocaml.warning "-32"]
let cprintf s = cfprintf !log_out_ch s
[@@@ocaml.warning "+32"]
let tokenize_string s =
let kwstate = Pcoq.get_keyword_state() in
let rec stream_tok acc str =
let e = Gramlib.LStream.next kwstate str in
if Tok.(equal e EOI) then
List.rev acc
else
stream_tok ((Tok.extract_string true e) :: acc) str
in
let st = CLexer.Lexer.State.get () in
Fun.protect ~finally:(fun () -> CLexer.Lexer.State.set st) @@ fun () ->
try
let istr = Gramlib.Stream.of_string s in
let lex = CLexer.LexerDiff.tok_func istr in
stream_tok [] lex
with exn when CErrors.noncritical exn ->
raise (Diff_Failure "Input string is not lexable")
type hyp_info = {
idents: string list;
rhs_pp: Pp.t;
}
let diff_hyps o_idents_in_lines o_map n_idents_in_lines n_map =
let rv : Pp.t list ref = ref [] in
let removals = ref CString.Map.empty in
let best_match old_ids =
let rec aux best best_score = function
| [] -> best
| nl_idents :: tl ->
let score = List.fold_left (fun rv ident ->
if List.mem ident nl_idents then rv+1 else rv) 0 old_ids in
if score > best_score then
aux (List.hd nl_idents) score tl
else
aux best best_score tl
in
aux "" 0 n_idents_in_lines
in
let gen_line old_ids old_rhs new_ids new_rhs otype =
let gen_pp ids map hyp =
if ids = [] then ("", Pp.mt ()) else begin
let open Pp in
let pp_ids = List.map (fun x -> str x) ids in
let hyp_pp = List.fold_left (fun l1 l2 -> l1 ++ str ", " ++ l2) (List.hd pp_ids) (List.tl pp_ids) ++ hyp in
(string_of_ppcmds hyp_pp, hyp_pp)
end;
in
let (o_line, o_pp) = gen_pp old_ids o_map old_rhs in
let (n_line, n_pp) = gen_pp new_ids n_map new_rhs in
let hyp_diffs = diff_str ~tokenize_string o_line n_line in
if otype = `Added then begin
let rems = try CString.Map.find (List.hd new_ids) !removals with Not_found -> [] in
rv := add_diff_tags otype n_pp hyp_diffs :: (rems @ !rv)
end else begin
let (has_added, has_removed) = has_changes hyp_diffs in
if has_removed then begin
let d_line = add_diff_tags otype o_pp hyp_diffs in
let best = best_match old_ids in
if best = "" then
rv := d_line :: !rv
else begin
let ent = try CString.Map.find best !removals with Not_found -> [] in
removals := CString.Map.add best (d_line :: ent) !removals
end
end
end
in
let half_diff old_ids o_map n_idents_in_lines n_map otype =
let rec do_lines = function
| [] -> ()
| ids_in_line :: tl ->
let nl_idents, new_rhs =
try let ent = CString.Map.find (List.hd ids_in_line) n_map in
ent.idents, ent.rhs_pp
with Not_found -> [], (Pp.mt ()) in
let rec get_ol_idents ol_idents old_rhs = function
| [] -> List.rev ol_idents, old_rhs
| ident :: tl ->
try
let o_ent = CString.Map.find ident o_map in
let eq = (o_ent.rhs_pp = new_rhs) in
let ol_idents = if eq then ident :: ol_idents else ol_idents in
let old_rhs = if eq || old_rhs = None then Some o_ent.rhs_pp else old_rhs in
get_ol_idents ol_idents old_rhs tl
with Not_found -> get_ol_idents ol_idents old_rhs tl
in
let (ol_idents, old_rhs) = get_ol_idents [] None nl_idents in
let old_rhs = Option.default (Pp.mt ()) old_rhs in
let rhs_eq = old_rhs = new_rhs in
let filter_ol () = if rhs_eq then ol_idents else
List.filter (fun ident -> CString.Map.mem ident o_map) nl_idents in
if otype = `Added then begin
let ol_idents = filter_ol () in
gen_line ol_idents old_rhs nl_idents new_rhs otype
end else if not rhs_eq || List.length nl_idents <> List.length ol_idents then begin
let ol_idents = filter_ol () in
gen_line nl_idents new_rhs ol_idents old_rhs otype
end;
do_lines tl
in
do_lines n_idents_in_lines
in
if show_removed () then
half_diff (List.flatten n_idents_in_lines) n_map o_idents_in_lines o_map `Removed;
half_diff (List.flatten o_idents_in_lines) o_map n_idents_in_lines n_map `Added;
List.rev !rv
type goal = { ty: EConstr.t; env : Environ.env; sigma : Evd.evar_map; }
module CDC = Context.Compacted.Declaration
let to_tuple : EConstr.compacted_declaration -> (Names.Id.t EConstr.binder_annot list * 'pc option * 'pc) =
let open CDC in function
| LocalAssum(idl, tm) -> (idl, None, tm)
| LocalDef(idl,tdef,tm) -> (idl, Some tdef, tm)
let make_goal env sigma g =
let evi = Evd.find_undefined sigma g in
let env = Evd.evar_filtered_env env evi in
let ty = Evd.evar_concl evi in
{ ty; env; sigma }
let pr_letype_env ?goal_concl_style env sigma ?impargs t =
Ppconstr.pr_lconstr_expr env sigma
(Constrextern.extern_type ?goal_concl_style env sigma ?impargs t)
let pp_of_type env sigma ty =
pr_letype_env ~goal_concl_style:true env sigma ty
let pr_leconstr_env ?inctx ?scope env sigma t =
Ppconstr.pr_lconstr_expr env sigma (Constrextern.extern_constr ?inctx ?scope env sigma t)
let pr_econstr_env ?inctx ?scope env sigma t =
Ppconstr.pr_constr_expr env sigma (Constrextern.extern_constr ?inctx ?scope env sigma t)
let diff_concl ?og_s ng =
let o_concl_pp = match og_s with
| Some { ty = oty; env = oenv; sigma = osigma } -> pp_of_type oenv osigma oty
| None -> Pp.mt()
in
let { ty = nty; env = nenv; sigma = nsigma } = ng in
let n_concl_pp = pp_of_type nenv nsigma nty in
let show_removed = Some (show_removed ()) in
diff_pp_combined ~tokenize_string ?show_removed o_concl_pp n_concl_pp
let goal_info goal =
let map = ref CString.Map.empty in
let line_idents = ref [] in
let build_hyp_info env sigma hyp =
let (names, body, ty) = to_tuple hyp in
let open Pp in
let idents = List.map (fun x -> Names.Id.to_string x.Context.binder_name) names in
line_idents := idents :: !line_idents;
let mid = match body with
| Some c ->
let pb = pr_leconstr_env env sigma c in
let pb = if EConstr.isCast sigma c then surround pb else pb in
str " := " ++ pb
| None -> mt() in
let ts = pp_of_type env sigma ty in
let rhs_pp = mid ++ str " : " ++ ts in
let make_entry () = { idents; rhs_pp } in
List.iter (fun ident -> map := (CString.Map.add ident (make_entry ()) !map); ()) idents
in
try
let { ty=ty; env=env; sigma } = goal in
let hyps = Termops.compact_named_context sigma (EConstr.named_context env) in
let () = List.iter (build_hyp_info env sigma) (List.rev hyps) in
let concl_pp = pp_of_type env sigma ty in
( List.rev !line_idents, !map, concl_pp )
with e when CErrors.noncritical e -> ([], !map, Pp.mt ())
let diff_goal_info ~short o_info n_info =
let (o_idents_in_lines, o_hyp_map, o_concl_pp) = o_info in
let (n_idents_in_lines, n_hyp_map, n_concl_pp) = n_info in
let show_removed = Some (show_removed ()) in
let concl_pp = diff_pp_combined ~tokenize_string ?show_removed o_concl_pp n_concl_pp in
let hyp_diffs_list =
if short then [] else diff_hyps o_idents_in_lines o_hyp_map n_idents_in_lines n_hyp_map in
(hyp_diffs_list, concl_pp)
let unwrap g_s =
match g_s with
| Some g_s -> goal_info g_s
| None -> ([], CString.Map.empty, Pp.mt ())
let diff_goal ?(short=false) ?og_s ng =
diff_goal_info ~short (unwrap og_s) (goal_info ng)
open Constrexpr
open Names
open CAst
let match_goals ot nt =
let nevar_to_oevar = ref CString.Map.empty in
let iter2 f l1 l2 =
if List.length l1 = (List.length l2) then
List.iter2 f l1 l2
in
let rec match_goals_r ogname ot nt =
let constr_expr ogname exp exp2 =
match_goals_r ogname exp.v exp2.v
in
let constr_expr_opt ogname exp exp2 =
match exp, exp2 with
| Some expa, Some expb -> constr_expr ogname expa expb
| None, None -> ()
| _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (1)")
in
let constr_arr ogname arr_exp arr_exp2 =
let len = Array.length arr_exp in
if len <> Array.length arr_exp2 then
raise (Diff_Failure "Unable to match goals between old and new proof states (6)");
for i = 0 to len -1 do
constr_expr ogname arr_exp.(i) arr_exp2.(i)
done
in
let local_binder_expr ogname exp exp2 =
match exp, exp2 with
| CLocalAssum (nal,_,bk,ty), CLocalAssum(nal2,_,bk2,ty2) ->
constr_expr ogname ty ty2
| CLocalDef (n,_,c,t), CLocalDef (n2,_,c2,t2) ->
constr_expr ogname c c2;
constr_expr_opt ogname t t2
| CLocalPattern p, CLocalPattern p2 ->
let ty = match p.v with CPatCast (_,ty) -> Some ty | _ -> None in
let ty2 = match p2.v with CPatCast (_,ty) -> Some ty | _ -> None in
constr_expr_opt ogname ty ty2
| _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (2)")
in
let recursion_order_expr ogname exp exp2 =
match exp.CAst.v, exp2.CAst.v with
| CStructRec _, CStructRec _ -> ()
| CWfRec (_,c), CWfRec (_,c2) ->
constr_expr ogname c c2
| CMeasureRec (_,m,r), CMeasureRec (_,m2,r2) ->
constr_expr ogname m m2;
constr_expr_opt ogname r r2
| _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (3)")
in
let fix_expr ogname exp exp2 =
let (l,_,ro,lb,ce1,ce2), (l2,_,ro2,lb2,ce12,ce22) = exp,exp2 in
Option.iter2 (recursion_order_expr ogname) ro ro2;
iter2 (local_binder_expr ogname) lb lb2;
constr_expr ogname ce1 ce12;
constr_expr ogname ce2 ce22
in
let cofix_expr ogname exp exp2 =
let (l,_,lb,ce1,ce2), (l2,_,lb2,ce12,ce22) = exp,exp2 in
iter2 (local_binder_expr ogname) lb lb2;
constr_expr ogname ce1 ce12;
constr_expr ogname ce2 ce22
in
let case_expr ogname exp exp2 =
let (ce,l,cp), (ce2,l2,cp2) = exp,exp2 in
constr_expr ogname ce ce2
in
let branch_expr ogname exp exp2 =
let (cpe,ce), (cpe2,ce2) = exp.v,exp2.v in
constr_expr ogname ce ce2
in
let constr_notation_substitution ogname exp exp2 =
let (ce, cel, cp, lb), (ce2, cel2, cp2, lb2) = exp, exp2 in
iter2 (constr_expr ogname) ce ce2;
iter2 (fun a a2 -> iter2 (constr_expr ogname) a a2) cel cel2;
iter2 (fun a a2 -> iter2 (local_binder_expr ogname) a a2) lb lb2
in
begin
match ot, nt with
| CRef (ref,us), CRef (ref2,us2) -> ()
| CFix (id,fl), CFix (id2,fl2) ->
iter2 (fix_expr ogname) fl fl2
| CCoFix (id,cfl), CCoFix (id2,cfl2) ->
iter2 (cofix_expr ogname) cfl cfl2
| CProdN (bl,c2), CProdN (bl2,c22)
| CLambdaN (bl,c2), CLambdaN (bl2,c22) ->
iter2 (local_binder_expr ogname) bl bl2;
constr_expr ogname c2 c22
| CLetIn (na,c1,t,c2), CLetIn (na2,c12,t2,c22) ->
constr_expr ogname c1 c12;
constr_expr_opt ogname t t2;
constr_expr ogname c2 c22
| CAppExpl ((ref,us),args), CAppExpl ((ref2,us2),args2) ->
iter2 (constr_expr ogname) args args2
| CApp (f,args), CApp (f2,args2) ->
constr_expr ogname f f2;
iter2 (fun a a2 -> let (c, _) = a and (c2, _) = a2 in
constr_expr ogname c c2) args args2
| CProj (expl,f,args,c), CProj (expl2,f2,args2,c2) ->
iter2 (fun a a2 -> let (c, _) = a and (c2, _) = a2 in
constr_expr ogname c c2) args args2;
constr_expr ogname c c2;
| CRecord fs, CRecord fs2 ->
iter2 (fun a a2 -> let (_, c) = a and (_, c2) = a2 in
constr_expr ogname c c2) fs fs2
| CCases (sty,rtnpo,tms,eqns), CCases (sty2,rtnpo2,tms2,eqns2) ->
constr_expr_opt ogname rtnpo rtnpo2;
iter2 (case_expr ogname) tms tms2;
iter2 (branch_expr ogname) eqns eqns2
| CLetTuple (nal,(na,po),b,c), CLetTuple (nal2,(na2,po2),b2,c2) ->
constr_expr_opt ogname po po2;
constr_expr ogname b b2;
constr_expr ogname c c2
| CIf (c,(na,po),b1,b2), CIf (c2,(na2,po2),b12,b22) ->
constr_expr ogname c c2;
constr_expr_opt ogname po po2;
constr_expr ogname b1 b12;
constr_expr ogname b2 b22
| CHole _, CHole _ -> ()
| CGenarg _, CGenarg _ -> ()
| CPatVar _, CPatVar _ -> ()
| CEvar (n,l), CEvar (n2,l2) ->
let oevar = if ogname = "" then Id.to_string n.CAst.v else ogname in
nevar_to_oevar := CString.Map.add (Id.to_string n2.CAst.v) oevar !nevar_to_oevar;
iter2 (fun x x2 -> let (_, g) = x and (_, g2) = x2 in constr_expr ogname g g2) l l2
| CEvar (n,l), nt' ->
match_goals_r (Id.to_string n.CAst.v) nt' nt'
| CSort s, CSort s2 -> ()
| CCast (c,k,t), CCast (c2,k2,t2) ->
constr_expr ogname c c2;
if not (Option.equal Glob_ops.cast_kind_eq k k2)
then raise (Diff_Failure "Unable to match goals between old and new proof states (4)");
constr_expr ogname t t2
| CNotation (_,ntn,args), CNotation (_,ntn2,args2) ->
constr_notation_substitution ogname args args2
| CGeneralization (b,c), CGeneralization (b2,c2) ->
constr_expr ogname c c2
| CPrim p, CPrim p2 -> ()
| CDelimiters (depth,key,e), CDelimiters (depth2,key2,e2) ->
constr_expr ogname e e2
| CArray(u,t,def,ty), CArray(u2,t2,def2,ty2) ->
constr_arr ogname t t2;
constr_expr ogname def def2;
constr_expr ogname ty ty2;
| _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (5)")
end
in
let () = match_goals_r "" ot nt in
!nevar_to_oevar
let get_proof_context (p : Proof.t) =
let Proof.{goals; sigma} = Proof.data p in
let env = Evd.evar_filtered_env (Global.env ()) (Evd.find_undefined sigma (List.hd goals)) in
sigma, env
let to_constr pf =
let open CAst in
let pprf = Proof.partial_proof pf in
let t = List.hd pprf in
let sigma, env = get_proof_context pf in
let x = Constrextern.extern_constr env sigma t in
x.v
let has_fg_goals pf =
let Proof.{goals} = Proof.data pf in
goals <> []
module GoalMap = Evar.Map
let goal_to_evar g sigma = Id.to_string (Termops.evar_suggested_name (Global.env ()) sigma g)
open Evar.Set
[@@@ocaml.warning "-32"]
let db_goal_map op np ng_to_og =
let pr_goals title prf =
Printf.printf "%s: " title;
let Proof.{goals;sigma} = Proof.data prf in
List.iter (fun g -> Printf.printf "%d -> %s " (Evar.repr g) (goal_to_evar g sigma)) goals;
let gs = diff (Proof.all_goals prf) (List.fold_left (fun s g -> add g s) empty goals) in
List.iter (fun g -> Printf.printf "%d " (Evar.repr g)) (elements gs);
in
pr_goals "New Goals" np;
(match op with
| Some op ->
pr_goals "\nOld Goals" op
| None -> ());
Printf.printf "\nGoal map: ";
GoalMap.iter (fun ng og -> Printf.printf "%d -> %d " (Evar.repr ng) (Evar.repr og)) ng_to_og;
let unmapped = ref (Proof.all_goals np) in
GoalMap.iter (fun ng _ -> unmapped := Evar.Set.remove ng !unmapped) ng_to_og;
if Evar.Set.cardinal !unmapped > 0 then begin
Printf.printf "\nUnmapped goals: ";
Evar.Set.iter (fun ng -> Printf.printf "%d " (Evar.repr ng)) !unmapped
end;
Printf.printf "\n"
[@@@ocaml.warning "+32"]
type goal_map = Evd.evar_map * Evar.t Evar.Map.t
let map_goal g (osigma, map) = match GoalMap.find_opt g map with
| None -> None
| Some g -> Some (make_goal (Global.env ()) osigma g)
let make_goal_map op np =
let open Evar.Set in
let ogs = Proof.all_goals op in
let ngs = Proof.all_goals np in
let rem_gs = diff ogs ngs in
let add_gs = diff ngs ogs in
let ng_to_og = Evar.Set.fold (fun x accu -> GoalMap.add x x accu) (inter ogs ngs) GoalMap.empty in
match Evar.Set.elements rem_gs with
| [] -> ng_to_og
| [hd] ->
Evar.Set.fold (fun x accu -> GoalMap.add x hd accu) add_gs ng_to_og
| elts ->
if Evar.Set.is_empty add_gs ||
not (has_fg_goals np) then ng_to_og
else
let nevar_to_oevar = match_goals (to_constr op) (to_constr np) in
let Proof.{sigma=osigma} = Proof.data op in
let fold accu og = CString.Map.add (goal_to_evar og osigma) og accu in
let oevar_to_og = List.fold_left fold CString.Map.empty elts in
let Proof.{sigma=nsigma} = Proof.data np in
let get_og ng =
let nevar = goal_to_evar ng nsigma in
let oevar = CString.Map.find nevar nevar_to_oevar in
let og = CString.Map.find oevar oevar_to_og in
og
in
let fold ng accu = try GoalMap.add ng (get_og ng) accu with Not_found -> accu in
Evar.Set.fold fold add_gs ng_to_og
let make_goal_map op np =
let map = make_goal_map op np in
((Proof.data op).Proof.sigma, map)
let notify_proof_diff_failure msg =
Feedback.msg_notice Pp.(str "Unable to compute diffs: " ++ str msg)
let diff_proofs ~diff_opt ?old proof =
let pp_proof p =
let sigma, env = Proof.get_proof_context p in
let pprf = Proof.partial_proof p in
Pp.prlist_with_sep Pp.fnl (pr_econstr_env env sigma) pprf in
match diff_opt with
| DiffOff -> pp_proof proof
| _ -> begin
try
let n_pp = pp_proof proof in
let o_pp = match old with
| None -> Pp.mt()
| Some old -> pp_proof old in
let show_removed = Some (diff_opt = DiffRemoved) in
Pp_diff.diff_pp_combined ~tokenize_string ?show_removed o_pp n_pp
with Pp_diff.Diff_Failure msg ->
notify_proof_diff_failure msg;
pp_proof proof
end