From 5fdf140096bb1a3be21d0427419040de024f1fd8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 7 May 2015 11:10:15 -0700 Subject: [PATCH] refactor(frontends/lean): simplify local_decls data-structure This is the first step for fixing #584 --- src/frontends/lean/local_decls.h | 23 ++++------------------- src/frontends/lean/parser.cpp | 16 +++++++--------- src/frontends/lean/parser.h | 7 +++++-- 3 files changed, 16 insertions(+), 30 deletions(-) diff --git a/src/frontends/lean/local_decls.h b/src/frontends/lean/local_decls.h index 33591f2c70..cb6ff17511 100644 --- a/src/frontends/lean/local_decls.h +++ b/src/frontends/lean/local_decls.h @@ -13,7 +13,7 @@ Author: Leonardo de Moura namespace lean { /** - \brief A "scoped" map from name to values. + \brief A map from name to values. It also supports the operation \c find_idx that returns "when a declaration was inserted into the map". */ @@ -21,20 +21,17 @@ template class local_decls { typedef name_map> map; typedef list> entries; - typedef std::tuple scope; - typedef list scopes; map m_map; - unsigned m_counter; - scopes m_scopes; entries m_entries; + unsigned m_counter; public: local_decls():m_counter(1) {} local_decls(local_decls const & d): - m_map(d.m_map), m_counter(d.m_counter), m_scopes(d.m_scopes), m_entries(d.m_entries) {} + m_map(d.m_map), m_entries(d.m_entries), m_counter(d.m_counter) {} void insert(name const & k, V const & v) { m_map.insert(k, mk_pair(v, m_counter)); - m_counter++; m_entries = cons(mk_pair(k, v), m_entries); + m_counter++; } void update(name const & k, V const & v) { if (auto it = m_map.find(k)) { @@ -47,18 +44,6 @@ public: unsigned find_idx(name const & k) const { auto it = m_map.find(k); return it ? it->second : 0; } bool contains(name const & k) const { return m_map.contains(k); } entries const & get_entries() const { return m_entries; } - void push() { m_scopes = cons(scope(m_map, m_counter, m_entries), m_scopes); } - void pop() { - lean_assert(!is_nil(m_scopes)); - std::tie(m_map, m_counter, m_entries) = head(m_scopes); - m_scopes = tail(m_scopes); - } - bool has_scopes() const { return !is_nil(m_scopes); } bool empty() const { return m_map.empty(); } - struct mk_scope { - local_decls & m_d; - mk_scope(local_decls & d):m_d(d) { m_d.push(); } - ~mk_scope() { m_d.pop(); } - }; }; } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index b9075812a3..7ed84e08ce 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -451,28 +451,26 @@ expr parser::mk_app(std::initializer_list const & args, pos_info const & p } void parser::push_local_scope(bool save_options) { - m_local_level_decls.push(); - m_local_decls.push(); optional opts; if (save_options) opts = m_ios.get_options(); m_parser_scope_stack = cons(parser_scope_stack_elem(opts, m_level_variables, m_variables, m_include_vars, - m_undef_ids.size(), m_has_params), + m_undef_ids.size(), m_has_params, m_local_level_decls, + m_local_decls), m_parser_scope_stack); } void parser::pop_local_scope() { - if (!m_local_level_decls.has_scopes()) { + if (!m_parser_scope_stack) { throw parser_error("invalid 'end', there is no open namespace/section", pos()); } - m_local_level_decls.pop(); - m_local_decls.pop(); - lean_assert(!is_nil(m_parser_scope_stack)); auto s = head(m_parser_scope_stack); if (s.m_options) { m_ios.set_options(*s.m_options); updt_options(); } + m_local_level_decls = s.m_local_level_decls; + m_local_decls = s.m_local_decls; m_level_variables = s.m_level_variables; m_variables = s.m_variables; m_include_vars = s.m_include_vars; @@ -912,8 +910,8 @@ void parser::parse_binders_core(buffer & r, buffer * nentr local_environment parser::parse_binders(buffer & r, buffer * nentries, bool & last_block_delimited, bool allow_empty, unsigned rbp, bool simple_only) { - flet save(m_env, m_env); // save environment - local_expr_decls::mk_scope scope(m_local_decls); + flet save1(m_env, m_env); // save environment + flet save2(m_local_decls, m_local_decls); unsigned old_sz = r.size(); parse_binders_core(r, nentries, last_block_delimited, rbp, simple_only); if (!allow_empty && old_sz == r.size()) diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index f93bbe151e..263868cdd5 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -54,10 +54,13 @@ struct parser_scope_stack_elem { name_set m_include_vars; unsigned m_num_undef_ids; bool m_has_params; + local_level_decls m_local_level_decls; + local_expr_decls m_local_decls; parser_scope_stack_elem(optional const & o, name_set const & lvs, name_set const & vs, name_set const & ivs, - unsigned num_undef_ids, bool has_params): + unsigned num_undef_ids, 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_has_params(has_params) {} + m_num_undef_ids(num_undef_ids), m_has_params(has_params), m_local_level_decls(lld), m_local_decls(led) {} }; typedef list parser_scope_stack;