Merge PR #6801: Highlight differences between successive proof steps (color, underline, etc.)

1 files changed, 339 insertions, 0 deletions

diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
new file mode 100644
index 0000000000..7131ced15b
--- /dev/null
+++ b/printing/proof_diffs.ml
@@ -0,0 +1,339 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(*
+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.  See pp_diff.ml for details on how
+the diff works.
+
+Diffs are computed for the hypotheses and conclusion of the first goal between
+the old and new proofs.
+
+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.
+
+In CoqIDE, colors and highlights can be set in the Edit/Preferences/Tags panel.
+For coqtop, these can be set through the COQ_COLORS environment variable.
+
+Limitations/Possible enhancements:
+
+- If you go back to a prior proof step, diffs are not shown on the new current
+step.  Diffs will be shown again once you do another proof step.
+
+- Diffs are done between the first active goal in the old and new proofs.
+If, for example, the proof step completed a goal, then the new goal is a
+different goal, not a transformation of the old goal, so a diff is probably
+not appropriate.  (There's currently no way to tell when this happens or to
+accurately match goals across old and new proofs.
+See https://github.com/coq/coq/issues/7653)  This is also why only the
+first goal is diffed.
+
+- "Set Diffs "xx"." should reprint the current goal using the new option.
+
+- coqtop colors were chosen for white text on a black background.  They're
+not the greatest.  I didn't want to change the existing green highlight.
+Suggestions welcome.
+
+- coqtop underlines removed text because (per Wikipedia) the ANSI escape code
+for strikeout is not commonly supported (it didn't work on mine).  CoqIDE
+uses strikeout on removed text.
+*)
+
+open Pp_diff
+
+let diff_option = ref `OFF
+
+(* todo: Is there a way to persist the setting between sessions?
+   Eg if the user wants this as a permanent config setting? *)
+let read_diffs_option () = match !diff_option with
+| `OFF -> "off"
+| `ON -> "on"
+| `REMOVED -> "removed"
+
+let write_diffs_option = function
+| "off" -> diff_option := `OFF
+| "on" -> diff_option := `ON
+| "removed" -> diff_option := `REMOVED
+| _ -> CErrors.user_err Pp.(str "Diffs option only accepts the following values: \"off\", \"on\", \"removed\".")
+
+let _ =
+  Goptions.(declare_string_option {
+    optdepr = false;
+    optname = "show diffs in proofs";
+    optkey = ["Diffs"];
+    optread = read_diffs_option;
+    optwrite = write_diffs_option
+  })
+
+let show_diffs () = !diff_option <> `OFF;;
+let show_removed () = !diff_option = `REMOVED;;
+
+
+(* DEBUG/UNIT TEST *)
+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"]
+
+module StringMap = Map.Make(String);;
+
+let tokenize_string s =
+  (* todo: cLexer changes buff as it proceeds.  Seems like that should be saved, too.
+  But I don't understand how it's used--it looks like things get appended to it but
+  it never gets cleared. *)
+  let rec stream_tok acc str =
+    let e = Stream.next str in
+    if Tok.(equal e EOI) then
+      List.rev acc
+    else
+      stream_tok ((Tok.extract_string e) :: acc) str
+  in
+  let st = CLexer.get_lexer_state () in
+  try
+    let istr = Stream.of_string s in
+    let lex = CLexer.lexer.Plexing.tok_func istr in
+    let toks = stream_tok [] (fst lex) in
+    CLexer.set_lexer_state st;
+    toks
+  with exn ->
+    CLexer.set_lexer_state st;
+    raise (Diff_Failure "Input string is not lexable");;
+
+
+type hyp_info = {
+  idents: string list;
+  rhs_pp: Pp.t;
+  mutable done_: bool;
+}
+
+(* Generate the diffs between the old and new hyps.
+   This works by matching lines with the hypothesis name and diffing the right-hand side.
+   Lines that have multiple names such as "n, m : nat" are handled specially to account
+   for, say, the addition of m to a pre-existing "n : nat".
+ *)
+let diff_hyps o_line_idents o_map n_line_idents n_map =
+  let rv : Pp.t list ref = ref [] in
+
+  let is_done ident map = (StringMap.find ident map).done_ in
+  let exists ident map =
+    try let _ = StringMap.find ident map in true
+    with Not_found -> false in
+  let contains l ident = try [List.find (fun x  -> x = ident) l] with Not_found -> [] in
+
+  let output old_ids_uo new_ids =
+    (* use the order from the old line in case it's changed in the new *)
+    let old_ids = if old_ids_uo = [] then [] else
+      let orig = (StringMap.find (List.hd old_ids_uo) o_map).idents in
+      List.concat (List.map (contains orig) old_ids_uo) in
+
+    let setup ids map = if ids = [] then ("", Pp.mt ()) else
+      let open Pp in
+      let rhs_pp = (StringMap.find (List.hd ids) map).rhs_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) ++ rhs_pp in
+      (string_of_ppcmds hyp_pp, hyp_pp)
+    in
+
+    let (o_line, o_pp) = setup old_ids o_map in
+    let (n_line, n_pp) = setup new_ids n_map in
+
+    let hyp_diffs = diff_str ~tokenize_string o_line n_line in
+    let (has_added, has_removed) = has_changes hyp_diffs in
+    if show_removed () && has_removed then begin
+      let o_entry = StringMap.find (List.hd old_ids) o_map in
+      o_entry.done_ <- true;
+      rv := (add_diff_tags `Removed o_pp hyp_diffs) :: !rv;
+    end;
+    if n_line <> "" then begin
+      let n_entry = StringMap.find (List.hd new_ids) n_map in
+      n_entry.done_ <- true;
+      rv := (add_diff_tags `Added n_pp hyp_diffs) :: !rv
+    end
+  in
+
+  (* process identifier level diff *)
+  let process_ident_diff diff =
+    let (dtype, ident) = get_dinfo diff in
+    match dtype with
+    | `Removed ->
+      if dtype = `Removed then begin
+        let o_idents = (StringMap.find ident o_map).idents in
+        (* only show lines that have all idents removed here; other removed idents appear later *)
+        if show_removed () &&
+            List.for_all (fun x -> not (exists x n_map)) o_idents then
+          output (List.rev o_idents) []
+      end
+    | _ -> begin (* Added or Common case *)
+      let n_idents = (StringMap.find ident n_map).idents in
+
+      (* Process a new hyp line, possibly splitting it.  Duplicates some of
+         process_ident iteration, but easier to understand this way *)
+      let process_line ident2 =
+        if not (is_done ident2 n_map) then begin
+          let n_ids_list : string list ref = ref [] in
+          let o_ids_list : string list ref = ref [] in
+          let fst_omap_idents = ref None in
+          let add ids id map =
+            ids := id :: !ids;
+            (StringMap.find id map).done_ <- true in
+
+          (* get identifiers shared by one old and one new line, plus
+             other Added in new and other Removed in old *)
+          let process_split ident3 =
+            if not (is_done ident3 n_map) then begin
+              let this_omap_idents = try Some (StringMap.find ident3 o_map).idents
+                                    with Not_found -> None in
+              if !fst_omap_idents = None then
+                fst_omap_idents := this_omap_idents;
+              match (!fst_omap_idents, this_omap_idents) with
+              | (Some fst, Some this) when fst == this ->  (* yes, == *)
+                add n_ids_list ident3 n_map;
+                (* include, in old order, all undone Removed idents in old *)
+                List.iter (fun x -> if x = ident3 || not (is_done x o_map) && not (exists x n_map) then
+                                    (add o_ids_list x o_map)) fst
+              | (_, None) ->
+                add n_ids_list ident3 n_map (* include all undone Added idents in new *)
+              | _ -> ()
+            end in
+          List.iter process_split n_idents;
+          output (List.rev !o_ids_list) (List.rev !n_ids_list)
+        end in
+      List.iter process_line n_idents (* O(n^2), so sue me *)
+    end in
+
+  let cvt s = Array.of_list (List.concat s) in
+  let ident_diffs = diff_strs (cvt o_line_idents) (cvt n_line_idents) in
+  List.iter process_ident_diff ident_diffs;
+  List.rev !rv;;
+
+
+type 'a hyp = (Names.Id.t list * 'a option * 'a)
+type 'a reified_goal = { name: string; ty: 'a; hyps: 'a hyp list; env : Environ.env; sigma: Evd.evar_map }
+
+(* XXX: Port to proofview, one day. *)
+(* open Proofview *)
+module CDC = Context.Compacted.Declaration
+
+let to_tuple : Constr.compacted_declaration -> (Names.Id.t list * 'pc option * 'pc) =
+  let open CDC in function
+    | LocalAssum(idl, tm)   -> (idl, None, tm)
+    | LocalDef(idl,tdef,tm) -> (idl, Some tdef, tm);;
+
+(* XXX: Very unfortunately we cannot use the Proofview interface as
+   Proof is still using the "legacy" one. *)
+let process_goal sigma g : Constr.t reified_goal =
+  let env  = Goal.V82.env   sigma g in
+  let hyps = Goal.V82.hyps  sigma g in
+  let ty   = Goal.V82.concl sigma g in
+  let name = Goal.uid g             in
+  (* There is a Constr/Econstr mess here... *)
+  let ty   = EConstr.to_constr sigma ty in
+  (* compaction is usually desired [eg for better display] *)
+  let hyps      = Termops.compact_named_context (Environ.named_context_of_val hyps) in
+  let hyps      = List.map to_tuple hyps in
+  { name; ty; hyps; env; sigma };;
+
+let pr_letype_core goal_concl_style env sigma t =
+  Ppconstr.pr_lconstr_expr (Constrextern.extern_type goal_concl_style env sigma t)
+
+let pp_of_type env sigma ty =
+  pr_letype_core true env sigma EConstr.(of_constr ty)
+
+(* fetch info from a goal, returning (idents, map, concl_pp) where
+idents is a list with one entry for each hypothesis, each entry is the list of
+idents on the lhs of the hypothesis.  map is a map from ident to hyp_info
+reoords.  For example: for the hypotheses:
+  b : bool
+  n, m : nat
+
+list will be [ ["b"]; ["n"; "m"] ]
+
+map will contain:
+  "b" -> { ["b"], Pp.t for ": bool"; false }
+  "n" -> { ["n"; "m"], Pp.t for ": nat"; false }
+  "m" -> { ["n"; "m"], Pp.t for ": nat"; false }
+ where the last two entries share the idents list.
+
+concl_pp is the conclusion as a Pp.t
+*)
+let goal_info goal sigma =
+  let map = ref StringMap.empty in
+  let line_idents = ref [] in
+  let build_hyp_info env sigma hyp =
+    let (names, body, ty) = hyp in
+    let open Pp in
+    let idents = List.map (fun x -> Names.Id.to_string x) names in
+
+    line_idents := idents :: !line_idents;
+    let mid = match body with
+    | Some x -> str " := " ++ pp_of_type env sigma ty ++ str " : "
+    | None -> str " : " in
+    let ts = pp_of_type env sigma ty in
+    let rhs_pp = mid ++ ts in
+
+    let make_entry () = { idents; rhs_pp; done_ = false } in
+    List.iter (fun ident -> map := (StringMap.add ident (make_entry ()) !map); ()) idents
+  in
+
+  try
+    let { ty=ty; hyps=hyps; env=env } = process_goal sigma goal in
+    List.iter (build_hyp_info env sigma) (List.rev hyps);
+    let concl_pp = pp_of_type env sigma ty in
+    ( List.rev !line_idents, !map, concl_pp )
+  with _ -> ([], !map, Pp.mt ());;
+
+let diff_goal_info o_info n_info =
+  let (o_line_idents, o_hyp_map, o_concl_pp) = o_info in
+  let (n_line_idents, 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 = diff_hyps o_line_idents o_hyp_map n_line_idents n_hyp_map in
+  (hyp_diffs_list, concl_pp)
+
+let hyp_list_to_pp hyps =
+  let open Pp in
+  match hyps with
+  | h :: tl -> List.fold_left (fun x y -> x ++ cut () ++ y) h tl
+  | [] -> mt ();;
+
+(* Special purpuse, use only for the IDE interface,  *)
+let diff_first_goal o_proof n_proof =
+  let first_goal_info proof =
+    match proof with
+    | None -> ([], StringMap.empty, Pp.mt ())
+    | Some proof2 ->
+      let (goals,_,_,_,sigma) = Proof.proof proof2 in
+      match goals with
+      | hd :: tl -> goal_info hd sigma;
+      | _ -> ([], StringMap.empty, Pp.mt ())
+  in
+  diff_goal_info (first_goal_info o_proof) (first_goal_info n_proof);;
+
+let diff_goals ?prev_gs n_gs =
+  let unwrap gs =
+    match gs with
+    | Some gs ->
+      let goal = Evd.sig_it gs in
+      let sigma = Refiner.project gs in
+      goal_info goal sigma
+    | None -> ([], StringMap.empty, Pp.mt ())
+  in
+  let (hyps_pp_list, concl_pp) = diff_goal_info (unwrap prev_gs) (unwrap n_gs) in
+  let open Pp in
+  v 0 (
+    (hyp_list_to_pp hyps_pp_list) ++ cut () ++
+    str "============================" ++ cut () ++
+    concl_pp);;