cleaned up: most of doc.ml

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 =

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,17 +470,19 @@ 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
   match doc.completed with
   (* 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;

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

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,23 +218,27 @@ 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
         if Doc.Completion.is_completed doc.completed then Register.fire ~io ~doc;
         (* 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"
         ("file " ^ Lang.LUri.File.to_string_uri uri ^ " not available");
       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