From aa697206e875e009749bf876ade50a5b797f41b1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 4 Nov 2015 11:29:34 -0800 Subject: [PATCH] refactor(library/type_context): rename set_context to set_local_instances --- src/library/app_builder.cpp | 4 ++-- src/library/app_builder.h | 4 ++-- src/library/blast/blast.cpp | 2 +- src/library/type_context.cpp | 8 ++++---- src/library/type_context.h | 8 ++++---- 5 files changed, 13 insertions(+), 13 deletions(-) diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp index dc426575d..cd9618d03 100644 --- a/src/library/app_builder.cpp +++ b/src/library/app_builder.cpp @@ -515,7 +515,7 @@ optional app_builder::mk_eq_drec(expr const & C, expr const & H1, expr con return m_ptr->mk_eq_drec(C, H1, H2); } -void app_builder::set_context(list const & ctx) { - m_ptr->m_ctx->set_context(ctx); +void app_builder::set_local_instances(list const & insts) { + m_ptr->m_ctx->set_local_instances(insts); } } diff --git a/src/library/app_builder.h b/src/library/app_builder.h index 9898a5bf9..76384fb64 100644 --- a/src/library/app_builder.h +++ b/src/library/app_builder.h @@ -105,11 +105,11 @@ public: because eq.rec is a dependent eliminator in HoTT. */ optional mk_eq_drec(expr const & C, expr const & H1, expr const & H2); - /** \brief Set the local context. This method is relevant when we want to expose local class instances + /** \brief Set the local instances. This method is relevant when we want to expose local class instances to the app_builder. \remark When the constructor app_builder(std::unique_ptr && ctx) is used the initialization can be performed outside. */ - void set_context(list const & ctx); + void set_local_instances(list const & insts); }; } diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index 6fc1e1645..f181689fd 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -392,7 +392,7 @@ public: void init_state(goal const & g) { m_curr_state = to_state(g); - // TODO(Leo): set local context for type class resolution at tctx + // TODO(Leo): set local instances for type class resolution at tctx } optional operator()(goal const & g) { diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 8431848c7..fd37bf929 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -98,10 +98,10 @@ type_context::type_context(environment const & env, io_state const & ios, bool m type_context::~type_context() { } -void type_context::set_context(list const & ctx) { +void type_context::set_local_instances(list const & insts) { clear_cache(); m_ci_local_instances.clear(); - for (expr const & e : ctx) { + for (expr const & e : insts) { if (auto cname = is_class(infer(e))) { m_ci_local_instances.push_back(mk_pair(*cname, e)); } @@ -1660,14 +1660,14 @@ type_context::scope_pos_info::~scope_pos_info() { } default_type_context::default_type_context(environment const & env, io_state const & ios, - list const & ctx, bool multiple_instances): + list const & insts, bool multiple_instances): type_context(env, ios, multiple_instances), m_not_reducible_pred(mk_not_reducible_pred(env)) { m_ignore_if_zero = false; m_next_local_idx = 0; m_next_uvar_idx = 0; m_next_mvar_idx = 0; - set_context(ctx); + set_local_instances(insts); } default_type_context::~default_type_context() {} diff --git a/src/library/type_context.h b/src/library/type_context.h index f488a584e..c50a3a29f 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -210,7 +210,7 @@ public: type_context(environment const & env, io_state const & ios, bool multiple_instances = false); virtual ~type_context(); - void set_context(list const & ctx); + void set_local_instances(list const & insts); environment const & env() const { return m_env; } @@ -361,10 +361,10 @@ public: \remark We assume pretty-printing options are irrelevant. */ bool update_options(options const & opts); - /** \brief Return true if the local instances at \c ctx are compatible with the ones + /** \brief Return true if the local instances at \c insts are compatible with the ones in the type inference object. This method is used to decide whether a type inference object can be reused by the elaborator. */ - bool compatible_local_instances(list const & ctx); + bool compatible_local_instances(list const & insts); /** \brief Auxiliary object used to set position information for the type class resolution trace. */ class scope_pos_info { @@ -420,7 +420,7 @@ class default_type_context : public type_context { public: default_type_context(environment const & env, io_state const & ios, - list const & ctx = list(), bool multiple_instances = false); + list const & insts = list(), bool multiple_instances = false); virtual ~default_type_context(); virtual bool is_extra_opaque(name const & n) const { return m_not_reducible_pred(n); } virtual bool ignore_universe_def_eq(level const & l1, level const & l2) const;