[plugin] Goal dump plugin.

This is a simple plugin that will output the Ast and goals of a
document. This is just a start, there are many tweaks that could be
performed indeed.

cc: @gbdrt

Co-authored-by: Guillaume Baudart <[email protected]>

compiler/compile.ml

@@ -28,8 +28,8 @@ let save_diags_file ~(doc : Fleche.Doc.t) =
 let compile_file ~cc file =
   let { Cc.io; root_state; workspaces } = cc in
   let lvl = Io.Level.info in
-  let message = Format.asprintf "compiling file %s@\n%!" file in
-  io.message ~lvl ~message;
+  let message = Format.asprintf "compiling file %s" file in
+  Io.Report.message ~io ~lvl ~message;
   match Lang.LUri.(File.of_uri (of_string file)) with
   | Error _ -> ()
   | Ok uri -> (

plugins/README.md

@@ -0,0 +1,13 @@
+# coq-lsp / Flèche plugins
+
+Easiest way to use plugins is
+
+```
+$ fcc --root=dir --plugin=coq-lsp.plugin.$name file.v
+```
+
+- `example`: prints a "this file was checked" message
+- `astdump`: dumps the Ast of the document, in both sexp and JSON
+  formats
+- `goaldump`: dumps the Ast of the document in JSON format, along with
+  the goals at that state.

plugins/goaldump/dune

@@ -0,0 +1,6 @@
+(library
+ (name Goaldumpl_plugin)
+ (public_name coq-lsp.plugin.goaldump)
+ (preprocess
+  (pps ppx_deriving_yojson))
+ (libraries coq-lsp.fleche coq-lsp.lsp))

plugins/goaldump/main.ml

@@ -0,0 +1,98 @@
+open Fleche
+
+(* Put these in an utility function for plugins *)
+let of_execution ~io ~what (v : (_, _) Coq.Protect.E.t) =
+  match v with
+  | { r; feedback = _ } -> (
+    match r with
+    | Coq.Protect.R.Completed (Ok goals) -> goals
+    | Coq.Protect.R.Completed (Error (Anomaly err))
+    | Coq.Protect.R.Completed (Error (User err)) ->
+      let message =
+        Format.asprintf "error when retrieving %s: %a" what Pp.pp_with (snd err)
+      in
+      Io.Report.message ~io ~lvl:Io.Level.error ~message;
+      None
+    | Coq.Protect.R.Interrupted -> None)
+
+let extract_raw ~(contents : Contents.t) ~(range : Lang.Range.t) =
+  let start = range.start.offset in
+  let length = range.end_.offset - start in
+  (* We need to be careful here as Doc.t always adds a last empty node on EOF,
+     but somehow the offset of this node seems suspicious, it seems like the Coq
+     parser increases the offset by one, we need to investigate. *)
+  let length =
+    if String.length contents.raw < start + length then
+      String.length contents.raw - start
+    else length
+  in
+  String.sub contents.raw start length
+
+(* We output a record for each sentence in the document, linear order. Note that
+   for unparseable nodes, we don't have an AST. *)
+module AstGoals = struct
+  (* Just to bring the serializers in scope *)
+  module Lang = Lsp.JLang
+  module Coq = Lsp.JCoq
+
+  type 'a t =
+    { raw : string
+    ; range : Lang.Range.t
+    ; ast : Coq.Ast.t option
+    ; goals : 'a Coq.Goals.reified_pp option
+    }
+  [@@deriving to_yojson]
+
+  let of_node ~io ~(contents : Contents.t) (node : Doc.Node.t) =
+    let range = node.range in
+    let raw = extract_raw ~contents ~range in
+    let ast = Option.map (fun n -> n.Doc.Node.Ast.v) node.ast in
+    let st = node.state in
+    let goals = of_execution ~io ~what:"goals" (Info.Goals.goals ~st) in
+    { raw; range; ast; goals }
+end
+
+let pp_json pp fmt (astgoal : _ AstGoals.t) =
+  let g_json = AstGoals.to_yojson pp astgoal in
+  Yojson.Safe.pretty_print fmt g_json
+
+(* For now we have not added sexp serialization, but we can easily do so *)
+(* let pp_sexp fmt (astgoal : AstGoals.t) = *)
+(*   let g_sexp = AstGoals.sexp_of astgoal in *)
+(*   Sexplib.Sexp.pp_hum fmt sast *)
+
+let pw pp fmt v = Format.fprintf fmt "@[%a@]@\n" pp v
+
+let pp_ast_goals ~io ~contents pp fmt node =
+  let res = AstGoals.of_node ~io ~contents node in
+  pw pp fmt res
+
+let dump_goals ~io ~out_file ~(doc : Doc.t) pp =
+  let out = Stdlib.open_out out_file in
+  let fmt = Format.formatter_of_out_channel out in
+  let contents = doc.contents in
+  List.iter (pp_ast_goals ~io ~contents pp fmt) doc.nodes;
+  Format.pp_print_flush fmt ();
+  Stdlib.close_out out
+
+let dump_ast ~io ~(doc : Doc.t) =
+  let uri = doc.uri in
+  let uri_str = Lang.LUri.File.to_string_uri uri in
+  let message = Format.asprintf "[ast plugin] dumping ast for %s ..." uri_str in
+  let lvl = Io.Level.info in
+  Io.Report.message ~io ~lvl ~message;
+  let out_file_j = Lang.LUri.File.to_string_file uri ^ ".json.goaldump" in
+  let pp d = `String (Pp.string_of_ppcmds d) in
+  (* Uncomment to output Pp-formatted goals *)
+  (* let pp d = Lsp.JCoq.Pp.to_yojson d in *)
+  let () = dump_goals ~io ~out_file:out_file_j ~doc (pp_json pp) in
+  (* let out_file_s = Lang.LUri.File.to_string_file uri ^ ".sexp.goaldump" in *)
+  (* let () = dump_goals ~out_file:out_file_s ~doc pp_sexp in *)
+  let message =
+    Format.asprintf "[ast plugin] dumping ast for %s was completed!" uri_str
+  in
+  Io.Report.message ~io ~lvl ~message;
+  ()
+
+let main () = Theory.Register.add dump_ast
+let () = main ()

test/compiler/run.t

@@ -23,7 +23,6 @@ Compile a single file
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] compiling file proj1/a.v
-
   $ ls proj1
   a.diags
   a.v
@@ -44,7 +43,6 @@ Compile a dependent file
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] compiling file proj1/b.v
-
   $ ls proj1
   a.diags
   a.v
@@ -65,9 +63,7 @@ Compile both files
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] compiling file proj1/a.v
-
   [message] compiling file proj1/b.v
-
   $ ls proj1
   a.diags
   a.v
@@ -88,7 +84,6 @@ Compile a dependent file without the dep being built
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] compiling file proj1/b.v
-
   $ ls proj1
   a.diags
   a.v
@@ -150,9 +145,7 @@ Use two workspaces
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] compiling file proj1/a.v
-
   [message] compiling file proj2/b.v
-
   fcc: internal error, uncaught exception:
        Sys_error("proj2/b.v: No such file or directory")
 
@@ -169,7 +162,6 @@ Load the example plugin
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] compiling file proj1/a.v
-
   [message] [example plugin] file checking for proj1/a.v was completed
 
 Load the astdump plugin
@@ -183,7 +175,6 @@ Load the astdump plugin
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] compiling file proj1/a.v
-
   [message] [ast plugin] dumping ast for proj1/a.v ...
   [message] [ast plugin] dumping ast for proj1/a.v was completed!
 
@@ -197,3 +188,19 @@ de-serialize the document back and check.
   $ ls proj1/a.v.json.astdump proj1/a.v.sexp.astdump
   proj1/a.v.json.astdump
   proj1/a.v.sexp.astdump
+
+We do the same for the goaldump plugin:
+  $ fcc --plugin=coq-lsp.plugin.goaldump --root proj1 proj1/a.v
+  [message] Configuration loaded from Command-line arguments
+   - coqlib is at: [TEST_PATH]
+     + coqcorelib is at: [TEST_PATH]
+   - Modules [Coq.Init.Prelude] will be loaded by default
+   - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope
+   - ocamlpath wasn't overriden
+     + findlib config: [TEST_PATH]
+     + findlib default location: [TEST_PATH]
+  [message] compiling file proj1/a.v
+  [message] [ast plugin] dumping ast for proj1/a.v ...
+  [message] [ast plugin] dumping ast for proj1/a.v was completed!
+  $ ls proj1/a.v.json.goaldump
+  proj1/a.v.json.goaldump