Merge PR #9909: Remove all but one call to `Global` in the pretyper

Ack-by: ejgallego
Reviewed-by: gares
Ack-by: maximedenes
Ack-by: ppedrot

1 files changed, 37 insertions, 85 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 5560e5e5f5..90ce1cc594 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -15,7 +15,6 @@ open Names
 open Constr
 open Libnames
 open Globnames
-open Libobject
 open Mod_subst
 
 (* usage qque peu general: utilise aussi dans record *)
@@ -288,7 +287,7 @@ let get_coercion_constructor env coe =
   let red x = fst (Reductionops.whd_all_stack env evd x) in
   match EConstr.kind evd (red (mkNamed coe.coe_value)) with
   | Constr.Construct (c, _) ->
-      c, Inductiveops.constructor_nrealargs c -1
+      c, Inductiveops.constructor_nrealargs env c -1
   | _ -> raise Not_found
 
 let lookup_pattern_path_between env (s,t) =
@@ -305,8 +304,8 @@ let install_path_printer f = path_printer := f
 
 let print_path x = !path_printer x
 
-let path_comparator : (inheritance_path -> inheritance_path -> bool) ref =
-  ref (fun _ _ -> false)
+let path_comparator : (Environ.env -> Evd.evar_map -> inheritance_path -> inheritance_path -> bool) ref =
+  ref (fun _ _ _ _ -> false)
 
 let install_path_comparator f = path_comparator := f
 
@@ -319,24 +318,24 @@ let warn_ambiguous_path =
 (* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit
                          coercion,source,target *)
 
-let different_class_params i =
+let different_class_params env i =
   let ci = class_info_from_index i in
     if (snd ci).cl_param > 0 then true
     else 
       match fst ci with
-      | CL_IND i -> Global.is_polymorphic (IndRef i)
-      | CL_CONST c -> Global.is_polymorphic (ConstRef c)
+      | CL_IND i -> Environ.is_polymorphic env (IndRef i)
+      | CL_CONST c -> Environ.is_polymorphic env (ConstRef c)
       | _ -> false
 
-let add_coercion_in_graph (ic,source,target) =
+let add_coercion_in_graph env sigma (ic,source,target) =
   let old_inheritance_graph = !inheritance_graph in
   let ambig_paths =
     (ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in
   let try_add_new_path (i,j as ij) p =
-    if not (Bijint.Index.equal i j) || different_class_params i then
+    if not (Bijint.Index.equal i j) || different_class_params env i then
       match lookup_path_between_class ij with
       | q ->
-        if not (compare_path p q) then
+        if not (compare_path env sigma p q) then
           ambig_paths := (ij,p)::!ambig_paths;
         false
       | exception Not_found -> (add_new_path ij p; true)
@@ -374,31 +373,42 @@ type coercion = {
   coercion_params : int;
 }
 
+let subst_coercion subst c =
+  let coe = subst_coe_typ subst c.coercion_type in
+  let cls = subst_cl_typ subst c.coercion_source in
+  let clt = subst_cl_typ subst c.coercion_target in
+  let clp = Option.Smart.map (subst_proj_repr subst) c.coercion_is_proj in
+  if c.coercion_type == coe && c.coercion_source == cls &&
+     c.coercion_target == clt && c.coercion_is_proj == clp
+  then c
+  else { c with coercion_type = coe; coercion_source = cls;
+                coercion_target = clt; coercion_is_proj = clp; }
+
 (* Computation of the class arity *)
 
-let reference_arity_length ref =
-  let t, _ = Typeops.type_of_global_in_context (Global.env ()) ref in
-  List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty (EConstr.of_constr t))) (** FIXME *)
+let reference_arity_length env sigma ref =
+  let t, _ = Typeops.type_of_global_in_context env ref in
+  List.length (fst (Reductionops.splay_arity env sigma (EConstr.of_constr t)))
 
-let projection_arity_length p =
-  let len = reference_arity_length (ConstRef (Projection.Repr.constant p)) in
+let projection_arity_length env sigma p =
+  let len = reference_arity_length env sigma (ConstRef (Projection.Repr.constant p)) in
   len - Projection.Repr.npars p
 
-let class_params = function
+let class_params env sigma = function
   | CL_FUN | CL_SORT -> 0
-  | CL_CONST sp -> reference_arity_length (ConstRef sp)
-  | CL_PROJ sp -> projection_arity_length sp
-  | CL_SECVAR sp -> reference_arity_length (VarRef sp)
-  | CL_IND sp  -> reference_arity_length (IndRef sp)
+  | CL_CONST sp -> reference_arity_length env sigma (ConstRef sp)
+  | CL_PROJ sp -> projection_arity_length env sigma sp
+  | CL_SECVAR sp -> reference_arity_length env sigma (VarRef sp)
+  | CL_IND sp  -> reference_arity_length env sigma (IndRef sp)
 
 (* add_class : cl_typ -> locality_flag option -> bool -> unit *)
 
-let add_class cl =
-  add_new_class cl { cl_param = class_params cl }
+let add_class env sigma cl =
+  add_new_class cl { cl_param = class_params env sigma cl }
 
-let cache_coercion (_, c) =
-  let () = add_class c.coercion_source in
-  let () = add_class c.coercion_target in
+let declare_coercion env sigma c =
+  let () = add_class env sigma c.coercion_source in
+  let () = add_class env sigma c.coercion_target in
   let is, _ = class_info c.coercion_source in
   let it, _ = class_info c.coercion_target in
   let xf =
@@ -409,65 +419,7 @@ let cache_coercion (_, c) =
       coe_param = c.coercion_params;
     } in
   let () = add_new_coercion c.coercion_type xf in
-  add_coercion_in_graph (xf,is,it)
-
-let open_coercion i o =
-  if Int.equal i 1 then
-    cache_coercion o
-
-let subst_coercion (subst, c) =
-  let coe = subst_coe_typ subst c.coercion_type in
-  let cls = subst_cl_typ subst c.coercion_source in
-  let clt = subst_cl_typ subst c.coercion_target in
-  let clp = Option.Smart.map (subst_proj_repr subst) c.coercion_is_proj in
-  if c.coercion_type == coe && c.coercion_source == cls &&
-     c.coercion_target == clt && c.coercion_is_proj == clp
-  then c
-  else { c with coercion_type = coe; coercion_source = cls;
-                coercion_target = clt; coercion_is_proj = clp; }
-
-let discharge_coercion (_, c) =
-  if c.coercion_local then None
-  else
-    let n =
-      try
-        let ins = Lib.section_instance c.coercion_type in
-        Array.length (snd ins)
-      with Not_found -> 0
-    in
-    let nc = { c with
-      coercion_params = n + c.coercion_params;
-      coercion_is_proj = Option.map Lib.discharge_proj_repr c.coercion_is_proj;
-    } in
-    Some nc
-
-let classify_coercion obj =
-  if obj.coercion_local then Dispose else Substitute obj
-
-let inCoercion : coercion -> obj =
-  declare_object {(default_object "COERCION") with
-    open_function = open_coercion;
-    cache_function = cache_coercion;
-    subst_function = subst_coercion;
-    classify_function = classify_coercion;
-    discharge_function = discharge_coercion }
-
-let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps =
-  let isproj = 
-    match coef with
-    | ConstRef c -> Recordops.find_primitive_projection c
-    | _ -> None
-  in
-  let c = {
-    coercion_type = coef;
-    coercion_local = local;
-    coercion_is_id = isid;
-    coercion_is_proj = isproj;
-    coercion_source = cls;
-    coercion_target = clt;
-    coercion_params = ps;
-  } in
-  Lib.add_anonymous_leaf (inCoercion c)
+  add_coercion_in_graph env sigma (xf,is,it)
 
 (* For printing purpose *)
 let pr_cl_index = Bijint.Index.print
@@ -490,7 +442,7 @@ module CoercionPrinting =
   struct
     type t = coe_typ
     let compare = GlobRef.Ordered.compare
-    let encode = coercion_of_reference
+    let encode _env = coercion_of_reference
     let subst = subst_coe_typ
     let printer x = Nametab.pr_global_env Id.Set.empty x
     let key = ["Printing";"Coercion"]