[serapi] Support for low-level evar information.

CHANGES.md

@@ -13,6 +13,8 @@
  - [nix]    Added Nix support (#249, fixes #248, @Zimmi48, reported
             by @nyraghu)
  - [serapi] Fix COQPATH support: interpret paths as absolute (#249, @Zimmi48)
+ - [serapi] New Query `(Evars (define %bool))` , which will serialize
+            low-level path information (#256, fixes #20, @ejgallego)
 
 ## Version 0.13.0:
 

serapi/serapi_protocol.ml

@@ -139,6 +139,7 @@ type coq_object =
                     (* * Evd.evar_map *)
   | CoqAssumptions of Serapi_assumptions.t
   | CoqComments of ((int * int) * string) list list
+  | CoqEvarInfo of (Evar.t * Evd.evar_info) list
 
 (******************************************************************************)
 (* Printing Sub-Protocol                                                      *)
@@ -239,6 +240,7 @@ let gen_pp_obj env sigma (obj : coq_object) : Pp.t =
   (* | CoqGoal (_,g,_) -> pr (Ppconstr.pr_lconstr_expr g) *)
   (* | CoqGlob   g -> pr (Printer.pr_glob_constr g) *)
   | CoqComments _ -> Pp.str "FIXME comments"
+  | CoqEvarInfo _ -> Pp.str "FIXME evarinfo"
 
 let str_pp_obj env sigma fmt (obj : coq_object)  =
   Format.fprintf fmt "%a" Pp.pp_with (gen_pp_obj env sigma obj)
@@ -384,6 +386,7 @@ let prefix_pred (prefix : string) (obj : coq_object) : bool =
   | CoqProof _      -> true
   | CoqAssumptions _-> true
   | CoqComments _   -> true
+  | CoqEvarInfo _   -> true
 
 let gen_pred (p : query_pred) (obj : coq_object) : bool = match p with
   | Prefix s -> prefix_pred s obj
@@ -421,6 +424,8 @@ type query_cmd =
   | Complete of string
   | Comments
   (** Get all comments of a document *)
+  | Evars of { defined : bool }
+  (** Get evar map, if [defined] is true, also output the defined variables. *)
 
 module QueryUtil = struct
 
@@ -567,6 +572,25 @@ module QueryUtil = struct
     let comments = Pcoq.Parsable.comments pa |> List.rev in
     _comments := comments :: !_comments
 
+  (* Include defined *)
+  let is_defined einfo =
+    match einfo.Evd.evar_body with
+    | Evd.Evar_empty -> false
+    | Evd.Evar_defined _ -> true
+
+  let build_evar_map ~defined sigma =
+    Evd.fold (fun ev einfo acc ->
+        if is_defined einfo && (not defined)
+        then acc
+        else (ev, einfo)::acc)
+      sigma []
+    |> List.rev
+
+  let evars ~pstate ~defined =
+    let proof = Declare.Proof.get pstate in
+    let Proof.{ sigma; _ } = Proof.data proof in
+    build_evar_map ~defined sigma
+
 end
 
 let obj_query ~doc ~pstate ~env (opt : query_opt) (cmd : query_cmd) : coq_object list =
@@ -609,6 +633,8 @@ let obj_query ~doc ~pstate ~env (opt : query_opt) (cmd : query_cmd) : coq_object
   | Complete prefix ->
     List.map (fun x -> CoqGlobRefExt x) (Nametab.completion_canditates (Libnames.qualid_of_string prefix))
   | Comments -> [CoqComments (List.rev !QueryUtil._comments)]
+  | Evars { defined } ->
+    Option.cata (fun pstate -> [CoqEvarInfo (QueryUtil.evars ~pstate ~defined)]) [] pstate
 
 let obj_filter preds objs =
   List.(fold_left (fun obj p -> filter (gen_pred p) obj) objs preds)

serapi/serapi_protocol.mli

@@ -237,6 +237,8 @@ type coq_object =
 
      See https://github.com/coq/coq/issues/12413 for updates on
      improved support *)
+  | CoqEvarInfo of (Evar.t * Evd.evar_info) list
+  (** List of evar bindings, maybe defined or undefined *)
 
 (******************************************************************************)
 (* Printing Sub-Protocol                                                      *)
@@ -360,6 +362,8 @@ type query_cmd =
   (** Naïve but efficient prefix-based completion of identifiers *)
   | Comments
   (** Get all comments of a document *)
+  | Evars of { defined : bool }
+  (** Get evar map, if [defined] is true, also output the defined variables. *)
 
 module QueryUtil : sig
   val info_of_id : Environ.env -> string -> coq_object list * coq_object list

serlib/ser_eConstr.ml

@@ -39,4 +39,3 @@ type types =
 type unsafe_judgment =
   [%import: EConstr.unsafe_judgment]
   [@@deriving sexp]
-

serlib/ser_environ.ml

@@ -42,6 +42,9 @@ type named_context_val =
   [%import: Environ.named_context_val]
   [@@deriving sexp_of]
 
+let named_context_val_of_sexp =
+  Serlib_base.opaque_of_sexp ~typ:"Environ.named_context_val"
+
 type link_info =
   [%import: Environ.link_info]
   [@@deriving sexp]
@@ -83,3 +86,4 @@ type ('constr, 'term) punsafe_judgment =
 type unsafe_judgment =
   [%import: Environ.unsafe_judgment]
   [@@deriving sexp]
+

serlib/ser_environ.mli

@@ -34,3 +34,5 @@ val sexp_of_punsafe_judgment :
 type unsafe_judgment = Environ.unsafe_judgment
 val unsafe_judgment_of_sexp : Sexp.t -> unsafe_judgment
 val sexp_of_unsafe_judgment : unsafe_judgment -> Sexp.t
+
+type named_context_val = Environ.named_context_val [@@deriving sexp]

serlib/ser_evd.ml

@@ -15,9 +15,11 @@
 
 open Sexplib.Std
 
+module Loc       = Ser_loc
 module Environ   = Ser_environ
 module Reduction = Ser_reduction
 module Constr    = Ser_constr
+module Evar_kinds = Ser_evar_kinds
 
 type econstr =
   [%import: Evd.econstr]
@@ -26,6 +28,41 @@ type econstr =
 let econstr_of_sexp s = Obj.magic (Constr.t_of_sexp s)
 let sexp_of_econstr c = Constr.sexp_of_t (Obj.magic c)
 
+type evar_body =
+  [%import: Evd.evar_body]
+  [@@deriving sexp]
+
+module Abstraction = struct
+
+  type abstraction =
+    [%import: Evd.Abstraction.abstraction]
+    [@@deriving sexp]
+
+  type t =
+    [%import: Evd.Abstraction.t]
+    [@@deriving sexp]
+end
+
+module Filter = struct
+
+  type t = Evd.Filter.t
+  let t_of_sexp = Serlib_base.opaque_of_sexp ~typ:"Evd.Filter.t"
+  let sexp_of_t = Serlib_base.sexp_of_opaque ~typ:"Evd.Filter.t"
+
+end
+
+module Identity = struct
+
+  type t = Evd.Identity.t
+  let t_of_sexp = Serlib_base.opaque_of_sexp ~typ:"Evd.Identity.t"
+  let sexp_of_t = Serlib_base.sexp_of_opaque ~typ:"Evd.Identity.t"
+
+end
+
+type evar_info =
+  [%import: Evd.evar_info]
+  [@@deriving sexp]
+
 type conv_pb = Reduction.conv_pb
   [@@deriving sexp]
 

serlib/ser_evd.mli

@@ -15,6 +15,8 @@
 
 open Sexplib
 
+type evar_info = Evd.evar_info [@@deriving sexp]
+
 type conv_pb = Evd.conv_pb
 val conv_pb_of_sexp : Sexp.t -> conv_pb
 val sexp_of_conv_pb : conv_pb -> Sexp.t

sertop/sertop_ser.ml

@@ -98,6 +98,7 @@ module Notation_gram = Ser_notation_gram
 module Genarg     = Ser_genarg
 module Loadpath   = Ser_loadpath
 module Printer    = Ser_printer
+module Evd        = Ser_evd
 
 (* Alias fails due to the [@@default in protocol] *)
 (* module Stm        = Ser_stm *)