From 01259b1e84d6bd851e7a2450b2f3630b9fe9fab1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 29 Jan 2014 16:31:00 -0800 Subject: [PATCH] feat(kernel): make sure U is the maximal universe Signed-off-by: Leonardo de Moura --- src/builtin/heq.lean | 1 - src/kernel/environment.cpp | 14 ++++++++++++++ tests/lean/univ.lean | 16 ++++------------ tests/lean/univ.lean.expected.out | 6 ++++-- tests/lean/univ2.lean | 12 ++++++------ tests/lean/univ2.lean.expected.out | 10 ++++++++-- 6 files changed, 36 insertions(+), 23 deletions(-) diff --git a/src/builtin/heq.lean b/src/builtin/heq.lean index 4547ea64f..8bc994b37 100644 --- a/src/builtin/heq.lean +++ b/src/builtin/heq.lean @@ -24,7 +24,6 @@ axiom hcongr {A A' : TypeU} {B : A → TypeU} {B' : A' → TypeU} {f : ∀ x, B f == f' → a == a' → f a == f' a' universe M ≥ 1 -universe U ≥ M + 1 definition TypeM := (Type M) -- In the following definitions the type of A and A' cannot be TypeU diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 7c5d39365..d5cee6677 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -25,6 +25,7 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "kernel/normalizer.h" #include "kernel/universe_constraints.h" +#include "kernel/kernel.h" #include "version.h" namespace lean { @@ -320,6 +321,9 @@ void environment_cell::add_constraints(name const & n, level const & l, int k) { void environment_cell::check_consistency(name const & n, level const & l, int k) const { switch (kind(l)) { case level_kind::UVar: + if (l == ty_level(TypeU)) + throw kernel_exception(env(), sstream() << "invalid universe constraint: " << n << " >= " << l << " + " << k + << ", several modules in Lean assume that " << l << " is the maximal universe"); if (!get_ro_ucs().is_consistent(n, uvar_name(l), k)) throw kernel_exception(env(), sstream() << "universe constraint inconsistency: " << n << " >= " << l << " + " << k); if (get_ro_ucs().overflows(n, uvar_name(l), k)) @@ -338,15 +342,25 @@ level environment_cell::add_uvar_cnstr(name const & n, level const & l) { level r; auto const & uvs = get_ro_universes().m_uvars; auto it = std::find_if(uvs.begin(), uvs.end(), [&](level const & l) { return uvar_name(l) == n; }); + bool new_universe; check_consistency(n, l, 0); if (it == uvs.end()) { r = add_uvar_core(n); + new_universe = true; } else { // universe n already exists, we must check consistency of the new constraint. r = *it; + new_universe = false; } m_objects.push_back(mk_uvar_cnstr(n, l)); add_constraints(n, l, 0); + name const & Uname = uvar_name(ty_level(TypeU)); + if (new_universe && n != Uname && !is_ge(ty_level(TypeU), r, 1)) { + // In Lean, U is the maximal universe, several Lean modules assume that, + // and the kernel axioms are all with respect to U. + // So, we force all other universes to smaller than U + add_uvar_cnstr(Uname, r+1); + } return r; } diff --git a/tests/lean/univ.lean b/tests/lean/univ.lean index f956c5ef9..3d4074f2f 100644 --- a/tests/lean/univ.lean +++ b/tests/lean/univ.lean @@ -8,24 +8,13 @@ assert(env:get_universe_distance("Z", "M") == 3) assert(not env:get_universe_distance("Z", "U")) *) -scope - universe Z ≥ U + 10 - (* - local env = get_environment() - assert(env:get_universe_distance("Z", "U") == 10) - assert(env:get_universe_distance("Z", "M") == - env:get_universe_distance("Z", "U") + - env:get_universe_distance("U", "M")) - *) -pop_scope - (* local env = get_environment() assert(env:get_universe_distance("Z", "M") == 3) assert(not env:get_universe_distance("Z", "U")) *) -universe Z1 ≥ U + 1073741824. +universe Z1 ≥ M + 1073741824. universe Z2 ≥ Z1 + 1073741824. universe U1 @@ -40,3 +29,6 @@ assert(env:get_universe_distance("U4", "U3") == 3) assert(env:get_universe_distance("U4", "U2") == 1) *) universe U1 ≥ U4. + +universe Z >= U. +universe Z >= U + 1. \ No newline at end of file diff --git a/tests/lean/univ.lean.expected.out b/tests/lean/univ.lean.expected.out index b30e35b4e..5927c52d7 100644 --- a/tests/lean/univ.lean.expected.out +++ b/tests/lean/univ.lean.expected.out @@ -1,5 +1,7 @@ Set: pp::colors Set: pp::unicode Defined: TypeM -univ.lean:29:0: error: universe constraint produces an integer overflow: Z2 >= Z1 + 1073741824 -univ.lean:42:0: error: universe constraint inconsistency: U1 >= U4 + 0 +univ.lean:18:0: error: universe constraint produces an integer overflow: Z2 >= Z1 + 1073741824 +univ.lean:31:0: error: universe constraint inconsistency: U1 >= U4 + 0 +univ.lean:33:0: error: invalid universe constraint: Z >= U + 0, several modules in Lean assume that U is the maximal universe +univ.lean:34:0: error: invalid universe constraint: Z >= U + 1, several modules in Lean assume that U is the maximal universe diff --git a/tests/lean/univ2.lean b/tests/lean/univ2.lean index 1a67e40f8..710088e28 100644 --- a/tests/lean/univ2.lean +++ b/tests/lean/univ2.lean @@ -1,9 +1,9 @@ -universe M >= 1 -universe U >= M + 1 -universe Z >= max U+1 M+1 -print environment 2 +universe M1 >= 1 +universe M2 >= 1 +universe Z >= max M1+1 M2+1 +print environment (* local env = get_environment() -assert(env:get_universe_distance("Z", "U") == 1) -assert(env:get_universe_distance("Z", "M") == 2) +assert(env:get_universe_distance("Z", "M1") == 1) +assert(env:get_universe_distance("Z", "M2") == 1) *) diff --git a/tests/lean/univ2.lean.expected.out b/tests/lean/univ2.lean.expected.out index d62395bb1..4d9bbecbb 100644 --- a/tests/lean/univ2.lean.expected.out +++ b/tests/lean/univ2.lean.expected.out @@ -1,4 +1,10 @@ Set: pp::colors Set: pp::unicode -universe U ≥ M+1 -universe Z ≥ U+1 ⊔ M+1 +import "kernel" +import "Nat" +universe M1 ≥ 1 +universe U ≥ M1+1 +universe M2 ≥ 1 +universe U ≥ M2+1 +universe Z ≥ M1+1 ⊔ M2+1 +universe U ≥ Z+1