From 6493adea8a7fe71eeae73fa492d33e562439fbf8 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 21 Sep 2021 21:05:15 +0200 Subject: [PATCH] [serapi] Support for low-level evar information. Fixes #20 This is still experimental, in particular we should maybe provide a better support for handling #251. --- CHANGES.md | 2 ++ serapi/serapi_protocol.ml | 26 ++++++++++++++++++++++++++ serapi/serapi_protocol.mli | 4 ++++ serlib/ser_eConstr.ml | 1 - serlib/ser_environ.ml | 4 ++++ serlib/ser_environ.mli | 2 ++ serlib/ser_evd.ml | 37 +++++++++++++++++++++++++++++++++++++ serlib/ser_evd.mli | 2 ++ sertop/sertop_ser.ml | 1 + 9 files changed, 78 insertions(+), 1 deletion(-) diff --git a/CHANGES.md b/CHANGES.md index e319646b..b3920abb 100644 --- a/CHANGES.md +++ b/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: diff --git a/serapi/serapi_protocol.ml b/serapi/serapi_protocol.ml index 74d867cd..9ba401a6 100644 --- a/serapi/serapi_protocol.ml +++ b/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) diff --git a/serapi/serapi_protocol.mli b/serapi/serapi_protocol.mli index 2fee755b..dcd5e85a 100644 --- a/serapi/serapi_protocol.mli +++ b/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 diff --git a/serlib/ser_eConstr.ml b/serlib/ser_eConstr.ml index 54d22c56..15b9167b 100644 --- a/serlib/ser_eConstr.ml +++ b/serlib/ser_eConstr.ml @@ -39,4 +39,3 @@ type types = type unsafe_judgment = [%import: EConstr.unsafe_judgment] [@@deriving sexp] - diff --git a/serlib/ser_environ.ml b/serlib/ser_environ.ml index f1f840ce..a3399b4b 100644 --- a/serlib/ser_environ.ml +++ b/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] + diff --git a/serlib/ser_environ.mli b/serlib/ser_environ.mli index b0e82b64..600b580f 100644 --- a/serlib/ser_environ.mli +++ b/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] diff --git a/serlib/ser_evd.ml b/serlib/ser_evd.ml index 985ba23d..ea57b105 100644 --- a/serlib/ser_evd.ml +++ b/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] diff --git a/serlib/ser_evd.mli b/serlib/ser_evd.mli index fc43a516..0324dfd5 100644 --- a/serlib/ser_evd.mli +++ b/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 diff --git a/sertop/sertop_ser.ml b/sertop/sertop_ser.ml index 9ecafc11..d86293ad 100644 --- a/sertop/sertop_ser.ml +++ b/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 *)