package coq-lsp

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

Install

Dune Dependency

Authors

Maintainers

Sources

coq-lsp-0.2.0.8.20.tbz
sha256=bcb9a4c3219aed47ffbfd7c8ea7a2f374140d8cdb76079927548f49c7e3576a9
sha512=945c0010b4952e41055cb7e35175d400e5c126dc340dd1c0ab53321605cd0d9539af6693a794cb81a9dec0385d0880d4417dae923b6d19c9b62913766a185d8c

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
44
45
46
module type Obj = sig
  val name : string

  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, _) Result.t =
    match Memo.find_opt memo id with
    | Some v -> Ok v
    | None ->
      if false then dump_memo ();
      Error (Format.asprintf "key %d for object %s not found" id O.name)

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

Innovation. Community. Security.