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

Refactor observe id #693

Merged
merged 4 commits into from
Nov 30, 2023
Merged

Refactor observe id #693

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
8e967dd
Refactor observe_id.
rtetley Aug 29, 2023
7a06d45
Correct unit tests.
rtetley Nov 24, 2023
22784f6
Reset view when switching from continuous to manual.
rtetley Nov 27, 2023
d17a89c
Fix Hashtbl.find_opt regression.
rtetley Nov 30, 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
1 change: 1 addition & 0 deletions language-server/dm/document.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -332,6 +332,7 @@ let validate_document ({ parsed_loc; raw_doc; } as document) =
(* We take the state strictly before parsed_loc to cover the case when the
end of the sentence is editted *)
let (stop, synterp_state, _scheduler_state) = state_strictly_before document parsed_loc in
(* let top_id = find_sentence_strictly_before document parsed_loc with None -> Top | Some sentence -> Id sentence.id 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
Expand Down
116 changes: 79 additions & 37 deletions language-server/dm/documentManager.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,13 +20,23 @@ open Types

let Log log = Log.mk_log "documentManager"

type observe_id = Id of Types.sentence_id | Top

let to_sentence_id = function
| Top -> None
| Id id -> Some id

(* let observe_id_to_string = function
| Top -> "Top"
| Id id -> Stateid.to_string id *)

type state = {
uri : DocumentUri.t;
init_vs : Vernacstate.t;
opts : Coqargs.injection_command list;
document : Document.document;
execution_state : ExecutionManager.state;
observe_id : Types.sentence_id option;
observe_id : observe_id option;
}

type event =
Expand Down Expand Up @@ -87,17 +97,23 @@ let executed_ranges doc execution_state loc =
}

let executed_ranges st =
let loc = match Option.bind st.observe_id (Document.get_sentence st.document) with
| None -> 0
| Some { stop } -> stop
let loc = match st.observe_id with
| None -> max_int
| Some Top -> 0
| Some (Id id) -> match Document.get_sentence st.document id with
| None -> failwith "observe_id does not exist"
| Some { stop } -> stop
in
executed_ranges st.document st.execution_state loc

let observe_id_range st =
let doc = Document.raw_document st.document in
match Option.bind st.observe_id (Document.get_sentence st.document) with
match st.observe_id with
| None -> None
| Some { start; stop} ->
| Some Top -> None
| Some (Id id) -> match Document.get_sentence st.document id with
| None -> failwith "observe_id does not exist"
| Some { start; stop } ->
let start = RawDocument.position_of_loc doc start in
let end_ = RawDocument.position_of_loc doc stop in
let range = Range.{ start; end_ } in
Expand Down Expand Up @@ -144,8 +160,12 @@ let id_of_pos st pos =
| None -> None
| Some { id } -> Some id

let id_of_pos_opt st = function
| None -> begin match st.observe_id with None | Some Top -> None | Some Id id -> Some id end
| Some pos -> id_of_pos st pos

let get_messages st pos =
match Option.cata (id_of_pos st) st.observe_id pos with
match id_of_pos_opt st pos with
| None -> log "get_messages: Could not find id";[]
| Some id -> log "get_messages: Found id";
let error = ExecutionManager.error st.execution_state id in
Expand All @@ -155,11 +175,10 @@ let get_messages st pos =
| Some (_oloc,msg) -> (DiagnosticSeverity.Error, pp_of_coqpp msg) :: feedback
| None -> feedback

let interpret_to ~stateful ~background state id : (state * event Sel.Event.t list) =
let observe ~background state id : (state * event Sel.Event.t list) =
match Document.get_sentence state.document id with
| None -> (state, []) (* TODO error? *)
| Some { id } ->
let state = if stateful then { state with observe_id = Some id } else state in
| Some {id } ->
let vst_for_next_todo, todo = ExecutionManager.build_tasks_for (Document.schedule state.document) state.execution_state id in
if CList.is_empty todo then
(state, [])
Expand All @@ -168,48 +187,61 @@ let interpret_to ~stateful ~background state id : (state * event Sel.Event.t lis
let event = Sel.now ?priority (Execute {id; vst_for_next_todo; todo; started = Unix.gettimeofday (); background }) in
(state, [ event ])

let interpret_to_position ~stateful st pos =
let clear_observe_id st =
{ st with observe_id = None }

let reset_to_top st =
{ st with observe_id = Some Top }

let interpret_to st id =
let observe_id = if st.observe_id = None then None else (Some (Id id)) in
let st = { st with observe_id} in
observe ~background:false st id

let interpret_to_position st pos =
match id_of_pos st pos with
| None -> (st, []) (* document is empty *)
| Some id -> interpret_to ~stateful ~background:false st id
| Some id -> interpret_to st id

let interpret_to_previous st =
match st.observe_id with
| None -> (st, [])
| Some oid ->
match Document.get_sentence st.document oid with
| None -> failwith "interpret to previous with no observe_id"
| Some Top -> (st, [])
| Some (Id id) ->
match Document.get_sentence st.document id with
| None -> (st, []) (* TODO error? *)
| Some { start } ->
match Document.find_sentence_before st.document start with
| None ->
Vernacstate.unfreeze_full_state st.init_vs;
{ st with observe_id=None}, []
| Some { id } -> interpret_to ~stateful:true ~background:false st id
{ st with observe_id=(Some Top)}, []
| Some { id } -> interpret_to st id

let interpret_to_next st =
match st.observe_id with
| None ->
| None -> failwith "interpret to next with no observe_id"
| Some Top ->
begin match Document.get_first_sentence st.document with
| None -> (st, []) (*The document is empty*)
| Some {id} -> interpret_to ~stateful:true ~background:false st id
| Some {id} -> interpret_to st id
end
| Some id ->
| Some (Id id) ->
match Document.get_sentence st.document id with
| None -> (st, []) (* TODO error? *)
| Some { stop } ->
match Document.find_sentence_after st.document (stop+1) with
| None -> (st, [])
| Some {id } -> interpret_to ~stateful:true ~background:false st id
| Some {id } -> interpret_to st id

let interpret_to_end st =
match Document.get_last_sentence st.document with
match Document.get_last_sentence st.document with
| None -> (st, [])
| Some {id} -> log ("interpret_to_end id = " ^ Stateid.to_string id); interpret_to ~stateful:true ~background:false st id
| Some {id} -> log ("interpret_to_end id = " ^ Stateid.to_string id); interpret_to st id

let interpret_in_background st =
match Document.get_last_sentence st.document with
match Document.get_last_sentence st.document with
| None -> (st, [])
| Some {id} -> log ("interpret_to_end id = " ^ Stateid.to_string id); interpret_to ~stateful:true ~background:true st id
| Some {id} -> log ("interpret_to_end id = " ^ Stateid.to_string id); observe ~background:true st id

let is_above st id1 id2 =
let range1 = Document.range_of_id st id1 in
Expand All @@ -219,16 +251,18 @@ let is_above st id1 id2 =
let validate_document state =
let unchanged_id, invalid_roots, document = Document.validate_document state.document in
let observe_id = match unchanged_id, state.observe_id with
| None, _ | _, None -> None
| Some id, Some id' -> if is_above state.document id id' then Some id else Some id'
| _, None -> None
| None, Some (Id _) -> None
| _, Some Top -> Some Top
| Some id, Some (Id id') -> if is_above state.document id id' then Some (Id id) else state.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_roots) in
{ state with document; execution_state; observe_id }

let init init_vs ~opts uri ~text =
let init init_vs ~opts uri ~text observe_id =
Vernacstate.unfreeze_full_state init_vs;
let top = try Coqargs.(dirpath_of_top (TopPhysical (DocumentUri.to_path uri))) with
e -> raise e
Expand All @@ -237,16 +271,17 @@ let init init_vs ~opts uri ~text =
let init_vs = Vernacstate.freeze_full_state () in
let document = Document.create_document init_vs.Vernacstate.synterp text in
let execution_state, feedback = ExecutionManager.init init_vs in
let st = { uri; opts; init_vs; document; execution_state; observe_id = None } in
let st = { uri; opts; init_vs; document; execution_state; observe_id } in
validate_document st, [inject_em_event feedback]

let reset { uri; opts; init_vs; document; execution_state } =
let reset { uri; opts; init_vs; document; execution_state; observe_id } =
let text = RawDocument.text @@ Document.raw_document document in
Vernacstate.unfreeze_full_state init_vs;
let document = Document.create_document init_vs.synterp text in
ExecutionManager.destroy execution_state;
let execution_state, feedback = ExecutionManager.init init_vs in
let st = { uri; opts; init_vs; document; execution_state; observe_id = None } in
let observe_id = if observe_id = None then None else (Some Top) in
let st = { uri; opts; init_vs; document; execution_state; observe_id} in
validate_document st, [inject_em_event feedback]

let apply_text_edits state edits =
Expand Down Expand Up @@ -285,7 +320,12 @@ let get_proof st diff_mode pos =
let oid = fst @@ Scheduler.task_for_sentence (Document.schedule st.document) id in
Option.bind oid (ExecutionManager.get_vernac_state st.execution_state)
in
let oid = Option.cata (id_of_pos st) st.observe_id pos in
let observe_id =
match st.observe_id with
| None -> None
| Some observe_id -> to_sentence_id observe_id
in
let oid = Option.cata (id_of_pos st) observe_id pos in
let ost = Option.bind oid (ExecutionManager.get_vernac_state st.execution_state) in
let previous = Option.bind oid previous_st in
Option.bind ost (ProofState.get_proof ~previous diff_mode)
Expand Down Expand Up @@ -315,7 +355,7 @@ let parse_entry st pos entry pattern =

let about st pos ~pattern =
let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in
match get_context st pos with
match get_context st pos with
| None -> Error ("No context found") (*TODO execute *)
| Some (sigma, env) ->
try
Expand All @@ -341,7 +381,7 @@ let hover st pos =
| Some pattern ->
log ("hover: found word at cursor: " ^ pattern);
let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in
match get_context st pos with
match get_context st pos with
| None -> log "hover: no context found"; None
| Some (sigma, env) ->
try
Expand All @@ -354,7 +394,7 @@ let hover st pos =

let check st pos ~pattern =
let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in
match get_context st pos with
match get_context st pos with
| None -> Error ("No context found") (*TODO execute *)
| Some (sigma,env) ->
let rc = parse_entry st loc Pcoq.Constr.lconstr pattern in
Expand All @@ -378,7 +418,7 @@ let locate st pos ~pattern =

let print st pos ~pattern =
let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in
match get_context st pos with
match get_context st pos with
| None -> Error("No context found")
| Some (sigma, env) ->
let qid = parse_entry st loc (Pcoq.Prim.smart_global) pattern in
Expand All @@ -397,7 +437,9 @@ module Internal = struct
st.execution_state

let observe_id st =
st.observe_id
match st.observe_id with
| None | Some Top -> None
| Some (Id id) -> Some id

let validate_document st =
validate_document st
Expand Down
14 changes: 11 additions & 3 deletions language-server/dm/documentManager.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,14 +24,16 @@ open CompletionItems
and get feedback. Note that it does not require IDEs to parse vernacular
sentences. *)

type observe_id = Id of Types.sentence_id | Top

type state

type event
val pp_event : Format.formatter -> event -> unit

type events = event Sel.Event.t list

val init : Vernacstate.t -> opts:Coqargs.injection_command list -> DocumentUri.t -> text:string -> state * events
val init : Vernacstate.t -> opts:Coqargs.injection_command list -> DocumentUri.t -> text:string -> observe_id option -> state * events
(** [init st opts uri text] initializes the document manager with initial vernac state
[st] on which command line opts will be set. *)

Expand All @@ -40,7 +42,13 @@ val apply_text_edits : state -> text_edit list -> state
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)
val clear_observe_id : state -> state
(** [clear_observe_id state] updates the state to make the observe_id None *)

val reset_to_top : state -> state
(** [reset_to_top state] updates the state to make the observe_id Top *)

val interpret_to_position : state -> Position.t -> (state * events)
(** [interpret_to_position stateful doc pos] navigates to the last sentence ending
before or at [pos] and returns the resulting state. The [stateful] flag
determines if we record the resulting position in the state. *)
Expand Down Expand Up @@ -111,7 +119,7 @@ module Internal : sig
val raw_document : state -> RawDocument.t
val execution_state : state -> ExecutionManager.state
val string_of_state : state -> string
val observe_id : state -> Types.sentence_id option
val observe_id : state -> sentence_id option

val validate_document : state -> state
(** [validate_document doc] reparses the text of [doc] and invalidates the
Expand Down
2 changes: 1 addition & 1 deletion language-server/tests/common.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ let injections =
let init_state = Vernacstate.freeze_full_state ()

let openDoc uri ~text =
DocumentManager.init init_state ~opts:injections uri ~text
DocumentManager.init init_state ~opts:injections uri ~text (Some DocumentManager.Top)

let run r =
[%test_pred: (_,string) Result.t ] (function Error _ -> false | _ -> true) r;
Expand Down
44 changes: 0 additions & 44 deletions language-server/tests/dm_tests.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -209,50 +209,6 @@ let%test_unit "step_backward.document_begin" =
let st = handle_events todo st in
[%test_eq: bool] (Option.is_none (DocumentManager.Internal.observe_id st)) true

(* With this test we can check that interpret_in_background has lower priority then interpret to *)
let%test_unit "interpret_in_background.interpret_to stateful" =
let st, init_events = init_test_doc ~text:"Definition x := true. Definition y := false. Definition z := 0." in
let st, (s1, (s2, (s3, ()))) = dm_parse st (P (P (P O))) in
let todo = Sel.Todo.(add empty init_events) in
let st = handle_events todo st in
let st1, events = DocumentManager.interpret_in_background st in
let todo = Sel.Todo.(add empty events) in
let position = RawDocument.position_of_loc (DocumentManager.Internal.raw_document st) s2.stop in
let st2, events = DocumentManager.interpret_to_position ~stateful:true st1 position in
let todo = Sel.Todo.(add todo events) in
let st = handle_events todo st1 in
[%test_pred: sentence_id option] (Option.equal Stateid.equal (Some s3.id)) (DocumentManager.Internal.observe_id st)

(* With this test interpret_to_end and interpret_to have the same priority, and interpret to is stateful
so it will modify observe id, they will get executed in order of insertion, hence observe_id = s2.id *)
let%test_unit "interpret_to_end.interpret_to stateful" =
let st, init_events = init_test_doc ~text:"Definition x := true. Definition y := false. Definition z := 0." in
let st, (s1, (s2, (s3, ()))) = dm_parse st (P (P (P O))) in
let todo = Sel.Todo.(add empty init_events) in
let st = handle_events todo st in
let st, events = DocumentManager.interpret_to_end st in
let todo = Sel.Todo.(add empty events) in
let position = RawDocument.position_of_loc (DocumentManager.Internal.raw_document st) s2.stop in
let st, events = DocumentManager.interpret_to_position ~stateful:true st position in
let todo = Sel.Todo.(add todo events) in
let st = handle_events todo st in
[%test_pred: sentence_id option] (Option.equal Stateid.equal (Some s2.id)) (DocumentManager.Internal.observe_id st)

(* With this test interpret_to_end and interpret_to have the same priority, and interpret to is not stateful
so it will not modify observe id, they will get executed in order of insertion, hence observe_id = s3.id *)
let%test_unit "interpret_to_end.interpret_to not stateful" =
let st, init_events = init_test_doc ~text:"Definition x := true. Definition y := false. Definition z := 0." in
let st, (s1, (s2, (s3, ()))) = dm_parse st (P (P (P O))) in
let todo = Sel.Todo.(add empty init_events) in
let st = handle_events todo st in
let st, events = DocumentManager.interpret_to_end st in
let todo = Sel.Todo.(add empty events) in
let position = RawDocument.position_of_loc (DocumentManager.Internal.raw_document st) s2.stop in
let st, events = DocumentManager.interpret_to_position ~stateful:false st position in
let todo = Sel.Todo.(add todo events) in
let st = handle_events todo st in
[%test_pred: sentence_id option] (Option.equal Stateid.equal (Some s3.id)) (DocumentManager.Internal.observe_id st)

(*
let%test_unit "exec.insert" =
let st, events = init_test_doc ~text:"Definition x := true. Definition y := false." in
Expand Down
Loading
Loading