Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

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

Merged
merged 2 commits into from
Aug 2, 2023
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
93a188b
Rework document validation
maximedenes Aug 2, 2023
09573e0
Fix handling of end-of-sentence text edits w.r.t. observe id
maximedenes Aug 2, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
73 changes: 36 additions & 37 deletions language-server/dm/document.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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

Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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

Expand Down
10 changes: 5 additions & 5 deletions language-server/dm/document.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;
Expand Down
49 changes: 24 additions & 25 deletions language-server/dm/documentManager.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 =
Expand Down
18 changes: 10 additions & 8 deletions language-server/dm/documentManager.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
1 change: 0 additions & 1 deletion language-server/tests/common.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
49 changes: 35 additions & 14 deletions language-server/tests/d_tests.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;
Expand All @@ -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;
()
Loading
Loading