From 9d130c96df2c9e585bf8db37dd46d6731f690910 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 1 Oct 2022 16:02:45 +0200 Subject: [PATCH] [info] Hook completion call, fix still some issues with range. --- CHANGES.md | 1 + controller/rq_completion.ml | 40 ++++++++++++++++----- etc/todo.org | 7 ++-- fleche/debug.ml | 5 ++- fleche/info.ml | 71 +++++++++++++++++++++++++++++++++---- fleche/span.ml | 50 ++++++++++++++++++++++++++ fleche/span.mli | 34 ++++++++++++++++++ 7 files changed, 190 insertions(+), 18 deletions(-) create mode 100644 fleche/span.ml create mode 100644 fleche/span.mli diff --git a/CHANGES.md b/CHANGES.md index 3d257e03..11473f02 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -63,6 +63,7 @@ - new trim command (both in the server and in VSCode) to liberate space used in the cache (@ejgallego, #662, fixes #367 cc: #253 #236 #348) + - completion and notation display (@ejgallego, #41 ???) # coq-lsp 0.1.8.1: Spring fix ----------------------------- diff --git a/controller/rq_completion.ml b/controller/rq_completion.ml index dd7e1243..3928d6f0 100644 --- a/controller/rq_completion.ml +++ b/controller/rq_completion.ml @@ -91,19 +91,43 @@ let get_char_at_point ~(doc : Fleche.Doc.t) ~point = None (* point is a utf char! *) -let completion ~token:_ ~doc ~point = +(* let completion ~token:_ ~doc ~point = *) + +let build_doc_idents_and_nametab ~token ~doc ~point prefix = + let st = Fleche.Info.LC.node ~doc ~point PrevIfEmpty in + let st = Option.map Fleche.Doc.Node.state st in + let st = Option.default doc.Fleche.Doc.root st in + let toc = build_doc_idents ~doc in + let open Coq.Protect.E.O in + let+ nametab = Fleche.Info.Completion.candidates ~token ~st prefix in + let nametab = Option.default [] nametab in + let nametab = CList.map (fun label -> mk_completion ~label ()) nametab in + toc @ nametab + +(* point is a utf-16 charpoint! *) +let completion ~token ~doc ~point = (* Instead of get_char_at_point we should have a CompletionContext.t, to be addressed in further completion PRs *) - (match get_char_at_point ~doc ~point with + match get_char_at_point ~doc ~point with | None -> let incomplete = true in let items = [] in - mk_completion_list ~incomplete ~items + mk_completion_list ~incomplete ~items |> Result.ok |> Coq.Protect.E.ok | Some c -> - let incomplete, items = - if c = '\\' then (false, unicode_list point) - else (true, build_doc_idents ~doc) + let open Coq.Protect.E.O in + let+ incomplete, items = + if c = '\\' then Coq.Protect.E.ok (false, unicode_list point) + else + (* We want to get the previous *) + let point = (fst point, max (snd point - 1) 0) in + let prefix = Rq_common.get_id_at_point ~contents:doc.contents ~point in + let prefix = Option.default (String.make 1 c) prefix in + let+ items = build_doc_idents_and_nametab ~token ~doc ~point prefix in + (true, items) in let res = mk_completion_list ~incomplete ~items in - res) - |> Result.ok + Result.ok res + +let completion ~token ~doc ~point = + let f () = completion ~token ~doc ~point in + Request.R.of_execution ~name:"completion" ~f () diff --git a/etc/todo.org b/etc/todo.org index 6eab1ec9..2112d65e 100644 --- a/etc/todo.org +++ b/etc/todo.org @@ -4,13 +4,16 @@ info. * Coq LSP Todos +** 0.2 + - jump to definition + - warnings suggestions / fix + +** 0.3 - profit from command refinement - lsp server process and coq-lsp-checker client for every document - dune integration, auto-build, dap - documentation links - - jump to definition - integration with tracing - - warnings suggestions / fix - flags for coq process - Implement onsave => compile vo file? [see on-disk cache issues below] diff --git a/fleche/debug.ml b/fleche/debug.ml index 06a3b82f..d3b8c370 100644 --- a/fleche/debug.ml +++ b/fleche/debug.ml @@ -12,6 +12,9 @@ let send = false || all || lsp let read = false || all || lsp let lsp_init = false || all || lsp +(* finding tokens from a position *) +let find = false || all + (* Parsing (this is a bit expensive as it will call the printer *) let parsing = false || all @@ -31,4 +34,4 @@ let sched_wakeup = false || all let request_delay = true || all (* Competion *) -let completion = false || all +let completion = true || all diff --git a/fleche/info.ml b/fleche/info.ml index 1cdd1253..da847a3c 100644 --- a/fleche/info.ml +++ b/fleche/info.ml @@ -69,6 +69,7 @@ module LineCol : Point with type t = int * int = struct if line1 = line && line2 = line then col1 <= col && col < col2 else (line1 = line && col1 <= col) || (line2 = line && col < col2) + (* Point is beyond [range] *) let gt_range ?range (line, col) = match range with | None -> false @@ -172,6 +173,18 @@ module Goals = struct end module Completion = struct + let obind f x = Option.bind x f + + (* let find ~doc ~point approx = *) + (* let res = find ~doc ~point approx in *) + (* match res with *) + (* | Some res -> *) + (* Io.Log.trace "info:find" ("found node at " ^ P.to_string point); *) + (* Some res *) + (* | None -> *) + (* Io.Log.trace "info:find" ("failed at " ^ P.to_string point); *) + (* None *) + (* XXX: This belongs in Coq *) let pr_extref gr = match gr with @@ -180,13 +193,57 @@ module Completion = struct (* XXX This may fail when passed "foo." for example, so more sanitizing is needed *) - let to_qualid p = try Some (Libnames.qualid_of_string p) with _ -> None + let remove_dot_if_last p : string = + let l = String.length p in + if l > 1 then if p.[l - 1] = '.' then String.sub p 0 (l - 1) else p else p + + (* let candidates ~token ~st prefix = *) + (* let ( let* ) = Option.bind in *) + (* Coq.State.in_state ~token ~st prefix ~f:(fun prefix -> *) + (* let* p = to_qualid prefix in *) + (* Nametab.completion_canditates p *) + (* |> List.map (fun x -> Pp.string_of_ppcmds (pr_extref x)) *) + (* |> some) *) + let to_qualid p = + let p = remove_dot_if_last p in + try Some (Libnames.qualid_of_string p) + with _ -> + Io.Log.trace "completion" ("broken qualid_of_string: " ^ p); + None + + let completion ~token ~st prefix = + Coq.State.in_state ~token ~st prefix ~f:(fun prefix -> + to_qualid prefix + |> obind (fun p -> + Nametab.completion_canditates p + |> List.map (fun x -> Pp.string_of_ppcmds (pr_extref x)) + |> List.append + (Notgram_ops.get_defined_notations () |> List.map snd) + |> some)) + + let _get_id_at_node_point offset range text = Span.find ~offset ~range text + let debug_completion cat msg = + if Debug.completion then Io.Log.trace ("completion: " ^ cat) msg + + let pr_completion_res = function + | None -> "no results" + | Some res -> string_of_int (List.length res) ^ " results" + + (* This is still buggy for the case that find doesn't work (i.e. no ast) *) + (* let candidates ~st ~point:_ () = *) let candidates ~token ~st prefix = - let ( let* ) = Option.bind in - Coq.State.in_state ~token ~st prefix ~f:(fun prefix -> - let* p = to_qualid prefix in - Nametab.completion_canditates p - |> List.map (fun x -> Pp.string_of_ppcmds (pr_extref x)) - |> some) + (* we do exact matching for... *) + (* let range = node.Doc.Node.range in *) + (* let text = doc.Doc.contents.text in *) + (* let span = Span.make ~contents:doc.Doc.contents ~loc in *) + (* let offset = P.to_offset point text in *) + (* debug_completion "offset" (string_of_int offset); *) + (* let prefix = get_id_at_node_point offset range text in *) + (* let prefix = "" in *) + debug_completion "prefix" prefix; + let open Coq.Protect.E.O in + let+ res = completion ~token ~st prefix in + debug_completion "n results" (pr_completion_res res); + res end diff --git a/fleche/span.ml b/fleche/span.ml new file mode 100644 index 00000000..ea815543 --- /dev/null +++ b/fleche/span.ml @@ -0,0 +1,50 @@ +(************************************************************************) +(* Coq Language Server Protocol *) +(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *) +(* Copyright 2022 Inria -- Dual License LGPL 2.1 / GPL3+ *) +(* Written by: Emilio J. Gallego Arias *) +(************************************************************************) +(* Status: Experimental *) +(************************************************************************) + +type t = + { range : Lang.Range.t + ; contents : String.t + } + +let make ~contents ~range = { range; contents } + +let delim c = + match c with + | '\n' | ' ' -> true + | _ -> false + +let rec find_backwards_delim offset lower text = + if offset = lower then offset + else if delim text.[offset - 1] then offset + else find_backwards_delim (offset - 1) lower text + +let rec id_at_point acc offset upper text = + if delim text.[offset] || offset + 1 = upper then acc + else id_at_point (text.[offset] :: acc) (offset + 1) upper text + +let id_at_point offset upper text = + let id = id_at_point [] offset upper text |> List.rev in + let len = List.length id in + String.init len (List.nth id) + +let debug_find cat msg = + if Debug.find then Io.Log.trace ("Span.find: " ^ cat) msg + +let find ~offset ~(range : Lang.Range.t) text = + let lower = range.start.offset in + let upper = range.end_.offset in + debug_find "lower / upper" (string_of_int lower ^ "/" ^ string_of_int upper); + debug_find "text length" (string_of_int (String.length text)); + let rtext = String.sub text lower (upper - lower) in + debug_find "ranged" rtext; + debug_find "char at off" (String.make 1 text.[offset]); + debug_find "initial offset" (string_of_int offset); + let offset = find_backwards_delim offset lower text in + debug_find "span.find, base offset" (string_of_int offset); + id_at_point offset upper text diff --git a/fleche/span.mli b/fleche/span.mli new file mode 100644 index 00000000..df386cbd --- /dev/null +++ b/fleche/span.mli @@ -0,0 +1,34 @@ +(************************************************************************) +(* Coq Language Server Protocol *) +(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *) +(* Copyright 2022 Inria -- Dual License LGPL 2.1 / GPL3+ *) +(* Written by: Emilio J. Gallego Arias *) +(************************************************************************) +(* Status: Experimental *) +(************************************************************************) + +type t = + { range : Lang.Range.t + ; contents : String.t + } + +val make : contents:String.t -> range:Lang.Range.t -> t + +(** [find ~offset ~range text] finds an identifier at offset, offset is + absolutely positioned *) +val find : offset:int -> range:Lang.Range.t -> string -> string + +(** TODO: + + - We want some kind of tokenization for the span, two kinds of spans, with + AST, and without *) + +(** Focused text span on a range / XXX same structure than caching *) + +(** + type context = + | Parsed of { span : t; node : Doc.node } + (** [span] corresponding to [node] *) + | Text of { span : t; prev : Doc.node } + (** Independent [span], [prev] node for help *) +*)