From 2141ee12f464268e1c300e85ba5ec2166d475065 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 7 Nov 2013 10:00:12 -0800 Subject: [PATCH] refactor(frontends/lean): use extension objects to store lean default frontend data in the environment Signed-off-by: Leonardo de Moura --- src/frontends/lean/frontend.cpp | 304 +++++++++++++------------- src/frontends/lean/frontend.h | 89 +++----- src/frontends/lean/parser.cpp | 10 +- src/frontends/lean/parser.h | 8 +- src/tests/frontends/lean/frontend.cpp | 1 - src/tests/frontends/lean/parser.cpp | 2 +- 6 files changed, 192 insertions(+), 222 deletions(-) diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp index 61e03b661..c16a2c576 100644 --- a/src/frontends/lean/frontend.cpp +++ b/src/frontends/lean/frontend.cpp @@ -25,8 +25,10 @@ Author: Leonardo de Moura namespace lean { static std::vector g_empty_vector; -/** \brief Implementation of the Lean frontend */ -struct frontend::imp { +/** + \brief Environment extension object for the Lean default frontend. +*/ +struct lean_extension : public environment::extension { typedef std::pair, name> implicit_info; // Remark: only named objects are stored in the dictionary. typedef std::unordered_map operator_table; @@ -36,9 +38,6 @@ struct frontend::imp { typedef std::unordered_map, expr_hash, std::equal_to> expr_to_coercions; typedef std::unordered_set> coercion_set; - std::atomic m_num_children; - std::shared_ptr m_parent; - environment m_env; operator_table m_nud; // nud table for Pratt's parser operator_table m_led; // led table for Pratt's parser expr_to_operators m_expr_to_operators; // map denotations to operators (this is used for pretty printing) @@ -46,21 +45,19 @@ struct frontend::imp { coercion_map m_coercion_map; // mapping from (given_type, expected_type) -> coercion coercion_set m_coercion_set; // Set of coercions expr_to_coercions m_type_coercions; // mapping type -> list (to-type, function) - state m_state; - bool has_children() const { return m_num_children > 0; } - void inc_children() { m_num_children++; } - void dec_children() { m_num_children--; } - - bool has_parent() const { return m_parent != nullptr; } + lean_extension const * get_parent() const { + return environment::extension::get_parent(); + } /** \brief Return the nud operator for the given symbol. */ operator_info find_nud(name const & n) const { auto it = m_nud.find(n); if (it != m_nud.end()) return it->second; - else if (has_parent()) - return m_parent->find_nud(n); + lean_extension const * parent = get_parent(); + if (parent) + return parent->find_nud(n); else return operator_info(); } @@ -70,8 +67,9 @@ struct frontend::imp { auto it = m_led.find(n); if (it != m_led.end()) return it->second; - else if (has_parent()) - return m_parent->find_led(n); + lean_extension const * parent = get_parent(); + if (parent) + return parent->find_led(n); else return operator_info(); } @@ -110,17 +108,18 @@ struct frontend::imp { return op; } } - - if (has_parent()) - return m_parent->find_op_for(e, unicode); + lean_extension const * parent = get_parent(); + if (parent) + return parent->find_op_for(e, unicode); else return operator_info(); } /** \brief Remove all internal denotations that are associated with the given operator symbol (aka notation) */ void remove_bindings(operator_info const & op) { + lean_extension const * parent = get_parent(); for (expr const & d : op.get_denotations()) { - if (has_parent() && m_parent->find_op_for(d, true)) { + if (parent && parent->find_op_for(d, true)) { // parent has an association for d... we must hide it. insert(m_expr_to_operators, d, list(operator_info())); } else { @@ -129,6 +128,7 @@ struct frontend::imp { } } + /** \brief Add a new entry d -> op in the mapping m_expr_to_operators */ void insert_expr_to_operator_entry(expr const & d, operator_info const & op) { list & l = m_expr_to_operators[d]; @@ -181,7 +181,7 @@ struct frontend::imp { 2) It is a real conflict, and report the issue in the diagnostic channel, and override the existing operator (aka notation). */ - void add_op(operator_info new_op, expr const & d, bool led) { + void add_op(operator_info new_op, expr const & d, bool led, environment & env, state & st) { name const & opn = new_op.get_op_name(); operator_info old_op = find_op(opn, led); if (!old_op) { @@ -199,31 +199,21 @@ struct frontend::imp { register_new_op(new_op, d, led); } } else { - diagnostic(m_state) << "The denotation(s) for the existing notation:\n " << old_op - << "\nhave been replaced with the new denotation:\n " << d - << "\nbecause they conflict on how implicit arguments are used.\n"; + diagnostic(st) << "The denotation(s) for the existing notation:\n " << old_op + << "\nhave been replaced with the new denotation:\n " << d + << "\nbecause they conflict on how implicit arguments are used.\n"; remove_bindings(old_op); register_new_op(new_op, d, led); } } else { - diagnostic(m_state) << "Notation has been redefined, the existing notation:\n " << old_op - << "\nhas been replaced with:\n " << new_op << "\nbecause they conflict with each other.\n"; + diagnostic(st) << "Notation has been redefined, the existing notation:\n " << old_op + << "\nhas been replaced with:\n " << new_op << "\nbecause they conflict with each other.\n"; remove_bindings(old_op); register_new_op(new_op, d, led); } - m_env.add_neutral_object(new notation_declaration(new_op, d)); + env.add_neutral_object(new notation_declaration(new_op, d)); } - void add_infix(name const & opn, unsigned p, expr const & d) { add_op(infix(opn, p), d, true); } - void add_infixl(name const & opn, unsigned p, expr const & d) { add_op(infixl(opn, p), d, true); } - void add_infixr(name const & opn, unsigned p, expr const & d) { add_op(infixr(opn, p), d, true); } - void add_prefix(name const & opn, unsigned p, expr const & d) { add_op(prefix(opn, p), d, false); } - void add_postfix(name const & opn, unsigned p, expr const & d) { add_op(postfix(opn, p), d, true); } - void add_mixfixl(unsigned sz, name const * opns, unsigned p, expr const & d) { add_op(mixfixl(sz, opns, p), d, false); } - void add_mixfixr(unsigned sz, name const * opns, unsigned p, expr const & d) { add_op(mixfixr(sz, opns, p), d, true); } - void add_mixfixc(unsigned sz, name const * opns, unsigned p, expr const & d) { add_op(mixfixc(sz, opns, p), d, false); } - void add_mixfixo(unsigned sz, name const * opns, unsigned p, expr const & d) { add_op(mixfixo(sz, opns, p), d, true); } - expr mk_explicit_definition_body(expr type, name const & n, unsigned i, unsigned sz) { if (i == sz) { buffer args; @@ -237,16 +227,16 @@ struct frontend::imp { } } - void mark_implicit_arguments(name const & n, unsigned sz, bool const * implicit) { - if (has_children()) + void mark_implicit_arguments(name const & n, unsigned sz, bool const * implicit, environment & env) { + if (env.has_children()) throw exception(sstream() << "failed to mark implicit arguments, frontend object is read-only"); - object const & obj = m_env.get_object(n); + object const & obj = env.get_object(n); if (obj.kind() != object_kind::Definition && obj.kind() != object_kind::Postulate && obj.kind() != object_kind::Builtin) throw exception(sstream() << "failed to mark implicit arguments, the object '" << n << "' is not a definition or postulate"); if (has_implicit_arguments(n)) throw exception(sstream() << "the object '" << n << "' already has implicit argument information associated with it"); name explicit_version(n, "explicit"); - if (m_env.find_object(explicit_version)) + if (env.find_object(explicit_version)) throw exception(sstream() << "failed to mark implicit arguments for '" << n << "', the frontend already has an object named '" << explicit_version << "'"); expr const & type = obj.get_type(); unsigned num_args = 0; @@ -258,58 +248,58 @@ struct frontend::imp { m_implicit_table[n] = mk_pair(v, explicit_version); expr body = mk_explicit_definition_body(type, n, 0, sz); if (obj.is_axiom() || obj.is_theorem()) { - m_env.add_theorem(explicit_version, type, body); + env.add_theorem(explicit_version, type, body); } else { - m_env.add_definition(explicit_version, type, body); + env.add_definition(explicit_version, type, body); } } - bool has_implicit_arguments(name const & n) { - if (m_implicit_table.find(n) != m_implicit_table.end()) { + bool has_implicit_arguments(name const & n) const { + if (m_implicit_table.find(n) != m_implicit_table.end()) return true; - } else if (has_parent()) { - return m_parent->has_implicit_arguments(n); - } else { + lean_extension const * parent = get_parent(); + if (parent) + return parent->has_implicit_arguments(n); + else return false; - } } - std::vector const & get_implicit_arguments(name const & n) { + std::vector const & get_implicit_arguments(name const & n) const { auto it = m_implicit_table.find(n); - if (it != m_implicit_table.end()) { + if (it != m_implicit_table.end()) return it->second.first; - } else if (has_parent()) { - return m_parent->get_implicit_arguments(n); - } else { + lean_extension const * parent = get_parent(); + if (parent) + return parent->get_implicit_arguments(n); + else return g_empty_vector; - } } - std::vector const & get_implicit_arguments(expr const & n) { + std::vector const & get_implicit_arguments(expr const & n) const { if (is_constant(n)) return get_implicit_arguments(const_name(n)); else return g_empty_vector; } - name const & get_explicit_version(name const & n) { + name const & get_explicit_version(name const & n) const { auto it = m_implicit_table.find(n); - if (it != m_implicit_table.end()) { + if (it != m_implicit_table.end()) return it->second.second; - } else if (has_parent()) { - return m_parent->get_explicit_version(n); - } else { + lean_extension const * parent = get_parent(); + if (parent) + return parent->get_explicit_version(n); + else return name::anonymous(); - } } - bool is_explicit(name const & n) { + bool is_explicit(name const & n) const { return !n.is_atomic() && get_explicit_version(n.get_prefix()) == n; } - void add_coercion(expr const & f) { - expr type = m_env.infer_type(f); - expr norm_type = m_env.normalize(type); + void add_coercion(expr const & f, environment & env) { + expr type = env.infer_type(f); + expr norm_type = env.normalize(type); if (!is_arrow(norm_type)) throw exception("invalid coercion declaration, a coercion must have an arrow type (i.e., a non-dependent functional type)"); expr from = abst_domain(norm_type); @@ -322,16 +312,17 @@ struct frontend::imp { m_coercion_set.insert(f); list l = get_coercions(from); insert(m_type_coercions, from, cons(expr_pair(to, f), l)); - m_env.add_neutral_object(new coercion_declaration(f)); + env.add_neutral_object(new coercion_declaration(f)); } - expr get_coercion(expr const & from_type, expr const & to_type) { + expr get_coercion(expr const & from_type, expr const & to_type) const { expr_pair p(from_type, to_type); auto it = m_coercion_map.find(p); if (it != m_coercion_map.end()) return it->second; - else if (has_parent()) - return m_parent->get_coercion(from_type, to_type); + lean_extension const * parent = get_parent(); + if (parent) + return parent->get_coercion(from_type, to_type); else return expr(); } @@ -340,91 +331,81 @@ struct frontend::imp { auto r = m_type_coercions.find(from_type); if (r != m_type_coercions.end()) return r->second; - else if (has_parent()) - return m_parent->get_coercions(from_type); + lean_extension const * parent = get_parent(); + if (parent) + return parent->get_coercions(from_type); else return list(); } - bool is_coercion(expr const & f) { + bool is_coercion(expr const & f) const { return m_coercion_set.find(f) != m_coercion_set.end(); } - - void set_interrupt(bool flag) { - m_env.set_interrupt(flag); - m_state.set_interrupt(flag); - } - - imp(frontend &): - m_num_children(0) { - } - - explicit imp(std::shared_ptr const & parent): - m_num_children(0), - m_parent(parent), - m_env(m_parent->m_env.mk_child()), - m_state(m_parent->m_state) { - m_parent->inc_children(); - } - - ~imp() { - if (m_parent) - m_parent->dec_children(); - } }; -frontend::frontend():m_ptr(new imp(*this)) { - import_all(m_ptr->m_env); +struct lean_extension_initializer { + unsigned m_extid; + lean_extension_initializer() { + m_extid = environment::register_extension([](){ return std::unique_ptr(new lean_extension()); }); + } +}; + +static lean_extension_initializer g_lean_extension_initializer; + +static lean_extension & to_ext(environment const & env) { + return env.get_extension(g_lean_extension_initializer.m_extid); +} + +frontend::frontend() { + import_all(m_env); init_builtin_notation(*this); - m_ptr->m_state.set_formatter(mk_pp_formatter(*this)); + m_state.set_formatter(mk_pp_formatter(*this)); } -frontend::frontend(imp * new_ptr):m_ptr(new_ptr) { - m_ptr->m_state.set_formatter(mk_pp_formatter(*this)); +frontend::frontend(environment const & env, state const & s):m_env(env), m_state(s) { } -frontend::frontend(std::shared_ptr const & ptr):m_ptr(ptr) {} -frontend::~frontend() {} -frontend frontend::mk_child() const { return frontend(new imp(m_ptr)); } -bool frontend::has_children() const { return m_ptr->has_children(); } -bool frontend::has_parent() const { return m_ptr->has_parent(); } -frontend frontend::parent() const { lean_assert(has_parent()); return frontend(m_ptr->m_parent); } - -environment const & frontend::get_environment() const { return m_ptr->m_env; } - -level frontend::add_uvar(name const & n, level const & l) { return m_ptr->m_env.add_uvar(n, l); } -level frontend::add_uvar(name const & n) { return m_ptr->m_env.add_uvar(n); } -level frontend::get_uvar(name const & n) const { return m_ptr->m_env.get_uvar(n); } - -void frontend::add_definition(name const & n, expr const & t, expr const & v, bool opaque) { - return m_ptr->m_env.add_definition(n, t, v, opaque); +void frontend::add_infix(name const & opn, unsigned p, expr const & d) { + to_ext(m_env).add_op(infix(opn, p), d, true, m_env, m_state); +} +void frontend::add_infixl(name const & opn, unsigned p, expr const & d) { + to_ext(m_env).add_op(infixl(opn, p), d, true, m_env, m_state); +} +void frontend::add_infixr(name const & opn, unsigned p, expr const & d) { + to_ext(m_env).add_op(infixr(opn, p), d, true, m_env, m_state); +} +void frontend::add_prefix(name const & opn, unsigned p, expr const & d) { + to_ext(m_env).add_op(prefix(opn, p), d, false, m_env, m_state); +} +void frontend::add_postfix(name const & opn, unsigned p, expr const & d) { + to_ext(m_env).add_op(postfix(opn, p), d, true, m_env, m_state); +} +void frontend::add_mixfixl(unsigned sz, name const * opns, unsigned p, expr const & d) { + to_ext(m_env).add_op(mixfixl(sz, opns, p), d, false, m_env, m_state); +} +void frontend::add_mixfixr(unsigned sz, name const * opns, unsigned p, expr const & d) { + to_ext(m_env).add_op(mixfixr(sz, opns, p), d, true, m_env, m_state); +} +void frontend::add_mixfixc(unsigned sz, name const * opns, unsigned p, expr const & d) { + to_ext(m_env).add_op(mixfixc(sz, opns, p), d, false, m_env, m_state); +} +void frontend::add_mixfixo(unsigned sz, name const * opns, unsigned p, expr const & d) { + to_ext(m_env).add_op(mixfixo(sz, opns, p), d, true, m_env, m_state); +} +operator_info frontend::find_op_for(expr const & n, bool unicode) const { + return to_ext(m_env).find_op_for(n, unicode); +} +operator_info frontend::find_nud(name const & n) const { + return to_ext(m_env).find_nud(n); +} +operator_info frontend::find_led(name const & n) const { + return to_ext(m_env).find_led(n); +} +void frontend::mark_implicit_arguments(name const & n, unsigned sz, bool const * implicit) { + to_ext(m_env).mark_implicit_arguments(n, sz, implicit, m_env); +} +void frontend::mark_implicit_arguments(name const & n, std::initializer_list const & l) { + mark_implicit_arguments(n, l.size(), l.begin()); } -void frontend::add_theorem(name const & n, expr const & t, expr const & v) { return m_ptr->m_env.add_theorem(n, t, v); } -void frontend::add_definition(name const & n, expr const & v, bool opaque) { return m_ptr->m_env.add_definition(n, v, opaque); } -void frontend::add_axiom(name const & n, expr const & t) { return m_ptr->m_env.add_axiom(n, t); } -void frontend::add_var(name const & n, expr const & t) { return m_ptr->m_env.add_var(n, t); } -object const & frontend::get_object(name const & n) const { return m_ptr->m_env.get_object(n); } -object const & frontend::find_object(name const & n) const { return m_ptr->m_env.find_object(n); } -bool frontend::has_object(name const & n) const { return m_ptr->m_env.has_object(n); } -frontend::object_iterator frontend::begin_objects() const { return m_ptr->m_env.begin_objects(); } -frontend::object_iterator frontend::end_objects() const { return m_ptr->m_env.end_objects(); } -frontend::object_iterator frontend::begin_local_objects() const { return m_ptr->m_env.begin_local_objects(); } -frontend::object_iterator frontend::end_local_objects() const { return m_ptr->m_env.end_local_objects(); } - -void frontend::add_infix(name const & opn, unsigned p, expr const & d) { m_ptr->add_infix(opn, p, d); } -void frontend::add_infixl(name const & opn, unsigned p, expr const & d) { m_ptr->add_infixl(opn, p, d); } -void frontend::add_infixr(name const & opn, unsigned p, expr const & d) { m_ptr->add_infixr(opn, p, d); } -void frontend::add_prefix(name const & opn, unsigned p, expr const & d) { m_ptr->add_prefix(opn, p, d); } -void frontend::add_postfix(name const & opn, unsigned p, expr const & d) { m_ptr->add_postfix(opn, p, d); } -void frontend::add_mixfixl(unsigned sz, name const * opns, unsigned p, expr const & d) { m_ptr->add_mixfixl(sz, opns, p, d); } -void frontend::add_mixfixr(unsigned sz, name const * opns, unsigned p, expr const & d) { m_ptr->add_mixfixr(sz, opns, p, d); } -void frontend::add_mixfixc(unsigned sz, name const * opns, unsigned p, expr const & d) { m_ptr->add_mixfixc(sz, opns, p, d); } -void frontend::add_mixfixo(unsigned sz, name const * opns, unsigned p, expr const & d) { m_ptr->add_mixfixo(sz, opns, p, d); } -operator_info frontend::find_op_for(expr const & n, bool unicode) const { return m_ptr->find_op_for(n, unicode); } -operator_info frontend::find_nud(name const & n) const { return m_ptr->find_nud(n); } -operator_info frontend::find_led(name const & n) const { return m_ptr->find_led(n); } - -void frontend::mark_implicit_arguments(name const & n, unsigned sz, bool const * implicit) { m_ptr->mark_implicit_arguments(n, sz, implicit); } -void frontend::mark_implicit_arguments(name const & n, std::initializer_list const & l) { mark_implicit_arguments(n, l.size(), l.begin()); } void frontend::mark_implicit_arguments(expr const & n, std::initializer_list const & l) { if (is_constant(n)) { mark_implicit_arguments(const_name(n), l); @@ -433,21 +414,28 @@ void frontend::mark_implicit_arguments(expr const & n, std::initializer_listhas_implicit_arguments(n); } -std::vector const & frontend::get_implicit_arguments(name const & n) const { return m_ptr->get_implicit_arguments(n); } -name const & frontend::get_explicit_version(name const & n) const { return m_ptr->get_explicit_version(n); } -bool frontend::is_explicit(name const & n) const { return m_ptr->is_explicit(n); } - -void frontend::add_coercion(expr const & f) { m_ptr->add_coercion(f); } -expr frontend::get_coercion(expr const & from_type, expr const & to_type) const { return m_ptr->get_coercion(from_type, to_type); } -list frontend::get_coercions(expr const & from_type) const { return m_ptr->get_coercions(from_type); } -bool frontend::is_coercion(expr const & f) const { return m_ptr->is_coercion(f); } - -state const & frontend::get_state() const { return m_ptr->m_state; } -state & frontend::get_state_core() { return m_ptr->m_state; } -void frontend::set_options(options const & opts) { return m_ptr->m_state.set_options(opts); } -void frontend::set_regular_channel(std::shared_ptr const & out) { return m_ptr->m_state.set_regular_channel(out); } -void frontend::set_diagnostic_channel(std::shared_ptr const & out) { return m_ptr->m_state.set_diagnostic_channel(out); } - -void frontend::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); } +bool frontend::has_implicit_arguments(name const & n) const { + return to_ext(m_env).has_implicit_arguments(n); +} +std::vector const & frontend::get_implicit_arguments(name const & n) const { + return to_ext(m_env).get_implicit_arguments(n); +} +name const & frontend::get_explicit_version(name const & n) const { + return to_ext(m_env).get_explicit_version(n); +} +bool frontend::is_explicit(name const & n) const { + return to_ext(m_env).is_explicit(n); +} +void frontend::add_coercion(expr const & f) { + to_ext(m_env).add_coercion(f, m_env); +} +expr frontend::get_coercion(expr const & from_type, expr const & to_type) const { + return to_ext(m_env).get_coercion(from_type, to_type); +} +list frontend::get_coercions(expr const & from_type) const { + return to_ext(m_env).get_coercions(from_type); +} +bool frontend::is_coercion(expr const & f) const { + return to_ext(m_env).is_coercion(f); +} } diff --git a/src/frontends/lean/frontend.h b/src/frontends/lean/frontend.h index 68a5b0e42..a0a053d45 100644 --- a/src/frontends/lean/frontend.h +++ b/src/frontends/lean/frontend.h @@ -14,64 +14,46 @@ Author: Leonardo de Moura namespace lean { /** - \brief Object for managing the environment, parser, pretty printer, - elaborator, etc. + \brief Wrapper for environment/state that provides additional objects + that are specific to the Lean frontend. + + This wrapper provides APIs for accessing/using the Lean frontend + extension data in the environment. */ class frontend { - struct imp; - std::shared_ptr m_ptr; - explicit frontend(imp * new_ptr); - explicit frontend(std::shared_ptr const & ptr); - state & get_state_core(); + environment m_env; + state m_state; public: frontend(); - ~frontend(); + frontend(environment const & env, state const & s); - /** - @name Parent/Child frontend management. - */ - /*@{*/ - /** - \brief Create a child environment. This frontend object will - only allow "read-only" operations until all children frontend - objects are deleted. - */ - frontend mk_child() const; + frontend mk_child() const { return frontend(m_env.mk_child(), m_state); } + bool has_children() const { return m_env.has_children(); } + bool has_parent() const { return m_env.has_parent(); } - /** \brief Return true iff this fronted has children frontend. */ - bool has_children() const; - - /** \brief Return true iff this frontend has a parent frontend. */ - bool has_parent() const; - - /** \brief Return parent frontend */ - frontend parent() const; - /*@}*/ + environment const & get_environment() const { return m_env; } + operator environment const &() const { return get_environment(); } /** @name Environment API */ /*@{*/ - /** \brief Coercion frontend -> environment. */ - environment const & get_environment() const; - operator environment const &() const { return get_environment(); } - - level add_uvar(name const & n, level const & l); - level add_uvar(name const & n); - level get_uvar(name const & n) const; - void add_definition(name const & n, expr const & t, expr const & v, bool opaque = false); - void add_theorem(name const & n, expr const & t, expr const & v); - void add_definition(name const & n, expr const & v, bool opaque = false); - void add_axiom(name const & n, expr const & t); - void add_var(name const & n, expr const & t); - object const & get_object(name const & n) const; - object const & find_object(name const & n) const; - bool has_object(name const & n) const; + level add_uvar(name const & n, level const & l) { return m_env.add_uvar(n, l); } + level add_uvar(name const & n) { return m_env.add_uvar(n); } + level get_uvar(name const & n) const { return m_env.get_uvar(n); } + void add_definition(name const & n, expr const & t, expr const & v, bool opaque = false) { m_env.add_definition(n, t, v, opaque); } + void add_theorem(name const & n, expr const & t, expr const & v) { m_env.add_theorem(n, t, v); } + void add_definition(name const & n, expr const & v, bool opaque = false) { m_env.add_definition(n, v, opaque); } + void add_axiom(name const & n, expr const & t) { m_env.add_axiom(n, t); } + void add_var(name const & n, expr const & t) { m_env.add_var(n, t); } + object const & get_object(name const & n) const { return m_env.get_object(n); } + object const & find_object(name const & n) const { return m_env.find_object(n); } + bool has_object(name const & n) const { return m_env.has_object(n); } typedef environment::object_iterator object_iterator; - object_iterator begin_objects() const; - object_iterator end_objects() const; - object_iterator begin_local_objects() const; - object_iterator end_local_objects() const; + object_iterator begin_objects() const { return m_env.begin_objects(); } + object_iterator end_objects() const { return m_env.end_objects(); } + object_iterator begin_local_objects() const { return m_env.begin_local_objects(); } + object_iterator end_local_objects() const { return m_env.end_local_objects(); } /*@}*/ /** @@ -195,18 +177,19 @@ public: @name State management. */ /*@{*/ - state const & get_state() const; - operator state const &() const { return get_state(); } - void set_options(options const & opts); - template void set_option(name const & n, T const & v) { get_state_core().set_option(n, v); } - void set_regular_channel(std::shared_ptr const & out); - void set_diagnostic_channel(std::shared_ptr const & out); + state const & get_state() const { return m_state; } + operator state const &() const { return m_state; } + options get_options() const { return m_state.get_options(); } + void set_options(options const & opts) { return m_state.set_options(opts); } + template void set_option(name const & n, T const & v) { m_state.set_option(n, v); } + void set_regular_channel(std::shared_ptr const & out) { m_state.set_regular_channel(out); } + void set_diagnostic_channel(std::shared_ptr const & out) { m_state.set_diagnostic_channel(out); } /*@}*/ /** @name Interrupts. */ - void set_interrupt(bool flag); + void set_interrupt(bool flag) { m_env.set_interrupt(flag); m_state.set_interrupt(flag); } void interrupt() { set_interrupt(true); } void reset_interrupt() { set_interrupt(false); } /*@}*/ diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 16fa6cf0c..6fa3a7f16 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -116,7 +116,7 @@ class parser::imp { typedef std::pair pos_info; typedef expr_map expr_pos_info; typedef buffer> bindings_buffer; - frontend m_frontend; + frontend & m_frontend; scanner m_scanner; frontend_elaborator m_elaborator; scanner::token m_curr; @@ -1563,7 +1563,7 @@ class parser::imp { } public: - imp(frontend const & fe, std::istream & in, bool use_exceptions, bool interactive): + imp(frontend & fe, std::istream & in, bool use_exceptions, bool interactive): m_frontend(fe), m_scanner(in), m_elaborator(fe), @@ -1576,7 +1576,7 @@ public: scan(); } - static void show_prompt(bool interactive, frontend const & fe) { + static void show_prompt(bool interactive, frontend & fe) { if (interactive) { regular(fe) << "# "; regular(fe).flush(); @@ -1655,7 +1655,7 @@ public: } }; -parser::parser(frontend const & fe, std::istream & in, bool use_exceptions, bool interactive) { +parser::parser(frontend & fe, std::istream & in, bool use_exceptions, bool interactive) { parser::imp::show_prompt(interactive, fe); m_ptr.reset(new imp(fe, in, use_exceptions, interactive)); } @@ -1675,7 +1675,7 @@ expr parser::parse_expr() { return m_ptr->parse_expr_main(); } -shell::shell(frontend const & fe):m_frontend(fe) { +shell::shell(frontend & fe):m_frontend(fe) { } shell::~shell() { diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index a7ecb0f56..c85dcb53e 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -15,7 +15,7 @@ class parser { class imp; std::unique_ptr m_ptr; public: - parser(frontend const & fe, std::istream & in, bool use_exceptions = true, bool interactive = false); + parser(frontend & fe, std::istream & in, bool use_exceptions = true, bool interactive = false); ~parser(); /** \brief Parse a sequence of commands */ @@ -31,10 +31,10 @@ public: /** \brief Implements the Read Eval Print loop */ class shell { - frontend m_frontend; + frontend & m_frontend; interruptable_ptr m_parser; public: - shell(frontend const & fe); + shell(frontend & fe); ~shell(); bool operator()(); @@ -47,7 +47,7 @@ public: inline bool parse_commands(frontend & fe, std::istream & in, bool use_exceptions = true, bool interactive = false) { return parser(fe, in, use_exceptions, interactive)(); } -inline expr parse_expr(frontend const & fe, std::istream & in) { +inline expr parse_expr(frontend & fe, std::istream & in) { return parser(fe, in).parse_expr(); } } diff --git a/src/tests/frontends/lean/frontend.cpp b/src/tests/frontends/lean/frontend.cpp index fbedd4eb7..f8cd0562b 100644 --- a/src/tests/frontends/lean/frontend.cpp +++ b/src/tests/frontends/lean/frontend.cpp @@ -127,7 +127,6 @@ static void tst9() { { frontend c = f.mk_child(); lean_assert(f.has_children()); - lean_assert(c.parent().has_children()); } lean_assert(!f.has_children()); f.add_uvar("l", level()+1); diff --git a/src/tests/frontends/lean/parser.cpp b/src/tests/frontends/lean/parser.cpp index 53d4f4cce..c515bf0bb 100644 --- a/src/tests/frontends/lean/parser.cpp +++ b/src/tests/frontends/lean/parser.cpp @@ -49,7 +49,7 @@ static void tst1() { parse(fe, "Check Pi (A : Type), A -> A"); } -static void check(frontend const & fe, char const * str, expr const & expected) { +static void check(frontend & fe, char const * str, expr const & expected) { std::istringstream in(str); try { expr got = parse_expr(fe, in);