[fleche] Write down the language interface to Flèche

This is both a sanity check and a step to prepare for other possible
users.

controller/coq_lsp.ml

@@ -1,17 +1,7 @@
-(************************************************************************)
-(*         *   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-2022 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
+(* Copyright 2019      MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *)
+(* Copyright 2019-2022 Inria           -- Dual License LGPL 2.1 / GPL3+ *)
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
 
@@ -140,7 +130,7 @@ let mk_syminfo file (name, _path, kind, pos) : J.t =
       ( "location"
       , `Assoc
           [ ("uri", `String file)
-          ; ("range", LSP.mk_range Fleche.Types.(to_range pos))
+          ; ("range", LSP.mk_range Fleche.Lang.Loc.(to_range pos))
           ] )
     ]
 
@@ -152,9 +142,11 @@ let _kind_of_type _tm = 13
 
 let do_symbols ofmt ~id params =
   let file, doc = grab_doc params in
-  let f loc id = mk_syminfo file (Names.Id.to_string id, "", 12, loc) in
+  let f loc id =
+    mk_syminfo file (Fleche.Lang.Ast.Id.to_string id, "", 12, loc)
+  in
   let ast = List.map (fun v -> v.Fleche.Doc.ast) doc.Fleche.Doc.nodes in
-  let slist = Coq.Ast.grab_definitions f ast in
+  let slist = Fleche.Lang.Ast.grab_definitions f ast in
   let msg = LSP.mk_reply ~id ~result:(`List slist) in
   LIO.send_json ofmt msg
 
@@ -192,9 +184,11 @@ let do_hover ofmt ~id params =
 let do_completion ofmt ~id params =
   let uri, _ = get_docTextPosition params in
   let doc = Hashtbl.find doc_table uri in
-  let f _loc id = `Assoc [ ("label", `String Names.Id.(to_string id)) ] in
+  let f _loc id =
+    `Assoc [ ("label", `String Fleche.Lang.Ast.Id.(to_string id)) ]
+  in
   let ast = List.map (fun v -> v.Fleche.Doc.ast) doc.Fleche.Doc.nodes in
-  let clist = Coq.Ast.grab_definitions f ast in
+  let clist = Fleche.Lang.Ast.grab_definitions f ast in
   let result = `List clist in
   let msg = LSP.mk_reply ~id ~result in
   LIO.send_json ofmt msg
@@ -319,25 +313,9 @@ let lsp_main log_file std vo_load_path ml_include_path =
   let debug_oc = open_out log_file in
   LIO.debug_fmt := F.formatter_of_out_channel debug_oc;
 
-  (* Dedukti stuff *)
-  let lvl_to_severity (lvl : Feedback.level) =
-    match lvl with
-    | Feedback.Debug -> 5
-    | Feedback.Info -> 4
-    | Feedback.Notice -> 3
-    | Feedback.Warning -> 2
-    | Feedback.Error -> 1
-  in
-
-  let fb_handler, fb_queue =
-    let q = ref [] in
-    ( (fun Feedback.{ contents; _ } ->
-        match contents with
-        | Message (lvl, loc, msg) ->
-          let lvl = lvl_to_severity lvl in
-          q := (loc, lvl, msg) :: !q
-        | _ -> ())
-    , q )
+  let msg_handler, msg_queue =
+    let q : Fleche.Lang.Message.t list ref = ref [] in
+    ((fun (loc, lvl, msg) -> q := (loc, lvl, msg) :: !q), q)
   in
 
   Fleche.Io.CallBack.set (lsp_cb oc);
@@ -347,10 +325,10 @@ let lsp_main log_file std vo_load_path ml_include_path =
 
   let debug = Fleche.Debug.backtraces in
   let state =
-    ( Coq.Init.(coq_init { fb_handler; debug; load_module; load_plugin })
+    ( Fleche.Lang.Init.(init { msg_handler; debug; load_module; load_plugin })
     , vo_load_path
     , ml_include_path
-    , fb_queue )
+    , msg_queue )
   in
 
   memo_read_from_disk ();

coq/ast.ml

@@ -4,8 +4,6 @@ type t = Vernacexpr.vernac_control
 
 let hash x = Serlib.Ser_vernacexpr.hash_vernac_control x
 let compare x y = Serlib.Ser_vernacexpr.compare_vernac_control x y
-let to_coq x = x
-let of_coq x = x
 let loc { CAst.loc; _ } = loc
 
 (* Printer is very fiddly w.r.t. state, especially when used for debug, so we
@@ -75,3 +73,38 @@ let grab_definitions f nodes =
 
 let marshal_in ic : t = Marshal.from_channel ic
 let marshal_out oc v = Marshal.to_channel oc v []
+
+module Internal = struct
+  let to_coq x = x
+  let of_coq x = x
+end
+
+(* Structure inference *)
+module View = struct
+  type ast = t
+
+  type t =
+    (* This could be also extracted from the interpretation *)
+    | Open of unit
+    | End of unit
+    | Require of
+        { prefix : Libnames.qualid option
+        ; refs : Libnames.qualid list
+        }
+    | Other
+
+  let kind ast =
+    match ast.CAst.v.Vernacexpr.expr with
+    | Vernacexpr.VernacStartTheoremProof _ -> Open ()
+    | Vernacexpr.VernacEndProof _ -> End ()
+    | Vernacexpr.VernacRequire (prefix, _export, module_refs) ->
+      let refs = List.map fst module_refs in
+      Require { prefix; refs }
+    | _ -> Other
+end
+
+module Id = Names.Id
+
+module QualId = struct
+  type t = Libnames.qualid
+end

coq/ast.mli

@@ -1,11 +1,46 @@
 type t
 
-val loc : t -> Loc.t option
+(* Single identifier *)
+module Id : sig
+  type t
+
+  val to_string : t -> string
+end
+
+(* Qualified Identifier *)
+module QualId : sig
+  type t
+end
+
+(* Comparison / hash functions *)
 val hash : t -> int
 val compare : t -> t -> int
-val to_coq : t -> Vernacexpr.vernac_control
-val of_coq : Vernacexpr.vernac_control -> t
+val loc : t -> Loc.t option
 val print : t -> Pp.t
-val grab_definitions : (Loc.t -> Names.Id.t -> 'a) -> t list -> 'a list
+val grab_definitions : (Loc.t -> Id.t -> 'a) -> t list -> 'a list
 val marshal_in : in_channel -> t
 val marshal_out : out_channel -> t -> unit
+
+(* Analysis on AST / Structure inference *)
+module View : sig
+  type ast = t
+
+  type t =
+    (* This could be also extracted from the interpretation *)
+    | Open of unit
+    | End of unit
+    | Require of
+        { prefix : QualId.t option
+        ; refs : QualId.t list
+        }
+    | Other
+
+  val kind : ast -> t
+end
+
+(* This can't be used outside of the [Coq] library, and will be gone once we
+   functiorialize the interface *)
+module Internal : sig
+  val to_coq : t -> Vernacexpr.vernac_control
+  val of_coq : Vernacexpr.vernac_control -> t
+end

coq/init.ml

@@ -18,16 +18,15 @@
 (* Low-level, internal Coq initialization                                 *)
 (**************************************************************************)
 
-type coq_opts =
-  { fb_handler : Feedback.feedback -> unit
-        (** callback to handle async feedback *)
+type opts =
+  { msg_handler : Message.t -> unit  (** callback to handle async feedback *)
   ; load_module : string -> unit  (** callback to load cma/cmo files *)
   ; load_plugin : Mltop.PluginSpec.t -> unit
         (** callback to load findlib packages *)
   ; debug : bool  (** Enable Coq Debug mode *)
   }
 
-let coq_init opts =
+let init opts =
   (* Core Coq initialization *)
   Lib.init ();
   Global.set_impredicative_set false;
@@ -41,7 +40,22 @@ let coq_init opts =
   (**************************************************************************)
 
   (* Initialize logging. *)
-  ignore (Feedback.add_feeder opts.fb_handler);
+  let lvl_to_severity (lvl : Feedback.level) =
+    match lvl with
+    | Feedback.Debug -> 5
+    | Feedback.Info -> 4
+    | Feedback.Notice -> 3
+    | Feedback.Warning -> 2
+    | Feedback.Error -> 1
+  in
+
+  let fb_handler = function
+    | Feedback.{ contents = Message (lvl, loc, msg); _ } ->
+      let lvl = lvl_to_severity lvl in
+      opts.msg_handler (loc, lvl, msg)
+    | _ -> ()
+  in
+  ignore (Feedback.add_feeder fb_handler);
 
   (* SerAPI plugins *)
   let load_plugin = opts.load_plugin in
@@ -61,7 +75,7 @@ let coq_init opts =
   (**************************************************************************)
   (* Add root state!!                                                       *)
   (**************************************************************************)
-  Vernacstate.freeze_interp_state ~marshallable:false |> State.of_coq
+  Vernacstate.freeze_interp_state ~marshallable:false |> State.Internal.of_coq
 
 (* End of initialization *)
 
@@ -90,33 +104,44 @@ let loadpath_from_coqproject () : Loadpath.vo_path list =
       (List.map (fun f -> to_vo_loadpath f.thing true) r_includes)
 
 (* Inits the context for a document *)
-let doc_init ~root_state ~vo_load_path ~ml_include_path ~libname ~require_libs =
-  (* Lsp.Io.log_error "init" "starting"; *)
-  Vernacstate.unfreeze_interp_state (State.to_coq root_state);
-
-  (* This should go away in Coq itself *)
-  Safe_typing.allow_delayed_constants := true;
-  let load_objs libs =
-    let rq_file (dir, from, exp) =
-      let mp = Libnames.qualid_of_string dir in
-      let mfrom = Option.map Libnames.qualid_of_string from in
-      Flags.silently
-        (Vernacentries.vernac_require mfrom exp)
-        [ (mp, Vernacexpr.ImportAll) ]
+module Doc = struct
+  type require_decl =
+    string * string option * Vernacexpr.export_with_cats option
+
+  type env =
+    { vo_load_path : Loadpath.vo_path list
+    ; ml_load_path : string list
+    ; requires : require_decl list
+    }
+
+  let make ~root_state ~env ~name =
+    (* Lsp.Io.log_error "init" "starting"; *)
+    Vernacstate.unfreeze_interp_state (State.Internal.to_coq root_state);
+
+    (* This should go away in Coq itself *)
+    Safe_typing.allow_delayed_constants := true;
+    let load_objs libs =
+      let rq_file (dir, from, exp) =
+        let mp = Libnames.qualid_of_string dir in
+        let mfrom = Option.map Libnames.qualid_of_string from in
+        Flags.silently
+          (Vernacentries.vernac_require mfrom exp)
+          [ (mp, Vernacexpr.ImportAll) ]
+      in
+      List.(iter rq_file (rev libs))
     in
-    List.(iter rq_file (rev libs))
-  in
 
-  (* Set load path; important, this has to happen before we declare the library
-     below as [Declaremods/Library] will infer the module name by looking at the
-     load path! *)
-  List.iter Mltop.add_ml_dir ml_include_path;
-  List.iter Loadpath.add_vo_path vo_load_path;
-  List.iter Loadpath.add_vo_path (loadpath_from_coqproject ());
-  Declaremods.start_library libname;
+    (* Set load path; important, this has to happen before we declare the
+       library below as [Declaremods/Library] will infer the module name by
+       looking at the load path! *)
+    List.iter Mltop.add_ml_dir env.ml_load_path;
+    List.iter Loadpath.add_vo_path env.vo_load_path;
+    List.iter Loadpath.add_vo_path (loadpath_from_coqproject ());
+    Declaremods.start_library name;
 
-  (* Import initial libraries. *)
-  load_objs require_libs;
+    (* Import initial libraries. *)
+    load_objs env.requires;
 
-  (* We return the state at this point! *)
-  Vernacstate.freeze_interp_state ~marshallable:false |> State.of_coq
+    (* We return the state at this point! *)
+    Vernacstate.freeze_interp_state ~marshallable:false |> State.Internal.of_coq
+end

coq/init.mli

@@ -18,22 +18,25 @@
 (* Low-level, internal Coq initialization                                 *)
 (**************************************************************************)
 
-type coq_opts =
-  { fb_handler : Feedback.feedback -> unit
-        (** callback to handle async feedback *)
+type opts =
+  { msg_handler : Message.t -> unit  (** callback to handle async feedback *)
   ; load_module : string -> unit  (** callback to load cma/cmo files *)
   ; load_plugin : Mltop.PluginSpec.t -> unit
         (** callback to load findlib packages *)
   ; debug : bool  (** Enable Coq Debug mode *)
   }
 
-val coq_init : coq_opts -> State.t
+val init : opts -> State.t
 
-val doc_init :
-     root_state:State.t
-  -> vo_load_path:Loadpath.vo_path list
-  -> ml_include_path:string list
-  -> libname:Names.DirPath.t
-  -> require_libs:
-       (string * string option * Vernacexpr.export_with_cats option) list
-  -> State.t
+module Doc : sig
+  type require_decl =
+    string * string option * Vernacexpr.export_with_cats option
+
+  type env =
+    { vo_load_path : Loadpath.vo_path list
+    ; ml_load_path : string list
+    ; requires : require_decl list
+    }
+
+  val make : root_state:State.t -> env:env -> name:Names.DirPath.t -> State.t
+end

coq/internal.ml

@@ -0,0 +1,23 @@
+module type Conv = sig
+  type t
+
+  module Internal : sig
+    type coq
+
+    val of_coq : coq -> t
+    val to_coq : t -> coq
+  end
+end
+
+module Make (S : sig
+  type coq
+end) : Conv with type Internal.coq = S.coq = struct
+  module Internal = struct
+    type coq = S.coq
+
+    let of_coq x = x
+    let to_coq x = x
+  end
+
+  type t = S.coq
+end

coq/interp.ml

@@ -30,9 +30,9 @@ let get_feedback fb_queue =
 type 'a interp_result = 'a Info.t Protect.R.t
 
 let coq_interp ~st cmd =
-  let st = State.to_coq st in
-  let cmd = Ast.to_coq cmd in
-  Vernacinterp.interp ~st cmd |> State.of_coq
+  let st = State.Internal.to_coq st in
+  let cmd = Ast.Internal.to_coq cmd in
+  Vernacinterp.interp ~st cmd |> State.Internal.of_coq
 
 let interp ~st ~fb_queue cmd =
   Protect.eval cmd ~f:(fun cmd ->