Remove calls to Global.env and Libobject from Recordops

interp/declare.ml

@@ -346,6 +346,25 @@ let inInductive : mutual_inductive_entry -> obj =
     discharge_function = discharge_inductive;
     rebuild_function = rebuild_inductive }
 
+let cache_prim (_,(p,c)) = Recordops.register_primitive_projection p c
+
+let load_prim _ p = cache_prim p
+
+let subst_prim (subst,(p,c)) = Mod_subst.subst_proj_repr subst p, Mod_subst.subst_constant subst c
+
+let discharge_prim (_,(p,c)) = Some (Lib.discharge_proj_repr p, c)
+
+let inPrim : (Projection.Repr.t * Constant.t) -> obj =
+  declare_object {
+    (default_object "PRIMPROJS") with
+    cache_function = cache_prim ;
+    load_function = load_prim;
+    subst_function = subst_prim;
+    classify_function = (fun x -> Substitute x);
+    discharge_function = discharge_prim }
+
+let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c))
+
 let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) =
   let id = Label.to_id label in
   let univs, u = match univs with
@@ -360,7 +379,7 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter
   let entry = definition_entry ~types ~univs term in
   let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in
   let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in
-  Recordops.declare_primitive_projection p cst
+  declare_primitive_projection p cst
 
 
 let declare_projections univs mind =

pretyping/recordops.ml

@@ -21,7 +21,6 @@ open Pp
 open Names
 open Globnames
 open Constr
-open Libobject
 open Mod_subst
 open Reductionops
 
@@ -50,10 +49,10 @@ let projection_table =
 type struc_tuple =
     constructor * (Name.t * bool) list * Constant.t option list
 
-let load_structure i (_, (id,kl,projs)) =
+let register_structure env (id,kl,projs) =
   let open Declarations in
   let ind = fst id in
-  let mib, mip = Global.lookup_inductive ind in
+  let mib, mip = Inductive.lookup_mind_specif env ind in
   let n = mib.mind_nparams in
   let struc =
     { s_CONST = id; s_EXPECTEDPARAM = n; s_PROJ = projs; s_PROJKIND = kl } in
@@ -62,10 +61,7 @@ let load_structure i (_, (id,kl,projs)) =
     List.fold_right (Option.fold_right (fun proj -> Cmap.add proj struc))
       projs !projection_table
 
-let cache_structure o =
-  load_structure 1 o
-
-let subst_structure (subst, (id, kl, projs as obj)) =
+let subst_structure subst (id, kl, projs as obj) =
   let projs' =
    (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *)
    (* the first component of subst_con.                                   *)
@@ -77,19 +73,6 @@ let subst_structure (subst, (id, kl, projs as obj)) =
   if projs' == projs && id' == id then obj else
     (id',kl,projs')
 
-let discharge_structure (_, x) = Some x
-
-let inStruc : struc_tuple -> obj =
-  declare_object {(default_object "STRUCTURE") with
-    cache_function = cache_structure;
-    load_function = load_structure;
-    subst_function = subst_structure;
-    classify_function = (fun x -> Substitute x);
-    discharge_function = discharge_structure }
-
-let declare_structure o =
-  Lib.add_anonymous_leaf (inStruc o)
-
 let lookup_structure indsp = Indmap.find indsp !structure_table
 
 let lookup_projections indsp = (lookup_structure indsp).s_PROJ
@@ -107,26 +90,9 @@ let is_projection cst = Cmap.mem cst !projection_table
 let prim_table =
   Summary.ref (Cmap_env.empty : Projection.Repr.t Cmap_env.t) ~name:"record-prim-projs"
 
-let load_prim i (_,(p,c)) =
+let register_primitive_projection p c =
   prim_table := Cmap_env.add c p !prim_table
 
-let cache_prim p = load_prim 1 p
-
-let subst_prim (subst,(p,c)) = subst_proj_repr subst p, subst_constant subst c
-
-let discharge_prim (_,(p,c)) = Some (Lib.discharge_proj_repr p, c)
-
-let inPrim : (Projection.Repr.t * Constant.t) -> obj =
-  declare_object {
-    (default_object "PRIMPROJS") with
-    cache_function = cache_prim ;
-    load_function = load_prim;
-    subst_function = subst_prim;
-    classify_function = (fun x -> Substitute x);
-    discharge_function = discharge_prim }
-
-let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c))
-
 let is_primitive_projection c = Cmap_env.mem c !prim_table
 
 let find_primitive_projection c =
@@ -224,7 +190,7 @@ let warn_projection_no_head_constant =
           ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")
 
 (* Intended to always succeed *)
-let compute_canonical_projections env warn (con,ind) =
+let compute_canonical_projections env ~warn (con,ind) =
   let ctx = Environ.constant_context env con in
   let u = Univ.make_abstract_instance ctx in
   let v = (mkConstU (con,u)) in
@@ -274,11 +240,8 @@ let warn_redundant_canonical_projection =
           ++ strbrk " by " ++ prj ++ strbrk " in "
           ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s)
 
-let add_canonical_structure warn o =
-    (* XXX: Undesired global access to env *)
-    let env = Global.env () in
-    let sigma = Evd.from_env env in
-    compute_canonical_projections env warn o |>
+let register_canonical_structure ~warn env sigma o =
+    compute_canonical_projections env ~warn o |>
     List.iter (fun ((proj, (cs_pat, _ as pat)), s) ->
       let l = try GlobRef.Map.find proj !object_table with Not_found -> [] in
       match assoc_pat cs_pat l with
@@ -294,31 +257,13 @@ let add_canonical_structure warn o =
           warn_redundant_canonical_projection (hd_val, prj, new_can_s, old_can_s)
       )
 
-let open_canonical_structure i (_, o) =
-  if Int.equal i 1 then add_canonical_structure false o
-
-let cache_canonical_structure (_, o) =
-  add_canonical_structure true o
-
-let subst_canonical_structure (subst,(cst,ind as obj)) =
+let subst_canonical_structure subst (cst,ind as obj) =
   (* invariant: cst is an evaluable reference. Thus we can take *)
   (* the first component of subst_con.                                   *)
   let cst' = subst_constant subst cst in
   let ind' = subst_ind subst ind in
   if cst' == cst && ind' == ind then obj else (cst',ind')
 
-let discharge_canonical_structure (_,x) = Some x
-
-let inCanonStruc : Constant.t * inductive -> obj =
-  declare_object {(default_object "CANONICAL-STRUCTURE") with
-    open_function = open_canonical_structure;
-    cache_function = cache_canonical_structure;
-    subst_function = subst_canonical_structure;
-    classify_function = (fun x -> Substitute x);
-    discharge_function = discharge_canonical_structure }
-
-let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
-
 (*s High-level declaration of a canonical structure *)
 
 let error_not_structure ref description =
@@ -327,20 +272,17 @@ let error_not_structure ref description =
        (Id.print (Nametab.basename_of_global ref) ++ str"." ++ spc() ++
           description))
 
-let check_and_decompose_canonical_structure ref =
+let check_and_decompose_canonical_structure env sigma ref =
   let sp =
     match ref with
       ConstRef sp -> sp
     |  _ -> error_not_structure ref (str "Expected an instance of a record or structure.")
   in
-  let env = Global.env () in
   let u = Univ.make_abstract_instance (Environ.constant_context env sp) in
   let vc = match Environ.constant_opt_value_in env (sp, u) with
     | Some vc -> vc
     | None -> error_not_structure ref (str "Could not find its value in the global environment.") in
-  let env = Global.env () in
-  let evd = Evd.from_env env in
-  let body = snd (splay_lam (Global.env()) evd (EConstr.of_constr vc)) in
+  let body = snd (splay_lam env sigma (EConstr.of_constr vc)) in
   let body = EConstr.Unsafe.to_constr body in
   let f,args = match kind body with
     | App (f,args) -> f,args
@@ -353,15 +295,12 @@ let check_and_decompose_canonical_structure ref =
     try lookup_structure indsp
     with Not_found ->
       error_not_structure ref
-        (str "Could not find the record or structure " ++ Termops.Internal.print_constr_env env evd (EConstr.mkInd indsp)) in
+        (str "Could not find the record or structure " ++ Termops.Internal.print_constr_env env sigma (EConstr.mkInd indsp)) in
   let ntrue_projs = List.count snd s.s_PROJKIND in
   if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then
     error_not_structure ref (str "Got too few arguments to the record or structure constructor.");
   (sp,indsp)
 
-let declare_canonical_structure ref =
-  add_canonical_structure (check_and_decompose_canonical_structure ref)
-
 let lookup_canonical_conversion (proj,pat) =
   assoc_pat pat (GlobRef.Map.find proj !object_table)
 

pretyping/recordops.mli

@@ -26,7 +26,8 @@ type struc_typ = {
 type struc_tuple =
     constructor * (Name.t * bool) list * Constant.t option list
 
-val declare_structure : struc_tuple -> unit
+val register_structure : Environ.env -> struc_tuple -> unit
+val subst_structure : Mod_subst.substitution -> struc_tuple -> struc_tuple
 
 (** [lookup_structure isp] returns the struc_typ associated to the
    inductive path [isp] if it corresponds to a structure, otherwise
@@ -47,7 +48,7 @@ val find_projection : GlobRef.t -> struc_typ
 val is_projection : Constant.t -> bool
 
 (** Sets up the mapping from constants to primitive projections *)
-val declare_primitive_projection : Projection.Repr.t -> Constant.t -> unit
+val register_primitive_projection : Projection.Repr.t -> Constant.t -> unit
 
 val is_primitive_projection : Constant.t -> bool
 
@@ -80,8 +81,12 @@ val cs_pattern_of_constr : Environ.env -> constr -> cs_pattern * int option * co
 val pr_cs_pattern : cs_pattern -> Pp.t
 
 val lookup_canonical_conversion : (GlobRef.t * cs_pattern) -> constr * obj_typ
-val declare_canonical_structure : GlobRef.t -> unit
+val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map ->
+  Constant.t * inductive -> unit
+val subst_canonical_structure : Mod_subst.substitution -> Constant.t * inductive -> Constant.t * inductive
 val is_open_canonical_projection :
   Environ.env -> Evd.evar_map -> Reductionops.state -> bool
 val canonical_projections : unit ->
   ((GlobRef.t * cs_pattern) * obj_typ) list
+
+val check_and_decompose_canonical_structure : Environ.env -> Evd.evar_map -> GlobRef.t -> Constant.t * inductive

vernac/canonical.ml

@@ -0,0 +1,39 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+open Names
+open Libobject
+open Recordops
+
+let open_canonical_structure i (_, o) =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  if Int.equal i 1 then register_canonical_structure env sigma ~warn:false o
+
+let cache_canonical_structure (_, o) =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  register_canonical_structure ~warn:true env sigma o
+
+let discharge_canonical_structure (_,x) = Some x
+
+let inCanonStruc : Constant.t * inductive -> obj =
+  declare_object {(default_object "CANONICAL-STRUCTURE") with
+                  open_function = open_canonical_structure;
+                  cache_function = cache_canonical_structure;
+                  subst_function = (fun (subst,c) -> subst_canonical_structure subst c);
+                  classify_function = (fun x -> Substitute x);
+                  discharge_function = discharge_canonical_structure }
+
+let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
+
+let declare_canonical_structure ref =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  add_canonical_structure (check_and_decompose_canonical_structure env sigma ref)

vernac/canonical.mli

@@ -0,0 +1,12 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+open Names
+
+val declare_canonical_structure : GlobRef.t -> unit

vernac/record.ml

@@ -30,6 +30,7 @@ open Constrexpr
 open Constrexpr_ops
 open Goptions
 open Context.Rel.Declaration
+open Libobject
 
 module RelDecl = Context.Rel.Declaration
 
@@ -373,6 +374,27 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f
 
 open Typeclasses
 
+let load_structure i (_, structure) =
+  Recordops.register_structure (Global.env()) structure
+
+let cache_structure o =
+  load_structure 1 o
+
+let subst_structure (subst, (id, kl, projs as obj)) =
+  Recordops.subst_structure subst obj
+
+let discharge_structure (_, x) = Some x
+
+let inStruc : Recordops.struc_tuple -> obj =
+  declare_object {(default_object "STRUCTURE") with
+    cache_function = cache_structure;
+    load_function = load_structure;
+    subst_function = subst_structure;
+    classify_function = (fun x -> Substitute x);
+    discharge_function = discharge_structure }
+
+let declare_structure_entry o =
+  Lib.add_anonymous_leaf (inStruc o)
 
 let declare_structure ~cum finite ubinders univs paramimpls params template ?(kind=StructureComponent) ?name record_data =
   let nparams = List.length params in
@@ -443,7 +465,7 @@ let declare_structure ~cum finite ubinders univs paramimpls params template ?(ki
     let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in
     let build = ConstructRef cstr in
     let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
-    let () = Recordops.declare_structure(cstr, List.rev kinds, List.rev sp_projs) in
+    let () = declare_structure_entry (cstr, List.rev kinds, List.rev sp_projs) in
     rsp
   in
   List.mapi map record_data

vernac/record.mli

@@ -24,6 +24,8 @@ val declare_projections :
   Constr.rel_context ->
     (Name.t * bool) list * Constant.t option list
 
+val declare_structure_entry : Recordops.struc_tuple -> unit
+
 val definition_structure :
   universe_decl_expr option -> inductive_kind -> template:bool option ->
   Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic ->

vernac/vernac.mllib

@@ -12,6 +12,7 @@ Vernacextend
 Ppvernac
 Proof_using
 Lemmas
+Canonical
 Class
 Egramcoq
 Metasyntax

vernac/vernacentries.ml

@@ -572,7 +572,7 @@ let vernac_definition_hook p = function
 | Coercion ->
   Some (Class.add_coercion_hook p)
 | CanonicalStructure ->
-  Some (Lemmas.mk_hook (fun _ _ _ -> Recordops.declare_canonical_structure))
+  Some (Lemmas.mk_hook (fun _ _ _ -> Canonical.declare_canonical_structure))
 | SubClass ->
   Some (Class.add_subclass_hook p)
 | _ -> None
@@ -1041,7 +1041,7 @@ let vernac_require from import qidl =
 (* Coercions and canonical structures *)
 
 let vernac_canonical r =
-  Recordops.declare_canonical_structure (smart_global r)
+  Canonical.declare_canonical_structure (smart_global r)
 
 let vernac_coercion ~atts ref qids qidt =
   let local, polymorphic = Attributes.(parse Notations.(locality ++ polymorphic) atts) in