From 0792bc13dbdcb5925de29d654f85459dbdd9227a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 14 Mar 2017 17:09:31 +0100 Subject: [PATCH] feat(frontends/lean/elaborator,init/meta/interactive): relax expr pattern elaboration and use it to implement a tactic signature pretty printer --- library/init/meta/interactive.lean | 67 ++++++++++++++++++++++++++++++ src/frontends/lean/elaborator.cpp | 15 ++++--- src/frontends/lean/elaborator.h | 3 +- src/frontends/lean/parser.cpp | 2 +- 4 files changed, 80 insertions(+), 7 deletions(-) diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 4ec4c17c5d..9a8c127c70 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -58,6 +58,73 @@ to_expr q ff tt namespace interactive open interactive interactive.types expr +open format +private meta def maybe_paren : list format → format +| [] := "" +| [f] := f +| fs := paren (join fs) + +private meta def unfold (e : expr) : tactic expr := do +(expr.const f_name f_lvls) ← return e^.get_app_fn | pp e >>= fail, +env ← get_env, +decl ← env^.get f_name, +new_f ← decl^.instantiate_value_univ_params f_lvls, +head_beta (expr.mk_app new_f e^.get_app_args) + +private meta def parser_desc_aux : expr → tactic (list format) +| ```(ident) := return ["id"] +| ```(qexpr) := return ["expr"] +| ```(tk %%c) := return <$> to_fmt <$> eval_expr string c +| ```(return ._) := return [] +| ```(._ <$> %%p) := parser_desc_aux p +| ```(%%p₁ <*> %%p₂) := do + f₁ ← parser_desc_aux p₁, + f₂ ← parser_desc_aux p₂, + return $ f₁ ++ [" "] ++ f₂ +| ```(%%p₁ <* %%p₂) := do + f₁ ← parser_desc_aux p₁, + f₂ ← parser_desc_aux p₂, + return $ f₁ ++ [" "] ++ f₂ +| ```(%%p₁ *> %%p₂) := do + f₁ ← parser_desc_aux p₁, + f₂ ← parser_desc_aux p₂, + return $ f₁ ++ [" "] ++ f₂ +| ```(many %%p) := do + f ← parser_desc_aux p, + return [maybe_paren f ++ "*"] +| ```(optional %%p) := do + f ← parser_desc_aux p, + return [maybe_paren f ++ "?"] +| ```(sep_by %%sep %%p) := do + f ← parser_desc_aux p, + fs ← eval_expr string sep, + return [maybe_paren f ++ to_fmt fs, " ..."] +| ```(%%p₁ <|> %%p₂) := do + f₁ ← parser_desc_aux p₁, + f₂ ← parser_desc_aux p₂, + return $ if list.empty f₁ then [maybe_paren f₂ ++ "?"] else + if list.empty f₂ then [maybe_paren f₁ ++ "?"] else + [maybe_paren f₁, " | ", maybe_paren f₂] +| e := do + e' ← unfold e, + if e ≠ e' then parser_desc_aux e' + else pp e >>= fail + +private meta def param_desc : expr → tactic format +| ```(parse %%p) := join <$> parser_desc_aux p +| ```(opt_param %%t ._) := (++ "?") <$> pp t +| e := paren <$> pp e + +meta def interactive_desc_aux : expr → tactic (list format) +| (expr.pi _ _ d b) := list.cons <$> param_desc d <*> interactive_desc_aux b +| _ := return [] + +meta def interactive_desc (n : name) : tactic format := do +env ← get_env, +decl ← env^.get n, +f ← interactive_desc_aux decl^.type, +return $ to_fmt n^.components^.ilast ++ " " ++ join (list.intersperse " " f) + /- itactic: parse a nested "interactive" tactic. That is, parse `(` tactic `)` diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 3d62ba6496..3ac30f44e1 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -128,11 +128,11 @@ elaborator_strategy get_elaborator_strategy(environment const & env, name const elaborator::elaborator(environment const & env, options const & opts, name const & decl_name, metavar_context const & mctx, local_context const & lctx, bool recover_from_errors, - bool in_pattern): + bool in_pattern, bool in_quote): m_env(env), m_opts(opts), m_decl_name(decl_name), m_ctx(env, opts, mctx, lctx, get_tcm(), transparency_mode::Semireducible), m_recover_from_errors(recover_from_errors), - m_uses_infom(get_global_info_manager() != nullptr), m_in_pattern(in_pattern) { + m_uses_infom(get_global_info_manager() != nullptr), m_in_pattern(in_pattern), m_in_quote(in_quote) { m_coercions = get_elaborator_coercions(opts); } @@ -307,7 +307,9 @@ bool elaborator::ready_to_synthesize(expr inst_type) { } expr elaborator::mk_instance(expr const & C, expr const & ref) { - if (!ready_to_synthesize(C)) { + if (m_in_pattern && m_in_quote) { + return mk_expr_placeholder(some(C)); + } else if (!ready_to_synthesize(C)) { expr inst = mk_metavar(C, ref); m_instances = cons(inst, m_instances); return inst; @@ -1245,6 +1247,9 @@ optional elaborator::process_optional_and_auto_params(expr type, expr cons new_arg = mk_local(mk_fresh_name(), binding_name(type), d, binding_info(type)); eta_args.push_back(new_arg); } + // implicit arguments are tagged as inaccessible in patterns + if (found && m_in_pattern) + new_arg = copy_tag(ref, mk_inaccessible(new_arg)); new_args.push_back(new_arg); type = instantiate(binding_body(type), new_arg); if (found) { @@ -2742,7 +2747,7 @@ expr elaborate_quote(expr e, environment const &env, options const &opts, bool i metavar_context ctx; local_context lctx; - elaborator elab(env, opts, "_elab_quote", ctx, lctx, false, in_pattern); + 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; @@ -3261,7 +3266,7 @@ void elaborator::report_error(tactic_state const & s, char const * state_header, void elaborator::ensure_no_unassigned_metavars(expr & e) { // TODO(gabriel): this needs to change e - if (!has_expr_metavar(e)) return; + if (!has_expr_metavar(e) || (m_in_pattern && m_in_quote)) return; for_each(e, [&](expr const & e, unsigned) { if (!has_expr_metavar(e)) return false; if (is_metavar_decl_ref(e) && !m_ctx.is_assigned(e)) { diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index ac7e85643e..4bc81107da 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -96,6 +96,7 @@ private: bool m_no_info{false}; bool m_in_pattern{false}; + bool m_in_quote{false}; expr get_default_numeral_type(); @@ -265,7 +266,7 @@ private: public: elaborator(environment const & env, options const & opts, name const & decl_name, metavar_context const & mctx, local_context const & lctx, - bool recover_from_errors = true, bool in_pattern = false); + bool recover_from_errors = true, bool in_pattern = false, bool in_quote = false); ~elaborator(); metavar_context const & mctx() const { return m_ctx.mctx(); } local_context const & lctx() const { return m_ctx.lctx(); } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index a734dde60b..32f87dd65d 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -114,7 +114,7 @@ LEAN_THREAD_VALUE(id_behavior, g_outer_id_behavior, id_behavior::ErrorIfUndef); parser::quote_scope::quote_scope(parser & p, bool q, id_behavior i): m_p(p), m_id_behavior(m_p.m_id_behavior), m_old_in_quote(m_p.m_in_quote), m_in_quote(q), m_saved_in_pattern(p.m_in_pattern) { - m_p.m_in_pattern = false; + // m_p.m_in_pattern = false; if (m_in_quote && !m_old_in_quote) { g_outer_id_behavior = m_p.m_id_behavior; m_p.m_id_behavior = i;