From c4c548dc5def0048f62d67fcccf231f302496626 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 12 Nov 2013 21:42:22 -0800 Subject: [PATCH] feat(*): simplify interrupt propagation Instead of having m_interrupted flags in several components. We use a thread_local global variable. The new approach is much simpler to get right since there is no risk of "forgetting" to propagate the set_interrupt method to sub-components. The plan is to support set_interrupt methods and m_interrupted flags only in tactic objects. We need to support them in tactics and tacticals because we want to implement combinators/tacticals such as (try_for T M) that fails if tactic T does not finish in M ms. For example, consider the tactic: try-for (T1 ORELSE T2) 5 It tries the tactic (T1 ORELSE T2) for 5ms. Thus, if T1 does not finish after 5ms an interrupt request is sent, and T1 is interrupted. Now, if you do not have a m_interrupted flag marking each tactic, the ORELSE combinator will try T2. The set_interrupt method for ORELSE tactical should turn on the m_interrupted flag. Signed-off-by: Leonardo de Moura --- src/frontends/lean/frontend.h | 8 ------ src/frontends/lean/frontend_elaborator.cpp | 17 ++---------- src/frontends/lean/frontend_elaborator.h | 4 --- src/frontends/lean/parser.cpp | 28 +------------------ src/frontends/lean/parser.h | 10 ------- src/frontends/lean/pp.cpp | 32 ++++------------------ src/kernel/environment.cpp | 8 ------ src/kernel/environment.h | 4 --- src/kernel/formatter.h | 3 -- src/kernel/normalizer.cpp | 7 ++--- src/kernel/normalizer.h | 4 --- src/kernel/type_checker.cpp | 11 ++------ src/kernel/type_checker.h | 5 ---- src/library/elaborator/elaborator.cpp | 20 +++----------- src/library/elaborator/elaborator.h | 2 -- src/library/elaborator/elaborator_plugin.h | 1 - src/library/elaborator/synthesizer.h | 1 - src/library/state.h | 1 - src/library/type_inferer.cpp | 11 ++------ src/library/type_inferer.h | 4 --- src/shell/lean.cpp | 9 ++---- src/tests/kernel/normalizer.cpp | 6 ++-- src/tests/kernel/type_checker.cpp | 6 ++-- src/tests/library/formatter.cpp | 2 -- src/util/interrupt.cpp | 6 ++-- src/util/interrupt.h | 6 ++-- 26 files changed, 35 insertions(+), 181 deletions(-) diff --git a/src/frontends/lean/frontend.h b/src/frontends/lean/frontend.h index 98d3b38b4..b6dc62b77 100644 --- a/src/frontends/lean/frontend.h +++ b/src/frontends/lean/frontend.h @@ -189,13 +189,5 @@ public: void set_regular_channel(std::shared_ptr const & out) { m_state.set_regular_channel(out); } void set_diagnostic_channel(std::shared_ptr const & out) { m_state.set_diagnostic_channel(out); } /*@}*/ - - /** - @name Interrupts. - */ - void set_interrupt(bool flag) { m_env.set_interrupt(flag); m_state.set_interrupt(flag); } - void interrupt() { set_interrupt(true); } - void reset_interrupt() { set_interrupt(false); } - /*@}*/ }; } diff --git a/src/frontends/lean/frontend_elaborator.cpp b/src/frontends/lean/frontend_elaborator.cpp index 4d4cfa17c..d1b0eaec6 100644 --- a/src/frontends/lean/frontend_elaborator.cpp +++ b/src/frontends/lean/frontend_elaborator.cpp @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include #include #include -#include "util/interruptable_ptr.h" +#include "util/interrupt.h" #include "kernel/type_checker.h" #include "kernel/type_checker_justification.h" #include "kernel/normalizer.h" @@ -112,8 +112,6 @@ class frontend_elaborator::imp { // We need that because a frontend may associate line number information // with the original non-elaborated expressions. expr_map m_trace; - interruptable_ptr m_elaborator; - volatile bool m_interrupted; /** \brief Replace placeholders and choices with metavariables. @@ -378,7 +376,7 @@ class frontend_elaborator::imp { } virtual expr visit(expr const & e, context const & ctx) { - check_interrupted(m_ref.m_interrupted); + check_interrupted(); expr r = replace_visitor::visit(e, ctx); if (!is_eqp(r, e)) m_ref.m_trace[r] = e; @@ -392,7 +390,6 @@ class frontend_elaborator::imp { // return !is_choice(c1) && is_choice(c2); // }); elaborator elb(m_env, m_menv, m_ucs.size(), m_ucs.data()); - scoped_set_interruptable_ptr set(m_elaborator, &elb); return elb.next(); } @@ -403,7 +400,6 @@ public: m_type_checker(m_env), m_type_inferer(m_env), m_normalizer(m_env) { - m_interrupted = false; } expr elaborate(expr const & e) { @@ -458,14 +454,6 @@ public: } } - void set_interrupt(bool f) { - m_interrupted = f; - m_type_checker.set_interrupt(f); - m_type_inferer.set_interrupt(f); - m_normalizer.set_interrupt(f); - m_elaborator.set_interrupt(f); - } - void clear() { m_menv = metavar_env(); m_ucs.clear(); @@ -485,7 +473,6 @@ frontend_elaborator::~frontend_elaborator() {} expr frontend_elaborator::operator()(expr const & e) { return m_ptr->elaborate(e); } std::pair frontend_elaborator::operator()(name const & n, expr const & t, expr const & e) { return m_ptr->elaborate(n, t, e); } expr const & frontend_elaborator::get_original(expr const & e) const { return m_ptr->get_original(e); } -void frontend_elaborator::set_interrupt(bool f) { m_ptr->set_interrupt(f); } void frontend_elaborator::clear() { m_ptr->clear(); } environment const & frontend_elaborator::get_environment() const { return m_ptr->get_environment(); } } diff --git a/src/frontends/lean/frontend_elaborator.h b/src/frontends/lean/frontend_elaborator.h index 19d81556d..3f22055c9 100644 --- a/src/frontends/lean/frontend_elaborator.h +++ b/src/frontends/lean/frontend_elaborator.h @@ -44,10 +44,6 @@ public: */ expr const & get_original(expr const & e) const; - void set_interrupt(bool flag); - void interrupt() { set_interrupt(true); } - void reset_interrupt() { set_interrupt(false); } - void clear(); environment const & get_environment() const; diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 6de369ea4..b1014f7a7 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -20,6 +20,7 @@ Author: Leonardo de Moura #include "util/exception.h" #include "util/sstream.h" #include "util/sexpr/option_declarations.h" +#include "util/interrupt.h" #include "kernel/normalizer.h" #include "kernel/type_checker.h" #include "kernel/free_vars.h" @@ -129,10 +130,6 @@ class parser::imp { expr_pos_info m_expr_pos_info; pos_info m_last_cmd_pos; pos_info m_last_script_pos; - // Reference to temporary parser used to process import command. - // We need this reference to be able to interrupt it. - interruptable_ptr m_import_parser; - interruptable_ptr m_normalizer; leanlua_state * m_leanlua_state; @@ -1170,7 +1167,6 @@ class parser::imp { next(); expr v = m_elaborator(parse_expr()); normalizer norm(m_frontend); - scoped_set_interruptable_ptr set(m_normalizer, &norm); expr r = norm(v); regular(m_frontend) << r << endl; } @@ -1403,7 +1399,6 @@ class parser::imp { if (m_verbose) regular(m_frontend) << "Importing file '" << fname << "'" << endl; parser import_parser(m_frontend, in, m_leanlua_state, true /* use exceptions */, false /* not interactive */); - scoped_set_interruptable_ptr set(m_import_parser, &import_parser); import_parser(); } catch (interrupted &) { throw; @@ -1686,17 +1681,6 @@ public: throw parser_exception(ex.what(), ex.m_pos.first, ex.m_pos.second); } } - - void set_interrupt(bool flag) { - m_frontend.set_interrupt(flag); - m_elaborator.set_interrupt(flag); - m_import_parser.set_interrupt(flag); - m_normalizer.set_interrupt(flag); - } - - void reset_interrupt() { - set_interrupt(false); - } }; parser::parser(frontend & fe, std::istream & in, leanlua_state * S, bool use_exceptions, bool interactive) { @@ -1711,10 +1695,6 @@ bool parser::operator()() { return m_ptr->parse_commands(); } -void parser::set_interrupt(bool flag) { - m_ptr->set_interrupt(flag); -} - expr parser::parse_expr() { return m_ptr->parse_expr_main(); } @@ -1736,7 +1716,6 @@ bool shell::operator()() { std::istringstream strm(input); { parser p(m_frontend, strm, m_leanlua_state, false, false); - scoped_set_interruptable_ptr set(m_parser, &p); if (!p()) errors = true; } @@ -1744,12 +1723,7 @@ bool shell::operator()() { } #else parser p(m_frontend, std::cin, m_leanlua_state, false, true); - scoped_set_interruptable_ptr set(m_parser, &p); return p(); #endif } - -void shell::set_interrupt(bool flag) { - m_parser.set_interrupt(flag); -} } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 061724dee..174b9029d 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -6,7 +6,6 @@ Author: Leonardo de Moura */ #pragma once #include -#include "util/interruptable_ptr.h" #include "frontends/lean/frontend.h" namespace lean { @@ -24,26 +23,17 @@ public: /** \brief Parse a single expression */ expr parse_expr(); - - void set_interrupt(bool flag); - void interrupt() { set_interrupt(true); } - void reset_interrupt() { set_interrupt(false); } }; /** \brief Implements the Read Eval Print loop */ class shell { frontend & m_frontend; leanlua_state * m_leanlua_state; - interruptable_ptr m_parser; public: shell(frontend & fe, leanlua_state * S); ~shell(); bool operator()(); - - void set_interrupt(bool flag); - void interrupt() { set_interrupt(true); } - void reset_interrupt() { set_interrupt(false); } }; inline bool parse_commands(frontend & fe, std::istream & in, leanlua_state * S = nullptr, bool use_exceptions = true, bool interactive = false) { diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index f41a0ce5c..07d5a044c 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -13,7 +13,7 @@ Author: Leonardo de Moura #include "util/exception.h" #include "util/scoped_set.h" #include "util/sexpr/options.h" -#include "util/interruptable_ptr.h" +#include "util/interrupt.h" #include "kernel/context.h" #include "kernel/for_each.h" #include "kernel/occurs.h" @@ -169,8 +169,6 @@ class pp_fn { bool m_notation; //!< if true use notation bool m_extra_lets; //!< introduce extra let-expression to cope with sharing. unsigned m_alias_min_weight; //!< minimal weight for creating an alias - volatile bool m_interrupted; - // Create a scope for local definitions struct mk_scope { @@ -1072,7 +1070,7 @@ class pp_fn { } result pp(expr const & e, unsigned depth, bool main = false) { - check_interrupted(m_interrupted); + check_interrupted(); if (!is_atomic(e) && (m_num_steps > m_max_steps || depth > m_max_depth)) { return pp_ellipsis(); } else { @@ -1170,7 +1168,6 @@ public: pp_fn(frontend const & fe, options const & opts): m_frontend(fe) { set_options(opts); - m_interrupted = false; m_num_steps = 0; } @@ -1190,10 +1187,6 @@ public: return pp_abstraction_core(e, 0, expr(), &implicit_args).first; } - void set_interrupt(bool flag) { - m_interrupted = flag; - } - void register_local(name const & n) { m_local_names.insert(n); } @@ -1201,24 +1194,20 @@ public: class pp_formatter_cell : public formatter_cell { frontend const & m_frontend; - interruptable_ptr m_pp_fn; - volatile bool m_interrupted; format pp(expr const & e, options const & opts) { pp_fn fn(m_frontend, opts); - scoped_set_interruptable_ptr set(m_pp_fn, &fn); return fn(e); } format pp(context const & c, expr const & e, bool include_e, options const & opts) { pp_fn fn(m_frontend, opts); - scoped_set_interruptable_ptr set(m_pp_fn, &fn); unsigned indent = get_pp_indent(opts); format r; bool first = true; expr c2 = context_to_lambda(c, e); while (is_fake_context(c2)) { - check_interrupted(m_interrupted); + check_interrupted(); name n1 = get_unused_name(c2); fn.register_local(n1); format entry = format{format(n1), space(), colon(), space(), fn(fake_context_domain(c2))}; @@ -1255,7 +1244,7 @@ class pp_formatter_cell : public formatter_cell { expr it1 = t; expr it2 = v; while (is_pi(it1) && is_lambda(it2)) { - check_interrupted(m_interrupted); + check_interrupted(); if (abst_domain(it1) != abst_domain(it2)) return pp_definition(kwd, n, t, v, opts); it1 = abst_body(it1); @@ -1269,7 +1258,6 @@ class pp_formatter_cell : public formatter_cell { if (m_frontend.has_implicit_arguments(n)) implicit_args = &(m_frontend.get_implicit_arguments(n)); pp_fn fn(m_frontend, opts); - scoped_set_interruptable_ptr set(m_pp_fn, &fn); format def = fn.pp_definition(v, t, implicit_args); return format{highlight_command(format(kwd)), space(), format(n), def}; } @@ -1286,7 +1274,6 @@ class pp_formatter_cell : public formatter_cell { format r = format{highlight_command(format(kwd)), space(), format(n)}; if (m_frontend.has_implicit_arguments(n)) { pp_fn fn(m_frontend, opts); - scoped_set_interruptable_ptr set(m_pp_fn, &fn); r += fn.pp_pi_with_implicit_args(obj.get_type(), m_frontend.get_implicit_arguments(n)); } else { r += format{space(), colon(), space(), pp(obj.get_type(), opts)}; @@ -1329,7 +1316,6 @@ class pp_formatter_cell : public formatter_cell { public: pp_formatter_cell(frontend const & fe): m_frontend(fe) { - m_interrupted = false; } virtual ~pp_formatter_cell() { @@ -1348,10 +1334,9 @@ public: return pp(c, e, true, opts); } else { pp_fn fn(m_frontend, opts); - scoped_set_interruptable_ptr set(m_pp_fn, &fn); expr c2 = context_to_lambda(c, e); while (is_fake_context(c2)) { - check_interrupted(m_interrupted); + check_interrupted(); name n1 = get_unused_name(c2); fn.register_local(n1); expr const & rest = fake_context_rest(c2); @@ -1389,17 +1374,12 @@ public: std::for_each(env.begin_objects(), env.end_objects(), [&](object const & obj) { - check_interrupted(m_interrupted); + check_interrupted(); if (first) first = false; else r += line(); r += operator()(obj, opts); }); return r; } - - virtual void set_interrupt(bool flag) { - m_pp_fn.set_interrupt(flag); - m_interrupted = flag; - } }; formatter mk_pp_formatter(frontend const & fe) { diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 39046d293..02b7e0048 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -402,10 +402,6 @@ struct environment::imp { } } - void set_interrupt(bool flag) { - m_type_checker->set_interrupt(flag); - } - imp(): m_num_children(0) { init_uvars(); @@ -531,10 +527,6 @@ void environment::display(std::ostream & out) const { m_ptr->display(out, *this); } -void environment::set_interrupt(bool flag) { - m_ptr->set_interrupt(flag); -} - environment::extension const & environment::get_extension_core(unsigned extid) const { return m_ptr->get_extension_core(extid); } diff --git a/src/kernel/environment.h b/src/kernel/environment.h index a4004d0e1..10a1f43c7 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -209,10 +209,6 @@ public: /** \brief Display universal variable constraints and objects stored in this environment and its parents. */ void display(std::ostream & out) const; - void set_interrupt(bool flag); - void interrupt() { set_interrupt(true); } - void reset_interrupt() { set_interrupt(false); } - /** \brief Frontend can store data in environment extensions. Each extension is associated with a unique token/id. diff --git a/src/kernel/formatter.h b/src/kernel/formatter.h index 2a8c34251..3d90f2b4f 100644 --- a/src/kernel/formatter.h +++ b/src/kernel/formatter.h @@ -34,8 +34,6 @@ public: virtual format operator()(object const & obj, options const & opts) = 0; /** \brief Format the given environment */ virtual format operator()(environment const & env, options const & opts) = 0; - /** \brief Request interruption */ - virtual void set_interrupt(bool ) {} }; /** \brief Smart-pointer for the actual formatter object (aka \c formatter_cell). @@ -50,7 +48,6 @@ public: format operator()(context const & c, expr const & e, bool format_ctx = false, options const & opts = options()) const { return (*m_cell)(c, e, format_ctx, opts); } format operator()(object const & obj, options const & opts = options()) const { return (*m_cell)(obj, opts); } format operator()(environment const & env, options const & opts = options()) const { return (*m_cell)(env, opts); } - void set_interrupt(bool flag) { m_cell->set_interrupt(flag); } }; /** \brief Create a simple formatter object based on \c print function. diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index 34705fd7b..0aefcc8b7 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include "util/list.h" #include "util/flet.h" #include "util/buffer.h" +#include "util/interrupt.h" #include "util/sexpr/options.h" #include "kernel/normalizer.h" #include "kernel/expr.h" @@ -74,7 +75,6 @@ class normalizer::imp { cache m_cache; unsigned m_max_depth; unsigned m_depth; - volatile bool m_interrupted; environment env() const { return environment(m_env); } @@ -179,7 +179,7 @@ class normalizer::imp { /** \brief Normalize the expression \c a in a context composed of stack \c s and \c k binders. */ svalue normalize(expr const & a, value_stack const & s, unsigned k) { flet l(m_depth, m_depth+1); - check_interrupted(m_interrupted); + check_interrupted(); if (m_depth > m_max_depth) throw kernel_exception(env(), "normalizer maximum recursion depth exceeded"); bool shared = false; @@ -294,7 +294,6 @@ class normalizer::imp { public: imp(environment const & env, unsigned max_depth): m_env(env.to_weak_ref()) { - m_interrupted = false; m_max_depth = max_depth; m_depth = 0; } @@ -306,7 +305,6 @@ public: } void clear() { m_ctx = context(); m_cache.clear(); } - void set_interrupt(bool flag) { m_interrupted = flag; } }; normalizer::normalizer(environment const & env, unsigned max_depth):m_ptr(new imp(env, max_depth)) {} @@ -315,7 +313,6 @@ normalizer::normalizer(environment const & env, options const & opts):normalizer normalizer::~normalizer() {} expr normalizer::operator()(expr const & e, context const & ctx) { return (*m_ptr)(e, ctx); } void normalizer::clear() { m_ptr->clear(); } -void normalizer::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); } expr normalize(expr const & e, environment const & env, context const & ctx) { return normalizer(env)(e, ctx); diff --git a/src/kernel/normalizer.h b/src/kernel/normalizer.h index bb76ae9ba..b7842f3b8 100644 --- a/src/kernel/normalizer.h +++ b/src/kernel/normalizer.h @@ -26,10 +26,6 @@ public: expr operator()(expr const & e, context const & ctx = context()); void clear(); - - void set_interrupt(bool flag); - void interrupt() { set_interrupt(true); } - void reset_interrupt() { set_interrupt(false); } }; /** \brief Normalize \c e using the environment \c env and context \c ctx */ expr normalize(expr const & e, environment const & env, context const & ctx = context()); diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index d261a1ec0..d6a8cafe6 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include "util/scoped_map.h" #include "util/flet.h" +#include "util/interrupt.h" #include "kernel/type_checker.h" #include "kernel/environment.h" #include "kernel/kernel_exception.h" @@ -29,7 +30,6 @@ class type_checker::imp { metavar_env * m_menv; unsigned m_menv_timestamp; unification_constraints * m_uc; - volatile bool m_interrupted; environment env() const { return environment(m_env); @@ -85,7 +85,7 @@ class type_checker::imp { } expr infer_type_core(expr const & e, context const & ctx) { - check_interrupted(m_interrupted); + check_interrupted(); bool shared = false; if (is_shared(e)) { shared = true; @@ -289,7 +289,6 @@ public: m_menv = nullptr; m_menv_timestamp = 0; m_uc = nullptr; - m_interrupted = false; } expr infer_type(expr const & e, context const & ctx, metavar_env * menv, buffer & uc) { @@ -315,11 +314,6 @@ public: check_type(t, e, ctx); } - void set_interrupt(bool flag) { - m_interrupted = flag; - m_normalizer.set_interrupt(flag); - } - void clear() { m_cache.clear(); m_normalizer.clear(); @@ -349,7 +343,6 @@ void type_checker::check_type(expr const & e, context const & ctx) { m_ptr->check_type(e, ctx); } void type_checker::clear() { m_ptr->clear(); } -void type_checker::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); } normalizer & type_checker::get_normalizer() { return m_ptr->get_normalizer(); } expr infer_type(expr const & e, environment const & env, context const & ctx) { diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 23e599220..b208f54c0 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -56,11 +56,6 @@ public: /** \brief Reset internal caches */ void clear(); - /** \brief Interrupt type checker */ - void set_interrupt(bool flag); - void interrupt() { set_interrupt(true); } - void reset_interrupt() { set_interrupt(false); } - /** \brief Return reference to the normalizer used by this type checker. */ normalizer & get_normalizer(); }; diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index f2f2eb579..f6e2afa95 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include #include "util/pdeque.h" +#include "util/interrupt.h" #include "kernel/formatter.h" #include "kernel/free_vars.h" #include "kernel/normalizer.h" @@ -143,8 +144,6 @@ class elaborator::imp { int m_quota; justification m_conflict; bool m_first; - bool m_interrupted; - // options bool m_use_justifications; @@ -596,7 +595,7 @@ class elaborator::imp { context const & ctx = get_context(c); bool modified = false; while (true) { - check_interrupted(m_interrupted); + check_interrupted(); expr new_a = normalize_step(ctx, a); expr new_b = normalize_step(ctx, b); if (new_a == a && new_b == b) { @@ -1380,13 +1379,12 @@ public: set_options(opts); m_next_id = 0; m_quota = 0; - m_interrupted = false; m_first = true; // display(std::cout); } metavar_env next() { - check_interrupted(m_interrupted); + check_interrupted(); if (m_conflict) throw elaborator_exception(m_conflict); if (!m_case_splits.empty()) { @@ -1404,7 +1402,7 @@ public: } reset_quota(); while (true) { - check_interrupted(m_interrupted); + check_interrupted(); cnstr_queue & q = m_state.m_queue; if (q.empty() || m_quota < - static_cast(q.size()) - 10) { // TODO(Leo): implement interface with synthesizer @@ -1420,12 +1418,6 @@ public: } } - void interrupt() { - m_interrupted = true; - m_type_inferer.set_interrupt(true); - m_normalizer.set_interrupt(true); - } - void display(std::ostream & out, unification_constraint const & c) const { formatter fmt = mk_simple_formatter(); out << c.pp(fmt, options(), nullptr, false) << "\n"; @@ -1462,8 +1454,4 @@ elaborator::~elaborator() { metavar_env elaborator::next() { return m_ptr->next(); } - -void elaborator::interrupt() { - m_ptr->interrupt(); -} } diff --git a/src/library/elaborator/elaborator.h b/src/library/elaborator/elaborator.h index 034162d6d..ded5fd124 100644 --- a/src/library/elaborator/elaborator.h +++ b/src/library/elaborator/elaborator.h @@ -61,7 +61,5 @@ public: ~elaborator(); metavar_env next(); - void interrupt(); - void set_interrupt(bool ) { interrupt(); } }; } diff --git a/src/library/elaborator/elaborator_plugin.h b/src/library/elaborator/elaborator_plugin.h index 60273b305..427971e3b 100644 --- a/src/library/elaborator/elaborator_plugin.h +++ b/src/library/elaborator/elaborator_plugin.h @@ -29,7 +29,6 @@ public: */ virtual std::pair> next(justification const & assumption) = 0; /** \brief Interrupt the computation for the next solution. */ - virtual void interrupt() = 0; }; /** diff --git a/src/library/elaborator/synthesizer.h b/src/library/elaborator/synthesizer.h index 197ba128d..fccccb0f3 100644 --- a/src/library/elaborator/synthesizer.h +++ b/src/library/elaborator/synthesizer.h @@ -25,7 +25,6 @@ public: /** \brief Return the next possible solution. An elaborator_exception is throw in case of failure. */ virtual expr next() = 0; /** \brief Interrupt the computation for the next solution. */ - virtual void interrupt() = 0; }; /** diff --git a/src/library/state.h b/src/library/state.h index 017257f51..3a6a51243 100644 --- a/src/library/state.h +++ b/src/library/state.h @@ -39,7 +39,6 @@ public: template void set_option(name const & n, T const & v) { set_options(get_options().update(n, v)); } - void set_interrupt(bool flag) { m_formatter.set_interrupt(flag); } }; /** diff --git a/src/library/type_inferer.cpp b/src/library/type_inferer.cpp index 85a2b7fec..b0b5b793b 100644 --- a/src/library/type_inferer.cpp +++ b/src/library/type_inferer.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include "util/flet.h" #include "util/scoped_map.h" +#include "util/interrupt.h" #include "kernel/environment.h" #include "kernel/normalizer.h" #include "kernel/builtin.h" @@ -29,7 +30,6 @@ class type_inferer::imp { unification_constraints * m_uc; normalizer m_normalizer; cache m_cache; - volatile bool m_interrupted; expr normalize(expr const & e, context const & ctx) { return m_normalizer(e, ctx); @@ -139,7 +139,7 @@ class type_inferer::imp { break; // expensive cases } - check_interrupted(m_interrupted); + check_interrupted(); bool shared = false; if (is_shared(e)) { shared = true; @@ -214,7 +214,6 @@ public: imp(environment const & env): m_env(env), m_normalizer(env) { - m_interrupted = false; m_menv = nullptr; m_menv_timestamp = 0; m_uc = nullptr; @@ -227,11 +226,6 @@ public: return infer_type(e, ctx); } - void set_interrupt(bool flag) { - m_interrupted = flag; - m_normalizer.set_interrupt(flag); - } - void clear() { m_cache.clear(); m_normalizer.clear(); @@ -250,5 +244,4 @@ expr type_inferer::operator()(expr const & e, context const & ctx) { return operator()(e, ctx, nullptr, uc); } void type_inferer::clear() { m_ptr->clear(); } -void type_inferer::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); } } diff --git a/src/library/type_inferer.h b/src/library/type_inferer.h index 2c99900f5..0c948d149 100644 --- a/src/library/type_inferer.h +++ b/src/library/type_inferer.h @@ -35,9 +35,5 @@ public: expr operator()(expr const & e, context const & ctx = context()); void clear(); - - void set_interrupt(bool flag); - void interrupt() { set_interrupt(true); } - void reset_interrupt() { set_interrupt(false); } }; } diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 4ff702472..217c1d2e4 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -7,23 +7,19 @@ Author: Leonardo de Moura #include #include #include -#include "util/interruptable_ptr.h" +#include "util/interrupt.h" #include "kernel/printer.h" #include "frontends/lean/parser.h" #include "bindings/lua/leanlua_state.h" #include "version.h" -using lean::interruptable_ptr; using lean::shell; using lean::frontend; -using lean::scoped_set_interruptable_ptr; using lean::parser; using lean::leanlua_state; -static interruptable_ptr g_lean_shell; - static void on_ctrl_c(int ) { - g_lean_shell.set_interrupt(true); + lean::request_interrupt(); } bool lean_shell() { @@ -32,7 +28,6 @@ bool lean_shell() { frontend f; leanlua_state S; shell sh(f, &S); - scoped_set_interruptable_ptr set(g_lean_shell, &sh); signal(SIGINT, on_ctrl_c); return sh(); } diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp index 928bc8f6e..62382a4fe 100644 --- a/src/tests/kernel/normalizer.cpp +++ b/src/tests/kernel/normalizer.cpp @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include "util/test.h" #include "util/trace.h" #include "util/exception.h" +#include "util/interrupt.h" #include "kernel/normalizer.h" #include "kernel/builtin.h" #include "kernel/expr_sets.h" @@ -219,7 +220,7 @@ static void tst5() { env.add_var("a", Bool); normalizer proc(env); std::chrono::milliseconds dura(50); - std::thread thread([&]() { + interruptible_thread thread([&]() { try { proc(t); // Remark: if the following code is reached, we @@ -230,7 +231,8 @@ static void tst5() { } }); std::this_thread::sleep_for(dura); - proc.interrupt(); + while (!thread.request_interrupt()) { + } thread.join(); #endif } diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp index f41c232b8..6316b8952 100644 --- a/src/tests/kernel/type_checker.cpp +++ b/src/tests/kernel/type_checker.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "util/test.h" #include "util/trace.h" #include "util/exception.h" +#include "util/interrupt.h" #include "kernel/type_checker.h" #include "kernel/environment.h" #include "kernel/abstract.h" @@ -227,7 +228,7 @@ static void tst12() { env.add_var("a", Int); type_checker checker(env); std::chrono::milliseconds dura(100); - std::thread thread([&]() { + interruptible_thread thread([&]() { try { std::cout << checker.infer_type(t) << "\n"; // Remark: if the following code is reached, we @@ -238,7 +239,8 @@ static void tst12() { } }); std::this_thread::sleep_for(dura); - checker.interrupt(); + while (!thread.request_interrupt()) { + } thread.join(); #endif } diff --git a/src/tests/library/formatter.cpp b/src/tests/library/formatter.cpp index 1f6b9a57a..6dd87cdd6 100644 --- a/src/tests/library/formatter.cpp +++ b/src/tests/library/formatter.cpp @@ -39,8 +39,6 @@ static void tst1() { check(fmt(ctx), "[x : f a; y : f x (N -> N); z : N := y == x]"); check(fmt(ctx, f(Var(0), Var(2))), "f z x"); check(fmt(ctx, f(Var(0), Var(2)), true), "[x : f a; y : f x (N -> N); z : N := y == x] |- f z x"); - fmt.set_interrupt(true); - fmt.set_interrupt(false); } int main() { diff --git a/src/util/interrupt.cpp b/src/util/interrupt.cpp index 98a655cac..ff40ab125 100644 --- a/src/util/interrupt.cpp +++ b/src/util/interrupt.cpp @@ -18,12 +18,12 @@ void reset_interrupt() { g_interrupt.store(false); } -bool interrupted() { +bool interrupt_requested() { return g_interrupt.load(); } -void check_interrupt() { - if (interrupted()) +void check_interrupted() { + if (interrupt_requested()) throw interrupted(); } diff --git a/src/util/interrupt.h b/src/util/interrupt.h index 7f9cddb1e..c56bc6bec 100644 --- a/src/util/interrupt.h +++ b/src/util/interrupt.h @@ -22,12 +22,12 @@ void reset_interrupt(); /** \brief Return true iff the current thread was marked for interruption. */ -bool interrupted(); +bool interrupt_requested(); /** - \brief Throw an interrupt exception if the (interrupt) flag is set. + \brief Throw an interrupted exception if the (interrupt) flag is set. */ -void check_interrupt(); +void check_interrupted(); /** \brief Thread that provides a method for setting its interrupt flag.