From a5feb9687819c5e7ef0db6e7b74d0e236a296674 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 21:01:57 +0200 Subject: Separate checking univ_decls and obtaining universe binder names. --- proofs/proof_global.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'proofs') diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index fdc9a236bf..9faff32112 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -331,8 +331,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let initial_euctx = Proof.initial_euctx proof in let fpl, univs = Future.split2 fpl in let universes = if poly || now then Future.force univs else initial_euctx in - let binders, univctx = Evd.check_univ_decl (Evd.from_ctx universes) universe_decl in - let binders = if poly then Some binders else None in + let univctx = Evd.check_univ_decl (Evd.from_ctx universes) universe_decl in + let binders = if poly then Some (UState.universe_binders universes) else None in (* Because of dependent subgoals at the beginning of proofs, we could have existential variables in the initial types of goals, we need to normalise them for the kernel. *) @@ -360,7 +360,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now the body. So we keep the two sets distinct. *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in let ctx_body = UState.restrict ctx used_univs in - let _, univs = Evd.check_univ_decl (Evd.from_ctx ctx_body) universe_decl in + let univs = Evd.check_univ_decl (Evd.from_ctx ctx_body) universe_decl in (initunivs, typ), ((body, Univ.ContextSet.of_context univs), eff) else (* Since the proof is computed now, we can simply have 1 set of @@ -370,7 +370,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now TODO: check if restrict is really necessary now. *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in let ctx = UState.restrict universes used_univs in - let _, univs = Evd.check_univ_decl (Evd.from_ctx ctx) universe_decl in + let univs = Evd.check_univ_decl (Evd.from_ctx ctx) universe_decl in (univs, typ), ((body, Univ.ContextSet.empty), eff) in fun t p -> Future.split2 (Future.chain p (make_body t)) @@ -383,7 +383,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now the declaration as well. If the declaration is non-extensible, this will prevent the body from adding universes and constraints. *) let bodyunivs = constrain_variables univctx (Future.force univs) in - let _, univs = Evd.check_univ_decl (Evd.from_ctx bodyunivs) universe_decl in + let univs = Evd.check_univ_decl (Evd.from_ctx bodyunivs) universe_decl in (pt,Univ.ContextSet.of_context univs),eff) in let entry_fn p (_, t) = -- cgit v1.2.3 From 60770e86f4ec925fce52ad3565a92beb98d253c1 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 22:21:46 +0200 Subject: Stop exposing UState.universe_context and its Evd wrapper. We can enforce properties through check_univ_decl, or get an arbitrary ordered context with UState.context / Evd.to_universe_context (the later being a new wrapper of the former). --- proofs/proof_global.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs') diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 9faff32112..ea04081693 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -353,7 +353,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let used_univs_typ = Univops.universes_of_constr typ in if keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff) then - let initunivs = Evd.evar_context_universe_context initial_euctx in + let initunivs = UState.context initial_euctx in let ctx = constrain_variables initunivs universes in (* For vi2vo compilation proofs are computed now but we need to complement the univ constraints of the typ with the ones of -- cgit v1.2.3 From 58c0784745f8b2ba7523f246c4611d780c9f3f70 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 18 Sep 2017 14:50:07 +0200 Subject: When declaring constants/inductives use ContextSet if monomorphic. Also use constant_universes_entry instead of a bool flag to indicate polymorphism in ParameterEntry. There are a few places where we convert back to ContextSet because check_univ_decl returns a UContext, this could be improved. --- proofs/proof_global.ml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) (limited to 'proofs') diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index ea04081693..905173efca 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -331,7 +331,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let initial_euctx = Proof.initial_euctx proof in let fpl, univs = Future.split2 fpl in let universes = if poly || now then Future.force univs else initial_euctx in - let univctx = Evd.check_univ_decl (Evd.from_ctx universes) universe_decl in + let univctx = UState.check_univ_decl universes universe_decl in let binders = if poly then Some (UState.universe_binders universes) else None in (* Because of dependent subgoals at the beginning of proofs, we could have existential variables in the initial types of goals, we need to @@ -360,7 +360,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now the body. So we keep the two sets distinct. *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in let ctx_body = UState.restrict ctx used_univs in - let univs = Evd.check_univ_decl (Evd.from_ctx ctx_body) universe_decl in + let univs = UState.check_univ_decl ctx_body universe_decl in (initunivs, typ), ((body, Univ.ContextSet.of_context univs), eff) else (* Since the proof is computed now, we can simply have 1 set of @@ -370,7 +370,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now TODO: check if restrict is really necessary now. *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in let ctx = UState.restrict universes used_univs in - let univs = Evd.check_univ_decl (Evd.from_ctx ctx) universe_decl in + let univs = UState.check_univ_decl ctx universe_decl in (univs, typ), ((body, Univ.ContextSet.empty), eff) in fun t p -> Future.split2 (Future.chain p (make_body t)) @@ -383,7 +383,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now the declaration as well. If the declaration is non-extensible, this will prevent the body from adding universes and constraints. *) let bodyunivs = constrain_variables univctx (Future.force univs) in - let univs = Evd.check_univ_decl (Evd.from_ctx bodyunivs) universe_decl in + let univs = UState.check_univ_decl bodyunivs universe_decl in (pt,Univ.ContextSet.of_context univs),eff) in let entry_fn p (_, t) = @@ -392,7 +392,9 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let univs, typ = Future.force univstyp in let univs = if poly then Entries.Polymorphic_const_entry univs - else Entries.Monomorphic_const_entry univs + else + (* FIXME be smarter about the unnecessary context linearisation in make_body *) + Entries.Monomorphic_const_entry (Univ.ContextSet.of_context univs) in {Entries. const_entry_body = body; -- cgit v1.2.3 From 34d85e1e899f8a045659ccc53bfd6a1f5104130b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 18 Sep 2017 17:22:24 +0200 Subject: Use Entries.constant_universes_entry more. This reduces conversions between ContextSet/UContext and encodes whether we are polymorphic by which constructor we use rather than using some boolean. --- proofs/proof_global.ml | 31 ++++++++++++------------------- 1 file changed, 12 insertions(+), 19 deletions(-) (limited to 'proofs') diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 905173efca..bfd64e21b0 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -316,10 +316,6 @@ let get_open_goals () = (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) + List.length shelf -let constrain_variables init uctx = - let levels = Univ.Instance.levels (Univ.UContext.instance init) in - UState.constrain_variables levels uctx - type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t let close_proof ~keep_body_ucst_separate ?feedback_id ~now @@ -329,9 +325,12 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let poly = pi2 strength (* Polymorphic *) in let initial_goals = Proof.initial_goals proof in let initial_euctx = Proof.initial_euctx proof in + let constrain_variables ctx = + UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx + in let fpl, univs = Future.split2 fpl in let universes = if poly || now then Future.force univs else initial_euctx in - let univctx = UState.check_univ_decl universes universe_decl in + let univctx = UState.check_univ_decl ~poly universes universe_decl in let binders = if poly then Some (UState.universe_binders universes) else None in (* Because of dependent subgoals at the beginning of proofs, we could have existential variables in the initial types of goals, we need to @@ -353,15 +352,15 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let used_univs_typ = Univops.universes_of_constr typ in if keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff) then - let initunivs = UState.context initial_euctx in - let ctx = constrain_variables initunivs universes in + let initunivs = UState.const_univ_entry ~poly initial_euctx in + let ctx = constrain_variables universes in (* For vi2vo compilation proofs are computed now but we need to complement the univ constraints of the typ with the ones of the body. So we keep the two sets distinct. *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in let ctx_body = UState.restrict ctx used_univs in - let univs = UState.check_univ_decl ctx_body universe_decl in - (initunivs, typ), ((body, Univ.ContextSet.of_context univs), eff) + let univs = UState.check_mono_univ_decl ctx_body universe_decl in + (initunivs, typ), ((body, univs), eff) else (* Since the proof is computed now, we can simply have 1 set of constraints in which we merge the ones for the body and the ones @@ -370,7 +369,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now TODO: check if restrict is really necessary now. *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in let ctx = UState.restrict universes used_univs in - let univs = UState.check_univ_decl ctx universe_decl in + let univs = UState.check_univ_decl ~poly ctx universe_decl in (univs, typ), ((body, Univ.ContextSet.empty), eff) in fun t p -> Future.split2 (Future.chain p (make_body t)) @@ -382,20 +381,14 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now the initial universes, ensure that the final universes respect the declaration as well. If the declaration is non-extensible, this will prevent the body from adding universes and constraints. *) - let bodyunivs = constrain_variables univctx (Future.force univs) in - let univs = UState.check_univ_decl bodyunivs universe_decl in - (pt,Univ.ContextSet.of_context univs),eff) + let bodyunivs = constrain_variables (Future.force univs) in + let univs = UState.check_mono_univ_decl bodyunivs universe_decl in + (pt,univs),eff) in let entry_fn p (_, t) = let t = EConstr.Unsafe.to_constr t in let univstyp, body = make_body t p in let univs, typ = Future.force univstyp in - let univs = - if poly then Entries.Polymorphic_const_entry univs - else - (* FIXME be smarter about the unnecessary context linearisation in make_body *) - Entries.Monomorphic_const_entry (Univ.ContextSet.of_context univs) - in {Entries. const_entry_body = body; const_entry_secctx = section_vars; -- cgit v1.2.3 From 00860c1b2209159fb2b6780004c8c8ea16b3cb3a Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 18 Sep 2017 20:39:08 +0200 Subject: In close_proof only check univ decls with the restricted context. --- proofs/proof_global.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'proofs') diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index bfd64e21b0..cf5dc95fe9 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -330,7 +330,6 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now in let fpl, univs = Future.split2 fpl in let universes = if poly || now then Future.force univs else initial_euctx in - let univctx = UState.check_univ_decl ~poly universes universe_decl in let binders = if poly then Some (UState.universe_binders universes) else None in (* Because of dependent subgoals at the beginning of proofs, we could have existential variables in the initial types of goals, we need to @@ -375,6 +374,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fun t p -> Future.split2 (Future.chain p (make_body t)) else fun t p -> + (* Already checked the univ_decl for the type universes when starting the proof. *) + let univctx = Entries.Monomorphic_const_entry (UState.context_set universes) in Future.from_val (univctx, nf t), Future.chain p (fun (pt,eff) -> (* Deferred proof, we already checked the universe declaration with -- cgit v1.2.3 From c93d5094bff73498ec8fc02837e16cc5ce9103b6 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 7 Sep 2017 16:56:34 +0200 Subject: Make restrict_universe_context stronger. This fixes BZ#5717. Also add a test and fix a changed test. --- proofs/proof_global.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'proofs') diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index cf5dc95fe9..aa5621770c 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -346,9 +346,14 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now if not (keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff)) then nf t else t - in + in let used_univs_body = Univops.universes_of_constr body in let used_univs_typ = Univops.universes_of_constr typ in + (* Universes for private constants are relevant to the body *) + let used_univs_body = + List.fold_left (fun acc (us,_) -> Univ.LSet.union acc us) + used_univs_body (Safe_typing.universes_of_private eff) + in if keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff) then let initunivs = UState.const_univ_entry ~poly initial_euctx in -- cgit v1.2.3