From c679c3a8d498c52ffaedf53b9da26c0411227054 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 8 Mar 2016 11:40:36 -0800 Subject: [PATCH] dev(kernel/abstract_type_context): extend abstract_type_context API --- src/frontends/lean/pp.cpp | 3 ++- src/kernel/CMakeLists.txt | 2 +- src/kernel/abstract_type_context.cpp | 28 ++++++++++++++++++++++++++++ src/kernel/abstract_type_context.h | 18 +++++++++++++++--- src/library/CMakeLists.txt | 2 +- src/library/old_type_context.h | 6 +++++- 6 files changed, 52 insertions(+), 7 deletions(-) create mode 100644 src/kernel/abstract_type_context.cpp diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index d5b1383b53..4a4af4c8be 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -631,11 +631,12 @@ bool pretty_fn::has_implicit_args(expr const & f) { } try { expr type = m_ctx.relaxed_whnf(m_ctx.infer(f)); + push_local_fn push_local(m_ctx); while (is_pi(type)) { binder_info bi = binding_info(type); if (bi.is_implicit() || bi.is_strict_implicit() || bi.is_inst_implicit()) return true; - expr local = m_ctx.mk_tmp_local(binding_name(type), binding_domain(type), binding_info(type)); + expr local = push_local(binding_name(type), binding_domain(type), binding_info(type)); type = m_ctx.relaxed_whnf(instantiate(binding_body(type), local)); } return false; diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index eb5d23c2b2..9f54719a38 100644 --- a/src/kernel/CMakeLists.txt +++ b/src/kernel/CMakeLists.txt @@ -4,4 +4,4 @@ formatter.cpp declaration.cpp environment.cpp justification.cpp pos_info_provider.cpp metavar.cpp converter.cpp constraint.cpp type_checker.cpp error_msgs.cpp kernel_exception.cpp normalizer_extension.cpp init_module.cpp extension_context.cpp expr_cache.cpp -default_converter.cpp equiv_manager.cpp) +default_converter.cpp equiv_manager.cpp abstract_type_context.cpp) diff --git a/src/kernel/abstract_type_context.cpp b/src/kernel/abstract_type_context.cpp new file mode 100644 index 0000000000..e7747709ba --- /dev/null +++ b/src/kernel/abstract_type_context.cpp @@ -0,0 +1,28 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "util/fresh_name.h" +#include "kernel/abstract_type_context.h" +#include "kernel/abstract.h" + +namespace lean { +expr abstract_type_context::push_local(name const & pp_name, expr const & type, binder_info const & bi) { + return mk_local(mk_fresh_name(), pp_name, type, bi); +} + +void abstract_type_context::pop_local() { + /* do nothing */ +} + +expr abstract_type_context::abstract_locals(expr const & e, unsigned num_locals, expr const * locals) { + return ::lean::abstract_locals(e, num_locals, locals); +} + +push_local_fn::~push_local_fn() { + for (unsigned i = 0; i < m_counter; i++) + m_ctx.pop_local(); +} +} diff --git a/src/kernel/abstract_type_context.h b/src/kernel/abstract_type_context.h index c025082574..9e1d54ea4e 100644 --- a/src/kernel/abstract_type_context.h +++ b/src/kernel/abstract_type_context.h @@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "util/fresh_name.h" #include "kernel/expr.h" namespace lean { @@ -30,8 +29,21 @@ public: virtual expr check(expr const & e) { return infer(e); } virtual optional is_stuck(expr const &) { return none_expr(); } virtual name get_local_pp_name(expr const & e) const { return local_pp_name(e); } - virtual expr mk_tmp_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info()) { - return mk_local(mk_fresh_name(), pp_name, type, bi); + + virtual expr push_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info()); + virtual void pop_local(); + virtual expr abstract_locals(expr const & e, unsigned num_locals, expr const * locals); +}; + +class push_local_fn { + abstract_type_context & m_ctx; + unsigned m_counter; +public: + push_local_fn(abstract_type_context & ctx):m_ctx(ctx), m_counter(0) {} + ~push_local_fn(); + expr operator()(name const & pp_name, expr const & type, binder_info const & bi = binder_info()) { + m_counter++; + return m_ctx.push_local(pp_name, type, bi); } }; } diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 8855dcf13b..07472a33c6 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -20,4 +20,4 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp abstract_expr_manager.cpp light_lt_manager.cpp trace.cpp attribute_manager.cpp error_handling.cpp unification_hint.cpp defeq_simp_lemmas.cpp defeq_simplifier.cpp proof_irrel_expr_manager.cpp local_context.cpp metavar_context.cpp - legacy_type_context.cpp) + legacy_type_context.cpp type_context.cpp) diff --git a/src/library/old_type_context.h b/src/library/old_type_context.h index aeb40bc863..b34700d5bd 100644 --- a/src/library/old_type_context.h +++ b/src/library/old_type_context.h @@ -330,7 +330,11 @@ public: /** \brief Create a temporary local constant using the given pretty print name. The pretty printing name has not semantic significance. */ - virtual expr mk_tmp_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info()) override; + expr mk_tmp_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info()); + + virtual expr push_local(name const & pp_name, expr const & type, binder_info const & bi) override { + return mk_tmp_local(pp_name, type, bi); + } /** \brief Create a temporary local constant based on the domain of the given binding (lambda/Pi) expression */ expr mk_tmp_local_from_binding(expr const & b) {