From 7f088b763535cc1cb4f7d6fd965d122c8ca9f4ed Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 19 Nov 2013 11:21:45 -0800
Subject: [PATCH] feat(kernel): add (optional) field m_type to expr_const, this
 field is useful for implementing the tactic framework

This field should not be visible in the external API.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/CMakeLists.txt      |  2 +-
 src/kernel/environment.cpp     | 13 +++++++++++++
 src/kernel/expr.cpp            | 15 ++++++++++-----
 src/kernel/expr.h              | 22 +++++++++++++++++++---
 src/kernel/expr_eq.h           |  2 +-
 src/kernel/for_each.h          | 15 +++++++++++++--
 src/kernel/free_vars.cpp       | 24 ++++++++++++++++++++----
 src/kernel/has_cached_type.cpp | 27 +++++++++++++++++++++++++++
 src/kernel/has_cached_type.h   | 22 ++++++++++++++++++++++
 src/kernel/replace.h           |  6 +++++-
 src/kernel/replace_visitor.cpp |  9 ++++++++-
 src/kernel/type_checker.cpp    | 14 +++++++++-----
 src/library/max_sharing.cpp    | 11 ++++++++++-
 src/library/type_inferer.cpp   | 14 +++++++++-----
 14 files changed, 167 insertions(+), 29 deletions(-)
 create mode 100644 src/kernel/has_cached_type.cpp
 create mode 100644 src/kernel/has_cached_type.h

diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt
index f5a0853b3..3aa0ae7d4 100644
--- a/src/kernel/CMakeLists.txt
+++ b/src/kernel/CMakeLists.txt
@@ -1,7 +1,7 @@
 add_library(kernel expr.cpp free_vars.cpp abstract.cpp instantiate.cpp
   normalizer.cpp context.cpp level.cpp object.cpp environment.cpp
   type_checker.cpp builtin.cpp occurs.cpp metavar.cpp justification.cpp
-  unification_constraint.cpp printer.cpp formatter.cpp
+  unification_constraint.cpp printer.cpp formatter.cpp has_cached_type.cpp
   kernel_exception.cpp type_checker_justification.cpp pos_info_provider.cpp
   replace_visitor.cpp)
 
diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index ea700bfdd..ab13f665c 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -20,6 +20,7 @@ Author: Leonardo de Moura
 #include "kernel/threadsafe_environment.h"
 #include "kernel/type_checker.h"
 #include "kernel/normalizer.h"
+#include "kernel/has_cached_type.h"
 
 namespace lean {
 static name g_builtin_module("builtin_module");
@@ -287,6 +288,11 @@ struct environment::imp {
         m_uvars.emplace_back();
     }
 
+    void check_no_cached_type(expr const & e, environment const & env) {
+        if (has_cached_type(e))
+            throw kernel_exception(env, "expression has a constant with a cached type, this is a bug in one of Lean tactics and/or solvers");
+    }
+
     /**
         \brief Throw an exception if \c t is not a type or type of \c
         v is not convertible to \c t.
@@ -331,6 +337,8 @@ struct environment::imp {
 
     /** \brief Add new definition. */
     void add_definition(name const & n, expr const & t, expr const & v, bool opaque, environment const & env) {
+        check_no_cached_type(t, env);
+        check_no_cached_type(v, env);
         check_new_definition(n, t, v, env);
         unsigned w = get_max_weight(v) + 1;
         register_named_object(mk_definition(n, t, v, opaque, w));
@@ -341,6 +349,7 @@ struct environment::imp {
         The type of the new definition is the type of \c v.
     */
     void add_definition(name const & n, expr const & v, bool opaque, environment const & env) {
+        check_no_cached_type(v, env);
         check_name(n, env);
         expr v_t = m_type_checker->infer_type(v);
         unsigned w = get_max_weight(v) + 1;
@@ -349,12 +358,15 @@ struct environment::imp {
 
     /** \brief Add new theorem. */
     void add_theorem(name const & n, expr const & t, expr const & v, environment const & env) {
+        check_no_cached_type(t, env);
+        check_no_cached_type(v, env);
         check_new_definition(n, t, v, env);
         register_named_object(mk_theorem(n, t, v));
     }
 
     /** \brief Add new axiom. */
     void add_axiom(name const & n, expr const & t, environment const & env) {
+        check_no_cached_type(t, env);
         check_name(n, env);
         m_type_checker->check_type(t);
         register_named_object(mk_axiom(n, t));
@@ -362,6 +374,7 @@ struct environment::imp {
 
     /** \brief Add new variable. */
     void add_var(name const & n, expr const & t, environment const & env) {
+        check_no_cached_type(t, env);
         check_name(n, env);
         m_type_checker->check_type(t);
         register_named_object(mk_var_decl(n, t));
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index cb1ab138d..992c0ac3f 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -67,9 +67,14 @@ expr_var::expr_var(unsigned idx):
     expr_cell(expr_kind::Var, idx, false),
     m_vidx(idx) {}
 
-expr_const::expr_const(name const & n):
-    expr_cell(expr_kind::Constant, n.hash(), false),
-    m_name(n) {}
+expr_const::expr_const(name const & n, expr const & t):
+    expr_cell(expr_kind::Constant, n.hash(), t && t.has_metavar()),
+    m_name(n),
+    m_type(t) {}
+void expr_const::dealloc(buffer<expr_cell*> & todelete) {
+    dec_ref(m_type, todelete);
+    delete(this);
+}
 
 expr_app::expr_app(unsigned num_args, bool has_mv):
     expr_cell(expr_kind::App, 0, has_mv),
@@ -196,10 +201,10 @@ void expr_cell::dealloc() {
             lean_assert(it->get_rc() == 0);
             switch (it->kind()) {
             case expr_kind::Var:        delete static_cast<expr_var*>(it); break;
-            case expr_kind::Constant:   delete static_cast<expr_const*>(it); break;
             case expr_kind::Value:      delete static_cast<expr_value*>(it); break;
             case expr_kind::MetaVar:    delete static_cast<expr_metavar*>(it); break;
             case expr_kind::Type:       delete static_cast<expr_type*>(it); break;
+            case expr_kind::Constant:   static_cast<expr_const*>(it)->dealloc(todo); break;
             case expr_kind::Eq:         static_cast<expr_eq*>(it)->dealloc(todo); break;
             case expr_kind::App:        static_cast<expr_app*>(it)->dealloc(todo); break;
             case expr_kind::Lambda:     static_cast<expr_lambda*>(it)->dealloc(todo); break;
@@ -229,7 +234,7 @@ bool is_arrow(expr const & t) {
 expr copy(expr const & a) {
     switch (a.kind()) {
     case expr_kind::Var:      return mk_var(var_idx(a));
-    case expr_kind::Constant: return mk_constant(const_name(a));
+    case expr_kind::Constant: return mk_constant(const_name(a), const_type(a));
     case expr_kind::Type:     return mk_type(ty_level(a));
     case expr_kind::Value:    return mk_value(static_cast<expr_value*>(a.raw())->m_val);
     case expr_kind::App:      return mk_app(num_args(a), begin_args(a));
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 084835a8f..d64a21b40 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -125,7 +125,7 @@ public:
     operator bool() const { return m_ptr != nullptr; }
 
     friend expr mk_var(unsigned idx);
-    friend expr mk_constant(name const & n);
+    friend expr mk_constant(name const & n, expr const & t);
     friend expr mk_value(value & v);
     friend expr mk_app(unsigned num_args, expr const * args);
     friend expr mk_eq(expr const & l, expr const & r);
@@ -160,9 +160,15 @@ public:
 /** \brief Constants. */
 class expr_const : public expr_cell {
     name     m_name;
+    expr     m_type; // (optional) cached type
+    // Remark: we do *not* perform destructive updates on m_type
+    // This field is used to efficiently implement the tactic framework
+    friend class expr_cell;
+    void dealloc(buffer<expr_cell*> & to_delete);
 public:
-    expr_const(name const & n);
+    expr_const(name const & n, expr const & type);
     name const & get_name() const { return m_name; }
+    expr const & get_type() const { return m_type; }
 };
 /** \brief Function Applications */
 class expr_app : public expr_cell {
@@ -375,7 +381,7 @@ inline bool is_abstraction(expr const & e) { return is_lambda(e) || is_pi(e); }
 // Constructors
 inline expr mk_var(unsigned idx) { return expr(new expr_var(idx)); }
 inline expr Var(unsigned idx) { return mk_var(idx); }
-inline expr mk_constant(name const & n) { return expr(new expr_const(n)); }
+inline expr mk_constant(name const & n, expr const & t = expr()) { return expr(new expr_const(n, t)); }
 inline expr Const(name const & n) { return mk_constant(n); }
 inline expr mk_value(value & v) { return expr(new expr_value(v)); }
 inline expr to_expr(value & v) { return mk_value(v); }
@@ -444,6 +450,8 @@ inline bool          is_shared(expr_cell * e)            { return get_rc(e) > 1;
 inline unsigned      var_idx(expr_cell * e)              { return to_var(e)->get_vidx(); }
 inline bool          is_var(expr_cell * e, unsigned i)   { return is_var(e) && var_idx(e) == i; }
 inline name const &  const_name(expr_cell * e)           { return to_constant(e)->get_name(); }
+// Remark: the following function should not be exposed in the internal API.
+inline expr const &  const_type(expr_cell * e)           { return to_constant(e)->get_type(); }
 inline value const & to_value(expr_cell * e)             { lean_assert(is_value(e)); return static_cast<expr_value*>(e)->get_value(); }
 inline unsigned      num_args(expr_cell * e)             { return to_app(e)->get_num_args(); }
 inline expr const &  arg(expr_cell * e, unsigned idx)    { return to_app(e)->get_arg(idx); }
@@ -469,6 +477,8 @@ inline unsigned      var_idx(expr const & e)              { return to_var(e)->ge
 /** \brief Return true iff the given expression is a variable with de Bruijn index equal to \c i. */
 inline bool          is_var(expr const & e, unsigned i)   { return is_var(e) && var_idx(e) == i; }
 inline name const &  const_name(expr const & e)           { return to_constant(e)->get_name(); }
+// Remark: the following function should not be exposed in the internal API.
+inline expr const &  const_type(expr const & e)           { return to_constant(e)->get_type(); }
 /** \brief Return true iff the given expression is a constant with name \c n. */
 inline bool          is_constant(expr const & e, name const & n) {
     return is_constant(e) && const_name(e) == n;
@@ -647,6 +657,12 @@ inline expr update_metavar(expr const & e, local_context const & lctx) {
     else
         return e;
 }
+inline expr update_const(expr const & e, expr const & t) {
+    if (!is_eqp(const_type(e), t))
+        return mk_constant(const_name(e), t);
+    else
+        return e;
+}
 // =======================================
 
 std::ostream & operator<<(std::ostream & out, expr const & e);
diff --git a/src/kernel/expr_eq.h b/src/kernel/expr_eq.h
index 2e8bbae2a..0c24a2680 100644
--- a/src/kernel/expr_eq.h
+++ b/src/kernel/expr_eq.h
@@ -46,7 +46,7 @@ class expr_eq_fn {
         }
         switch (a.kind()) {
         case expr_kind::Var:      lean_unreachable(); // LCOV_EXCL_LINE
-        case expr_kind::Constant: return const_name(a) == const_name(b);
+        case expr_kind::Constant: return const_name(a) == const_name(b) && apply(const_type(a), const_type(b));
         case expr_kind::App:
             if (num_args(a) != num_args(b))
                 return false;
diff --git a/src/kernel/for_each.h b/src/kernel/for_each.h
index bee6e7272..f93c3a9eb 100644
--- a/src/kernel/for_each.h
+++ b/src/kernel/for_each.h
@@ -40,7 +40,14 @@ class for_each_fn {
             unsigned offset = p.second;
             if (!CacheAtomic) {
                 switch (e.kind()) {
-                case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
+                case expr_kind::Constant:
+                    if (!const_type(e)) {
+                        // only constants without cached types are considered atomic
+                        m_f(e, offset);
+                        goto begin_loop;
+                    }
+                    break;
+                case expr_kind::Type: case expr_kind::Value:
                 case expr_kind::Var: case expr_kind::MetaVar:
                     m_f(e, offset);
                     goto begin_loop;
@@ -62,7 +69,11 @@ class for_each_fn {
                 goto begin_loop;
 
             switch (e.kind()) {
-            case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
+            case expr_kind::Constant:
+                if (const_type(e))
+                    todo.emplace_back(const_type(e), offset);
+                goto begin_loop;
+            case expr_kind::Type: case expr_kind::Value:
             case expr_kind::Var: case expr_kind::MetaVar:
                 goto begin_loop;
             case expr_kind::App: {
diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp
index b91e9243c..a8ef36817 100644
--- a/src/kernel/free_vars.cpp
+++ b/src/kernel/free_vars.cpp
@@ -24,7 +24,11 @@ protected:
     bool apply(expr const & e, unsigned offset) {
         // handle easy cases
         switch (e.kind()) {
-        case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
+        case expr_kind::Constant:
+            if (!const_type(e))
+                return false;
+            break;
+        case expr_kind::Type: case expr_kind::Value:
             return false;
         case expr_kind::MetaVar:
             return true;
@@ -58,7 +62,11 @@ protected:
         bool result = false;
 
         switch (e.kind()) {
-        case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: case expr_kind::MetaVar:
+        case expr_kind::Constant:
+            lean_assert(const_type(e));
+            result = apply(const_type(e), offset);
+            break;
+        case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: case expr_kind::MetaVar:
             // easy cases were already handled
             lean_unreachable(); // LCOV_EXCL_LINE
         case expr_kind::App:
@@ -109,7 +117,11 @@ protected:
     bool apply(expr const & e, unsigned offset) {
         // handle easy cases
         switch (e.kind()) {
-        case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
+        case expr_kind::Constant:
+            if (!const_type(e))
+                return false;
+            break;
+        case expr_kind::Type: case expr_kind::Value:
             return false;
         case expr_kind::MetaVar:
             return true;
@@ -133,7 +145,11 @@ protected:
         bool result = false;
 
         switch (e.kind()) {
-        case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: case expr_kind::MetaVar:
+        case expr_kind::Constant:
+            lean_assert(const_type(e));
+            result = apply(const_type(e), offset);
+            break;
+        case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: case expr_kind::MetaVar:
             // easy cases were already handled
             lean_unreachable(); // LCOV_EXCL_LINE
         case expr_kind::App:
diff --git a/src/kernel/has_cached_type.cpp b/src/kernel/has_cached_type.cpp
new file mode 100644
index 000000000..e3a743af4
--- /dev/null
+++ b/src/kernel/has_cached_type.cpp
@@ -0,0 +1,27 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/expr.h"
+#include "kernel/for_each.h"
+
+namespace lean {
+bool has_cached_type(expr const & e) {
+    bool result = false;
+    auto f = [&](expr const & e, unsigned) {
+        if (result) {
+            return false; // do not continue the search
+        } else if (is_constant(e) && const_type(e)) {
+            result = true;
+            return false;
+        } else {
+            return true;
+        }
+    };
+    for_each_fn<decltype(f)> proc(f);
+    proc(e);
+    return result;
+}
+}
diff --git a/src/kernel/has_cached_type.h b/src/kernel/has_cached_type.h
new file mode 100644
index 000000000..eba6a15cc
--- /dev/null
+++ b/src/kernel/has_cached_type.h
@@ -0,0 +1,22 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/expr.h"
+
+namespace lean {
+/**
+   \brief Return true iff \c e contains a constant with a cached type.
+
+   The kernel should *not* accept expressions containing cached types.
+   Reason: Cached types may introduce unsoundness.
+   For example, in the environment env, the constant x may have type T.
+   Now suppose we are trying to add a new definition D that contains x,
+   and x is associated with a cached type T'. The cached type may allow
+   us to accept a definition that is type incorrect with respect to env.
+*/
+bool has_cached_type(expr const & e);
+}
diff --git a/src/kernel/replace.h b/src/kernel/replace.h
index b532fafca..e4d776f30 100644
--- a/src/kernel/replace.h
+++ b/src/kernel/replace.h
@@ -59,7 +59,11 @@ class replace_fn {
         expr r = m_f(e, offset);
         if (is_eqp(e, r)) {
             switch (e.kind()) {
-            case expr_kind::Type: case expr_kind::Value: case expr_kind::Constant:
+            case expr_kind::Constant:
+                if (const_type(e))
+                    r = update_const(e, apply(const_type(e), offset));
+                break;
+            case expr_kind::Type: case expr_kind::Value:
             case expr_kind::Var: case expr_kind::MetaVar:
                 break;
             case expr_kind::App:
diff --git a/src/kernel/replace_visitor.cpp b/src/kernel/replace_visitor.cpp
index f670dd435..90317c589 100644
--- a/src/kernel/replace_visitor.cpp
+++ b/src/kernel/replace_visitor.cpp
@@ -10,9 +10,16 @@ Author: Leonardo de Moura
 namespace lean {
 expr replace_visitor::visit_type(expr const & e, context const &) { lean_assert(is_type(e)); return e; }
 expr replace_visitor::visit_value(expr const & e, context const &) { lean_assert(is_value(e)); return e; }
-expr replace_visitor::visit_constant(expr const & e, context const &) { lean_assert(is_constant(e)); return e; }
 expr replace_visitor::visit_var(expr const & e, context const &) { lean_assert(is_var(e)); return e; }
 expr replace_visitor::visit_metavar(expr const & e, context const &) { lean_assert(is_metavar(e)); return e; }
+expr replace_visitor::visit_constant(expr const & e, context const & ctx) {
+    lean_assert(is_constant(e));
+    if (const_type(e)) {
+        return update_const(e, visit(const_type(e), ctx));
+    } else {
+        return e;
+    }
+}
 expr replace_visitor::visit_app(expr const & e, context const & ctx) {
     lean_assert(is_app(e));
     return update_app(e, [&](expr const & c) { return visit(c, ctx); });
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 735f4b707..d42387dc5 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -107,11 +107,15 @@ class type_checker::imp {
             }
             break;
         case expr_kind::Constant: {
-            object const & obj = env().get_object(const_name(e));
-            if (obj.has_type())
-                r = obj.get_type();
-            else
-                throw has_no_type_exception(env(), e);
+            if (const_type(e)) {
+                r = const_type(e);
+            } else {
+                object const & obj = env().get_object(const_name(e));
+                if (obj.has_type())
+                    r = obj.get_type();
+                else
+                    throw has_no_type_exception(env(), e);
+            }
             break;
         }
         case expr_kind::Var:
diff --git a/src/library/max_sharing.cpp b/src/library/max_sharing.cpp
index f931b57fb..e932ad692 100644
--- a/src/library/max_sharing.cpp
+++ b/src/library/max_sharing.cpp
@@ -36,7 +36,16 @@ struct max_sharing_fn::imp {
             return a;
         }
         switch (a.kind()) {
-        case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
+        case expr_kind::Constant:
+            if (const_type(a)) {
+                expr r = update_const(a, apply(const_type(a)));
+                cache(r);
+                return r;
+            } else {
+                cache(a);
+                return a;
+            }
+        case expr_kind::Var: case expr_kind::Type: case expr_kind::Value:
             cache(a);
             return a;
         case expr_kind::App: {
diff --git a/src/library/type_inferer.cpp b/src/library/type_inferer.cpp
index cc20dc87c..49603e09c 100644
--- a/src/library/type_inferer.cpp
+++ b/src/library/type_inferer.cpp
@@ -110,11 +110,15 @@ class type_inferer::imp {
                 throw unexpected_metavar_occurrence(m_env, e);
             }
         case expr_kind::Constant: {
-            object const & obj = m_env.get_object(const_name(e));
-            if (obj.has_type())
-                return obj.get_type();
-            else
-                throw has_no_type_exception(m_env, e);
+            if (const_type(e)) {
+                return const_type(e);
+            } else {
+                object const & obj = m_env.get_object(const_name(e));
+                if (obj.has_type())
+                    return obj.get_type();
+                else
+                    throw has_no_type_exception(m_env, e);
+            }
             break;
         }
         case expr_kind::Var: {