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

5 files changed, 351 insertions, 6 deletions

diff --git a/test-suite/unit-tests/clib/inteq.ml b/test-suite/unit-tests/clib/inteq.ml
index c07ec293f0..89717c79d5 100644
--- a/test-suite/unit-tests/clib/inteq.ml
+++ b/test-suite/unit-tests/clib/inteq.ml
@@ -1,5 +1,7 @@
 open Utest
 
+let log_out_ch = open_log_out_ch __FILE__
+
 let eq0 = mk_bool_test "clib-inteq0"
             "Int.equal on 0"
             (Int.equal 0 0)
@@ -10,4 +12,4 @@ let eq42 = mk_bool_test "clib-inteq42"
 
 let tests = [ eq0; eq42 ]
 
-let _ = run_tests __FILE__ tests
+let _ = run_tests __FILE__ log_out_ch tests
diff --git a/test-suite/unit-tests/clib/unicode_tests.ml b/test-suite/unit-tests/clib/unicode_tests.ml
index 9ae405977b..95316ad3aa 100644
--- a/test-suite/unit-tests/clib/unicode_tests.ml
+++ b/test-suite/unit-tests/clib/unicode_tests.ml
@@ -1,5 +1,7 @@
 open Utest
 
+let log_out_ch = open_log_out_ch __FILE__
+
 let unicode0 = mk_eq_test "clib-unicode0"
                  "split_at_first_letter, first letter is character"
                  None
@@ -12,4 +14,4 @@ let unicode1 = mk_eq_test "clib-unicode1"
 
 let tests = [ unicode0; unicode1 ]
 
-let _ = run_tests __FILE__ tests
+let _ = run_tests __FILE__ log_out_ch tests
diff --git a/test-suite/unit-tests/printing/proof_diffs_test.ml b/test-suite/unit-tests/printing/proof_diffs_test.ml
new file mode 100644
index 0000000000..526cefec44
--- /dev/null
+++ b/test-suite/unit-tests/printing/proof_diffs_test.ml
@@ -0,0 +1,333 @@
+open OUnit
+open Utest
+open Pp_diff
+open Proof_diffs
+
+let tokenize_string = Proof_diffs.tokenize_string
+let diff_pp = diff_pp ~tokenize_string
+let diff_str = diff_str ~tokenize_string
+
+let tests = ref []
+let add_test name test = tests := (mk_test name (TestCase test)) :: !tests
+
+let log_out_ch = open_log_out_ch __FILE__
+let cfprintf oc = Printf.(kfprintf (fun oc -> fprintf oc "") oc)
+let cprintf s = cfprintf log_out_ch s
+let _ = Proof_diffs.log_out_ch := log_out_ch
+
+let string_of_string s : string = "\"" ^ s ^ "\""
+
+(* todo: OCaml: why can't the body of the test function be given in the add_test line? *)
+
+let t () =
+  let expected : diff_list = [] in
+  let diffs = diff_str "" "   " in
+
+  assert_equal ~msg:"empty" ~printer:string_of_diffs expected diffs;
+  let (has_added, has_removed) = has_changes diffs in
+  assert_equal ~msg:"has `Added" ~printer:string_of_bool false has_added;
+  assert_equal ~msg:"has `Removed" ~printer:string_of_bool false has_removed
+let _ = add_test "diff_str empty" t
+
+
+let t () =
+  let expected : diff_list =
+    [ `Common (0, 0, "a"); `Common (1, 1, "b"); `Common (2, 2, "c")] in
+  let diffs = diff_str "a b c" " a  b\t  c\n" in
+
+  assert_equal ~msg:"white space" ~printer:string_of_diffs expected diffs;
+  let (has_added, has_removed) = has_changes diffs in
+  assert_equal ~msg:"no `Added" ~printer:string_of_bool false has_added;
+  assert_equal ~msg:"no `Removed" ~printer:string_of_bool false has_removed
+let _ = add_test "diff_str white space" t
+
+let t () =
+  let expected : diff_list = [ `Removed (0, "a"); `Added (0, "b")] in
+  let diffs = diff_str "a" "b" in
+
+  assert_equal ~msg:"add/remove" ~printer:string_of_diffs expected diffs;
+  let (has_added, has_removed) = has_changes diffs in
+  assert_equal ~msg:"has `Added" ~printer:string_of_bool true has_added;
+  assert_equal ~msg:"has `Removed" ~printer:string_of_bool true has_removed
+let _ = add_test "diff_str add/remove" t
+
+(* example of a limitation, not really a test *)
+let t () =
+  try
+    let _ = diff_str "a" ">" in
+    assert_failure "unlexable string gives an exception"
+  with _ -> ()
+let _ = add_test "diff_str unlexable" t
+
+(* problematic examples for tokenize_string:
+   comments omitted
+   quoted string loses quote marks (are escapes supported/handled?)
+   char constant split into 2
+   *)
+let t () =
+  List.iter (fun x -> cprintf "'%s' " x) (tokenize_string "(* comment *) \"string\" 'c' xx");
+  cprintf "\n"
+let _ = add_test "tokenize_string examples" t
+
+open Pp
+
+(* note pp_to_string concatenates adjacent strings, could become one token,
+e.g. str " a" ++ str "b " will give a token "ab" *)
+(* checks background is present and correct *)
+let t () =
+  let o_pp = str "a" ++ str "!" ++ str "c" in
+  let n_pp = str "a" ++ str "?" ++ str "c" in
+  let (o_exp, n_exp) = (wrap_in_bg "diff.removed" (str "a" ++ (tag "diff.removed" (str "!")) ++ str "c"),
+                        wrap_in_bg "diff.added" (str "a" ++ (tag "diff.added" (str "?")) ++ str "c")) in
+  let (o_diff, n_diff) = diff_pp o_pp n_pp in
+
+  assert_equal ~msg:"removed" ~printer:db_string_of_pp o_exp o_diff;
+  assert_equal ~msg:"added"   ~printer:db_string_of_pp n_exp n_diff
+let _ = add_test "diff_pp/add_diff_tags add/remove" t
+
+let t () =
+  (*Printf.printf "%s\n" (string_of_diffs (diff_str "a d" "a b c d"));*)
+  let o_pp = str "a" ++ str " d" in
+  let n_pp = str "a" ++ str " b " ++ str " c " ++ str "d" ++ str " e " in
+  let n_exp = flatten (wrap_in_bg "diff.added" (seq [
+      str "a";
+      str " "; (tag "start.diff.added" (str "b "));
+      (tag "end.diff.added" (str " c")); str " ";
+      (str "d");
+      str " "; (tag "diff.added" (str "e")); str " "
+      ])) in
+  let (_, n_diff) = diff_pp o_pp n_pp in
+
+  assert_equal ~msg:"added"   ~printer:db_string_of_pp n_exp (flatten n_diff);;
+let _ = add_test "diff_pp/add_diff_tags a span with spaces" t
+
+
+let t () =
+  let o_pp = str " " in
+  let n_pp = tag "sometag" (str "a") in
+  let n_exp = flatten (wrap_in_bg "diff.added" (tag "diff.added" (tag "sometag" (str "a")))) in
+  let (_, n_diff) = diff_pp o_pp n_pp in
+
+  assert_equal ~msg:"added"   ~printer:db_string_of_pp n_exp (flatten n_diff)
+let _ = add_test "diff_pp/add_diff_tags diff tags outside existing tags" t
+
+let t () =
+  let o_pp = str " " in
+  let n_pp = seq [(tag "sometag" (str " a ")); str "b"] in
+  let n_exp = flatten (wrap_in_bg "diff.added"
+      (seq [tag "sometag" (str " "); (tag "start.diff.added" (tag "sometag" (str "a ")));
+          (tag "end.diff.added" (str "b"))]) ) in
+  let (_, n_diff) = diff_pp o_pp n_pp in
+
+  assert_equal ~msg:"added"   ~printer:db_string_of_pp n_exp (flatten n_diff)
+let _ = add_test "diff_pp/add_diff_tags existing tagged values with spaces" t
+
+let t () =
+  let o_pp = str " " in
+  let n_pp = str " a b " in
+  let n_exp = flatten (wrap_in_bg "diff.added"
+      (seq [str " "; tag "diff.added" (str "a b"); str " "])) in
+  let (_, n_diff) = diff_pp o_pp n_pp in
+
+  assert_equal ~msg:"added"   ~printer:db_string_of_pp n_exp (flatten n_diff)
+let _ = add_test "diff_pp/add_diff_tags multiple tokens in pp" t
+
+let t () =
+  let o_pp = str "a d" in
+  let n_pp = seq [str "a b"; str "c d"] in
+  let n_exp = flatten (wrap_in_bg "diff.added"
+      (seq [str "a "; tag "start.diff.added" (str "b");
+            tag "end.diff.added" (str "c"); str " d"])) in
+  let (_, n_diff) = diff_pp o_pp n_pp in
+
+  assert_equal ~msg:"added"   ~printer:db_string_of_pp n_exp (flatten n_diff)
+let _ = add_test "diff_pp/add_diff_tags token spanning multiple Ppcmd_strs" t
+
+let t () =
+  let o_pp = seq [str ""; str "a"] in
+  let n_pp = seq [str ""; str "a b"] in
+  let n_exp = flatten (wrap_in_bg "diff.added"
+      (seq [str ""; str "a "; tag "diff.added" (str "b")])) in
+  let (_, n_diff) = diff_pp o_pp n_pp in
+
+  assert_equal ~msg:"added"   ~printer:db_string_of_pp n_exp (flatten n_diff)
+let _ = add_test "diff_pp/add_diff_tags empty string preserved" t
+
+(* todo: awaiting a change in the lexer to return the quotes of the string token *)
+let t () =
+  let s = "\"a b\"" in
+  let o_pp = seq [str s] in
+  let n_pp = seq [str "\"a b\" "] in
+  cprintf "ppcmds: %s\n" (string_of_ppcmds n_pp);
+  let n_exp = flatten (wrap_in_bg "diff.added"
+      (seq [str ""; str "a "; tag "diff.added" (str "b")])) in
+  let (_, n_diff) = diff_pp o_pp n_pp in
+
+  assert_equal ~msg:"string" ~printer:string_of_string "a b" (List.hd (tokenize_string s));
+  assert_equal ~msg:"added"   ~printer:db_string_of_pp n_exp (flatten n_diff)
+let _ = if false then add_test "diff_pp/add_diff_tags token containing white space" t
+
+let add_entries map idents rhs_pp =
+  let make_entry() = { idents; rhs_pp; done_ = false } in
+  List.iter (fun ident -> map := (StringMap.add ident (make_entry ()) !map); ()) idents;;
+
+let print_list hyps = List.iter (fun x -> cprintf "%s\n" (string_of_ppcmds (flatten x))) hyps
+let db_print_list hyps = List.iter (fun x -> cprintf "%s\n" (db_string_of_pp (flatten x))) hyps
+
+
+(* a : foo
+   b : bar car ->
+   b : car
+   a : foo bar *)
+let t () =
+  write_diffs_option "removed";   (* turn on "removed" option *)
+  let o_line_idents = [ ["a"]; ["b"]] in
+  let o_hyp_map = ref StringMap.empty in
+  add_entries o_hyp_map ["a"] (str " : foo");
+  add_entries o_hyp_map ["b"] (str " : bar car");
+  let n_line_idents = [ ["b"]; ["a"]] in
+  let n_hyp_map = ref StringMap.empty in
+  add_entries n_hyp_map ["b"] (str " : car");
+  add_entries n_hyp_map ["a"] (str " : foo bar");
+  let expected = [flatten (wrap_in_bg "diff.removed" (seq [str "b"; str " : "; (tag "diff.removed" (str "bar")); str " car" ]));
+                  flatten (wrap_in_bg "diff.added" (seq [str "b"; str " : car" ]));
+                  flatten (wrap_in_bg "diff.added" (seq [str "a"; str " : foo "; (tag "diff.added" (str "bar")) ]))
+  ] in
+
+  let hyps_diff_list = diff_hyps o_line_idents !o_hyp_map n_line_idents !n_hyp_map in
+
+  (*print_list hyps_diff_list;*)
+  (*db_print_list hyps_diff_list;*)
+
+  List.iter2 (fun exp act ->
+      assert_equal ~msg:"added"   ~printer:db_string_of_pp exp (flatten act))
+      expected hyps_diff_list
+let _ = add_test "diff_hyps simple diffs" t
+
+(* a : nat
+  c, d : int ->
+  a, b : nat
+  d : int
+ and keeps old order *)
+let t () =
+  write_diffs_option "removed";   (* turn on "removed" option *)
+  let o_line_idents = [ ["a"]; ["c"; "d"]] in
+  let o_hyp_map = ref StringMap.empty in
+  add_entries o_hyp_map ["a"] (str " : nat");
+  add_entries o_hyp_map ["c"; "d"] (str " : int");
+  let n_line_idents = [ ["a"; "b"]; ["d"]] in
+  let n_hyp_map = ref StringMap.empty in
+  add_entries n_hyp_map ["a"; "b"] (str " : nat");
+  add_entries n_hyp_map ["d"] (str " : int");
+  let expected = [flatten (wrap_in_bg "diff.added" (seq [str "a"; (tag "start.diff.added" (str ", ")); (tag "end.diff.added" (str "b")); str " : nat" ]));
+                  flatten (wrap_in_bg "diff.removed" (seq [(tag "start.diff.removed" (str "c"));  (tag "end.diff.removed" (str ",")); str " "; str "d";  str " : int" ]));
+                  flatten (wrap_in_bg "diff.added" (seq [str "d"; str " : int" ]))
+  ] in
+
+  let hyps_diff_list = diff_hyps o_line_idents !o_hyp_map n_line_idents !n_hyp_map in
+
+  (*print_list hyps_diff_list;*)
+  (*print_list expected;*)
+
+  (*db_print_list hyps_diff_list;*)
+  (*db_print_list expected;*)
+
+  List.iter2 (fun exp act ->
+      assert_equal ~msg:"added"   ~printer:db_string_of_pp exp (flatten act))
+      expected hyps_diff_list
+let _ = add_test "diff_hyps compacted" t
+
+(* a : foo
+   b : bar
+   c : nat ->
+   b, a, c : nat
+DIFFS
+   b : bar (remove bar)
+   b : nat (add nat)
+   a : foo (remove foo)
+   a : nat (add nat)
+   c : nat
+ is this a realistic use case?
+*)
+let t () =
+  write_diffs_option "removed";   (* turn on "removed" option *)
+  let o_line_idents = [ ["a"]; ["b"]; ["c"]] in
+  let o_hyp_map = ref StringMap.empty in
+  add_entries o_hyp_map ["a"] (str " : foo");
+  add_entries o_hyp_map ["b"] (str " : bar");
+  add_entries o_hyp_map ["c"] (str " : nat");
+  let n_line_idents = [ ["b"; "a"; "c"] ] in
+  let n_hyp_map = ref StringMap.empty in
+  add_entries n_hyp_map ["b"; "a"; "c"] (str " : nat");
+  let expected = [flatten (wrap_in_bg "diff.removed" (seq [str "b"; str " : "; (tag "diff.removed" (str "bar"))]));
+                  flatten (wrap_in_bg "diff.added" (seq [str "b"; str " : "; (tag "diff.added" (str "nat"))]));
+                  flatten (wrap_in_bg "diff.removed" (seq [str "a"; str " : "; (tag "diff.removed" (str "foo"))]));
+                  flatten (wrap_in_bg "diff.added" (seq [str "a"; str " : "; (tag "diff.added" (str "nat"))]));
+                  flatten (seq [str "c"; str " : nat"])
+  ] in
+
+  let hyps_diff_list = diff_hyps o_line_idents !o_hyp_map n_line_idents !n_hyp_map in
+
+  (*print_list hyps_diff_list;*)
+  (*db_print_list hyps_diff_list;*)
+
+  List.iter2 (fun exp act ->
+      assert_equal ~msg:"added"   ~printer:db_string_of_pp exp (flatten act))
+      expected hyps_diff_list
+let _ = add_test "diff_hyps compacted with join" t
+
+(* b, a, c : nat ->
+   a : foo
+   b : bar
+   c : nat
+DIFFS
+   a : nat (remove nat)
+   a : foo (add foo)
+   b : nat (remove nat)
+   b : bar (add bar)
+   c : nat
+ is this a realistic use case? *)
+let t () =
+  write_diffs_option "removed";   (* turn on "removed" option *)
+  let o_line_idents = [ ["b"; "a"; "c"] ] in
+  let o_hyp_map = ref StringMap.empty in
+  add_entries o_hyp_map ["b"; "a"; "c"] (str " : nat");
+  let n_line_idents = [ ["a"]; ["b"]; ["c"]] in
+  let n_hyp_map = ref StringMap.empty in
+  add_entries n_hyp_map ["a"] (str " : foo");
+  add_entries n_hyp_map ["b"] (str " : bar");
+  add_entries n_hyp_map ["c"] (str " : nat");
+  let expected = [flatten (wrap_in_bg "diff.removed" (seq [str "a"; str " : "; (tag "diff.removed" (str "nat"))]));
+                  flatten (wrap_in_bg "diff.added" (seq [str "a"; str " : "; (tag "diff.added" (str "foo"))]));
+                  flatten (wrap_in_bg "diff.removed" (seq [str "b"; str " : "; (tag "diff.removed" (str "nat"))]));
+                  flatten (wrap_in_bg "diff.added" (seq [str "b"; str " : "; (tag "diff.added" (str "bar"))]));
+                  flatten (seq [str "c"; str " : nat"])
+  ] in
+
+  let hyps_diff_list = diff_hyps o_line_idents !o_hyp_map n_line_idents !n_hyp_map in
+
+  (*print_list hyps_diff_list;*)
+  (*db_print_list hyps_diff_list;*)
+
+  List.iter2 (fun exp act ->
+      assert_equal ~msg:"added"   ~printer:db_string_of_pp exp (flatten act))
+      expected hyps_diff_list
+let _ = add_test "diff_hyps compacted with split" t
+
+
+(* other potential tests
+coqtop/terminal formatting BLOCKED: CAN'T GET TAGS IN FORMATTER
+  white space at end of line
+  spanning diffs
+shorten_diff_span
+
+MAYBE NOT WORTH IT
+diff_pp/add_diff_tags
+  add/remove - show it preserves, recurs and processes:
+    nested in boxes
+    breaks, etc.  preserved
+diff_pp_combined with/without removed
+*)
+
+
+let _ = run_tests __FILE__ log_out_ch (List.rev !tests)
diff --git a/test-suite/unit-tests/src/utest.ml b/test-suite/unit-tests/src/utest.ml
index 069e6a4bf3..0cb1780ec9 100644
--- a/test-suite/unit-tests/src/utest.ml
+++ b/test-suite/unit-tests/src/utest.ml
@@ -42,10 +42,12 @@ let run_one logit test =
   let results = perform_test (fun _ -> ()) test in
   process_results results
 
-(* run list of OUnit test cases, log results *)
-let run_tests ml_fn tests =
+let open_log_out_ch ml_fn =
   let log_fn = ml_fn ^ ".log" in
-  let out_ch = open_out log_fn in
+  open_out log_fn
+
+(* run list of OUnit test cases, log results *)
+let run_tests ml_fn out_ch tests =
   let cprintf s = cfprintf out_ch s in
   let ceprintf s = cfprintf stderr s in
   let logit = logger out_ch in
diff --git a/test-suite/unit-tests/src/utest.mli b/test-suite/unit-tests/src/utest.mli
index 70928228bf..2e0f26e96b 100644
--- a/test-suite/unit-tests/src/utest.mli
+++ b/test-suite/unit-tests/src/utest.mli
@@ -9,4 +9,10 @@ val mk_bool_test : string -> string -> bool -> OUnit.test
 (* the string argument should be the name of the .ml file
    containing the tests; use __FILE__ for that purpose.
  *)
-val run_tests : string -> OUnit.test list -> unit
+val run_tests : string -> out_channel -> OUnit.test list -> unit
+
+(** open output channel for the test log file *)
+(* the string argument should be the name of the .ml file
+   containing the tests; use __FILE__ for that purpose.
+ *)
+val open_log_out_ch : string -> out_channel