From 7d588636a1c461b2d19bc0927e6958db85a5da8d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 7 Nov 2015 11:02:32 -0800
Subject: [PATCH] feat(library/fun_info_manager): collect additional
 information

---
 src/library/fun_info_manager.cpp | 39 ++++++++++++++++++--------------
 src/library/fun_info_manager.h   | 14 ++++++++----
 2 files changed, 32 insertions(+), 21 deletions(-)

diff --git a/src/library/fun_info_manager.cpp b/src/library/fun_info_manager.cpp
index 2df6853c2..d4b3f7103 100644
--- a/src/library/fun_info_manager.cpp
+++ b/src/library/fun_info_manager.cpp
@@ -16,6 +16,23 @@ fun_info_manager::fun_info_manager(type_context & ctx):
     m_ctx(ctx) {
 }
 
+list<unsigned> fun_info_manager::collect_deps(expr const & e, buffer<expr> const & locals) {
+    buffer<unsigned> deps;
+    for_each(e, [&](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());
+    return to_list(deps);
+}
+
 auto fun_info_manager::get(expr const & e) -> fun_info {
     if (auto r = m_fun_info.find(e))
         return *r;
@@ -28,28 +45,16 @@ auto fun_info_manager::get(expr const & e) -> fun_info {
         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;
+        bool is_dep     = !closed(binding_body(type));
+        expr new_type   = m_ctx.whnf(instantiate(binding_body(type), local));
         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));
+                          is_prop, is_sub, is_dep, collect_deps(local_type, locals));
+        type = new_type;
     }
-    fun_info r(info.size(), to_list(info));
+    fun_info r(info.size(), to_list(info), collect_deps(type, locals));
     m_fun_info.insert(e, r);
     return r;
 }
diff --git a/src/library/fun_info_manager.h b/src/library/fun_info_manager.h
index 1527c7665..54549c636 100644
--- a/src/library/fun_info_manager.h
+++ b/src/library/fun_info_manager.h
@@ -14,31 +14,37 @@ class param_info {
     unsigned       m_inst_implicit:1;
     unsigned       m_prop:1;
     unsigned       m_subsingleton:1;
+    unsigned       m_is_dep:1; // true if rest depends on this parameter
     list<unsigned> m_deps; // previous arguments it depends on
 public:
-    param_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) {}
+    param_info(bool imp, bool inst_imp, bool prop, bool sub, bool is_dep, list<unsigned> const & deps):
+        m_implicit(imp), m_inst_implicit(inst_imp), m_prop(prop), m_subsingleton(sub),
+        m_is_dep(is_dep), 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; }
+    bool is_dep() const { return m_is_dep; }
 };
 
 class fun_info {
     unsigned         m_arity;
     list<param_info> m_params_info;
+    list<unsigned>   m_deps;
 public:
     fun_info():m_arity(0) {}
-    fun_info(unsigned arity, list<param_info> const & info):m_arity(arity), m_params_info(info) {}
+    fun_info(unsigned arity, list<param_info> const & info, list<unsigned> const & deps):
+        m_arity(arity), m_params_info(info), m_deps(deps) {}
     unsigned get_arity() const { return m_arity; }
     list<param_info> const & get_params_info() const { return m_params_info; }
+    list<unsigned> const & get_dependencies() const { return m_deps; }
 };
 
 class fun_info_manager {
     type_context &                         m_ctx;
     rb_map<expr, fun_info, expr_quick_cmp> m_fun_info;
-
+    list<unsigned> collect_deps(expr const & e, buffer<expr> const & locals);
 public:
     fun_info_manager(type_context & ctx);
     type_context & ctx() { return m_ctx; }