diff --git a/src/kernel/type_check.cpp b/src/kernel/type_check.cpp index 6884bf4cd..72783115f 100644 --- a/src/kernel/type_check.cpp +++ b/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 cache; - environment const & m_env; - cache m_cache; + environment m_env; + 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): - m_env(env) { + void set_interrupt(bool flag) { + m_interrupted = true; } - expr operator()(expr const & e, context const & ctx) { - return infer_type(e, ctx); + void clear() { + 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); } } diff --git a/src/kernel/type_check.h b/src/kernel/type_check.h index dcdbf0421..ed697e1de 100644 --- a/src/kernel/type_check.h +++ b/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 #include "expr.h" #include "context.h" namespace lean { class environment; +class type_checker { + struct imp; + std::unique_ptr 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()); diff --git a/src/tests/kernel/type_check.cpp b/src/tests/kernel/type_check.cpp index e30a0bc9a..87fac7b7f 100644 --- a/src/tests/kernel/type_check.cpp +++ b/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 +#include +#include #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; } diff --git a/src/util/exception.h b/src/util/exception.h index 9f1624de5..a3f9eab33 100644 --- a/src/util/exception.h +++ b/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"; } +}; }