michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

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

Browse source 
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 <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-20 12:47:36 -08:00
parent 026f666526
commit 7772c16033
26 changed files with 151 additions and 244 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/parser.cpp
View file

@ -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;
}

12
src/kernel/builtin.cpp
View file

@ -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)))))));

4
src/kernel/environment.cpp
View file

@ -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. */

5
src/kernel/environment.h
View file

@ -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.

25
src/kernel/normalizer.cpp
View file

@ -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<cache> 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<metavar_env> const & menv) {
expr operator()(expr const & e, context const & ctx, optional<metavar_env> 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<unsigned>::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<metavar_env> 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<metavar_env> 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);
}
}

8
src/kernel/normalizer.h
View file

@ -24,12 +24,12 @@ public:
normalizer(ro_environment const & env, options const & opts);
~normalizer();
expr operator()(expr const & e, context const & ctx, optional<metavar_env> 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<metavar_env> 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);
}

17
src/kernel/object.h
View file

@ -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<object> const & obj, bool unfold_opaque) {
return obj && should_unfold(*obj, unfold_opaque);
}
inline bool should_unfold(optional<object> const & obj) {
return should_unfold(obj, false);
}
}

25
src/kernel/type_checker.cpp
View file

@ -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();

2
src/library/CMakeLists.txt
View file

@ -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})

2
src/library/all/all.cpp
View file

@ -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);

27
src/library/arith/int.cpp
View file

@ -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) {

13
src/library/arith/nat.cpp
View file

@ -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) {

22
src/library/arith/real.cpp
View file

@ -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) {

28
src/library/arith/special_fn.cpp
View file

@ -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))));
}
}

3
src/library/elaborator/elaborator.cpp
View file

@ -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<object> 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;

87
src/library/hidden_defs.cpp
View file

@ -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<bool> hidden_defs;
hidden_defs m_hidden_defs;
hidden_defs_extension const * get_parent() const {
return environment_extension::get_parent<hidden_defs_extension>();
}
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<environment_extension>(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<hidden_defs_extension>(g_hidden_defs_extension_initializer.m_extid);
}
static hidden_defs_extension & to_ext(environment const & env) {
return env->get_extension<hidden_defs_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");
}
}

37
src/library/hidden_defs.h
View file

@ -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);
}

15
src/library/kernel_bindings.cpp
View file

@ -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<environment_tostring>},
@ -1142,6 +1155,8 @@ static const struct luaL_Reg environment_m[] = {
{"normalize", safe_function<environment_normalize>},
{"objects", safe_function<environment_objects>},
{"local_objects", safe_function<environment_local_objects>},
{"set_opaque", safe_function<environment_set_opaque>},
{"is_opaque", safe_function<environment_is_opaque>},
{0, 0}
};

2
src/library/register_module.h
View file

@ -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);

3
src/library/tactic/tactic.cpp
View file

@ -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<object> 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 {

2
src/library/tactic/tactic.h
View file

@ -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();
/**

22
src/library/type_inferer.cpp
View file

@ -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)) {}

3
src/tests/kernel/environment.cpp
View file

@ -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() {

6
src/tests/library/arith.cpp
View file

@ -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() {

4
tests/lean/interactive/elab6.lean
View file

@ -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))

19
tests/lua/hidden1.lua
View file

@ -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"))