diff options
-rw-r--r-- | kernel/environ.ml | 39 | ||||
-rw-r--r-- | kernel/environ.mli | 4 | ||||
-rw-r--r-- | kernel/term_typing.ml | 8 | ||||
-rw-r--r-- | kernel/univ.ml | 26 | ||||
-rw-r--r-- | kernel/univ.mli | 4 | ||||
-rw-r--r-- | library/universes.ml | 9 | ||||
-rw-r--r-- | pretyping/evd.ml | 4 | ||||
-rw-r--r-- | test-suite/bugs/closed/3309.v | 6 |
8 files changed, 61 insertions, 39 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 109e3830c..c433c0789 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -181,26 +181,41 @@ let fold_named_context_reverse f ~init env = (* Universe constraints *) -let add_constraints c env = - if Univ.Constraint.is_empty c then - env - else - let s = env.env_stratification in +let map_universes f env = + let s = env.env_stratification in { env with env_stratification = - { s with env_universes = Univ.merge_constraints c s.env_universes } } + { s with env_universes = f s.env_universes } } + +let add_constraints c env = + if Univ.Constraint.is_empty c then env + else map_universes (Univ.merge_constraints c) env let check_constraints c env = Univ.check_constraints c env.env_stratification.env_universes -let set_engagement c env = (* Unsafe *) - { env with env_stratification = - { env.env_stratification with env_engagement = c } } - let push_constraints_to_env (_,univs) env = add_constraints univs env -let push_context ctx env = add_constraints (Univ.UContext.constraints ctx) env -let push_context_set ctx env = add_constraints (Univ.ContextSet.constraints ctx) env +let add_universes strict ctx g = + let g = Array.fold_left (fun g v -> Univ.add_universe v strict g) + g (Univ.Instance.to_array (Univ.UContext.instance ctx)) + in + Univ.merge_constraints (Univ.UContext.constraints ctx) g + +let push_context ?(strict=false) ctx env = + map_universes (add_universes strict ctx) env + +let add_universes_set strict ctx g = + let g = Univ.LSet.fold (fun v g -> Univ.add_universe v strict g) + (Univ.ContextSet.levels ctx) g + in Univ.merge_constraints (Univ.ContextSet.constraints ctx) g + +let push_context_set ?(strict=false) ctx env = + map_universes (add_universes_set strict ctx) env + +let set_engagement c env = (* Unsafe *) + { env with env_stratification = + { env.env_stratification with env_engagement = c } } (* Global constants *) diff --git a/kernel/environ.mli b/kernel/environ.mli index 4ad0327fc..9f6ea522a 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -208,8 +208,8 @@ val add_constraints : Univ.constraints -> env -> env (** Check constraints are satifiable in the environment. *) val check_constraints : Univ.constraints -> env -> bool -val push_context : Univ.universe_context -> env -> env -val push_context_set : Univ.universe_context_set -> env -> env +val push_context : ?strict:bool -> Univ.universe_context -> env -> env +val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env val push_constraints_to_env : 'a Univ.constrained -> env -> env val set_engagement : engagement -> env -> env diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 83e566041..e89b6ef8f 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -100,11 +100,11 @@ let hcons_j j = let feedback_completion_typecheck = Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete) - + let infer_declaration env kn dcl = match dcl with | ParameterEntry (ctx,poly,(t,uctx),nl) -> - let env = push_context uctx env in + let env = push_context ~strict:(not poly) uctx env in let j = infer env t in let abstract = poly && not (Option.is_empty kn) in let usubst, univs = Univ.abstract_universes abstract uctx in @@ -115,7 +115,7 @@ let infer_declaration env kn dcl = | DefinitionEntry ({ const_entry_type = Some typ; const_entry_opaque = true; const_entry_polymorphic = false} as c) -> - let env = push_context c.const_entry_universes env in + let env = push_context ~strict:true c.const_entry_universes env in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let tyj = infer_type env typ in let proofterm = @@ -135,7 +135,7 @@ let infer_declaration env kn dcl = c.const_entry_inline_code, c.const_entry_secctx | DefinitionEntry c -> - let env = push_context c.const_entry_universes env in + let env = push_context ~strict:(not c.const_entry_polymorphic) c.const_entry_universes env in let { const_entry_type = typ; const_entry_opaque = opaque } = c in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let (body, ctx), side_eff = Future.join body in diff --git a/kernel/univ.ml b/kernel/univ.ml index 040e9bc27..b61b441d2 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -750,17 +750,6 @@ let get_set_arc g = repr g Level.set let is_set_arc u = Level.is_set u.univ let is_prop_arc u = Level.is_prop u.univ -let add_universe vlev ~predicative g = - let v = terminal ~predicative vlev in - let arc = - let arc = - if predicative then get_set_arc g else get_prop_arc g - in - { arc with le=vlev::arc.le} - in - let g = enter_arc arc g in - enter_arc v g - (* [safe_repr] also search for the canonical representative, but if the graph doesn't contain the searched universe, we add it. *) @@ -777,6 +766,18 @@ let safe_repr g u = let g = enter_arc {setarc with le=u::setarc.le} g in enter_arc can g, can +let add_universe vlev strict g = + let v = terminal ~predicative:true vlev in + let arc = + let arc = get_set_arc g in + if strict then + { arc with lt=vlev::arc.lt} + else + { arc with le=vlev::arc.le} + in + let g = enter_arc arc g in + enter_arc v g + (* reprleq : canonical_arc -> canonical_arc list *) (* All canonical arcv such that arcu<=arcv with arcv#arcu *) let reprleq g arcu = @@ -1145,7 +1146,8 @@ let merge g arcu arcv = (* we find the arc with the biggest rank, and we redirect all others to it *) let arcu, g, v = let best_ranked (max_rank, old_max_rank, best_arc, rest) arc = - if arc.rank >= max_rank && not (Level.is_small best_arc.univ) + if Level.is_small arc.univ || + (arc.rank >= max_rank && not (Level.is_small best_arc.univ)) then (arc.rank, max_rank, arc, best_arc::rest) else (max_rank, old_max_rank, best_arc, arc::rest) in diff --git a/kernel/univ.mli b/kernel/univ.mli index 76453cbb0..fe7fc1ab9 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -163,8 +163,8 @@ val is_initial_universes : universes -> bool val sort_universes : universes -> universes -(** Adds a universe to the graph, ensuring it is >= Prop or Set. *) -val add_universe : universe_level -> predicative:bool -> universes -> universes +(** Adds a universe to the graph, ensuring it is >= or > Set. *) +val add_universe : universe_level -> bool -> universes -> universes (** {6 Constraints. } *) diff --git a/library/universes.ml b/library/universes.ml index c67371e3b..0544585dc 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -830,8 +830,13 @@ let normalize_context_set ctx us algs = (** Keep the Prop/Set <= i constraints separate for minimization *) let smallles, csts = Constraint.fold (fun (l,d,r as cstr) (smallles, noneqs) -> - if d == Le && Univ.Level.is_small l then - (Constraint.add cstr smallles, noneqs) + if d == Le then + if Univ.Level.is_small l then + (Constraint.add cstr smallles, noneqs) + else if Level.is_small r then + raise (Univ.UniverseInconsistency + (Le,Universe.make l,Universe.make r,None)) + else (smallles, Constraint.add cstr noneqs) else (smallles, Constraint.add cstr noneqs)) csts (Constraint.empty, Constraint.empty) in diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 9f2d28438..a25479d48 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1083,11 +1083,11 @@ let uctx_new_univ_variable rigid name predicative | None -> uctx.uctx_names in let initial = - Univ.add_universe u true uctx.uctx_initial_universes + Univ.add_universe u false uctx.uctx_initial_universes in let uctx' = {uctx' with uctx_names = names; uctx_local = ctx'; - uctx_universes = Univ.add_universe u true uctx.uctx_universes; + uctx_universes = Univ.add_universe u false uctx.uctx_universes; uctx_initial_universes = initial} in uctx', u diff --git a/test-suite/bugs/closed/3309.v b/test-suite/bugs/closed/3309.v index 980431576..6e97ed2af 100644 --- a/test-suite/bugs/closed/3309.v +++ b/test-suite/bugs/closed/3309.v @@ -117,7 +117,7 @@ intros. hnf. apply dirprodpair. exact ax0. apply dirprodpair. exact ax1. exact a Defined. Definition eqax0 { X : UU } { R : hrel X } { A : hsubtypes X } : iseqclass R A -> ishinh ( carrier A ) . -intros X R A; exact ( fun is : iseqclass R A => projT1' _ is ). +intros X R A. exact (fun is : iseqclass R A => projT1' _ is ). Defined. Lemma iseqclassdirprod { X Y : UU } { R : hrel X } { Q : hrel Y } { A : hsubtypes X } { B : hsubtypes Y } ( isa : iseqclass R A ) ( isb : iseqclass Q B ) : iseqclass ( hreldirprod R Q ) ( subtypesdirprod A B ) . @@ -141,7 +141,7 @@ Definition prtoimage { X Y : UU } (f : X -> Y) : X -> image f. admit. Defined. -Definition setquot { X : UU } ( R : hrel X ) : Type. +Definition setquot { X : UU } ( R : hrel X ) : Set. intros; exact ( sigT' ( fun A : _ => iseqclass R A ) ). Defined. Definition setquotpair { X : UU } ( R : hrel X ) ( A : hsubtypes X ) ( is : iseqclass R A ) : setquot R. @@ -157,7 +157,7 @@ Definition setquotinset { X : UU } ( R : hrel X ) : hSet. intros; exact ( hSetpair (setquot R) admit) . Defined. -Definition dirprodtosetquot { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ) (cd : dirprod ( setquot RX ) ( setquot RY ) ) : setquot ( hreldirprod RX RY ). +Definition dirprodtosetquot { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ) (cd : dirprod ( setquot@{i j k l m n p Set q r} RX ) ( setquot RY ) ) : setquot ( hreldirprod RX RY ). intros; exact ( setquotpair _ _ ( iseqclassdirprod ( projT2' _ ( projT1' _ cd ) ) ( projT2' _ ( projT2' _ cd ) ) ) ). Defined. |