From ee95987944bf40f2de6e33260c933d50b8c0e105 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Thu, 3 Oct 2024 17:24:54 +0200
Subject: [PATCH] [coq] Abstract the feedback / error payloads better.

This is in preparation for cleaner code in #840
---
 controller/request.ml          |  2 +-
 controller/rq_goals.ml         |  3 ++-
 coq/init.ml                    |  5 +++--
 coq/message.ml                 | 14 ++++++++++++-
 coq/message.mli                | 22 +++++++++++++++++++-
 coq/protect.ml                 | 22 ++++++++++----------
 coq/protect.mli                |  8 +++----
 coq/workspace.ml               |  4 ++--
 fleche/doc.ml                  | 38 +++++++++++++++++++---------------
 fleche/doc.mli                 |  2 +-
 petanque/agent.ml              |  4 ++--
 plugins/explain_errors/main.ml |  6 ++++--
 plugins/goaldump/main.ml       |  7 +++----
 13 files changed, 87 insertions(+), 50 deletions(-)

diff --git a/controller/request.ml b/controller/request.ml
index 3ea2fac4..27abf50e 100644
--- a/controller/request.ml
+++ b/controller/request.ml
@@ -26,7 +26,7 @@ module R = struct
 
   let print_err ~name e =
     match e with
-    | Coq.Protect.Error.Anomaly (_loc, msg) | User (_loc, msg) ->
+    | Coq.Protect.Error.Anomaly { msg; _ } | User { msg; _ } ->
       Format.asprintf "Error in %s request: %a" name Pp.pp_with msg
 
   let of_execution ~name ~f x : t =
diff --git a/controller/rq_goals.ml b/controller/rq_goals.ml
index e420b884..47d672db 100644
--- a/controller/rq_goals.ml
+++ b/controller/rq_goals.ml
@@ -6,7 +6,8 @@
 (************************************************************************)
 
 (* Replace by ppx when we can print goals properly in the client *)
-let mk_message (range, level, text) = Lsp.JFleche.Message.{ range; level; text }
+let mk_message (level, { Coq.Message.Payload.range; msg }) =
+  Lsp.JFleche.Message.{ range; level; text = msg }
 
 let mk_messages node =
   Option.map Fleche.Doc.Node.messages node
diff --git a/coq/init.ml b/coq/init.ml
index 3eaeaf4f..eaabe9ed 100644
--- a/coq/init.ml
+++ b/coq/init.ml
@@ -36,9 +36,10 @@ let coq_lvl_to_severity (lvl : Feedback.level) =
   | Feedback.Warning -> warning
   | Feedback.Error -> error
 
-let add_message lvl loc msg q =
+let add_message lvl range msg q =
   let lvl = coq_lvl_to_severity lvl in
-  q := (loc, lvl, msg) :: !q
+  let payload = Message.Payload.make ?range msg in
+  q := (lvl, payload) :: !q
 
 let mk_fb_handler q Feedback.{ contents; _ } =
   match contents with
diff --git a/coq/message.ml b/coq/message.ml
index dfba4ccd..f48644d2 100644
--- a/coq/message.ml
+++ b/coq/message.ml
@@ -1,2 +1,14 @@
 (** Messages from Coq *)
-type 'l t = 'l option * Lang.Diagnostic.Severity.t * Pp.t
+module Payload = struct
+  type 'l t =
+    { range : 'l option
+    ; msg : Pp.t
+    }
+
+  let make ?range msg = { range; msg }
+  let map ~f { range; msg } = { range = Option.map f range; msg }
+end
+
+type 'l t = Lang.Diagnostic.Severity.t * 'l Payload.t
+
+let map ~f (lvl, pl) = (lvl, Payload.map ~f pl)
diff --git a/coq/message.mli b/coq/message.mli
index dfba4ccd..2935dd5b 100644
--- a/coq/message.mli
+++ b/coq/message.mli
@@ -1,2 +1,22 @@
 (** Messages from Coq *)
-type 'l t = 'l option * Lang.Diagnostic.Severity.t * Pp.t
+
+(** Coq provides payload to our layer via two different mechanisms:
+    - feedback messages
+    - error exceptions
+
+    In both cases, the payload is the same, and it comes via different ways due
+    to historical reasons. We abstract the payload as to better handle the
+    common paths. *)
+module Payload : sig
+  type 'l t =
+    { range : 'l option
+    ; msg : Pp.t
+    }
+
+  val make : ?range:'l -> Pp.t -> 'l t
+  val map : f:('l -> 'm) -> 'l t -> 'm t
+end
+
+type 'l t = Lang.Diagnostic.Severity.t * 'l Payload.t
+
+val map : f:('l -> 'm) -> 'l t -> 'm t
diff --git a/coq/protect.ml b/coq/protect.ml
index c768e1e9..f9560312 100644
--- a/coq/protect.ml
+++ b/coq/protect.ml
@@ -1,9 +1,7 @@
 module Error = struct
-  type 'l payload = 'l option * Pp.t
-
   type 'l t =
-    | User of 'l payload
-    | Anomaly of 'l payload
+    | User of 'l Message.Payload.t
+    | Anomaly of 'l Message.Payload.t
 
   let map ~f = function
     | User e -> User (f e)
@@ -15,7 +13,9 @@ module R = struct
     | Completed of ('a, 'l Error.t) result
     | Interrupted (* signal sent, eval didn't complete *)
 
-  let error e = Completed (Error (Error.User (None, e)))
+  let error msg =
+    let payload = Message.Payload.make msg in
+    Completed (Error (Error.User payload))
 
   let map ~f = function
     | Completed (Result.Ok r) -> Completed (Result.Ok (f r))
@@ -28,7 +28,7 @@ module R = struct
     | Interrupted -> Interrupted
 
   let map_loc ~f =
-    let f (loc, msg) = (Option.map f loc, msg) in
+    let f = Message.Payload.map ~f in
     map_error ~f
 end
 
@@ -41,11 +41,12 @@ let eval_exn ~token ~f x =
     R.Interrupted
   | exception exn ->
     let e, info = Exninfo.capture exn in
-    let loc = Loc.(get_loc info) in
+    let range = Loc.(get_loc info) in
     let msg = CErrors.iprint (e, info) in
+    let payload = Message.Payload.make ?range msg in
     Vernacstate.Interp.invalidate_cache ();
-    if CErrors.is_anomaly e then R.Completed (Error (Anomaly (loc, msg)))
-    else R.Completed (Error (User (loc, msg)))
+    if CErrors.is_anomaly e then R.Completed (Error (Anomaly payload))
+    else R.Completed (Error (User payload))
 
 let _bind_exn ~f x =
   match x with
@@ -68,10 +69,9 @@ module E = struct
     { r; feedback }
 
   let map ~f { r; feedback } = { r = R.map ~f r; feedback }
-  let map_message ~f (loc, lvl, msg) = (Option.map f loc, lvl, msg)
 
   let map_loc ~f { r; feedback } =
-    { r = R.map_loc ~f r; feedback = List.map (map_message ~f) feedback }
+    { r = R.map_loc ~f r; feedback = List.map (Message.map ~f) feedback }
 
   let bind ~f { r; feedback } =
     match r with
diff --git a/coq/protect.mli b/coq/protect.mli
index c0c2fe73..cfbd6595 100644
--- a/coq/protect.mli
+++ b/coq/protect.mli
@@ -4,11 +4,9 @@
 
     As of today this includes feedback and exceptions. *)
 module Error : sig
-  type 'l payload = 'l option * Pp.t
-
   type 'l t = private
-    | User of 'l payload
-    | Anomaly of 'l payload
+    | User of 'l Message.Payload.t
+    | Anomaly of 'l Message.Payload.t
 end
 
 (** This "monad" could be related to "Runners in action" (Ahman, Bauer), thanks
@@ -22,7 +20,7 @@ module R : sig
   val map : f:('a -> 'b) -> ('a, 'l) t -> ('b, 'l) t
 
   val map_error :
-    f:('l Error.payload -> 'm Error.payload) -> ('a, 'l) t -> ('a, 'm) t
+    f:('l Message.Payload.t -> 'm Message.Payload.t) -> ('a, 'l) t -> ('a, 'm) t
 
   (** Update the loc stored in the result, this is used by our cache-aware
       location *)
diff --git a/coq/workspace.ml b/coq/workspace.ml
index 365e29d7..56a6ccbc 100644
--- a/coq/workspace.ml
+++ b/coq/workspace.ml
@@ -387,8 +387,8 @@ let guess ~token ~debug ~cmdline ~dir =
   ignore feedback;
   match r with
   | Protect.R.Interrupted -> Error "Workspace Scanning Interrupted"
-  | Protect.R.Completed (Error (User (_, msg)))
-  | Protect.R.Completed (Error (Anomaly (_, msg))) ->
+  | Protect.R.Completed (Error (User { msg; _ }))
+  | Protect.R.Completed (Error (Anomaly { msg; _ })) ->
     Error (Format.asprintf "Workspace Scanning Errored: %a" Pp.pp_with msg)
   | Protect.R.Completed (Ok workspace) -> Ok workspace
 
diff --git a/fleche/doc.ml b/fleche/doc.ml
index 282afecc..cd73263e 100644
--- a/fleche/doc.ml
+++ b/fleche/doc.ml
@@ -116,8 +116,9 @@ module Node = struct
   module Message = struct
     type t = Lang.Range.t Coq.Message.t
 
-    let feedback_to_message ~lines (loc, lvl, msg) =
-      (Coq.Utils.to_orange ~lines loc, lvl, msg)
+    let feedback_to_message ~lines message =
+      let f = Coq.Utils.to_range ~lines in
+      Coq.Message.map ~f message
   end
 
   type t =
@@ -197,9 +198,10 @@ end = struct
     let data = extra_diagnostics_of_ast stm_range ast in
     make ?data err_range Lang.Diagnostic.Severity.error msg
 
-  let of_feed ~drange (range, severity, message) =
+  let of_feed ~drange (severity, payload) =
+    let { Coq.Message.Payload.range; msg } = payload in
     let range = Option.default drange range in
-    make range severity message
+    make range severity msg
 
   type partition_kind =
     | Left
@@ -224,7 +226,7 @@ end = struct
       else if !Config.v.show_notices_as_diagnostics then 4
       else 3
     in
-    let f (_, lvl, _) =
+    let f (lvl, _) =
       (* warning = 2 *)
       if lvl = Lang.Diagnostic.Severity.warning then Both
       else if lvl < cutoff then Left
@@ -354,8 +356,9 @@ let empty_doc ~uri ~contents ~version ~env ~root ~nodes ~completed =
   let completed = completed init_range in
   { uri; contents; toc; version; env; root; nodes; diags_dirty; completed }
 
-let error_doc ~loc ~message ~uri ~contents ~version ~env =
-  let feedback = [ (loc, Diags.err, Pp.str message) ] in
+let error_doc ~range ~message ~uri ~contents ~version ~env =
+  let payload = Coq.Message.Payload.make ?range (Pp.str message) in
+  let feedback = [ (Diags.err, payload) ] in
   let root = env.Env.init in
   let nodes = [] in
   let completed range = Completion.Failed range in
@@ -365,7 +368,8 @@ let conv_error_doc ~raw ~uri ~version ~env ~root err =
   let contents = Contents.make_raw ~raw in
   let lines = contents.lines in
   let err =
-    (None, Diags.err, Pp.(str "Error in document conversion: " ++ str err))
+    let msg = Pp.(str "Error in document conversion: " ++ str err) in
+    (Diags.err, Coq.Message.Payload.make msg)
   in
   (* No execution to add *)
   let stats = None in
@@ -394,14 +398,14 @@ let handle_doc_creation_exec ~token ~env ~uri ~version ~contents =
     match r with
     | Interrupted ->
       let message = "Document Creation Interrupted!" in
-      let loc = None in
-      error_doc ~loc ~message ~uri ~version ~contents ~env
-    | Completed (Error (User (loc, err_msg)))
-    | Completed (Error (Anomaly (loc, err_msg))) ->
+      let range = None in
+      error_doc ~range ~message ~uri ~version ~contents ~env
+    | Completed (Error (User { range; msg = err_msg }))
+    | Completed (Error (Anomaly { range; msg = err_msg })) ->
       let message =
         Format.asprintf "Doc.create, internal error: @[%a@]" Pp.pp_with err_msg
       in
-      error_doc ~loc ~message ~uri ~version ~contents ~env
+      error_doc ~range ~message ~uri ~version ~contents ~env
     | Completed (Ok doc) -> (doc, [])
   in
   let state = doc.root in
@@ -749,7 +753,7 @@ let parse_action ~token ~lines ~st last_tok doc_handle =
     | Ok (Some ast) ->
       let () = if Debug.parsing then DDebug.parsed_sentence ~ast in
       (Process ast, [], feedback, time)
-    | Error (Anomaly (_, msg)) | Error (User (None, msg)) ->
+    | Error (Anomaly { msg; _ }) | Error (User { range = None; msg }) ->
       (* We don't have a better alternative :(, usually missing error loc here
          means an anomaly, so we stop *)
       let err_range = last_tok in
@@ -757,7 +761,7 @@ let parse_action ~token ~lines ~st last_tok doc_handle =
         [ Diags.error ~err_range ~msg ~stm_range:err_range () ]
       in
       (EOF (Failed last_tok), parse_diags, feedback, time)
-    | Error (User (Some err_range, msg)) ->
+    | Error (User { range = Some err_range; msg }) ->
       Coq.Parsing.discard_to_dot doc_handle;
       let last_tok = Coq.Parsing.Parsable.loc doc_handle in
       let last_tok_range = Coq.Utils.to_range ~lines last_tok in
@@ -816,8 +820,8 @@ let node_of_coq_result ~token ~doc ~range ~prev ~ast ~st ~parsing_diags
         ~diags:[] ~feedback ~info
     in
     Continue { state; last_tok; node }
-  | Error (Coq.Protect.Error.Anomaly (err_range, msg) as coq_err)
-  | Error (User (err_range, msg) as coq_err) ->
+  | Error (Coq.Protect.Error.Anomaly { range = err_range; msg } as coq_err)
+  | Error (User { range = err_range; msg } as coq_err) ->
     let err_range = Option.default range err_range in
     let err_diags = [ Diags.error ~err_range ~msg ~stm_range:range ~ast () ] in
     let contents, nodes = (doc.contents, doc.nodes) in
diff --git a/fleche/doc.mli b/fleche/doc.mli
index f309d9bc..ff2a0c24 100644
--- a/fleche/doc.mli
+++ b/fleche/doc.mli
@@ -24,7 +24,7 @@ module Node : sig
   end
 
   module Message : sig
-    type t = Lang.Range.t option * Lang.Diagnostic.Severity.t * Pp.t
+    type t = Lang.Range.t Coq.Message.t
   end
 
   type t = private
diff --git a/petanque/agent.ml b/petanque/agent.ml
index 7a74b241..320b890d 100644
--- a/petanque/agent.ml
+++ b/petanque/agent.ml
@@ -137,9 +137,9 @@ let execute_precommands ~token ~memo ~pre_commands ~(node : Fleche.Doc.Node.t) =
 let protect_to_result (r : _ Coq.Protect.E.t) : (_, _) Result.t =
   match r with
   | { r = Interrupted; feedback = _ } -> Error Error.Interrupted
-  | { r = Completed (Error (User (_loc, msg))); feedback = _ } ->
+  | { r = Completed (Error (User { msg; _ })); feedback = _ } ->
     Error (Error.Coq (Pp.string_of_ppcmds msg))
-  | { r = Completed (Error (Anomaly (_loc, msg))); feedback = _ } ->
+  | { r = Completed (Error (Anomaly { msg; _ })); feedback = _ } ->
     Error (Error.Anomaly (Pp.string_of_ppcmds msg))
   | { r = Completed (Ok r); feedback = _ } -> Ok r
 
diff --git a/plugins/explain_errors/main.ml b/plugins/explain_errors/main.ml
index 599a856e..fb72c4ba 100644
--- a/plugins/explain_errors/main.ml
+++ b/plugins/explain_errors/main.ml
@@ -10,8 +10,10 @@ let pp_goals ~token ~st =
   | Some proof -> (
     match Coq.Print.pr_goals ~token ~proof with
     | { Coq.Protect.E.r = Completed (Ok goals); _ } -> goals
-    | { Coq.Protect.E.r = Completed (Error (User msg | Anomaly msg)); _ } ->
-      Pp.(str "error when printing goals: " ++ snd msg)
+    | { Coq.Protect.E.r =
+          Completed (Error (User { msg; _ } | Anomaly { msg; _ }))
+      ; _
+      } -> Pp.(str "error when printing goals: " ++ msg)
     | { Coq.Protect.E.r = Interrupted; _ } ->
       Pp.str "goal printing was interrupted")
 
diff --git a/plugins/goaldump/main.ml b/plugins/goaldump/main.ml
index 4f753945..474e1fac 100644
--- a/plugins/goaldump/main.ml
+++ b/plugins/goaldump/main.ml
@@ -6,11 +6,10 @@ let of_execution ~io ~what (v : (_, _) Coq.Protect.E.t) =
   | { r; feedback = _ } -> (
     match r with
     | Coq.Protect.R.Completed (Ok goals) -> goals
-    | Coq.Protect.R.Completed (Error (Anomaly err))
-    | Coq.Protect.R.Completed (Error (User err)) ->
+    | Coq.Protect.R.Completed (Error (Anomaly { msg; _ }))
+    | Coq.Protect.R.Completed (Error (User { msg; _ })) ->
       let lvl = Io.Level.Error in
-      Io.Report.msg ~io ~lvl "error when retrieving %s: %a" what Pp.pp_with
-        (snd err);
+      Io.Report.msg ~io ~lvl "error when retrieving %s: %a" what Pp.pp_with msg;
       None
     | Coq.Protect.R.Interrupted -> None)