Merge pull request #380 from ejgallego/cache_create

[fleche] Cache document creation

controller/cache.ml

@@ -22,7 +22,7 @@ let memo_cache_file = ".coq-lsp.cache"
 
 let memo_save_to_disk () =
   try
-    Fleche.Memo.save_to_disk ~file:memo_cache_file;
+    (* Fleche.Memo.save_to_disk ~file:memo_cache_file; *)
     LIO.trace "memo" "cache saved to disk"
   with exn ->
     LIO.trace "memo" (Printexc.to_string exn);
@@ -36,7 +36,7 @@ let memo_read_from_disk () =
   try
     if Sys.file_exists memo_cache_file then (
       LIO.trace "memo" "trying to load cache file";
-      Fleche.Memo.load_from_disk ~file:memo_cache_file;
+      (* Fleche.Memo.load_from_disk ~file:memo_cache_file; *)
       LIO.trace "memo" "cache file loaded")
     else LIO.trace "memo" "cache file not present"
   with exn ->

coq/interp.ml

@@ -15,18 +15,11 @@
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
 
-module Info = struct
-  type 'a t = { res : 'a }
-end
-
-type 'a interp_result = ('a Info.t, Loc.t) Protect.E.t
+type 'a interp_result = ('a, Loc.t) Protect.E.t
 
 let coq_interp ~st cmd =
   let st = State.to_coq st in
   let cmd = Ast.to_coq cmd in
   Vernacinterp.interp ~st cmd |> State.of_coq
 
-let interp ~st cmd =
-  Protect.eval cmd ~f:(fun cmd ->
-      let res = coq_interp ~st cmd in
-      { Info.res })
+let interp ~st cmd = Protect.eval cmd ~f:(coq_interp ~st)

coq/interp.mli

@@ -15,10 +15,6 @@
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
 
-module Info : sig
-  type 'a t = { res : 'a }
-end
-
-type 'a interp_result = ('a Info.t, Loc.t) Protect.E.t
+type 'a interp_result = ('a, Loc.t) Protect.E.t
 
 val interp : st:State.t -> Ast.t -> State.t interp_result

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

@@ -22,7 +22,7 @@ module Util = struct
 
   let print_stats () =
     (if !Config.v.mem_stats then
-     let size = Memo.mem_stats () in
+     let size = Memo.Interp.stats () in
      Io.Log.trace "stats" (string_of_int size));
 
     Io.Log.trace "cache" (Stats.to_string ());
@@ -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
@@ -422,7 +423,7 @@ let recovery_for_failed_qed ~default nodes =
   | None -> Coq.Protect.E.ok (default, None)
   | Some ({ range; state; _ }, prev) -> (
     if !Config.v.admit_on_bad_qed then
-      Memo.interp_admitted ~st:state
+      Memo.Admit.eval state
       |> Coq.Protect.E.map ~f:(fun state -> (state, Some range))
     else
       match prev with
@@ -433,7 +434,7 @@ let log_qed_recovery v =
   Coq.Protect.E.map ~f:(fun (st, range) ->
       let loc_msg = Option.cata Lang.Range.to_string "no loc" range in
       Io.Log.trace "recovery"
-        ("success" ^ loc_msg ^ " " ^ Memo.input_info (v, st));
+        ("success" ^ loc_msg ^ " " ^ Memo.Interp.input_info (st, v));
       st)
 
 (* Simple heuristic for Qed. *)
@@ -447,16 +448,14 @@ let state_recovery_heuristic doc st v =
   | Vernacexpr.VernacBullet _ | Vernacexpr.VernacEndSubproof ->
     Io.Log.trace "recovery" "bullet";
     Coq.State.admit_goal ~st
-    |> Coq.Protect.E.bind ~f:(fun st ->
-           Coq.Interp.interp ~st v.v
-           |> Coq.Protect.E.map ~f:(fun { Coq.Interp.Info.res } -> res))
+    |> Coq.Protect.E.bind ~f:(fun st -> Coq.Interp.interp ~st v.v)
   | _ -> Coq.Protect.E.ok st
 
 let interp_and_info ~parsing_time ~st ast =
   let { Gc.major_words = mw_prev; _ } = Gc.quick_stat () in
   (* memo memory stats are disabled: slow and misleading *)
   let { Memo.Stats.res; cache_hit; memory = _; time } =
-    Memo.interp_command ~st ast
+    Memo.Interp.eval (st, ast)
   in
   let { Gc.major_words = mw_after; _ } = Gc.quick_stat () in
   let stats = Stats.dump () in
@@ -559,7 +558,7 @@ let recovery_interp ~doc ~st ~ast =
 let node_of_coq_result ~doc ~range ~ast ~st ~parsing_diags ~parsing_feedback
     ~feedback ~info last_tok res =
   match res with
-  | Ok { Coq.Interp.Info.res = state } ->
+  | Ok state ->
     let node =
       parsed_node ~range ~ast ~state ~parsing_diags ~parsing_feedback ~diags:[]
         ~feedback ~info

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