From 8de046df97b1ea391a3f3879c20c74d53c9fba48 Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Mon, 9 Apr 2018 13:16:46 -0700 Subject: Displays the differences between successive proof steps in coqtop and CoqIDE. Proof General requires minor changes to make the diffs visible, but this code shouldn't break the existing version of PG. Diffs are computed for the hypotheses and conclusion of the first goal between the old and new proofs. Strings are split into tokens using the Coq lexer, then the list of tokens are diffed using the Myers algorithm. A fixup routine (Pp_diff.shorten_diff_span) shortens the span of the diff result in some cases. Diffs can be enabled with the Coq commmand "Set Diffs on|off|removed." or "-diffs on|off|removed" on the OS command line. The "on" option shows only the new item with added text, while "removed" shows each modified item twice--once with the old value showing removed text and once with the new value showing added text. The highlights use 4 tags to specify the color and underline/strikeout. These are "diffs.added", "diffs.removed", "diffs.added.bg" and "diffs.removed.bg". The first two are for added or removed text; the last two are for unmodified parts of a modified item. Diffs that span multiple strings in the Pp are tagged with "start.diff.*" and "end.diff.*", but only on the first and last strings of the span. --- printing/printer.ml | 88 +++++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 72 insertions(+), 16 deletions(-) (limited to 'printing/printer.ml') diff --git a/printing/printer.ml b/printing/printer.ml index 92224c992c..ba094596ff 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -493,16 +493,23 @@ let pr_transparent_state (ids, csts) = hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++ str"CONSTANTS: " ++ pr_cpred csts ++ fnl ()) -(* display complete goal *) -let pr_goal gs = +(* display complete goal + prev_gs has info on the previous proof step for diffs + gs has info on the current proof step + *) +let pr_goal ?(diffs=false) ?prev_gs gs = let g = sig_it gs in let sigma = project gs in let env = Goal.V82.env sigma g in let concl = Goal.V82.concl sigma g in let goal = - pr_context_of env sigma ++ cut () ++ - str "============================" ++ cut () ++ - pr_goal_concl_style_env env sigma concl in + if diffs then + Proof_diffs.diff_goals ?prev_gs (Some gs) + else + pr_context_of env sigma ++ cut () ++ + str "============================" ++ cut () ++ + pr_goal_concl_style_env env sigma concl + in str " " ++ v 0 goal (* display a goal tag *) @@ -695,7 +702,8 @@ let print_dependent_evars gl sigma seeds = (* spiwack: [seeds] is for printing dependent evars in emacs mode. *) (* spiwack: [pr_first] is true when the first goal must be singled out and printed in its entirety. *) -let pr_subgoals ?(pr_first=true) +(* [prev] is the previous proof step, used for diffs *) +let pr_subgoals ?(pr_first=true) ?(diffs=false) ?prev close_cmd sigma ~seeds ~shelf ~stack ~unfocused ~goals = (** Printing functions for the extra informations. *) let rec print_stack a = function @@ -729,7 +737,7 @@ let pr_subgoals ?(pr_first=true) if needed then str" focused " else str" " (* non-breakable space *) in - (** Main function *) + let rec pr_rec n = function | [] -> (mt ()) | g::rest -> @@ -739,7 +747,14 @@ let pr_subgoals ?(pr_first=true) in let print_multiple_goals g l = if pr_first then - pr_goal { it = g ; sigma = sigma; } + let prev_gs = + match prev with + | Some (prev_goals, prev_sigma) -> + if prev_goals = [] then None + else Some { it = List.hd prev_goals; sigma = prev_sigma} + | None -> None + in + pr_goal ~diffs ?prev_gs { it = g ; sigma = sigma } ++ (if l=[] then mt () else cut ()) ++ pr_rec 2 l else @@ -751,6 +766,8 @@ let pr_subgoals ?(pr_first=true) | Some cmd -> Feedback.msg_info cmd | None -> () in + + (** Main function *) match goals with | [] -> begin @@ -780,7 +797,7 @@ let pr_subgoals ?(pr_first=true) ++ print_dependent_evars (Some g1) sigma seeds ) -let pr_open_subgoals ~proof = +let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?prev_proof proof = (* spiwack: it shouldn't be the job of the printer to look up stuff in the [evar_map], I did stuff that way because it was more straightforward, but seriously, [Proof.proof] should return @@ -803,21 +820,33 @@ let pr_open_subgoals ~proof = fnl () ++ pr_subgoals ~pr_first:false None bsigma ~seeds ~shelf:[] ~stack:[] ~unfocused:[] ~goals:shelf | _ , _, _ -> - let end_cmd = - str "This subproof is complete, but there are some unfocused goals." ++ - (let s = Proof_bullet.suggest p in - if Pp.ismt s then s else fnl () ++ s) ++ - fnl () + let cmd = if quiet then None else + Some + (str "This subproof is complete, but there are some unfocused goals." ++ + (let s = Proof_bullet.suggest p in + if Pp.ismt s then s else fnl () ++ s) ++ + fnl ()) in - pr_subgoals ~pr_first:false (Some end_cmd) bsigma ~seeds ~shelf ~stack:[] ~unfocused:[] ~goals:bgoals + pr_subgoals ~pr_first:false cmd bsigma ~seeds ~shelf ~stack:[] ~unfocused:[] ~goals:bgoals end | _ -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in let bgoals_focused, bgoals_unfocused = List.partition (fun x -> List.mem x goals) bgoals in let unfocused_if_needed = if should_unfoc() then bgoals_unfocused else [] in - pr_subgoals ~pr_first:true None bsigma ~seeds ~shelf ~stack:[] ~unfocused:unfocused_if_needed ~goals:bgoals_focused + let prev = match prev_proof with + | Some op -> + let (ogoals , _, _, _, _) = Proof.proof op in + let { Evd.it = obgoals; sigma = osigma } = Proof.V82.background_subgoals op in + let obgoals_focused = List.filter (fun x -> List.mem x ogoals) obgoals in + Some (obgoals_focused, osigma) + | None -> None + in + pr_subgoals ~pr_first:true ~diffs ?prev None bsigma ~seeds ~shelf ~stack:[] ~unfocused:unfocused_if_needed ~goals:bgoals_focused end +let pr_open_subgoals ~proof = + pr_open_subgoals_diff proof + let pr_nth_open_subgoal ~proof n = let gls,_,_,_,sigma = Proof.proof proof in pr_subgoal n sigma gls @@ -990,3 +1019,30 @@ let pr_polymorphic b = let pr_universe_instance evd ctx = let inst = Univ.UContext.instance ctx in str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}" + +(* print the proof step, possibly with diffs highlighted, *) +let print_and_diff oldp newp = + match newp with + | None -> () + | Some proof -> + let output = + if Proof_diffs.show_diffs () then + try pr_open_subgoals_diff ~diffs:true ?prev_proof:oldp proof + with Pp_diff.Diff_Failure msg -> begin + (* todo: print the unparsable string (if we know it) *) + Feedback.msg_warning Pp.(str ("Diff failure:" ^ msg ^ "; showing results without diff highlighting" )); + pr_open_subgoals ~proof + end + else + pr_open_subgoals ~proof + in + Feedback.msg_notice output;; + +(* Do diffs on the first goal returning a Pp. *) +let diff_pr_open_subgoals ?(quiet=false) o_proof n_proof = + match n_proof with + | None -> Pp.mt () + | Some proof -> + try pr_open_subgoals_diff ~quiet ~diffs:true ?prev_proof:o_proof proof + with Pp_diff.Diff_Failure _ -> pr_open_subgoals ~proof + (* todo: print the unparsable string (if we know it) *) -- cgit v1.2.3