diff options
| -rw-r--r-- | engine/evd.mli | 2 | ||||
| -rw-r--r-- | engine/uState.ml | 28 | ||||
| -rw-r--r-- | engine/uState.mli | 2 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 78 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 6 |
5 files changed, 63 insertions, 53 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index 76fa69e31..8c3771cd9 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -493,7 +493,7 @@ val empty_evar_universe_context : evar_universe_context val union_evar_universe_context : evar_universe_context -> evar_universe_context -> evar_universe_context val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst -val constrain_variables : Univ.LSet.t -> evar_universe_context -> Univ.constraints +val constrain_variables : Univ.LSet.t -> evar_universe_context -> evar_universe_context val evar_universe_context_of_binders : diff --git a/engine/uState.ml b/engine/uState.ml index 312502491..979a9b086 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -101,16 +101,6 @@ let initial_graph ctx = ctx.uctx_initial_universes let algebraics ctx = ctx.uctx_univ_algebraic -let constrain_variables diff ctx = - Univ.LSet.fold - (fun l cstrs -> - try - match Univ.LMap.find l ctx.uctx_univ_variables with - | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs - | None -> cstrs - with Not_found | Option.IsNone -> cstrs) - diff Univ.Constraint.empty - let add_uctx_names ?loc s l (names, names_rev) = (UNameMap.add s l names, Univ.LMap.add l { uname = Some s; uloc = loc } names_rev) @@ -242,6 +232,24 @@ let add_universe_constraints ctx cstrs = uctx_univ_variables = vars; uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes } +let constrain_variables diff ctx = + let univs, local = ctx.uctx_local in + let univs, vars, local = + Univ.LSet.fold + (fun l (univs, vars, cstrs) -> + try + match Univ.LMap.find l vars with + | Some u -> + (Univ.LSet.add l univs, + Univ.LMap.remove l vars, + Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs) + | None -> (univs, vars, cstrs) + with Not_found | Option.IsNone -> (univs, vars, cstrs)) + diff (univs, ctx.uctx_univ_variables, local) + in + { ctx with uctx_local = (univs, local); uctx_univ_variables = vars } + + let pr_uctx_level uctx = let map, map_rev = uctx.uctx_names in fun l -> diff --git a/engine/uState.mli b/engine/uState.mli index ba0305869..0b67bb71f 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -108,7 +108,7 @@ val is_sort_variable : t -> Sorts.t -> Univ.Level.t option val normalize_variables : t -> Univ.universe_subst * t -val constrain_variables : Univ.LSet.t -> t -> Univ.constraints +val constrain_variables : Univ.LSet.t -> t -> t val abstract_undefined_variables : t -> t diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index e8266f5c8..cd4d1dcf6 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -318,8 +318,7 @@ let get_open_goals () = let constrain_variables init uctx = let levels = Univ.Instance.levels (Univ.UContext.instance init) in - let cstrs = UState.constrain_variables levels uctx in - Univ.ContextSet.add_constraints cstrs (UState.context_set uctx) + UState.constrain_variables levels uctx type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context @@ -332,6 +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 (* 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. *) @@ -355,55 +356,54 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let initunivs = Evd.evar_context_universe_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 - * the body. So we keep the two sets distinct. *) + 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 = Univops.restrict_universe_context ctx used_univs in - (initunivs, typ), ((body, ctx_body), eff) + let ctx_body = UState.restrict ctx used_univs 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 - let initunivs = Univ.UContext.empty in - let ctx = constrain_variables initunivs universes in (* 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 - * for the typ *) + constraints in which we merge the ones for the body and the ones + for the typ. We recheck the declaration after restricting with + the actually used universes. + TODO: check if restrict is really necessary now. *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let ctx = Univops.restrict_universe_context ctx used_univs in - let univs = Univ.ContextSet.to_context ctx in + let ctx = UState.restrict universes used_univs 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 ~pure:true p (make_body t)) else fun t p -> - let initunivs = Evd.evar_context_universe_context initial_euctx in - Future.from_val (initunivs, nf t), + Future.from_val (univctx, nf t), Future.chain ~pure:true p (fun (pt,eff) -> - (pt,constrain_variables initunivs (Future.force univs)),eff) + (* Deferred proof, we already checked the universe declaration with + 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 = Evd.check_univ_decl (Evd.from_ctx bodyunivs) universe_decl in + (pt,Univ.ContextSet.of_context univs),eff) in - let entries = - Future.map2 (fun 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 Entries.Monomorphic_const_entry univs - in - { Entries. - const_entry_body = body; - const_entry_secctx = section_vars; - const_entry_feedback = feedback_id; - const_entry_type = Some typ; - const_entry_inline_code = false; - const_entry_opaque = true; - const_entry_universes = univs; - }) - fpl initial_goals in - let binders = - if not poly || (List.is_empty universe_decl.Misctypes.univdecl_instance && - universe_decl.Misctypes.univdecl_extensible_instance) then None - else - Some (fst (Evd.check_univ_decl (Evd.from_ctx universes) universe_decl)) + 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 Entries.Monomorphic_const_entry univs + in + {Entries. + const_entry_body = body; + const_entry_secctx = section_vars; + const_entry_feedback = feedback_id; + const_entry_type = Some typ; + const_entry_inline_code = false; + const_entry_opaque = true; + const_entry_universes = univs; } in + let entries = Future.map2 entry_fn fpl initial_goals in { id = pid; entries = entries; persistence = strength; universes = (universes, binders) }, fun pr_ending -> CEphemeron.get terminator pr_ending diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index d78cd14f6..793022377 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -510,8 +510,10 @@ let save_proof ?proof = function let decl = Proof_global.get_universe_decl () in let evd = Evd.from_ctx universes in let binders, ctx = Evd.check_univ_decl evd decl in - Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None), - (universes, Some binders)) + let poly = pi2 k in + let binders = if poly then Some binders else None in + Admitted(id,k,(sec_vars, poly, (typ, ctx), None), + (universes, binders)) in Proof_global.apply_terminator (Proof_global.get_terminator ()) pe | Vernacexpr.Proved (is_opaque,idopt) -> |