Merge pull request #840 from ejgallego/codeAction

Code Actions

CHANGES.md

@@ -36,6 +36,8 @@
    see some motivation for that (@ejgallego, #841)
  - [lsp] [diagnostics] (! breaking change) change type of diagnostics
    extra data from list to named record (@ejgallego, #843)
+ - [lsp] Implement support for `textDocument/codeAction`. For now, we
+   support Coq's 8.21 `quickFix` data (@ejgallego, #840, #843, #845)
 
 # coq-lsp 0.2.0: From Green to Blue
 -----------------------------------

controller/lsp_core.ml

@@ -416,6 +416,20 @@ let do_document = do_document_request_maybe ~handler:Rq_document.request
 let do_save_vo = do_document_request_maybe ~handler:Rq_save.request
 let do_lens = do_document_request_maybe ~handler:Rq_lens.request
 
+(* could be smarter *)
+let do_action ~params =
+  let range = field "range" params in
+  match Lsp.JLang.Diagnostic.Range.of_yojson range with
+  | Ok range ->
+    let range = Lsp.JLang.Diagnostic.Range.vnoc range in
+    do_immediate ~params ~handler:(Rq_action.request ~range)
+  | Error err ->
+    (* XXX: We really need to fix the parsing error handling in lsp_core, we got
+       it right in petanque haha *)
+    (* JSON-RPC Parse error (EJGA: is this the right code) *)
+    let code = -32700 in
+    Rq.Action.error (code, err)
+
 let do_cancel ~ofn_rq ~params =
   let id = int_field "id" params in
   let code = -32800 in
@@ -584,6 +598,7 @@ let dispatch_request ~token ~method_ ~params : Rq.Action.t =
   | "textDocument/hover" -> do_hover ~params
   | "textDocument/codeLens" -> do_lens ~params
   | "textDocument/selectionRange" -> do_selectionRange ~params
+  | "textDocument/codeAction" -> do_action ~params
   (* Proof-specific stuff *)
   | "proof/goals" -> do_goals ~params
   (* Proof-specific stuff *)

controller/rq_action.ml

@@ -0,0 +1,65 @@
+let point_lt { Lang.Point.line = l1; Lang.Point.character = c1; offset = _ }
+    { Lang.Point.line = l2; Lang.Point.character = c2; offset = _ } =
+  l1 < l2 || (l1 = l2 && c1 < c2)
+
+let point_gt { Lang.Point.line = l1; Lang.Point.character = c1; offset = _ }
+    { Lang.Point.line = l2; Lang.Point.character = c2; offset = _ } =
+  l1 > l2 || (l1 = l2 && c1 > c2)
+
+(* To move to doc.ml *)
+let filter_map_range ~range ~nodes ~f =
+  let rec aux (nodes : Fleche.Doc.Node.t list) acc =
+    match nodes with
+    | [] -> List.rev acc
+    | node :: nodes -> (
+      let open Lang.Range in
+      let nrange = node.range in
+      if point_lt nrange.end_ range.start then aux nodes acc
+      else if point_gt nrange.start range.end_ then List.rev acc
+      else
+        (* Node in scope *)
+        match f node with
+        | Some res -> aux nodes (res :: acc)
+        | None -> aux nodes acc)
+  in
+  aux nodes []
+
+(* util *)
+let filter_map_cut f l =
+  match List.filter_map f l with
+  | [] -> None
+  | res -> Some res
+
+(* Return list of pairs of diags, qf *)
+let get_qf (d : Lang.Diagnostic.t) : _ option =
+  Option.bind d.data (function
+    | { Lang.Diagnostic.Data.quickFix = Some qf; _ } -> Some (d, qf)
+    | _ -> None)
+
+let get_qfs ~range (doc : Fleche.Doc.t) =
+  let f { Fleche.Doc.Node.diags; _ } = filter_map_cut get_qf diags in
+  filter_map_range ~range ~nodes:doc.nodes ~f |> List.concat
+
+let request ~range ~token:_ ~(doc : Fleche.Doc.t) =
+  let kind = Some "quickfix" in
+  let isPreferred = Some true in
+  let qf = get_qfs ~range doc in
+  let bf (d, qf) =
+    List.map
+      (fun { Lang.Qf.range; newText } ->
+        let oldText =
+          Fleche.Contents.extract_raw ~contents:doc.contents ~range
+        in
+        let title = Format.asprintf "Replace `%s` by `%s`" oldText newText in
+        let diagnostics = [ d ] in
+        let qf = [ Lsp.Workspace.TextEdit.{ range; newText } ] in
+        let changes = [ (doc.uri, qf) ] in
+        let edit = Some Lsp.Workspace.WorkspaceEdit.{ changes } in
+        Lsp.Core.CodeAction.{ title; kind; diagnostics; isPreferred; edit })
+      qf
+  in
+  List.concat_map bf qf
+
+let request ~range ~token ~(doc : Fleche.Doc.t) =
+  let res = request ~range ~token ~doc in
+  Ok (`List (List.map Lsp.Core.CodeAction.to_yojson res))

controller/rq_action.mli

@@ -0,0 +1 @@
+val request : range:Lang.Range.t -> Request.document

controller/rq_goals.ml

@@ -6,7 +6,7 @@
 (************************************************************************)
 
 (* Replace by ppx when we can print goals properly in the client *)
-let mk_message (level, { Coq.Message.Payload.range; msg }) =
+let mk_message (level, { Coq.Message.Payload.range; msg; quickFix = _ }) =
   Lsp.JFleche.Message.{ range; level; text = msg }
 
 let mk_messages node =

controller/rq_init.ml

@@ -117,7 +117,7 @@ let do_initialize ~io ~params =
     [ ("textDocumentSync", `Int 1)
     ; ("documentSymbolProvider", `Bool true)
     ; ("hoverProvider", `Bool true)
-    ; ("codeActionProvider", `Bool false)
+    ; ("codeActionProvider", `Bool true)
     ; ( "completionProvider"
       , `Assoc
           [ ("triggerCharacters", `List [ `String "\\" ])

coq/init.ml

@@ -36,14 +36,20 @@ let coq_lvl_to_severity (lvl : Feedback.level) =
   | Feedback.Warning -> warning
   | Feedback.Error -> error
 
-let add_message lvl range msg q =
+let qf_of_coq qf =
+  let range = Quickfix.loc qf in
+  let newText = Quickfix.pp qf |> Pp.string_of_ppcmds in
+  { Lang.Qf.range; newText }
+
+let add_message lvl range qf msg q =
   let lvl = coq_lvl_to_severity lvl in
-  let payload = Message.Payload.make ?range msg in
+  let quickFix = if qf = [] then None else Some (List.map qf_of_coq qf) in
+  let payload = Message.Payload.make ?range ?quickFix msg in
   q := (lvl, payload) :: !q
 
 let mk_fb_handler q Feedback.{ contents; _ } =
   match contents with
-  | Message (lvl, loc, _, msg) -> add_message lvl loc msg q
+  | Message (lvl, loc, qf, msg) -> add_message lvl loc qf msg q
   | _ -> ()
 
 let coq_init opts =

coq/message.ml

@@ -2,11 +2,15 @@
 module Payload = struct
   type 'l t =
     { range : 'l option
+    ; quickFix : 'l Lang.Qf.t list option
     ; msg : Pp.t
     }
 
-  let make ?range msg = { range; msg }
-  let map ~f { range; msg } = { range = Option.map f range; msg }
+  let make ?range ?quickFix msg = { range; quickFix; msg }
+
+  let map ~f { range; quickFix; msg } =
+    let quickFix = Option.map (List.map (Lang.Qf.map ~f)) quickFix in
+    { range = Option.map f range; quickFix; msg }
 end
 
 type 'l t = Lang.Diagnostic.Severity.t * 'l Payload.t

coq/message.mli

@@ -10,10 +10,11 @@
 module Payload : sig
   type 'l t =
     { range : 'l option
+    ; quickFix : 'l Lang.Qf.t list option
     ; msg : Pp.t
     }
 
-  val make : ?range:'l -> Pp.t -> 'l t
+  val make : ?range:'l -> ?quickFix:'l Lang.Qf.t list -> Pp.t -> 'l t
   val map : f:('l -> 'm) -> 'l t -> 'm t
 end
 

coq/protect.ml

@@ -27,11 +27,24 @@ module R = struct
     | Completed (Ok r) -> Completed (Ok r)
     | Interrupted -> Interrupted
 
+  (* Similar to Message.map, but missing the priority field, this is due to Coq
+     having to sources of feedback, an async one, and the exn sync one.
+     Ultimately both carry the same [payload].
+
+     See coq/coq#5479 for some information about this, among some other relevant
+     issues. AFAICT, the STM tried to use a full async error reporting however
+     due to problems the more "legacy" exn is the actuall error mechanism in
+     use *)
   let map_loc ~f =
     let f = Message.Payload.map ~f in
     map_error ~f
 end
 
+let qf_of_coq qf =
+  let range = Quickfix.loc qf in
+  let newText = Quickfix.pp qf |> Pp.string_of_ppcmds in
+  { Lang.Qf.range; newText }
+
 (* Eval and reify exceptions *)
 let eval_exn ~token ~f x =
   match Limits.limit ~token ~f x with
@@ -43,7 +56,12 @@ let eval_exn ~token ~f x =
     let e, info = Exninfo.capture exn in
     let range = Loc.(get_loc info) in
     let msg = CErrors.iprint (e, info) in
-    let payload = Message.Payload.make ?range msg in
+    let quickFix =
+      match Quickfix.from_exception exn with
+      | Ok [] | Error _ -> None
+      | Ok qf -> Some (List.map qf_of_coq qf)
+    in
+    let payload = Message.Payload.make ?range ?quickFix msg in
     Vernacstate.Interp.invalidate_cache ();
     if CErrors.is_anomaly e then R.Completed (Error (Anomaly payload))
     else R.Completed (Error (User payload))

coq/protect.mli

@@ -28,7 +28,7 @@ module R : sig
 end
 
 module E : sig
-  type ('a, 'l) t =
+  type ('a, 'l) t = private
     { r : ('a, 'l) R.t
     ; feedback : 'l Message.t list
     }

examples/Pff.v

@@ -14,7 +14,7 @@ Require Import Psatz.
 Set Warnings "-deprecated".
 
 (* Compatibility workaround, remove once requiring Coq >= 8.16 *)
-Module Import Compat.
+Module Import Compat816.
 
 Lemma Even_0 : Nat.Even 0.
 Proof. exists 0; reflexivity. Qed.
@@ -67,7 +67,21 @@ Proof proj1 (proj1 (Even_Odd_double n)).
 Definition Odd_double n : Nat.Odd n -> n = S (Nat.double (Nat.div2 n)).
 Proof proj1 (proj2 (Even_Odd_double n)).
 
-End Compat.
+Definition Rinv_mult_distr := Rinv_mult_distr.
+Definition Rabs_Rinv := Rabs_Rinv.
+Definition Rinv_pow := Rinv_pow.
+Definition Rinv_involutive := Rinv_involutive.
+Definition Rlt_Rminus := Rlt_Rminus.
+Definition powerRZ_inv := powerRZ_inv.
+Definition powerRZ_neg := powerRZ_neg.
+
+End Compat816.
+
+Module Import Compat819.
+
+Definition IZR_neq := IZR_neq.
+
+End Compat819.
 
 (*** was file sTactic.v  ***)
 
@@ -17553,7 +17567,7 @@ apply Z.le_trans with  (Nat.double (Nat.div2 t)).
 unfold Nat.double; rewrite inj_plus; auto with zarith.
 rewrite <- Even_double; auto with zarith.
 apply Z.le_trans with (-1+(S ( Nat.double (Nat.div2 t))))%Z.
-rewrite inj_S; unfold Z.succ; auto with zarith.
+rewrite inj_S; unfold Z.succ; auto with zarith;
 unfold Nat.double; rewrite inj_plus; auto with zarith.
 rewrite <- Odd_double by easy. lia.
 Qed.
@@ -17568,9 +17582,9 @@ case (Nat.Even_or_Odd t); intros I.
 apply Z.le_trans with  ((Nat.double (Nat.div2 t)+1))%Z.
 2:unfold Nat.double; rewrite inj_plus; auto with zarith.
 rewrite <- Even_double; auto with zarith.
-apply Z.le_trans with ((S ( Nat.double (Nat.div2 t))))%Z; auto with zarith.
-2: rewrite inj_S; unfold Z.succ; auto with zarith.
-2: unfold Nat.double; rewrite inj_plus; auto with zarith.
+apply Z.le_trans with ((S ( Nat.double (Nat.div2 t))))%Z; auto with zarith;
+try solve [rewrite inj_S; unfold Z.succ; auto with zarith;
+  unfold Nat.double; rewrite inj_plus; auto with zarith].
 rewrite <- Odd_double; auto with zarith.
 Qed.
 

examples/codeAction.v

@@ -0,0 +1,54 @@
+(* Test for Coq's QF for Coq to Stdlib PRs *)
+
+Require Import Coq.ssr.ssrbool.
+From Coq Require Import ssreflect ssrbool.
+
+(* Note: this tests the two different lookup modes *)
+About Coq.Init.Nat.add.
+Check Coq.Init.Nat.add.
+
+(* Example codeAction, from Coq's test suite *)
+
+Module M. Definition y := 4. End M.
+Import M.
+
+#[deprecated(use=y)]
+Definition x := 3.
+
+Module N. Definition y := 5. End N.
+Import N.
+
+Definition d1 := x = 3.
+
+Module M1.
+Notation w := x.
+End M1.
+Import M1.
+
+#[deprecated(use=w)]
+Notation v := 3.
+
+Module M2.
+Notation w := 5.
+End M2.
+Import M2.
+
+Definition d2 := v = 3.
+
+Fail #[deprecated(use=w)]
+Notation "a +++ b" := (a + b) (at level 2).
+
+Fail #[deprecated(use=nonexisting)]
+Definition y := 2.
+
+(***********************************************)
+Module A.
+End B.
+
+(***********************************************)
+Require Import Extraction.
+
+Module nat. End nat.
+
+Extraction nat.
+