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

feat(frontends/lean): add scope management to parser_state, remove unnecessary undef_ids

Browse source
This commit is contained in:
Leonardo de Moura 2017-02-08 11:58:14 -08:00
parent 1fb49baaaa
commit aa5eea6416
4 changed files with 115 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -483,7 +483,7 @@ expr parser::mk_app(std::initializer_list<expr> const & args, pos_info const & p
parser_scope parser::mk_parser_scope(optional<options> const & opts) {
return parser_scope(opts, m_level_variables, m_variables, m_include_vars,
m_undef_ids.size(), m_next_inst_idx, m_has_params,
m_next_inst_idx, m_has_params,
m_local_level_decls, m_local_decls);
}
@ -512,7 +512,6 @@ void parser::pop_local_scope() {
lean_assert(m_parser_scope_stack);
auto s = head(m_parser_scope_stack);
restore_parser_scope(s);
m_undef_ids.shrink(s.m_num_undef_ids);
m_parser_scope_stack = tail(m_parser_scope_stack);
}
@ -1813,8 +1812,6 @@ expr parser::id_to_expr(name const & id, pos_info const & p, bool resolve_only)
if (!r) {
if (m_id_behavior == id_behavior::AssumeLocalIfUndef) {
expr local = mk_local(id, save_pos(mk_expr_placeholder(), p));
if (!resolve_only)
m_undef_ids.push_back(local);
r = save_pos(local, p);
}
}

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

@ -74,8 +74,6 @@ class parser : public abstract_parser {
// curr command token
name m_cmd_token;
buffer<expr> m_undef_ids;
// profiling
bool m_profile;
@ -458,11 +456,6 @@ public:
struct error_if_undef_scope : public flet<id_behavior> { error_if_undef_scope(parser & p); };
struct all_id_local_scope : public flet<id_behavior> { all_id_local_scope(parser & p); };
/** \brief Return the size of the stack of undefined local constants */
unsigned get_num_undef_ids() const { return m_undef_ids.size(); }
/** \brief Return the i-th undefined local constants */
expr const & get_undef_id(unsigned i) const { return m_undef_ids[i]; }
private:
pair<expr, level_param_names> elaborate(name const & decl_name, metavar_context & mctx, local_context_adapter const & adapter,
expr const & e, bool check_unassigned = true);

121
src/frontends/lean/parser_state.cpp
View file

@ -10,6 +10,7 @@ Author: Leonardo de Moura
#include "kernel/for_each_fn.h"
#include "library/class.h"
#include "library/deep_copy.h"
#include "library/quote.h"
#include "frontends/lean/parser_state.h"
#include "frontends/lean/tokens.h"
@ -108,14 +109,34 @@ name parser_state::mk_anonymous_inst_name() {
return n;
}
optional<pos_info> parser_state::get_pos_info(expr const & /* e */) const {
/* TODO(Leo): */
return optional<pos_info>();
optional<pos_info> parser_state::get_pos_info(expr const & e) const {
tag t = e.get_tag();
if (t == nulltag)
return optional<pos_info>();
if (auto it = m_pos_table.find(t))
return optional<pos_info>(*it);
else
return optional<pos_info>();
}
token const * parser_state::get_last_cmd_tk() const {
unsigned i = m_tv_cmd_idx;
while (true) {
token const & tk = get_token(i);
if (tk.kind() == token_kind::CommandKeyword &&
tk.get_token_info().token() != get_end_tk()) {
return &tk;
}
if (i == 0) return nullptr;
i--;
}
}
pos_info parser_state::get_some_pos() const {
/* TODO(Leo): */
return pos_info(0, 0);
if (token const * tk = get_last_cmd_tk())
return tk->get_pos();
else
return get_token(0).get_pos();
}
expr parser_state::save_pos(expr e, pos_info p) {
@ -149,16 +170,24 @@ expr parser_state::rec_save_pos(expr const & e, pos_info p) {
expr parser_state::copy_with_new_pos(expr const & e, pos_info p) {
switch (e.kind()) {
case expr_kind::Sort: case expr_kind::Constant: case expr_kind::Meta:
case expr_kind::Local: case expr_kind::Var:
case expr_kind::Var: case expr_kind::Local:
return save_pos(copy(e), p);
case expr_kind::App:
return save_pos(::lean::mk_app(copy_with_new_pos(app_fn(e), p),
copy_with_new_pos(app_arg(e), p)),
p);
case expr_kind::Lambda: case expr_kind::Pi:
return save_pos(update_binding(e,
copy_with_new_pos(binding_domain(e), p),
copy_with_new_pos(binding_body(e), p)),
case expr_kind::Lambda:
return save_pos(::lean::mk_lambda(binding_name(e),
copy_with_new_pos(binding_domain(e), p),
copy_with_new_pos(binding_body(e), p),
binding_info(e)),
p);
case expr_kind::Pi:
return save_pos(::lean::mk_pi(binding_name(e),
copy_with_new_pos(binding_domain(e), p),
copy_with_new_pos(binding_body(e), p),
binding_info(e)),
p);
case expr_kind::Let:
return save_pos(::lean::mk_let(let_name(e),
@ -166,12 +195,16 @@ expr parser_state::copy_with_new_pos(expr const & e, pos_info p) {
copy_with_new_pos(let_value(e), p),
copy_with_new_pos(let_body(e), p)),
p);
case expr_kind::Macro: {
buffer<expr> args;
for (unsigned i = 0; i < macro_num_args(e); i++)
args.push_back(copy_with_new_pos(macro_arg(e, i), p));
return save_pos(::lean::mk_macro(macro_def(e), args.size(), args.data()), p);
}}
case expr_kind::Macro:
if (is_quote(e)) {
return save_pos(mk_quote_core(copy_with_new_pos(get_quote_expr(e), p)), p);
} else {
buffer<expr> args;
for (unsigned i = 0; i < macro_num_args(e); i++)
args.push_back(copy_with_new_pos(macro_arg(e, i), p));
return save_pos(::lean::mk_macro(macro_def(e), args.size(), args.data()), p);
}
}
lean_unreachable(); // LCOV_EXCL_LINE
}
@ -254,4 +287,60 @@ name parser_state::check_atomic_decl_id_next(char const * msg) {
return id;
}
expr parser_state::mk_app(expr fn, expr arg, pos_info const & p) {
return save_pos(::lean::mk_app(fn, arg), p);
}
expr parser_state::mk_app(expr fn, buffer<expr> const & args, pos_info const & p) {
expr r = fn;
for (expr const & arg : args) {
r = mk_app(r, arg, p);
}
return r;
}
expr parser_state::mk_app(std::initializer_list<expr> const & args, pos_info const & p) {
lean_assert(args.size() >= 2);
auto it = args.begin();
expr r = *it;
it++;
for (; it != args.end(); it++)
r = mk_app(r, *it, p);
return r;
}
parser_state::scope parser_state::mk_scope(optional<options> const & opts) {
return scope(opts, m_context->m_level_variables, m_context->m_variables, m_context->m_include_vars,
m_next_inst_idx, m_has_params, m_context->m_local_level_decls, m_context->m_local_decls);
}
void parser_state::restore_scope(scope const & s) {
ensure_exclusive_context();
if (s.m_options) {
m_context->m_ios.set_options(*s.m_options);
}
m_context->m_local_level_decls = s.m_local_level_decls;
m_context->m_local_decls = s.m_local_decls;
m_context->m_level_variables = s.m_level_variables;
m_context->m_variables = s.m_variables;
m_context->m_include_vars = s.m_include_vars;
m_has_params = s.m_has_params;
m_next_inst_idx = s.m_next_inst_idx;
}
void parser_state::push_local_scope(bool save_options) {
ensure_exclusive_context();
optional<options> opts;
if (save_options)
opts = m_context->m_ios.get_options();
m_context->m_scope_stack = cons(mk_scope(opts), m_context->m_scope_stack);
}
void parser_state::pop_local_scope() {
lean_assert(m_context->m_scope_stack);
ensure_exclusive_context();
auto s = head(m_context->m_scope_stack);
restore_scope(s);
m_context->m_scope_stack = tail(m_context->m_scope_stack);
}
}

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

@ -73,16 +73,15 @@ public:
name_set m_level_variables;
name_set m_variables;
name_set m_include_vars;
unsigned m_num_undef_ids;
unsigned m_next_inst_idx;
bool m_has_params;
local_level_decls m_local_level_decls;
local_expr_decls m_local_decls;
scope(optional<options> const & o, name_set const & lvs, name_set const & vs, name_set const & ivs,
unsigned num_undef_ids, unsigned next_inst_idx, bool has_params,
unsigned next_inst_idx, bool has_params,
local_level_decls const & lld, local_expr_decls const & led):
m_options(o), m_level_variables(lvs), m_variables(vs), m_include_vars(ivs),
m_num_undef_ids(num_undef_ids), m_next_inst_idx(next_inst_idx), m_has_params(has_params),
m_next_inst_idx(next_inst_idx), m_has_params(has_params),
m_local_level_decls(lld), m_local_decls(led) {}
};
@ -106,7 +105,6 @@ public:
name_set m_include_vars; // subset of m_local_decls that is marked as include
scope_stack m_scope_stack;
scope_stack m_quote_stack;
list<expr> m_undef_ids;
/* Tasks that need to be successful (no exception) for parsing to succeed. */
list<generic_task_result> m_required_successes;
context(environment const & env, io_state const & ios):m_env(env), m_ios(ios) {}
@ -228,6 +226,8 @@ private:
void ensure_exclusive_context();
token const * get_last_cmd_tk() const;
public:
parser_state(environment const & env, io_state const & ios, header_ptr const & h,
bool use_exceptions = false, std::shared_ptr<snapshot const> const & s = {});
@ -236,6 +236,7 @@ public:
environment const & env() const { return m_context->m_env; }
std::vector<token> const & get_token_vector() const { return m_header->m_token_vector; }
token const & get_token(unsigned i) const { return m_header->m_token_vector[i]; }
token const & curr_token() const { return get_token_vector()[m_tv_curr_idx]; }
token_kind curr() const { return curr_token().kind(); }
@ -296,12 +297,15 @@ public:
/** \brief Check if the current token is a constant, if it is, return it and move to next token, otherwise throw an exception. */
name check_constant_next(char const * msg);
void check_break_at_pos(break_at_pos_exception::token_context ctxt = break_at_pos_exception::token_context::none);
/** \brief Throw \c break_at_pos_exception with empty token and given context if \c m_break_at_pos is before current
position. */
void check_break_before(break_at_pos_exception::token_context ctxt = break_at_pos_exception::token_context::none);
expr mk_app(expr fn, expr arg, pos_info const & p);
expr mk_app(expr fn, buffer<expr> const & args, pos_info const & p);
expr mk_app(std::initializer_list<expr> const & args, pos_info const & p);
name mk_anonymous_inst_name();
bool parse_local_notation_decl() { return parse_local_notation_decl(nullptr); }
@ -467,8 +471,6 @@ public:
struct error_if_undef_scope : public flet<id_behavior> { error_if_undef_scope(parser_state & p); };
struct all_id_local_scope : public flet<id_behavior> { all_id_local_scope(parser_state & p); };
list<expr> get_undef_ids() const { return m_context->m_undef_ids; }
private:
pair<expr, level_param_names> elaborate(name const & decl_name, metavar_context & mctx, local_context_adapter const & adapter,
expr const & e, bool check_unassigned = true);