diff options
-rw-r--r-- | engine/evd.ml | 4 | ||||
-rw-r--r-- | kernel/reduction.ml | 50 | ||||
-rw-r--r-- | kernel/reduction.mli | 19 | ||||
-rw-r--r-- | pretyping/reductionops.ml | 8 |
4 files changed, 27 insertions, 54 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 425b67e08..206014164 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -926,10 +926,10 @@ let update_sigma_env evd env = let test_conversion_gen env evd pb t u = match pb with | Reduction.CONV -> - Reduction.trans_conv_universes + Reduction.conv_universes full_transparent_state ~evars:(existential_opt_value evd) env (UState.ugraph evd.universes) t u - | Reduction.CUMUL -> Reduction.trans_conv_leq_universes + | Reduction.CUMUL -> Reduction.conv_leq_universes full_transparent_state ~evars:(existential_opt_value evd) env (UState.ugraph evd.universes) t u diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 33beca28a..8c9be0edd 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -126,7 +126,7 @@ let whd_betadeltaiota_nolet env t = (* Conversion utility functions *) type 'a conversion_function = env -> 'a -> 'a -> unit -type 'a trans_conversion_function = Names.transparent_state -> 'a conversion_function +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 @@ -616,7 +616,7 @@ let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = { compare = infer_cmp_universes; compare_instances = infer_convert_instances } -let trans_fconv_universes reds cv_pb l2r evars env univs t1 t2 = +let fconv_universes reds cv_pb l2r evars env univs t1 t2 = let b = if cv_pb = CUMUL then leq_constr_univs univs t1 t2 else eq_constr_univs univs t1 t2 @@ -627,38 +627,22 @@ let trans_fconv_universes reds cv_pb l2r evars env univs t1 t2 = () (* Profiling *) -let trans_fconv_universes = +let fconv_universes = if Flags.profile then - let trans_fconv_universes_key = Profile.declare_profile "trans_fconv_universes" in - Profile.profile8 trans_fconv_universes_key trans_fconv_universes - else trans_fconv_universes - -let trans_fconv reds cv_pb l2r evars env = - trans_fconv_universes reds cv_pb l2r evars env (universes env) - -let trans_conv_cmp ?(l2r=false) conv reds = trans_fconv reds conv l2r (fun _->None) -let trans_conv ?(l2r=false) ?(evars=fun _->None) reds = trans_fconv reds CONV l2r evars -let trans_conv_leq ?(l2r=false) ?(evars=fun _->None) reds = trans_fconv reds CUMUL l2r evars - -let trans_conv_universes ?(l2r=false) ?(evars=fun _->None) reds = - trans_fconv_universes reds CONV l2r evars -let trans_conv_leq_universes ?(l2r=false) ?(evars=fun _->None) reds = - trans_fconv_universes reds CUMUL l2r evars - -let fconv = trans_fconv full_transparent_state - -let conv_cmp ?(l2r=false) cv_pb = fconv cv_pb l2r (fun _->None) -let conv ?(l2r=false) ?(evars=fun _->None) = fconv CONV l2r evars -let conv_leq ?(l2r=false) ?(evars=fun _->None) = fconv CUMUL l2r evars - -let conv_leq_vecti ?(l2r=false) ?(evars=fun _->None) env v1 v2 = - Array.fold_left2_i - (fun i _ t1 t2 -> - try conv_leq ~l2r ~evars env t1 t2 - with NotConvertible -> raise (NotConvertibleVect i)) - () - v1 - v2 + let fconv_universes_key = Profile.declare_profile "trans_fconv_universes" in + Profile.profile8 fconv_universes_key fconv_universes + else fconv_universes + +let fconv ?(reds=full_transparent_state) cv_pb l2r evars env = + fconv_universes reds cv_pb l2r evars env (universes env) + +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 generic_conv cv_pb ~l2r evars reds env univs t1 t2 = let (s, _) = diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 7db7e57bb..304046a1d 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -27,7 +27,7 @@ exception NotConvertible exception NotConvertibleVect of int type 'a conversion_function = env -> 'a -> 'a -> unit -type 'a trans_conversion_function = Names.transparent_state -> 'a conversion_function +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 @@ -58,25 +58,14 @@ 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 trans_conv_cmp : ?l2r:bool -> conv_pb -> constr trans_conversion_function -val trans_conv : +val conv : ?l2r:bool -> ?evars:(existential->constr option) -> constr trans_conversion_function -val trans_conv_leq : - ?l2r:bool -> ?evars:(existential->constr option) -> types trans_conversion_function -val trans_conv_universes : +val conv_universes : ?l2r:bool -> ?evars:(existential->constr option) -> constr trans_universe_conversion_function -val trans_conv_leq_universes : +val conv_leq_universes : ?l2r:bool -> ?evars:(existential->constr option) -> types trans_universe_conversion_function -val conv_cmp : ?l2r:bool -> conv_pb -> constr conversion_function -val conv : - ?l2r:bool -> ?evars:(existential->constr option) -> constr conversion_function -val conv_leq : - ?l2r:bool -> ?evars:(existential->constr option) -> types conversion_function -val conv_leq_vecti : - ?l2r:bool -> ?evars:(existential->constr option) -> types array conversion_function - (** These conversion functions are used by module subtyping, which needs to infer universe constraints inside the kernel *) val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) -> diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index d5a93230f..03e7f2642 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1264,8 +1264,8 @@ let test_trans_conversion (f: ?l2r:bool-> ?evars:'a->'b) reds env sigma x y = with Reduction.NotConvertible -> false | e when is_anomaly e -> report_anomaly e -let is_trans_conv reds env sigma = test_trans_conversion Reduction.trans_conv_universes reds env sigma -let is_trans_conv_leq reds env sigma = test_trans_conversion Reduction.trans_conv_leq_universes reds env sigma +let is_trans_conv reds env sigma = test_trans_conversion Reduction.conv_universes reds env sigma +let is_trans_conv_leq reds env sigma = test_trans_conversion Reduction.conv_leq_universes reds env sigma let is_trans_fconv = function Reduction.CONV -> is_trans_conv | Reduction.CUMUL -> is_trans_conv_leq let is_conv = is_trans_conv full_transparent_state @@ -1274,8 +1274,8 @@ let is_fconv = function | Reduction.CONV -> is_conv | Reduction.CUMUL -> is_conv let check_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = let f = match pb with - | Reduction.CONV -> Reduction.trans_conv_universes - | Reduction.CUMUL -> Reduction.trans_conv_leq_universes + | Reduction.CONV -> Reduction.conv_universes + | Reduction.CUMUL -> Reduction.conv_leq_universes in try f ~evars:(safe_evar_value sigma) ts env (Evd.universes sigma) x y; true with Reduction.NotConvertible -> false |