diff options
| -rw-r--r-- | library/universes.ml | 20 | ||||
| -rw-r--r-- | pretyping/evd.ml | 16 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3446.v | 44 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3922.v | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4089.v | 2 | ||||
| -rw-r--r-- | toplevel/command.ml | 56 |
6 files changed, 84 insertions, 56 deletions
diff --git a/library/universes.ml b/library/universes.ml index 16e6ebb029..a3926bc6f2 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -757,7 +757,7 @@ let minimize_univ_variables ctx us algs left right cstrs = if alg then (* u is algebraic: we instantiate it with it's lower bound, if any, or enforce the constraints if it is bounded from the top. *) - instantiate_with_lbound u lbound true (not (Option.is_empty right)) acc + instantiate_with_lbound u lbound true false acc else (* u is non algebraic *) match Universe.level lbound with | Some l -> (* The lowerbound is directly a level *) @@ -767,7 +767,8 @@ let minimize_univ_variables ctx us algs left right cstrs = if not (Level.equal l u) then (* Should check that u does not have upper constraints that are not already in right *) - instantiate_with_lbound u lbound false (LSet.mem l algs) acc + let acc' = (ctx', us, LSet.remove l algs, insts, cstrs) in + instantiate_with_lbound u lbound false false acc else acc, (true, false, lbound) | None -> try @@ -1017,13 +1018,14 @@ let solve_constraints_system levels level_bounds level_min = for i=0 to nind-1 do for j=0 to nind-1 do if not (Int.equal i j) && Int.Set.mem j clos.(i) then - (v.(i) <- Universe.sup v.(i) level_bounds.(j); - level_min.(i) <- Universe.sup level_min.(i) level_min.(j)) + (v.(i) <- Universe.sup v.(i) level_bounds.(j)); + (* level_min.(i) <- Universe.sup level_min.(i) level_min.(j)) *) done; - for j=0 to nind-1 do - match levels.(j) with - | Some u -> v.(i) <- univ_level_rem u v.(i) level_min.(i) - | None -> () - done + (* for j=0 to nind-1 do *) + (* match levels.(j) with *) + (* | Some u when not (Univ.Level.is_small u) -> *) + (* v.(i) <- univ_level_rem u v.(i) level_min.(i) *) + (* | _ -> () *) + (* done *) done; v diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 60b1da7049..168a10df93 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -351,10 +351,7 @@ let evar_universe_context_of ctx = { empty_evar_universe_context with uctx_local let evar_universe_context_subst ctx = ctx.uctx_univ_variables let instantiate_variable l b v = - (* let b = Univ.subst_large_constraint (Univ.Universe.make l) Univ.type0m_univ b in *) - (* if Univ.univ_depends (Univ.Universe.make l) b then *) - (* error ("Occur-check in universe variable instantiation") *) - (* else *) v := Univ.LMap.add l (Some b) !v + v := Univ.LMap.add l (Some b) !v exception UniversesDiffer @@ -420,7 +417,16 @@ let process_universe_constraints univs vars alg cstrs = raise UniversesDiffer in Univ.enforce_eq_level l' r' local - | _, _ (* One of the two is algebraic or global *) -> + | Inr (l, loc, alg), Inl r + | Inl r, Inr (l, loc, alg) -> + let inst = Univ.univ_level_rem l r r in + if alg then (instantiate_variable l inst vars; local) + else + let lu = Univ.Universe.make l in + if Univ.univ_level_mem l r then + Univ.enforce_leq inst lu local + else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None)) + | _, _ (* One of the two is algebraic or global *) -> if Univ.check_eq univs l r then local else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None)) in diff --git a/test-suite/bugs/closed/3446.v b/test-suite/bugs/closed/3446.v index 4f29b76c6e..dce73e1a50 100644 --- a/test-suite/bugs/closed/3446.v +++ b/test-suite/bugs/closed/3446.v @@ -1,28 +1,32 @@ (* File reduced by coq-bug-finder from original input, then from 7372 lines to 539 lines, then from 531 lines to 107 lines, then from 76 lines to 46 lines *) -(* Set Asymmetric Patterns. *) -(* Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). *) -(* Notation "A -> B" := (forall (_ : A), B). *) +Module First. +Set Asymmetric Patterns. +Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). +Notation "A -> B" := (forall (_ : A), B). +Set Universe Polymorphism. + -(* Notation "x → y" := (x -> y) *) -(* (at level 99, y at level 200, right associativity): type_scope. *) -(* Record sigT A (P : A -> Type) := *) -(* { projT1 : A ; projT2 : P projT1 }. *) -(* Arguments projT1 {A P} s. *) -(* Arguments projT2 {A P} s. *) -(* Set Universe Polymorphism. *) -(* Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x). *) -(* Reserved Notation "x = y" (at level 70, no associativity). *) -(* Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y). *) -(* Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end. *) -(* Reserved Notation "{ x : A & P }" (at level 0, x at level 99). *) -(* Notation "{ x : A & P }" := (sigT A (fun x => P)) : type_scope. *) +Notation "x → y" := (x -> y) + (at level 99, y at level 200, right associativity): type_scope. +Record sigT A (P : A -> Type) := + { projT1 : A ; projT2 : P projT1 }. +Arguments projT1 {A P} s. +Arguments projT2 {A P} s. +Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x). +Reserved Notation "x = y" (at level 70, no associativity). +Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y). +Notation " x = y " := (paths x y) : type_scope. +Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end. +Reserved Notation "{ x : A & P }" (at level 0, x at level 99). +Notation "{ x : A & P }" := (sigT A (fun x => P)) : type_scope. -(* Axiom path_sigma_uncurried : forall {A : Type} (P : A -> Type) (u v : sigT A P) (pq : {p : projT1 u = projT1 v & transport _ p (projT2 u) = projT2 v}), u = v. *) -(* Axiom isequiv_pr1_contr : forall {A} {P : A -> Type}, (A -> {x : A & P x}). *) +Axiom path_sigma_uncurried : forall {A : Type} (P : A -> Type) (u v : sigT A P) (pq : {p : projT1 u = projT1 v & transport _ p (projT2 u) = projT2 v}), u = v. +Axiom isequiv_pr1_contr : forall {A} {P : A -> Type}, (A -> {x : A & P x}). -(* Definition path_sigma_hprop {A : Type} {P : A -> Type} (u v : sigT _ P) := *) -(* @compose _ _ _ (path_sigma_uncurried P u v) (@isequiv_pr1_contr _ _). *) +Definition path_sigma_hprop {A : Type} {P : A -> Type} (u v : sigT _ P) := + @compose _ _ _ (path_sigma_uncurried P u v) (@isequiv_pr1_contr _ _). +End First. Set Asymmetric Patterns. Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/3922.v b/test-suite/bugs/closed/3922.v index 9320848910..0ccc92067d 100644 --- a/test-suite/bugs/closed/3922.v +++ b/test-suite/bugs/closed/3922.v @@ -43,7 +43,7 @@ Notation IsHProp := (IsTrunc -1). Monomorphic Axiom dummy_funext_type : Type0. Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }. -Inductive Unit : Type1 := +Inductive Unit : Set := tt : Unit. Record TruncType (n : trunc_index) := BuildTruncType { diff --git a/test-suite/bugs/closed/4089.v b/test-suite/bugs/closed/4089.v index 1449f242b4..c6cb9c35e6 100644 --- a/test-suite/bugs/closed/4089.v +++ b/test-suite/bugs/closed/4089.v @@ -163,7 +163,7 @@ Notation "A <~> B" := (Equiv A B) (at level 85) : type_scope. Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : function_scope. -Inductive Unit : Type1 := +Inductive Unit : Set := tt : Unit. Ltac done := diff --git a/toplevel/command.ml b/toplevel/command.ml index 1b396d57ba..77339aef44 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -402,20 +402,33 @@ let extract_level env evd min tys = sign_level env evd ((Anonymous, None, concl) :: ctx)) tys in sup_list min sorts +let is_flexible_sort evd u = + match Univ.Universe.level u with + | Some l -> Evd.is_flexible_level evd l + | None -> false + let inductive_levels env evdref poly arities inds = - let destarities = List.map (Reduction.dest_arity env) arities in - let levels = List.map (fun (ctx,a) -> + let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in + let levels = List.map (fun (x,(ctx,a)) -> if a = Prop Null then None else Some (univ_of_sort a)) destarities in let cstrs_levels, min_levels, sizes = CList.split3 - (List.map2 (fun (_,tys,_) (ctx,du) -> + (List.map2 (fun (_,tys,_) (arity,(ctx,du)) -> let len = List.length tys in + let minlev = Sorts.univ_of_sort du in let minlev = if len > 1 && not (is_impredicative env du) then - Univ.type0_univ - else Univ.type0m_univ + Univ.sup minlev Univ.type0_univ + else minlev + in + let minlev = + (** Indices contribute. *) + if Indtypes.is_indices_matter () && List.length ctx > 0 then ( + let ilev = sign_level env !evdref ctx in + Univ.sup ilev minlev) + else minlev in let clev = extract_level env !evdref minlev tys in (clev, minlev, len)) inds destarities) @@ -425,32 +438,25 @@ let inductive_levels env evdref poly arities inds = let levels' = Universes.solve_constraints_system (Array.of_list levels) (Array.of_list cstrs_levels) (Array.of_list min_levels) in - let evd = - CList.fold_left3 (fun evd cu (ctx,du) len -> + let evd, arities = + CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len -> if is_impredicative env du then (** Any product is allowed here. *) - evd + evd, arity :: arities else (** If in a predicative sort, or asked to infer the type, we take the max of: - indices (if in indices-matter mode) - constructors - Type(1) if there is more than 1 constructor *) - let evd = - (** Indices contribute. *) - if Indtypes.is_indices_matter () && List.length ctx > 0 then ( - let ilev = sign_level env !evdref ctx in - Evd.set_leq_sort env evd (Type ilev) du) - else evd - in (** Constructors contribute. *) let evd = if Sorts.is_set du then if not (Evd.check_leq evd cu Univ.type0_univ) then raise (Indtypes.InductiveError Indtypes.LargeNonPropInductiveNotInType) else evd - else - Evd.set_leq_sort env evd (Type cu) du + else evd + (* Evd.set_leq_sort env evd (Type cu) du *) in let evd = if len >= 2 && Univ.is_type0m_univ cu then @@ -459,9 +465,19 @@ let inductive_levels env evdref poly arities inds = land in Prop directly (no informative arguments as well). *) Evd.set_leq_sort env evd (Prop Pos) du else evd - in evd) - !evdref (Array.to_list levels') destarities sizes - in evdref := evd; arities + in + (* let arity = it_mkProd_or_LetIn (mkType cu) ctx in *\) *) + let duu = Sorts.univ_of_sort du in + let evd = + if not (Univ.is_small_univ duu) && Evd.check_eq evd cu duu then + if is_flexible_sort evd duu then + Evd.set_eq_sort env evd (Prop Null) du + else evd + else Evd.set_eq_sort env evd (Type cu) du + in + (evd, arity :: arities)) + (!evdref,[]) (Array.to_list levels') destarities sizes + in evdref := evd; List.rev arities let check_named (loc, na) = match na with | Name _ -> () |