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

Block on parse error #1002

Open
wants to merge 4 commits into
base: main
Choose a base branch
from
+114 −52
Open

Block on parse error #1002

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
3723aa5
feat(document): add a sentence state (Parsed or Error)
rtetley Jan 21, 2025
e4016bf
fix: block on parse error
rtetley Jan 22, 2025
72a5a36
fix: test spec in common.ml
rtetley Jan 23, 2025
93bd0fe
fix: correct loc for error
rtetley Jan 30, 2025
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
96 changes: 63 additions & 33 deletions language-server/dm/document.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,12 +50,29 @@ type parsed_ast = {
tokens: Tok.t list
}

type comment = {
start: int;
stop: int;
content: string;
}

type parsing_error = {
start: int;
stop: int;
msg: string Loc.located;
qf: Quickfix.t list option;
}

type sentence_state =
| Error of parsing_error
| Parsed of parsed_ast

type pre_sentence = {
parsing_start : int;
start : int;
stop : int;
synterp_state : Vernacstate.Synterp.t; (* synterp state after this sentence's synterp phase *)
ast : parsed_ast;
ast : sentence_state;
}

(* Example: *)
Expand All @@ -70,23 +87,10 @@ type sentence = {
synterp_state : Vernacstate.Synterp.t; (* synterp state after this sentence's synterp phase *)
scheduler_state_before : Scheduler.state;
scheduler_state_after : Scheduler.state;
ast : parsed_ast;
ast : sentence_state;
id : sentence_id;
}

type comment = {
start: int;
stop: int;
content: string;
}

type parsing_error = {
start: int;
stop: int;
msg: string Loc.located;
qf: Quickfix.t list option;
}

type document = {
sentences_by_id : sentence SM.t;
sentences_by_end : sentence LM.t;
Expand Down Expand Up @@ -223,8 +227,13 @@ let record_outline document id (ast : Synterp.vernac_control_entry) classif (out
end
| _ -> outline

let record_outline document {id; ast} outline =
match ast with
| Error _ -> outline
| Parsed ast -> record_outline document id ast.ast ast.classification outline

let compute_outline ({ sentences_by_end } as document) =
LM.fold (fun _ {id; ast} -> record_outline document id ast.ast ast.classification) sentences_by_end []
LM.fold (fun _ s -> record_outline document s) sentences_by_end []


let schedule doc = doc.schedule
Expand All @@ -235,11 +244,14 @@ let outline doc = doc.outline
let parse_errors parsed =
List.map snd (LM.bindings parsed.parsing_errors_by_end)

let add_sentence parsed parsing_start start stop (ast: parsed_ast) synterp_state scheduler_state_before =
let add_sentence parsed parsing_start start stop (ast: sentence_state) synterp_state scheduler_state_before =
let id = Stateid.fresh () in
let ast' = (ast.ast, ast.classification, synterp_state) in
let scheduler_state_after, schedule =
Scheduler.schedule_sentence (id, ast') scheduler_state_before parsed.schedule
let scheduler_state_after, schedule =
match ast with
| Error _ -> scheduler_state_before, parsed.schedule (* If the sentence has a parsing error we do not schedule it *)
| Parsed ast ->
let ast' = (ast.ast, ast.classification, synterp_state) in
Scheduler.schedule_sentence (id, ast') scheduler_state_before parsed.schedule
in
(* FIXME may invalidate scheduler_state_XXX for following sentences -> propagate? *)
let sentence = { parsing_start; start; stop; ast; id; synterp_state; scheduler_state_before; scheduler_state_after } in
Expand Down Expand Up @@ -337,9 +349,12 @@ let find_next_qed parsed loc =
let exception Found of sentence in
let f k sentence =
if loc <= k then
match sentence.ast.classification with
| VtQed _ -> raise (Found sentence)
| _ -> () in
match sentence.ast with
| Error _ -> ()
| Parsed ast ->
match ast.classification with
| VtQed _ -> raise (Found sentence)
| _ -> () in
(* We can't use find_first since f isn't monotone *)
match LM.iter f parsed.sentences_by_end with
| () -> None
Expand Down Expand Up @@ -373,12 +388,19 @@ let string_of_parsed_ast { tokens } =
(* TODO implement printer for vernac_entry *)
"[" ^ String.concat "--" (List.map (Tok.extract_string false) tokens) ^ "]"

let string_of_parsed_ast = function
| Error _ -> "errored sentence"
| Parsed ast -> string_of_parsed_ast ast

let patch_sentence parsed scheduler_state_before id ({ parsing_start; ast; start; stop; synterp_state } : pre_sentence) =
let old_sentence = SM.find id parsed.sentences_by_id in
log @@ Format.sprintf "Patching sentence %s , %s" (Stateid.to_string id) (string_of_parsed_ast old_sentence.ast);
let scheduler_state_after, schedule =
let ast = (ast.ast, ast.classification, synterp_state) in
Scheduler.schedule_sentence (id,ast) scheduler_state_before parsed.schedule
match ast with
| Error _ -> scheduler_state_before, parsed.schedule
| Parsed ast ->
let ast = (ast.ast, ast.classification, synterp_state) in
Scheduler.schedule_sentence (id,ast) scheduler_state_before parsed.schedule
in
let new_sentence = { old_sentence with ast; parsing_start; start; stop; scheduler_state_before; scheduler_state_after } in
let sentences_by_id = SM.add id new_sentence parsed.sentences_by_id in
Expand All @@ -398,7 +420,11 @@ type diff =


let same_tokens (s1 : sentence) (s2 : pre_sentence) =
CList.equal Tok.equal s1.ast.tokens s2.ast.tokens
match s1.ast, s2.ast with
| Error _, Error _ -> false
| Parsed ast1, Parsed ast2 ->
CList.equal Tok.equal ast1.tokens ast2.tokens
| _, _ -> false

(* TODO improve diff strategy (insertions,etc) *)
let rec diff old_sentences new_sentences =
Expand Down Expand Up @@ -505,12 +531,15 @@ let get_entry ast =
[%%endif]


let handle_parse_error start msg qf ({stream; errors;} as parse_state) =
let handle_parse_error start parsing_start msg qf ({stream; errors; parsed} as parse_state) =
log @@ "handling parse error at " ^ string_of_int start;
let stop = Stream.count stream in
let parsing_error = { msg; start; stop; qf} in
let synterp_state = Vernacstate.Synterp.freeze () in
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think you should just pass the synterp state you used to parser the sentence, rather than freezing it here.
I think in practice it will be the same, but there is no need to recompute the snapshot.

let sentence = { parsing_start; ast = Error parsing_error; start; stop; synterp_state } in
let parsed = sentence :: parsed in
let errors = parsing_error :: errors in
let parse_state = {parse_state with errors} in
let parse_state = {parse_state with errors; parsed} in
(* TODO: we could count the \n between start and stop and increase Loc.line_nb *)
create_parsing_event (ParseEvent parse_state)

Expand Down Expand Up @@ -538,7 +567,8 @@ let handle_parse_more ({loc; synterp_state; stream; raw; parsed; parsed_comments
let entry = get_entry ast in
let classification = Vernac_classifier.classify_vernac ast in
let synterp_state = Vernacstate.Synterp.freeze () in
let sentence = { parsing_start = start; ast = { ast = entry; classification; tokens }; start = begin_char; stop; synterp_state } in
let parsed_ast = Parsed { ast = entry; classification; tokens } in
let sentence = { parsing_start = start; ast = parsed_ast; start = begin_char; stop; synterp_state } in
let parsed = sentence :: parsed in
let comments = List.map (fun ((start, stop), content) -> {start; stop; content}) comments in
let parsed_comments = List.append comments parsed_comments in
Expand All @@ -549,24 +579,24 @@ let handle_parse_more ({loc; synterp_state; stream; raw; parsed; parsed_comments
let e, info = Exninfo.capture exn in
let loc = get_loc_from_info_or_exn e info in
let qf = Result.value ~default:[] @@ Quickfix.from_exception e in
handle_parse_error start (loc, Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info)) (Some qf) parse_state
handle_parse_error start begin_char (loc, Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info)) (Some qf) parse_state
end
| exception (E msg as exn) ->
let loc = Loc.get_loc @@ Exninfo.info exn in
let qf = Result.value ~default:[] @@ Quickfix.from_exception exn in
junk_sentence_end stream;
handle_parse_error start (loc,msg) (Some qf) {parse_state with stream}
handle_parse_error start start (loc,msg) (Some qf) {parse_state with stream}
| exception (CLexer.Error.E e as exn) -> (* May be more problematic to handle for the diff *)
let loc = Loc.get_loc @@ Exninfo.info exn in
let qf = Result.value ~default:[] @@ Quickfix.from_exception exn in
junk_sentence_end stream;
handle_parse_error start (loc,CLexer.Error.to_string e) (Some qf) {parse_state with stream}
handle_parse_error start start (loc,CLexer.Error.to_string e) (Some qf) {parse_state with stream}
| exception exn ->
let e, info = Exninfo.capture exn in
let loc = Loc.get_loc @@ info in
let qf = Result.value ~default:[] @@ Quickfix.from_exception exn in
junk_sentence_end stream;
handle_parse_error start (loc, "Unexpected parse error: " ^ Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info)) (Some qf) {parse_state with stream}
handle_parse_error start start (loc, "Unexpected parse error: " ^ Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info)) (Some qf) {parse_state with stream}
end

let rec unchanged_id id = function
Expand Down
6 changes: 5 additions & 1 deletion language-server/dm/document.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -100,6 +100,10 @@ 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. *)

type sentence_state =
| Error of parsing_error
| Parsed of parsed_ast

(* Example: *)
(* " Check 3. " *)
(* ^ ^ ^---- end *)
Expand All @@ -112,7 +116,7 @@ type sentence = {
synterp_state : Vernacstate.Synterp.t; (* synterp state after this sentence's synterp phase *)
scheduler_state_before : Scheduler.state;
scheduler_state_after : Scheduler.state;
ast : parsed_ast;
ast : sentence_state;
id : sentence_id;
}

Expand Down
9 changes: 6 additions & 3 deletions language-server/dm/documentManager.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -770,11 +770,14 @@ let hover st pos =
match hover_of_sentence st loc pattern opt with
| Some _ as x -> x
| None ->
match sentence.ast.classification with
match sentence.ast with
| Error _ -> None
| Parsed ast ->
match ast.classification with
(* next sentence in proof mode, hover at qed *)
| VtProofStep _ | VtStartProof _ ->
| VtProofStep _ | VtStartProof _ ->
hover_of_sentence st loc pattern (Document.find_next_qed st.document loc)
| _ -> None
| _ -> None

[%%if coq = "8.18" || coq = "8.19" || coq = "8.20"]
let lconstr = Pcoq.Constr.lconstr
Expand Down
Loading