Merge PR #12874: Add a "Show Proof Diffs" message to the XML protocol

Reviewed-by: herbelin
Ack-by: gares
Ack-by: ejgallego

1 files changed, 28 insertions, 3 deletions

diff --git a/ide/coqide/protocol/xmlprotocol.ml b/ide/coqide/protocol/xmlprotocol.ml
index 9e861baac6..6a33ff8abc 100644
--- a/ide/coqide/protocol/xmlprotocol.ml
+++ b/ide/coqide/protocol/xmlprotocol.ml
@@ -12,7 +12,7 @@
 
 (** WARNING: TO BE UPDATED WHEN MODIFIED! *)
 
-let protocol_version = "20170413"
+let protocol_version = "20200911"
 
 type msg_format = Richpp of int | Ppcmds
 let msg_format = ref (Richpp 72)
@@ -278,6 +278,7 @@ module ReifType : sig
   val state_id_t     : state_id val_t
   val route_id_t     : route_id val_t
   val search_cst_t   : search_constraint val_t
+  val pp_t           : Pp.t val_t
 
   val of_value_type : 'a val_t -> 'a -> xml
   val to_value_type : 'a val_t -> xml -> 'a
@@ -314,6 +315,7 @@ end = struct
     | State_id : state_id val_t
     | Route_id : route_id val_t
     | Search_cst : search_constraint val_t
+    | Pp : Pp.t val_t
 
   type value_type = Value_type : 'a val_t -> value_type
 
@@ -340,6 +342,7 @@ end = struct
   let state_id_t     = State_id
   let route_id_t     = Route_id
   let search_cst_t   = Search_cst
+  let pp_t           = Pp
 
   let of_value_type (ty : 'a val_t) : 'a -> xml =
     let rec convert : type a. a val_t -> a -> xml = function
@@ -362,6 +365,7 @@ end = struct
       | State_id      -> of_stateid
       | Route_id      -> of_routeid
       | Search_cst    -> of_search_cst
+      | Pp            -> of_pp
     in
       convert ty
 
@@ -386,6 +390,7 @@ end = struct
       | State_id      -> to_stateid
       | Route_id      -> to_routeid
       | Search_cst    -> to_search_cst
+      | Pp            -> to_pp
     in
       convert ty
 
@@ -443,6 +448,8 @@ end = struct
     | In_Module s -> "In_Module " ^ String.concat "." s
     | Include_Blacklist -> "Include_Blacklist"
 
+  let pr_pp = Pp.string_of_ppcmds
+
   let rec print : type a. a val_t -> a -> string = function
   | Unit          -> pr_unit
   | Bool          -> pr_bool
@@ -463,6 +470,7 @@ end = struct
   | Union (t1,t2) -> (pr_union (print t1) (print t2))
   | State_id      -> pr_state_id
   | Route_id      -> pr_int
+  | Pp            -> pr_pp
 
   (* This is to break if a rename/refactoring makes the strings below outdated *)
   type 'a exists = bool
@@ -489,6 +497,7 @@ end = struct
                      Printf.sprintf "((%s, %s) CSig.union)" (print_val_t t1) (print_val_t t2)
   | State_id      -> assert(true : Stateid.t exists); "Stateid.t"
   | Route_id      -> assert(true : route_id exists); "route_id"
+  | Pp            -> assert(true : Pp.t exists); "Pp.t"
 
   let print_type = function Value_type ty -> print_val_t ty
 
@@ -507,6 +516,8 @@ end = struct
       (pr_xml (of_pair of_bool of_int (false,3)));
     Printf.printf "%s:\n\n%s\n\n" (print_val_t (Union (Bool,Int)))
       (pr_xml (of_union of_bool of_int (Inl false)));
+    Printf.printf "%s:\n\n%s\n\n" (print_val_t Pp)
+      (pr_xml (of_pp Pp.(hv 3 (str "foo" ++ spc () ++ str "bar") )));
     print_endline ("All other types are records represented by a node named like the OCaml\n"^
                    "type which contains a flattened n-tuple.  We provide one example.\n");
     Printf.printf "%s:\n\n%s\n\n" (print_val_t Option_state)
@@ -538,6 +549,7 @@ let interp_sty_t : interp_sty val_t = pair_t (pair_t bool_t bool_t) string_t
 let stop_worker_sty_t : stop_worker_sty val_t = string_t
 let print_ast_sty_t : print_ast_sty val_t = state_id_t
 let annotate_sty_t : annotate_sty val_t = string_t
+let proof_diff_sty_t : proof_diff_sty val_t = pair_t string_t state_id_t
 
 let add_rty_t : add_rty val_t =
   pair_t state_id_t (pair_t (union_t unit_t state_id_t) string_t)
@@ -563,6 +575,7 @@ let interp_rty_t : interp_rty val_t = pair_t state_id_t (union_t string_t string
 let stop_worker_rty_t : stop_worker_rty val_t = unit_t
 let print_ast_rty_t : print_ast_rty val_t = xml_t
 let annotate_rty_t : annotate_rty val_t = xml_t
+let proof_diff_rty_t : proof_diff_rty val_t = pp_t
 
 let ($) x = erase x
 let calls = [|
@@ -585,6 +598,7 @@ let calls = [|
   "StopWorker", ($)stop_worker_sty_t, ($)stop_worker_rty_t;
   "PrintAst",   ($)print_ast_sty_t,   ($)print_ast_rty_t;
   "Annotate",   ($)annotate_sty_t,    ($)annotate_rty_t;
+  "PDiff",      ($)proof_diff_sty_t,  ($)proof_diff_rty_t;
 |]
 
 type 'a call =
@@ -609,7 +623,9 @@ type 'a call =
   | Interp     : interp_sty -> interp_rty call
   | PrintAst   : print_ast_sty -> print_ast_rty call
   | Annotate   : annotate_sty -> annotate_rty call
+  | PDiff      : proof_diff_sty -> proof_diff_rty call
 
+(* the order of the entries must match the order in "calls" above *)
 let id_of_call : type a. a call -> int = function
   | Add _        -> 0
   | Edit_at _    -> 1
@@ -630,6 +646,7 @@ let id_of_call : type a. a call -> int = function
   | StopWorker _ -> 16
   | PrintAst _   -> 17
   | Annotate _   -> 18
+  | PDiff _     -> 19
 
 let str_of_call c = pi1 calls.(id_of_call c)
 
@@ -652,8 +669,9 @@ let init x        : init_rty call        = Init x
 let wait x        : wait_rty call        = Wait x
 let interp x      : interp_rty call      = Interp x
 let stop_worker x : stop_worker_rty call = StopWorker x
-let print_ast   x : print_ast_rty call   = PrintAst x
-let annotate   x : annotate_rty call    = Annotate x
+let print_ast x   : print_ast_rty call   = PrintAst x
+let annotate x    : annotate_rty call    = Annotate x
+let proof_diff x  : proof_diff_rty call  = PDiff x
 
 let abstract_eval_call : type a. _ -> a call -> a value = fun handler c ->
   let mkGood : type a. a -> a value = fun x -> Good x in
@@ -678,6 +696,7 @@ let abstract_eval_call : type a. _ -> a call -> a value = fun handler c ->
     | StopWorker x -> mkGood (handler.stop_worker x)
     | PrintAst x   -> mkGood (handler.print_ast x)
     | Annotate x   -> mkGood (handler.annotate x)
+    | PDiff x      -> mkGood (handler.proof_diff x)
   with any ->
     let any = Exninfo.capture any in
     Fail (handler.handle_exn any)
@@ -703,6 +722,7 @@ let of_answer : type a. a call -> a value -> xml = function
   | StopWorker _ -> of_value (of_value_type stop_worker_rty_t)
   | PrintAst _   -> of_value (of_value_type print_ast_rty_t  )
   | Annotate _   -> of_value (of_value_type annotate_rty_t   )
+  | PDiff _      -> of_value (of_value_type proof_diff_rty_t )
 
 let of_answer msg_fmt =
   msg_format := msg_fmt; of_answer
@@ -727,6 +747,7 @@ let to_answer : type a. a call -> xml -> a value = function
   | StopWorker _ -> to_value (to_value_type stop_worker_rty_t)
   | PrintAst _   -> to_value (to_value_type print_ast_rty_t  )
   | Annotate _   -> to_value (to_value_type annotate_rty_t   )
+  | PDiff _      -> to_value (to_value_type proof_diff_rty_t )
 
 let of_call : type a. a call -> xml = fun q ->
   let mkCall x = constructor "call" (str_of_call q) [x] in
@@ -750,6 +771,7 @@ let of_call : type a. a call -> xml = fun q ->
   | StopWorker x -> mkCall (of_value_type stop_worker_sty_t x)
   | PrintAst x   -> mkCall (of_value_type print_ast_sty_t   x)
   | Annotate x   -> mkCall (of_value_type annotate_sty_t    x)
+  | PDiff x      -> mkCall (of_value_type proof_diff_sty_t  x)
 
 let to_call : xml -> unknown_call =
   do_match "call" (fun s a ->
@@ -774,6 +796,7 @@ let to_call : xml -> unknown_call =
     | "StopWorker" -> Unknown (StopWorker (mkCallArg stop_worker_sty_t a))
     | "PrintAst"   -> Unknown (PrintAst   (mkCallArg print_ast_sty_t   a))
     | "Annotate"   -> Unknown (Annotate   (mkCallArg annotate_sty_t    a))
+    | "PDiff"      -> Unknown (PDiff      (mkCallArg proof_diff_sty_t  a))
     | x -> raise (Marshal_error("call",PCData x)))
 
 (** Debug printing *)
@@ -805,6 +828,7 @@ let pr_full_value : type a. a call -> a value -> string = fun call value -> matc
   | StopWorker _ -> pr_value_gen (print stop_worker_rty_t) value
   | PrintAst _   -> pr_value_gen (print print_ast_rty_t  ) value
   | Annotate _   -> pr_value_gen (print annotate_rty_t   ) value
+  | PDiff _      -> pr_value_gen (print proof_diff_rty_t ) value
 let pr_call : type a. a call -> string = fun call ->
   let return what x = str_of_call call ^ " " ^ print what x in
   match call with
@@ -827,6 +851,7 @@ let pr_call : type a. a call -> string = fun call ->
     | StopWorker x -> return stop_worker_sty_t x
     | PrintAst x   -> return print_ast_sty_t x
     | Annotate x   -> return annotate_sty_t x
+    | PDiff x      -> return proof_diff_sty_t x
 
 let document to_string_fmt =
   Printf.printf "=== Available calls ===\n\n";