[petanque] Add petanque/toc protocol call.

This is already available in LSP, but we expose it here for the
lighter client.

CHANGES.md

@@ -68,6 +68,8 @@
    (@ejgallego @gbdrt, #779)
  - [petanque] New methods to hash proof states; use proof state hash
    by default in petanque agent (@ejgallego, @gbdrt, #808)
+ - [petanque] New shell method `petanque/toc` that returns a document
+   outline in LSP-style (@ejgallego, #794)
 
 # coq-lsp 0.1.10: Hasta el 40 de Mayo _en effect_...
 ----------------------------------------------------

lang/ast.mli

@@ -4,7 +4,7 @@ end
 
 (** Information about the Ast, to move to lang *)
 module Info : sig
-  type t = private
+  type t =
     { range : Range.t
     ; name : Name.t With_range.t
     ; kind : int

petanque/json/jAgent.ml

@@ -54,6 +54,27 @@ module Lang = struct
   module Range = struct
     type t = Lsp.JLang.Range.t [@@deriving yojson]
   end
+
+  module With_range = struct
+    type 'a t = [%import: ('a Lang.With_range.t[@with Lang.Range.t := Range.t])]
+    [@@deriving yojson]
+  end
+
+  module Ast = struct
+    module Name = struct
+      type t = [%import: Lang.Ast.Name.t] [@@deriving yojson]
+    end
+
+    module Info = struct
+      type t =
+        [%import:
+          (Lang.Ast.Info.t
+          [@with
+            Lang.Range.t := Range.t;
+            Lang.With_range.t := With_range.t])]
+      [@@deriving yojson]
+    end
+  end
 end
 
 module Premise = struct

petanque/json/protocol.ml

@@ -67,15 +67,7 @@ module Start = struct
   end
 
   module Handler = struct
-    module Params = struct
-      type t =
-        { uri : Lsp.JLang.LUri.File.t
-        ; opts : Run_opts.t option [@default None]
-        ; pre_commands : string option [@default None]
-        ; thm : string
-        }
-      [@@deriving yojson]
-    end
+    module Params = Params
 
     module Response = struct
       type t = State.t Run_result.t [@@deriving yojson]

petanque/json_shell/client.ml

@@ -71,10 +71,16 @@ module S (C : Chans) = struct
   open Protocol
   open Protocol_shell
 
+  (* Shell calls (they do have an equivalent version in LSP) *)
   let set_workspace =
     let module M = Wrap (SetWorkspace) (C) in
     M.call
 
+  let toc =
+    let module M = Wrap (TableOfContents) (C) in
+    M.call
+
+  (* Standard calls *)
   let start =
     let module M = Wrap (Start) (C) in
     M.call

petanque/json_shell/client.mli

@@ -14,6 +14,9 @@ module S (C : Chans) : sig
   val set_workspace :
     SetWorkspace.Params.t -> (SetWorkspace.Response.t, string) result
 
+  val toc :
+    TableOfContents.Params.t -> (TableOfContents.Response.t, string) result
+
   val start : Start.Params.t -> (Start.Response.t, string) result
   val run : RunTac.Params.t -> (RunTac.Response.t, string) result
   val goals : Goals.Params.t -> (Goals.Response.t, string) result

petanque/json_shell/interp_shell.ml

@@ -20,6 +20,8 @@ let request ~fn ~token ~id ~method_ ~params =
     match method_ with
     | s when String.equal SetWorkspace.method_ s ->
       do_handle ~fn ~token (do_request (module SetWorkspace) ~params)
+    | s when String.equal TableOfContents.method_ s ->
+      do_handle ~fn ~token (do_request (module TableOfContents) ~params)
     | _ ->
       (* JSON-RPC method not found *)
       let code = -32601 in

petanque/json_shell/protocol_shell.ml

@@ -1,6 +1,15 @@
+(************************************************************************)
+(* Flèche => RL agent: petanque                                         *)
+(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+      *)
+(* Copyright 2019-2024 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
+(* Written by: Emilio J. Gallego Arias & coq-lsp contributors           *)
+(************************************************************************)
+
 open Petanque_json
+open JAgent
 
-(* set_workspace RPC *)
+(** [set_workspace { debug; root }] sets the current workspace to the directory
+    specified in [root] *)
 module SetWorkspace = struct
   let method_ = "petanque/setWorkspace"
 
@@ -18,14 +27,37 @@ module SetWorkspace = struct
 
   module Handler = struct
     module Params = Params
-
-    module Response = struct
-      type t = unit [@@deriving yojson]
-    end
+    module Response = Response
 
     let handler =
       Protocol.HType.Immediate
         (fun ~token { Params.debug; root } ->
           Shell.set_workspace ~token ~debug ~root)
   end
 end
+
+(** [toc { uri } ] returns the table of contents for a document; the semantics
+    are quite Coq-specific, in particular, each sentence of the document can
+    contribute *)
+module TableOfContents = struct
+  let method_ = "petanque/toc"
+
+  module Params = struct
+    type t = { uri : Lsp.JLang.LUri.File.t } [@@deriving yojson]
+  end
+
+  module Response = struct
+    type t = (string * Lang.Ast.Info.t list option) list [@@deriving yojson]
+  end
+
+  module Handler = struct
+    module Params = Params
+    module Response = Response
+
+    let handler =
+      Protocol.HType.FullDoc
+        { uri_fn = (fun { Params.uri } -> uri)
+        ; handler = (fun ~token ~doc _ -> Shell.get_toc ~token ~doc)
+        }
+  end
+end

petanque/json_shell/shell.ml

@@ -102,3 +102,16 @@ let init_agent ~token ~debug ~roots =
   init_st := Some (init_coq ~debug);
   Fleche.Io.CallBack.set io;
   set_roots ~token ~debug ~roots
+
+let toc_to_info (name, node) =
+  let open Coq.Compat.Option.O in
+  let+ ast = Fleche.Doc.Node.ast node in
+  (name, ast.Fleche.Doc.Node.Ast.ast_info)
+
+let get_toc ~token:_ ~(doc : Fleche.Doc.t) :
+    ( (string * Lang.Ast.Info.t list option) list
+    , Petanque.Agent.Error.t )
+    Result.t =
+  let { Fleche.Doc.toc; _ } = doc in
+  let toc = CString.Map.bindings toc |> List.filter_map toc_to_info in
+  Ok toc

petanque/json_shell/shell.mli

@@ -25,3 +25,10 @@ val build_doc :
      token:Coq.Limits.Token.t
   -> uri:Lang.LUri.File.t
   -> (Fleche.Doc.t, Agent.Error.t) Result.t
+
+val get_toc :
+     token:Coq.Limits.Token.t
+  -> doc:Fleche.Doc.t
+  -> ( (string * Lang.Ast.Info.t list option) list
+     , Petanque.Agent.Error.t )
+     Result.t

petanque/test/json_api.ml

@@ -34,6 +34,20 @@ let pp_premise fmt { Petanque.Agent.Premise.full_name; file; info } =
 
 let print_premises = false
 
+let pp_toc fmt (name, ast_info) =
+  let pp_ast_info fmt ast_info =
+    let ast_info =
+      Option.map (List.map JAgent.Lang.Ast.Info.to_yojson) ast_info
+    in
+    Format.fprintf fmt "@[%a@]"
+      Format.(pp_print_option (pp_print_list Yojson.Safe.pp))
+      ast_info
+  in
+  Format.(
+    fprintf fmt "@[{ name = %s; ast_info = @[%a@] @]" name pp_ast_info ast_info)
+
+let print_toc = false
+
 let run (ic, oc) =
   let open Coq.Compat.Result.O in
   let debug = false in
@@ -57,6 +71,8 @@ let run (ic, oc) =
   let* premises = S.premises { st } in
   (if print_premises then
      Format.(eprintf "@[%a@]@\n%!" (pp_print_list pp_premise) premises));
+  let* toc = S.toc { uri } in
+  (if print_toc then Format.(eprintf "@[%a@]@\n%!" (pp_print_list pp_toc) toc));
   let* st = S.run { opts = None; st; tac = "induction l." } in
   let* h1 = S.state_hash { st = st.st } in
   let* h1_p = S.state_proof_hash { st = st.st } in