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

feat(frontends/lean/elaborator): elaborate ``(e) to type reflected e` if possible and add coercion reflected -> expr

Browse source
This commit is contained in:
Sebastian Ullrich 2017-04-28 17:12:32 +02:00 • committed by Leonardo de Moura
parent 85cf1b7075
commit 2825c5fbcc
13 changed files with 128 additions and 122 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -46,12 +46,20 @@ meta inductive expr
| elet : name → expr → expr → expr → expr
| macro : macro_def → ∀ n, (fin n → expr) → expr
universe u
/-- (reflected a) is a special opaque container for an `expr` representing `a`.
It can only be obtained via type class inference, which will use the representation
of `a` in the calling context. -/
meta constant {u} reflected {α : Type u} : α → Type u
meta constant reflected {α : Type u} : α → Type u
meta constant reflected.to_expr {α : Type u} {a : α} : reflected a → expr
meta structure typed_expr (α : Type u) :=
(val : α)
(reflected : reflected val)
attribute [class] reflected
meta constant {u} reflect {α : Type u} (a : α) [reflected a] : expr
meta instance {α : Type u} (a : α) : has_coe (reflected a) expr :=
⟨reflected.to_expr⟩
meta instance : inhabited expr :=
⟨expr.sort level.zero⟩

3
library/init/meta/smt/ematch.lean
View file

@ -79,10 +79,9 @@ meta def to_hinst_lemmas_core (m : transparency) : bool → list name → hinst_
meta def mk_hinst_lemma_attr_core (attr_name : name) (as_simp : bool) : command :=
do let t := ```(caching_user_attribute hinst_lemmas),
let b := if as_simp then ```(tt) else ```(ff),
v ← to_expr ``({name := %%(quote attr_name),
descr := "hinst_lemma attribute",
mk_cache := λ ns, to_hinst_lemmas_core reducible %%b ns hinst_lemmas.mk,
mk_cache := λ ns, to_hinst_lemmas_core reducible %%(quote as_simp) ns hinst_lemmas.mk,
dependencies := [`reducibility] } : caching_user_attribute hinst_lemmas),
add_decl (declaration.defn attr_name [] t v reducibility_hints.abbrev ff),
attribute.register attr_name

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

@ -651,7 +651,7 @@ static expr parse_lazy_quoted_pexpr(parser_state & p, unsigned, expr const *, po
e = mk_typed_expr_distrib_choice(p, t, e, pos);
}
p.check_token_next(get_rparen_tk(), "invalid quoted expression, `)` expected");
return p.save_pos(mk_pexpr_quote(e), pos);
return p.save_pos(mk_quote(e, /* is_expr */ false), pos);
}
static expr parse_quoted_pexpr(parser_state & p, unsigned, expr const *, pos_info const & pos) {
@ -665,7 +665,7 @@ static expr parse_quoted_pexpr(parser_state & p, unsigned, expr const *, pos_inf
e = mk_typed_expr_distrib_choice(p, t, e, pos);
}
p.check_token_next(get_rparen_tk(), "invalid quoted expression, `)` expected");
return p.save_pos(mk_pexpr_quote(e), pos);
return p.save_pos(mk_quote(e, /* is_expr */ false), pos);
}
static expr parse_quoted_expr(parser_state & p, unsigned, expr const *, pos_info const & pos) {
@ -682,11 +682,8 @@ static expr parse_quoted_expr(parser_state & p, unsigned, expr const *, pos_info
}
p.check_token_next(get_rparen_tk(), "invalid quoted expression, `)` expected");
}
e = mk_quote_core(e, true);
if (!p.in_pattern()) {
e = elaborate_quote(e, p.env(), p.get_options(), /* in_pattern */ false);
// note: when `p.in_pattern()`, quote will be elaborated in `parser::patexpr_to_{pattern,expr}`
}
// do not introduce `expr.subst` calls in patterns
e = p.in_pattern() ? mk_quote_core(e, true) : mk_quote(e, true);
return p.save_pos(e, pos);
}

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

@ -266,11 +266,9 @@ expr elaborator::mk_type_metavar(expr const & ref) {
expr elaborator::mk_instance_core(local_context const & lctx, expr const & C, expr const & ref) {
// synthesize `reflected e` by quoting e
if (is_app_of(C, get_reflected_name(), 2)) {
expr const & r = instantiate_mvars(app_arg(C));
if (closed(r) && !has_local(r)) {
expr r_ty = instantiate_mvars(app_arg(app_fn(C)));
level l = *::lean::dec_level(::lean::get_level(m_ctx, r_ty));
return mk_reflected(r, r_ty, l);
expr const & e = app_arg(C);
if (!is_local(e)) {
return visit(mk_quote(e, /* is_expr */ true), some_expr(C));
}
}
@ -2816,86 +2814,6 @@ expr elaborator::visit_structure_instance(expr const & e, optional<expr> const &
return e2;
}
static expr quote(expr const & e) {
switch (e.kind()) {
case expr_kind::Var:
lean_unreachable();
case expr_kind::Sort:
return mk_app(mk_constant({"expr", "sort"}), mk_expr_placeholder());
case expr_kind::Constant:
return mk_app(mk_constant({"expr", "const"}), quote(const_name(e)), mk_expr_placeholder());
case expr_kind::Meta:
return mk_expr_placeholder();
case expr_kind::Local:
throw elaborator_exception(e, sstream() << "invalid quotation, unexpected local constant '"
<< local_pp_name(e) << "'");
case expr_kind::App:
return mk_app(mk_constant({"expr", "app"}), quote(app_fn(e)), quote(app_arg(e)));
case expr_kind::Lambda:
return mk_app(mk_constant({"expr", "lam"}), mk_expr_placeholder(), mk_expr_placeholder(),
quote(binding_domain(e)), quote(binding_body(e)));
case expr_kind::Pi:
return mk_app(mk_constant({"expr", "pi"}), mk_expr_placeholder(), mk_expr_placeholder(),
quote(binding_domain(e)), quote(binding_body(e)));
case expr_kind::Let:
return mk_app(mk_constant({"expr", "elet"}), mk_expr_placeholder(), quote(let_type(e)),
quote(let_value(e)), quote(let_body(e)));
case expr_kind::Macro:
if (is_antiquote(e))
return get_antiquote_expr(e);
if (is_typed_expr(e))
return mk_typed_expr(quote(get_typed_expr_expr(e)), quote(get_typed_expr_type(e)));
if (is_inaccessible(e))
return mk_expr_placeholder();
throw elaborator_exception(e, sstream() << "invalid quotation, unsupported macro '"
<< macro_def(e).get_name() << "'");
}
lean_unreachable();
}
expr elaborate_quote(expr e, environment const &env, options const &opts, bool in_pattern) {
lean_assert(is_expr_quote(e));
e = get_quote_expr(e);
name x("_x");
buffer<expr> locals;
buffer<expr> aqs;
e = replace(e, [&](expr const & t, unsigned) {
if (is_antiquote(t)) {
expr local = mk_local(mk_fresh_name(), x.append_after(locals.size() + 1),
mk_expr_placeholder(), binder_info());
locals.push_back(local);
aqs.push_back(t);
return some_expr(local);
}
return none_expr();
});
e = copy_tag(e, Fun(locals, e));
metavar_context ctx;
local_context lctx;
elaborator elab(env, opts, "_elab_quote", ctx, lctx, false, in_pattern, /* in_quote */ true);
e = elab.elaborate(e);
e = elab.finalize(e, true, true).first;
expr body = e;
for (unsigned i = 0; i < aqs.size(); i++)
body = binding_body(body);
if (in_pattern) {
e = instantiate_rev(body, aqs.size(), aqs.data());
e = quote(e);
} else {
if (has_param_univ(body))
throw elaborator_exception(e, "invalid quotation, contains universe parameter");
e = mk_quote_core(e, true);
expr subst = mk_constant(get_expr_subst_name());
for (expr aq : aqs)
e = mk_app(subst, e, get_antiquote_expr(aq));
}
return 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);
@ -2937,6 +2855,15 @@ expr elaborator::visit_macro(expr const & e, optional<expr> const & expected_typ
return visit_structure_instance(e, expected_type);
} else if (is_frozen_name(e)) {
return visit(get_annotation_arg(e), expected_type);
} else if (is_expr_quote(e)) {
expr r = visit(get_quote_expr(e), none_expr());
if (has_metavar(r)) {
return mk_quote_core(r, /* is_expr */ true);
} else {
expr r_type = infer_type(r);
level l = dec_level(get_level(r_type, e), e);
return mk_reflected(r, r_type, l);
}
} else if (is_annotation(e)) {
expr r = visit(get_annotation_arg(e), expected_type);
return update_macro(e, 1, &r);

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

@ -348,10 +348,6 @@ pair<expr, level_param_names> elaborate(environment & env, options const & opts,
Throw exception is \c ctx does not contain the local constant. */
expr resolve_names(environment const & env, local_context const & lctx, expr const & e);
/** Elaborate the content of an quote macro. If \c in_pattern is true, return a reflected expression tree,
else return a new quote macro surrounded by \c expr.subst calls for antiquotations. */
expr elaborate_quote(expr e, environment const &env, options const &opts, bool in_pattern);
void initialize_elaborator();
void finalize_elaborator();
}

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

@ -1639,11 +1639,84 @@ struct to_pattern_fn {
}
};
static expr quote(expr const & e) {
switch (e.kind()) {
case expr_kind::Var:
return mk_app(mk_constant({"expr", "var"}), quote(var_idx(e)));
case expr_kind::Sort:
return mk_app(mk_constant({"expr", "sort"}), mk_expr_placeholder());
case expr_kind::Constant:
return mk_app(mk_constant({"expr", "const"}), quote(const_name(e)), mk_expr_placeholder());
case expr_kind::Meta:
return mk_expr_placeholder();
case expr_kind::Local:
throw elaborator_exception(e, sstream() << "invalid quotation, unexpected local constant '"
<< local_pp_name(e) << "'");
case expr_kind::App:
return mk_app(mk_constant({"expr", "app"}), quote(app_fn(e)), quote(app_arg(e)));
case expr_kind::Lambda:
return mk_app(mk_constant({"expr", "lam"}), mk_expr_placeholder(), mk_expr_placeholder(),
quote(binding_domain(e)), quote(binding_body(e)));
case expr_kind::Pi:
return mk_app(mk_constant({"expr", "pi"}), mk_expr_placeholder(), mk_expr_placeholder(),
quote(binding_domain(e)), quote(binding_body(e)));
case expr_kind::Let:
return mk_app(mk_constant({"expr", "elet"}), mk_expr_placeholder(), quote(let_type(e)),
quote(let_value(e)), quote(let_body(e)));
case expr_kind::Macro:
if (is_antiquote(e))
return get_antiquote_expr(e);
if (is_typed_expr(e))
return mk_typed_expr(quote(get_typed_expr_expr(e)), quote(get_typed_expr_type(e)));
if (is_inaccessible(e))
return mk_expr_placeholder();
throw elaborator_exception(e, sstream() << "invalid quotation, unsupported macro '"
<< macro_def(e).get_name() << "'");
}
lean_unreachable();
}
/** \brief Elaborate quote in an empty local context. We need to elaborate expr patterns in the parser to find out
their pattern variables. */
expr elaborate_quote(expr e, environment const & env, options const & opts) {
lean_assert(is_expr_quote(e));
e = get_quote_expr(e);
name x("_x");
buffer<expr> locals;
buffer<expr> aqs;
e = replace(e, [&](expr const & t, unsigned) {
if (is_antiquote(t)) {
expr local = mk_local(mk_fresh_name(), x.append_after(locals.size() + 1),
mk_expr_placeholder(), binder_info());
locals.push_back(local);
aqs.push_back(t);
return some_expr(local);
}
return none_expr();
});
e = copy_tag(e, Fun(locals, e));
metavar_context ctx;
local_context lctx;
elaborator elab(env, opts, "_elab_quote", ctx, lctx, false, /* in_pattern */ true, /* in_quote */ true);
e = elab.elaborate(e);
e = elab.finalize(e, true, true).first;
expr body = e;
for (unsigned i = 0; i < aqs.size(); i++)
body = binding_body(body);
e = instantiate_rev(body, aqs.size(), aqs.data());
e = quote(e);
return e;
}
expr parser::patexpr_to_pattern(expr const & pat_or_expr, bool skip_main_fn, buffer<expr> & new_locals) {
undef_id_to_local_scope scope(*this);
auto e = replace(pat_or_expr, [&](expr const & e) {
if (is_expr_quote(e)) {
return some_expr(elaborate_quote(e, env(), get_options(), /* in_pattern */ true));
return some_expr(elaborate_quote(e, env(), get_options()));
} else {
return none_expr();
}
@ -1713,7 +1786,7 @@ expr parser::patexpr_to_expr(expr const & pat_or_expr) {
// start with expr quotes, which may make more locals from inside antiquotations accessible
expr e = replace(pat_or_expr, [&](expr const & e, unsigned) {
if (is_expr_quote(e)) {
return some_expr(elaborate_quote(e, env(), get_options(), /* in_pattern */ false));
return some_expr(mk_quote(get_quote_expr(e), /* is_expr */ true));
} else {
return none_expr();
}

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

@ -221,7 +221,7 @@ struct parse_tactic_fn {
auto p = m_p.pos();
parser::quote_scope scope(m_p, true);
expr e = m_p.parse_expr(rbp);
return m_p.save_pos(mk_pexpr_quote(e), p);
return m_p.save_pos(mk_quote(e, /* is_expr */ false), p);
}
expr parse_elem_core(bool save_info) {

21
src/library/quote.cpp
View file

@ -12,6 +12,7 @@ Author: Leonardo de Moura
#include "library/constants.h"
#include "library/annotation.h"
#include "library/kernel_serializer.h"
#include "exception.h"
namespace lean {
static std::string * g_quote_opcode = nullptr;
@ -44,7 +45,7 @@ public:
return this == &other;
}
char const * prefix() const {
return "`(";
return m_type == *g_pexpr ? "``(" : "```(";
}
virtual void display(std::ostream & out) const {
out << prefix() << m_value << ")";
@ -73,7 +74,7 @@ bool is_quote(expr const & e) {
}
bool is_expr_quote(expr const &e) {
return is_quote(e) && static_cast<quote_macro const *>(macro_def(e).raw())->get_type() == *g_expr;
return is_quote(e) && static_cast<quote_macro const *>(macro_def(e).raw())->get_type() != *g_pexpr;
}
expr const & get_quote_expr(expr const & e) {
@ -81,6 +82,11 @@ expr const & get_quote_expr(expr const & e) {
return static_cast<quote_macro const *>(macro_def(e).raw())->get_value();
}
expr const & get_quote_type(expr const & e) {
lean_assert(is_quote(e));
return static_cast<quote_macro const *>(macro_def(e).raw())->get_type();
}
static name * g_antiquote = nullptr;
expr mk_antiquote(expr const & e) { return mk_annotation(*g_antiquote, e); }
@ -90,7 +96,7 @@ expr const & get_antiquote_expr(expr const & e) {
return get_annotation_arg(e);
}
expr mk_pexpr_quote(expr const &e) {
expr mk_quote(expr const & e, bool is_expr) {
name x("_x");
buffer<expr> locals;
buffer<expr> aqs;
@ -102,13 +108,16 @@ expr mk_pexpr_quote(expr const &e) {
aqs.push_back(get_antiquote_expr(t));
return some_expr(local);
}
if (is_local(t) && is_expr) {
throw generic_exception(t, "unexpected local in quotation expression");
}
return none_expr();
});
expr r = mk_quote_core(Fun(locals, s), false);
expr subst = mk_constant(get_pexpr_subst_name());
expr r = mk_quote_core(Fun(locals, s), is_expr);
expr subst = mk_constant(is_expr ? get_expr_subst_name() : get_pexpr_subst_name());
expr to_pexpr = mk_constant(get_to_pexpr_name());
for (expr const & aq : aqs) {
r = mk_app(subst, r, mk_app(to_pexpr, aq));
r = mk_app(subst, r, is_expr ? aq : mk_app(to_pexpr, aq));
}
return r;
}

3
src/library/quote.h
View file

@ -8,10 +8,11 @@ Author: Leonardo de Moura
#include "kernel/expr.h"
namespace lean {
expr mk_pexpr_quote(expr const &e);
expr mk_quote(expr const & e, bool is_expr);
bool is_quote(expr const & e);
bool is_expr_quote(expr const &e);
expr const & get_quote_expr(expr const & e);
expr const & get_quote_type(expr const & e);
expr mk_quote_core(expr const & e, bool is_expr);
expr mk_reflected(expr const & e, expr const & ty, level const & l);

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

@ -463,7 +463,7 @@ vm_obj expr_is_annotation(vm_obj const & _e) {
}
}
vm_obj reflect(vm_obj const &, vm_obj const &, vm_obj const & r) {
vm_obj reflected_to_expr(vm_obj const &, vm_obj const &, vm_obj const & r) {
return r;
}
@ -506,7 +506,7 @@ void initialize_vm_expr() {
DECLARE_VM_BUILTIN(name({"expr", "collect_univ_params"}), expr_collect_univ_params);
DECLARE_VM_CASES_BUILTIN(name({"expr", "cases_on"}), expr_cases_on);
DECLARE_VM_BUILTIN("reflect", reflect);
DECLARE_VM_BUILTIN(name({"reflected", "to_expr"}), reflected_to_expr);
DECLARE_VM_BUILTIN(name("mk_nat_val_ne_proof"), vm_mk_nat_val_ne_proof);
DECLARE_VM_BUILTIN(name("mk_nat_val_lt_proof"), vm_mk_nat_val_lt_proof);

2
src/library/vm/vm_pexpr.cpp
View file

@ -50,7 +50,7 @@ vm_obj pexpr_pos(vm_obj const & e) {
}
vm_obj pexpr_mk_quote_macro(vm_obj const & e) {
return to_obj(mk_pexpr_quote(to_expr(e)));
return to_obj(mk_quote(to_expr(e), /* is_expr */ false));
}
vm_obj pexpr_mk_prenum_macro(vm_obj const & n) {

6
tests/lean/eval_expr_error.lean.expected.out
View file

@ -1,8 +1,4 @@
eval_expr_error.lean:5:8: error: failed to synthesize type class instance for
A : Type,
tst1 : tactic unit,
a : expr
⊢ reflected A
eval_expr_error.lean:5:18: error: unexpected local in quotation expression
eval_expr_error.lean:8:0: error: invalid eval_expr, type mismatch
state:
⊢ true

8
tests/lean/run/pi_patterns.lean
View file

@ -1,6 +1,6 @@
open tactic
run_cmd do ```(%%a → %%b) ← pure ```(nat → nat) | failed, skip
run_cmd do ```(%%a → %%b) ← pure ```(Π (b : nat), nat) | failed, skip
run_cmd do ```(λ a : %%a, (%%b : %%c)) ← pure ```(λ n, n + 1) | failed, skip
run_cmd do ```(let a := (%%a : %%c) in (%%b : %%d)) ← pure ```(let n := 1 in n) | failed, skip
run_cmd do ```(%%a → %%b) ← pure ↑```(nat → nat) | failed, skip
run_cmd do ```(%%a → %%b) ← pure ↑```(Π (b : nat), nat) | failed, skip
run_cmd do ```(λ a : %%a, (%%b : %%c)) ← pure ↑```(λ n, n + 1) | failed, skip
run_cmd do ```(let a := (%%a : %%c) in (%%b : %%d)) ← pure ↑```(let n := 1 in n) | failed, skip