From ed04b8eb07ca3925af852c30a75c553c134f7d72 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 29 Oct 2018 17:56:10 +0100 Subject: Local universes for opaque polymorphic constants. --- kernel/cooking.ml | 9 ++++++++- kernel/cooking.mli | 1 + kernel/declarations.ml | 1 + kernel/declareops.ml | 11 +++++++++-- kernel/environ.ml | 12 ++++++++++++ kernel/environ.mli | 6 ++++++ kernel/modops.ml | 3 ++- kernel/safe_typing.ml | 2 +- kernel/term_typing.ml | 27 ++++++++++++++++----------- kernel/uGraph.ml | 2 ++ kernel/uGraph.mli | 3 +++ 11 files changed, 61 insertions(+), 16 deletions(-) (limited to 'kernel') diff --git a/kernel/cooking.ml b/kernel/cooking.ml index b39aed01e8..f4b4834d98 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -158,6 +158,7 @@ type result = { cook_body : constant_def; cook_type : types; cook_universes : constant_universes; + cook_private_univs : Univ.ContextSet.t option; cook_inline : inline; cook_context : Constr.named_context option; } @@ -204,7 +205,8 @@ let lift_univs cb subst auctx0 = else let ainst = Univ.make_abstract_instance auctx in let subst = Instance.append subst ainst in - let auctx' = Univ.subst_univs_level_abstract_universe_context (Univ.make_instance_subst subst) auctx in + let substf = Univ.make_instance_subst subst in + let auctx' = Univ.subst_univs_level_abstract_universe_context substf auctx in subst, (Polymorphic_const (AUContext.union auctx0 auctx')) let cook_constant ~hcons { from = cb; info } = @@ -229,10 +231,15 @@ let cook_constant ~hcons { from = cb; info } = hyps) hyps0 ~init:cb.const_hyps in let typ = abstract_constant_type (expmod cb.const_type) hyps in + let private_univs = Option.map (on_snd (Univ.subst_univs_level_constraints + (Univ.make_instance_subst usubst))) + cb.const_private_poly_univs + in { cook_body = body; cook_type = typ; cook_universes = univs; + cook_private_univs = private_univs; cook_inline = cb.const_inline_code; cook_context = Some const_hyps; } diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 6ebe691b83..7ff4b657d3 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -21,6 +21,7 @@ type result = { cook_body : constant_def; cook_type : types; cook_universes : constant_universes; + cook_private_univs : Univ.ContextSet.t option; cook_inline : inline; cook_context : Constr.named_context option; } diff --git a/kernel/declarations.ml b/kernel/declarations.ml index c1b38b4156..68ccd933e7 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -78,6 +78,7 @@ type constant_body = { const_type : types; const_body_code : Cemitcodes.to_patch_substituted option; const_universes : constant_universes; + const_private_poly_univs : Univ.ContextSet.t option; const_inline_code : bool; const_typing_flags : typing_flags; (** The typing options which were used for diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 3ed599c538..90638be3ec 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -101,6 +101,7 @@ let subst_const_body sub cb = const_body_code = Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; const_universes = cb.const_universes; + const_private_poly_univs = cb.const_private_poly_univs; const_inline_code = cb.const_inline_code; const_typing_flags = cb.const_typing_flags } @@ -126,14 +127,20 @@ let hcons_const_universes cbu = match cbu with | Monomorphic_const ctx -> Monomorphic_const (Univ.hcons_universe_context_set ctx) - | Polymorphic_const ctx -> + | Polymorphic_const ctx -> Polymorphic_const (Univ.hcons_abstract_universe_context ctx) +let hcons_const_private_univs = function + | None -> None + | Some univs -> Some (Univ.hcons_universe_context_set univs) + let hcons_const_body cb = { cb with const_body = hcons_const_def cb.const_body; const_type = Constr.hcons cb.const_type; - const_universes = hcons_const_universes cb.const_universes } + const_universes = hcons_const_universes cb.const_universes; + const_private_poly_univs = hcons_const_private_univs cb.const_private_poly_univs; + } (** {6 Inductive types } *) diff --git a/kernel/environ.ml b/kernel/environ.ml index 019c0a6819..a6bc579cf7 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -380,6 +380,18 @@ let add_universes_set strict ctx g = let push_context_set ?(strict=false) ctx env = map_universes (add_universes_set strict ctx) env +let push_subgraph (levels,csts) env = + let add_subgraph g = + let newg = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g) levels g in + let newg = UGraph.merge_constraints csts newg in + (if not (Univ.Constraint.is_empty csts) then + let restricted = UGraph.constraints_for ~kept:(UGraph.domain g) newg in + (if not (UGraph.check_constraints restricted g) then + CErrors.anomaly Pp.(str "Local constraints imply new transitive constraints."))); + newg + in + map_universes add_subgraph env + let set_engagement c env = (* Unsafe *) { env with env_stratification = { env.env_stratification with env_engagement = c } } diff --git a/kernel/environ.mli b/kernel/environ.mli index c285f907fc..dd0df7d3d6 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -268,6 +268,12 @@ val push_context : ?strict:bool -> Univ.UContext.t -> env -> env val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env val push_constraints_to_env : 'a Univ.constrained -> env -> env +val push_subgraph : Univ.ContextSet.t -> env -> env +(** [push_subgraph univs env] adds the universes and constraints in + [univs] to [env] as [push_context_set ~strict:false univs env], and + also checks that they do not imply new transitive constraints + between pre-existing universes in [env]. *) + val set_engagement : engagement -> env -> env val set_typing_flags : typing_flags -> env -> env diff --git a/kernel/modops.ml b/kernel/modops.ml index 0dde1c7e75..f43dbd88f9 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -338,7 +338,8 @@ let strengthen_const mp_from l cb resolver = | Polymorphic_const ctx -> Univ.make_abstract_instance ctx in { cb with - const_body = Def (Mod_subst.from_val (mkConstU (con,u))); + const_body = Def (Mod_subst.from_val (mkConstU (con,u))); + const_private_poly_univs = None; const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias con)) } let rec strengthen_mod mp_from mp_to mb = diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 2464df799e..98a7014bee 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -599,7 +599,7 @@ let inline_side_effects env body side_eff = let subst = Cmap_env.add c (Inr var) subst in let ctx = Univ.ContextSet.union ctx univs in (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args) - | Polymorphic_const _auctx -> + | Polymorphic_const _ -> (** Inline the term to emulate universe polymorphism *) let subst = Cmap_env.add c (Inl b) subst in (subst, var, ctx, args) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 35fa871b4e..f9fdbdd68e 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -88,6 +88,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = Cooking.cook_body = Undef nl; cook_type = t; cook_universes = univs; + cook_private_univs = None; cook_inline = false; cook_context = ctx; } @@ -130,6 +131,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = Cooking.cook_body = def; cook_type = typ; cook_universes = Monomorphic_const univs; + cook_private_univs = None; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; } @@ -145,24 +147,25 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let body, ctx', _ = handle env body side_eff in body, Univ.ContextSet.union ctx ctx' in - let env, usubst, univs = match c.const_entry_universes with + let env, usubst, univs, private_univs = match c.const_entry_universes with | Monomorphic_const_entry univs -> let ctx = Univ.ContextSet.union univs ctx in let env = push_context_set ~strict:true ctx env in - env, Univ.empty_level_subst, Monomorphic_const ctx + env, Univ.empty_level_subst, Monomorphic_const ctx, None | Polymorphic_const_entry (nas, uctx) -> - (** Ensure not to generate internal constraints in polymorphic mode. - The only way for this to happen would be that either the body - contained deferred universes, or that it contains monomorphic - side-effects. The first property is ruled out by upper layers, - and the second one is ensured by the fact we currently - unconditionally export side-effects from polymorphic definitions, - i.e. [trust] is always [Pure]. *) - let () = assert (Univ.ContextSet.is_empty ctx) in + (** [ctx] must contain local universes, such that it has no impact + on the rest of the graph (up to transitivity). *) let env = push_context ~strict:false uctx env in let sbst, auctx = Univ.abstract_universes nas uctx in let sbst = Univ.make_instance_subst sbst in - env, sbst, Polymorphic_const auctx + let env, local = + if opaque then + push_subgraph ctx env, Some (on_snd (Univ.subst_univs_level_constraints sbst) ctx) + else + if Univ.ContextSet.is_empty ctx then env, None + else CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.") + in + env, sbst, Polymorphic_const auctx, local in let j = infer env body in let typ = match typ with @@ -183,6 +186,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = Cooking.cook_body = def; cook_type = typ; cook_universes = univs; + cook_private_univs = private_univs; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; } @@ -277,6 +281,7 @@ let build_constant_declaration _kn env result = const_type = typ; const_body_code = tps; const_universes = univs; + const_private_poly_univs = result.cook_private_univs; const_inline_code = result.cook_inline; const_typing_flags = Environ.typing_flags env } diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 9083156745..fe07a1c90e 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -866,6 +866,8 @@ let constraints_for ~kept g = arc.ltle csts) kept csts +let domain g = LMap.domain g.entries + (** [sort_universes g] builds a totally ordered universe graph. The output graph should imply the input graph (and the implication will be strict most of the time), but is not necessarily minimal. diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index a2cc5b3116..a389b35993 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -79,6 +79,9 @@ val constraints_of_universes : t -> Constraint.t * LSet.t list eg if [g] is [a <= b <= c] then [constraints_for ~kept:{a, c} g] is [a <= c]. *) val constraints_for : kept:LSet.t -> t -> Constraint.t +val domain : t -> LSet.t +(** Known universes *) + val check_subtype : AUContext.t check_function (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of [ctx1]. *) -- cgit v1.2.3