[coq] API to handle Require Ast specifically

We add some convenience functions to inspect and evaluate Coq's
requires specifically.

Note that we don't yet handle the attributes / control pair of the
require, this is required to be fixed before merge (likely requires
cut and paste from Coq code + Coq PR to export the relevant functions
to do without duplication)

Co-authored-by: BHAKTISHAH <shahbhakti21@gmail.com>

coq/ast.ml

@@ -24,6 +24,44 @@ module Id = struct
   module Map = Names.Id.Map
 end
 
+module Require = struct
+  type ast = t
+
+  open Ppx_hash_lib.Std.Hash.Builtin
+  open Ppx_compare_lib.Builtin
+  module Loc = Serlib.Ser_loc
+  module Libnames = Serlib.Ser_libnames
+  module Attributes = Serlib.Ser_attributes
+  module Vernacexpr = Serlib.Ser_vernacexpr
+
+  type t =
+    { from : Libnames.qualid option
+    ; export : Vernacexpr.export_with_cats option
+    ; mods : (Libnames.qualid * Vernacexpr.import_filter_expr) list
+    ; loc : Loc.t option
+          [@ignore]
+          [@hash.ignore]
+          (* We need to ignore the loc of the Require statement, maybe it'd be
+             better to keep the wrapping of the original vernac into a
+             CAst.t? *)
+    ; attrs : Attributes.vernac_flag list
+    ; control : Vernacexpr.control_flag list
+    }
+  [@@deriving hash, compare]
+
+  (** Determine if the Ast is a Require *)
+  let extract = function
+    | { CAst.v =
+          { Vernacexpr.expr =
+              Vernacexpr.(VernacSynterp (VernacRequire (from, export, mods)))
+          ; control
+          ; attrs
+          }
+      ; loc
+      } -> Some { from; export; mods; loc; attrs; control }
+    | _ -> None
+end
+
 module Kinds = struct
   (* LSP kinds *)
   let _file = 1

coq/ast.mli

@@ -15,6 +15,23 @@ module Id : sig
   module Map : CMap.ExtS with type key = t and module Set := Set
 end
 
+module Require : sig
+  type ast = t
+
+  type t = private
+    { from : Libnames.qualid option
+    ; export : Vernacexpr.export_with_cats option
+    ; mods : (Libnames.qualid * Vernacexpr.import_filter_expr) list
+    ; loc : Loc.t option
+    ; attrs : Attributes.vernac_flag list
+    ; control : Vernacexpr.control_flag list
+    }
+  [@@deriving hash, compare]
+
+  (** Determine if the Ast is a Require *)
+  val extract : ast -> t option
+end
+
 (** [make_info ~st ast] Compute info about a possible definition in [ast], we
     need [~st] to compute the type. *)
 val make_info :

coq/dune

@@ -5,5 +5,5 @@
  ; depending on it, we should fix this upstream
  (inline_tests)
  (preprocess
-  (pps ppx_inline_test))
+  (pps ppx_compare ppx_hash ppx_inline_test))
  (libraries lang coq-core.vernac coq-serapi.serlib))

coq/files.ml

@@ -0,0 +1,24 @@
+(************************************************************************)
+(*         *   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                    *)
+(************************************************************************)
+
+open Ppx_hash_lib.Std.Hash.Builtin
+open Ppx_compare_lib.Builtin
+
+type t = int [@@deriving hash, compare]
+
+let make () = 0
+let bump i = i + 1

coq/files.mli

@@ -0,0 +1,23 @@
+(************************************************************************)
+(*         *   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                    *)
+(************************************************************************)
+
+type t [@@deriving hash, compare]
+
+val make : unit -> t
+
+(** [bump ()] Signal the files have changed *)
+val bump : t -> t

coq/interp.ml

@@ -21,3 +21,24 @@ let coq_interp ~st cmd =
   Vernacinterp.interp ~st cmd |> State.of_coq
 
 let interp ~st cmd = Protect.eval cmd ~f:(coq_interp ~st)
+
+(* XXX: We ignore control, to fix before merge *)
+let with_ctrl _ctrl fn x = fn x
+
+let with_control ~control fn x =
+  List.fold_left (fun fn ctrl -> with_ctrl ctrl fn) fn control x
+
+module Require = struct
+  let interp ~st _files
+      { Ast.Require.from; export; mods; loc = _; attrs; control } =
+    let () = Vernacstate.unfreeze_full_state (State.to_coq st) in
+    (* Fail if attributes are not empty *)
+    Attributes.unsupported_attributes attrs;
+    (* Execute control commands *)
+    let () =
+      with_control ~control (Vernacentries.vernac_require from export) mods
+    in
+    Vernacstate.freeze_full_state () |> State.of_coq
+
+  let interp ~st files cmd = Protect.eval ~f:(interp ~st files) cmd
+end

coq/interp.mli

@@ -15,4 +15,16 @@
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
 
+(** Intepretation of "pure" Coq commands, that is to say, commands that are
+    assumed not to interact with the file-system, etc... Note these commands
+    will be memoized. *)
 val interp : st:State.t -> Ast.t -> (State.t, Loc.t) Protect.E.t
+
+(** Interpretation of "require". We wrap this function for two reasons:
+
+    - to make the read-effect dependency explicit
+    - to workaround the lack of a pure interface in Coq *)
+module Require : sig
+  val interp :
+    st:State.t -> Files.t -> Ast.Require.t -> (State.t, Loc.t) Protect.E.t
+end

fleche/doc.ml

@@ -2,7 +2,7 @@
 (* Flèche => document manager: Document                                 *)
 (* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+      *)
 (* Copyright 2019-2023 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
-(* Written by: Emilio J. Gallego Arias                                  *)
+(* Written by: Emilio J. Gallego Arias & coq-lsp contributors           *)
 (************************************************************************)
 
 (* Should be moved to the right place *)
@@ -157,13 +157,10 @@ end = struct
 
   (* ast-dependent error diagnostic generation *)
   let extra_diagnostics_of_ast ast =
-    match (Node.Ast.to_coq ast).v with
-    | Vernacexpr.
-        { expr = VernacSynterp (VernacRequire (prefix, _export, module_refs))
-        ; _
-        } ->
-      let refs = List.map fst module_refs in
-      Some [ Lang.Diagnostic.Extra.FailedRequire { prefix; refs } ]
+    match Coq.Ast.Require.extract ast.Node.Ast.v with
+    | Some { Coq.Ast.Require.from; mods; _ } ->
+      let refs = List.map fst mods in
+      Some [ Lang.Diagnostic.Extra.FailedRequire { prefix = from; refs } ]
     | _ -> None
 
   let error ~range ~msg ~ast =

fleche/doc.mli

@@ -1,8 +1,8 @@
 (************************************************************************)
 (* Flèche => document manager: Document                                 *)
 (* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+      *)
-(* Copyright 2019-2023 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
-(* Written by: Emilio J. Gallego Arias                                  *)
+(* Copyright 2019-2024 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
+(* Written by: Emilio J. Gallego Arias & coq-lsp contributors           *)
 (************************************************************************)
 
 module Node : sig