Add interrupt method to type checker.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/type_check.cpp

@@ -42,11 +42,12 @@ bool is_convertible(expr const & expected, expr const & given, environment const
 }
 
 /** \brief Auxiliary functional object used to implement infer_type. */
-struct infer_type_fn {
+class type_checker::imp {
     typedef scoped_map<expr, expr, expr_hash, expr_eqp> cache;
 
-    environment const & m_env;
+    environment     m_env;
-    cache               m_cache;
+    cache           m_cache;
+    volatile bool   m_interrupted;
 
     expr lookup(context const & c, unsigned i) {
         auto p = lookup_ext(c, i);
@@ -56,15 +57,6 @@ struct infer_type_fn {
         return lift_free_vars(def.get_domain(), length(c) - length(def_c));
     }
 
-    level infer_universe(expr const & t, context const & ctx) {
-        expr u = normalize(infer_type(t, ctx), m_env, ctx);
-        if (is_type(u))
-            return ty_level(u);
-        if (u == Bool)
-            return level();
-        throw type_expected_exception(m_env, ctx, t);
-    }
-
     expr check_pi(expr const & e, expr const & s, context const & ctx) {
         if (is_pi(e))
             return e;
@@ -78,7 +70,24 @@ struct infer_type_fn {
         return check_pi(infer_type(e, ctx), e, ctx);
     }
 
+public:
+    imp(environment const & env):
+        m_env(env) {
+        m_interrupted = false;
+    }
+
+    level infer_universe(expr const & t, context const & ctx) {
+        expr u = normalize(infer_type(t, ctx), m_env, ctx);
+        if (is_type(u))
+            return ty_level(u);
+        if (u == Bool)
+            return level();
+        throw type_expected_exception(m_env, ctx, t);
+    }
+
     expr infer_type(expr const & e, context const & ctx) {
+        if (m_interrupted)
+            throw interrupted();
         bool shared = false;
         if (is_shared(e)) {
             shared = true;
@@ -167,20 +176,27 @@ struct infer_type_fn {
         return r;
     }
 
-    infer_type_fn(environment const & env):
+    void set_interrupt(bool flag) {
-        m_env(env) {
+        m_interrupted = true;
     }
 
-    expr operator()(expr const & e, context const & ctx) {
+    void clear() {
-        return infer_type(e, ctx);
+        m_cache.clear();
     }
 };
 
+type_checker::type_checker(environment const & env):m_ptr(new imp(env)) {}
+type_checker::~type_checker() {}
+expr type_checker::infer_type(expr const & e, context const & ctx) { return m_ptr->infer_type(e, ctx); }
+level type_checker::infer_universe(expr const & e, context const & ctx) { return m_ptr->infer_universe(e, ctx); }
+void type_checker::clear() { m_ptr->clear(); }
+void type_checker::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); }
+
 expr  infer_type(expr const & e, environment const & env, context const & ctx) {
-    return infer_type_fn(env)(e, ctx);
+    return type_checker(env).infer_type(e, ctx);
 }
 
 level infer_universe(expr const & t, environment const & env, context const & ctx) {
-    return infer_type_fn(env).infer_universe(t, ctx);
+    return type_checker(env).infer_universe(t, ctx);
 }
 }

src/kernel/type_check.h

@@ -5,11 +5,30 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <memory>
 #include "expr.h"
 #include "context.h"
 
 namespace lean {
 class environment;
+class type_checker {
+    struct imp;
+    std::unique_ptr<imp> m_ptr;
+public:
+    type_checker(environment const & env);
+    ~type_checker();
+
+    expr infer_type(expr const & e, context const & ctx = context());
+    level infer_universe(expr const & e, context const & ctx = context());
+    void check(expr const & e, context const & ctx = context()) { infer_type(e, ctx); }
+
+    void clear();
+
+    void set_interrupt(bool flag);
+    void interrupt() { set_interrupt(true); }
+    void reset_interrupt() { set_interrupt(false); }
+};
+
 expr infer_type(expr const & e, environment const & env, context const & ctx = context());
 level infer_universe(expr const & t, environment const & env, context const & ctx = context());
 bool is_convertible(expr const & t1, expr const & t2, environment const & env, context const & ctx = context());

src/tests/kernel/type_check.cpp

@@ -5,6 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <iostream>
+#include <thread>
+#include <chrono>
 #include "type_check.h"
 #include "environment.h"
 #include "abstract.h"
@@ -14,6 +16,7 @@ Author: Leonardo de Moura
 #include "builtin.h"
 #include "arith.h"
 #include "normalize.h"
+#include "printer.h"
 #include "trace.h"
 #include "test.h"
 using namespace lean;
@@ -205,6 +208,37 @@ static void tst11() {
     env.add_theorem("eqs2", Eq(t1,t3), Refl(Int, t1));
 }
 
+static expr mk_big(unsigned depth) {
+    if (depth == 0)
+        return Const("a");
+    else
+        return Const("f")(mk_big(depth - 1), mk_big(depth - 1));
+}
+
+static void tst12() {
+#ifndef __APPLE__
+    expr t = mk_big(18);
+    environment env;
+    env.add_var("f", Int >> (Int >> Int));
+    env.add_var("a", Int);
+    type_checker checker(env);
+    std::chrono::milliseconds dura(100);
+    std::thread thread([&]() {
+            try {
+                std::cout << checker.infer_type(t) << "\n";
+                // Remark: if the following code is reached, we
+                // should decrease dura.
+                lean_unreachable();
+            } catch (interrupted & it) {
+                std::cout << "interrupted\n";
+            }
+        });
+    std::this_thread::sleep_for(dura);
+    checker.interrupt();
+    thread.join();
+#endif
+}
+
 int main() {
     tst1();
     tst2();
@@ -217,5 +251,6 @@ int main() {
     tst9();
     tst10();
     tst11();
+    tst12();
     return has_violations() ? 1 : 0;
 }

src/util/exception.h

@@ -35,4 +35,11 @@ public:
     unsigned get_line() const { return m_line; }
     unsigned get_pos() const { return m_pos; }
 };
+/** \brief Exception used to sign that a computation was interrupted */
+class interrupted : public exception {
+public:
+    interrupted() {}
+    virtual ~interrupted() noexcept {}
+    virtual char const * what() const noexcept { return "interrupted"; }
+};
 }