Merge pull request #709 from ejgallego/support_meta_commands

[fleche] Support Coq Meta Commands Reset and Back

CHANGES.md

@@ -123,6 +123,9 @@
    engine. (@ejgallego, @gbdrt, #703, thanks to Alex Sanchez-Stern)
  - Always dispose UI elements. This should improve some strange
    behaviors on extension restart (@ejgallego, #708)
+ - Support Coq meta-commands (Reset, Reset Initial, Back) They are
+   actually pretty useful to hint the incremental engine to ignore
+   changes in some part of the document (@ejgallego, #709)
 
 # coq-lsp 0.1.8.1: Spring fix
 -----------------------------

coq/ast.ml

@@ -62,6 +62,51 @@ module Require = struct
     | _ -> None
 end
 
+module Meta = struct
+  type ast = t
+
+  open Ppx_hash_lib.Std.Hash.Builtin
+  open Ppx_compare_lib.Builtin
+  module Loc = Serlib.Ser_loc
+  module Names = Serlib.Ser_names
+  module Attributes = Serlib.Ser_attributes
+  module Vernacexpr = Serlib.Ser_vernacexpr
+
+  module Command = struct
+    type t =
+      | Back of int
+      | ResetName of Names.lident
+      | ResetInitial
+    [@@deriving hash, compare]
+  end
+
+  type t =
+    { command : Command.t
+    ; loc : Loc.t option
+    ; attrs : Attributes.vernac_flag list
+    ; control : Vernacexpr.control_flag list
+    }
+  [@@deriving hash, compare]
+
+  (* EJGA: Coq classification puts these commands as pure? Seems like yet
+     another bug... *)
+  let extract : ast -> t option =
+    CAst.with_loc_val (fun ?loc -> function
+      | { Vernacexpr.expr = Vernacexpr.(VernacSynPure (VernacResetName id))
+        ; control
+        ; attrs
+        } ->
+        let command = Command.ResetName id in
+        Some { command; loc; attrs; control }
+      | { expr = VernacSynPure VernacResetInitial; control; attrs } ->
+        let command = Command.ResetInitial in
+        Some { command; loc; attrs; control }
+      | { expr = VernacSynPure (VernacBack num); control; attrs } ->
+        let command = Command.Back num in
+        Some { command; loc; attrs; control }
+      | _ -> None)
+end
+
 module Kinds = struct
   (* LSP kinds *)
   let _file = 1

coq/ast.mli

@@ -32,6 +32,28 @@ module Require : sig
   val extract : ast -> t option
 end
 
+module Meta : sig
+  type ast = t
+
+  module Command : sig
+    type t =
+      | Back of int
+      | ResetName of Names.lident
+      | ResetInitial
+  end
+
+  type t =
+    { command : Command.t
+    ; loc : Loc.t option
+    ; attrs : Attributes.vernac_flag list
+    ; control : Vernacexpr.control_flag list
+    }
+  [@@deriving hash, compare]
+
+  (** Determine if we are under a meta-command *)
+  val extract : ast -> t option
+end
+
 (** [make_info ~st ast] Compute info about a possible definition in [ast], we
     need [~st] to compute the type. *)
 val make_info :

coq/protect.ml

@@ -82,6 +82,7 @@ module E = struct
       { r; feedback = feedback @ fb2 }
 
   let ok v = { r = Completed (Ok v); feedback = [] }
+  let error err = { r = R.error err; feedback = [] }
 
   module O = struct
     let ( let+ ) x f = map ~f x

coq/protect.mli

@@ -39,6 +39,7 @@ module E : sig
   val map_loc : f:('l -> 'm) -> ('a, 'l) t -> ('a, 'm) t
   val bind : f:('a -> ('b, 'l) t) -> ('a, 'l) t -> ('b, 'l) t
   val ok : 'a -> ('a, 'l) t
+  val error : Pp.t -> ('a, 'l) t
 
   module O : sig
     val ( let+ ) : ('a, 'l) t -> ('a -> 'b) -> ('b, 'l) t

etc/doc/USER_MANUAL.md

@@ -47,3 +47,33 @@ from `memprof-limits`. The situation is better in Coq 8.20, but users
 on Coq <= 8.19 do need to install a version of Coq with the backported
 fixes. See the information about Coq upstream bugs in the README for
 more information about available branches.
+
+## Advanced incremental tricks
+
+You can use the `Reset $id` and `Back $steps` commands to isolate
+parts of the document from each others in terms of rechecking.
+
+For example, the command `Reset $id` will make the parts of the
+document after it use the state before the node `id` was found. Thus,
+any change between `$id` and the `Reset $id` command will not trigger
+a recheck of the rest of the document.
+
+```coq
+(* Coq code 1 *)
+
+Lemma foo : T.
+Proof. ... Qed.
+
+(* Coq code 2 *)
+
+Reset foo.
+
+(* Coq code 3 *)
+```
+
+In the above code, any change in the "`Coq code 2`" section will not
+trigger a recheck of the "`Coq code 3`" Section, by virtue of the
+incremental engine.
+
+Using `Reset Initial`, you can effectively partition the document on
+`N` parts! This is pretty cool for some use cases!

examples/MetaCommands.v

@@ -0,0 +1,38 @@
+Lemma foo : 3 = 3.
+Proof. now reflexivity. Qed.
+
+About foo.
+
+Reset Initial.
+
+About foo.
+
+Lemma foo : 2 = 2.
+Proof. now reflexivity. Qed.
+
+Lemma bar : 4 = 4.
+Proof. now reflexivity. Qed.
+
+About bar.
+About foo.
+
+Reset foo.
+
+About foo.
+About bar.
+
+Lemma muu : 4 = 4.
+Proof.
+now reflexivity.
+Back 2.
+now reflexivity.
+Qed.
+
+Reset Initial.
+
+About muu.
+About foo.
+About bar.
+
+
+

fleche/doc.ml

@@ -672,13 +672,64 @@ end = struct
     | Completed (Error _) -> st
 end
 
-let interp_and_info ~st ~files ast =
+let interp_and_info ~token ~st ~files ast =
   match Coq.Ast.Require.extract ast with
-  | None -> Memo.Interp.evalS (st, ast)
-  | Some ast -> Memo.Require.evalS (st, files, ast)
+  | None -> Memo.Interp.evalS ~token (st, ast)
+  | Some ast -> Memo.Require.evalS ~token (st, files, ast)
 
-let interp_and_info ~token ~parsing_time ~st ~files ast =
-  let res, stats = interp_and_info ~token ~st ~files ast in
+(* Support for meta-commands, a bit messy, but cool in itself *)
+let search_node ~command ~doc =
+  let nstats (node : Node.t option) =
+    Option.cata
+      (fun (node : Node.t) -> Option.default Memo.Stats.zero node.info.stats)
+      Memo.Stats.zero node
+  in
+  match command with
+  | Coq.Ast.Meta.Command.Back num -> (
+    match Base.List.nth doc.nodes num with
+    | None ->
+      let ll = List.length doc.nodes in
+      let message =
+        Pp.(
+          str "not enough nodes: [" ++ int num ++ str " > " ++ int ll
+          ++ str "] available document nodes")
+      in
+      (Coq.Protect.E.error message, nstats None)
+    | Some node -> (Coq.Protect.E.ok node.state, nstats (Some node)))
+  | ResetName id -> (
+    let toc = doc.toc in
+    let id = Names.Id.to_string id.v in
+    match CString.Map.find_opt id toc with
+    | None ->
+      ( Coq.Protect.E.error Pp.(str "identifier " ++ str id ++ str " not found")
+      , Memo.Stats.zero )
+    | Some range ->
+      (* this is painful *)
+      let rec aux st node (nodes : Node.t list) =
+        match nodes with
+        | [] -> (st, nstats node)
+        | node :: nodes ->
+          if node.range.end_.offset < range.start.offset then
+            (node.state, nstats (Some node))
+          else aux node.state (Some node) nodes
+      in
+      (* We could error here too *)
+      let res, stats = aux doc.root None doc.nodes in
+      (Coq.Protect.E.ok res, stats))
+  | ResetInitial -> (Coq.Protect.E.ok doc.root, nstats None)
+
+let interp_and_info ~token ~st ~files ~doc ast =
+  match Coq.Ast.Meta.extract ast with
+  | None -> interp_and_info ~token ~st ~files ast
+  | Some { command; loc = _; attrs = _; control = _ } ->
+    (* That's an interesting point, for now we don't measure time Flèche is
+       spending on error recovery and meta stuff, we should record that time
+       actually at some point too. In this case, maybe we could recover the
+       cache hit from the original node? *)
+    search_node ~command ~doc
+
+let interp_and_info ~token ~parsing_time ~st ~files ~doc ast =
+  let res, stats = interp_and_info ~token ~st ~files ~doc ast in
   let global_stats = Stats.Global.dump () in
   let info = Node.Info.make ~parsing_time ~stats ~global_stats () in
   (res, info)
@@ -816,7 +867,7 @@ let document_action ~token ~st ~parsing_diags ~parsing_feedback ~parsing_time
   | Process ast -> (
     let lines, files = (doc.contents.lines, doc.env.files) in
     let process_res, info =
-      interp_and_info ~token ~parsing_time ~st ~files ast
+      interp_and_info ~token ~parsing_time ~st ~files ~doc 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

fleche/memo.ml

@@ -13,6 +13,12 @@ module Stats = struct
        precise option *)
     (* let memory = Obj.magic res |> Obj.reachable_words in *)
     { stats; time_hash; cache_hit }
+
+  let zero =
+    { stats = { Stats.time = 0.0; memory = 0.0 }
+    ; time_hash = 0.0
+    ; cache_hit = false
+    }
 end
 
 module GlobalCacheStats = struct

fleche/memo.mli

@@ -5,6 +5,8 @@ module Stats : sig
           (** Time in hashing consumed in the original execution *)
     ; cache_hit : bool  (** Whether we had a cache hit *)
     }
+
+  val zero : t
 end
 
 (** Flèche memo / cache tables, with some advanced features *)