package coq-lsp

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

Source file glob.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
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(************************************************************************)
(* Coq Language Server Protocol                                         *)
(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+      *)
(* Copyright 2019-2024 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
(* Written by: Emilio J. Gallego Arias & Bhakti Shah                    *)
(************************************************************************)

module DefMap = CString.Map

module Error = struct
  type t =
    | Ill_formed of string
    | Outdated

  let to_string = function
    | Ill_formed s -> "Ill-formed file: " ^ s
    | Outdated -> "Outdated .glob file"
end

module Info = struct
  type t =
    { kind : string
    ; offset : int * int
    }
end

(* This is taken from coqdoc/glob_file.ml , we should share this code, but no
   cycles ATM *)
module Coq = struct
  module Entry_type = struct
    type t =
      | Library
      | Module
      | Definition
      | Inductive
      | Constructor
      | Lemma
      | Record
      | Projection
      | Instance
      | Class
      | Method
      | Variable
      | Axiom
      | TacticDefinition
      | Abbreviation
      | Notation
      | Section
      | Binder

    let of_string = function
      | "def"
      | "coe"
      | "subclass"
      | "canonstruc"
      | "fix"
      | "cofix"
      | "ex"
      | "scheme" -> Definition
      | "prf" | "thm" -> Lemma
      | "ind" | "variant" | "coind" -> Inductive
      | "constr" -> Constructor
      | "indrec" | "rec" | "corec" -> Record
      | "proj" -> Projection
      | "class" -> Class
      | "meth" -> Method
      | "inst" -> Instance
      | "var" -> Variable
      | "defax" | "prfax" | "ax" -> Axiom
      | "abbrev" | "syndef" -> Abbreviation
      | "not" -> Notation
      | "lib" -> Library
      | "mod" | "modtype" -> Module
      | "tac" -> TacticDefinition
      | "sec" -> Section
      | "binder" -> Binder
      | s -> invalid_arg ("type_of_string:" ^ s)
  end

  let read_dp ic =
    let line = input_line ic in
    let n = String.length line in
    match line.[0] with
    | 'F' ->
      let lib_name = String.sub line 1 (n - 1) in
      Ok lib_name
    | _ -> Error (Error.Ill_formed "lib name not found in header")

  let correct_file vfile ic =
    let s = input_line ic in
    if String.length s < 7 || String.sub s 0 7 <> "DIGEST " then
      Error (Error.Ill_formed "DIGEST ill-formed")
    else
      let s = String.sub s 7 (String.length s - 7) in
      match (vfile, s) with
      | None, "NO" -> read_dp ic
      | Some _, "NO" -> Error (Ill_formed "coming from .v file but no digest")
      | None, _ -> Error (Ill_formed "digest but .v source file not available")
      | Some vfile, s ->
        if s = Digest.to_hex (Digest.file vfile) then
          (* XXX Read F line *)
          read_dp ic
        else Error Outdated

  let parse_ref line =
    try
      (* Disable for now *)
      if false then
        let add_ref _ _ _ _ _ = () in
        Scanf.sscanf line "R%d:%d %s %s %s %s" (fun loc1 loc2 lib_dp sp id ty ->
            for loc = loc1 to loc2 do
              add_ref loc lib_dp sp id (Entry_type.of_string ty);
              (* Also add an entry for each module mentioned in [lib_dp], * to
                 use in interpolation. *)
              ignore
                (List.fold_right
                   (fun thisPiece priorPieces ->
                     let newPieces =
                       match priorPieces with
                       | "" -> thisPiece
                       | _ -> thisPiece ^ "." ^ priorPieces
                     in
                     add_ref loc "" "" newPieces Entry_type.Library;
                     newPieces)
                   (Str.split (Str.regexp_string ".") lib_dp)
                   "")
            done)
    with _ -> ()

  let parse_def line : _ Result.t =
    try
      Scanf.sscanf line "%s %d:%d %s %s"
        (fun kind loc1 loc2 section_path name ->
          Ok (name, section_path, kind, (loc1, loc2)))
    with Scanf.Scan_failure err -> Error err

  let process_line dp map line =
    match line.[0] with
    | 'R' ->
      let _reference = parse_ref line in
      map
    | _ -> (
      match parse_def line with
      | Error _ -> map
      | Ok (name, section_path, kind, offset) ->
        let section_path =
          if String.equal "<>" section_path then "" else section_path ^ "."
        in
        let name = dp ^ "." ^ section_path ^ name in
        let info = { Info.kind; offset } in
        DefMap.add name info map)

  let read_glob vfile inc =
    match correct_file vfile inc with
    | Error e -> Error (Error.to_string e)
    | Ok dp -> (
      let map = ref DefMap.empty in
      try
        while true do
          let line = input_line inc in
          let n = String.length line in
          if n > 0 then map := process_line dp !map line
        done;
        assert false
      with End_of_file -> Ok !map)
end

(* Glob file that was read and parsed successfully *)
type t = Info.t DefMap.t

let open_file file =
  if Sys.file_exists file then
    let vfile = Filename.remove_extension file ^ ".v" in
    Compat.Ocaml_414.In_channel.with_open_text file (Coq.read_glob (Some vfile))
  else Error (Format.asprintf "Cannot open file: %s" file)

let get_info map name = DefMap.find_opt name map
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