package coq-lsp

  1. Overview
  2. Docs
package coq-lsp
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file main.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
module Lsp = Fleche_lsp
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 { msg; _ }))
    | Coq.Protect.R.Completed (Error (User { msg; _ })) ->
      let lvl = Io.Level.Error in
      Io.Report.msg ~io ~lvl "error when retrieving %s: %a" what Pp.pp_with msg;
      None
    | Coq.Protect.R.Interrupted -> None)

(* 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 ~token ~(contents : Contents.t) (node : Doc.Node.t) =
    let range = node.range in
    let raw = Fleche.Contents.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 ~token ~st) in
    { raw; range; ast; goals }
end

let pp_json pp fmt (astgoal : _ AstGoals.t) =
  AstGoals.to_yojson pp astgoal |> Yojson.Safe.pretty_print fmt

(* For now we have not added sexp serialization, but we can easily do so *)
(* let pp_sexp fmt (astgoal : AstGoals.t) = *)
(*   AstGoals.sexp_of astgoal *)
(*   |> Sexplib.Sexp.pp_hum fmt *)

let pw pp fmt v = Format.fprintf fmt "@[%a@]@\n" pp v

let pp_ast_goals ~io ~token ~contents pp fmt node =
  AstGoals.of_node ~io ~token ~contents node |> pw pp fmt

let dump_goals ~io ~token ~out_file ~(doc : Doc.t) pp =
  let contents = doc.contents in
  let f fmt nodes =
    List.iter (pp_ast_goals ~io ~token ~contents pp fmt) nodes
  in
  Coq.Compat.format_to_file ~file:out_file ~f doc.nodes

let pp d =
  (* Set to true to output Pp-formatted goals *)
  let output_pp = false in
  if output_pp then Lsp.JCoq.Pp.to_yojson d else `String (Pp.string_of_ppcmds d)

let dump_ast ~io ~token ~(doc : Doc.t) =
  let uri = doc.uri in
  let uri_str = Lang.LUri.File.to_string_uri uri in
  let lvl = Io.Level.Info in
  Io.Report.msg ~io ~lvl "[goaldump plugin] dumping goals for %s ..." uri_str;
  let out_file_j = Lang.LUri.File.to_string_file uri ^ ".json.goaldump" in
  let () = dump_goals ~io ~token ~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 *)
  Io.Report.msg ~io ~lvl "[goaldump plugin] dumping ast for %s was completed!"
    uri_str;
  ()

let main () = Theory.Register.Completed.add dump_ast
let () = main ()
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct