From 7772c1603341f4f5baf9089ff59325258e84154a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 20 Dec 2013 12:47:36 -0800 Subject: [PATCH] refactor(kernel): add unfold_opaque flag to normalizer, modify how type checker uses the opaque flag, remove hidden_defs, and mark most builtin definitions as opaque After this commit, in the type checker, when checking convertability, we first compute a normal form without expanding opaque terms. If the terms are convertible, then we are done, and saved a lot of time by not expanding unnecessary definitions. If they are not, instead of throwing an error, we try again expanding the opaque terms. This seems to be the best of both worlds. The opaque flag is a hint for the type checker, but it would never prevent us from type checking a valid term. Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser.cpp | 2 +- src/kernel/builtin.cpp | 12 ++-- src/kernel/environment.cpp | 4 +- src/kernel/environment.h | 5 +- src/kernel/normalizer.cpp | 25 +++++--- src/kernel/normalizer.h | 8 +-- src/kernel/object.h | 17 ++++++ src/kernel/type_checker.cpp | 25 +++++--- src/library/CMakeLists.txt | 2 +- src/library/all/all.cpp | 2 - src/library/arith/int.cpp | 27 +++------ src/library/arith/nat.cpp | 13 ++-- src/library/arith/real.cpp | 22 +++---- src/library/arith/special_fn.cpp | 28 ++++----- src/library/elaborator/elaborator.cpp | 3 +- src/library/hidden_defs.cpp | 87 --------------------------- src/library/hidden_defs.h | 37 ------------ src/library/kernel_bindings.cpp | 15 +++++ src/library/register_module.h | 2 - src/library/tactic/tactic.cpp | 3 +- src/library/tactic/tactic.h | 2 +- src/library/type_inferer.cpp | 22 +++++-- src/tests/kernel/environment.cpp | 3 +- src/tests/library/arith.cpp | 6 +- tests/lean/interactive/elab6.lean | 4 +- tests/lua/hidden1.lua | 19 +++--- 26 files changed, 151 insertions(+), 244 deletions(-) delete mode 100644 src/library/hidden_defs.cpp delete mode 100644 src/library/hidden_defs.h diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 7d3e8326f..daa9ac3d3 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1941,7 +1941,7 @@ class parser::imp { next(); expr v = m_elaborator(parse_expr()); normalizer norm(m_env); - expr r = norm(v); + expr r = norm(v, context(), true); regular(m_io_state) << r << endl; } diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp index e4bcc8ad8..d9903bf84 100644 --- a/src/kernel/builtin.cpp +++ b/src/kernel/builtin.cpp @@ -235,22 +235,22 @@ void import_basic(environment const & env) { env->add_builtin(mk_if_fn()); // implies(x, y) := if x y True - env->add_definition(implies_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, y, True))); + env->add_opaque_definition(implies_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, y, True))); // iff(x, y) := x = y - env->add_definition(iff_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Eq(x, y))); + env->add_opaque_definition(iff_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Eq(x, y))); // not(x) := if x False True - env->add_definition(not_fn_name, p1, Fun({x, Bool}, bIf(x, False, True))); + env->add_opaque_definition(not_fn_name, p1, Fun({x, Bool}, bIf(x, False, True))); // or(x, y) := Not(x) => y - env->add_definition(or_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Implies(Not(x), y))); + env->add_opaque_definition(or_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Implies(Not(x), y))); // and(x, y) := Not(x => Not(y)) - env->add_definition(and_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Not(Implies(x, Not(y))))); + env->add_opaque_definition(and_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Not(Implies(x, Not(y))))); // forall : Pi (A : Type u), (A -> Bool) -> Bool - env->add_definition(forall_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Eq(P, Fun({x, A}, True)))); + env->add_opaque_definition(forall_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Eq(P, Fun({x, A}, True)))); // TODO(Leo): introduce epsilon env->add_definition(exists_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Not(Forall(A, Fun({x, A}, Not(P(x))))))); diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 1f8391afe..0e71ab030 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -397,8 +397,8 @@ expr environment_cell::infer_type(expr const & e, context const & ctx) const { return m_type_checker->infer_type(e, ctx); } -expr environment_cell::normalize(expr const & e, context const & ctx) const { - return m_type_checker->get_normalizer()(e, ctx); +expr environment_cell::normalize(expr const & e, context const & ctx, bool unfold_opaque) const { + return m_type_checker->get_normalizer()(e, ctx, unfold_opaque); } /** \brief Display universal variable constraints and objects stored in this environment and its parents. */ diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 652cecca8..3cd013e64 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -152,15 +152,14 @@ public: \brief Add a new definition n : t := v. It throws an exception if v does not have type t. It throws an exception if there is already an object with the given name. - If opaque == true, then definition is not used by normalizer. */ void add_definition(name const & n, expr const & t, expr const & v, bool opaque = false); + void add_opaque_definition(name const & n, expr const & t, expr const & v) { add_definition(n, t, v, true); } void add_theorem(name const & n, expr const & t, expr const & v); /** \brief Add a new definition n : infer_type(v) := v. It throws an exception if there is already an object with the given name. - If opaque == true, then definition is not used by normalizer. */ void add_definition(name const & n, expr const & v, bool opaque = false); @@ -207,7 +206,7 @@ public: /** \brief Normalize \c e in the given context and this environment. */ - expr normalize(expr const & e, context const & ctx = context()) const; + expr normalize(expr const & e, context const & ctx = context(), bool unfold_opaque = false) const; /** \brief Low-level function for accessing objects. Consider using iterators. diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index d2043f2cc..6d95be471 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -79,6 +79,7 @@ class normalizer::imp { context m_ctx; cached_metavar_env m_menv; cache m_cache; + bool m_unfold_opaque; unsigned m_max_depth; unsigned m_depth; @@ -201,7 +202,7 @@ class normalizer::imp { break; case expr_kind::Constant: { object const & obj = env()->get_object(const_name(a)); - if (obj.is_definition() && !obj.is_opaque()) { + if (should_unfold(obj, m_unfold_opaque)) { freset reset(m_cache); r = normalize(obj.get_value(), value_stack(), 0); } else { @@ -291,9 +292,13 @@ public: m_env(env) { m_max_depth = max_depth; m_depth = 0; + m_unfold_opaque = false; } - expr operator()(expr const & e, context const & ctx, optional const & menv) { + expr operator()(expr const & e, context const & ctx, optional const & menv, bool unfold_opaque) { + if (m_unfold_opaque != unfold_opaque) + m_cache.clear(); + m_unfold_opaque = unfold_opaque; set_ctx(ctx); if (m_menv.update(menv)) m_cache.clear(); @@ -308,13 +313,19 @@ normalizer::normalizer(ro_environment const & env, unsigned max_depth):m_ptr(new normalizer::normalizer(ro_environment const & env):normalizer(env, std::numeric_limits::max()) {} normalizer::normalizer(ro_environment const & env, options const & opts):normalizer(env, get_normalizer_max_depth(opts)) {} normalizer::~normalizer() {} -expr normalizer::operator()(expr const & e, context const & ctx, optional const & menv) { return (*m_ptr)(e, ctx, menv); } -expr normalizer::operator()(expr const & e, context const & ctx, metavar_env const & menv) { return operator()(e, ctx, some_menv(menv)); } -expr normalizer::operator()(expr const & e, context const & ctx) { return operator()(e, ctx, none_menv()); } +expr normalizer::operator()(expr const & e, context const & ctx, optional const & menv, bool unfold_opaque) { + return (*m_ptr)(e, ctx, menv, unfold_opaque); +} +expr normalizer::operator()(expr const & e, context const & ctx, metavar_env const & menv, bool unfold_opaque) { + return operator()(e, ctx, some_menv(menv), unfold_opaque); +} +expr normalizer::operator()(expr const & e, context const & ctx, bool unfold_opaque) { + return operator()(e, ctx, none_menv(), unfold_opaque); +} void normalizer::clear() { m_ptr->clear(); } -expr normalize(expr const & e, ro_environment const & env, context const & ctx) { - return normalizer(env)(e, ctx); +expr normalize(expr const & e, ro_environment const & env, context const & ctx, bool unfold_opaque) { + return normalizer(env)(e, ctx, unfold_opaque); } } diff --git a/src/kernel/normalizer.h b/src/kernel/normalizer.h index 25310a264..ebbc46fa7 100644 --- a/src/kernel/normalizer.h +++ b/src/kernel/normalizer.h @@ -24,12 +24,12 @@ public: normalizer(ro_environment const & env, options const & opts); ~normalizer(); - expr operator()(expr const & e, context const & ctx, optional const & menv); - expr operator()(expr const & e, context const & ctx, metavar_env const & menv); - expr operator()(expr const & e, context const & ctx = context()); + expr operator()(expr const & e, context const & ctx, optional const & menv, bool unfold_opaque = false); + expr operator()(expr const & e, context const & ctx, metavar_env const & menv, bool unfold_opaque = false); + expr operator()(expr const & e, context const & ctx = context(), bool unfold_opaque = false); void clear(); }; /** \brief Normalize \c e using the environment \c env and context \c ctx */ -expr normalize(expr const & e, ro_environment const & env, context const & ctx = context()); +expr normalize(expr const & e, ro_environment const & env, context const & ctx = context(), bool unfold_opaque = false); } diff --git a/src/kernel/object.h b/src/kernel/object.h index 033e952dd..863438cf6 100644 --- a/src/kernel/object.h +++ b/src/kernel/object.h @@ -145,4 +145,21 @@ object mk_theorem(name const & n, expr const & t, expr const & v); object mk_axiom(name const & n, expr const & t); object mk_var_decl(name const & n, expr const & t); inline object mk_neutral(neutral_object_cell * c) { lean_assert(c->get_rc() == 1); return object(c); } + +/** + \brief Helper function whether we should unfold an definition or not. + + 1- We unfold definitions. + 2- We never unfold theorems. + 3- We unfold opaque definitions if \c unfold_opaque == true +*/ +inline bool should_unfold(object const & obj, bool unfold_opaque) { + return obj.is_definition() && !obj.is_theorem() && (unfold_opaque || !obj.is_opaque()); +} +inline bool should_unfold(optional const & obj, bool unfold_opaque) { + return obj && should_unfold(*obj, unfold_opaque); +} +inline bool should_unfold(optional const & obj) { + return should_unfold(obj, false); +} } diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 5e6736742..273d06345 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -51,14 +51,14 @@ class type_checker::imp { return ::lean::instantiate(e, v, m_menv.to_some_menv()); } - expr normalize(expr const & e, context const & ctx) { - return m_normalizer(e, ctx, m_menv.to_some_menv()); + expr normalize(expr const & e, context const & ctx, bool unfold_opaque) { + return m_normalizer(e, ctx, m_menv.to_some_menv(), unfold_opaque); } expr check_pi(expr const & e, expr const & s, context const & ctx) { if (is_pi(e)) return e; - expr r = normalize(e, ctx); + expr r = normalize(e, ctx, false); if (is_pi(r)) return r; if (has_metavar(r) && m_menv && m_uc) { @@ -71,6 +71,9 @@ class type_checker::imp { m_uc->push_back(mk_eq_constraint(ctx, e, p, jst)); return p; } + r = normalize(e, ctx, true); + if (is_pi(r)) + return r; throw function_expected_exception(env(), ctx, s); } @@ -79,7 +82,7 @@ class type_checker::imp { return e; if (is_bool(e)) return Type(); - expr u = normalize(e, ctx); + expr u = normalize(e, ctx, false); if (is_type(u)) return u; if (is_bool(u)) @@ -89,6 +92,11 @@ class type_checker::imp { m_uc->push_back(mk_convertible_constraint(ctx, e, TypeU, jst)); return u; } + u = normalize(e, ctx, true); + if (is_type(u)) + return u; + if (is_bool(u)) + return Type(); throw type_expected_exception(env(), ctx, s); } @@ -267,18 +275,21 @@ class type_checker::imp { bool is_convertible(expr const & given, expr const & expected, context const & ctx, MkJustification const & mk_justification) { if (is_convertible_core(given, expected)) return true; - expr new_given = normalize(given, ctx); - expr new_expected = normalize(expected, ctx); + expr new_given = normalize(given, ctx, false); + expr new_expected = normalize(expected, ctx, false); if (is_convertible_core(new_given, new_expected)) return true; if (m_menv && m_uc && (has_metavar(new_given) || has_metavar(new_expected))) { m_uc->push_back(mk_convertible_constraint(ctx, given, expected, mk_justification())); return true; } + new_given = normalize(new_given, ctx, true); + new_expected = normalize(new_expected, ctx, true); + if (is_convertible_core(new_given, new_expected)) + return true; return false; } - void set_ctx(context const & ctx) { if (!is_eqp(m_ctx, ctx)) { clear(); diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 741900bc7..4c5502ea3 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -1,6 +1,6 @@ add_library(library kernel_bindings.cpp basic_thms.cpp deep_copy.cpp max_sharing.cpp context_to_lambda.cpp io_state.cpp type_inferer.cpp - placeholder.cpp expr_lt.cpp hidden_defs.cpp substitution.cpp + placeholder.cpp expr_lt.cpp substitution.cpp fo_unify.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/all/all.cpp b/src/library/all/all.cpp index 4fd71f7e3..d19c4711c 100644 --- a/src/library/all/all.cpp +++ b/src/library/all/all.cpp @@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "kernel/builtin.h" -#include "library/hidden_defs.h" #include "library/basic_thms.h" #include "library/arith/arith.h" #include "library/cast/cast.h" @@ -14,7 +13,6 @@ Author: Leonardo de Moura namespace lean { void import_all(environment const & env) { import_basic(env); - hide_builtin(env); import_basic_thms(env); import_cast(env); import_arith(env); diff --git a/src/library/arith/int.cpp b/src/library/arith/int.cpp index f2900a5f1..ac935276f 100644 --- a/src/library/arith/int.cpp +++ b/src/library/arith/int.cpp @@ -6,7 +6,6 @@ Author: Leonardo de Moura */ #include "kernel/abstract.h" #include "kernel/environment.h" -#include "library/hidden_defs.h" #include "library/kernel_bindings.h" #include "library/arith/int.h" #include "library/arith/nat.h" @@ -162,23 +161,17 @@ void import_int(environment const & env) { env->add_builtin(mk_int_le_fn()); env->add_builtin(mk_nat_to_int_fn()); - env->add_definition(int_sub_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iAdd(x, iMul(iVal(-1), y)))); - env->add_definition(int_neg_fn_name, i_i, Fun({x, Int}, iMul(iVal(-1), x))); - env->add_definition(int_mod_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iSub(x, iMul(y, iDiv(x, y))))); - env->add_definition(int_divides_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Eq(iMod(y, x), iVal(0)))); - env->add_definition(int_ge_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, iLe(y, x))); - env->add_definition(int_lt_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Not(iLe(y, x)))); - env->add_definition(int_gt_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Not(iLe(x, y)))); - env->add_definition(int_abs_fn_name, i_i, Fun({x, Int}, iIf(iLe(iVal(0), x), x, iNeg(x)))); + env->add_opaque_definition(int_sub_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iAdd(x, iMul(iVal(-1), y)))); + env->add_opaque_definition(int_neg_fn_name, i_i, Fun({x, Int}, iMul(iVal(-1), x))); + env->add_opaque_definition(int_mod_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iSub(x, iMul(y, iDiv(x, y))))); + env->add_opaque_definition(int_divides_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Eq(iMod(y, x), iVal(0)))); + env->add_opaque_definition(int_ge_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, iLe(y, x))); + env->add_opaque_definition(int_lt_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Not(iLe(y, x)))); + env->add_opaque_definition(int_gt_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Not(iLe(x, y)))); + env->add_opaque_definition(int_abs_fn_name, i_i, Fun({x, Int}, iIf(iLe(iVal(0), x), x, iNeg(x)))); - env->add_definition(nat_sub_fn_name, Nat >> (Nat >> Int), Fun({{x, Nat}, {y, Nat}}, iSub(n2i(x), n2i(y)))); - env->add_definition(nat_neg_fn_name, Nat >> Int, Fun({x, Nat}, iNeg(n2i(x)))); - - for (auto n : {int_sub_fn_name, int_neg_fn_name, int_mod_fn_name, int_divides_fn_name, - int_ge_fn_name, int_lt_fn_name, int_gt_fn_name, int_abs_fn_name, - nat_sub_fn_name, nat_neg_fn_name}) { - set_hidden_flag(env, n); - } + env->add_opaque_definition(nat_sub_fn_name, Nat >> (Nat >> Int), Fun({{x, Nat}, {y, Nat}}, iSub(n2i(x), n2i(y)))); + env->add_opaque_definition(nat_neg_fn_name, Nat >> Int, Fun({x, Nat}, iNeg(n2i(x)))); } static int mk_int_value(lua_State * L) { diff --git a/src/library/arith/nat.cpp b/src/library/arith/nat.cpp index 3e10f6a8a..0d0928c83 100644 --- a/src/library/arith/nat.cpp +++ b/src/library/arith/nat.cpp @@ -6,7 +6,6 @@ Author: Leonardo de Moura */ #include "kernel/abstract.h" #include "kernel/environment.h" -#include "library/hidden_defs.h" #include "library/kernel_bindings.h" #include "library/arith/nat.h" #include "library/arith/num_type.h" @@ -122,14 +121,10 @@ void import_nat(environment const & env) { env->add_builtin(mk_nat_mul_fn()); env->add_builtin(mk_nat_le_fn()); - env->add_definition(nat_ge_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, nLe(y, x))); - env->add_definition(nat_lt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(y, x)))); - env->add_definition(nat_gt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(x, y)))); - env->add_definition(nat_id_fn_name, Nat >> Nat, Fun({x, Nat}, x)); - - for (auto n : {nat_ge_fn_name, nat_lt_fn_name, nat_gt_fn_name, nat_id_fn_name}) { - set_hidden_flag(env, n); - } + env->add_opaque_definition(nat_ge_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, nLe(y, x))); + env->add_opaque_definition(nat_lt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(y, x)))); + env->add_opaque_definition(nat_gt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(x, y)))); + env->add_opaque_definition(nat_id_fn_name, Nat >> Nat, Fun({x, Nat}, x)); } static int mk_nat_value(lua_State * L) { diff --git a/src/library/arith/real.cpp b/src/library/arith/real.cpp index 5c2b08a8c..2e136608f 100644 --- a/src/library/arith/real.cpp +++ b/src/library/arith/real.cpp @@ -6,7 +6,6 @@ Author: Leonardo de Moura */ #include "kernel/abstract.h" #include "kernel/environment.h" -#include "library/hidden_defs.h" #include "library/kernel_bindings.h" #include "library/arith/real.h" #include "library/arith/int.h" @@ -149,17 +148,12 @@ void import_real(environment const & env) { env->add_builtin(mk_real_div_fn()); env->add_builtin(mk_real_le_fn()); - env->add_definition(real_sub_fn_name, rr_r, Fun({{x, Real}, {y, Real}}, rAdd(x, rMul(rVal(-1), y)))); - env->add_definition(real_neg_fn_name, r_r, Fun({x, Real}, rMul(rVal(-1), x))); - env->add_definition(real_abs_fn_name, r_r, Fun({x, Real}, rIf(rLe(rVal(0), x), x, rNeg(x)))); - env->add_definition(real_ge_fn_name, rr_b, Fun({{x, Real}, {y, Real}}, rLe(y, x))); - env->add_definition(real_lt_fn_name, rr_b, Fun({{x, Real}, {y, Real}}, Not(rLe(y, x)))); - env->add_definition(real_gt_fn_name, rr_b, Fun({{x, Real}, {y, Real}}, Not(rLe(x, y)))); - - for (auto n : {real_sub_fn_name, real_neg_fn_name, real_abs_fn_name, real_ge_fn_name, - real_lt_fn_name, real_gt_fn_name}) { - set_hidden_flag(env, n); - } + env->add_opaque_definition(real_sub_fn_name, rr_r, Fun({{x, Real}, {y, Real}}, rAdd(x, rMul(rVal(-1), y)))); + env->add_opaque_definition(real_neg_fn_name, r_r, Fun({x, Real}, rMul(rVal(-1), x))); + env->add_opaque_definition(real_abs_fn_name, r_r, Fun({x, Real}, rIf(rLe(rVal(0), x), x, rNeg(x)))); + env->add_opaque_definition(real_ge_fn_name, rr_b, Fun({{x, Real}, {y, Real}}, rLe(y, x))); + env->add_opaque_definition(real_lt_fn_name, rr_b, Fun({{x, Real}, {y, Real}}, Not(rLe(y, x)))); + env->add_opaque_definition(real_gt_fn_name, rr_b, Fun({{x, Real}, {y, Real}}, Not(rLe(x, y)))); } class int_to_real_value : public const_value { @@ -184,9 +178,7 @@ void import_int_to_real_coercions(environment const & env) { env->add_builtin(mk_int_to_real_fn()); expr x = Const("x"); - env->add_definition(nat_to_real_fn_name, Nat >> Real, Fun({x, Nat}, i2r(n2i(x)))); - - set_hidden_flag(env, nat_to_real_fn_name); + env->add_opaque_definition(nat_to_real_fn_name, Nat >> Real, Fun({x, Nat}, i2r(n2i(x)))); } static int mk_real_value(lua_State * L) { diff --git a/src/library/arith/special_fn.cpp b/src/library/arith/special_fn.cpp index a111673ad..8dbed647b 100644 --- a/src/library/arith/special_fn.cpp +++ b/src/library/arith/special_fn.cpp @@ -6,7 +6,6 @@ Author: Leonardo de Moura */ #include "kernel/environment.h" #include "kernel/abstract.h" -#include "library/hidden_defs.h" #include "library/arith/special_fn.h" #include "library/arith/real.h" @@ -43,24 +42,19 @@ void import_special_fn(environment const & env) { env->add_var(real_pi_name, Real); env->add_definition(name("pi"), Real, mk_real_pi()); // alias for pi env->add_var(sin_fn_name, r_r); - env->add_definition(cos_fn_name, r_r, Fun({x, Real}, Sin(rSub(x, rDiv(mk_real_pi(), rVal(2)))))); - env->add_definition(tan_fn_name, r_r, Fun({x, Real}, rDiv(Sin(x), Cos(x)))); - env->add_definition(cot_fn_name, r_r, Fun({x, Real}, rDiv(Cos(x), Sin(x)))); - env->add_definition(sec_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Cos(x)))); - env->add_definition(csc_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Sin(x)))); + env->add_opaque_definition(cos_fn_name, r_r, Fun({x, Real}, Sin(rSub(x, rDiv(mk_real_pi(), rVal(2)))))); + env->add_opaque_definition(tan_fn_name, r_r, Fun({x, Real}, rDiv(Sin(x), Cos(x)))); + env->add_opaque_definition(cot_fn_name, r_r, Fun({x, Real}, rDiv(Cos(x), Sin(x)))); + env->add_opaque_definition(sec_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Cos(x)))); + env->add_opaque_definition(csc_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Sin(x)))); - env->add_definition(sinh_fn_name, r_r, Fun({x, Real}, rDiv(rSub(rVal(1), Exp(rMul(rVal(-2), x))), + env->add_opaque_definition(sinh_fn_name, r_r, Fun({x, Real}, rDiv(rSub(rVal(1), Exp(rMul(rVal(-2), x))), rMul(rVal(2), Exp(rNeg(x)))))); - env->add_definition(cosh_fn_name, r_r, Fun({x, Real}, rDiv(rAdd(rVal(1), Exp(rMul(rVal(-2), x))), + env->add_opaque_definition(cosh_fn_name, r_r, Fun({x, Real}, rDiv(rAdd(rVal(1), Exp(rMul(rVal(-2), x))), rMul(rVal(2), Exp(rNeg(x)))))); - env->add_definition(tanh_fn_name, r_r, Fun({x, Real}, rDiv(Sinh(x), Cosh(x)))); - env->add_definition(coth_fn_name, r_r, Fun({x, Real}, rDiv(Cosh(x), Sinh(x)))); - env->add_definition(sech_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Cosh(x)))); - env->add_definition(csch_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Sinh(x)))); - - for (auto n : {cos_fn_name, tan_fn_name, cot_fn_name, sec_fn_name, csc_fn_name, sinh_fn_name, - cosh_fn_name, tanh_fn_name, coth_fn_name, sech_fn_name, csch_fn_name}) { - set_hidden_flag(env, n); - } + env->add_opaque_definition(tanh_fn_name, r_r, Fun({x, Real}, rDiv(Sinh(x), Cosh(x)))); + env->add_opaque_definition(coth_fn_name, r_r, Fun({x, Real}, rDiv(Cosh(x), Sinh(x)))); + env->add_opaque_definition(sech_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Cosh(x)))); + env->add_opaque_definition(csch_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Sinh(x)))); } } diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 4efea6f37..c348036f8 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -19,7 +19,6 @@ Author: Leonardo de Moura #include "kernel/replace_fn.h" #include "kernel/builtin.h" #include "kernel/update_expr.h" -#include "library/hidden_defs.h" #include "library/type_inferer.h" #include "library/elaborator/elaborator.h" #include "library/elaborator/elaborator_justification.h" @@ -627,7 +626,7 @@ class elaborator::imp { int get_const_weight(expr const & a) { lean_assert(is_constant(a)); optional obj = m_env->find_object(const_name(a)); - if (obj && obj->is_definition() && !obj->is_opaque() && !is_hidden(m_env, const_name(a))) + if (should_unfold(obj)) return obj->get_weight(); else return -1; diff --git a/src/library/hidden_defs.cpp b/src/library/hidden_defs.cpp deleted file mode 100644 index 28180f9fe..000000000 --- a/src/library/hidden_defs.cpp +++ /dev/null @@ -1,87 +0,0 @@ -/* -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 "util/name.h" -#include "util/sstream.h" -#include "util/name_map.h" -#include "kernel/environment.h" -#include "kernel/builtin.h" -#include "library/hidden_defs.h" -#include "library/kernel_bindings.h" - -namespace lean { -struct hidden_defs_extension : public environment_extension { - typedef name_map hidden_defs; - hidden_defs m_hidden_defs; - - hidden_defs_extension const * get_parent() const { - return environment_extension::get_parent(); - } - - bool is_hidden(name const & n) const { - auto it = m_hidden_defs.find(n); - if (it != m_hidden_defs.end()) - return it->second; - hidden_defs_extension const * parent = get_parent(); - return parent && parent->is_hidden(n); - } - - void set_hidden_flag(name const & d, bool f) { - m_hidden_defs[d] = f; - } -}; - -struct hidden_defs_extension_initializer { - unsigned m_extid; - hidden_defs_extension_initializer() { - m_extid = environment_cell::register_extension([](){ return std::unique_ptr(new hidden_defs_extension()); }); - } -}; - -static hidden_defs_extension_initializer g_hidden_defs_extension_initializer; - -static hidden_defs_extension const & to_ext(ro_environment const & env) { - return env->get_extension(g_hidden_defs_extension_initializer.m_extid); -} - -static hidden_defs_extension & to_ext(environment const & env) { - return env->get_extension(g_hidden_defs_extension_initializer.m_extid); -} - -bool is_hidden(ro_environment const & env, name const & d) { - return to_ext(env).is_hidden(d); -} - -void set_hidden_flag(environment const & env, name const & d, bool flag) { - if (!env->get_object(d).is_definition()) - throw exception(sstream() << "'" << d << "' is not a definition"); - to_ext(env).set_hidden_flag(d, flag); -} - -void hide_builtin(environment const & env) { - for (auto c : { mk_implies_fn(), mk_iff_fn(), mk_not_fn(), mk_or_fn(), mk_and_fn(), - mk_forall_fn() }) - set_hidden_flag(env, const_name(c)); -} - -static int is_hidden(lua_State * L) { - ro_shared_environment env(L, 1); - lua_pushboolean(L, is_hidden(env, to_name_ext(L, 2))); - return 1; -} - -static int set_hidden_flag(lua_State * L) { - int nargs = lua_gettop(L); - rw_shared_environment env(L, 1); - set_hidden_flag(env, to_name_ext(L, 2), nargs <= 2 ? true : lua_toboolean(L, 3)); - return 0; -} - -void open_hidden_defs(lua_State * L) { - SET_GLOBAL_FUN(is_hidden, "is_hidden"); - SET_GLOBAL_FUN(set_hidden_flag, "set_hidden_flag"); -} -} diff --git a/src/library/hidden_defs.h b/src/library/hidden_defs.h deleted file mode 100644 index 588c69a7e..000000000 --- a/src/library/hidden_defs.h +++ /dev/null @@ -1,37 +0,0 @@ -/* -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 -#include "util/lua.h" -namespace lean { -class environment; -class ro_environment; -class name; -/** - \brief Return true iff the definition named \c d is hidden in - the given environment. - - This information is just a hint used by tactics and solvers. For - example, unfold_tactic uses it to decide whether a definition - should be unfolded or not. -*/ -bool is_hidden(ro_environment const & env, name const & d); -/** - \brief Mark the definition named \c d as hidden in the given environment. - - \see is_hidden - - \remark It throws an exception if \c d is not a definition in \c env. -*/ -void set_hidden_flag(environment const & env, name const & d, bool flag = true); -/** - \brief Hide definitions at builtin.cpp. We hide them here because - the hidden_defs module is not part of the kernel. -*/ -void hide_builtin(environment const & env); - -void open_hidden_defs(lua_State * L); -} diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index cc86d2341..1e5c49066 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -1121,6 +1121,19 @@ static int environment_tostring(lua_State * L) { return 1; } +static int environment_set_opaque(lua_State * L) { + rw_shared_environment env(L, 1); + env->set_opaque(to_name_ext(L, 2), lua_toboolean(L, 3)); + return 0; +} + +static int environment_is_opaque(lua_State * L) { + ro_shared_environment env(L, 1); + auto obj = env->find_object(to_name_ext(L, 2)); + lua_pushboolean(L, obj && obj->is_opaque()); + return 1; +} + static const struct luaL_Reg environment_m[] = { {"__gc", environment_gc}, // never throws {"__tostring", safe_function}, @@ -1142,6 +1155,8 @@ static const struct luaL_Reg environment_m[] = { {"normalize", safe_function}, {"objects", safe_function}, {"local_objects", safe_function}, + {"set_opaque", safe_function}, + {"is_opaque", safe_function}, {0, 0} }; diff --git a/src/library/register_module.h b/src/library/register_module.h index a668791b7..9ee5685ab 100644 --- a/src/library/register_module.h +++ b/src/library/register_module.h @@ -9,7 +9,6 @@ Author: Leonardo de Moura #include "library/kernel_bindings.h" #include "library/io_state.h" #include "library/type_inferer.h" -#include "library/hidden_defs.h" #include "library/substitution.h" #include "library/fo_unify.h" #include "library/placeholder.h" @@ -19,7 +18,6 @@ inline void open_core_module(lua_State * L) { open_kernel_module(L); open_io_state(L); open_type_inferer(L); - open_hidden_defs(L); open_substitution(L); open_fo_unify(L); open_placeholder(L); diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index d7720a4c1..0a866ee09 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -15,7 +15,6 @@ Author: Leonardo de Moura #include "kernel/replace_visitor.h" #include "kernel/instantiate.h" #include "kernel/update_expr.h" -#include "library/hidden_defs.h" #include "library/kernel_bindings.h" #include "library/tactic/tactic.h" @@ -397,7 +396,7 @@ protected: virtual expr visit_constant(expr const & c, context const &) { optional obj = m_env->find_object(const_name(c)); - if (obj && obj->is_definition() && !obj->is_opaque() && !is_hidden(m_env, const_name(c))) { + if (should_unfold(obj)) { m_unfolded = true; return obj->get_value(); } else { diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h index 1e44e154b..53b66a6a5 100644 --- a/src/library/tactic/tactic.h +++ b/src/library/tactic/tactic.h @@ -294,7 +294,7 @@ inline tactic focus(tactic const & t) { return focus(t, 1); } */ tactic unfold_tactic(name const & n); /** - \brief Return a tactic that unfolds all (non-hidden and non-opaque) definitions. + \brief Return a tactic that unfolds all (non-opaque) definitions. */ tactic unfold_tactic(); /** diff --git a/src/library/type_inferer.cpp b/src/library/type_inferer.cpp index 8ea0523df..1cb361d2d 100644 --- a/src/library/type_inferer.cpp +++ b/src/library/type_inferer.cpp @@ -32,8 +32,8 @@ class type_inferer::imp { normalizer m_normalizer; cache m_cache; - expr normalize(expr const & e, context const & ctx) { - return m_normalizer(e, ctx, m_menv.to_some_menv()); + expr normalize(expr const & e, context const & ctx, bool unfold_opaque) { + return m_normalizer(e, ctx, m_menv.to_some_menv(), unfold_opaque); } expr lift_free_vars(expr const & e, unsigned s, unsigned d) { return ::lean::lift_free_vars(e, s, d, m_menv.to_some_menv()); @@ -52,7 +52,7 @@ class type_inferer::imp { return e; if (is_bool(e)) return Type(); - expr u = normalize(e, ctx); + expr u = normalize(e, ctx, false); if (is_type(u)) return u; if (is_bool(u)) @@ -62,6 +62,11 @@ class type_inferer::imp { m_uc->push_back(mk_convertible_constraint(ctx, u, TypeU, jst)); return u; } + u = normalize(e, ctx, true); + if (is_type(u)) + return u; + if (is_bool(u)) + return Type(); throw type_expected_exception(m_env, ctx, s); } @@ -72,7 +77,7 @@ class type_inferer::imp { if (is_pi(t)) { t = abst_body(t); } else { - t = m_normalizer(t, ctx); + t = normalize(t, ctx, false); if (is_pi(t)) { t = abst_body(t); } else if (has_metavar(t) && m_menv && m_uc) { @@ -85,7 +90,12 @@ class type_inferer::imp { m_uc->push_back(mk_eq_constraint(ctx, t, p, jst)); t = abst_body(p); } else { - throw function_expected_exception(m_env, ctx, e); + t = normalize(t, ctx, true); + if (is_pi(t)) { + t = abst_body(t); + } else { + throw function_expected_exception(m_env, ctx, e); + } } } } @@ -249,7 +259,7 @@ public: if (is_bool(t)) return true; else - return is_bool(normalize(t, ctx)); + return is_bool(normalize(t, ctx, true)); } }; type_inferer::type_inferer(ro_environment const & env):m_ptr(new imp(env)) {} diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index 4025fa2c1..374ab09c6 100644 --- a/src/tests/kernel/environment.cpp +++ b/src/tests/kernel/environment.cpp @@ -121,7 +121,8 @@ static void tst4() { env->add_definition("b", Int, iAdd(Const("a"), iVal(1))); expr t2 = iSub(Const("b"), iVal(9)); std::cout << t2 << " --> " << normalize(t2, env) << "\n"; - lean_assert(normalize(t2, env) == iAdd(iAdd(Const("a"), iVal(1)), iVal(-9))); + lean_assert_eq(normalize(t2, env, context()), + iSub(iAdd(Const("a"), iVal(1)), iVal(9))); } static void tst5() { diff --git a/src/tests/library/arith.cpp b/src/tests/library/arith.cpp index a4f6b4879..bbf71aa2b 100644 --- a/src/tests/library/arith.cpp +++ b/src/tests/library/arith.cpp @@ -95,15 +95,15 @@ static void tst4() { expr e = iSub(iVal(10), iVal(30)); std::cout << e << "\n"; std::cout << normalize(e, env) << "\n"; - lean_assert(normalize(e, env) == iVal(-20)); + lean_assert(normalize(e, env, context(), true) == iVal(-20)); std::cout << infer_type(mk_int_sub_fn(), env) << "\n"; lean_assert(infer_type(e, env) == Int); lean_assert(infer_type(mk_app(mk_int_sub_fn(), iVal(10)), env) == mk_arrow(Int, Int)); - lean_assert(is_int_value(normalize(e, env))); + lean_assert(is_int_value(normalize(e, env, context(), true))); expr e2 = Fun("a", Int, iSub(Const("a"), iSub(iVal(10), iVal(30)))); std::cout << e2 << " --> " << normalize(e2, env) << "\n"; lean_assert(infer_type(e2, env) == (Int >> Int)); - lean_assert(normalize(e2, env) == Fun("a", Int, iAdd(Const("a"), iVal(20)))); + lean_assert_eq(normalize(e2, env, context(), true), Fun("a", Int, iAdd(Const("a"), iVal(20)))); } static void tst5() { diff --git a/tests/lean/interactive/elab6.lean b/tests/lean/interactive/elab6.lean index 9cf23fdbd..339fc7e5f 100644 --- a/tests/lean/interactive/elab6.lean +++ b/tests/lean/interactive/elab6.lean @@ -1,9 +1,9 @@ (** --- The elaborator does not expand definitions marked as 'hidden'. +-- The elaborator does not expand definitions marked as 'opaque'. -- To be able to prove the following theorem, we have to unmark the -- 'forall' local env = get_environment() -set_hidden_flag(env, "forall", false) +env:set_opaque("forall", false) **) Theorem ForallIntro2 (A : (Type U)) (P : A -> Bool) (H : Pi x, P x) : forall x, P x := Abst (fun x, EqTIntro (H x)) diff --git a/tests/lua/hidden1.lua b/tests/lua/hidden1.lua index 2927aaa85..4222bac49 100644 --- a/tests/lua/hidden1.lua +++ b/tests/lua/hidden1.lua @@ -1,14 +1,13 @@ local env = environment() -assert(is_hidden(env, "and")) -assert(is_hidden(env, "or")) -assert(is_hidden(env, {"Int", "lt"})) +assert(env:is_opaque("and")) +assert(env:is_opaque("or")) +assert(env:is_opaque({"Int", "lt"})) parse_lean_cmds([[ Definition a : Bool := true ]], env) -assert(not is_hidden(env, "a")) -set_hidden_flag(env, "a") -assert(is_hidden(env, "a")) -set_hidden_flag(env, "a", false) -assert(not is_hidden(env, "a")) -assert(not is_hidden(env, "b")) -assert(not pcall(function () set_hidden_flag(env, "b") end)) +assert(not env:is_opaque("a")) +env:set_opaque("a", true) +assert(env:is_opaque("a")) +env:set_opaque("a", false) +assert(not env:is_opaque("a")) +assert(not env:is_opaque("b"))