max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(kernel/expr): fix binder_info

Browse source
This commit is contained in:
Leonardo de Moura 2018-06-13 12:20:58 -07:00
parent 017e1d7a5f
commit 4c370e4558
9 changed files with 37 additions and 71 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/builtin_exprs.cpp
View file

@ -184,7 +184,7 @@ static expr parse_let(parser & p, pos_info const & pos, bool in_do_block) {
p.add_local(l);
expr body = parse_let_body(p, pos, in_do_block);
match_definition_scope match_scope(p.env());
expr fn = p.save_pos(mk_local(p.next_name(), *g_let_match_name, mk_expr_placeholder(), mk_rec_info(true)), pos);
expr fn = p.save_pos(mk_local(p.next_name(), *g_let_match_name, mk_expr_placeholder(), mk_rec_info()), pos);
expr eqn = Fun(fn, Fun(new_locals, p.save_pos(mk_equation(p.rec_save_pos(mk_app(fn, lhs), pos), body), pos), p), p);
equations_header h = mk_match_header(match_scope.get_name(), match_scope.get_actual_name());
expr eqns = p.save_pos(mk_equations(h, 1, &eqn), pos);
@ -317,7 +317,7 @@ static expr parse_do(parser & p, bool has_braces) {
// must introduce a "fake" match
auto pos = ps[i];
match_definition_scope match_scope(p.env());
expr fn = p.save_pos(mk_local(p.next_name(), *g_do_match_name, mk_expr_placeholder(), mk_rec_info(true)), pos);
expr fn = p.save_pos(mk_local(p.next_name(), *g_do_match_name, mk_expr_placeholder(), mk_rec_info()), pos);
buffer<expr> locals;
to_buffer(lhss_locals[i], locals);
buffer<expr> eqs;
@ -745,7 +745,7 @@ static expr parse_lambda_constructor(parser & p, pos_info const & ini_pos) {
body = parse_lambda_core(p, ini_pos);
}
match_definition_scope match_scope(p.env());
expr fn = p.save_pos(mk_local(p.next_name(), *g_lambda_match_name, mk_expr_placeholder(), mk_rec_info(true)), pos);
expr fn = p.save_pos(mk_local(p.next_name(), *g_lambda_match_name, mk_expr_placeholder(), mk_rec_info()), pos);
expr eqn = Fun(fn, Fun(locals, p.save_pos(mk_equation(p.rec_save_pos(mk_app(fn, pattern), pos), body), pos), p), p);
equations_header h = mk_match_header(match_scope.get_name(), match_scope.get_actual_name());
expr x = p.rec_save_pos(mk_local(p.next_name(), "_x", mk_expr_placeholder(), binder_info()), pos);

6
src/frontends/lean/definition_cmds.cpp
View file

@ -144,7 +144,7 @@ static expr parse_mutual_definition(parser & p, buffer<name> & lp_names, buffer<
}
check_valid_end_of_equations(p);
}
expr fn = mk_local(mlocal_name(pre_fn), mlocal_pp_name(pre_fn), fn_type, mk_rec_info(true));
expr fn = mk_local(mlocal_name(pre_fn), mlocal_pp_name(pre_fn), fn_type, mk_rec_info());
fns.push_back(fn);
}
if (p.curr_is_token(get_with_tk()))
@ -530,7 +530,7 @@ static std::tuple<expr, expr, name> parse_definition(parser & p, buffer<name> &
p.next();
if (is_meta) {
declaration_name_scope scope2("_main");
fn = mk_local(mlocal_name(fn), mlocal_pp_name(fn), mlocal_type(fn), mk_rec_info(true));
fn = mk_local(mlocal_name(fn), mlocal_pp_name(fn), mlocal_type(fn), mk_rec_info());
p.add_local(fn);
val = p.parse_expr();
/* add fake equation */
@ -545,7 +545,7 @@ static std::tuple<expr, expr, name> parse_definition(parser & p, buffer<name> &
if (is_abbrev)
throw exception("invalid abbreviation, abbreviations should not be defined using pattern matching");
declaration_name_scope scope2("_main");
fn = mk_local(mlocal_name(fn), mlocal_pp_name(fn), mlocal_type(fn), mk_rec_info(true));
fn = mk_local(mlocal_name(fn), mlocal_pp_name(fn), mlocal_type(fn), mk_rec_info());
p.add_local(fn);
buffer<expr> eqns;
if (p.curr_is_token(get_period_tk())) {

4
src/frontends/lean/match_expr.cpp
View file

@ -36,9 +36,9 @@ expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos) {
if (p.curr_is_token(get_colon_tk())) {
p.next();
expr type = p.parse_expr();
fn = mk_local(p.next_name(), *g_match_name, type, mk_rec_info(true));
fn = mk_local(p.next_name(), *g_match_name, type, mk_rec_info());
} else {
fn = mk_local(p.next_name(), *g_match_name, mk_expr_placeholder(), mk_rec_info(true));
fn = mk_local(p.next_name(), *g_match_name, mk_expr_placeholder(), mk_rec_info());
}
p.check_token_next(get_with_tk(), "invalid 'match' expression, 'with' expected");

12
src/kernel/expr.cpp
View file

@ -142,10 +142,6 @@ void expr_const::dealloc() {
delete this;
}
unsigned binder_info::hash() const {
return (m_rec << 3) | (m_implicit << 2) | (m_strict_implicit << 1) | m_inst_implicit;
}
// Expr metavariables and local variables
expr_mlocal::expr_mlocal(bool is_meta, name const & n, name const & pp_n, expr const & t):
expr_composite(is_meta ? expr_kind::Meta : expr_kind::FVar, n.hash(), is_meta || t.has_expr_metavar(), t.has_univ_metavar(),
@ -215,14 +211,6 @@ void expr_app::dealloc(buffer<expr_cell*> & todelete) {
static unsigned dec(unsigned k) { return k == 0 ? 0 : k - 1; }
bool operator==(binder_info const & i1, binder_info const & i2) {
return
i1.is_implicit() == i2.is_implicit() &&
i1.is_strict_implicit() == i2.is_strict_implicit() &&
i1.is_inst_implicit() == i2.is_inst_implicit() &&
i1.is_rec() == i2.is_rec();
}
// Expr binders (Lambda, Pi)
expr_binding::expr_binding(expr_kind k, name const & n, expr const & t, expr const & b, binder_info const & i):
expr_composite(k, ::lean::hash(t.hash(), b.hash()),

53
src/kernel/expr.h
View file

@ -204,41 +204,38 @@ public:
expr const & get_type() const { return m_type; }
};
/**
\brief Auxiliary annotation for binders (Lambda and Pi). This information
is only used for elaboration.
*/
/** \brief Auxiliary annotation for binders (Lambda and Pi). */
class binder_info {
unsigned m_implicit:1; //! if true, binder argument is an implicit argument
unsigned m_strict_implicit:1; //! if true, binder argument is assumed to be a strict implicit argument
/** \brief if m_inst_implicit is true, binder argument is an implicit argument, and should be
inferred by class-instance resolution. */
unsigned m_inst_implicit:1;
/** \brief Auxiliary internal attribute used to mark local constants representing recursive functions
in recursive equations. TODO(Leo): rename to eqn_decl since we also mark non recursive equations
(e.g., `match ... with ... end`) with this flag. */
unsigned m_rec:1;
enum kind { Default, Implicit, StrictImplicit, InstImplicit, Rec };
object * m_val;
binder_info(object * v):m_val(v) {}
public:
binder_info(bool implicit = false, bool strict_implicit = false, bool inst_implicit = false, bool rec = false):
m_implicit(implicit), m_strict_implicit(strict_implicit), m_inst_implicit(inst_implicit), m_rec(rec) {}
bool is_implicit() const { return m_implicit; }
bool is_strict_implicit() const { return m_strict_implicit; }
bool is_inst_implicit() const { return m_inst_implicit; }
bool is_rec() const { return m_rec; }
unsigned hash() const;
binder_info():m_val(box(static_cast<unsigned>(Default))) {}
friend binder_info mk_implicit_binder_info();
friend binder_info mk_strict_implicit_binder_info();
friend binder_info mk_inst_implicit_binder_info();
friend binder_info mk_rec_info();
bool is_implicit() const { return unbox(m_val) == static_cast<unsigned>(Implicit); }
bool is_strict_implicit() const { return unbox(m_val) == static_cast<unsigned>(StrictImplicit); }
bool is_inst_implicit() const { return unbox(m_val) == static_cast<unsigned>(InstImplicit); }
bool is_rec() const { return unbox(m_val) == static_cast<unsigned>(Rec); }
unsigned hash() const { return unbox(m_val); }
friend bool operator==(binder_info const & i1, binder_info const & i2) { return i1.m_val == i2.m_val; }
friend bool operator!=(binder_info const & i1, binder_info const & i2) { return !(i1 == i2); }
friend binder_info read_binder_info(deserializer & d);
void serialize(serializer & s) const { s.write_object(m_val); }
};
inline binder_info mk_implicit_binder_info() { return binder_info(true); }
inline binder_info mk_strict_implicit_binder_info() { return binder_info(false, true); }
inline binder_info mk_inst_implicit_binder_info() { return binder_info(false, false, true); }
inline binder_info mk_rec_info(bool f) { return binder_info(false, false, false, f); }
inline binder_info mk_implicit_binder_info() { return binder_info(box(static_cast<unsigned>(binder_info::Implicit))); }
inline binder_info mk_strict_implicit_binder_info() { return binder_info(box(static_cast<unsigned>(binder_info::StrictImplicit))); }
inline binder_info mk_inst_implicit_binder_info() { return binder_info(box(static_cast<unsigned>(binder_info::InstImplicit))); }
inline binder_info mk_rec_info() { return binder_info(box(static_cast<unsigned>(binder_info::Rec))); }
inline bool is_explicit(binder_info const & bi) {
return !bi.is_implicit() && !bi.is_strict_implicit() && !bi.is_inst_implicit();
}
bool operator==(binder_info const & i1, binder_info const & i2);
inline bool operator!=(binder_info const & i1, binder_info const & i2) { return !(i1 == i2); }
inline serializer & operator<<(serializer & s, binder_info const & bi) { bi.serialize(s); return s; }
inline binder_info read_binder_info(deserializer & d) { return binder_info(d.read_object()); }
inline deserializer & operator>>(deserializer & d, binder_info & bi) { bi = read_binder_info(d); return d; }
/** \brief Compute a hash code that takes binder_info into account.
\remark This information is not cached like hash(). */

2
src/library/equations_compiler/pack_mutual.cpp
View file

@ -183,7 +183,7 @@ struct pack_mutual_fn {
expr x = locals.push_local("_x", new_domain);
expr new_codomain = mk_new_codomain(x, 0, codomains, codomains_lvl);
expr new_fn_type = m_ctx.mk_pi(x, new_codomain);
expr new_fn = locals.push_local(new_fn_name, new_fn_type, mk_rec_info(true));
expr new_fn = locals.push_local(new_fn_name, new_fn_type, mk_rec_info());
trace_debug_mutual(tout() << "new function " << new_fn_name << " : " << new_fn_type << "\n";);

2
src/library/equations_compiler/util.cpp
View file

@ -144,7 +144,7 @@ unpack_eqns::unpack_eqns(type_context_old & ctx, expr const & e):
}
expr unpack_eqns::update_fn_type(unsigned fidx, expr const & type) {
expr new_fn = m_locals.push_local(mlocal_pp_name(m_fns[fidx]), type, mk_rec_info(true));
expr new_fn = m_locals.push_local(mlocal_pp_name(m_fns[fidx]), type, mk_rec_info());
m_fns[fidx] = new_fn;
return new_fn;
}

19
src/library/kernel_serializer.cpp
View file

@ -34,25 +34,6 @@ static expr read_macro_definition(deserializer & d, unsigned num, expr const * a
return it->second(d, num, args);
}
serializer & operator<<(serializer & s, binder_info const & i) {
unsigned w =
(i.is_rec() ? 8 : 0) +
(i.is_implicit() ? 4 : 0) +
(i.is_strict_implicit() ? 2 : 0) +
(i.is_inst_implicit() ? 1 : 0);
s.write_char(w);
return s;
}
static binder_info read_binder_info(deserializer & d) {
unsigned w = d.read_char();
bool rec = (w & 8) != 0;
bool imp = (w & 4) != 0;
bool s_imp = (w & 2) != 0;
bool i_imp = (w & 1) != 0;
return binder_info(imp, s_imp, i_imp, rec);
}
static name * g_binder_name = nullptr;
class expr_serializer : public object_serializer<expr, expr_hash, is_bi_equal_proc> {

4
src/library/vm/vm_expr.cpp
View file

@ -91,7 +91,7 @@ binder_info to_binder_info(vm_obj const & o) {
case 1: return mk_implicit_binder_info();
case 2: return mk_strict_implicit_binder_info();
case 3: return mk_inst_implicit_binder_info();
default: return mk_rec_info(true);
default: return mk_rec_info();
}
}
@ -205,7 +205,7 @@ unsigned expr_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
break;
}
case expr_kind::Quote:
data.push_back(to_obj(quote_is_reflected(e)));
data.push_back(mk_vm_bool(quote_is_reflected(e)));
data.push_back(to_obj(quote_value(e)));
break;
}