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

refactor(frontends/lean/parser): add name_generator

Browse source
This commit is contained in:
Leonardo de Moura 2018-02-07 11:16:32 -08:00
parent fa2e67e8f3
commit 28d6326228
9 changed files with 39 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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<expr> locals;
to_buffer(lhss_locals[i], locals);
buffer<expr> 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<notation::accepting> const
expr args[2];
buffer<expr> 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<expr> 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<expr> cs;
for (notation::accepting const & acc : head(ts).second.is_accepting()) {

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

@ -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);

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

@ -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).

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

@ -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");

5
src/frontends/lean/module_parser.cpp
View file

@ -36,7 +36,8 @@ pair<cancellation_token, task<module_parser_result>>
module_parser::resume(module_parser_result const & res, optional<std::vector<gtask>> 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<std::vector<gta
m_parser.m_ignore_noncomputable = s.m_noncomputable_theory;
m_parser.m_parser_scope_stack = s.m_parser_scope_stack;
m_parser.m_next_inst_idx = s.m_next_inst_idx;
set_fresh_name_generator(s.m_name_gen_snapshot);
set_fresh_name_generator(s.m_global_ngen);
auto lt = res.m_lt;
scope_log_tree_core scope_lt(&lt);
return parse_next_command_like(dependencies);

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

@ -70,6 +70,7 @@ Author: Leonardo de Moura
#endif
namespace lean {
static name * g_frontend_fresh = nullptr;
void break_at_pos_exception::report_goal_pos(pos_info goal_pos) {
if (!m_goal_pos)
@ -1407,7 +1408,7 @@ expr parser::parse_notation(parse_table t, expr * left) {
unsigned idx = 1;
for (expr & arg : args) {
actual_args.push_back(arg);
arg = mk_local(mk_fresh_name(), x.append_after(idx), mk_expr_placeholder(), binder_info());
arg = mk_local(next_name(), x.append_after(idx), mk_expr_placeholder(), binder_info());
idx++;
}
}
@ -1459,7 +1460,7 @@ expr parser::parse_placeholder() {
expr parser::parse_anonymous_var_pattern() {
auto p = pos();
next();
expr t = mk_local(mk_fresh_name(), "_x", mk_expr_placeholder(), binder_info());
expr t = mk_local(next_name(), "_x", mk_expr_placeholder(), binder_info());
return save_pos(t, p);
}
@ -1609,7 +1610,7 @@ struct to_pattern_fn {
} else if (is_inaccessible(e)) {
// do nothing
} else if (is_placeholder(e)) {
expr r = copy_tag(e, mk_local(mk_fresh_name(), "_x", copy_tag(e, mk_expr_placeholder()), binder_info()));
expr r = copy_tag(e, mk_local(m_parser.next_name(), "_x", copy_tag(e, mk_expr_placeholder()), binder_info()));
m_new_locals.push_back(r);
m_anonymous_vars.insert(mk_pair(e, r));
} else if (is_as_pattern(e)) {
@ -1782,8 +1783,10 @@ static expr quote(expr const & e) {
/** \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) {
static expr elaborate_quote(parser & p, expr e) {
lean_assert(is_expr_quote(e));
environment const & env = p.env();
options const & opts = p.get_options();
e = get_expr_quote_value(e);
name x("_x");
@ -1791,7 +1794,7 @@ expr elaborate_quote(expr e, environment const & env, options const & opts) {
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),
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<snapshot> parser::mk_snapshot() {
return std::make_shared<snapshot>(
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;
}

3
src/frontends/lean/parser.h
View file

@ -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<pos_info> const & get_break_at_pos() const { return m_break_at_pos; }
template <class T>

10
src/frontends/lean/parser_state.h
View file

@ -511,6 +511,7 @@ typedef list<parser_scope> 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()) {}
};
}

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

@ -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) {