Merge pull request #534 from coq-community/fix-end-sentence-edits

Fix handling of end-of-sentence text edits w.r.t. observe id

language-server/dm/document.ml

@@ -78,12 +78,6 @@ let range_of_id document id =
 let parse_errors parsed =
   List.map snd (LM.bindings parsed.parsing_errors_by_end)
 
-let set_parse_errors parsed errors =
-  let parsing_errors_by_end =
-    List.fold_left (fun acc error -> LM.add error.stop error acc) LM.empty errors
-  in
-  { parsed with parsing_errors_by_end }
-
 let add_sentence parsed start stop (ast: parsed_ast) synterp_state scheduler_state_before =
   let id = Stateid.fresh () in
   let ast' = (ast.ast, ast.classification, synterp_state) in
@@ -122,6 +116,9 @@ let sentences_after parsed loc =
   let after = Option.cata (fun v -> LM.add loc v after) after ov in
   List.map (fun (_id,s) -> s) @@ LM.bindings after
 
+let parsing_errors_before parsed loc =
+  LM.filter (fun stop _v -> stop <= loc) parsed.parsing_errors_by_end
+
 let get_sentence parsed id =
   SM.find_opt id parsed.sentences_by_id
 
@@ -135,6 +132,11 @@ let find_sentence_before parsed loc =
   | Some (_, sentence) -> Some sentence
   | _ -> None
 
+let find_sentence_strictly_before parsed loc =
+  match LM.find_last_opt (fun k -> k < loc) parsed.sentences_by_end with
+  | Some (_, sentence) -> Some sentence
+  | _ -> None
+
 let find_sentence_after parsed loc = 
   match LM.find_first_opt (fun k -> loc <= k) parsed.sentences_by_end with
   | Some (_, sentence) -> Some sentence
@@ -151,11 +153,14 @@ let state_after_sentence = function
     (stop, synterp_state, scheduler_state_after)
   | None -> (-1, Vernacstate.Synterp.init (), Scheduler.initial_state)
 
-(** Returns the state at position [pos] if it does not require execution *)
 let state_at_pos parsed pos =
   state_after_sentence @@
     LM.find_last_opt (fun stop -> stop <= pos) parsed.sentences_by_end
 
+let state_strictly_before parsed pos =
+  state_after_sentence @@
+    LM.find_last_opt (fun stop -> stop < pos) parsed.sentences_by_end
+
 let pos_at_end parsed =
   match LM.max_binding_opt parsed.sentences_by_end with
   | Some (stop, _) -> stop
@@ -235,8 +240,6 @@ let rec junk_sentence_end stream =
   | [] -> ()
   | _ ->  Stream.junk () stream; junk_sentence_end stream
 
-
-(** TODO move inside ParsedDoc, remove set_parsing_errors *)
 let rec parse_more synterp_state stream raw parsed errors =
   let handle_parse_error start msg =
     log @@ "handling parse error at " ^ string_of_int start;
@@ -288,29 +291,18 @@ let rec parse_more synterp_state stream raw parsed errors =
 let parse_more synterp_state stream raw =
   parse_more synterp_state stream raw [] []
 
-let invalidate top_edit parsed_doc new_sentences =
-  (* Algo:
-  We parse the new doc from the topmost edit to the bottom one.
-  - If execution is required, we invalidate everything after the parsing
-  effect. Then we diff the truncated zone and invalidate execution states.
-  - If the previous doc contained a parsing effect in the editted zone, we also invalidate.
-  Otherwise, we diff the editted zone.
-  We invalidate dependents of changed/removed/added sentences (according to
-  both/old/new graphs). When we have to invalidate a parsing effect state, we
-  invalidate the parsing after it.
-   *)
-   (* TODO optimize by reducing the diff to the modified zone *)
-   (*
-  let text = RawDocument.text current.raw_doc in
-  let len = String.length text in
-  let stream = Stream.of_string text in
-  let parsed_current = parse_more len stream current.parsed_doc () in
-  *)
+let rec unchanged_id id = function
+  | [] -> id
+  | Equal s :: diffs ->
+    unchanged_id (List.fold_left (fun _ (id,_) -> Some id) id s) diffs
+  | (Added _ | Deleted _) :: _ -> id
+
+let invalidate top_edit top_id parsed_doc new_sentences =
   let rec invalidate_diff parsed_doc scheduler_state invalid_ids = function
     | [] -> invalid_ids, parsed_doc
     | Equal s :: diffs ->
-      let patch_sentence (parsed_doc,scheduler_state) (old_s,new_s) =
-        patch_sentence parsed_doc scheduler_state old_s new_s
+      let patch_sentence (parsed_doc,scheduler_state) (id,new_s) =
+        patch_sentence parsed_doc scheduler_state id new_s
       in
       let parsed_doc, scheduler_state = List.fold_left patch_sentence (parsed_doc, scheduler_state) s in
       invalidate_diff parsed_doc scheduler_state invalid_ids diffs
@@ -330,22 +322,30 @@ let invalidate top_edit parsed_doc new_sentences =
   let (_,_synterp_state,scheduler_state) = state_at_pos parsed_doc top_edit in
   let old_sentences = sentences_after parsed_doc top_edit in
   let diff = diff old_sentences new_sentences in
+  let unchanged_id = unchanged_id top_id diff in
   log @@ "diff:\n" ^ string_of_diff parsed_doc diff;
-  invalidate_diff parsed_doc scheduler_state Stateid.Set.empty diff
+  let invalid_ids, doc = invalidate_diff parsed_doc scheduler_state Stateid.Set.empty diff in
+  unchanged_id, invalid_ids, doc
 
 (** Validate document when raw text has changed *)
 let validate_document ({ parsed_loc; raw_doc; } as document) =
-  let (stop, parsing_state, _scheduler_state) = state_at_pos document parsed_loc in
+  (* We take the state strictly before parsed_loc to cover the case when the
+  end of the sentence is editted *)
+  let (stop, parsing_state, _scheduler_state) = state_strictly_before document parsed_loc in
+  let top_id = Option.map (fun sentence -> sentence.id) (find_sentence_strictly_before document parsed_loc) in
   let text = RawDocument.text raw_doc in
   let stream = Stream.of_string text in
   while Stream.count stream < stop do Stream.junk () stream done;
   log @@ Format.sprintf "Parsing more from pos %i" stop;
-  let new_sentences, errors = parse_more parsing_state stream raw_doc (* TODO invalidate first *) in
+  let errors = parsing_errors_before document stop in
+  let new_sentences, new_errors = parse_more parsing_state stream raw_doc (* TODO invalidate first *) in
   log @@ Format.sprintf "%i new sentences" (List.length new_sentences);
-  let invalid_ids, document = invalidate (stop+1) document new_sentences in
-  let document = set_parse_errors document errors in
+  let unchanged_id, invalid_ids, document = invalidate (stop+1) top_id document new_sentences in
+  let parsing_errors_by_end =
+    List.fold_left (fun acc error -> LM.add error.stop error acc) errors new_errors
+  in
   let parsed_loc = pos_at_end document in
-  invalid_ids, { document with parsed_loc }
+  unchanged_id, invalid_ids, { document with parsed_loc; parsing_errors_by_end }
 
 let create_document text =
   let raw_doc = RawDocument.create text in
@@ -364,8 +364,7 @@ let apply_text_edit document edit =
 
 let apply_text_edits document edits =
   let doc' = { document with raw_doc = document.raw_doc } in
-  let doc = List.fold_left apply_text_edit doc' edits in
-  doc, doc.parsed_loc
+  List.fold_left apply_text_edit doc' edits
 
 module Internal = struct
 

language-server/dm/document.mli

@@ -28,9 +28,10 @@ val create_document : string -> document
 (** [create_document text] creates a fresh document with content defined by
     [text]. *)
 
-val validate_document : document -> sentence_id_set * document
+val validate_document : document -> sentence_id option * sentence_id_set * document
 (** [validate_document doc] parses the document without forcing any execution
-    and returns the set of invalidated sentences *)
+    and returns the id of the bottommost sentence of the prefix which has not changed
+    since the previous validation, as well as the set of invalidated sentences *)
 
 type parsed_ast = {
   ast: Synterp.vernac_control_entry;
@@ -48,10 +49,9 @@ val parse_errors : document -> parsing_error list
 (** [parse_errors doc] returns the list of sentences which failed to parse
     (see validate_document) together with their error message *)
 
-val apply_text_edits : document -> text_edit list -> document * int
+val apply_text_edits : document -> text_edit list -> document
 (** [apply_text_edits doc edits] updates the text of [doc] with [edits]. The new
-    text is not parsed or executed. The returned int is the start loc of the topmost
-    edit. *)
+    text is not parsed or executed. *)
 
 type sentence = {
   start : int;

language-server/dm/documentManager.ml

@@ -23,7 +23,7 @@ type state = {
   opts : Coqargs.injection_command list;
   document : Document.document;
   execution_state : ExecutionManager.state;
-  observe_id : Types.sentence_id option; (* TODO materialize observed loc and line-by-line execution status *)
+  observe_id : Types.sentence_id option;
 }
 
 type event =
@@ -131,14 +131,6 @@ let diagnostics st =
     List.map mk_error_diag exec_errors @
     List.map mk_diag feedback
 
-let init init_vs ~opts uri ~text =
-  let document = Document.create_document text in
-  Vernacstate.unfreeze_full_state init_vs;
-  let top = Coqargs.(dirpath_of_top (TopPhysical (Uri.path uri))) in
-  Coqinit.start_library ~top opts;
-  let execution_state, feedback = ExecutionManager.init (Vernacstate.freeze_full_state ()) in
-  { uri; opts; init_vs; document; execution_state; observe_id = None }, [inject_em_event feedback]
-
 let reset { uri; opts; init_vs; document; execution_state } =
   let text = RawDocument.text @@ Document.raw_document document in
   let document = Document.create_document text in
@@ -206,27 +198,31 @@ let interpret_in_background st =
   | None -> (st, [])
   | Some {id} -> log ("interpret_to_end id = " ^ Stateid.to_string id); interpret_to ~stateful:true ~background:true st id
 
-let retract state loc =
-  match Option.bind state.observe_id (Document.get_sentence state.document) with
-  | None -> state
-  | Some { stop } ->
-    if loc < stop then
-      let observe_id = Option.map (fun s -> s.Document.id) @@ Document.find_sentence_before state.document loc in
-      { state with observe_id }
-    else state
-
-let apply_text_edits state edits =
-  let document, loc = Document.apply_text_edits state.document edits in
-  let state = { state with document } in
-  retract state loc
-
 let validate_document state =
-  let invalid_ids, document = Document.validate_document state.document in
+  let unchanged_id, invalid_ids, document = Document.validate_document state.document in
+  let update_observe_id id =
+    if Stateid.Set.mem id invalid_ids then unchanged_id
+    else Some id
+  in
+  let observe_id = Option.bind state.observe_id update_observe_id in
   let execution_state =
     List.fold_left (fun st id ->
       ExecutionManager.invalidate (Document.schedule state.document) id st
       ) state.execution_state (Stateid.Set.elements invalid_ids) in
-  { state with document; execution_state }
+  { state with document; execution_state; observe_id }
+
+let init init_vs ~opts uri ~text =
+  let document = Document.create_document text in
+  Vernacstate.unfreeze_full_state init_vs;
+  let top = Coqargs.(dirpath_of_top (TopPhysical (Uri.path uri))) in
+  Coqinit.start_library ~top opts;
+  let execution_state, feedback = ExecutionManager.init (Vernacstate.freeze_full_state ()) in
+  let st = { uri; opts; init_vs; document; execution_state; observe_id = None } in
+  validate_document st, [inject_em_event feedback]
+
+let apply_text_edits state edits =
+  let document = Document.apply_text_edits state.document edits in
+  validate_document { state with document }
 
 let handle_event ev st =
   match ev with
@@ -357,6 +353,9 @@ module Internal = struct
   let observe_id st =
     st.observe_id
 
+  let validate_document st =
+    validate_document st
+
   let string_of_state st =
     let sentences = Document.sentences_sorted_by_loc st.document in
     let string_of_state id =

language-server/dm/documentManager.mli

@@ -33,14 +33,9 @@ val init : Vernacstate.t -> opts:Coqargs.injection_command list -> Uri.t -> text
     [st] on which command line opts will be set. *)
 
 val apply_text_edits : state -> text_edit list -> state
-(** [apply_text_edits doc edits] updates the text of [doc] with [edits]. The
-    new text is not parsed or executed. *)
-
-val validate_document : state -> state
-(** [validate_document doc] reparses the text of [doc] and invalidates the
-    states impacted by the diff with the previously validated content. If the
-    text of [doc] has not changed since the last call to [validate_document], it
-    has no effect. *)
+(** [apply_text_edits doc edits] updates the text of [doc] with [edits]. The new
+    document is parsed, outdated executions states are invalidated, and the observe
+    id is updated. *)
 
 val interpret_to_position : stateful:bool -> state -> Position.t -> (state * events)
 (** [interpret_to_position stateful doc pos] navigates to the last sentence ending
@@ -112,4 +107,11 @@ module Internal : sig
   val string_of_state : state -> string
   val observe_id : state -> Types.sentence_id option
 
+  val validate_document : state -> state
+  (** [validate_document doc] reparses the text of [doc] and invalidates the
+      states impacted by the diff with the previously validated content. If the
+      text of [doc] has not changed since the last call to [validate_document], it
+      has no effect. *)
+
+
 end

language-server/tests/common.ml

@@ -71,7 +71,6 @@ let d_sentences doc spec =
   r
 
 let dm_parse st spec =
-  let st = DocumentManager.validate_document st in
   let doc = DocumentManager.Internal.document st in
   st, d_sentences doc spec
 

language-server/tests/d_tests.ml

@@ -18,13 +18,15 @@ let uri = Uri.make ~scheme:"file" ~path:"foo" ()
 let %test_unit "document: invalidate top" =
   let dm, _ = openDoc uri ~text:"Definition x := 3. Lemma foo : x = 3. Proof. reflexivity. Qed." in
   let doc = DocumentManager.Internal.document dm in
-  let invalid, doc = Document.validate_document doc in
+  let unchanged, invalid, doc = Document.validate_document doc in
   [%test_eq: sentence_id list] [] (Stateid.Set.elements invalid);
   let s1,(s2,(s3,(s4,(s5,())))) = d_sentences doc (P(P(P(P(P(O)))))) in
-  let doc, _loc = Document.apply_text_edits doc [Document.range_of_id doc s1.id,"Definition x := 4."] in
-  let invalid, doc = Document.validate_document doc in
+  [%test_eq: sentence_id option] (Some s5.id) unchanged;
+  let doc = Document.apply_text_edits doc [Document.range_of_id doc s1.id,"Definition x := 4."] in
+  let unchanged, invalid, doc = Document.validate_document doc in
   let r1,(r2,(r3,(r4,(r5,())))) = d_sentences doc (P(P(P(P(P(O)))))) in
   [%test_eq: sentence_id list] [s1.id] (Stateid.Set.elements invalid);
+  [%test_eq: sentence_id option] None unchanged;
   [%test_eq: sentence_id] s2.id r2.id;
   [%test_eq: sentence_id] s3.id r3.id;
   [%test_eq: sentence_id] s4.id r4.id;
@@ -39,13 +41,15 @@ let %test_unit "document: invalidate top" =
 let %test_unit "document: invalidate proof" =
   let dm, _ = openDoc uri ~text:"Definition x := 3. Lemma foo : x = 3. Proof. reflexivity. Qed." in
   let doc = DocumentManager.Internal.document dm in
-  let invalid, doc = Document.validate_document doc in
+  let unchanged, invalid, doc = Document.validate_document doc in
   [%test_eq: sentence_id list] [] (Stateid.Set.elements invalid);
   let s1,(s2,(s3,(s4,(s5,())))) = d_sentences doc (P(P(P(P(P(O)))))) in
-  let doc, _loc = Document.apply_text_edits doc [Document.range_of_id doc s3.id,"idtac."] in
-  let invalid, doc = Document.validate_document doc in
+  [%test_eq: sentence_id option] (Some s5.id) unchanged;
+  let doc = Document.apply_text_edits doc [Document.range_of_id doc s3.id,"idtac."] in
+  let unchanged, invalid, doc = Document.validate_document doc in
   let r1,(r2,(r3,(r4,(r5,())))) = d_sentences doc (P(P(P(P(P(O)))))) in
   [%test_eq: sentence_id list] [s3.id] (Stateid.Set.elements invalid);
+  [%test_eq: sentence_id option] (Some s2.id) unchanged;
   [%test_eq: sentence_id] s1.id r1.id;
   [%test_eq: sentence_id] s2.id r2.id;
   [%test_eq: sentence_id] s4.id r4.id;
@@ -61,23 +65,40 @@ let %test_unit "document: invalidate proof" =
 let %test_unit "document: invalidate proof 2" =
   let dm, _ = openDoc uri ~text:"Definition x := 3. Lemma foo : x = 3. Proof. reflexivity. Qed." in
   let doc = DocumentManager.Internal.document dm in
-  let invalid, doc = Document.validate_document doc in
+  let unchanged, invalid, doc = Document.validate_document doc in
   [%test_eq: sentence_id list] [] (Stateid.Set.elements invalid);
   let s1,(s2,(s3,(s4,(s5,())))) = d_sentences doc (P(P(P(P(P(O)))))) in
-  let doc, _ = Document.apply_text_edits doc [Document.range_of_id doc s3.id,""] in
-  let (invalid, doc) = Document.validate_document doc in
+  [%test_eq: sentence_id option] (Some s5.id) unchanged;
+  let doc = Document.apply_text_edits doc [Document.range_of_id doc s3.id,""] in
+  let unchanged, invalid, doc = Document.validate_document doc in
   let r1,(r2,(r3,(r4,()))) = d_sentences doc (P(P(P(P(O))))) in
-  (* HERE THE BUG *)
-  ()
+  [%test_eq: sentence_id list] [s3.id;s4.id;s5.id] (Stateid.Set.elements invalid);
+  [%test_eq: sentence_id option] (Some s2.id) unchanged;
+  [%test_eq: sentence_id] s1.id r1.id;
+  [%test_eq: sentence_id] s2.id r2.id
 
 let %test_unit "document: delete line" = 
   let dm, _ = openDoc uri ~text:"Definition x:= 3. Lemma foo : x = 3. Proof. reflexitivity. Qed." in 
   let doc = DocumentManager.Internal.document dm in 
-  let invalid, doc = Document.validate_document doc in
+  let unchanged, invalid, doc = Document.validate_document doc in
   [%test_eq: sentence_id list] [] (Stateid.Set.elements invalid);
   let s1,(s2,(s3,(s4,(s5,())))) = d_sentences doc (P(P(P(P(P(O)))))) in
-  let doc, _loc = Document.apply_text_edits doc [Document.range_of_id doc s5.id,""] in
-  let invalid, doc = Document.validate_document doc in 
+  let doc = Document.apply_text_edits doc [Document.range_of_id doc s5.id,""] in
+  let unchanged, invalid, doc = Document.validate_document doc in 
   let sentences_id = Stateid.Set.of_list (List.map (Document.sentences doc) ~f:(fun s -> s.id)) in
   [%test_pred: sentence_id] (fun x -> not (Stateid.Set.mem x sentences_id)) s5.id;
+  ()
+
+let %test_unit "document: expand sentence" =
+  let dm, _ = openDoc uri ~text:"Lemma foo : x = 3. M." in
+  let doc = DocumentManager.Internal.document dm in
+  let unchanged, invalid, doc = Document.validate_document doc in
+  [%test_eq: sentence_id list] [] (Stateid.Set.elements invalid);
+  let s1,(s2,()) = d_sentences doc (P(P(O))) in
+  let range = Document.range_of_id doc s2.id in
+  let new_range = Lsp.LspData.Range.{ start = range.end_; end_ = range.end_ } in
+  let doc = Document.apply_text_edits doc [new_range,"foo."] in
+  let unchanged, invalid, doc = Document.validate_document doc in
+  let r1,(r2,()) = d_sentences doc (P(P(O))) in
+  [%test_eq: sentence_id] s1.id r1.id;
   ()