package coq-lsp

You can search for identifiers within the package.

in-package search v0.2.0

Language Server Protocol native server for Coq

Install

dune-project

Dependency

github.com Readme Changelog Edit opam file Versions (34)

Authors

Maintainers

E

e@x80.org

Sources

coq-lsp-0.2.4.9.0.tbz

sha256=b6bf58331589b0bc750c01cc96a607322cf20260e61bd74f64998e04a9b909d3

sha512=b74f88117a180b089f99dc2d0cd867bdeb7aef071fa487334cdd2961ac61b9ba592e7f58c509dd6920ca2708dcc64992944009d4dce504bb5d0e28bb7d963c07

doc/src/coq-lsp.coq/module.ml.html

Source file `module.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
(*************************************************************************)
(* Copyright 2015-2019 MINES ParisTech -- Dual License LGPL 2.1+ / GPL3+ *)
(* Copyright 2019-2024 Inria           -- Dual License LGPL 2.1+ / GPL3+ *)
(* Copyright 2024-2025 Emilio J. Gallego Arias  -- LGPL 2.1+ / GPL3+     *)
(* Copyright 2025      CNRS                     -- LGPL 2.1+ / GPL3+     *)
(* Written by: Emilio J. Gallego Arias & coq-lsp contributors            *)
(*************************************************************************)
(* Rocq Language Server Protocol: Rocq module API                        *)
(*************************************************************************)

type t =
  { dp : Names.DirPath.t
  ; source : string
  ; vo : string
  ; uri : Lang.LUri.File.t
  }

let uri { uri; _ } = uri
let source { source; _ } = source

let make dp =
  match Loadpath.locate_absolute_library dp with
  | Ok vo ->
    (* Fleche.Io.Log.trace "rq_definition" "File Found"; *)
    let source = Filename.remove_extension vo ^ ".v" in
    let source = Str.replace_first (Str.regexp "_build/default/") "" source in
    let uri = Lang.LUri.of_string ("file://" ^ source) in
    let uri = Lang.LUri.File.of_uri uri |> Result.get_ok in
    Ok { dp; source; vo; uri }
  | Error err ->
    (* Fleche.Io.Log.trace "rq_definition" "File Not Found :("; *)
    (* Debug? *)
    Error err

let offset_to_range source (bp, ep) =
  let text = Compat.Ocaml_414.In_channel.(with_open_text source input_all) in
  let rec count (lines, char) cur goal =
    if cur >= goal then (lines, char)
    else
      match text.[cur] with
      | '\n' -> count (lines + 1, 0) (cur + 1) goal
      | _ -> count (lines, char + 1) (cur + 1) goal
  in
  (* XXX UTF-8 / 16 adjust *)
  let bline, bchar = count (0, 0) 0 bp in
  let eline, echar = count (bline, bchar) bp ep in
  let start = Lang.Point.{ line = bline; character = bchar; offset = bp } in
  let end_ = Lang.Point.{ line = eline; character = echar; offset = ep } in
  Lang.Range.{ start; end_ }

let find { vo; source; _ } name =
  let glob = Filename.remove_extension vo ^ ".glob" in
  match Glob.open_file glob with
  | Error err ->
    (* Fleche.Io.Log.trace "rq_definition:open_file" "Error: %s" err; *)
    Error err
  | Ok g -> (
    match Glob.get_info g name with
    | Some { offset; _ } -> Ok (Some (offset_to_range source offset))
    | None ->
      (* Fleche.Io.Log.trace "rq_definition:get_info" "Not found"; *)
      Ok None)