From 749d468440c0d7aa80861067cf1670d1a107866e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 5 Nov 2015 15:29:30 -0800
Subject: [PATCH] feat(library): add fun_info_manager

---
 src/library/CMakeLists.txt       |  2 +-
 src/library/fun_info_manager.cpp | 53 ++++++++++++++++++++++++++++++++
 src/library/fun_info_manager.h   | 47 ++++++++++++++++++++++++++++
 3 files changed, 101 insertions(+), 1 deletion(-)
 create mode 100644 src/library/fun_info_manager.cpp
 create mode 100644 src/library/fun_info_manager.h

diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index fb0e18d2c..398cae5f0 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -17,4 +17,4 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   composition_manager.cpp tc_multigraph.cpp noncomputable.cpp
   aux_recursors.cpp norm_num.cpp decl_stats.cpp meng_paulson.cpp
   norm_num.cpp class_instance_resolution.cpp type_context.cpp
-  tmp_type_context.cpp)
+  tmp_type_context.cpp fun_info_manager.cpp)
diff --git a/src/library/fun_info_manager.cpp b/src/library/fun_info_manager.cpp
new file mode 100644
index 000000000..ce720639d
--- /dev/null
+++ b/src/library/fun_info_manager.cpp
@@ -0,0 +1,53 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/for_each_fn.h"
+#include "kernel/instantiate.h"
+#include "library/fun_info_manager.h"
+
+namespace lean {
+fun_info_manager::fun_info_manager(type_context & ctx):
+    m_ctx(ctx) {
+}
+
+auto fun_info_manager::get(expr const & e) -> fun_info {
+    if (auto r = m_fun_info.find(e))
+        return *r;
+    expr type = m_ctx.infer(e);
+    buffer<arg_info> info;
+    buffer<expr> locals;
+    while (is_pi(type)) {
+        expr local      = m_ctx.mk_tmp_local_from_binding(type);
+        expr local_type = m_ctx.infer(local);
+        bool is_prop    = m_ctx.is_prop(local_type);
+        // TODO(Leo): check if the following line is a performance bottleneck.
+        bool is_sub     = is_prop;
+        if (!is_sub)
+            is_sub = static_cast<bool>(m_ctx.mk_subsingleton_instance(local_type));
+        buffer<unsigned> deps;
+        for_each(local_type, [&](expr const & e, unsigned) {
+                if (m_ctx.is_tmp_local(e)) {
+                    unsigned idx;
+                    for (idx = 0; idx < locals.size(); idx++)
+                        if (locals[idx] == e)
+                            break;
+                    if (idx < locals.size() && std::find(deps.begin(), deps.end(), idx) == deps.end())
+                        deps.push_back(idx);
+                }
+                return has_local(e); // continue the search only if e has locals
+            });
+        std::sort(deps.begin(), deps.end());
+        locals.push_back(local);
+        info.emplace_back(binding_info(type).is_implicit(),
+                          binding_info(type).is_inst_implicit(),
+                          is_prop, is_sub, to_list(deps));
+        type = m_ctx.whnf(instantiate(binding_body(type), local));
+    }
+    fun_info r(info.size(), to_list(info));
+    m_fun_info.insert(e, r);
+    return r;
+}
+}
diff --git a/src/library/fun_info_manager.h b/src/library/fun_info_manager.h
new file mode 100644
index 000000000..0243991b7
--- /dev/null
+++ b/src/library/fun_info_manager.h
@@ -0,0 +1,47 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "library/expr_lt.h"
+#include "library/type_context.h"
+
+namespace lean {
+class fun_info_manager {
+public:
+    class arg_info {
+        unsigned       m_implicit:1;
+        unsigned       m_inst_implicit:1;
+        unsigned       m_prop:1;
+        unsigned       m_subsingleton:1;
+        list<unsigned> m_deps; // previous arguments it depends on
+    public:
+        arg_info(bool imp, bool inst_imp, bool prop, bool sub, list<unsigned> const & deps):
+            m_implicit(imp), m_inst_implicit(inst_imp), m_prop(prop), m_subsingleton(sub), m_deps(deps) {}
+        list<unsigned> const & get_dependencies() const { return m_deps; }
+        bool is_prop() const { return m_prop; }
+        bool is_implicit() const { return m_implicit; }
+        bool is_inst_implicit() const { return m_inst_implicit; }
+        bool is_subsingleton() const { return m_subsingleton; }
+    };
+
+    class fun_info {
+        unsigned       m_arity;
+        list<arg_info> m_args_info;
+    public:
+        fun_info():m_arity(0) {}
+        fun_info(unsigned arity, list<arg_info> const & info):m_arity(arity), m_args_info(info) {}
+        unsigned get_arity() const { return m_arity; }
+        list<arg_info> const & get_args_info() const { return m_args_info; }
+    };
+private:
+    type_context &                         m_ctx;
+    rb_map<expr, fun_info, expr_quick_cmp> m_fun_info;
+
+public:
+    fun_info_manager(type_context & ctx);
+    fun_info get(expr const & e);
+};
+}