From 4cbddfd27fc3f150290a748f10ec0acecc951903 Mon Sep 17 00:00:00 2001 From: BHAKTISHAH Date: Sat, 13 Jan 2024 00:20:34 +0000 Subject: [PATCH] cleaned up: most of doc.ml --- controller/rq_document.ml | 2 +- fleche/doc.ml | 36 ++++++++++++++++++++++++++++++++---- fleche/doc.mli | 3 +++ fleche/theory.ml | 38 ++++++++++++++++++++++++-------------- 4 files changed, 60 insertions(+), 19 deletions(-) diff --git a/controller/rq_document.ml b/controller/rq_document.ml index d202f275c..3b04c3167 100644 --- a/controller/rq_document.ml +++ b/controller/rq_document.ml @@ -12,7 +12,7 @@ let to_span { Fleche.Doc.Node.range; ast; _ } = let to_completed = function | Fleche.Doc.Completion.Yes range -> { Lsp.JFleche.CompletionStatus.status = `Yes; range } - | Stopped range -> { status = `Stopped; range } + | Stopped range | Waiting (range, _) -> { status = `Stopped; range } | Failed range | FailedPermanent range -> { status = `Failed; range } let request ~doc = diff --git a/fleche/doc.ml b/fleche/doc.ml index b4dc15a1d..badc11263 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -206,22 +206,32 @@ module Completion = struct type t = | Yes of Lang.Range.t (** Location of the last token in the document *) | Stopped of Lang.Range.t (** Location of the last valid token *) + | Waiting of Lang.Range.t * Lang.LUri.File.t | Failed of Lang.Range.t (** Critical failure, like an anomaly *) | FailedPermanent of Lang.Range.t (** Temporal Coq hack, avoids any computation *) let range = function - | Yes range | Stopped range | Failed range | FailedPermanent range -> range + | Yes range + | Stopped range + | Failed range + | FailedPermanent range + | Waiting (range, _) -> range let to_string = function | Yes _ -> "fully checked" | Stopped _ -> "stopped" | Failed _ -> "failed" | FailedPermanent _ -> "refused to create due to Coq parsing bug" + | Waiting (_, _doc) -> "waiting for doc" let is_completed = function | Yes _ | Failed _ | FailedPermanent _ -> true | _ -> false + + let is_waiting_for = function + | Waiting (_, doc) -> Some doc + | _ -> None end (** Enviroment external to the document, this includes for now the [init] Coq @@ -231,9 +241,10 @@ module Env = struct type t = { init : Coq.State.t ; workspace : Coq.Workspace.t + ; beacon : int } - let make ~init ~workspace = { init; workspace } + let make ~init ~workspace = { init; workspace; beacon = 0 } end (** A Flèche document is basically a [node list], which is a crude form of a @@ -459,6 +470,7 @@ let bump_version ~init_range ~version ~contents doc = ; env } +(* TODO what is this bumping *) let bump_version ~version ~(contents : Contents.t) doc = let init_loc = init_loc ~uri:doc.uri in let init_range = Coq.Utils.to_range ~lines:contents.lines init_loc in @@ -466,10 +478,11 @@ let bump_version ~version ~(contents : Contents.t) doc = (* We can do better, but we need to handle the case where the anomaly is when restoring / executing the first sentence *) | FailedPermanent _ -> doc - | Failed _ -> + | Failed _ | Waiting _ -> (* re-create the document on failed, as the env may have changed *) recreate ~doc ~version ~contents | Stopped _ | Yes _ -> bump_version ~init_range ~version ~contents doc +(* | Waiting _ -> restart_doc () *) let bump_version ~version ~raw doc = let uri = doc.uri in @@ -691,6 +704,8 @@ type document_action = } | Interrupted of Lang.Range.t +(* ..... Require a. *) + let unparseable_node ~range ~parsing_diags ~parsing_feedback ~state ~parsing_time = let fb_diags, messages = Diags.of_messages ~drange:range parsing_feedback in @@ -772,6 +787,14 @@ let document_action ~st ~parsing_diags ~parsing_feedback ~parsing_time ~doc (* We can interpret the command now *) | Process ast -> ( let lines = doc.contents.lines in + (* f1 : nat , f2 : nat , f3 : nat |- f1 : nat + + f1 : nat , f2 : bool , f3 : nat |- f1 : nat *) + (* interp_require : State.t -> Files.t -> State.t interp : State.t -> Ast.t + -> State.t *) + (* match ast with | Require file -> if is_file_ready file then + interp_require (env, st) else Stop Waiting file | other -> + interp_and_info ~parsing ~st ast in *) let process_res, info = interp_and_info ~parsing_time ~st ast in let f = Coq.Utils.to_range ~lines in let { Coq.Protect.E.r; feedback } = Coq.Protect.E.map_loc ~f process_res in @@ -960,7 +983,12 @@ let check ~io ~target ~doc () = | FailedPermanent _ | Failed _ -> Io.Log.trace "check" "can't resume, failed=yes, nothing to do"; doc - | Stopped last_tok -> + (* Invariant: we only check a document if the dependencies are ready. *) + (* | Waiting (last_tok, dep) when not (io.file_ready dep) -> Io.Log.trace + "check" "the file was resumed, however the dependencies are not ready" ; + { doc with completed = FailedPermanent last_tok } *) + (* Set the document to FailedPermanet *) + | Waiting (last_tok, _) | Stopped last_tok -> DDebug.resume last_tok doc.version; let doc = resume_check ~io ~last_tok ~doc ~target in log_doc_completion doc.completed; diff --git a/fleche/doc.mli b/fleche/doc.mli index d39e7ed95..a77e3eb07 100644 --- a/fleche/doc.mli +++ b/fleche/doc.mli @@ -51,11 +51,13 @@ module Completion : sig type t = private | Yes of Lang.Range.t (** Location of the last token in the document *) | Stopped of Lang.Range.t (** Location of the last valid token *) + | Waiting of Lang.Range.t * Lang.LUri.File.t | Failed of Lang.Range.t (** Critical failure, like an anomaly *) | FailedPermanent of Lang.Range.t (** Temporal Coq hack, avoids any computation *) val is_completed : t -> bool + val is_waiting_for : t -> Lang.LUri.File.t option end (** Enviroment external to the document, this includes for now the [init] Coq @@ -65,6 +67,7 @@ module Env : sig type t = private { init : Coq.State.t ; workspace : Coq.Workspace.t + ; beacon : int } val make : init:Coq.State.t -> workspace:Coq.Workspace.t -> t diff --git a/fleche/theory.ml b/fleche/theory.ml index 44338745b..6b6e99fdb 100644 --- a/fleche/theory.ml +++ b/fleche/theory.ml @@ -25,6 +25,7 @@ module Handle = struct "wake up when a location is reached", or always to continue the streaming *) ; pt_requests : (int * (int * int)) list (* id, point *) + ; rev_deps : Lang.LUri.t list } let pt_eq (id1, (l1, c1)) (id2, (l2, c2)) = id1 = id2 && l1 = l2 && c1 = c2 @@ -45,7 +46,7 @@ module Handle = struct ^ Lang.LUri.File.to_string_uri uri ^ " not properly closed by client")); Hashtbl.add doc_table uri - { doc; cp_requests = Int.Set.empty; pt_requests = [] } + { doc; cp_requests = Int.Set.empty; pt_requests = []; rev_deps = [] } let close ~uri = Hashtbl.remove doc_table uri let find_opt ~uri = Hashtbl.find_opt doc_table uri @@ -59,24 +60,26 @@ module Handle = struct let clear_requests ~uri = match Hashtbl.find_opt doc_table uri with | None -> Int.Set.empty - | Some { cp_requests; pt_requests; doc } -> + | Some { cp_requests; pt_requests; doc; rev_deps } -> let invalid_reqs = Int.Set.union cp_requests (pt_ids pt_requests) in Hashtbl.replace doc_table uri - { doc; cp_requests = Int.Set.empty; pt_requests = [] }; + { doc; cp_requests = Int.Set.empty; pt_requests = []; rev_deps }; invalid_reqs (* Clear requests and update doc *) let update_doc_version ~(doc : Doc.t) = let invalid_reqs = clear_requests ~uri:doc.uri in + let { rev_deps; _ } = Hashtbl.find doc_table doc.uri in Hashtbl.replace doc_table doc.uri - { doc; cp_requests = Int.Set.empty; pt_requests = [] }; + (* TODO invalidate rev_deps *) + { doc; cp_requests = Int.Set.empty; pt_requests = []; rev_deps }; invalid_reqs let map_cp_requests ~uri ~f = match Hashtbl.find_opt doc_table uri with - | Some { doc; cp_requests; pt_requests } -> + | Some { doc; cp_requests; pt_requests; rev_deps } -> let cp_requests = f cp_requests in - Hashtbl.replace doc_table uri { doc; cp_requests; pt_requests } + Hashtbl.replace doc_table uri { doc; cp_requests; pt_requests; rev_deps } | None -> () let attach_cp_request ~uri ~id = @@ -89,9 +92,9 @@ module Handle = struct let map_pt_requests ~uri ~f = match Hashtbl.find_opt doc_table uri with - | Some { doc; cp_requests; pt_requests } -> + | Some { doc; cp_requests; pt_requests; rev_deps } -> let pt_requests = f pt_requests in - Hashtbl.replace doc_table uri { doc; cp_requests; pt_requests } + Hashtbl.replace doc_table uri { doc; cp_requests; pt_requests; rev_deps } | None -> () (* This needs to be insertion sort! *) @@ -116,7 +119,7 @@ module Handle = struct let pt_requests = [] in let cp_requests = Int.Set.empty in ({ handle with cp_requests; pt_requests }, wake_up) - | Stopped range -> + | Stopped range | Waiting (range, _) -> let fullfilled, delayed = List.partition (fun (_id, point) -> Doc.Target.reached ~range point) @@ -199,6 +202,9 @@ end = struct Option.map target_of_pt_handle (List.nth_opt pt_requests 0) (* Notification handling; reply is optional / asynchronous *) + + let schedule ~uri = pending := pend_push uri !pending + let check ~io ~uri = Io.Log.trace "process_queue" "resuming document checking"; match Handle.find_opt ~uri with @@ -212,7 +218,7 @@ end = struct && Int.Set.is_empty handle.cp_requests -> pending := pend_pop !pending; None - | (None | Some _) as tgt -> + | (None | Some _) as tgt -> ( let target = Option.default Doc.Target.End tgt in let doc = Doc.check ~io ~target ~doc:handle.doc () in let requests = Handle.update_doc_info ~handle ~doc in @@ -220,7 +226,12 @@ end = struct (* Remove from the queue *) if Doc.Completion.is_completed doc.completed then pending := pend_pop !pending; - Some (requests, doc)) + match Doc.Completion.is_waiting_for doc.completed with + | None -> Some (requests, doc) + | Some uri -> + schedule ~uri; + (* todo add to handler: rev_dep of uri *) + Some (requests, doc))) | None -> pending := pend_pop !pending; Io.Log.trace "Check.check" @@ -228,7 +239,6 @@ end = struct None let maybe_check ~io = pend_try (fun uri -> check ~io ~uri) !pending - let schedule ~uri = pending := pend_push uri !pending let deschedule ~uri = pending := CList.remove Lang.LUri.File.equal uri !pending @@ -344,8 +354,8 @@ module Request = struct let in_range = match doc.completed with | Yes _ -> true - | Failed range | FailedPermanent range | Stopped range -> - Doc.Target.reached ~range (line, col) + | Failed range | FailedPermanent range | Stopped range | Waiting (range, _) + -> Doc.Target.reached ~range (line, col) in let in_range = match version with