Remove the compare_graph field from the conversion API.

We know statically that the first thing the conversion algorithm is going to
do is to get it from the provided function, so we simply explicitly pass it
around.

kernel/nativeconv.ml

@@ -150,10 +150,10 @@ let warn_no_native_compiler =
          (fun () -> strbrk "Native compiler is disabled," ++
                       strbrk " falling back to VM conversion test.")
 
-let native_conv_gen pb sigma env univs t1 t2 =
+let native_conv_gen pb sigma env graph univs t1 t2 =
   if not (typing_flags env).Declarations.enable_native_compiler then begin
     warn_no_native_compiler ();
-    Vconv.vm_conv_gen pb env univs t1 t2
+    Vconv.vm_conv_gen pb env graph univs t1 t2
   end
   else
   let ml_filename, prefix = get_ml_filename () in
@@ -176,7 +176,7 @@ let native_conv cv_pb sigma env t1 t2 =
     else Constr.eq_constr_univs univs t1 t2
   in
   if not b then
-    let univs = (univs, checked_universes) in
+    let state = (univs, checked_universes) in
     let t1 = Term.it_mkLambda_or_LetIn t1 (Environ.rel_context env) in
     let t2 = Term.it_mkLambda_or_LetIn t2 (Environ.rel_context env) in
-    let _ = native_conv_gen cv_pb sigma env univs t1 t2 in ()
+    let _ = native_conv_gen cv_pb sigma env univs state t1 t2 in ()

kernel/reduction.ml

@@ -210,9 +210,6 @@ type conv_pb =
 let is_cumul = function CUMUL -> true | CONV -> false
 
 type 'a universe_compare = {
-  (* used in reduction *)
-  compare_graph : 'a -> UGraph.t;
-
   (* Might raise NotConvertible *)
   compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
   compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
@@ -222,7 +219,7 @@ type 'a universe_compare = {
 
 type 'a universe_state = 'a * 'a universe_compare
 
-type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b
+type ('a,'b) generic_conversion_function = env -> UGraph.t -> 'b universe_state -> 'a -> 'a -> 'b
 
 type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t
 
@@ -765,9 +762,8 @@ and convert_list l2r infos lft1 lft2 v1 v2 cuniv = match v1, v2 with
   convert_list l2r infos lft1 lft2 v1 v2 cuniv
 | _, _ -> raise NotConvertible
 
-let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
+let clos_gen_conv trans cv_pb l2r evars env graph univs t1 t2 =
   let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in
-  let graph = (snd univs).compare_graph (fst univs) in
   let infos = create_clos_infos ~univs:graph ~evars reds env in
   let infos = {
     cnv_inf = infos;
@@ -815,8 +811,7 @@ let check_inductive_instances cv_pb variance u1 u2 univs =
   else raise NotConvertible
 
 let checked_universes =
-  { compare_graph = (fun x -> x);
-    compare_sorts = checked_sort_cmp_universes;
+  { compare_sorts = checked_sort_cmp_universes;
     compare_instances = check_convert_instances;
     compare_cumul_instances = check_inductive_instances; }
 
@@ -878,8 +873,7 @@ let infer_inductive_instances cv_pb variance u1 u2 (univs,csts') =
   (univs, Univ.Constraint.union csts csts')
 
 let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare =
-  { compare_graph = (fun (x,_) -> x);
-    compare_sorts = infer_cmp_universes;
+  { compare_sorts = infer_cmp_universes;
     compare_instances = infer_convert_instances;
     compare_cumul_instances = infer_inductive_instances; }
 
@@ -890,7 +884,7 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 =
   in
     if b then ()
     else
-      let _ = clos_gen_conv reds cv_pb l2r evars env (univs, checked_universes) t1 t2 in
+      let _ = clos_gen_conv reds cv_pb l2r evars env univs (univs, checked_universes) t1 t2 in
         ()
 
 (* Profiling *)
@@ -905,9 +899,9 @@ let conv = gen_conv CONV
 
 let conv_leq = gen_conv CUMUL
 
-let generic_conv cv_pb ~l2r evars reds env univs t1 t2 =
+let generic_conv cv_pb ~l2r evars reds env graph univs t1 t2 =
   let (s, _) =
-    clos_gen_conv reds cv_pb l2r evars env univs t1 t2
+    clos_gen_conv reds cv_pb l2r evars env graph univs t1 t2
   in s
 
 let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 =
@@ -917,8 +911,8 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 =
   in
     if b then cstrs
     else
-      let univs = ((univs, Univ.Constraint.empty), inferred_universes) in
-      let ((_,cstrs), _) = clos_gen_conv reds cv_pb l2r evars env univs t1 t2 in
+      let state = ((univs, Univ.Constraint.empty), inferred_universes) in
+      let ((_,cstrs), _) = clos_gen_conv reds cv_pb l2r evars env univs state t1 t2 in
         cstrs
 
 (* Profiling *)

kernel/reduction.mli

@@ -37,8 +37,6 @@ type 'a extended_conversion_function =
 type conv_pb = CONV | CUMUL
 
 type 'a universe_compare = {
-  compare_graph : 'a -> UGraph.t; (* used for case inversion in reduction *)
-
   (* Might raise NotConvertible *)
   compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
   compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
@@ -48,7 +46,7 @@ type 'a universe_compare = {
 
 type 'a universe_state = 'a * 'a universe_compare
 
-type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b
+type ('a,'b) generic_conversion_function = env -> UGraph.t -> 'b universe_state -> 'a -> 'a -> 'b
 
 type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t
 

kernel/vconv.ml

@@ -190,10 +190,10 @@ let warn_bytecode_compiler_failed =
          (fun () -> strbrk "Bytecode compiler failed, " ++
                       strbrk "falling back to standard conversion")
 
-let vm_conv_gen cv_pb env univs t1 t2 =
+let vm_conv_gen cv_pb env graph univs t1 t2 =
   if not (typing_flags env).Declarations.enable_VM then
     Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
-      TransparentState.full env univs t1 t2
+      TransparentState.full env graph univs t1 t2
   else
   try
     let v1 = val_of_constr env t1 in
@@ -202,7 +202,7 @@ let vm_conv_gen cv_pb env univs t1 t2 =
   with Not_found | Invalid_argument _ ->
     warn_bytecode_compiler_failed ();
     Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
-      TransparentState.full env univs t1 t2
+      TransparentState.full env graph univs t1 t2
 
 let vm_conv cv_pb env t1 t2 =
   let univs = Environ.universes env in
@@ -211,5 +211,5 @@ let vm_conv cv_pb env t1 t2 =
     else Constr.eq_constr_univs univs t1 t2
   in
   if not b then
-    let univs = (univs, checked_universes) in
-    let _ = vm_conv_gen cv_pb env univs t1 t2 in ()
+    let state = (univs, checked_universes) in
+    let _ = vm_conv_gen cv_pb env univs state t1 t2 in ()

pretyping/reductionops.ml

@@ -1138,8 +1138,7 @@ let sigma_check_inductive_instances cv_pb variance u1 u2 sigma =
 
 let sigma_univ_state =
   let open Reduction in
-  { compare_graph = Evd.universes;
-    compare_sorts = sigma_compare_sorts;
+  { compare_sorts = sigma_compare_sorts;
     compare_instances = sigma_compare_instances;
     compare_cumul_instances = sigma_check_inductive_instances; }
 
@@ -1164,9 +1163,10 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
       | None ->
         let x = EConstr.Unsafe.to_constr x in
         let y = EConstr.Unsafe.to_constr y in
+        let graph = Evd.universes sigma in
         let sigma' =
           conv_fun pb ~l2r:false sigma ts
-            env (sigma, sigma_univ_state) x y in
+            env graph (sigma, sigma_univ_state) x y in
         Some sigma'
   with
   | Reduction.NotConvertible -> None