diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.ml | 2 | ||||
| -rw-r--r-- | engine/uState.ml | 47 | ||||
| -rw-r--r-- | engine/uState.mli | 8 | ||||
| -rw-r--r-- | engine/univMinim.ml | 10 | ||||
| -rw-r--r-- | engine/univMinim.mli | 2 | ||||
| -rw-r--r-- | engine/univops.mli | 2 |
6 files changed, 41 insertions, 30 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index b621a3fe2f..6a721a1a8a 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -702,7 +702,7 @@ let empty = { } let from_env e = - { empty with universes = UState.make (Environ.universes e) } + { empty with universes = UState.make ~lbound:(Environ.universes_lbound e) (Environ.universes e) } let from_ctx ctx = { empty with universes = ctx } diff --git a/engine/uState.ml b/engine/uState.ml index 5ed016e0d0..cb40e6eadd 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -34,6 +34,7 @@ type t = (** The subset of unification variables that can be instantiated with algebraic universes as they appear in inferred types only. *) uctx_universes : UGraph.t; (** The current graph extended with the local constraints *) + uctx_universes_lbound : Univ.Level.t; (** The lower bound on universes (e.g. Set or Prop) *) uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *) uctx_weak_constraints : UPairSet.t } @@ -47,6 +48,7 @@ let empty = uctx_univ_variables = LMap.empty; uctx_univ_algebraic = LSet.empty; uctx_universes = initial_sprop_cumulative; + uctx_universes_lbound = Univ.Level.set; uctx_initial_universes = initial_sprop_cumulative; uctx_weak_constraints = UPairSet.empty; } @@ -54,10 +56,12 @@ let elaboration_sprop_cumul = Goptions.declare_bool_option_and_ref ~depr:false ~name:"SProp cumulativity during elaboration" ~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true -let make u = +let make ~lbound u = let u = if elaboration_sprop_cumul () then UGraph.make_sprop_cumulative u else u in - { empty with - uctx_universes = u; uctx_initial_universes = u} + { empty with + uctx_universes = u; + uctx_universes_lbound = lbound; + uctx_initial_universes = u} let is_empty ctx = ContextSet.is_empty ctx.uctx_local && @@ -83,7 +87,7 @@ let union ctx ctx' = let newus = LSet.diff newus (LMap.domain ctx.uctx_univ_variables) in let weak = UPairSet.union ctx.uctx_weak_constraints ctx'.uctx_weak_constraints in let declarenew g = - LSet.fold (fun u g -> UGraph.add_universe u false g) newus g + LSet.fold (fun u g -> UGraph.add_universe u ~lbound:ctx.uctx_universes_lbound ~strict:false g) newus g in let names_rev = LMap.lunion (snd ctx.uctx_names) (snd ctx'.uctx_names) in { uctx_names = (names, names_rev); @@ -99,6 +103,7 @@ let union ctx ctx' = else let cstrsr = ContextSet.constraints ctx'.uctx_local in UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes)); + uctx_universes_lbound = ctx.uctx_universes_lbound; uctx_weak_constraints = weak} let context_set ctx = ctx.uctx_local @@ -431,18 +436,19 @@ let check_univ_decl ~poly uctx decl = (ContextSet.constraints uctx.uctx_local); ctx -let restrict_universe_context (univs, csts) keep = +let restrict_universe_context ~lbound (univs, csts) keep = let removed = LSet.diff univs keep in if LSet.is_empty removed then univs, csts else let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in let g = UGraph.initial_universes in - let g = LSet.fold (fun v g -> if Level.is_small v then g else UGraph.add_universe v false g) allunivs g in + let g = LSet.fold (fun v g -> if Level.is_small v then g else + UGraph.add_universe v ~lbound ~strict:false g) allunivs g in let g = UGraph.merge_constraints csts g in let allkept = LSet.union (UGraph.domain UGraph.initial_universes) (LSet.diff allunivs removed) in let csts = UGraph.constraints_for ~kept:allkept g in let csts = Constraint.filter (fun (l,d,r) -> - not ((Level.is_set l && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in + not ((Level.equal l lbound && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in (LSet.inter univs keep, csts) let restrict ctx vars = @@ -450,7 +456,7 @@ let restrict ctx vars = let vars = Names.Id.Map.fold (fun na l vars -> LSet.add l vars) (fst ctx.uctx_names) vars in - let uctx' = restrict_universe_context ctx.uctx_local vars in + let uctx' = restrict_universe_context ~lbound:ctx.uctx_universes_lbound ctx.uctx_local vars in { ctx with uctx_local = uctx' } let demote_seff_univs universes uctx = @@ -497,7 +503,7 @@ let merge ?loc ~sideff ~extend rigid uctx ctx' = else ContextSet.append ctx' uctx.uctx_local in let declare g = LSet.fold (fun u g -> - try UGraph.add_universe u false g + try UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u g with UGraph.AlreadyDeclared when sideff -> g) levels g in @@ -544,16 +550,17 @@ let new_univ_variable ?loc rigid name | None -> add_uctx_loc u loc uctx.uctx_names in let initial = - UGraph.add_universe u false uctx.uctx_initial_universes + UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u uctx.uctx_initial_universes in let uctx' = {uctx' with uctx_names = names; uctx_local = ctx'; - uctx_universes = UGraph.add_universe u false uctx.uctx_universes; + uctx_universes = UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false + u uctx.uctx_universes; uctx_initial_universes = initial} in uctx', u -let make_with_initial_binders e us = - let uctx = make e in +let make_with_initial_binders ~lbound e us = + let uctx = make ~lbound e in List.fold_left (fun uctx { CAst.loc; v = id } -> fst (new_univ_variable ?loc univ_rigid (Some id) uctx)) @@ -561,10 +568,10 @@ let make_with_initial_binders e us = let add_global_univ uctx u = let initial = - UGraph.add_universe u true uctx.uctx_initial_universes + UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_initial_universes in let univs = - UGraph.add_universe u true uctx.uctx_universes + UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_universes in { uctx with uctx_local = ContextSet.add_universe u uctx.uctx_local; uctx_initial_universes = initial; @@ -679,8 +686,9 @@ let refresh_undefined_univ_variables uctx = uctx.uctx_univ_variables LMap.empty in let weak = UPairSet.fold (fun (u,v) acc -> UPairSet.add (subst_fn u, subst_fn v) acc) uctx.uctx_weak_constraints UPairSet.empty in - let declare g = LSet.fold (fun u g -> UGraph.add_universe u false g) - (ContextSet.levels ctx') g in + let lbound = uctx.uctx_universes_lbound in + let declare g = LSet.fold (fun u g -> UGraph.add_universe u ~lbound ~strict:false g) + (ContextSet.levels ctx') g in let initial = declare uctx.uctx_initial_universes in let univs = declare UGraph.initial_universes in let uctx' = {uctx_names = uctx.uctx_names; @@ -688,14 +696,16 @@ let refresh_undefined_univ_variables uctx = uctx_seff_univs = uctx.uctx_seff_univs; uctx_univ_variables = vars; uctx_univ_algebraic = alg; uctx_universes = univs; + uctx_universes_lbound = lbound; uctx_initial_universes = initial; uctx_weak_constraints = weak; } in uctx', subst let minimize uctx = let open UnivMinim in + let lbound = uctx.uctx_universes_lbound in let ((vars',algs'), us') = - normalize_context_set uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables + normalize_context_set ~lbound uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables uctx.uctx_univ_algebraic uctx.uctx_weak_constraints in if ContextSet.equal us' uctx.uctx_local then uctx @@ -709,6 +719,7 @@ let minimize uctx = uctx_univ_variables = vars'; uctx_univ_algebraic = algs'; uctx_universes = universes; + uctx_universes_lbound = lbound; uctx_initial_universes = uctx.uctx_initial_universes; uctx_weak_constraints = UPairSet.empty; (* weak constraints are consumed *) } diff --git a/engine/uState.mli b/engine/uState.mli index 9689f2e961..52e48c4eeb 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -25,9 +25,9 @@ type t val empty : t -val make : UGraph.t -> t +val make : lbound:Univ.Level.t -> UGraph.t -> t -val make_with_initial_binders : UGraph.t -> lident list -> t +val make_with_initial_binders : lbound:Univ.Level.t -> UGraph.t -> lident list -> t val is_empty : t -> bool @@ -88,11 +88,11 @@ val universe_of_name : t -> Id.t -> Univ.Level.t (** {5 Unification} *) -(** [restrict_universe_context (univs,csts) keep] restricts [univs] to +(** [restrict_universe_context lbound (univs,csts) keep] restricts [univs] to the universes in [keep]. The constraints [csts] are adjusted so that transitive constraints between remaining universes (those in [keep] and those not in [univs]) are preserved. *) -val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t +val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> ContextSet.t (** [restrict uctx ctx] restricts the local universes of [uctx] to [ctx] extended by local named universes and side effect universes diff --git a/engine/univMinim.ml b/engine/univMinim.ml index 1b7c33b9c1..30fdd28997 100644 --- a/engine/univMinim.ml +++ b/engine/univMinim.ml @@ -269,11 +269,11 @@ module UPairs = OrderedType.UnorderedPair(Univ.Level) module UPairSet = Set.Make (UPairs) (* TODO check is_small/sprop *) -let normalize_context_set g ctx us algs weak = +let normalize_context_set ~lbound g ctx us algs weak = let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in (* Keep the Prop/Set <= i constraints separate for minimization *) let smallles, csts = - Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts + Constraint.partition (fun (l,d,r) -> d == Le && (Level.equal l lbound || Level.is_sprop l)) csts in let smallles = if get_set_minimization () then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx && not (Level.is_sprop l)) smallles @@ -282,12 +282,12 @@ let normalize_context_set g ctx us algs weak = let csts, partition = (* We first put constraints in a normal-form: all self-loops are collapsed to equalities. *) - let g = LSet.fold (fun v g -> UGraph.add_universe v false g) + let g = LSet.fold (fun v g -> UGraph.add_universe ~lbound ~strict:false v g) ctx UGraph.initial_universes in let add_soft u g = if not (Level.is_small u || LSet.mem u ctx) - then try UGraph.add_universe u false g with UGraph.AlreadyDeclared -> g + then try UGraph.add_universe ~lbound ~strict:false u g with UGraph.AlreadyDeclared -> g else g in let g = Constraint.fold @@ -300,7 +300,7 @@ let normalize_context_set g ctx us algs weak = (* We ignore the trivial Prop/Set <= i constraints. *) let noneqs = Constraint.filter - (fun (l,d,r) -> not ((d == Le && Level.is_small l) || + (fun (l,d,r) -> not ((d == Le && Level.equal l lbound) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in diff --git a/engine/univMinim.mli b/engine/univMinim.mli index 21f6efe86a..72b432e62f 100644 --- a/engine/univMinim.mli +++ b/engine/univMinim.mli @@ -25,7 +25,7 @@ module UPairSet : CSet.S with type elt = (Level.t * Level.t) (a global one if there is one) and transitively saturate the constraints w.r.t to the equalities. *) -val normalize_context_set : UGraph.t -> ContextSet.t -> +val normalize_context_set : lbound:Univ.Level.t -> UGraph.t -> ContextSet.t -> universe_opt_subst (* The defined and undefined variables *) -> LSet.t (* univ variables that can be substituted by algebraics *) -> UPairSet.t (* weak equality constraints *) -> diff --git a/engine/univops.mli b/engine/univops.mli index 6cc7868a38..1f1edbed16 100644 --- a/engine/univops.mli +++ b/engine/univops.mli @@ -15,5 +15,5 @@ open Univ val universes_of_constr : constr -> LSet.t [@@ocaml.deprecated "Use [Vars.universes_of_constr]"] -val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t +val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> ContextSet.t [@@ocaml.deprecated "Use [UState.restrict_universe_context]"] |