dev(kernel/abstract_type_context): extend abstract_type_context API

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;

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)

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();
+}
+}

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<expr> 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);
     }
 };
 }

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)

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) {