From 2825c5fbccd58413f104498fce563dbabab27469 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 28 Apr 2017 17:12:32 +0200 Subject: [PATCH] feat(frontends/lean/elaborator): elaborate ```(e) to type `reflected e` if possible and add coercion reflected -> expr --- library/init/meta/expr.lean | 12 ++- library/init/meta/smt/ematch.lean | 3 +- src/frontends/lean/builtin_exprs.cpp | 11 +-- src/frontends/lean/elaborator.cpp | 97 +++----------------- src/frontends/lean/elaborator.h | 4 - src/frontends/lean/parser.cpp | 77 +++++++++++++++- src/frontends/lean/tactic_notation.cpp | 2 +- src/library/quote.cpp | 21 +++-- src/library/quote.h | 3 +- src/library/vm/vm_expr.cpp | 4 +- src/library/vm/vm_pexpr.cpp | 2 +- tests/lean/eval_expr_error.lean.expected.out | 6 +- tests/lean/run/pi_patterns.lean | 8 +- 13 files changed, 128 insertions(+), 122 deletions(-) diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean index 0a6b4d5136..3933ef1b81 100644 --- a/library/init/meta/expr.lean +++ b/library/init/meta/expr.lean @@ -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⟩ diff --git a/library/init/meta/smt/ematch.lean b/library/init/meta/smt/ematch.lean index d8f3d4e8a4..0205ea3241 100644 --- a/library/init/meta/smt/ematch.lean +++ b/library/init/meta/smt/ematch.lean @@ -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 diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 8b9749a977..7a59d0449c 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -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); } diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 8d74491091..f19c9deb57 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -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 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 locals; - buffer 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 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 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); diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index aa19f0f773..5e1912cf23 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -348,10 +348,6 @@ pair 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(); } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index f5f1ba0f2c..5bf0699463 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -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 locals; + buffer 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 & 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(); } diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp index b655ce121d..7b66862a27 100644 --- a/src/frontends/lean/tactic_notation.cpp +++ b/src/frontends/lean/tactic_notation.cpp @@ -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) { diff --git a/src/library/quote.cpp b/src/library/quote.cpp index ddd847fba3..d2c05ce1ac 100644 --- a/src/library/quote.cpp +++ b/src/library/quote.cpp @@ -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(macro_def(e).raw())->get_type() == *g_expr; + return is_quote(e) && static_cast(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(macro_def(e).raw())->get_value(); } +expr const & get_quote_type(expr const & e) { + lean_assert(is_quote(e)); + return static_cast(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 locals; buffer 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; } diff --git a/src/library/quote.h b/src/library/quote.h index 6c8c170fd7..2b422ea11f 100644 --- a/src/library/quote.h +++ b/src/library/quote.h @@ -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); diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp index b5f6d7aefd..3f5d1108e9 100644 --- a/src/library/vm/vm_expr.cpp +++ b/src/library/vm/vm_expr.cpp @@ -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); diff --git a/src/library/vm/vm_pexpr.cpp b/src/library/vm/vm_pexpr.cpp index 0168a652f7..810952fa3e 100644 --- a/src/library/vm/vm_pexpr.cpp +++ b/src/library/vm/vm_pexpr.cpp @@ -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) { diff --git a/tests/lean/eval_expr_error.lean.expected.out b/tests/lean/eval_expr_error.lean.expected.out index bf5463ec6b..dc5b52abaa 100644 --- a/tests/lean/eval_expr_error.lean.expected.out +++ b/tests/lean/eval_expr_error.lean.expected.out @@ -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 diff --git a/tests/lean/run/pi_patterns.lean b/tests/lean/run/pi_patterns.lean index f3cd6347be..e5dd4f08ea 100644 --- a/tests/lean/run/pi_patterns.lean +++ b/tests/lean/run/pi_patterns.lean @@ -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