From 9a026fcaeb3fa2678b9c93da8204f9f1ddcc0b31 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 28 Sep 2020 09:54:42 +0200 Subject: 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 | 8 ++++---- kernel/reduction.ml | 24 +++++++++--------------- kernel/reduction.mli | 4 +--- kernel/vconv.ml | 10 +++++----- 4 files changed, 19 insertions(+), 27 deletions(-) (limited to 'kernel') 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 () -- cgit v1.2.3 From eb5a67de1fc586acc588d5c61c84df670284f054 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 11 Oct 2020 17:40:01 +0200 Subject: Pick the universe graph out of the environment in conversion API. --- kernel/mod_typing.ml | 10 ++++------ kernel/nativeconv.ml | 6 +++--- kernel/reduction.ml | 20 +++++++++++--------- kernel/reduction.mli | 4 ++-- kernel/subtyping.ml | 2 +- kernel/vconv.ml | 8 ++++---- 6 files changed, 25 insertions(+), 25 deletions(-) (limited to 'kernel') diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 5873d1f502..c7b866179b 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -80,12 +80,11 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = let j = Typeops.infer env' c in assert (j.uj_val == c); (* relevances should already be correct here *) let typ = cb.const_type in - let cst' = Reduction.infer_conv_leq env' (Environ.universes env') - j.uj_type typ in + let cst' = Reduction.infer_conv_leq env' j.uj_type typ in j.uj_val, cst' | Def cs -> let c' = Mod_subst.force_constr cs in - c, Reduction.infer_conv env' (Environ.universes env') c c' + c, Reduction.infer_conv env' c c' | Primitive _ -> error_incorrect_with_constraint lab in @@ -103,12 +102,11 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = let j = Typeops.infer env' c in assert (j.uj_val == c); (* relevances should already be correct here *) let typ = cb.const_type in - let cst' = Reduction.infer_conv_leq env' (Environ.universes env') - j.uj_type typ in + let cst' = Reduction.infer_conv_leq env' j.uj_type typ in cst' | Def cs -> let c' = Mod_subst.force_constr cs in - let cst' = Reduction.infer_conv env' (Environ.universes env') c c' in + let cst' = Reduction.infer_conv env' c c' in cst' | Primitive _ -> error_incorrect_with_constraint lab diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 3543168175..fc6afb79d4 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 graph univs t1 t2 = +let native_conv_gen pb sigma env univs t1 t2 = if not (typing_flags env).Declarations.enable_native_compiler then begin warn_no_native_compiler (); - Vconv.vm_conv_gen pb env graph univs t1 t2 + Vconv.vm_conv_gen pb env univs t1 t2 end else let ml_filename, prefix = get_ml_filename () in @@ -179,4 +179,4 @@ let native_conv cv_pb sigma env t1 t2 = 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 state t1 t2 in () + let _ = native_conv_gen cv_pb sigma env state t1 t2 in () diff --git a/kernel/reduction.ml b/kernel/reduction.ml index b572a39047..8258c1c086 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -219,9 +219,9 @@ type 'a universe_compare = { type 'a universe_state = 'a * 'a universe_compare -type ('a,'b) generic_conversion_function = env -> UGraph.t -> 'b universe_state -> 'a -> 'a -> 'b +type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b -type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t +type 'a infer_conversion_function = env -> 'a -> 'a -> Univ.Constraint.t let sort_cmp_universes env pb s0 s1 (u, check) = (check.compare_sorts env pb s0 s1 u, check) @@ -899,12 +899,14 @@ let conv = gen_conv CONV let conv_leq = gen_conv CUMUL -let generic_conv cv_pb ~l2r evars reds env graph univs t1 t2 = +let generic_conv cv_pb ~l2r evars reds env univs t1 t2 = + let graph = Environ.universes env in let (s, _) = 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 = +let infer_conv_universes cv_pb l2r evars reds env t1 t2 = + let univs = Environ.universes env in let b, cstrs = if cv_pb == CUMUL then Constr.leq_constr_univs_infer univs t1 t2 else Constr.eq_constr_univs_infer univs t1 t2 @@ -919,16 +921,16 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 = let infer_conv_universes = if Flags.profile then let infer_conv_universes_key = CProfile.declare_profile "infer_conv_universes" in - CProfile.profile8 infer_conv_universes_key infer_conv_universes + CProfile.profile7 infer_conv_universes_key infer_conv_universes else infer_conv_universes let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full) - env univs t1 t2 = - infer_conv_universes CONV l2r evars ts env univs t1 t2 + env t1 t2 = + infer_conv_universes CONV l2r evars ts env t1 t2 let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full) - env univs t1 t2 = - infer_conv_universes CUMUL l2r evars ts env univs t1 t2 + env t1 t2 = + infer_conv_universes CUMUL l2r evars ts env t1 t2 let default_conv cv_pb ?l2r:_ env t1 t2 = gen_conv cv_pb env t1 t2 diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 0027b7bf47..3c747f0ff8 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -46,9 +46,9 @@ type 'a universe_compare = { type 'a universe_state = 'a * 'a universe_compare -type ('a,'b) generic_conversion_function = env -> UGraph.t -> 'b universe_state -> 'a -> 'a -> 'b +type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b -type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t +type 'a infer_conversion_function = env -> 'a -> 'a -> Univ.Constraint.t val get_cumulativity_constraints : conv_pb -> Univ.Variance.t array -> Univ.Instance.t -> Univ.Instance.t -> Univ.Constraint.t diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 28baa82666..76a1c190be 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -85,7 +85,7 @@ let make_labmap mp list = let check_conv_error error why cst poly f env a1 a2 = try - let cst' = f env (Environ.universes env) a1 a2 in + let cst' = f env a1 a2 in if poly then if Constraint.is_empty cst' then cst else error (IncompatiblePolymorphism (env, a1, a2)) diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 304e7e8470..948195797e 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 graph univs t1 t2 = +let vm_conv_gen cv_pb env univs t1 t2 = if not (typing_flags env).Declarations.enable_VM then Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None) - TransparentState.full env graph univs t1 t2 + TransparentState.full env univs t1 t2 else try let v1 = val_of_constr env t1 in @@ -202,7 +202,7 @@ let vm_conv_gen cv_pb env graph univs t1 t2 = with Not_found | Invalid_argument _ -> warn_bytecode_compiler_failed (); Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None) - TransparentState.full env graph univs t1 t2 + TransparentState.full env univs t1 t2 let vm_conv cv_pb env t1 t2 = let univs = Environ.universes env in @@ -212,4 +212,4 @@ let vm_conv cv_pb env t1 t2 = in if not b then let state = (univs, checked_universes) in - let _ = vm_conv_gen cv_pb env univs state t1 t2 in () + let _ = vm_conv_gen cv_pb env state t1 t2 in () -- cgit v1.2.3 From 7320cd84f92793572550d1fe1a2181f40466fa81 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 11 Oct 2020 17:50:40 +0200 Subject: Similarly remove the explicit graph argument in the ~evar conversion API. --- kernel/reduction.ml | 6 +++--- kernel/reduction.mli | 2 +- kernel/typeops.mli | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) (limited to 'kernel') diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 8258c1c086..96bf370342 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -189,7 +189,7 @@ type 'a kernel_conversion_function = env -> 'a -> 'a -> unit (* functions of this type can be called from outside the kernel *) type 'a extended_conversion_function = ?l2r:bool -> ?reds:TransparentState.t -> env -> - ?evars:((existential->constr option) * UGraph.t) -> + ?evars:(existential->constr option) -> 'a -> 'a -> unit exception NotConvertible @@ -888,8 +888,8 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 = () (* Profiling *) -let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _->None), universes env) = - let evars, univs = evars in +let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _->None)) = + let univs = Environ.universes env in if Flags.profile then let fconv_universes_key = CProfile.declare_profile "trans_fconv_universes" in CProfile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 3c747f0ff8..7d32596f74 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -31,7 +31,7 @@ exception NotConvertible type 'a kernel_conversion_function = env -> 'a -> 'a -> unit type 'a extended_conversion_function = ?l2r:bool -> ?reds:TransparentState.t -> env -> - ?evars:((existential->constr option) * UGraph.t) -> + ?evars:(existential->constr option) -> 'a -> 'a -> unit type conv_pb = CONV | CUMUL diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 87a5666fcc..d381e55dd6 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -111,7 +111,7 @@ val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t (** {6 Miscellaneous. } *) (** Check that hyps are included in env and fails with error otherwise *) -val check_hyps_inclusion : env -> ?evars:((existential->constr option) * UGraph.t) -> +val check_hyps_inclusion : env -> ?evars:(existential->constr option) -> GlobRef.t -> Constr.named_context -> unit (** Types for primitives *) -- cgit v1.2.3