[fleche] Cache document creation

Some clients, such as Visual Studio Code, may open / close buffers
aggressively when working, this creates some extra load as we don't
cache document creation.

This PR does cache it. In general this has a very low footprint on
memory by itself, as the root state is shared across all buffers, but
of course, the documents themselves could be a big load, but that's
already the case so we don't make things worse.

Fixes #363

[Test suite passes ;)]

coq/workspace.ml

@@ -27,6 +27,9 @@ type t =
   ; debug : bool
   }
 
+let hash = Hashtbl.hash
+let compare = Stdlib.compare
+
 (* Lib setup, XXX unify with sysinit *)
 let coq_root = Names.DirPath.make [ Libnames.coq_root ]
 let default_root = Libnames.default_root_prefix

coq/workspace.mli

@@ -27,6 +27,12 @@ type t = private
   ; debug : bool  (** Enable backtraces *)
   }
 
+(** compare *)
+val compare : t -> t -> int
+
+(** hash *)
+val hash : t -> int
+
 (** user message, debug extra data *)
 val describe : t -> string * string
 

fleche/doc.ml

@@ -207,9 +207,7 @@ type t =
   ; completed : Completion.t
   }
 
-let mk_doc root_state workspace uri =
-  Coq.Init.doc_init ~root_state ~workspace ~uri
-
+(* Flatten the list of document asts *)
 let asts doc = List.filter_map Node.ast doc.nodes
 
 (* TOC handling *)
@@ -248,6 +246,9 @@ let process_init_feedback ~stats range state messages =
     [ { Node.range; ast = None; state; diags; messages; info } ]
   else []
 
+(* Memoized call to [Coq.Init.doc_init] *)
+let mk_doc root_state workspace uri = Memo.Init.eval (root_state, workspace, uri)
+
 let create ~state ~workspace ~uri ~version ~contents =
   let () = Stats.reset () in
   let { Coq.Protect.E.r; feedback } = mk_doc state workspace uri in

fleche/doc.mli

@@ -73,7 +73,7 @@ type t = private
 (** Return the list of all asts in the doc *)
 val asts : t -> Node.Ast.t list
 
-(** Note, [create] calls Coq but it is not cached in the Memo.t table *)
+(** Create a new Coq document, this is cached! *)
 val create :
      state:Coq.State.t
   -> workspace:Coq.Workspace.t

fleche/memo.ml

@@ -135,15 +135,47 @@ end
 module Admit = struct
   type t = Coq.State.t
 
-  module AC = Hashtbl.Make (Coq.State)
+  module C = Hashtbl.Make (Coq.State)
 
-  let admit_cache = AC.create 1000
+  let cache = C.create 1000
 
-  let eval st =
-    match AC.find_opt admit_cache st with
+  let eval v =
+    match C.find_opt cache v with
     | None ->
-      let admitted_st = Coq.State.admit ~st in
-      AC.add admit_cache st admitted_st;
+      let admitted_st = Coq.State.admit ~st:v in
+      C.add cache v admitted_st;
       admitted_st
     | Some admitted_st -> admitted_st
 end
+
+module Init = struct
+  module S = struct
+    type t = Coq.State.t * Coq.Workspace.t * Lang.LUri.File.t
+
+    let equal (s1, w1, u1) (s2, w2, u2) : bool =
+      if Lang.LUri.File.compare u1 u2 = 0 then
+        if Coq.Workspace.compare w1 w2 = 0 then
+          if Coq.State.compare s1 s2 = 0 then true else false
+        else false
+      else false
+
+    let hash (st, w, uri) =
+      Hashtbl.hash
+        (Coq.State.hash st, Coq.Workspace.hash w, Lang.LUri.File.hash uri)
+  end
+
+  type t = S.t
+
+  module C = Hashtbl.Make (S)
+
+  let cache = C.create 1000
+
+  let eval v =
+    match C.find_opt cache v with
+    | None ->
+      let root_state, workspace, uri = v in
+      let admitted_st = Coq.Init.doc_init ~root_state ~workspace ~uri in
+      C.add cache v admitted_st;
+      admitted_st
+    | Some res -> res
+end

fleche/memo.mli

@@ -7,6 +7,12 @@ module Stats : sig
     }
 end
 
+module Init : sig
+  type t = Coq.State.t * Coq.Workspace.t * Lang.LUri.File.t
+
+  val eval : t -> (Coq.State.t, Loc.t) Coq.Protect.E.t
+end
+
 module Interp : sig
   type t = Coq.State.t * Coq.Ast.t
 

lang/lUri.ml

@@ -21,4 +21,6 @@ module File = struct
   let to_string_uri { uri; _ } = Uri.to_string uri
   let to_string_file { file; _ } = file
   let extension { file; _ } = Filename.extension file
+  let hash = Hashtbl.hash
+  let compare = Stdlib.compare
 end

lang/lUri.mli

@@ -27,4 +27,10 @@ module File : sig
 
   (** Filename version, fit for OS functions *)
   val to_string_file : t -> string
+
+  (** compare *)
+  val compare : t -> t -> int
+
+  (** hash *)
+  val hash : t -> int
 end