Merge pull request #735 from ejgallego/premise_info

[petanque] Return extra premise information.

CHANGES.md

@@ -168,6 +168,11 @@
  - [petanque] Return basic goal information after `run_tac`, so we
    avoid a `goals` round-trip for each tactic (@gbdrt, @ejgallego,
    #733)
+ - [coq] Add support for reading glob files metadata (@ejgallego,
+   #735)
+ - [petanque] Return extra premise information: file name, position,
+   raw_text, using the above support for reading .glob files
+   (@ejgallego, #735)
 
 # coq-lsp 0.1.8.1: Spring fix
 -----------------------------

compiler/compile.ml

@@ -22,7 +22,7 @@ let save_diags_file ~(doc : Fleche.Doc.t) =
   let file = Lang.LUri.File.to_string_file doc.uri in
   let file = Filename.remove_extension file ^ ".diags" in
   let diags = Fleche.Doc.diags doc in
-  Fleche.Compat.format_to_file ~file ~f:Output.pp_diags diags
+  Coq.Compat.format_to_file ~file ~f:Output.pp_diags diags
 
 (** Return: exit status for file:
 
@@ -47,9 +47,7 @@ let compile_file ~cc file : int =
     let workspace = workspace_of_uri ~io ~workspaces ~uri ~default in
     let files = Coq.Files.make () in
     let env = Doc.Env.make ~init:root_state ~workspace ~files in
-    let raw =
-      Fleche.Compat.Ocaml_414.In_channel.(with_open_bin file input_all)
-    in
+    let raw = Coq.Compat.Ocaml_414.In_channel.(with_open_bin file input_all) in
     let () = Theory.create ~io ~token ~env ~uri ~raw ~version:1 in
     match Theory.Check.maybe_check ~io ~token with
     | None -> 102

fleche/compat.ml → coq/compat.ml

@@ -105,6 +105,14 @@ module Result = struct
     let ( let+ ) r f = map f r
     let ( let* ) r f = bind r f
   end
+
+  let split = function
+    | Ok (x1, x2) -> (Ok x1, Ok x2)
+    | Error err -> (Error err, Error err)
+
+  let pp pp_r pp_e fmt = function
+    | Ok r -> Format.fprintf fmt "@[Ok: @[%a@]@]" pp_r r
+    | Error e -> Format.fprintf fmt "@[Error: @[%a@]@]" pp_e e
 end
 
 let format_to_file ~file ~f x =

fleche/compat.mli → coq/compat.mli

@@ -25,4 +25,13 @@ module Result : sig
     val ( let+ ) : ('a, 'l) t -> ('a -> 'b) -> ('b, 'l) t
     val ( let* ) : ('a, 'l) t -> ('a -> ('b, 'l) t) -> ('b, 'l) t
   end
+
+  val split : ('a * 'b, 'e) t -> ('a, 'e) t * ('b, 'e) t
+
+  val pp :
+       (Format.formatter -> 'r -> unit)
+    -> (Format.formatter -> 'e -> unit)
+    -> Format.formatter
+    -> ('r, 'e) Result.t
+    -> unit
 end

coq/glob.ml

@@ -0,0 +1,190 @@
+(************************************************************************)
+(*         *   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 =
+  match DefMap.find_opt name map with
+  | Some info -> Ok info
+  | None -> Error (Format.asprintf "definition %s not found in glob table" name)

coq/glob.mli

@@ -0,0 +1,30 @@
+(************************************************************************)
+(*         *   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                    *)
+(************************************************************************)
+
+(* Glob file that was read and parsed successfully *)
+type t
+
+val open_file : string -> (t, string) Result.t
+
+module Info : sig
+  type t =
+    { kind : string
+    ; offset : int * int
+    }
+end
+
+val get_info : t -> string -> (Info.t, string) Result.t

coq/library_file.ml

@@ -31,7 +31,7 @@ let iter_constructors indsp u fn env nconstr =
     fn (Names.GlobRef.ConstructRef (indsp, i)) typ
   done
 
-let ind_handler fn prefix (id, _) =
+let ind_handler fn prefix (id, (_obj : DeclareInd.Internal.inductive_obj)) =
   let open Names in
   let kn = KerName.make prefix.Nametab.obj_mp (Label.of_id id) in
   let mind = Global.mind_of_delta_kn kn in
@@ -84,8 +84,26 @@ let constructor_info (gref : Names.GlobRef.t) =
 let belongs_to_lib dps dp =
   List.exists (fun p -> Libnames.is_dirpath_prefix_of p dp) dps
 
-let toc dps : _ list =
-  let res = ref [] in
+module Entry = struct
+  type t =
+    { name : string
+    ; typ : Constr.t
+    ; file : string
+    }
+end
+
+let try_locate_absolute_library dir =
+  let f = Loadpath.try_locate_absolute_library in
+  CErrors.to_result ~f dir
+
+let find_v_file dir =
+  match try_locate_absolute_library dir with
+  (* EJGA: we want to improve this as to pass the error to the client *)
+  | Error _ -> "error when trying to locate the .v file"
+  | Ok file -> file
+
+let toc dps : Entry.t list =
+  let res : Entry.t list ref = ref [] in
   let obj_action =
     let fn_c (cst : Names.Constant.t) (_ : Decls.logical_kind) (typ : Constr.t)
         =
@@ -94,7 +112,8 @@ let toc dps : _ list =
         (* let () = F.eprintf "cst found: %s@\n%!" (Names.Constant.to_string
            cst) in *)
         let name = Names.Constant.to_string cst in
-        res := (name, typ) :: !res
+        let file = find_v_file cst_dp in
+        res := { name; typ; file } :: !res
       else ()
     in
     (* We do nothing for inductives, note this is called both on constructors
@@ -103,7 +122,9 @@ let toc dps : _ list =
       match constructor_info gref with
       | None -> ()
       | Some (ind_dp, name) ->
-        if belongs_to_lib dps ind_dp then res := (name, typ) :: !res
+        if belongs_to_lib dps ind_dp then
+          let file = find_v_file ind_dp in
+          res := { name; typ; file } :: !res
     in
     obj_action fn_c fn_i
   in

coq/library_file.mli

@@ -7,6 +7,14 @@ type t
 (** Logical path of the library *)
 val name : t -> Names.DirPath.t
 
+module Entry : sig
+  type t =
+    { name : string
+    ; typ : Constr.t
+    ; file : string
+    }
+end
+
 (** [toc libs] Returns the list of constants and inductives found on .vo
     libraries [libs], as pairs of [name, typ]. Note that the constants are
     returned in the order they appear on the file.
@@ -24,7 +32,7 @@ val toc :
      token:Limits.Token.t
   -> st:State.t
   -> t list
-  -> ((string * Constr.t) list, Loc.t) Protect.E.t
+  -> (Entry.t list, Loc.t) Protect.E.t
 
 (** Recovers the list of loaded libraries for state [st] *)
 val loaded : token:Limits.Token.t -> st:State.t -> (t list, Loc.t) Protect.E.t