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

refactor(*): remove transparent_scope hack, replace [strict] with [all-transparent] annotation

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-07 15:19:41 -08:00
parent 7945b8adab
commit c04c0e8381
12 changed files with 44 additions and 41 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/emacs/lean-syntax.el
View file

@ -118,7 +118,7 @@
;; modifiers
(,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[instance\]" "\[class\]" "\[parsing-only\]"
"\[coercion\]" "\[reducible\]" "\[irreducible\]" "\[wf\]" "\[whnf\]" "\[multiple-instances\]"
"\[decls\]" "\[strict\]" "\[coercions\]" "\[classes\]" "\[notations\]" "\[tactic_hints\]" "\[reduce_hints\]"))
"\[decls\]" "\[all-transparent\]" "\[coercions\]" "\[classes\]" "\[notations\]" "\[tactic_hints\]" "\[reduce_hints\]"))
. 'font-lock-doc-face)
(,(rx "\[priority" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face)
(,(rx "\[unfold-c" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face)

24
src/frontends/lean/builtin_cmds.cpp
View file

@ -12,6 +12,7 @@ Author: Leonardo de Moura
#include "kernel/abstract.h"
#include "kernel/instantiate.h"
#include "kernel/inductive/inductive.h"
#include "kernel/default_converter.h"
#include "library/io_state_stream.h"
#include "library/scoped_ext.h"
#include "library/aliases.h"
@ -322,15 +323,25 @@ environment check_cmd(parser & p) {
return p.env();
}
class all_transparent_converter : public default_converter {
public:
all_transparent_converter(environment const & env):
default_converter(env, optional<module_idx>(), true) {
}
virtual bool is_opaque(declaration const &) const {
return false;
}
};
environment eval_cmd(parser & p) {
bool whnf = false;
bool strict = false;
bool all_transparent = false;
if (p.curr_is_token(get_whnf_tk())) {
p.next();
whnf = true;
} else if (p.curr_is_token(get_strict_tk())) {
} else if (p.curr_is_token(get_all_transparent_tk())) {
p.next();
strict = true;
all_transparent = true;
}
expr e; level_param_names ls;
std::tie(e, ls) = parse_local_expr(p);
@ -338,10 +349,11 @@ environment eval_cmd(parser & p) {
if (whnf) {
auto tc = mk_type_checker(p.env(), p.mk_ngen(), true);
r = tc->whnf(e).first;
} else if (strict) {
r = normalize(p.env(), ls, e);
} else if (all_transparent) {
type_checker tc(p.env(), name_generator(),
std::unique_ptr<converter>(new all_transparent_converter(p.env())));
r = normalize(tc, ls, e);
} else {
transparent_scope scope;
r = normalize(p.env(), ls, e);
}
flycheck_information info(p.regular_stream());

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

@ -90,7 +90,7 @@ void init_token_table(token_table & t) {
{"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "example", "coercion",
"variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]",
"[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[parsing-only]", "[multiple-instances]",
"evaluate", "check", "eval", "[wf]", "[whnf]", "[strict]", "[priority", "[unfold-c", "print", "end", "namespace", "section", "prelude",
"evaluate", "check", "eval", "[wf]", "[whnf]", "[all-transparent]", "[priority", "[unfold-c", "print", "end", "namespace", "section", "prelude",
"import", "inductive", "record", "structure", "module", "universe", "universes", "local",
"precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
"exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint",

8
src/frontends/lean/tokens.cpp
View file

@ -71,7 +71,7 @@ static name * g_off = nullptr;
static name * g_none = nullptr;
static name * g_whnf = nullptr;
static name * g_wf = nullptr;
static name * g_strict = nullptr;
static name * g_all_transparent = nullptr;
static name * g_in = nullptr;
static name * g_at = nullptr;
static name * g_assign = nullptr;
@ -187,7 +187,7 @@ void initialize_tokens() {
g_none = new name("[none]");
g_whnf = new name("[whnf]");
g_wf = new name("[wf]");
g_strict = new name("[strict]");
g_all_transparent = new name("[all-transparent]");
g_in = new name("in");
g_at = new name("at");
g_assign = new name(":=");
@ -309,7 +309,7 @@ void finalize_tokens() {
delete g_none;
delete g_whnf;
delete g_wf;
delete g_strict;
delete g_all_transparent;
delete g_ellipsis;
delete g_fun;
delete g_take;
@ -420,7 +420,7 @@ name const & get_off_tk() { return *g_off; }
name const & get_none_tk() { return *g_none; }
name const & get_whnf_tk() { return *g_whnf; }
name const & get_wf_tk() { return *g_wf; }
name const & get_strict_tk() { return *g_strict; }
name const & get_all_transparent_tk() { return *g_all_transparent; }
name const & get_in_tk() { return *g_in; }
name const & get_at_tk() { return *g_at; }
name const & get_assign_tk() { return *g_assign; }

2
src/frontends/lean/tokens.h
View file

@ -73,7 +73,7 @@ name const & get_off_tk();
name const & get_none_tk();
name const & get_whnf_tk();
name const & get_wf_tk();
name const & get_strict_tk();
name const & get_all_transparent_tk();
name const & get_in_tk();
name const & get_at_tk();
name const & get_assign_tk();

11
src/kernel/converter.cpp
View file

@ -14,16 +14,6 @@ Author: Leonardo de Moura
#include "kernel/default_converter.h"
namespace lean {
// Temporary hack for ignoring opaque annotations in the kernel
LEAN_THREAD_VALUE(unsigned, g_everything_transparent, false);
transparent_scope::transparent_scope():m_old_value(g_everything_transparent) {
g_everything_transparent = true;
}
transparent_scope::~transparent_scope() {
g_everything_transparent = m_old_value;
}
/**
\brief Predicate for deciding whether \c d is an opaque definition or not.
@ -46,7 +36,6 @@ transparent_scope::~transparent_scope() {
*/
bool is_opaque(declaration const & d, extra_opaque_pred const & pred, optional<module_idx> const & mod_idx) {
lean_assert(d.is_definition());
if (g_everything_transparent) return false; // temporary hack
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

8
src/kernel/converter.h
View file

@ -25,14 +25,6 @@ public:
pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, type_checker & c);
};
/** \brief Temporary hack for creating a scope where the opaque annotations are ignored in the kernel. */
class transparent_scope {
bool m_old_value;
public:
transparent_scope();
~transparent_scope();
};
std::unique_ptr<converter> mk_dummy_converter();
std::unique_ptr<converter> mk_default_converter(environment const & env, optional<module_idx> mod_idx = optional<module_idx>(),
bool memoize = true);

18
src/kernel/default_converter.cpp
View file

@ -21,6 +21,9 @@ default_converter::default_converter(environment const & env, optional<module_id
m_jst = nullptr;
}
default_converter::default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize):
default_converter(env, mod_idx, memoize, [](name const &) { return false; }) {}
constraint default_converter::mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j) {
return ::lean::mk_eq_cnstr(lhs, rhs, j, static_cast<bool>(m_module_idx));
}
@ -105,19 +108,20 @@ expr default_converter::whnf_core(expr const & e) {
return r;
}
bool default_converter::is_opaque_core(declaration const & d) const {
return ::lean::is_opaque(d, m_extra_pred, m_module_idx);
}
bool default_converter::is_opaque(declaration const & d) const {
return is_opaque_core(d);
lean_assert(d.is_definition());
if (d.is_theorem()) return true; // theorems are always opaque
if (m_extra_pred(d.get_name())) return true; // extra_opaque predicate overrides opaque flag
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 */
expr default_converter::unfold_name_core(expr e, unsigned w) {
if (is_constant(e)) {
if (auto d = m_env.find(const_name(e))) {
if (d->is_definition() && !is_opaque_core(*d) && d->get_weight() >= w)
if (d->is_definition() && !is_opaque(*d) && d->get_weight() >= w)
return unfold_name_core(instantiate_value_univ_params(*d, const_levels(e)), w);
}
}
@ -472,7 +476,7 @@ pair<bool, constraint_seq> default_converter::is_def_eq(expr const & t, expr con
// If they are, then t_n and s_n must be definitionally equal, and we can
// skip the delta-reduction step.
// If the flag use_conv_opt() is not true, then we skip this optimization
if (!is_opaque_core(*d_t) && d_t->use_conv_opt() &&
if (!is_opaque(*d_t) && d_t->use_conv_opt() &&
is_def_eq_args(t_n, s_n, cs))
return to_bcs(true, cs);
}

2
src/kernel/default_converter.h
View file

@ -35,7 +35,6 @@ protected:
optional<pair<expr, constraint_seq>> norm_ext(expr const & e);
optional<expr> d_norm_ext(expr const & e, constraint_seq & cs);
expr whnf_core(expr const & e);
bool is_opaque_core(declaration const & d) const;
expr unfold_name_core(expr e, unsigned w);
expr unfold_names(expr const & e, unsigned w);
optional<declaration> is_delta(expr const & e);
@ -75,6 +74,7 @@ protected:
public:
default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize,
extra_opaque_pred const & pred);
default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize);
virtual bool is_opaque(declaration const & d) const;
virtual optional<module_idx> get_module_idx() const { return m_module_idx; }

5
src/library/normalize.cpp
View file

@ -199,6 +199,11 @@ expr normalize(type_checker & tc, expr const & e) {
return normalize_fn(tc, save_cnstrs)(e);
}
expr normalize(type_checker & tc, level_param_names const & ls, expr const & e) {
bool save_cnstrs = false;
return normalize_fn(tc, save_cnstrs)(ls, e);
}
expr normalize(type_checker & tc, expr const & e, constraint_seq & cs) {
normalize_fn fn(tc);
expr r = fn(e);

1
src/library/normalize.h
View file

@ -19,6 +19,7 @@ expr normalize(environment const & env, level_param_names const & ls, expr const
/** \brief Similar to <tt>expr normalize(environment const & env, expr const & e)</tt>, but
uses the converter associated with \c tc. */
expr normalize(type_checker & tc, expr const & e);
expr normalize(type_checker & tc, level_param_names const & ls, expr const & e);
/** \brief Return the \c e normal form with respect to \c tc, and store generated constraints
into \c cs.
*/

2
tests/lean/eta_bug.lean
View file

@ -1,4 +1,4 @@
import logic
eval λ (A : Type) (x y : A) (H₁ : x = y) (H₂ : y = x), eq.trans H₁ H₂
eval [all-transparent] λ (A : Type) (x y : A) (H₁ : x = y) (H₂ : y = x), eq.trans H₁ H₂
-- Should not reduce to
-- λ (A : Type) (x y : A), eq.trans