diff options
-rw-r--r-- | engine/evd.ml | 12 | ||||
-rw-r--r-- | kernel/nativeconv.mli | 2 | ||||
-rw-r--r-- | kernel/reduction.ml | 44 | ||||
-rw-r--r-- | kernel/reduction.mli | 26 | ||||
-rw-r--r-- | kernel/vconv.mli | 2 | ||||
-rw-r--r-- | pretyping/reductionops.ml | 14 |
6 files changed, 48 insertions, 52 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 206014164..6651ff5f6 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -926,12 +926,12 @@ let update_sigma_env evd env = let test_conversion_gen env evd pb t u = match pb with | Reduction.CONV -> - Reduction.conv_universes - full_transparent_state ~evars:(existential_opt_value evd) env - (UState.ugraph evd.universes) t u - | Reduction.CUMUL -> Reduction.conv_leq_universes - full_transparent_state ~evars:(existential_opt_value evd) env - (UState.ugraph evd.universes) t u + Reduction.conv env + ~evars:((existential_opt_value evd), (UState.ugraph evd.universes)) + t u + | Reduction.CUMUL -> Reduction.conv_leq env + ~evars:((existential_opt_value evd), (UState.ugraph evd.universes)) + t u let test_conversion env d pb t u = try test_conversion_gen env d pb t u; true diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli index 4dddb9fd3..abc9e3a3c 100644 --- a/kernel/nativeconv.mli +++ b/kernel/nativeconv.mli @@ -11,7 +11,7 @@ open Nativelambda (** This module implements the conversion test by compiling to OCaml code *) -val native_conv : conv_pb -> evars -> types conversion_function +val native_conv : conv_pb -> evars -> types kernel_conversion_function (** A conversion function parametrized by a universe comparator. Used outside of the kernel. *) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 8c9be0edd..95bea9292 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -125,11 +125,15 @@ let whd_betadeltaiota_nolet env t = (********************************************************************) (* Conversion utility functions *) -type 'a conversion_function = env -> 'a -> 'a -> unit -type 'a trans_conversion_function = ?reds:Names.transparent_state -> 'a conversion_function -type 'a universe_conversion_function = env -> UGraph.t -> 'a -> 'a -> unit -type 'a trans_universe_conversion_function = - Names.transparent_state -> 'a universe_conversion_function + +(* functions of this type are called from the kernel *) +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:Names.transparent_state -> env -> + ?evars:((existential->constr option) * UGraph.t) -> + 'a -> 'a -> unit exception NotConvertible exception NotConvertibleVect of int @@ -616,7 +620,7 @@ let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = { compare = infer_cmp_universes; compare_instances = infer_convert_instances } -let fconv_universes reds cv_pb l2r evars env univs t1 t2 = +let fconv cv_pb l2r reds env evars univs t1 t2 = let b = if cv_pb = CUMUL then leq_constr_univs univs t1 t2 else eq_constr_univs univs t1 t2 @@ -627,22 +631,16 @@ let fconv_universes reds cv_pb l2r evars env univs t1 t2 = () (* Profiling *) -let fconv_universes = +let fconv cv_pb ?(l2r=false) ?(reds=full_transparent_state) env ?(evars=(fun _->None), universes env) = + let evars, univs = evars in if Flags.profile then let fconv_universes_key = Profile.declare_profile "trans_fconv_universes" in - Profile.profile8 fconv_universes_key fconv_universes - else fconv_universes + Profile.profile8 fconv_universes_key fconv cv_pb l2r reds env evars univs + else fconv cv_pb l2r reds env evars univs -let fconv ?(reds=full_transparent_state) cv_pb l2r evars env = - fconv_universes reds cv_pb l2r evars env (universes env) +let conv = fconv CONV -let conv ?(l2r=false) ?(evars=fun _->None) ?(reds=full_transparent_state) = - fconv ~reds CONV l2r evars - -let conv_universes ?(l2r=false) ?(evars=fun _->None) reds = - fconv_universes reds CONV l2r evars -let conv_leq_universes ?(l2r=false) ?(evars=fun _->None) reds = - fconv_universes reds CUMUL l2r evars +let conv_leq = fconv CUMUL let generic_conv cv_pb ~l2r evars reds env univs t1 t2 = let (s, _) = @@ -676,17 +674,19 @@ let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_sta infer_conv_universes CUMUL l2r evars ts env univs t1 t2 (* This reference avoids always having to link C code with the kernel *) -let vm_conv = ref (fun cv_pb -> fconv cv_pb false (fun _->None)) -let set_vm_conv f = vm_conv := f +let vm_conv = ref (fun cv_pb env -> + fconv cv_pb env ~evars:((fun _->None), universes env)) + +let set_vm_conv (f:conv_pb -> Term.types kernel_conversion_function) = vm_conv := f let vm_conv cv_pb env t1 t2 = try !vm_conv cv_pb env t1 t2 with Not_found | Invalid_argument _ -> Pp.msg_warning (Pp.str "Bytecode compilation failed, falling back to standard conversion"); - fconv cv_pb false (fun _->None) env t1 t2 + fconv cv_pb env t1 t2 let default_conv cv_pb ?(l2r=false) env t1 t2 = - fconv cv_pb false (fun _ -> None) env t1 t2 + fconv cv_pb env t1 t2 let default_conv_leq = default_conv CUMUL (* diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 304046a1d..f7a8d88c2 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -26,11 +26,11 @@ val nf_betaiota : env -> constr -> constr exception NotConvertible exception NotConvertibleVect of int -type 'a conversion_function = env -> 'a -> 'a -> unit -type 'a trans_conversion_function = ?reds:Names.transparent_state -> 'a conversion_function -type 'a universe_conversion_function = env -> UGraph.t -> 'a -> 'a -> unit -type 'a trans_universe_conversion_function = - Names.transparent_state -> 'a universe_conversion_function +type 'a kernel_conversion_function = env -> 'a -> 'a -> unit +type 'a extended_conversion_function = + ?l2r:bool -> ?reds:Names.transparent_state -> env -> + ?evars:((existential->constr option) * UGraph.t) -> + 'a -> 'a -> unit type conv_pb = CONV | CUMUL @@ -58,13 +58,9 @@ val convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t -> val checked_universes : UGraph.t universe_compare val inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare -val conv : - ?l2r:bool -> ?evars:(existential->constr option) -> constr trans_conversion_function +val conv : constr extended_conversion_function -val conv_universes : - ?l2r:bool -> ?evars:(existential->constr option) -> constr trans_universe_conversion_function -val conv_leq_universes : - ?l2r:bool -> ?evars:(existential->constr option) -> types trans_universe_conversion_function +val conv_leq : types extended_conversion_function (** These conversion functions are used by module subtyping, which needs to infer universe constraints inside the kernel *) @@ -77,11 +73,11 @@ val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) -> Names.transparent_state -> (constr,'a) generic_conversion_function (** option for conversion *) -val set_vm_conv : (conv_pb -> types conversion_function) -> unit -val vm_conv : conv_pb -> types conversion_function +val set_vm_conv : (conv_pb -> types kernel_conversion_function) -> unit +val vm_conv : conv_pb -> types kernel_conversion_function -val default_conv : conv_pb -> ?l2r:bool -> types conversion_function -val default_conv_leq : ?l2r:bool -> types conversion_function +val default_conv : conv_pb -> ?l2r:bool -> types kernel_conversion_function +val default_conv_leq : ?l2r:bool -> types kernel_conversion_function (************************************************************************) diff --git a/kernel/vconv.mli b/kernel/vconv.mli index 49e5d23e6..acf4c408f 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -12,7 +12,7 @@ open Reduction (********************************************************************** s conversion functions *) -val vm_conv : conv_pb -> types conversion_function +val vm_conv : conv_pb -> types kernel_conversion_function (** A conversion function parametrized by a universe comparator. Used outside of the kernel. *) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 97f35fbd3..3f02e4bfb 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1256,26 +1256,26 @@ let report_anomaly _ = let e = Errors.push e in iraise e -let test_trans_conversion (f: ?l2r:bool-> ?evars:'a->'b) reds env sigma x y = +let test_trans_conversion (f: constr Reduction.extended_conversion_function) reds env sigma x y = try let evars ev = safe_evar_value sigma ev in - let _ = f ~evars reds env (Evd.universes sigma) x y in + let _ = f ~reds env ~evars:(evars, Evd.universes sigma) x y in true with Reduction.NotConvertible -> false | e when is_anomaly e -> report_anomaly e -let is_conv ?(reds=full_transparent_state) env sigma = test_trans_conversion Reduction.conv_universes reds env sigma -let is_conv_leq ?(reds=full_transparent_state) env sigma = test_trans_conversion Reduction.conv_leq_universes reds env sigma +let is_conv ?(reds=full_transparent_state) env sigma = test_trans_conversion Reduction.conv reds env sigma +let is_conv_leq ?(reds=full_transparent_state) env sigma = test_trans_conversion Reduction.conv_leq reds env sigma let is_fconv ?(reds=full_transparent_state) = function | Reduction.CONV -> is_conv ~reds | Reduction.CUMUL -> is_conv_leq ~reds let check_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = let f = match pb with - | Reduction.CONV -> Reduction.conv_universes - | Reduction.CUMUL -> Reduction.conv_leq_universes + | Reduction.CONV -> Reduction.conv + | Reduction.CUMUL -> Reduction.conv_leq in - try f ~evars:(safe_evar_value sigma) ts env (Evd.universes sigma) x y; true + try f ~reds:ts env ~evars:(safe_evar_value sigma, Evd.universes sigma) x y; true with Reduction.NotConvertible -> false | Univ.UniverseInconsistency _ -> false | e when is_anomaly e -> report_anomaly e |