From cf5e7e4185ff47b7bd5abbfd724d5e6c54932e69 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 24 May 2016 14:38:21 -0700 Subject: [PATCH] chore(library/type_context): improve aux_type_context interface --- src/library/type_context.h | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/src/library/type_context.h b/src/library/type_context.h index 8c3927775b..6ab74ab9bc 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -407,6 +407,25 @@ public: friend class tmp_locals; }; +/** Auxiliary object for automating the creation of temporary type_context objects */ +class aux_type_context { + metavar_context m_mctx; + type_context m_ctx; +public: + aux_type_context(environment const & env, options const & opts, local_context const & lctx, + transparency_mode m = transparency_mode::Reducible): + m_ctx(env, opts, m_mctx, lctx, m) {} + aux_type_context(environment const & env, options const & opts, + transparency_mode m = transparency_mode::Reducible): + m_ctx(env, opts, m_mctx, local_context(), m) {} + aux_type_context(environment const & env, transparency_mode m = transparency_mode::Reducible): + m_ctx(env, options(), m_mctx, local_context(), m) {} + + operator type_context&() { return m_ctx; } + operator type_context() { return m_ctx; } + type_context * operator->() { return &m_ctx; } +}; + void initialize_type_context(); void finalize_type_context(); }