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

feat(kernel): add mdata constructor

Browse source
This commit is contained in:
Leonardo de Moura 2018-06-18 10:36:27 -07:00
parent 70970ce5e0
commit 0847571ea6
35 changed files with 204 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/meta/expr.lean
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import init.meta.level init.control.monad
import init.meta.level init.control.monad init.lean.expr
universes u v
structure pos :=
@ -49,6 +49,7 @@ meta inductive expr
| pi : name → binder_info → expr → expr → expr
| elet : name → expr → expr → expr → expr
| lit : literal → expr
| mdata : lean.kvmap → expr → expr
| macro : macro_def → list expr → expr
| quote : bool → expr → expr
@ -339,6 +340,7 @@ meta def to_raw_fmt : expr → format
| (lam n bi e t) := p ["lam", to_fmt n, repr bi, to_raw_fmt e, to_raw_fmt t]
| (pi n bi e t) := p ["pi", to_fmt n, repr bi, to_raw_fmt e, to_raw_fmt t]
| (elet n g e f) := p ["elet", to_fmt n, to_raw_fmt g, to_raw_fmt e, to_raw_fmt f]
| (mdata d e) := p ["mdata", to_raw_fmt e]
| (macro d args) := sbracket (format.join (list.intersperse " " ("macro" :: to_fmt (macro_def_name d) :: args.map to_raw_fmt)))
| (quote b v) := p ["quote", to_fmt b, to_raw_fmt v]

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

@ -969,6 +969,7 @@ expr elaborator::visit_function(expr const & fn, bool has_args, optional<expr> c
case expr_kind::FVar: r = fn; break;
case expr_kind::Constant: r = visit_const_core(fn); break;
case expr_kind::Macro: r = visit_macro(fn, expected_type, true); break;
case expr_kind::MData: r = visit_mdata(fn, expected_type); break;
case expr_kind::Lambda: r = visit_lambda(fn, expected_type); break;
case expr_kind::Let: r = visit_let(fn, expected_type); break;
case expr_kind::Quote:
@ -3354,6 +3355,11 @@ expr elaborator::visit_expr_quote(expr const & e, optional<expr> const & expecte
return visit(q, expected_type);
}
expr elaborator::visit_mdata(expr const & e, optional<expr> const & expected_type) {
expr new_e = visit(mdata_expr(e), expected_type);
return update_mdata(e, new_e);
}
expr elaborator::visit_macro(expr const & e, optional<expr> const & expected_type, bool is_app_fn) {
if (is_as_is(e)) {
return get_as_is_arg(e);
@ -3647,6 +3653,8 @@ expr elaborator::visit(expr const & e, optional<expr> const & expected_type) {
return e;
}
lean_unreachable();
case expr_kind::MData:
return copy_pos(e, visit_mdata(e, expected_type));
case expr_kind::Sort:
return copy_pos(e, visit_sort(e));
case expr_kind::FVar:

1
src/frontends/lean/elaborator.h
View file

@ -236,6 +236,7 @@ private:
expr visit_macro(expr const & e, optional<expr> const & expected_type, bool is_app_fn);
expr visit_lambda(expr const & e, optional<expr> const & expected_type);
expr visit_pi(expr const & e);
expr visit_mdata(expr const & e, optional<expr> const & expected_type);
expr visit_app(expr const & e, optional<expr> const & expected_type);
expr visit_let(expr const & e, optional<expr> const & expected_type);
expr visit_convoy(expr const & e, optional<expr> const & expected_type);

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

@ -277,6 +277,8 @@ expr parser::copy_with_new_pos(expr const & e, pos_info p) {
case expr_kind::Sort: case expr_kind::Constant: case expr_kind::MVar:
case expr_kind::BVar: case expr_kind::FVar: case expr_kind::Lit:
return save_pos(copy(e), p);
case expr_kind::MData:
return save_pos(::lean::mk_mdata(mdata_data(e), copy_with_new_pos(mdata_expr(e), p)), p);
case expr_kind::App:
return save_pos(::lean::mk_app(copy_with_new_pos(app_fn(e), p),
copy_with_new_pos(app_arg(e), p)),
@ -1743,6 +1745,8 @@ static expr quote(expr const & e) {
return mk_app(mk_constant({"expr", "const"}), quote(const_name(e)), mk_expr_placeholder());
case expr_kind::MVar:
return mk_expr_placeholder();
case expr_kind::MData:
throw exception("expr.mdata is not supported at quote function");
case expr_kind::FVar:
throw elaborator_exception(e, sstream() << "invalid quotation, unexpected local constant '"
<< mlocal_pp_name(e) << "'");

1
src/frontends/lean/pp.cpp
View file

@ -1784,6 +1784,7 @@ auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result {
case expr_kind::BVar: return pp_var(e);
case expr_kind::FVar: return pp_local(e);
case expr_kind::Sort: return pp_sort(e);
case expr_kind::MData: return pp(mdata_expr(e), ignore_hide);
case expr_kind::Constant: return pp_const(e);
case expr_kind::MVar: return pp_meta(e);
case expr_kind::App: return pp_app(e);

3
src/kernel/equiv_manager.cpp
View file

@ -95,6 +95,9 @@ bool equiv_manager::is_equiv_core(expr const & a, expr const & b) {
case expr_kind::Lit:
result = lit_value(a) == lit_value(b);
break;
case expr_kind::MData:
result = mdata_expr(a) == mdata_expr(b);
break;
case expr_kind::Let:
result =
is_equiv_core(let_type(a), let_type(b)) &&

36
src/kernel/expr.cpp
View file

@ -299,6 +299,26 @@ expr lit_type(expr_ptr e) {
lean_unreachable();
}
// Expr metadata
expr_mdata::expr_mdata(kvmap const & data, expr const & e):
expr_composite(expr_kind::MData, e.hash(),
e.has_expr_metavar(),
e.has_univ_metavar(),
e.has_fvar(),
e.has_param_univ(),
inc_weight(get_weight(e)),
get_loose_bvar_range(e)),
m_data(data), m_expr(e) {
m_depth = get_depth(e) + 1;
m_hash = ::lean::hash(m_hash, m_weight);
m_hash = ::lean::hash(m_hash, m_depth);
}
void expr_mdata::dealloc(buffer<expr_cell*> & todelete) {
dec_ref(m_expr, todelete);
delete this;
}
// Let expressions
expr_let::expr_let(name const & n, expr const & t, expr const & v, expr const & b):
expr_composite(expr_kind::Let,
@ -362,7 +382,9 @@ expr mk_metavar(name const & n, name const & pp_n, expr const & t) {
expr mk_metavar(name const & n, expr const & t) {
return mk_metavar(n, n, t);
}
expr mk_mdata(kvmap const & d, expr const & e) {
return expr(new expr_mdata(d, e));
}
expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info const & bi) {
return expr(new expr_fvar(n, pp_n, t, bi));
}
@ -398,6 +420,7 @@ void expr_cell::dealloc() {
lean_assert(it->get_rc() == 0);
switch (it->kind()) {
case expr_kind::Lit: static_cast<expr_lit*>(it)->dealloc(); break;
case expr_kind::MData: static_cast<expr_mdata*>(it)->dealloc(todo); break;
case expr_kind::BVar: static_cast<expr_bvar*>(it)->dealloc(); break;
case expr_kind::MVar: static_cast<expr_mlocal*>(it)->dealloc(todo); break;
case expr_kind::FVar: static_cast<expr_fvar*>(it)->dealloc(todo); break;
@ -527,6 +550,7 @@ unsigned get_weight(expr const & e) {
return 1;
case expr_kind::Lambda: case expr_kind::Pi:
case expr_kind::App: case expr_kind::Let:
case expr_kind::MData:
return static_cast<expr_composite*>(e.raw())->m_weight;
@ -545,6 +569,7 @@ unsigned get_depth(expr const & e) {
return 1;
case expr_kind::Lambda: case expr_kind::Pi:
case expr_kind::App: case expr_kind::Let:
case expr_kind::MData:
return static_cast<expr_composite*>(e.raw())->m_depth;
@ -556,6 +581,13 @@ unsigned get_depth(expr const & e) {
lean_unreachable(); // LCOV_EXCL_LINE
}
expr update_mdata(expr const & e, expr const & t) {
if (!is_eqp(mdata_expr(e), t))
return mk_mdata(mdata_data(e), t);
else
return e;
}
expr update_app(expr const & e, expr const & new_fn, expr const & new_arg) {
if (!is_eqp(app_fn(e), new_fn) || !is_eqp(app_arg(e), new_arg))
return mk_app(new_fn, new_arg);
@ -626,6 +658,7 @@ bool is_atomic(expr const & e) {
case expr_kind::App: case expr_kind::MVar:
case expr_kind::FVar: case expr_kind::Lambda:
case expr_kind::Pi: case expr_kind::Let:
case expr_kind::MData:
return false;
@ -779,6 +812,7 @@ unsigned hash_bi(expr const & e) {
std::ostream & operator<<(std::ostream & out, expr_kind const & k) {
switch (k) {
case expr_kind::MData: out << "MData"; break;
case expr_kind::Lit: out << "Lit"; break;
case expr_kind::BVar: out << "BVar"; break;
case expr_kind::FVar: out << "FVar"; break;

23
src/kernel/expr.h
View file

@ -19,6 +19,7 @@ Author: Leonardo de Moura
#include "util/nat.h"
#include "util/hash.h"
#include "util/buffer.h"
#include "util/kvmap.h"
#include "util/list_fn.h"
#include "util/sexpr/format.h"
#include "kernel/level.h"
@ -40,13 +41,14 @@ class expr;
| Pi name expr expr
| Let name expr expr expr
| Lit literal
| MData kvmap expr
The following constructors will be deleted in the future
| Quote bool expr
| Macro macro
*/
enum class expr_kind { BVar, FVar, Sort, Constant, MVar, App, Lambda, Pi, Let, Lit, Macro, Quote };
enum class expr_kind { BVar, FVar, Sort, Constant, MVar, App, Lambda, Pi, Let, Lit, MData, Macro, Quote };
class expr_cell {
protected:
// The bits of the following field mean:
@ -133,6 +135,7 @@ public:
friend expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info const & i);
friend expr mk_let(name const & n, expr const & t, expr const & v, expr const & b);
friend expr mk_lit(literal const & lit);
friend expr mk_mdata(kvmap const & m, expr const & e);
friend bool is_eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; }
// TODO(Leo): delete
@ -366,6 +369,18 @@ public:
literal const & get_literal() const { return m_lit; }
};
class expr_mdata : public expr_composite {
kvmap m_data;
expr m_expr;
friend expr_cell;
void dealloc(buffer<expr_cell*> & todelete);
public:
expr_mdata(kvmap const & m, expr const & e);
~expr_mdata() {}
kvmap const & get_data() const { return m_data; }
expr const & get_expr() const { return m_expr; }
};
// =======================================
// Testers
inline bool is_bvar(expr_ptr e) { return e->kind() == expr_kind::BVar; }
@ -378,6 +393,7 @@ inline bool is_pi(expr_ptr e) { return e->kind() == expr_kind::Pi; }
inline bool is_let(expr_ptr e) { return e->kind() == expr_kind::Let; }
inline bool is_sort(expr_ptr e) { return e->kind() == expr_kind::Sort; }
inline bool is_lit(expr_ptr e) { return e->kind() == expr_kind::Lit; }
inline bool is_mdata(expr_ptr e) { return e->kind() == expr_kind::MData; }
inline bool is_binding(expr_ptr e) { return is_lambda(e) || is_pi(e); }
bool is_atomic(expr const & e);
@ -389,6 +405,7 @@ bool is_metavar_app(expr const & e);
// =======================================
// Constructors
expr mk_lit(literal const & lit);
expr mk_mdata(kvmap const & d, expr const & e);
expr mk_bvar(unsigned idx);
expr mk_fvar(name const & n);
inline expr BVar(unsigned idx) { return mk_bvar(idx); }
@ -449,6 +466,7 @@ inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const
// =======================================
// Casting (these functions are only needed for low-level code)
inline expr_lit * to_lit(expr_ptr e) { lean_assert(is_lit(e)); return static_cast<expr_lit*>(e); }
inline expr_mdata * to_mdata(expr_ptr e) { lean_assert(is_mdata(e)); return static_cast<expr_mdata*>(e); }
inline expr_bvar * to_bvar(expr_ptr e) { lean_assert(is_bvar(e)); return static_cast<expr_bvar*>(e); }
inline expr_fvar * to_fvar(expr_ptr e) { lean_assert(is_fvar(e)); return static_cast<expr_fvar*>(e); }
inline expr_const * to_constant(expr_ptr e) { lean_assert(is_constant(e)); return static_cast<expr_const*>(e); }
@ -466,6 +484,8 @@ inline unsigned get_rc(expr_ptr e) { return e->get_rc(); }
inline bool is_shared(expr_ptr e) { return get_rc(e) > 1; }
inline literal const & lit_value(expr_ptr e) { return to_lit(e)->get_literal(); }
expr lit_type(expr_ptr e);
inline expr const & mdata_expr(expr_ptr e) { return to_mdata(e)->get_expr(); }
inline kvmap const & mdata_data(expr_ptr e) { return to_mdata(e)->get_data(); }
inline unsigned bvar_idx(expr_ptr e) { return to_bvar(e)->get_vidx(); }
inline bool is_bvar(expr_ptr e, unsigned i) { return is_bvar(e) && bvar_idx(e) == i; }
inline name const & fvar_name(expr_ptr e) { return to_fvar(e)->get_name(); }
@ -555,6 +575,7 @@ expr update_local(expr const & e, binder_info const & bi);
expr update_sort(expr const & e, level const & new_level);
expr update_constant(expr const & e, levels const & new_levels);
expr update_let(expr const & e, expr const & new_type, expr const & new_value, expr const & new_body);
expr update_mdata(expr const & e, expr const & t);
// =======================================

4
src/kernel/expr_eq_fn.cpp
View file

@ -72,6 +72,10 @@ class expr_eq_fn {
switch (a.kind()) {
case expr_kind::BVar:
lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::MData:
return
apply(mdata_expr(a), mdata_expr(b)) &&
mdata_data(a) == mdata_data(b);
case expr_kind::Lit:
return lit_value(a) == lit_value(b);
case expr_kind::Constant:

3
src/kernel/for_each_fn.cpp
View file

@ -88,6 +88,9 @@ class for_each_fn {
case expr_kind::Constant: case expr_kind::BVar:
case expr_kind::Sort: case expr_kind::Lit:
goto begin_loop;
case expr_kind::MData:
todo.emplace_back(mdata_expr(e), offset);
goto begin_loop;
case expr_kind::FVar:
// TODO(Leo): delete after refactoring
todo.emplace_back(mlocal_type(e), offset);

8
src/kernel/old_type_checker.cpp
View file

@ -225,6 +225,7 @@ expr old_type_checker::infer_type_core(expr const & e, bool infer_only) {
if (!infer_only) check_level(sort_level(e));
r = mk_sort(mk_succ(sort_level(e)));
break;
case expr_kind::MData: r = infer_type_core(mdata_expr(e), infer_only); break;
case expr_kind::Constant: r = infer_constant(e, infer_only); break;
case expr_kind::Macro: r = infer_macro(e, infer_only); break;
case expr_kind::Lambda: r = infer_lambda(e, infer_only); break;
@ -287,6 +288,8 @@ expr old_type_checker::whnf_core(expr const & e) {
case expr_kind::BVar: case expr_kind::Sort: case expr_kind::MVar: case expr_kind::FVar:
case expr_kind::Pi: case expr_kind::Constant: case expr_kind::Lambda: case expr_kind::Lit:
return e;
case expr_kind::MData:
return whnf_core(mdata_expr(e));
case expr_kind::Macro: case expr_kind::App: case expr_kind::Let:
break;
case expr_kind::Quote: throw_found_quote(m_env);
@ -304,6 +307,7 @@ expr old_type_checker::whnf_core(expr const & e) {
switch (e.kind()) {
case expr_kind::BVar: case expr_kind::Sort: case expr_kind::MVar: case expr_kind::FVar:
case expr_kind::Pi: case expr_kind::Constant: case expr_kind::Lambda: case expr_kind::Lit:
case expr_kind::MData:
lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::Macro:
if (auto m = expand_macro(e))
@ -392,6 +396,8 @@ expr old_type_checker::whnf(expr const & e) {
case expr_kind::BVar: case expr_kind::Sort: case expr_kind::MVar: case expr_kind::FVar:
case expr_kind::Pi: case expr_kind::Lit:
return e;
case expr_kind::MData:
return whnf(mdata_expr(e));
case expr_kind::Lambda: case expr_kind::Macro: case expr_kind::App:
case expr_kind::Constant: case expr_kind::Let:
break;
@ -482,6 +488,8 @@ lbool old_type_checker::quick_is_def_eq(expr const & t, expr const & s, bool use
switch (t.kind()) {
case expr_kind::Lambda: case expr_kind::Pi:
return to_lbool(is_def_eq_binding(t, s));
case expr_kind::MData:
return to_lbool(is_def_eq(mdata_expr(t), mdata_expr(s)));
case expr_kind::Sort:
return to_lbool(is_def_eq(sort_level(t), sort_level(s)));
case expr_kind::MVar:

4
src/kernel/replace_fn.cpp
View file

@ -82,6 +82,10 @@ class replace_rec_fn {
case expr_kind::Constant: case expr_kind::Sort:
case expr_kind::BVar: case expr_kind::Lit:
return save_result(e, offset, e, shared);
case expr_kind::MData: {
expr new_e = apply(mdata_expr(e), offset);
return save_result(e, offset, update_mdata(e, new_e), shared);
}
case expr_kind::MVar: {
expr new_t = apply(mlocal_type(e), offset);
return save_result(e, offset, update_mlocal(e, new_t), shared);

13
src/kernel/type_checker.cpp
View file

@ -219,6 +219,7 @@ expr type_checker::infer_type_core(expr const & e, bool infer_only) {
expr r;
switch (e.kind()) {
case expr_kind::Lit: r = lit_type(e); break;
case expr_kind::MData: r = infer_type_core(mdata_expr(e), infer_only); break;
case expr_kind::FVar: r = infer_fvar(e); break;
case expr_kind::MVar: r = mlocal_type(e); break;
case expr_kind::BVar:
@ -306,6 +307,8 @@ expr type_checker::whnf_core(expr const & e) {
case expr_kind::Pi: case expr_kind::Constant: case expr_kind::Lambda:
case expr_kind::Lit:
return e;
case expr_kind::MData:
return whnf_core(mdata_expr(e));
case expr_kind::FVar:
return whnf_fvar(e);
case expr_kind::Macro: case expr_kind::App: case expr_kind::Let:
@ -325,9 +328,9 @@ expr type_checker::whnf_core(expr const & e) {
// do the actual work
expr r;
switch (e.kind()) {
case expr_kind::BVar: case expr_kind::Sort: case expr_kind::MVar: case expr_kind::FVar:
case expr_kind::Pi: case expr_kind::Constant: case expr_kind::Lambda:
case expr_kind::Lit:
case expr_kind::BVar: case expr_kind::Sort: case expr_kind::MVar: case expr_kind::FVar:
case expr_kind::Pi: case expr_kind::Constant: case expr_kind::Lambda:
case expr_kind::Lit: case expr_kind::MData:
lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::Quote:
@ -419,6 +422,8 @@ expr type_checker::whnf(expr const & e) {
case expr_kind::BVar: case expr_kind::Sort: case expr_kind::MVar: case expr_kind::Pi:
case expr_kind::Lit:
return e;
case expr_kind::MData:
return whnf(mdata_expr(e));
case expr_kind::FVar:
return whnf_fvar(e);
case expr_kind::Lambda: case expr_kind::Macro: case expr_kind::App:
@ -516,6 +521,8 @@ lbool type_checker::quick_is_def_eq(expr const & t, expr const & s, bool use_has
return to_lbool(is_def_eq_binding(t, s));
case expr_kind::Sort:
return to_lbool(is_def_eq(sort_level(t), sort_level(s)));
case expr_kind::MData:
return to_lbool(is_def_eq(mdata_expr(t), mdata_expr(s)));
case expr_kind::MVar:
lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::BVar: case expr_kind::FVar: case expr_kind::App:

2
src/library/check.cpp
View file

@ -125,6 +125,8 @@ struct check_fn {
return visit_app(e);
case expr_kind::Let:
return visit_let(e);
case expr_kind::MData:
return visit(mdata_expr(e));
case expr_kind::Macro:
return visit_macro(e);
case expr_kind::Quote:

1
src/library/compiler/cse.cpp
View file

@ -57,6 +57,7 @@ class cse_fn : public compiler_step_visitor {
case expr_kind::Macro: visit_macro(e); break;
case expr_kind::App: visit_app(e); break;
case expr_kind::Let: visit_let(e); break;
case expr_kind::MData: visit(mdata_expr(e)); break;
case expr_kind::Quote:
break;
}

1
src/library/compiler/vm_compiler.cpp
View file

@ -310,6 +310,7 @@ class vm_compiler_fn {
case expr_kind::Pi: lean_unreachable();
case expr_kind::Lambda: lean_unreachable();
case expr_kind::Macro: compile_macro(e, bpz, m); break;
case expr_kind::MData: compile(mdata_expr(e), bpz, m); break;
case expr_kind::Constant: compile_constant(e); break;
case expr_kind::FVar: compile_local(e, m); break;
case expr_kind::App: compile_app(e, bpz, m); break;

1
src/library/deep_copy.cpp
View file

@ -12,6 +12,7 @@ namespace lean {
expr copy(expr const & a) {
switch (a.kind()) {
case expr_kind::Lit: return mk_lit(lit_value(a));
case expr_kind::MData: return mk_mdata(mdata_data(a), mdata_expr(a));
case expr_kind::BVar: return mk_var(var_idx(a));
case expr_kind::FVar: return mk_local(mlocal_name(a), mlocal_pp_name(a), mlocal_type(a), local_info(a));
case expr_kind::Constant: return mk_constant(const_name(a), const_levels(a));

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

@ -151,6 +151,8 @@ struct structural_rec_fn {
}
return true;
}
case expr_kind::MData:
return check_rhs(mdata_expr(e));
case expr_kind::Let:
if (!check_rhs(let_value(e))) {
return false;

10
src/library/expr_lt.cpp
View file

@ -25,6 +25,11 @@ bool is_lt(expr const & a, expr const & b, bool use_hash, local_context const *
return lit_value(a) < lit_value(b);
case expr_kind::BVar:
return var_idx(a) < var_idx(b);
case expr_kind::MData:
if (mdata_expr(a) != mdata_expr(b))
return is_lt(mdata_expr(a), mdata_expr(b), use_hash, lctx);
else
return mdata_data(a) < mdata_data(b);
case expr_kind::Constant:
if (const_name(a) != const_name(b))
return const_name(a) < const_name(b);
@ -136,6 +141,11 @@ bool is_lt_no_level_params(expr const & a, expr const & b) {
return lit_value(a) < lit_value(b);
case expr_kind::BVar:
return var_idx(a) < var_idx(b);
case expr_kind::MData:
if (mdata_expr(a) != mdata_expr(b))
return is_lt_no_level_params(mdata_expr(a), mdata_expr(b));
else
return mdata_data(a) < mdata_data(b);
case expr_kind::Constant:
if (const_name(a) != const_name(b))
return const_name(a) < const_name(b);

2
src/library/inductive_compiler/nested.cpp
View file

@ -534,6 +534,7 @@ class add_nested_inductive_decl_fn {
case expr_kind::Macro:
case expr_kind::Quote:
case expr_kind::Lit:
case expr_kind::MData:
return _e;
case expr_kind::Lambda:
case expr_kind::Pi:
@ -590,6 +591,7 @@ class add_nested_inductive_decl_fn {
case expr_kind::Macro:
case expr_kind::Quote:
case expr_kind::Lit:
case expr_kind::MData:
return _e;
case expr_kind::Lambda:
case expr_kind::Pi:

8
src/library/kernel_serializer.cpp
View file

@ -61,6 +61,10 @@ class expr_serializer : public object_serializer<expr, expr_hash, is_bi_equal_pr
case expr_kind::Lit:
s << lit_value(a);
break;
case expr_kind::MData:
s << mdata_data(a);
write_core(mdata_expr(a));
break;
case expr_kind::Constant:
lean_assert(!const_name(a).is_anonymous());
s << const_name(a) << const_levels(a);
@ -131,6 +135,10 @@ public:
return mk_var(d.read_unsigned());
case expr_kind::Lit:
return mk_lit(read_literal(d));
case expr_kind::MData: {
kvmap m = read_list_ref<pair_ref<name, data_value>>(d);
return mk_mdata(m, read());
}
case expr_kind::Constant: {
auto n = read_name(d);
return mk_constant(n, read_levels(d));

3
src/library/locals.cpp
View file

@ -75,6 +75,9 @@ void collect_locals(expr const & e, collected_locals & ls, bool restricted) {
case expr_kind::BVar: case expr_kind::Constant:
case expr_kind::Sort: case expr_kind::Lit:
break; // do nothing
case expr_kind::MData:
visit(mdata_expr(e));
break;
case expr_kind::FVar:
if (!restricted)
visit(mlocal_type(e));

7
src/library/max_sharing.cpp
View file

@ -62,10 +62,15 @@ struct max_sharing_fn::imp {
case expr_kind::Sort:
res = update_sort(a, apply(sort_level(a)));
break;
case expr_kind::MData: {
expr new_e = apply(mdata_expr(a));
res = update_mdata(a, new_e);
break;
}
case expr_kind::App: {
expr new_f = apply(app_fn(a));
expr new_a = apply(app_arg(a));
res = update_app(a, new_f, new_a);
res = update_app(a, new_f, new_a);
break;
}
case expr_kind::Lambda: case expr_kind::Pi: {

1
src/library/noncomputable.cpp
View file

@ -200,6 +200,7 @@ struct get_noncomputable_reason_fn {
case expr_kind::Lambda: visit_binding(e); return;
case expr_kind::Pi: visit_binding(e); return;
case expr_kind::Let: visit_let(e); return;
case expr_kind::MData: visit(mdata_expr(e)); return;
case expr_kind::Quote: return;
}
}

2
src/library/normalize.cpp
View file

@ -119,6 +119,8 @@ class normalize_fn {
case expr_kind::BVar: case expr_kind::Constant: case expr_kind::Sort:
case expr_kind::MVar: case expr_kind::FVar: case expr_kind::Lit:
return e;
case expr_kind::MData:
lean_unreachable();
case expr_kind::Lambda: {
e = normalize_binding(e);
if (m_use_eta)

4
src/library/pos_info_provider.cpp
View file

@ -143,6 +143,10 @@ class replace_rec_fn2 {
expr new_t = apply(mlocal_type(e), offset);
return save_result(e, offset, copy_pos(e, update_mlocal(e, new_t)), shared);
}
case expr_kind::MData: {
expr new_e = apply(mdata_expr(e), offset);
return save_result(e, offset, copy_pos(e, update_mdata(e, new_e)), shared);
}
case expr_kind::App: {
expr new_f = apply(app_fn(e), offset);
expr new_a = apply(app_arg(e), offset);

3
src/library/print.cpp
View file

@ -222,6 +222,9 @@ struct print_expr_fn {
case expr_kind::FVar:
out() << fix_name(mlocal_pp_name(a));
break;
case expr_kind::MData:
out() << "[mdata "; print(mdata_expr(a)); out() << "]";
break;
case expr_kind::BVar:
out() << "#" << var_idx(a);
break;

2
src/library/replace_visitor.cpp
View file

@ -24,6 +24,7 @@ expr replace_visitor::visit_mlocal(expr const & e) {
}
expr replace_visitor::visit_meta(expr const & e) { return visit_mlocal(e); }
expr replace_visitor::visit_local(expr const & e) { return visit_mlocal(e); }
expr replace_visitor::visit_mdata(expr const & e) { return visit(mdata_expr(e)); }
expr replace_visitor::visit_app(expr const & e) {
lean_assert(is_app(e));
expr new_fn = visit(app_fn(e));
@ -69,6 +70,7 @@ expr replace_visitor::visit(expr const & e) {
switch (e.kind()) {
case expr_kind::Lit: return save_result(e, visit_lit(e), shared);
case expr_kind::MData: return save_result(e, visit_mdata(e), shared);
case expr_kind::Sort: return save_result(e, visit_sort(e), shared);
case expr_kind::Constant: return save_result(e, visit_constant(e), shared);
case expr_kind::BVar: return save_result(e, visit_var(e), shared);

1
src/library/replace_visitor.h
View file

@ -30,6 +30,7 @@ protected:
virtual expr visit_pi(expr const &);
virtual expr visit_let(expr const & e);
virtual expr visit_lit(expr const & e);
virtual expr visit_mdata(expr const & e);
virtual expr visit(expr const &);
virtual expr visit_macro(expr const &);

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

@ -260,6 +260,9 @@ expr dsimplify_core_fn::visit(expr const & e) {
case expr_kind::Constant:
new_e = curr_e;
break;
case expr_kind::MData:
new_e = mdata_expr(curr_e);
break;
case expr_kind::BVar:
lean_unreachable();
case expr_kind::MVar:

2
src/library/tactic/simp_lemmas.cpp
View file

@ -645,6 +645,8 @@ static bool is_permutation(expr const & lhs, expr const & rhs, unsigned offset,
} else {
return lhs == rhs; // free variable
}
case expr_kind::MData:
return is_permutation(mdata_expr(lhs), mdata_expr(rhs), offset, p);
case expr_kind::Lambda: case expr_kind::Pi:
return
is_permutation(binding_domain(lhs), binding_domain(rhs), offset, p) &&

4
src/library/tactic/simplify.cpp
View file

@ -668,7 +668,9 @@ simp_result simplify_core_fn::visit(expr const & e, optional<expr> const & paren
case expr_kind::Let:
new_result = join(curr_result, visit_let(curr_result.get_new()));
break;
case expr_kind::MData:
new_result = join(curr_result, visit(mdata_expr(e), some_expr(e)));
break;
case expr_kind::Macro:
new_result = join(curr_result, visit_macro(curr_result.get_new()));
break;

11
src/library/type_context.cpp
View file

@ -790,6 +790,9 @@ expr type_context_old::whnf_core(expr const & e0, bool proj_reduce) {
case expr_kind::Constant: case expr_kind::Lit:
/* Remark: we do not unfold Constants eagerly in this method */
return e;
case expr_kind::MData:
e = mdata_expr(e);
continue;
case expr_kind::FVar:
if (use_zeta() && is_local_decl_ref(e)) {
if (auto d = m_lctx.find_local_decl(e)) {
@ -1010,6 +1013,9 @@ expr type_context_old::infer_core(expr const & e) {
case expr_kind::MVar:
r = infer_metavar(e);
break;
case expr_kind::MData:
r = infer_core(mdata_expr(e));
break;
case expr_kind::BVar:
throw exception("failed to infer type, unexpected bound variable occurrence");
case expr_kind::Sort:
@ -2717,6 +2723,8 @@ lbool type_context_old::quick_is_def_eq(expr const & e1, expr const & e2) {
return to_lbool(is_def_eq_binding(e1, e2));
case expr_kind::Sort:
return to_lbool(is_def_eq(sort_level(e1), sort_level(e2)));
case expr_kind::MData:
return to_lbool(is_def_eq_core(mdata_expr(e1), mdata_expr(e2)));
case expr_kind::Lit:
return to_lbool(lit_value(e1) == lit_value(e2));
case expr_kind::MVar: case expr_kind::BVar:
@ -3378,6 +3386,9 @@ lbool type_context_old::is_quick_class(expr const & type, name & result) {
case expr_kind::Pi:
it = &binding_body(*it);
break;
case expr_kind::MData:
it = &mdata_expr(*it);
break;
case expr_kind::Macro:
return l_undef;
case expr_kind::Quote:

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

@ -167,6 +167,31 @@ vm_obj expr_macro_def_name(vm_obj const & d) {
return to_obj(to_macro_definition(d).get_name());
}
/*
inductive data_value
| of_string (v : string)
| of_nat (v : nat)
| of_bool (v : bool)
| of_name (v : name)
*/
vm_obj to_obj(data_value const & d) {
switch (d.kind()) {
case data_value_kind::String: return mk_vm_constructor(0, to_obj(d.get_string().to_std_string()));
case data_value_kind::Nat: return mk_vm_constructor(1, mk_vm_nat(d.get_nat().to_mpz()));
case data_value_kind::Bool: return mk_vm_constructor(2, mk_vm_bool(d.get_bool()));
case data_value_kind::Name: return mk_vm_constructor(3, to_obj(d.get_name()));
}
lean_unreachable();
}
vm_obj to_obj(kvmap const & m) {
buffer<vm_obj> objs;
for (pair_ref<name, data_value> const & p : m) {
objs.push_back(mk_vm_pair(to_obj(p.fst()), to_obj(p.snd())));
}
return to_obj(objs);
}
unsigned expr_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
expr const & e = to_expr(o);
switch (e.kind()) {
@ -215,6 +240,10 @@ unsigned expr_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
break;
}
break;
case expr_kind::MData:
data.push_back(to_obj(mdata_data(e)));
data.push_back(to_obj(mdata_expr(e)));
break;
case expr_kind::Macro: {
data.push_back(to_obj(macro_def(e)));
buffer<expr> args;

2
src/util/list_ref.h
View file

@ -77,7 +77,7 @@ public:
T const & h2 = ::lean::head<T>(it2);
if (h1 < h2)
return true;
if (h2 > h1)
if (h2 < h1)
return false;
it1 = cnstr_obj(it1, 1);
it2 = cnstr_obj(it2, 1);