lsp: warn on refinement-induced splay failures#8
Conversation
brandonzstride
left a comment
brandonzstride
left a comment
There was a problem hiding this comment.
I have some comments about code and style, but the big concern is about weaving together the splay-no-refinements check with the normal check. I believe there is a particularly subtle case where they cannot run one after the other.
leon-xu-04
force-pushed
the
refinement-stripping
branch
from
1e3e0b2 to
467d467
Compare
leon-xu-04
force-pushed
the
refinement-stripping
branch
from
467d467 to
9a4128b
Compare
brandonzstride
left a comment
brandonzstride
left a comment
There was a problem hiding this comment.
I've left some specific comments and questions directly on the code, but I have some general remarks here.
My overall feeling is that this seems more complicated than it needs to be. I say this because there are a lot of complex and specific interactions that I had to follow when reading it. Maybe it is just fundamentally complicated, and we simply must accept that, but my first impression is this solution feels more specific to the problem than is necessary. I would attempt to find an abstraction that makes any work item cancellable and also able to spawn any number of new (cancellable) tasks as a result (possibly not unlike the Fork example in the OCaml manual on effects). The two behaviors upon finishing we need are "spawn more tasks" and "cancel other tasks with the same position". I have a feeling that abstracting it to this level might be helpful.
You currently wait to print anything about the refinements until the non-splay times out. This seems to contribute to the complexity and specificity of the solution. Is it possible that you print the refinement warnings eagerly and erase them if the non-splay later errors? I do not know if that is difficult or not. But if you could do that, then it would more nicely fit into the abstraction I describe above.
brandonzstride
left a comment
brandonzstride
left a comment
There was a problem hiding this comment.
This is looking really good. I now recommend a big change to structure for the parser. We might have files like this (all in src/):
parsing/parser.mlyparsing/lexer.mllparsing/tokens.mlyparsing/tools.ml(relevant parsing tools fromLang.Ast.Tools)parsing/param.ml(where the current module typePARAMis justSonce it's insideParsing.Param, henceParsing.Param.S)parsing/parse.mlfor the main behavior, which is inlang/parser.mlright now.
I think the caprice qualifier is implicit and does not need to be spelled out in every module name. And these names are up for debate. I just think it's time to move the parsing logic out of the Lang module now that it has grown quite a bit.
| let module Ignore = Parser_param.Make_ignore_refine () in | ||
| let module Stripped_parser = Caprice_parser.Make (Ignore) in | ||
| let buf = Lexing.from_string input in | ||
| let stmts = handle_parse_error buf @@ fun () -> Stripped_parser.prog_with_pos Caprice_lexer.token buf in |
There was a problem hiding this comment.
This line is running very long.
| let stmts = handle_parse_error buf @@ fun () -> Stripped_parser.prog_with_pos Caprice_lexer.token buf in | |
| let stmts = handle_parse_error buf @@ fun () -> | |
| Stripped_parser.prog_with_pos Caprice_lexer.token buf | |
| in |
| | Done -> dequeue () | ||
| | Cont k -> enqueue span k; dequeue () | ||
| | Spawn children -> | ||
| List.iter (fun c -> Queue.push c run_q) children; |
There was a problem hiding this comment.
Can we modify enqueue to support this behavior? Or add another function very similar to enqueue to do this? It feels out of place amidst the other code that only calls enqueue and dequeue, for the most part.
| let round_robin (fs : work_item list) : unit = | ||
| let run_q = Queue.of_seq (List.to_seq fs) in | ||
| let cancelled : (Lang.Ast.pos_span, unit) Hashtbl.t = Hashtbl.create 16 in | ||
| let is_cancelled span = Hashtbl.mem cancelled span in |
There was a problem hiding this comment.
I also suggest a cancel function that does the Hashtbl.replace cancelled s () we see below.
| let enqueue span k = | ||
| let task () = Effect.Deep.continue k () in | ||
| Queue.push { span ; task } run_q | ||
| let handle_fallback ~options ~refinement_positions (span : Lang.Ast.pos_span) pgm stripped_pgm : Scheduler.r = |
There was a problem hiding this comment.
Very long line. Any newline/indentation will help.
| let handle_fallback ~options ~refinement_positions (span : Lang.Ast.pos_span) pgm stripped_pgm : Scheduler.r = | |
| let handle_fallback ~options ~refinement_positions (span : Lang.Ast.pos_span) | |
| pgm stripped_pgm : Scheduler.r = |
2 participants
Parses the program twice — once normally, once with refinements stripped to base types. If splay fails with refinements but passes without, and a full check finds no real error, each refinement is yellow-underlined with "Splay-checking failed because of refinement types".