From d85df500fdb182f16bfdf894e042d9768afeb28c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Thu, 22 Dec 2022 22:40:41 +0100
Subject: [PATCH] [fleche] Resume checking from common prefix on new version.

This does greatly reduce latency when editing deep down in a
document; closes #110 .

Also, kind of makes the need for parsing caching (#25, #36) moot, at
least with the current checking workflow.
---
 CHANGES.md    |  6 ++++--
 fleche/doc.ml | 43 +++++++++++++++++++++++++++++++++++++++----
 2 files changed, 43 insertions(+), 6 deletions(-)

diff --git a/CHANGES.md b/CHANGES.md
index 542da3648..5da3d540b 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,8 +1,8 @@
 # coq-lsp 0.1.1: Location
 -------------------------
 
- - Don't crash if the log file can't be created (@ejgallego , #87)
- - Use LSP functions for client-side logging (@ejgallego , #87)
+ - Don't crash if the log file can't be created (@ejgallego, #87)
+ - Use LSP functions for client-side logging (@ejgallego, #87)
  - Log `_CoqProject` detection settings to client window (@ejgallego, #88)
  - Use plugin include paths from `_CoqProject` (@ejgallego, #88)
  - Support OCaml >= 4.12 (@ejgallego, #93)
@@ -21,6 +21,8 @@
    fixes #89)
  - Show file position in goal buffer, use collapsible elements for
    goal list (@ejgallego, #115, fixes #109)
+ - Resume checking from common prefix on document update (@ejgallego,
+   #111, fixes #110)
 
 # coq-lsp 0.1.0: Memory
 -----------------------
diff --git a/fleche/doc.ml b/fleche/doc.ml
index cdecde750..d7a4726c6 100644
--- a/fleche/doc.ml
+++ b/fleche/doc.ml
@@ -66,16 +66,48 @@ let create ~state ~workspace ~uri ~version ~contents =
   ; completed = Stopped (init_loc ~uri)
   }
 
+let recover_up_to_offset doc offset =
+  Io.Log.error "prefix"
+    (Format.asprintf "common prefix offset found at %d" offset);
+  let rec find acc_nodes acc_loc nodes =
+    match nodes with
+    | [] -> (List.rev acc_nodes, acc_loc)
+    | n :: ns ->
+      Io.Log.error "scan"
+        (Format.asprintf "consider node at %s" (Coq.Ast.pr_loc n.loc));
+      if n.loc.Loc.ep >= offset then (List.rev acc_nodes, acc_loc)
+      else find (n :: acc_nodes) n.loc ns
+  in
+  let loc = init_loc ~uri:doc.uri in
+  find [] loc doc.nodes
+
+let compute_common_prefix ~contents doc =
+  let s1 = doc.contents in
+  let l1 = String.length s1 in
+  let s2 = contents in
+  let l2 = String.length s2 in
+  let rec match_or_stop i =
+    if i = l1 || i = l2 then i
+    else if Char.equal s1.[i] s2.[i] then match_or_stop (i + 1)
+    else i
+  in
+  let common_idx = match_or_stop 0 in
+  let nodes, loc = recover_up_to_offset doc common_idx in
+  Io.Log.error "prefix" ("resuming from " ^ Coq.Ast.pr_loc loc);
+  let completed = Completion.Stopped loc in
+  (nodes, completed)
+
 let bump_version ~version ~contents doc =
+  (* When a new document, we resume checking from a common prefix *)
+  let nodes, completed = compute_common_prefix ~contents doc in
   let end_loc = get_last_text contents in
-  (* We need to resume checking in full when a new document *)
   { doc with
     version
-  ; nodes = []
+  ; nodes
   ; contents
   ; end_loc
-  ; diags_dirty = false
-  ; completed = Stopped (init_loc ~uri:doc.uri)
+  ; diags_dirty = true (* EJGA: Is it worth to optimize this? *)
+  ; completed
   }
 
 let add_node ~node doc =
@@ -338,6 +370,9 @@ let process_and_parse ~uri ~version ~fb_queue doc last_tok doc_handle =
           stm doc st last_tok_new))
   in
   (* Note that nodes and diags in reversed order here *)
+  (match doc.nodes with
+  | [] -> ()
+  | n :: _ -> Io.Log.error "resume" ("last node :" ^ Coq.Ast.pr_loc n.loc));
   let st =
     hd_opt ~default:doc.root (List.map (fun { state; _ } -> state) doc.nodes)
   in