From 739d8e50b3681491bd82b516dbbba892ac5b424b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 2 Nov 2015 13:48:53 -0500 Subject: Refresh rigid universes as well, and in 8.4 compatibility mode, make them rigid to disallow minimization. --- pretyping/evarsolve.ml | 18 +++++++++++------- pretyping/evarutil.ml | 6 ++++-- 2 files changed, 15 insertions(+), 9 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index f06207c3b9..3c3720388f 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -42,11 +42,15 @@ let get_polymorphic_positions f = templ.template_param_levels) | _ -> assert false -(** - forall A (l : list A) -> typeof A = Type i <= Datatypes.j -> i not refreshed - hd ?A (l : list t) -> A = t +let default_universe_status u = + if Flags.version_less_or_equal Flags.V8_4 then univ_rigid + else u + +let refresh_level evd s = + match Evd.is_sort_variable evd s with + | None -> true + | Some l -> not (Evd.is_flexible_level evd l) -*) let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = let evdref = ref evd in let modified = ref false in @@ -54,10 +58,10 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = match kind_of_term t with | Sort (Type u as s) when (match Univ.universe_level u with - | None -> true - | Some l -> not onlyalg && Option.is_empty (Evd.is_sort_variable evd s)) -> + | None -> true + | Some l -> not onlyalg && refresh_level evd s) -> let status = if inferred then Evd.univ_flexible_alg else Evd.univ_flexible in - let s' = evd_comb0 (new_sort_variable status) evdref in + let s' = evd_comb0 (new_sort_variable (default_universe_status status)) evdref in let evd = if dir then set_leq_sort env !evdref s' s else set_leq_sort env !evdref s s' diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index d3d6901b66..b27803bd05 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -715,7 +715,8 @@ let define_pure_evar_as_product evd evk = let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in let concl = whd_betadeltaiota evenv evd evi.evar_concl in let s = destSort concl in - let evd1,(dom,u1) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in + let evd1,(dom,u1) = + new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in let evd2,rng = let newenv = push_named (id, None, dom) evenv in let src = evar_source evk evd1 in @@ -724,8 +725,9 @@ let define_pure_evar_as_product evd evk = (* Impredicative product, conclusion must fall in [Prop]. *) new_evar newenv evd1 concl ~src ~filter else + let status = univ_flexible_alg in let evd3, (rng, srng) = - new_type_evar newenv evd1 univ_flexible_alg ~src ~filter in + new_type_evar newenv evd1 status ~src ~filter in let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) s in evd3, rng -- cgit v1.2.3 From c920b420a27bd561967e316dcaca41d5e019a7b8 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 2 Nov 2015 14:41:17 -0500 Subject: Fix bug #4151: discrepancy between exact and eexact/eassumption. --- pretyping/evd.ml | 10 ++-------- pretyping/evd.mli | 9 +++------ 2 files changed, 5 insertions(+), 14 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evd.ml b/pretyping/evd.ml index db6b366b75..82c068be07 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1369,7 +1369,7 @@ let update_sigma_env evd env = (* Conversion w.r.t. an evar map and its local universes. *) -let conversion_gen env evd pb t u = +let test_conversion_gen env evd pb t u = match pb with | Reduction.CONV -> Reduction.trans_conv_universes @@ -1379,14 +1379,8 @@ let conversion_gen env evd pb t u = full_transparent_state ~evars:(existential_opt_value evd) env evd.universes.uctx_universes t u -(* let conversion_gen_key = Profile.declare_profile "conversion_gen" *) -(* let conversion_gen = Profile.profile5 conversion_gen_key conversion_gen *) - -let conversion env d pb t u = - conversion_gen env d pb t u; d - let test_conversion env d pb t u = - try conversion_gen env d pb t u; true + try test_conversion_gen env d pb t u; true with _ -> false let eq_constr_univs evd t u = diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 671d62021a..5c508419a4 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -573,14 +573,11 @@ val fresh_global : ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> Globnames.global_reference -> evar_map * constr (******************************************************************** - Conversion w.r.t. an evar map: might generate universe unifications - that are kept in the evarmap. - Raises [NotConvertible]. *) - -val conversion : env -> evar_map -> conv_pb -> constr -> constr -> evar_map + Conversion w.r.t. an evar map, not unifying universes. See + [Reductionops.infer_conv] for conversion up-to universes. *) val test_conversion : env -> evar_map -> conv_pb -> constr -> constr -> bool -(** This one forgets about the assignemts of universes. *) +(** WARNING: This does not allow unification of universes *) val eq_constr_univs : evar_map -> constr -> constr -> evar_map * bool (** Syntactic equality up to universes, recording the associated constraints *) -- cgit v1.2.3 From 95a4fcf8cd36e29034e886682ed3a6e2914ce04f Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 4 Nov 2015 12:52:35 -0500 Subject: Univs: compatibility with 8.4. When refreshing a type variable, always use a rigid universe to force the most general universe constraint, as in 8.4. --- pretyping/evarsolve.ml | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 3c3720388f..ee666e1154 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -42,10 +42,6 @@ let get_polymorphic_positions f = templ.template_param_levels) | _ -> assert false -let default_universe_status u = - if Flags.version_less_or_equal Flags.V8_4 then univ_rigid - else u - let refresh_level evd s = match Evd.is_sort_variable evd s with | None -> true @@ -60,8 +56,7 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = (match Univ.universe_level u with | None -> true | Some l -> not onlyalg && refresh_level evd s) -> - let status = if inferred then Evd.univ_flexible_alg else Evd.univ_flexible in - let s' = evd_comb0 (new_sort_variable (default_universe_status status)) evdref in + let s' = evd_comb0 (new_sort_variable univ_rigid) evdref in let evd = if dir then set_leq_sort env !evdref s' s else set_leq_sort env !evdref s s' -- cgit v1.2.3 From 209faf81c432c39d4537f8b1dc5c9947d4349d30 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 4 Nov 2015 14:35:02 -0500 Subject: Univs: update refman, better printers for universe contexts. --- pretyping/evd.ml | 5 ++--- pretyping/pretyping.ml | 2 +- 2 files changed, 3 insertions(+), 4 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 82c068be07..4a9466f4f3 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -280,9 +280,8 @@ type evar_universe_context = uctx_univ_variables : Universes.universe_opt_subst; (** The local universes that are unification variables *) uctx_univ_algebraic : Univ.universe_set; - (** The subset of unification variables that - can be instantiated with algebraic universes as they appear in types - and universe instances only. *) + (** The subset of unification variables that can be instantiated with + algebraic universes as they appear in inferred types only. *) uctx_universes : Univ.universes; (** The current graph extended with the local constraints *) uctx_initial_universes : Univ.universes; (** The graph at the creation of the evar_map *) } diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index d484df69c1..d354a6c3c4 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -118,7 +118,7 @@ let _ = { optsync = true; optdepr = false; optname = "minimization to Set"; - optkey = ["Universe";"set";"Minimization"]; + optkey = ["Universe";"Minimization";"ToSet"]; optread = Universes.is_set_minimization; optwrite = (:=) Universes.set_minimization }) -- cgit v1.2.3 From 7c102bb3a3798a234701fdc28a8e8ec28ee2549c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 4 Nov 2015 18:09:02 -0500 Subject: Univs: missing checks in evarsolve with candidates and missing a whd_evar in refresh_universes. --- pretyping/evarsolve.ml | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index ee666e1154..35bc1de593 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -50,24 +50,24 @@ let refresh_level evd s = let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = let evdref = ref evd in let modified = ref false in - let rec refresh dir t = + let rec refresh status dir t = match kind_of_term t with | Sort (Type u as s) when (match Univ.universe_level u with | None -> true | Some l -> not onlyalg && refresh_level evd s) -> - let s' = evd_comb0 (new_sort_variable univ_rigid) evdref in + let s' = evd_comb0 (new_sort_variable status) evdref in let evd = if dir then set_leq_sort env !evdref s' s else set_leq_sort env !evdref s s' in modified := true; evdref := evd; mkSort s' | Prod (na,u,v) -> - mkProd (na,u,refresh dir v) + mkProd (na,u,refresh status dir v) | _ -> t (** Refresh the types of evars under template polymorphic references *) and refresh_term_evars onevars top t = - match kind_of_term t with + match kind_of_term (whd_evar !evdref t) with | App (f, args) when is_template_polymorphic env f -> let pos = get_polymorphic_positions f in refresh_polymorphic_positions args pos @@ -76,7 +76,7 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = Array.iter (refresh_term_evars onevars false) args | Evar (ev, a) when onevars -> let evi = Evd.find !evdref ev in - let ty' = refresh true evi.evar_concl in + let ty' = refresh univ_flexible true evi.evar_concl in if !modified then evdref := Evd.add !evdref ev {evi with evar_concl = ty'} else () @@ -98,7 +98,7 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = if isArity t then (match pbty with | None -> t - | Some dir -> refresh dir t) + | Some dir -> refresh univ_rigid dir t) else (refresh_term_evars false true t; t) in if !modified then !evdref, t' else !evdref, t @@ -1274,7 +1274,10 @@ let solve_candidates conv_algo env evd (evk,argsv) rhs = | [c,evd] -> (* solve_candidates might have been called recursively in the mean *) (* time and the evar been solved by the filtering process *) - if Evd.is_undefined evd evk then Evd.define evk c evd else evd + if Evd.is_undefined evd evk then + let evd' = Evd.define evk c evd in + check_evar_instance evd' evk c conv_algo + else evd | l when List.length l < List.length l' -> let candidates = List.map fst l in restrict_evar evd evk None (UpdateWith candidates) -- cgit v1.2.3