From ad901ce087f268648bc3d504bcf90de0e8edf1b0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 17 Sep 2013 14:42:44 -0700 Subject: [PATCH] Use consistent naming conventions Signed-off-by: Leonardo de Moura --- src/frontends/lean/frontend.cpp | 104 ++++++++++++++++---------------- src/frontends/lean/frontend.h | 2 +- src/kernel/environment.cpp | 52 ++++++++-------- src/kernel/environment.h | 2 +- src/library/max_sharing.cpp | 6 +- src/library/max_sharing.h | 2 +- 6 files changed, 84 insertions(+), 84 deletions(-) diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp index 2ad315061..ddcc9e2eb 100644 --- a/src/frontends/lean/frontend.cpp +++ b/src/frontends/lean/frontend.cpp @@ -365,74 +365,74 @@ struct frontend::imp { } }; -frontend::frontend():m_imp(new imp(*this)) { - import_all(m_imp->m_env); +frontend::frontend():m_ptr(new imp(*this)) { + import_all(m_ptr->m_env); init_builtin_notation(*this); - m_imp->m_state.set_formatter(mk_pp_formatter(*this)); + m_ptr->m_state.set_formatter(mk_pp_formatter(*this)); } -frontend::frontend(imp * new_ptr):m_imp(new_ptr) { - m_imp->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(std::shared_ptr const & ptr):m_imp(ptr) {} +frontend::frontend(std::shared_ptr const & ptr):m_ptr(ptr) {} frontend::~frontend() {} -frontend frontend::mk_child() const { return frontend(new imp(m_imp)); } -bool frontend::has_children() const { return m_imp->has_children(); } -bool frontend::has_parent() const { return m_imp->has_parent(); } -frontend frontend::parent() const { lean_assert(has_parent()); return frontend(m_imp->m_parent); } +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_imp->m_env; } +environment const & frontend::get_environment() const { return m_ptr->m_env; } -level frontend::add_uvar(name const & n, level const & l) { return m_imp->m_env.add_uvar(n, l); } -level frontend::add_uvar(name const & n) { return m_imp->m_env.add_uvar(n); } -level frontend::get_uvar(name const & n) const { return m_imp->m_env.get_uvar(n); } +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_imp->m_env.add_definition(n, t, v, opaque); + return m_ptr->m_env.add_definition(n, t, v, opaque); } -void frontend::add_theorem(name const & n, expr const & t, expr const & v) { return m_imp->m_env.add_theorem(n, t, v); } -void frontend::add_definition(name const & n, expr const & v, bool opaque) { return m_imp->m_env.add_definition(n, v, opaque); } -void frontend::add_axiom(name const & n, expr const & t) { return m_imp->m_env.add_axiom(n, t); } -void frontend::add_var(name const & n, expr const & t) { return m_imp->m_env.add_var(n, t); } -object const & frontend::get_object(name const & n) const { return m_imp->m_env.get_object(n); } -object const & frontend::find_object(name const & n) const { return m_imp->m_env.find_object(n); } -bool frontend::has_object(name const & n) const { return m_imp->m_env.has_object(n); } -frontend::object_iterator frontend::begin_objects() const { return m_imp->m_env.begin_objects(); } -frontend::object_iterator frontend::end_objects() const { return m_imp->m_env.end_objects(); } -frontend::object_iterator frontend::begin_local_objects() const { return m_imp->m_env.begin_local_objects(); } -frontend::object_iterator frontend::end_local_objects() const { return m_imp->m_env.end_local_objects(); } +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_imp->add_infix(opn, p, d); } -void frontend::add_infixl(name const & opn, unsigned p, expr const & d) { m_imp->add_infixl(opn, p, d); } -void frontend::add_infixr(name const & opn, unsigned p, expr const & d) { m_imp->add_infixr(opn, p, d); } -void frontend::add_prefix(name const & opn, unsigned p, expr const & d) { m_imp->add_prefix(opn, p, d); } -void frontend::add_postfix(name const & opn, unsigned p, expr const & d) { m_imp->add_postfix(opn, p, d); } -void frontend::add_mixfixl(unsigned sz, name const * opns, unsigned p, expr const & d) { m_imp->add_mixfixl(sz, opns, p, d); } -void frontend::add_mixfixr(unsigned sz, name const * opns, unsigned p, expr const & d) { m_imp->add_mixfixr(sz, opns, p, d); } -void frontend::add_mixfixc(unsigned sz, name const * opns, unsigned p, expr const & d) { m_imp->add_mixfixc(sz, opns, p, d); } -void frontend::add_mixfixo(unsigned sz, name const * opns, unsigned p, expr const & d) { m_imp->add_mixfixo(sz, opns, p, d); } -operator_info frontend::find_op_for(expr const & n, bool unicode) const { return m_imp->find_op_for(n, unicode); } -operator_info frontend::find_nud(name const & n) const { return m_imp->find_nud(n); } -operator_info frontend::find_led(name const & n) const { return m_imp->find_led(n); } +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_imp->mark_implicit_arguments(n, sz, implicit); } +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()); } -bool frontend::has_implicit_arguments(name const & n) const { return m_imp->has_implicit_arguments(n); } -std::vector const & frontend::get_implicit_arguments(name const & n) const { return m_imp->get_implicit_arguments(n); } -name const & frontend::get_explicit_version(name const & n) const { return m_imp->get_explicit_version(n); } -bool frontend::is_explicit(name const & n) const { return m_imp->is_explicit(n); } +bool frontend::has_implicit_arguments(name const & n) const { return m_ptr->has_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_imp->add_coercion(f); } +void frontend::add_coercion(expr const & f) { m_ptr->add_coercion(f); } expr frontend::get_coercion(expr const & given_type, expr const & expected_type, context const & ctx) const { - return m_imp->get_coercion(given_type, expected_type, ctx); + return m_ptr->get_coercion(given_type, expected_type, ctx); } -bool frontend::is_coercion(expr const & f) const { return m_imp->is_coercion(f); } +bool frontend::is_coercion(expr const & f) const { return m_ptr->is_coercion(f); } -state const & frontend::get_state() const { return m_imp->m_state; } -state & frontend::get_state_core() { return m_imp->m_state; } -void frontend::set_options(options const & opts) { return m_imp->m_state.set_options(opts); } -void frontend::set_regular_channel(std::shared_ptr const & out) { return m_imp->m_state.set_regular_channel(out); } -void frontend::set_diagnostic_channel(std::shared_ptr const & out) { return m_imp->m_state.set_diagnostic_channel(out); } +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_imp->set_interrupt(flag); } +void frontend::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); } } diff --git a/src/frontends/lean/frontend.h b/src/frontends/lean/frontend.h index a5144b4cf..0ed208d31 100644 --- a/src/frontends/lean/frontend.h +++ b/src/frontends/lean/frontend.h @@ -18,7 +18,7 @@ namespace lean { */ class frontend { struct imp; - std::shared_ptr m_imp; + std::shared_ptr m_ptr; explicit frontend(imp * new_ptr); explicit frontend(std::shared_ptr const & ptr); state & get_state_core(); diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 0ff5c168e..2383c7be9 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -355,112 +355,112 @@ struct environment::imp { }; environment::environment(): - m_imp(new imp(*this)) { + m_ptr(new imp(*this)) { } // used when creating a new child environment environment::environment(std::shared_ptr const & parent, bool): - m_imp(new imp(parent, *this)) { + m_ptr(new imp(parent, *this)) { } // used when creating a reference to the parent environment environment::environment(std::shared_ptr const & ptr): - m_imp(ptr) { + m_ptr(ptr) { } environment::~environment() { } environment environment::mk_child() const { - return environment(m_imp, true); + return environment(m_ptr, true); } bool environment::has_children() const { - return m_imp->has_children(); + return m_ptr->has_children(); } bool environment::has_parent() const { - return m_imp->has_parent(); + return m_ptr->has_parent(); } environment environment::parent() const { lean_assert(has_parent()); - return environment(m_imp->m_parent); + return environment(m_ptr->m_parent); } level environment::add_uvar(name const & n, level const & l) { - return m_imp->add_uvar(n, l, *this); + return m_ptr->add_uvar(n, l, *this); } bool environment::is_ge(level const & l1, level const & l2) const { - return m_imp->is_ge(l1, l2); + return m_ptr->is_ge(l1, l2); } level environment::get_uvar(name const & n) const { - return m_imp->get_uvar(n, *this); + return m_ptr->get_uvar(n, *this); } void environment::add_builtin(expr const & v) { - return m_imp->add_builtin(v, *this); + return m_ptr->add_builtin(v, *this); } void environment::add_builtin_set(expr const & r) { - return m_imp->add_builtin_set(r, *this); + return m_ptr->add_builtin_set(r, *this); } void environment::add_definition(name const & n, expr const & t, expr const & v, bool opaque) { - m_imp->add_definition(n, t, v, opaque, *this); + m_ptr->add_definition(n, t, v, opaque, *this); } void environment::add_theorem(name const & n, expr const & t, expr const & v) { - m_imp->add_theorem(n, t, v, *this); + m_ptr->add_theorem(n, t, v, *this); } void environment::add_definition(name const & n, expr const & v, bool opaque) { - m_imp->add_definition(n, v, opaque, *this); + m_ptr->add_definition(n, v, opaque, *this); } void environment::add_axiom(name const & n, expr const & t) { - m_imp->add_axiom(n, t, *this); + m_ptr->add_axiom(n, t, *this); } void environment::add_var(name const & n, expr const & t) { - m_imp->add_var(n, t, *this); + m_ptr->add_var(n, t, *this); } void environment::add_neutral_object(neutral_object_cell * o) { - m_imp->m_objects.push_back(mk_neutral(o)); + m_ptr->m_objects.push_back(mk_neutral(o)); } object const & environment::get_object(name const & n) const { - return m_imp->get_object(n, *this); + return m_ptr->get_object(n, *this); } object const & environment::find_object(name const & n) const { - return m_imp->get_object_core(n); + return m_ptr->get_object_core(n); } unsigned environment::get_num_objects(bool local) const { - return m_imp->get_num_objects(local); + return m_ptr->get_num_objects(local); } object const & environment::get_object(unsigned i, bool local) const { - return m_imp->get_object(i, local); + return m_ptr->get_object(i, local); } expr environment::infer_type(expr const & e, context const & ctx) { - return m_imp->infer_type(e, ctx); + return m_ptr->infer_type(e, ctx); } expr environment::normalize(expr const & e, context const & ctx) { - return m_imp->normalize(e, ctx); + return m_ptr->normalize(e, ctx); } void environment::display(std::ostream & out) const { - m_imp->display(out, *this); + m_ptr->display(out, *this); } void environment::set_interrupt(bool flag) { - m_imp->set_interrupt(flag); + m_ptr->set_interrupt(flag); } } diff --git a/src/kernel/environment.h b/src/kernel/environment.h index cdc86a943..0e3b11f51 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -19,7 +19,7 @@ namespace lean { class environment { private: struct imp; - std::shared_ptr m_imp; + std::shared_ptr m_ptr; void check_type(name const & n, expr const & t, expr const & v); environment(std::shared_ptr const & parent, bool); explicit environment(std::shared_ptr const & ptr); diff --git a/src/library/max_sharing.cpp b/src/library/max_sharing.cpp index 99999ffb3..be723d81a 100644 --- a/src/library/max_sharing.cpp +++ b/src/library/max_sharing.cpp @@ -78,10 +78,10 @@ struct max_sharing_fn::imp { expr operator()(expr const & a) { return apply(a); } }; -max_sharing_fn::max_sharing_fn():m_imp(new imp) {} +max_sharing_fn::max_sharing_fn():m_ptr(new imp) {} max_sharing_fn::~max_sharing_fn() {} -expr max_sharing_fn::operator()(expr const & a) { return (*m_imp)(a); } -void max_sharing_fn::clear() { m_imp->m_cache.clear(); } +expr max_sharing_fn::operator()(expr const & a) { return (*m_ptr)(a); } +void max_sharing_fn::clear() { m_ptr->m_cache.clear(); } expr max_sharing(expr const & a) { if (a.raw()->max_shared()) diff --git a/src/library/max_sharing.h b/src/library/max_sharing.h index 4c58d0022..79a78b1ac 100644 --- a/src/library/max_sharing.h +++ b/src/library/max_sharing.h @@ -16,7 +16,7 @@ namespace lean { class max_sharing_fn { struct imp; friend expr max_sharing(expr const & a); - std::unique_ptr m_imp; + std::unique_ptr m_ptr; public: max_sharing_fn(); ~max_sharing_fn();