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
open Fleche

let rec dump_univs ~token ~contents fmt (nuniv_prev, nconst_prev)
    (qed_total, qed_yes) (nodes : Doc.Node.t list) =
  match nodes with
  | [] -> Format.fprintf fmt "qed_total: %d / qed_yes: %d" qed_total qed_yes
  | next :: nodes -> (
    let st = next.state in
    let raw = Fleche.Contents.extract_raw ~contents ~range:next.range in
    let qed_total = qed_total + if String.equal "Qed." raw then 1 else 0 in
    match Coq.State.info_universes ~token ~st with
    | Coq.Protect.{ E.r = R.Completed (Ok (nuniv, nconst)); feedback = _ } ->
      let qed_yes =
        qed_yes
        +
        if nuniv_prev <> nuniv || nconst_prev <> nconst then (
          let raw = raw in
          (* maybe trim above ? *)
          Format.fprintf fmt "@[univs for \"%s\":@\n (%4d,%4d) {+%d, +%d}@\n@]"
            raw nuniv nconst (nuniv - nuniv_prev) (nconst - nconst_prev);
          if String.equal "Qed." raw then 1 else 0)
        else 0
      in
      dump_univs ~token ~contents fmt (nuniv, nconst) (qed_total, qed_yes) nodes
    | _ ->
      Format.fprintf fmt "Error!! Terminating!! X_X O_O@\n%!";
      ())

let dump_univs ~token ~out_file (doc : Doc.t) =
  let f fmt nodes =
    match Coq.State.info_universes ~token ~st:doc.root with
    | Coq.Protect.{ E.r = R.Completed (Ok root); feedback = _ } ->
      dump_univs ~token ~contents:doc.contents fmt root (0, 0) nodes
    | _ -> ()
  in
  Coq.Compat.format_to_file ~file:out_file ~f doc.nodes

let dump_univdiff ~io ~token ~(doc : Doc.t) =
  let uri = doc.uri in
  let uri_str = Lang.LUri.File.to_string_uri uri in
  let out_file = Lang.LUri.File.to_string_file uri ^ ".unidiff" in
  let lvl = Io.Level.Info in
  let ndiags = Doc.diags doc |> List.length in
  Io.Report.msg ~io ~lvl "[univdiff plugin] %d diags present for file..." ndiags;
  Io.Report.msg ~io ~lvl "[univdiff plugin] dumping universe diff for %s ..."
    uri_str;
  dump_univs ~token ~out_file doc;
  Io.Report.msg ~io ~lvl
    "[univdiff plugin] dumping universe diff for %s was completed!" uri_str;
  ()

let main () = Theory.Register.Completed.add dump_univdiff
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