package coq-lsp

  1. Overview
  2. Docs
Language Server Protocol native server for Coq

Install

Dune Dependency

Authors

Maintainers

Sources

coq-lsp-0.1.9.8.19.tbz
sha256=ef664281ab6e242dd79374cbbe4f177f2f071d3457cd3b75c23643948d475961
sha512=3c180c0c2e1218936b6cacb37197370cf80be4c372c46e38a2ab403a5a6e99cd6403f927ecfc017aefa2ead856abb389d48feb183049bf2c7badb029ce13f1ee

doc/src/petanque_json/obj_map.ml.html

Source file obj_map.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
module type Obj = sig
  type t
  (* Not yet *)
  (* val equal : t -> t -> bool *)
end

module type S = sig
  type t [@@deriving yojson]
end

module Make (O : Obj) : S with type t = O.t = struct
  type t = O.t
  type _t = int [@@deriving yojson]

  module Memo = Hashtbl.Make (Int)

  let memo = Memo.create 1000

  let dump_memo () =
    let keys = Memo.to_seq_keys memo |> List.of_seq in
    Format.(eprintf "@[size: %d@]@\n%!" (List.length keys));
    Format.(eprintf "@[<v>%a@]@\n%!" (pp_print_list pp_print_int) keys)

  let last_id = ref 0

  let mk_id _ =
    incr last_id;
    !last_id

  let of_obj (s : O.t) : int =
    let id = mk_id s in
    let () = Memo.add memo id s in
    id

  let to_obj (id : int) : O.t =
    try Memo.find memo id
    with Not_found ->
      dump_memo ();
      raise Not_found

  let of_yojson json = _t_of_yojson json |> Result.map to_obj
  let to_yojson st : Yojson.Safe.t = of_obj st |> _t_to_yojson
end
OCaml

Innovation. Community. Security.