diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-05 20:22:14 +0100 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-06 13:23:31 +0100 |
commit | 5b8b02cd060097c3c980b0498257c30eda1ad207 (patch) | |
tree | ff0e51230d3518bb2db523187644cd73d40aecf5 /engine | |
parent | 2c5e81e3bc6ec17d253aeedd1b2bf4ccd3b81933 (diff) |
Fix #6323: stronger restrict universe context vs abstract.
In the test we do [let X : Type@{i} := Set in ...] with Set
abstracted. The constraint [Set < i] was lost in the abstract.
Universes of a monomorphic reference [c] are considered to appear in
the term [c].
Diffstat (limited to 'engine')
-rw-r--r-- | engine/eConstr.ml | 19 | ||||
-rw-r--r-- | engine/eConstr.mli | 2 | ||||
-rw-r--r-- | engine/uState.ml | 19 | ||||
-rw-r--r-- | engine/uState.mli | 2 | ||||
-rw-r--r-- | engine/univops.ml | 21 | ||||
-rw-r--r-- | engine/univops.mli | 5 |
6 files changed, 56 insertions, 12 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index ea098902a..d303038c5 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -645,12 +645,25 @@ let eq_constr_universes_proj env sigma m n = let res = eq_constr' (unsafe_to_constr m) (unsafe_to_constr n) in if res then Some !cstrs else None -let universes_of_constr sigma c = +let universes_of_constr env sigma c = let open Univ in + let open Declarations in let rec aux s c = match kind sigma c with - | Const (_, u) | Ind (_, u) | Construct (_, u) -> - LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s + | Const (c, u) -> + begin match (Environ.lookup_constant c env).const_universes with + | Polymorphic_const _ -> + LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s + | Monomorphic_const (univs, _) -> + LSet.union s univs + end + | Ind ((mind,_), u) | Construct (((mind,_),_), u) -> + begin match (Environ.lookup_mind mind env).mind_universes with + | Cumulative_ind _ | Polymorphic_ind _ -> + LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s + | Monomorphic_ind (univs,_) -> + LSet.union s univs + end | Sort u -> let sort = ESorts.kind sigma u in if Sorts.is_small sort then s diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 3e6a13f70..651ccbb10 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -203,7 +203,7 @@ val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a (** Gather the universes transitively used in the term, including in the type of evars appearing in it. *) -val universes_of_constr : Evd.evar_map -> t -> Univ.LSet.t +val universes_of_constr : Environ.env -> Evd.evar_map -> t -> Univ.LSet.t (** {6 Substitutions} *) diff --git a/engine/uState.ml b/engine/uState.ml index 511d55328..57e61bb82 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -22,6 +22,7 @@ type uinfo = { type t = { uctx_names : Universes.universe_binders * uinfo Univ.LMap.t; uctx_local : Univ.ContextSet.t; (** The local context of variables *) + uctx_seff_univs : Univ.LSet.t; (** Local universes used through private constants *) uctx_univ_variables : Universes.universe_opt_subst; (** The local universes that are unification variables *) uctx_univ_algebraic : Univ.LSet.t; @@ -34,6 +35,7 @@ type t = let empty = { uctx_names = UNameMap.empty, Univ.LMap.empty; uctx_local = Univ.ContextSet.empty; + uctx_seff_univs = Univ.LSet.empty; uctx_univ_variables = Univ.LMap.empty; uctx_univ_algebraic = Univ.LSet.empty; uctx_universes = UGraph.initial_universes; @@ -60,6 +62,7 @@ let union ctx ctx' = else if is_empty ctx' then ctx else let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in + let seff = Univ.LSet.union ctx.uctx_seff_univs ctx'.uctx_seff_univs in let names = uname_union (fst ctx.uctx_names) (fst ctx'.uctx_names) in let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local) (Univ.ContextSet.levels ctx.uctx_local) in @@ -70,6 +73,7 @@ let union ctx ctx' = let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in { uctx_names = (names, names_rev); uctx_local = local; + uctx_seff_univs = seff; uctx_univ_variables = Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables; uctx_univ_algebraic = @@ -365,12 +369,21 @@ let check_univ_decl ~poly uctx decl = ctx let restrict ctx vars = + let vars = Univ.LSet.union vars ctx.uctx_seff_univs in let vars = Names.Id.Map.fold (fun na l vars -> Univ.LSet.add l vars) (fst ctx.uctx_names) vars in let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in { ctx with uctx_local = uctx' } +let demote_seff_univs entry uctx = + let open Entries in + match entry.const_entry_universes with + | Polymorphic_const_entry _ -> uctx + | Monomorphic_const_entry (univs, _) -> + let seff = Univ.LSet.union uctx.uctx_seff_univs univs in + { uctx with uctx_seff_univs = seff } + type rigid = | UnivRigid | UnivFlexible of bool (** Is substitution by an algebraic ok? *) @@ -552,7 +565,8 @@ let refresh_undefined_univ_variables uctx = let initial = declare uctx.uctx_initial_universes in let univs = declare UGraph.initial_universes in let uctx' = {uctx_names = uctx.uctx_names; - uctx_local = ctx'; + uctx_local = ctx'; + uctx_seff_univs = uctx.uctx_seff_univs; uctx_univ_variables = vars; uctx_univ_algebraic = alg; uctx_universes = univs; uctx_initial_universes = initial } in @@ -569,7 +583,8 @@ let normalize uctx = Universes.refresh_constraints uctx.uctx_initial_universes us' in { uctx_names = uctx.uctx_names; - uctx_local = us'; + uctx_local = us'; + uctx_seff_univs = uctx.uctx_seff_univs; (* not sure about this *) uctx_univ_variables = vars'; uctx_univ_algebraic = algs'; uctx_universes = universes; diff --git a/engine/uState.mli b/engine/uState.mli index 2c39e85f7..5dfe9a22d 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -87,6 +87,8 @@ val universe_of_name : t -> Id.t -> Univ.Level.t val restrict : t -> Univ.LSet.t -> t +val demote_seff_univs : Safe_typing.private_constants Entries.definition_entry -> t -> t + type rigid = | UnivRigid | UnivFlexible of bool (** Is substitution by an algebraic ok? *) diff --git a/engine/univops.ml b/engine/univops.ml index 9a9ae12ca..df25d8725 100644 --- a/engine/univops.ml +++ b/engine/univops.ml @@ -9,12 +9,25 @@ open Univ open Constr -let universes_of_constr c = +let universes_of_constr env c = + let open Declarations in let rec aux s c = match kind c with - | Const (_, u) | Ind (_, u) | Construct (_, u) -> - LSet.fold LSet.add (Instance.levels u) s - | Sort u when not (Sorts.is_small u) -> + | Const (c, u) -> + begin match (Environ.lookup_constant c env).const_universes with + | Polymorphic_const _ -> + LSet.fold LSet.add (Instance.levels u) s + | Monomorphic_const (univs, _) -> + LSet.union s univs + end + | Ind ((mind,_), u) | Construct (((mind,_),_), u) -> + begin match (Environ.lookup_mind mind env).mind_universes with + | Cumulative_ind _ | Polymorphic_ind _ -> + LSet.fold LSet.add (Instance.levels u) s + | Monomorphic_ind (univs,_) -> + LSet.union s univs + end + | Sort u when not (Sorts.is_small u) -> let u = Sorts.univ_of_sort u in LSet.fold LSet.add (Universe.levels u) s | _ -> Constr.fold aux s c diff --git a/engine/univops.mli b/engine/univops.mli index 9af568bcb..30fcc4368 100644 --- a/engine/univops.mli +++ b/engine/univops.mli @@ -9,7 +9,8 @@ open Constr open Univ -(** Shrink a universe context to a restricted set of variables *) +(** The universes of monomorphic constants appear. *) +val universes_of_constr : Environ.env -> constr -> LSet.t -val universes_of_constr : constr -> LSet.t +(** Shrink a universe context to a restricted set of variables *) val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t |