From be11ab322fa73804118738e7a08e9910fdf4600d Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 22 Oct 2016 11:03:13 +0200 Subject: Renamings to avoid confusion deprecating old names reconsider_conv_pbs -> reconsider_unif_constraints consider_remaining_unif_problems -> solve_unif_constraints_with_heuristics --- toplevel/command.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'toplevel/command.ml') diff --git a/toplevel/command.ml b/toplevel/command.ml index 12c387dcf3..7ffe680e5e 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1129,7 +1129,7 @@ let interp_recursive isfix fixl notations = () in (* Instantiate evars and check all are resolved *) - let evd = consider_remaining_unif_problems env_rec !evdref in + let evd = solve_unif_constraints_with_heuristics env_rec !evdref in let evd, nf = nf_evars_and_universes evd in let fixdefs = List.map (Option.map nf) fixdefs in let fixtypes = List.map nf fixtypes in -- cgit v1.2.3 From 25c82d55497db43bf2cd131f10d2ef366758bbe1 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 18 Nov 2016 13:25:05 +0100 Subject: Fix UGraph.check_eq! Universes are kept in normal form w.r.t. equality but not the <= relation, so the previous check worked almost always but was actually too strict! In cases like (max(Set,u) = u) when u is declared >= Set it was failing to find an equality. Applying the KISS principle: u = v <-> u <= v /\ v <= u. Fix invariant breakage that triggered the discovery of the check_eq bug as well. No algebraic universes should appear in a term position (on the left of a colon in a typing judgment), this was not the case when an algebraic universe instantiated an evar that appeared in the term. We force their universe variable status to change in refresh_universes to avoid this. Fix ind sort inference: Use syntactic universe equality for inductive sort inference instead of check_leq (which now correctly takes constraints into account) and simplify code --- toplevel/command.ml | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) (limited to 'toplevel/command.ml') diff --git a/toplevel/command.ml b/toplevel/command.ml index 7ffe680e5e..ed3eac51b6 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -537,11 +537,9 @@ let inductive_levels env evdref poly arities inds = in let duu = Sorts.univ_of_sort du in let evd = - if not (Univ.is_small_univ duu) && Evd.check_eq evd cu duu then - if is_flexible_sort evd duu then - if Evd.check_leq evd Univ.type0_univ duu then - evd - else Evd.set_eq_sort env evd (Prop Null) du + if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then + if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then + Evd.set_eq_sort env evd (Prop Null) du else evd else Evd.set_eq_sort env evd (Type cu) du in -- cgit v1.2.3 From af58f731322527af1d81233beade4c98fbb2d7bd Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 28 Nov 2016 19:05:23 +0100 Subject: Univs: fix bug #5188 Parameter was implemented the wrong way trying to separate the universes of the telescope. --- toplevel/command.ml | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) (limited to 'toplevel/command.ml') diff --git a/toplevel/command.ml b/toplevel/command.ml index 7ffe680e5e..f6172a4b85 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -261,10 +261,7 @@ match local with let interp_assumption evdref env impls bl c = let c = prod_constr_expr c bl in - let ty, impls = interp_type_evars_impls env evdref ~impls c in - let evd, nf = nf_evars_and_universes !evdref in - let ctx = Evd.universe_context_set evd in - ((nf ty, ctx), impls) + interp_type_evars_impls env evdref ~impls c let declare_assumptions idl is_coe k (c,ctx) pl imps impl_is_on nl = let refs, status, _ = @@ -290,25 +287,27 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = else l in let _,l = List.fold_map (fun (env,ienv) (is_coe,(idl,c)) -> - let (t,ctx),imps = interp_assumption evdref env ienv [] c in + let t,imps = interp_assumption evdref env ienv [] c in let env = push_named_context (List.map (fun (_,id) -> LocalAssum (id,t)) idl) env in let ienv = List.fold_right (fun (_,id) ienv -> let impls = compute_internalization_data env Variable t imps in Id.Map.add id impls ienv) idl ienv in - ((env,ienv),((is_coe,idl),t,(ctx,imps)))) + ((env,ienv),((is_coe,idl),t,imps))) (env,empty_internalization_env) l in let evd = solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref) in + let evd = Evd.nf_constraints evd in + let ctx = Evd.universe_context_set evd in let l = List.map (on_pi2 (nf_evar evd)) l in - snd (List.fold_left (fun (subst,status) ((is_coe,idl),t,(ctx,imps)) -> + pi2 (List.fold_left (fun (subst,status,ctx) ((is_coe,idl),t,imps) -> let t = replace_vars subst t in let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) [] imps false nl in let subst' = List.map2 (fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u))) idl refs in - (subst'@subst, status' && status)) ([],true) l) + (subst'@subst, status' && status, Univ.ContextSet.empty)) ([],true,ctx) l) let do_assumptions_bound_univs coe kind nl id pl c = let env = Global.env () in -- cgit v1.2.3 From f492ddb3f9949993ad9072688e9e2cac7cfcbce0 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 2 Dec 2016 16:46:05 +0100 Subject: Comment on universe handling in Parameters --- toplevel/command.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'toplevel/command.ml') diff --git a/toplevel/command.ml b/toplevel/command.ml index f6172a4b85..8b527ebd6f 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -286,6 +286,7 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = l [] else l in + (* We intepret all declarations in the same evar_map, i.e. as a telescope. *) let _,l = List.fold_map (fun (env,ienv) (is_coe,(idl,c)) -> let t,imps = interp_assumption evdref env ienv [] c in let env = @@ -297,6 +298,7 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = (env,empty_internalization_env) l in let evd = solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref) in + (* The universe constraints come from the whole telescope. *) let evd = Evd.nf_constraints evd in let ctx = Evd.universe_context_set evd in let l = List.map (on_pi2 (nf_evar evd)) l in @@ -307,7 +309,9 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = (fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u))) idl refs in - (subst'@subst, status' && status, Univ.ContextSet.empty)) ([],true,ctx) l) + (subst'@subst, status' && status, + (* The universe constraints are declared with the first declaration only. *) + Univ.ContextSet.empty)) ([],true,ctx) l) let do_assumptions_bound_univs coe kind nl id pl c = let env = Global.env () in -- cgit v1.2.3