From 28d63262282e03004b6fa625e7ee12ae1adfa504 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 7 Feb 2018 11:16:32 -0800 Subject: [PATCH] refactor(frontends/lean/parser): add name_generator --- src/frontends/lean/builtin_exprs.cpp | 18 +++++++++--------- src/frontends/lean/decl_cmds.cpp | 2 +- src/frontends/lean/inductive_cmds.cpp | 2 +- src/frontends/lean/match_expr.cpp | 4 ++-- src/frontends/lean/module_parser.cpp | 5 +++-- src/frontends/lean/parser.cpp | 19 ++++++++++++------- src/frontends/lean/parser.h | 3 +++ src/frontends/lean/parser_state.h | 10 ++++++---- src/frontends/lean/structure_cmd.cpp | 4 ++-- 9 files changed, 39 insertions(+), 28 deletions(-) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index f8ea991611..89c9d852fb 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -187,7 +187,7 @@ static expr parse_let(parser_state & 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(mk_fresh_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(true)), 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); @@ -320,7 +320,7 @@ static expr parse_do(parser_state & 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(mk_fresh_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(true)), pos); buffer locals; to_buffer(lhss_locals[i], locals); buffer eqs; @@ -336,7 +336,7 @@ static expr parse_do(parser_state & p, bool has_braces) { } // add case // _ := else_case - expr x = mk_local(mk_fresh_name(), "_x", mk_expr_placeholder(), binder_info()); + expr x = mk_local(p.next_name(), "_x", mk_expr_placeholder(), binder_info()); expr else_eq = Fun(fn, Fun(x, p.save_pos(mk_equation(p.rec_save_pos(mk_app(fn, x), pos), else_case, ignore_if_unused), @@ -748,10 +748,10 @@ static expr parse_lambda_constructor(parser_state & 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(mk_fresh_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(true)), 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(mk_fresh_name(), "_x", mk_expr_placeholder(), binder_info()), pos); + expr x = p.rec_save_pos(mk_local(p.next_name(), "_x", mk_expr_placeholder(), binder_info()), pos); bool use_cache = false; return p.rec_save_pos(Fun(x, mk_app(mk_equations(h, 1, &eqn), x), use_cache), pos); } @@ -829,12 +829,12 @@ static expr parse_infix_paren(parser_state & p, list const expr args[2]; buffer vars; bool fixed_second_arg = false; - args[0] = mk_local(mk_fresh_name(), "_x", mk_expr_placeholder(), binder_info()); + args[0] = mk_local(p.next_name(), "_x", mk_expr_placeholder(), binder_info()); vars.push_back(args[0]); p.next(); if (p.curr_is_token(get_rparen_tk())) { p.next(); - args[1] = mk_local(mk_fresh_name(), "_y", mk_expr_placeholder(), binder_info()); + args[1] = mk_local(p.next_name(), "_y", mk_expr_placeholder(), binder_info()); vars.push_back(args[1]); } else { fixed_second_arg = true; @@ -897,9 +897,9 @@ static expr parse_lambda_cons(parser_state & p, unsigned, expr const *, pos_info throw parser_error("invalid '(::)' notation, declaration for operator '::' is not compatible with the `(::)` syntactic sugar", pos); expr args[2]; buffer vars; - args[0] = mk_local(mk_fresh_name(), "_x", mk_expr_placeholder(), binder_info()); + args[0] = mk_local(p.next_name(), "_x", mk_expr_placeholder(), binder_info()); vars.push_back(args[0]); - args[1] = mk_local(mk_fresh_name(), "_y", mk_expr_placeholder(), binder_info()); + args[1] = mk_local(p.next_name(), "_y", mk_expr_placeholder(), binder_info()); vars.push_back(args[1]); buffer cs; for (notation::accepting const & acc : head(ts).second.is_accepting()) { diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 15ae45ed7d..607e3c5b6f 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -104,7 +104,7 @@ static environment declare_var(parser & p, environment env, if (p.get_local(n)) throw parser_error(sstream() << "invalid parameter/variable declaration, '" << n << "' has already been declared", pos); - name u = mk_fresh_name(); + name u = p.next_name(); expr l = p.save_pos(mk_local(u, n, type, bi), pos); if (k == variable_kind::Parameter) p.add_parameter(n, l); diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp index 02375a1f69..b626cb7e43 100644 --- a/src/frontends/lean/inductive_cmds.cpp +++ b/src/frontends/lean/inductive_cmds.cpp @@ -230,7 +230,7 @@ class inductive_cmd_fn { /** \brief Create a local constant based on the given binding */ expr mk_local_for(expr const & b) { - return mk_local(mk_fresh_name(), binding_name(b), binding_domain(b), binding_info(b), b.get_tag()); + return mk_local(m_p.next_name(), binding_name(b), binding_domain(b), binding_info(b), b.get_tag()); } /* \brief Add \c lvl to \c r_lvls (if it is not already there). diff --git a/src/frontends/lean/match_expr.cpp b/src/frontends/lean/match_expr.cpp index 35f23a9ad2..f7bdf3e97b 100644 --- a/src/frontends/lean/match_expr.cpp +++ b/src/frontends/lean/match_expr.cpp @@ -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(mk_fresh_name(), *g_match_name, type, mk_rec_info(true)); + fn = mk_local(p.next_name(), *g_match_name, type, mk_rec_info(true)); } else { - fn = mk_local(mk_fresh_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(true)); } p.check_token_next(get_with_tk(), "invalid 'match' expression, 'with' expected"); diff --git a/src/frontends/lean/module_parser.cpp b/src/frontends/lean/module_parser.cpp index 64adc1c178..a803997451 100644 --- a/src/frontends/lean/module_parser.cpp +++ b/src/frontends/lean/module_parser.cpp @@ -36,7 +36,8 @@ pair> module_parser::resume(module_parser_result const & res, optional> const & dependencies) { snapshot const & s = *res.m_snapshot_at_end; m_parser.m_scanner.skip_to_pos(s.m_pos); - m_parser.m_env = s.m_env; + m_parser.m_env = s.m_env; + m_parser.m_ngen = s.m_ngen; m_parser.m_ios.set_options(s.m_options); m_parser.m_local_level_decls = s.m_lds; m_parser.m_local_decls = s.m_eds; @@ -47,7 +48,7 @@ module_parser::resume(module_parser_result const & res, optional 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), + expr local = mk_local(p.next_name(), x.append_after(locals.size() + 1), mk_expr_placeholder(), binder_info()); locals.push_back(local); aqs.push_back(t); @@ -1821,7 +1824,7 @@ expr parser::patexpr_to_pattern(expr const & pat_or_expr, bool skip_main_fn, buf 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())); + return some_expr(elaborate_quote(*this, e)); } else { return none_expr(); } @@ -2584,7 +2587,7 @@ bool parser::curr_is_command_like() const { std::shared_ptr parser::mk_snapshot() { return std::make_shared( - m_env, m_local_level_decls, m_local_decls, + m_env, m_ngen, m_local_level_decls, m_local_decls, m_level_variables, m_variables, m_include_vars, m_ios.get_options(), m_imports_parsed, m_ignore_noncomputable, m_parser_scope_stack, m_next_inst_idx, pos()); } @@ -2669,6 +2672,7 @@ bool parse_commands(environment & env, io_state & ios, char const * fname) { } void initialize_parser() { + g_frontend_fresh = new name("_ffresh"); g_parser_show_errors = new name{"parser", "show_errors"}; register_bool_option(*g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS, "(lean parser) display error messages in the regular output channel"); @@ -2676,6 +2680,7 @@ void initialize_parser() { } void finalize_parser() { + delete g_frontend_fresh; delete g_tmp_prefix; delete g_parser_show_errors; } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 42e6c7f271..22bfce11eb 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -37,6 +37,7 @@ class scope_message_context; class parser : public abstract_parser { environment m_env; + name_generator m_ngen; io_state m_ios; bool m_use_exceptions; bool m_show_errors; @@ -213,6 +214,8 @@ public: void init_scanner(); + name next_name() { return m_ngen.next(); } + void set_break_at_pos(pos_info const & pos) { m_break_at_pos = some(pos); } optional const & get_break_at_pos() const { return m_break_at_pos; } template diff --git a/src/frontends/lean/parser_state.h b/src/frontends/lean/parser_state.h index bddb0d53ee..229a0fce85 100644 --- a/src/frontends/lean/parser_state.h +++ b/src/frontends/lean/parser_state.h @@ -511,6 +511,7 @@ typedef list parser_scope_stack; /* For storing checkpoints in a file/buffer. This object is not exposed in the Lean API. */ struct snapshot { environment m_env; + name_generator m_ngen; local_level_decls m_lds; local_expr_decls m_eds; name_set m_lvars; // subset of m_lds that is tagged as level variable @@ -522,15 +523,16 @@ struct snapshot { parser_scope_stack m_parser_scope_stack; unsigned m_next_inst_idx; pos_info m_pos; - name_generator m_name_gen_snapshot; - snapshot(environment const & env, local_level_decls const & lds, + /* TODO(Leo): delete following field after we remove ::lean::mk_fresh_name */ + name_generator m_global_ngen; + snapshot(environment const & env, name_generator const & ngen, local_level_decls const & lds, local_expr_decls const & eds, name_set const & lvars, name_set const & vars, name_set const & includes, options const & opts, bool imports_parsed, bool noncomputable_theory, parser_scope_stack const & pss, unsigned next_inst_idx, pos_info const & pos): - m_env(env), m_lds(lds), m_eds(eds), m_lvars(lvars), m_vars(vars), m_include_vars(includes), + m_env(env), m_ngen(ngen), m_lds(lds), m_eds(eds), m_lvars(lvars), m_vars(vars), m_include_vars(includes), m_options(opts), m_imports_parsed(imports_parsed), m_noncomputable_theory(noncomputable_theory), m_parser_scope_stack(pss), m_next_inst_idx(next_inst_idx), m_pos(pos), - m_name_gen_snapshot(get_fresh_name_generator_snapshot()) {} + m_global_ngen(get_fresh_name_generator_snapshot()) {} }; } diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index db83990e27..5b40267591 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -902,7 +902,7 @@ struct structure_cmd_fn { return elab(tmp); expr type = decl.get_type(); expr value = *decl.m_default_val; - expr new_tmp = elab(mk_let(mk_fresh_name(), type, value, tmp)); + expr new_tmp = elab(mk_let(m_p.next_name(), type, value, tmp)); decl.m_local = update_local(decl.m_local, let_type(new_tmp), local_info(decl.m_local)); decl.m_default_val = let_value(new_tmp); return let_body(new_tmp); @@ -1215,7 +1215,7 @@ struct structure_cmd_fn { binder_info bi; if (m_meta_info.m_attrs.has_class()) bi = mk_inst_implicit_binder_info(); - expr st = mk_local(mk_fresh_name(), "s", st_type, bi); + expr st = mk_local(m_p.next_name(), "s", st_type, bi); expr coercion_type = infer_implicit(Pi(m_params, Pi(st, parent, m_p), m_p), m_params.size(), true);; expr coercion_value = parent_intro; for (unsigned idx : fmap) {