From 2986f0543e019ebfbc9b5affe6e3e05b0e48b04a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 5 Aug 2013 15:17:58 -0700 Subject: [PATCH] Simplify how universe variable constraints are represented in the kernel. Allow universe variable to be created without an environment. Signed-off-by: Leonardo de Moura --- src/kernel/environment.cpp | 123 +++++++++++++++---------------------- src/kernel/expr.cpp | 2 +- src/kernel/level.cpp | 13 ++-- src/kernel/level.h | 4 +- src/util/CMakeLists.txt | 2 +- src/util/safe_arith.cpp | 36 +++++++++++ src/util/safe_arith.h | 18 ++++++ 7 files changed, 111 insertions(+), 87 deletions(-) create mode 100644 src/util/safe_arith.cpp create mode 100644 src/util/safe_arith.h diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 568beb907e..b85f4a527b 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -6,11 +6,11 @@ Author: Leonardo de Moura */ #include #include -#include #include #include #include #include "environment.h" +#include "safe_arith.h" #include "type_check.h" #include "exception.h" #include "debug.h" @@ -55,10 +55,14 @@ void environment::fact::display(std::ostream & out) const { /** \brief Implementation of the Lean environment. */ struct environment::imp { typedef std::unordered_map object_dictionary; - std::vector> m_uvar_distances; + typedef std::tuple constraint; + // Universe variable management + std::vector m_constraints; std::vector m_uvars; + // Children environment management std::atomic m_num_children; std::shared_ptr m_parent; + // Object management std::vector m_objects; object_dictionary m_object_dictionary; @@ -68,43 +72,30 @@ struct environment::imp { bool has_parent() const { return m_parent != nullptr; } - /** \brief Return v - k. It throws an exception if there is a underflow. */ - static int sub(int v, unsigned k) { - long long r = static_cast(v) - static_cast(k); - if (r < std::numeric_limits::min()) - throw exception("universe overflow"); - return static_cast(r); - } - - /** \brief Return v + k. It throws an exception if there is an overflow. */ - static int add(int v, unsigned k) { - long long r = static_cast(v) + static_cast(k); - if (r > std::numeric_limits::max() - 1) - throw exception("universe overflow"); - return static_cast(r); - } - - /** \brief Return v + k. It throws an exception if there is an overflow. */ - static unsigned add(unsigned v, unsigned k) { - unsigned long long r = static_cast(v) + static_cast(k); - if (r > std::numeric_limits::max() - 1) - throw exception("universe overflow"); - return static_cast(r); + /** \brief Return true if l1 >= l2 + k is implied by constraints + \pre is_uvar(l1) && is_uvar(l2) + */ + bool is_implied(level const & l1, level const & l2, int k) { + lean_assert(is_uvar(l1) && is_uvar(l2)); + if (l1 == l2) + return k <= 0; + else + return std::any_of(m_constraints.begin(), m_constraints.end(), + [&](constraint const & c) { return std::get<0>(c) == l1 && std::get<1>(c) == l2 && std::get<2>(c) >= k; }); } /** \brief Return true iff l1 >= l2 + k */ bool is_ge(level const & l1, level const & l2, int k) { + if (l1 == l2) + return k == 0; switch (kind(l2)) { case level_kind::UVar: switch (kind(l1)) { - case level_kind::UVar: { - unsigned d = m_uvar_distances[uvar_idx(l1)][uvar_idx(l2)]; - return d != uninit && (k < 0 || (k >= 0 && d >= static_cast(k))); - } - case level_kind::Lift: return is_ge(lift_of(l1), l2, sub(k, lift_offset(l1))); + case level_kind::UVar: return is_implied(l1, l2, k); + case level_kind::Lift: return is_ge(lift_of(l1), l2, safe_sub(k, lift_offset(l1))); case level_kind::Max: return std::any_of(max_begin_levels(l1), max_end_levels(l1), [&](level const & l) { return is_ge(l, l2, k); }); } - case level_kind::Lift: return is_ge(l1, lift_of(l2), add(k, lift_offset(l2))); + case level_kind::Lift: return is_ge(l1, lift_of(l2), safe_add(k, lift_offset(l2))); case level_kind::Max: return std::all_of(max_begin_levels(l2), max_end_levels(l2), [&](level const & l) { return is_ge(l1, l, k); }); } lean_unreachable(); @@ -121,43 +112,35 @@ struct environment::imp { level add_var(name const & n) { if (std::any_of(m_uvars.begin(), m_uvars.end(), [&](level const & l){ return uvar_name(l) == n; })) throw exception("invalid universe variable declaration, it has already been declared"); - unsigned idx = m_uvars.size(); - level r(n, idx); + level r(n); m_uvars.push_back(r); - std::for_each(m_uvar_distances.begin(), m_uvar_distances.end(), [](std::vector & v) { v.push_back(uninit); }); - m_uvar_distances.push_back(std::vector()); - std::vector & d = m_uvar_distances.back(); - d.resize(m_uvars.size(), static_cast(uninit)); - d[idx] = 0; return r; } - void add_constraint(uvar v1, uvar v2, unsigned d) { - lean_assert(v1 != v2); - unsigned num = m_uvar_distances.size(); - lean_assert(v1 < num); - lean_assert(v2 < num); - std::vector & v1_dists = m_uvar_distances[v1]; - if (v1_dists[v2] == uninit || d >= v1_dists[v2]) { - v1_dists[v2] = d; - // update forward - std::vector & v2_dists = m_uvar_distances[v2]; - for (uvar v3 = 0; v3 < num; v3++) { - if (v2_dists[v3] != uninit) { - lean_assert(v1 != v3); - unsigned d_v1_v3 = add(d, v2_dists[v3]); - if (v1_dists[v3] == uninit || d_v1_v3 >= v1_dists[v3]) - v1_dists[v3] = d_v1_v3; - } + void add_constraint(level const & l1, level const & l2, int d) { + if (is_implied(l1, l2, d)) + return; // redundant + buffer to_add; + for (constraint const & c : m_constraints) { + if (std::get<0>(c) == l2) { + level const & l3 = std::get<1>(c); + int l1_l3_d = safe_add(d, std::get<2>(c)); + if (!is_implied(l1, l3, l1_l3_d)) + to_add.push_back(constraint(l1, l3, l1_l3_d)); } } + m_constraints.push_back(constraint(l1, l2, d)); + for (constraint const & c: to_add) { + m_constraints.push_back(c); + } } - void add_constraints(uvar v1, level const & l, unsigned k) { + void add_constraints(level const & n, level const & l, int k) { + lean_assert(is_uvar(n)); switch (kind(l)) { - case level_kind::UVar: add_constraint(v1, uvar_idx(l), k); return; - case level_kind::Lift: add_constraints(v1, lift_of(l), add(k, lift_offset(l))); return; - case level_kind::Max: std::for_each(max_begin_levels(l), max_end_levels(l), [&](level const & l1) { add_constraints(v1, l1, k); }); return; + case level_kind::UVar: add_constraint(n, l, k); return; + case level_kind::Lift: add_constraints(n, lift_of(l), safe_add(k, lift_offset(l))); return; + case level_kind::Max: std::for_each(max_begin_levels(l), max_end_levels(l), [&](level const & l1) { add_constraints(n, l1, k); }); return; } lean_unreachable(); } @@ -168,7 +151,7 @@ struct environment::imp { if (has_children()) throw exception("invalid universe declaration, environment has children environments"); level r = add_var(n); - add_constraints(uvar_idx(r), l, 0); + add_constraints(r, l, 0); return r; } @@ -189,25 +172,15 @@ struct environment::imp { void init_uvars() { m_uvars.push_back(level()); - m_uvar_distances.push_back(std::vector()); - m_uvar_distances.back().push_back(0); - lean_assert(uvar_idx(m_uvars.back()) == 0); } void display_uvars(std::ostream & out) const { - std::for_each(m_uvars.begin(), m_uvars.end(), - [&](level const & u) { - std::vector const & u_dists = m_uvar_distances[uvar_idx(u)]; - unsigned num = u_dists.size(); - for (uvar v2 = 0; v2 < num; v2++) { - if (v2 != uvar_idx(u) && u_dists[v2] != uninit) { - out << uvar_name(u) << " >= " << uvar_name(m_uvars[v2]); - if (u_dists[v2] > 0) - out << " + " << u_dists[v2]; - out << "\n"; - } - } - }); + for (constraint const & c : m_constraints) { + out << uvar_name(std::get<0>(c)) << " >= " << uvar_name(std::get<1>(c)); + if (std::get<2>(c) >= 0) + out << " + " << std::get<2>(c); + out << "\n"; + } } void check_no_children() { diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 56baf239d1..965b835df1 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -210,7 +210,7 @@ std::ostream & operator<<(std::ostream & out, expr const & a) { case expr_kind::Let: out << "(let " << let_name(a) << " := " << let_value(a) << " in " << let_body(a) << ")"; break; case expr_kind::Type: { level const & l = ty_level(a); - if (is_uvar(l) && uvar_idx(l) == 0) + if (l == level()) out << "Type"; else out << "(Type " << ty_level(a) << ")"; diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp index 887d86628f..b946b37b36 100644 --- a/src/kernel/level.cpp +++ b/src/kernel/level.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include "safe_arith.h" #include "level.h" #include "buffer.h" #include "rc.h" @@ -20,8 +21,7 @@ struct level_cell { }; struct level_uvar : public level_cell { name m_name; - uvar m_uvar; - level_uvar(name const & n, uvar u):level_cell(level_kind::UVar), m_name(n), m_uvar(u) {} + level_uvar(name const & n):level_cell(level_kind::UVar), m_name(n) {} }; struct level_lift : public level_cell { level m_l; @@ -52,8 +52,8 @@ void level_cell::dealloc() { case level_kind::Max: static_cast(this)->~level_max(); delete[] reinterpret_cast(this); break; } } -level::level(): m_ptr(new level_uvar(name("bot"), 0)) { lean_assert(uvar_name(*this) == name("bot")); } -level::level(name const & n, uvar u): m_ptr(new level_uvar(n, u)) {} +level::level(): m_ptr(new level_uvar(name("bot"))) { lean_assert(uvar_name(*this) == name("bot")); } +level::level(name const & n): m_ptr(new level_uvar(n)) {} level::level(level const & l, unsigned k):m_ptr(new level_lift(l, k)) { lean_assert(is_uvar(l)); } level::level(level_cell * ptr): m_ptr(ptr) { lean_assert(m_ptr->get_rc() == 1); } level::level(level const & s): @@ -133,7 +133,7 @@ level max(level const & l1, level const & l2) { level operator+(level const & l, unsigned k) { switch (kind(l)) { case level_kind::UVar: return level(l, k); - case level_kind::Lift: return level(lift_of(l), lift_offset(l) + k); + case level_kind::Lift: return level(lift_of(l), safe_add(lift_offset(l), k)); case level_kind::Max: { std::cout << l << "\n"; buffer new_lvls; @@ -147,7 +147,6 @@ level operator+(level const & l, unsigned k) { level_kind kind (level const & l) { lean_assert(l.m_ptr); return l.m_ptr->m_kind; } name const & uvar_name (level const & l) { lean_assert(is_uvar(l)); return static_cast(l.m_ptr)->m_name; } -uvar uvar_idx (level const & l) { lean_assert(is_uvar(l)); return static_cast(l.m_ptr)->m_uvar; } level const & lift_of (level const & l) { lean_assert(is_lift(l)); return static_cast(l.m_ptr)->m_l; } unsigned lift_offset(level const & l) { lean_assert(is_lift(l)); return static_cast(l.m_ptr)->m_k; } unsigned max_size (level const & l) { lean_assert(is_max(l)); return static_cast(l.m_ptr)->m_size; } @@ -159,7 +158,7 @@ level & level::operator=(level&& l) { LEAN_MOVE_REF(level, l); } bool operator==(level const & l1, level const & l2) { if (kind(l1) != kind(l2)) return false; switch (kind(l1)) { - case level_kind::UVar: return uvar_idx(l1) == uvar_idx(l2); + case level_kind::UVar: return uvar_name(l1) == uvar_name(l2); case level_kind::Lift: return lift_of(l1) == lift_of(l2) && lift_offset(l1) == lift_offset(l2); case level_kind::Max: if (max_size(l1) == max_size(l2)) { diff --git a/src/kernel/level.h b/src/kernel/level.h index 0803cec8b1..c67577d80c 100644 --- a/src/kernel/level.h +++ b/src/kernel/level.h @@ -11,7 +11,6 @@ Author: Leonardo de Moura namespace lean { class environment; struct level_cell; -typedef unsigned uvar; enum class level_kind { UVar, Lift, Max }; /** \brief Universe level. @@ -20,7 +19,6 @@ class level { friend class environment; level_cell * m_ptr; /** \brief Private constructor used by the environment to create a new universe variable named \c n with internal id \c u. */ - level(name const & n, uvar u); level(level const & l, unsigned k); level(level_cell * ptr); friend level to_level(level_cell * c); @@ -29,6 +27,7 @@ class level { public: /** \brief Universe 0 */ level(); + level(name const & n); level(level const & l); level(level&& s); ~level(); @@ -37,7 +36,6 @@ public: friend level_kind kind (level const & l); friend name const & uvar_name (level const & l); - friend uvar uvar_idx (level const & l); friend level const & lift_of (level const & l); friend unsigned lift_offset(level const & l); friend unsigned max_size (level const & l); diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index fa69d0ec84..91f21e3b7a 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -1,4 +1,4 @@ add_library(util trace.cpp debug.cpp name.cpp exception.cpp verbosity.cpp interrupt.cpp hash.cpp escaped.cpp bit_tricks.cpp - format.cpp + format.cpp safe_arith.cpp ) diff --git a/src/util/safe_arith.cpp b/src/util/safe_arith.cpp new file mode 100644 index 0000000000..cc9b62b22b --- /dev/null +++ b/src/util/safe_arith.cpp @@ -0,0 +1,36 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include "exception.h" + +namespace lean { +void check_int_overflow(long long n) { + if (n < std::numeric_limits::min()) + throw exception("integer underflow"); + if (n > std::numeric_limits::max()) + throw exception("integer overflow"); +} + +template +int safe_sub_core(int v, Num k) { + long long r = static_cast(v) - static_cast(k); + check_int_overflow(r); + return static_cast(r); +} +int safe_sub(int v, int k) { return safe_sub_core(v, k); } +int safe_sub(int v, unsigned k) { return safe_sub_core(v, k); } + +template +Num1 safe_add_core(Num1 v, Num2 k) { + long long r = static_cast(v) + static_cast(k); + check_int_overflow(r); + return static_cast(r); +} +int safe_add(int v, int k) { return safe_add_core(v, k); } +int safe_add(int v, unsigned k) { return safe_add_core(v, k); } +unsigned safe_add(unsigned v, unsigned k) { return safe_add_core(v, k); } +} diff --git a/src/util/safe_arith.h b/src/util/safe_arith.h new file mode 100644 index 0000000000..4715ab6f1a --- /dev/null +++ b/src/util/safe_arith.h @@ -0,0 +1,18 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once + +namespace lean { +/** \brief Return v - k. It throws an exception if there is a underflow. */ +int safe_sub(int v, int k); +int safe_sub(int v, unsigned k); + +/** \brief Return v + k. It throws an exception if there is an overflow. */ +int safe_add(int v, int k); +int safe_add(int v, unsigned k); +unsigned safe_add(unsigned v, unsigned k); +}