Merge PR #18820: APIs for elpi stuff

Reviewed-by: SkySkimmer
Ack-by: CohenCyril
Ack-by: ppedrot
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>

engine/evd.ml

@@ -892,6 +892,8 @@ let mem d e = EvMap.mem e d.undf_evars || EvMap.mem e d.defn_evars
 
 let undefined_map d = d.undf_evars
 
+let defined_map d = d.defn_evars
+
 let drop_all_defined d = { d with defn_evars = EvMap.empty }
 
 (* spiwack: not clear what folding over an evar_map, for now we shall

engine/evd.mli

@@ -277,6 +277,9 @@ val add_quconstraints : evar_map -> Sorts.QUConstraints.t -> evar_map
 val undefined_map : evar_map -> undefined evar_info Evar.Map.t
 (** Access the undefined evar mapping directly. *)
 
+val defined_map : evar_map -> defined evar_info Evar.Map.t
+(** Access the defined evar mapping directly. *)
+
 val drop_all_defined : evar_map -> evar_map
 
 val drop_new_defined : original:evar_map -> evar_map -> evar_map

pretyping/structures.ml

@@ -97,6 +97,11 @@ let projection_nparams cst = (Cmap.find cst !projection_table).nparams
 
 let is_projection cst = Cmap.mem cst !projection_table
 
+let projection_number env cst =
+  let s = find_from_projection cst in
+  CList.index0 (Option.equal (Environ.QConstant.equal env)) (Some cst)
+    (List.map (fun x -> x.proj_body) s.projections)
+
 end
 
 (************************************************************************)
@@ -397,6 +402,18 @@ let is_open_canonical_projection env sigma c =
     with Failure _ -> false
   with Not_found -> false
 
+let print env sigma s =
+  let pr_econstr = Termops.Internal.debug_print_constr sigma in
+  let pr_econstr_list l = Pp.(str "[ " ++ prlist_with_sep (fun () -> str "; ") pr_econstr l ++ str " ]") in
+  Pp.(str "{ constant = " ++ pr_econstr s.constant ++ cut () ++
+     str "abstractions_ty = " ++ pr_econstr_list s.abstractions_ty ++ cut () ++
+     str "body = " ++ pr_econstr s.body ++ cut () ++
+     str "nparams = " ++ int s.nparams ++ cut () ++
+     str "params = " ++ pr_econstr_list s.params ++ cut () ++
+     str "cvalue_abstractions = " ++ pr_opt int s.cvalue_abstraction ++ cut () ++
+     str "cvalue_arguments = " ++ pr_econstr_list s.cvalue_arguments ++ cut () ++
+     str "}")
+
 end
 
 module CSTable = struct

pretyping/structures.mli

@@ -53,6 +53,10 @@ val projection_nparams : Names.Constant.t -> int
 
 val is_projection : Names.Constant.t -> bool
 
+val projection_number : Environ.env -> Names.Constant.t -> int
+(** [projection_number env p] returns the position of the projection p in
+    the structure it corresponds to, counting from 0. *)
+
 end
 
 (** A canonical instance declares "canonical" conversion hints between
@@ -129,6 +133,8 @@ val find :
 val is_open_canonical_projection :
   Environ.env -> Evd.evar_map -> EConstr.t -> bool
 
+val print : Environ.env -> Evd.evar_map -> t -> Pp.t
+
 end
 
 (** Low level access to the Canonical Structure database *)