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

feat(kernel/converter): more cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-07 19:19:01 -08:00
parent 73acaca21e
commit 4c2277fccf
3 changed files with 19 additions and 49 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

57
src/kernel/converter.cpp
View file

@ -24,65 +24,44 @@ namespace lean {
We also believe it increases the modularity of Lean developments by minimizing the dependency on how things are defined. We also believe it increases the modularity of Lean developments by minimizing the dependency on how things are defined.
We should view non-opaque definitions as "inline definitions" used in programming languages such as C++. We should view non-opaque definitions as "inline definitions" used in programming languages such as C++.
2) Whenever type checking an expression, the user can provide a predicate that is true for for additional definitions that 2) To be able to prove theorems about an opaque definition, we treat an opaque definition D in a module M as
should be considered opaque. Note that, if \c t type checks when using predicate P, then t also type checks
(modulo resource constraints) without it. Again, the purpose of the predicate is to mimimize the number
of delta-reduction steps.
3) To be able to prove theorems about an opaque definition, we treat an opaque definition D in a module M as
transparent when we are type checking another definition/theorem D' also in M. This rule only applies if transparent when we are type checking another definition/theorem D' also in M. This rule only applies if
D is not a theorem, nor pred(D) is true. To implement this feature, this class has a field D is not a theorem, nor pred(D) is true. To implement this feature, this class has a field
m_module_idx that is not none when this rule should be applied. m_module_idx that is not none when this rule should be applied.
*/ */
bool is_opaque(declaration const & d, extra_opaque_pred const & pred, optional<module_idx> const & mod_idx) { bool is_opaque(declaration const & d, optional<module_idx> const & mod_idx) {
lean_assert(d.is_definition()); lean_assert(d.is_definition());
if (d.is_theorem()) return true; // theorems are always opaque if (d.is_theorem()) return true; // theorems are always opaque
if (pred(d.get_name())) return true; // extra_opaque predicate overrides opaque flag
if (!d.is_opaque()) return false; // d is a transparent definition if (!d.is_opaque()) return false; // d is a transparent definition
if (mod_idx && d.get_module_idx() == *mod_idx) return false; // the opaque definitions in mod_idx are considered transparent if (mod_idx && d.get_module_idx() == *mod_idx) return false; // the opaque definitions in mod_idx are considered transparent
return true; // d is opaque return true; // d is opaque
} }
extra_opaque_pred g_always_false([](name const &) { return false; }); static optional<module_idx> * g_opt_main_module_idx = nullptr;
extra_opaque_pred const & no_extra_opaque() {
return g_always_false;
}
/** \brief Auxiliary method for \c is_delta */ optional<declaration> is_delta(environment const & env, expr const & e) {
static optional<declaration> is_delta_core(environment const & env, expr const & e, extra_opaque_pred const & pred, expr const & f = get_app_fn(e);
optional<module_idx> const & mod_idx) { if (is_constant(f)) {
if (is_constant(e)) { if (auto d = env.find(const_name(f)))
if (auto d = env.find(const_name(e))) if (d->is_definition() && !is_opaque(*d, *g_opt_main_module_idx))
if (d->is_definition() && !is_opaque(*d, pred, mod_idx))
return d; return d;
} }
return none_declaration(); return none_declaration();
} }
/**
\brief Return some definition \c d iff \c e is a target for delta-reduction, and the given definition is the one
to be expanded.
*/
optional<declaration> is_delta(environment const & env, expr const & e,
extra_opaque_pred const & pred, optional<module_idx> const & mod_idx) {
return is_delta_core(env, get_app_fn(e), pred, mod_idx);
}
static optional<module_idx> * g_opt_main_module_idx = nullptr;
optional<declaration> is_delta(environment const & env, expr const & e, extra_opaque_pred const & pred) {
return is_delta(env, e, pred, *g_opt_main_module_idx);
}
optional<declaration> is_delta(environment const & env, expr const & e) {
return is_delta(env, e, g_always_false);
}
static no_delayed_justification * g_no_delayed_jst = nullptr; static no_delayed_justification * g_no_delayed_jst = nullptr;
pair<bool, constraint_seq> converter::is_def_eq(expr const & t, expr const & s, type_checker & c) { pair<bool, constraint_seq> converter::is_def_eq(expr const & t, expr const & s, type_checker & c) {
return is_def_eq(t, s, c, *g_no_delayed_jst); return is_def_eq(t, s, c, *g_no_delayed_jst);
} }
name converter::mk_fresh_name(type_checker & tc) { return tc.mk_fresh_name(); }
pair<expr, constraint_seq> converter::infer_type(type_checker & tc, expr const & e) { return tc.infer_type(e); }
extension_context & converter::get_extension(type_checker & tc) { return tc.get_extension(); }
/** \brief Do nothing converter */ /** \brief Do nothing converter */
struct dummy_converter : public converter { struct dummy_converter : public converter {
virtual pair<expr, constraint_seq> whnf(expr const & e, type_checker &) { virtual pair<expr, constraint_seq> whnf(expr const & e, type_checker &) {
@ -99,10 +78,6 @@ std::unique_ptr<converter> mk_dummy_converter() {
return std::unique_ptr<converter>(new dummy_converter()); return std::unique_ptr<converter>(new dummy_converter());
} }
name converter::mk_fresh_name(type_checker & tc) { return tc.mk_fresh_name(); }
pair<expr, constraint_seq> converter::infer_type(type_checker & tc, expr const & e) { return tc.infer_type(e); }
extension_context & converter::get_extension(type_checker & tc) { return tc.get_extension(); }
void initialize_converter() { void initialize_converter() {
g_opt_main_module_idx = new optional<module_idx>(g_main_module_idx); g_opt_main_module_idx = new optional<module_idx>(g_main_module_idx);
g_no_delayed_jst = new no_delayed_justification(); g_no_delayed_jst = new no_delayed_justification();

5
src/kernel/converter.h
View file

@ -27,9 +27,8 @@ public:
std::unique_ptr<converter> mk_dummy_converter(); std::unique_ptr<converter> mk_dummy_converter();
bool is_opaque(declaration const & d, extra_opaque_pred const & pred, optional<module_idx> const & mod_idx); /** \brief Default procedure for deciding whether a declaration is opaque or not */
optional<declaration> is_delta(environment const & env, expr const & e, extra_opaque_pred const & pred, optional<module_idx> const & mod_idx); bool is_opaque(declaration const & d, optional<module_idx> const & mod_idx);
optional<declaration> is_delta(environment const & env, expr const & e, extra_opaque_pred const & pred);
optional<declaration> is_delta(environment const & env, expr const & e); optional<declaration> is_delta(environment const & env, expr const & e);
void initialize_converter(); void initialize_converter();

6
src/kernel/default_converter.cpp
View file

@ -108,11 +108,7 @@ expr default_converter::whnf_core(expr const & e) {
} }
bool default_converter::is_opaque(declaration const & d) const { bool default_converter::is_opaque(declaration const & d) const {
lean_assert(d.is_definition()); return ::lean::is_opaque(d, m_module_idx);
if (d.is_theorem()) return true; // theorems are always opaque
if (!d.is_opaque()) return false; // d is a transparent definition
if (m_module_idx && d.get_module_idx() == *m_module_idx) return false; // the opaque definitions in mod_idx are considered transparent
return true; // d is opaque
} }
/** \brief Expand \c e if it is non-opaque constant with weight >= w */ /** \brief Expand \c e if it is non-opaque constant with weight >= w */