Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[plugins] Fix the output of the AST dump plugin to be valid JSON #874

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
+16 −10
Open

[plugins] Fix the output of the AST dump plugin to be valid JSON #874

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
fe03e2b
Fix the output of the AST dump plugin to be a valid JSON
blackbird1128 Nov 15, 2024
56717c2
add a note in CHANGES.md
blackbird1128 Nov 15, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions CHANGES.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
# unreleased
------------

- [fcc] fix the output of the AST dump plugin to be valid JSON
- [fleche] fix quick fixes for errors being lost due to incorrect
handling of `send_diags_extra_data` (@ejgallego, #850)
- [vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, #872)
Expand Down
25 changes: 15 additions & 10 deletions plugins/astdump/main.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,17 +1,22 @@
open Fleche

let pp_json fmt (ast : Doc.Node.Ast.t) =
Lsp.JCoq.Ast.to_yojson ast.v |> Yojson.Safe.pretty_print fmt
type outputFormat = Json | Sexp

let pp_sexp fmt (ast : Doc.Node.Ast.t) =
let ast_to_json (ast : Doc.Node.Ast.t) =
Lsp.JCoq.Ast.to_yojson ast.v

let ast_to_sexp_string (ast : Doc.Node.Ast.t) =
Serlib.Ser_vernacexpr.sexp_of_vernac_control (Coq.Ast.to_coq ast.v)
|> Sexplib.Sexp.pp_hum fmt
|> Sexplib.Sexp.to_string_hum

let pw pp fmt ast = Format.fprintf fmt "@[%a@]" pp ast

let dump_asts ~out_file pp asts =
let f fmt asts = List.iter (pw pp fmt) asts in
Coq.Compat.format_to_file ~file:out_file ~f asts
let dump_asts ~out_file (asts: Doc.Node.Ast.t list) output_format =
let out_chan = open_out out_file in
match output_format with
Json ->
Yojson.Safe.pretty_to_channel out_chan (`List (List.map ast_to_json asts));
| Sexp ->
output_string out_chan (List.map (fun ast -> ast_to_sexp_string ast) asts |> String.concat "\n")

let dump_ast ~io ~token:_ ~(doc : Doc.t) =
let uri = doc.uri in
Expand All @@ -21,10 +26,10 @@ let dump_ast ~io ~token:_ ~(doc : Doc.t) =
let asts = Doc.asts doc in
(* Output json *)
let out_file_j = Lang.LUri.File.to_string_file uri ^ ".json.astdump" in
let () = dump_asts ~out_file:out_file_j pp_json asts in
dump_asts ~out_file:out_file_j asts Json;
(* Output sexp *)
let out_file_s = Lang.LUri.File.to_string_file uri ^ ".sexp.astdump" in
let () = dump_asts ~out_file:out_file_s pp_sexp asts in
dump_asts ~out_file:out_file_s asts Sexp;
Io.Report.msg ~io ~lvl "[ast plugin] dumping ast for %s was completed!"
uri_str;
()
Expand Down