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

5 files changed, 301 insertions, 14 deletions

diff --git a/clib/clib.mllib b/clib/clib.mllib
index afece4074c..5a2c9a9ce9 100644
--- a/clib/clib.mllib
+++ b/clib/clib.mllib
@@ -37,3 +37,5 @@ Backtrace
 IStream
 Terminal
 Monad
+
+Diff2
diff --git a/clib/diff2.ml b/clib/diff2.ml
new file mode 100644
index 0000000000..42c4733fed
--- /dev/null
+++ b/clib/diff2.ml
@@ -0,0 +1,158 @@
+(* copied from https://github.com/leque/ocaml-diff.git and renamed from "diff.ml" *)
+
+(*
+ * Copyright (C) 2016 OOHASHI Daichi
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+ * The above copyright notice and this permission notice shall be included in
+ * all copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+ * THE SOFTWARE.
+ *)
+
+type 'a common =
+  [ `Common of int * int * 'a ]
+
+type 'a edit =
+  [ `Added of int * 'a
+  | `Removed of int * 'a
+  | 'a common
+  ]
+
+module type SeqType = sig
+  type t
+  type elem
+  val get : t -> int -> elem
+  val length : t -> int
+end
+
+module type S = sig
+  type t
+  type elem
+
+  val lcs :
+      ?equal:(elem -> elem -> bool) ->
+      t -> t -> elem common list
+
+  val diff :
+      ?equal:(elem -> elem -> bool) ->
+      t -> t -> elem edit list
+
+  val fold_left :
+      ?equal:(elem -> elem -> bool) ->
+      f:('a -> elem edit -> 'a) ->
+      init:'a ->
+      t -> t -> 'a
+
+  val iter :
+      ?equal:(elem -> elem -> bool) ->
+      f:(elem edit -> unit) ->
+      t -> t -> unit
+end
+
+module Make(M : SeqType) : (S with type t = M.t and type elem = M.elem) = struct
+  type t = M.t
+  type elem = M.elem
+
+  let lcs ?(equal = (=)) a b =
+    let n = M.length a in
+    let m = M.length b in
+    let mn = m + n in
+    let sz = 2 * mn + 1 in
+    let vd = Array.make sz 0 in
+    let vl = Array.make sz 0 in
+    let vr = Array.make sz [] in
+    let get v i = Array.get v (i + mn) in
+    let set v i x = Array.set v (i + mn) x in
+    let finish () =
+      let rec loop i maxl r =
+        if i > mn then
+          List.rev r
+        else if get vl i > maxl then
+          loop (i + 1) (get vl i) (get vr i)
+        else
+          loop (i + 1) maxl r
+      in loop (- mn) 0 []
+    in
+    if mn = 0 then
+      []
+    else
+      (* For d <- 0 to mn Do *)
+      let rec dloop d =
+        assert (d <= mn);
+        (* For k <- -d to d in steps of 2 Do *)
+        let rec kloop k =
+          if k > d then
+            dloop @@ d + 1
+          else
+            let x, l, r =
+              if k = -d || (k <> d && get vd (k - 1) < get vd (k + 1)) then
+                get vd (k + 1), get vl (k + 1), get vr (k + 1)
+              else
+                get vd (k - 1) + 1, get vl (k - 1), get vr (k - 1)
+            in
+            let x, y, l, r =
+              let rec xyloop x y l r =
+                if x < n && y < m && equal (M.get a x) (M.get b y) then
+                  xyloop (x + 1) (y + 1) (l + 1) (`Common(x, y, M.get a x) :: r)
+                else
+                  x, y, l, r
+              in xyloop x (x - k) l r
+            in
+            set vd k x;
+            set vl k l;
+            set vr k r;
+            if x >= n && y >= m then
+              (* Stop *)
+              finish ()
+            else
+              kloop @@ k + 2
+        in kloop @@ -d
+      in dloop 0
+
+  let fold_left ?(equal = (=)) ~f ~init a b =
+    let ff x y = f y x in
+    let fold_map f g x from to_ init =
+      let rec loop i init =
+        if i >= to_ then
+          init
+        else
+          loop (i + 1) (f (g i @@ M.get x i) init)
+      in loop from init
+    in
+    let added i x = `Added (i, x) in
+    let removed i x = `Removed (i, x) in
+    let rec loop cs apos bpos init =
+      match cs with
+      | [] ->
+          init
+          |> fold_map ff removed a apos (M.length a)
+          |> fold_map ff added b bpos (M.length b)
+      | `Common (aoff, boff, _) as e :: rest ->
+          init
+          |> fold_map ff removed a apos aoff
+          |> fold_map ff added b bpos boff
+          |> ff e
+          |> loop rest (aoff + 1) (boff + 1)
+    in loop (lcs ~equal a b) 0 0 init
+
+  let diff ?(equal = (=)) a b =
+    fold_left ~equal ~f:(fun xs x -> x::xs) ~init:[] a b
+
+  let iter ?(equal = (=)) ~f a b =
+    fold_left a b
+      ~equal
+      ~f:(fun () x -> f x)
+      ~init:()
+end
diff --git a/clib/diff2.mli b/clib/diff2.mli
new file mode 100644
index 0000000000..a085f4ffe8
--- /dev/null
+++ b/clib/diff2.mli
@@ -0,0 +1,101 @@
+(* copied from https://github.com/leque/ocaml-diff.git and renamed from "diff.mli" *)
+(**
+   An implementation of Eugene Myers' O(ND) Difference Algorithm\[1\].
+   This implementation is a port of util.lcs module of
+   {{:http://practical-scheme.net/gauche} Gauche Scheme interpreter}.
+
+   - \[1\] Eugene Myers, An O(ND) Difference Algorithm and Its Variations, Algorithmica Vol. 1 No. 2, pp. 251-266, 1986.
+ *)
+
+type 'a common = [
+    `Common of int * int * 'a
+  ]
+(** an element of lcs of seq1 and seq2 *)
+
+type 'a edit =
+  [ `Removed of int * 'a
+  | `Added of int * 'a
+  | 'a common
+  ]
+(** an element of diff of seq1 and seq2. *)
+
+module type SeqType = sig
+  type t
+  (** The type of the sequence. *)
+
+  type elem
+  (** The type of the elements of the sequence. *)
+
+  val get : t -> int -> elem
+  (** [get t n] returns [n]-th element of the sequence [t]. *)
+
+  val length : t -> int
+  (** [length t] returns the length of the sequence [t]. *)
+end
+(** Input signature of {!Diff.Make}. *)
+
+module type S = sig
+  type t
+  (** The type of input sequence. *)
+
+  type elem
+  (** The type of the elements of result / input sequence. *)
+
+  val lcs :
+      ?equal:(elem -> elem -> bool) ->
+      t -> t -> elem common list
+  (**
+     [lcs ~equal seq1 seq2] computes the LCS (longest common sequence) of
+     [seq1] and [seq2].
+     Elements of [seq1] and [seq2] are compared with [equal].
+     [equal] defaults to [Pervasives.(=)].
+
+     Elements of lcs are [`Common (pos1, pos2, e)]
+     where [e] is an element, [pos1] is a position in [seq1],
+     and [pos2] is a position in [seq2].
+   *)
+
+  val diff :
+      ?equal:(elem -> elem -> bool) ->
+      t -> t -> elem edit list
+  (**
+     [diff ~equal seq1 seq2] computes the diff of [seq1] and [seq2].
+     Elements of [seq1] and [seq2] are compared with [equal].
+
+     Elements only in [seq1] are represented as [`Removed (pos, e)]
+     where [e] is an element, and [pos] is a position in [seq1];
+     those only in [seq2] are represented as [`Added (pos, e)]
+     where [e] is an element, and [pos] is a position in [seq2];
+     those common in [seq1] and [seq2] are represented as
+     [`Common (pos1, pos2, e)]
+     where [e] is an element, [pos1] is a position in [seq1],
+     and [pos2] is a position in [seq2].
+   *)
+
+  val fold_left :
+      ?equal:(elem -> elem -> bool) ->
+      f:('a -> elem edit -> 'a) ->
+      init:'a ->
+      t -> t -> 'a
+  (**
+     [fold_left ~equal ~f ~init seq1 seq2] is same as
+     [diff ~equal seq1 seq2 |> ListLabels.fold_left ~f ~init],
+     but does not create an intermediate list.
+   *)
+
+  val iter :
+      ?equal:(elem -> elem -> bool) ->
+      f:(elem edit -> unit) ->
+      t -> t -> unit
+  (**
+     [iter ~equal ~f seq1 seq2] is same as
+     [diff ~equal seq1 seq2 |> ListLabels.iter ~f],
+     but does not create an intermediate list.
+   *)
+end
+(** Output signature of {!Diff.Make}. *)
+
+module Make :
+  functor (M : SeqType) -> (S with type t = M.t and type elem = M.elem)
+(** Functor building an implementation of the diff structure
+    given a sequence type.  *)
diff --git a/clib/terminal.ml b/clib/terminal.ml
index 1d9468137b..d243d6599e 100644
--- a/clib/terminal.ml
+++ b/clib/terminal.ml
@@ -59,6 +59,19 @@ let default = {
   suffix = None;
 }
 
+let reset = "\027[0m"
+
+let reset_style = {
+  fg_color = Some `DEFAULT;
+  bg_color = Some `DEFAULT;
+  bold = Some false;
+  italic = Some false;
+  underline = Some false;
+  negative = Some false;
+  prefix = None;
+  suffix = None;
+}
+
 let make ?fg_color ?bg_color ?bold ?italic ?underline ?negative ?style ?prefix ?suffix () =
   let st = match style with
   | None -> default
@@ -87,6 +100,25 @@ let merge s1 s2 =
     suffix = set s1.suffix s2.suffix;
   }
 
+let diff s1 s2 =
+  let diff_op o1 o2 reset_val = match o1 with
+  | None -> o2
+  | Some _ ->
+    match o2 with
+    | None -> reset_val
+    | Some _ -> if o1 = o2 then None else o2 in
+
+  {
+    fg_color = diff_op s1.fg_color s2.fg_color reset_style.fg_color;
+    bg_color = diff_op s1.bg_color s2.bg_color reset_style.bg_color;
+    bold = diff_op s1.bold s2.bold reset_style.bold;
+    italic = diff_op s1.italic s2.italic reset_style.italic;
+    underline = diff_op s1.underline s2.underline reset_style.underline;
+    negative = diff_op s1.negative s2.negative reset_style.negative;
+    prefix = diff_op s1.prefix s2.prefix reset_style.prefix;
+    suffix = diff_op s1.suffix s2.suffix reset_style.suffix;
+  }
+
 let base_color = function
 | `DEFAULT -> 9
 | `BLACK -> 0
@@ -167,20 +199,8 @@ let repr st =
 let eval st =
   let tags = repr st in
   let tags = List.map string_of_int tags in
-  Printf.sprintf "\027[%sm" (String.concat ";" tags)
-
-let reset = "\027[0m"
-
-let reset_style = {
-  fg_color = Some `DEFAULT;
-  bg_color = Some `DEFAULT;
-  bold = Some false;
-  italic = Some false;
-  underline = Some false;
-  negative = Some false;
-  prefix = None;
-  suffix = None;
-}
+  if List.length tags = 0 then "" else
+    Printf.sprintf "\027[%sm" (String.concat ";" tags)
 
 let has_style t =
   Unix.isatty t && Sys.os_type = "Unix"
diff --git a/clib/terminal.mli b/clib/terminal.mli
index dbf8d4640c..bc30b0016f 100644
--- a/clib/terminal.mli
+++ b/clib/terminal.mli
@@ -51,6 +51,9 @@ val make : ?fg_color:color -> ?bg_color:color ->
 val merge : style -> style -> style
 (** [merge s1 s2] returns [s1] with all defined values of [s2] overwritten. *)
 
+val diff : style -> style -> style
+(** [diff s1 s2] returns the differences between [s1] and [s2]. *)
+
 val repr : style -> int list
 (** Generate the ANSI code representing the given style. *)
 
@@ -60,6 +63,9 @@ val eval : style -> string
 val reset : string
 (** This escape sequence resets all attributes. *)
 
+val reset_style : style
+(** The default style *)
+
 val has_style : Unix.file_descr -> bool
 (** Whether an output file descriptor handles styles. Very heuristic, only
     checks it is a terminal. *)