aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/nativeconv.ml8
-rw-r--r--kernel/reduction.ml24
-rw-r--r--kernel/reduction.mli4
-rw-r--r--kernel/vconv.ml10
-rw-r--r--pretyping/reductionops.ml6
5 files changed, 22 insertions, 30 deletions
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 01e9550ec5..3543168175 100644
--- a/kernel/nativeconv.ml
+++ b/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 ()
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 7c6b869b4a..b572a39047 100644
--- a/kernel/reduction.ml
+++ b/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 *)
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 4ae3838691..0027b7bf47 100644
--- a/kernel/reduction.mli
+++ b/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
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index cc2c2c0b4b..304e7e8470 100644
--- a/kernel/vconv.ml
+++ b/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 ()
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 08a6db5639..bea62c8bef 100644
--- a/pretyping/reductionops.ml
+++ b/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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:10:43 +0000