Add Ctrl-C support for interrupting Lean shell.

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

src/frontends/lean/lean_frontend.cpp

@@ -163,6 +163,11 @@ struct frontend::imp {
     void add_mixfixr(unsigned sz, name const * opns, unsigned p, expr const & d) { add_op(mixfixr(sz, opns, p), d, true);  }
     void add_mixfixc(unsigned sz, name const * opns, unsigned p, expr const & d) { add_op(mixfixc(sz, opns, p), d, false); }
 
+    void set_interrupt(bool flag) {
+        m_env.set_interrupt(flag);
+        m_state.set_interrupt(flag);
+    }
+
     imp(frontend & fe):
         m_num_children(0) {
     }
@@ -235,4 +240,6 @@ state & frontend::get_state_core() { return m_imp->m_state; }
 void frontend::set_options(options const & opts) { return m_imp->m_state.set_options(opts); }
 void frontend::set_regular_channel(std::shared_ptr<output_channel> const & out) { return m_imp->m_state.set_regular_channel(out); }
 void frontend::set_diagnostic_channel(std::shared_ptr<output_channel> const & out) { return m_imp->m_state.set_diagnostic_channel(out); }
+
+void frontend::set_interrupt(bool flag) { m_imp->set_interrupt(flag); }
 }

src/frontends/lean/lean_frontend.h

@@ -127,5 +127,13 @@ public:
     void set_regular_channel(std::shared_ptr<output_channel> const & out);
     void set_diagnostic_channel(std::shared_ptr<output_channel> const & out);
     /*@}*/
+
+    /**
+       @name Interrupts.
+    */
+    void set_interrupt(bool flag);
+    void interrupt() { set_interrupt(true); }
+    void reset_interrupt() { set_interrupt(false); }
+    /*@}*/
 };
 }

src/frontends/lean/lean_parser.cpp

@@ -1132,6 +1132,7 @@ class parser_fn {
 
     /** \brief Parse a Lean command. */
     void parse_command() {
+        m_frontend.reset_interrupt();
         m_expr_pos_info.clear();
         m_last_cmd_pos = pos();
         name const & cmd_id = curr_name();
@@ -1234,6 +1235,13 @@ public:
                 } else {
                     display_error(ex);
                 }
+            } catch (interrupted & ex) {
+                if (m_use_exceptions) {
+                    throw;
+                } else {
+                    regular(m_frontend) << "\n!!!Interrupted!!!" << endl;
+                    sync();
+                }
             } catch (exception & ex) {
                 m_found_errors = true;
                 if (m_use_exceptions) {

src/frontends/lean/lean_pp.cpp

@@ -15,6 +15,8 @@ Author: Leonardo de Moura
 #include "free_vars.h"
 #include "context_to_lambda.h"
 #include "options.h"
+#include "interruptable_ptr.h"
+#include "exception.h"
 #include "lean_notation.h"
 #include "lean_pp.h"
 #include "lean_frontend.h"
@@ -126,6 +128,8 @@ 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 {
@@ -700,6 +704,8 @@ class pp_fn {
     }
 
     result pp(expr const & e, unsigned depth, bool main = false) {
+        if (m_interrupted)
+            throw interrupted();
         if (!is_atomic(e) && (m_num_steps > m_max_steps || depth > m_max_depth)) {
             return pp_ellipsis();
         } else {
@@ -789,6 +795,7 @@ public:
     pp_fn(frontend const & fe, options const & opts):
         m_frontend(fe) {
         set_options(opts);
+        m_interrupted = false;
     }
 
     format operator()(expr const & e) {
@@ -801,13 +808,20 @@ public:
         expr T(t);
         return pp_abstraction_core(v, 0, T).first;
     }
+
+    void set_interrupt(bool flag) {
+        m_interrupted = flag;
+    }
 };
 
 class pp_formatter_cell : public formatter_cell {
-    frontend const & m_frontend;
+    frontend const &         m_frontend;
+    interruptable_ptr<pp_fn> m_pp_fn;
 
     format pp(expr const & e, options const & opts) {
-        return pp_fn(m_frontend, opts)(e);
+        pp_fn fn(m_frontend, opts);
+        scoped_set_interruptable_ptr<pp_fn> set(m_pp_fn, &fn);
+        return fn(e);
     }
 
     format pp(context const & c, expr const & e, bool include_e, options const & opts) {
@@ -859,9 +873,10 @@ class pp_formatter_cell : public formatter_cell {
         if (!is_lambda(v) || is_pi(it1)) {
             return pp_definition(kwd, n, t, v, opts);
         } else {
-
             lean_assert(is_lambda(v));
-            format def = pp_fn(m_frontend, opts).pp_definition(v, t);
+            pp_fn fn(m_frontend, opts);
+            scoped_set_interruptable_ptr<pp_fn> set(m_pp_fn, &fn);
+            format def = fn.pp_definition(v, t);
             return format{highlight_command(format(kwd)), space(), format(n), def};
         }
     }
@@ -942,6 +957,10 @@ public:
                       });
         return r;
     }
+
+    virtual void set_interrupt(bool flag) {
+        m_pp_fn.set_interrupt(flag);
+    }
 };
 
 formatter mk_pp_formatter(frontend const & fe) {

src/kernel/environment.cpp

@@ -30,6 +30,7 @@ struct environment::imp {
     // Object management
     std::vector<object>                  m_objects;
     object_dictionary                    m_object_dictionary;
+    type_checker                         m_type_checker;
 
     /**
        \brief Return true iff this environment has children.
@@ -221,9 +222,9 @@ struct environment::imp {
         infer_universe and infer_type expect an environment instead of environment::imp.
     */
     void check_type(name const & n, expr const & t, expr const & v, environment const & env) {
-        infer_universe(t, env);
+        m_type_checker.infer_universe(t);
-        expr v_t = infer_type(v, env);
+        expr v_t = m_type_checker.infer_type(v);
-        if (!is_convertible(t, v_t, env))
+        if (!m_type_checker.is_convertible(t, v_t))
             throw def_type_mismatch_exception(env, n, t, v, v_t);
     }
 
@@ -245,7 +246,7 @@ struct environment::imp {
     */
     void add_definition(name const & n, expr const & v, bool opaque, environment const & env) {
         check_name(n, env);
-        expr v_t = infer_type(v, env);
+        expr v_t = m_type_checker.infer_type(v);
         register_named_object(mk_definition(n, v_t, v, opaque));
     }
 
@@ -300,14 +301,20 @@ struct environment::imp {
         }
     }
 
-    imp():
+    void set_interrupt(bool flag) {
-        m_num_children(0) {
+        m_type_checker.set_interrupt(flag);
+    }
+
+    imp(environment const & env):
+        m_num_children(0),
+        m_type_checker(env) {
         init_uvars();
     }
 
-    explicit imp(std::shared_ptr<imp> const & parent):
+    imp(std::shared_ptr<imp> const & parent, environment const & env):
         m_num_children(0),
-        m_parent(parent) {
+        m_parent(parent),
+        m_type_checker(env) {
         m_parent->inc_children();
     }
 
@@ -318,13 +325,15 @@ struct environment::imp {
 };
 
 environment::environment():
-    m_imp(new imp()) {
+    m_imp(new imp(*this)) {
 }
 
+// used when creating a new child environment
 environment::environment(imp * new_ptr):
     m_imp(new_ptr) {
 }
 
+// used when creating a reference to the parent environment
 environment::environment(std::shared_ptr<imp> const & ptr):
     m_imp(ptr) {
 }
@@ -333,7 +342,7 @@ environment::~environment() {
 }
 
 environment environment::mk_child() const {
-    return environment(new imp(m_imp));
+    return environment(new imp(m_imp, *this));
 }
 
 bool environment::has_children() const {
@@ -404,4 +413,8 @@ object const & environment::get_object(unsigned i, bool local) const {
 void environment::display(std::ostream & out) const {
     m_imp->display(out, *this);
 }
+
+void environment::set_interrupt(bool flag) {
+    m_imp->set_interrupt(flag);
+}
 }

src/kernel/environment.h

@@ -174,5 +174,9 @@ 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); }
 };
 }

src/kernel/normalize.cpp

@@ -66,12 +66,12 @@ value_stack extend(value_stack const & s, svalue const & v) { return cons(v, s);
 class normalizer::imp {
     typedef scoped_map<expr, svalue, expr_hash, expr_eqp> cache;
 
-    environment   m_env;
+    environment const & m_env;
-    context       m_ctx;
+    context             m_ctx;
-    cache         m_cache;
+    cache               m_cache;
-    unsigned      m_max_depth;
+    unsigned            m_max_depth;
-    unsigned      m_depth;
+    unsigned            m_depth;
-    volatile bool m_interrupted;
+    volatile bool       m_interrupted;
 
     /**
         \brief Auxiliary object for saving the current context.

src/kernel/type_check.cpp

@@ -18,10 +18,10 @@ namespace lean {
 class type_checker::imp {
     typedef scoped_map<expr, expr, expr_hash, expr_eqp> cache;
 
-    environment     m_env;
+    environment const & m_env;
-    cache           m_cache;
+    cache               m_cache;
-    normalizer      m_normalizer;
+    normalizer          m_normalizer;
-    volatile bool   m_interrupted;
+    volatile bool       m_interrupted;
 
     expr lookup(context const & c, unsigned i) {
         auto p = lookup_ext(c, i);
@@ -151,8 +151,12 @@ public:
         return r;
     }
 
+    bool is_convertible(expr const & t1, expr const & t2, context const & ctx) {
+        return m_normalizer.is_convertible(t1, t2, ctx);
+    }
+
     void set_interrupt(bool flag) {
-        m_interrupted = true;
+        m_interrupted = flag;
         m_normalizer.set_interrupt(flag);
     }
 
@@ -168,6 +172,9 @@ expr type_checker::infer_type(expr const & e, context const & ctx) { return m_pt
 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); }
+bool type_checker::is_convertible(expr const & t1, expr const & t2, context const & ctx) {
+    return m_ptr->is_convertible(t1, t2, ctx);
+}
 
 expr  infer_type(expr const & e, environment const & env, context const & ctx) {
     return type_checker(env).infer_type(e, ctx);

src/kernel/type_check.h

@@ -21,6 +21,7 @@ public:
     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); }
+    bool is_convertible(expr const & t1, expr const & t2, context const & ctx = context());
 
     void clear();
 

src/library/formatter.h

@@ -34,6 +34,8 @@ 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 flag) {}
 };
 class kernel_exception;
 class formatter {
@@ -48,6 +50,7 @@ public:
     format operator()(environment const & env, options const & opts = options()) { return (*m_cell)(env, opts); }
     /** \brief Pretty print a kernel exception using the this formatter */
     format operator()(kernel_exception const & ex, options const & opts = options());
+    void set_interrupt(bool flag) { m_cell->set_interrupt(flag); }
 };
 
 formatter mk_simple_formatter();

src/library/state.h

@@ -39,6 +39,7 @@ public:
     template<typename T> 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); }
 };
 
 struct regular {

src/shell/lean.cpp

@@ -1,18 +1,33 @@
 #include <iostream>
 #include <fstream>
+#include <signal.h>
 #include "version.h"
 #include "printer.h"
+#include "interruptable_ptr.h"
 #include "lean_parser.h"
 using namespace lean;
 
-int main(int argc, char ** argv) {
+static interruptable_ptr<frontend> g_lean_frontend;
+
+static void on_ctrl_c(int) {
+    g_lean_frontend.set_interrupt(true);
+}
+
+bool lean_shell() {
     std::cout << "Lean (version " << LEAN_VERSION_MAJOR << "." << LEAN_VERSION_MINOR << ")\n";
     std::cout << "Type Ctrl-D to exit or 'Help.' for help."<< std::endl;
     frontend f;
+    scoped_set_interruptable_ptr<frontend> set(g_lean_frontend, &f);
+    signal(SIGINT, on_ctrl_c);
+    return parse_commands_from_stdin(f);
+}
+
+int main(int argc, char ** argv) {
     if (argc == 1) {
-        return parse_commands_from_stdin(f) ? 0 : 1;
+        return lean_shell() ? 0 : 1;
     } else {
         bool ok = true;
+        frontend f;
         for (int i = 1; i < argc; i++) {
             std::ifstream in(argv[i]);
             if (!parse_commands(f, in))

src/util/interruptable_ptr.h

@@ -0,0 +1,60 @@
+/*
+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 <mutex>
+
+namespace lean {
+/**
+    \brief Auxiliary class that wraps a pointer to a type that has a
+    set_interrupt method. The set_interrupt can be invoked from a different
+    execution thread. To prevent race conditions, we use mutex whenever we
+    reset the pointer, or invoke the set_interrupt method.
+
+    The common usage scenario is:
+    1) Thread A creates creates a new object Obj and invokes set(Obj)
+    2) Thread B invokes set_interrupt, which invokes Obj->set_interrupt
+    3) Thread A invokes set(nullptr) before deleting Obj.
+
+    We use the mutex to avoid a race condition in 2&3.
+*/
+template<typename T>
+class interruptable_ptr {
+    T *        m_ptr;
+    std::mutex m_mutex;
+public:
+    interruptable_ptr():m_ptr(nullptr) {}
+
+    T * set(T * ptr) {
+        std::lock_guard<std::mutex> lock(m_mutex);
+        T * old = m_ptr;
+        m_ptr = ptr;
+        return old;
+    }
+
+    void set_interrupt(bool flag) {
+        std::lock_guard<std::mutex> lock(m_mutex);
+        if (m_ptr)
+            m_ptr->set_interrupt(flag);
+    }
+};
+
+/**
+   \brief Auxiliary class for setting/resetting  a interruptable_ptr.
+*/
+template<typename T>
+struct scoped_set_interruptable_ptr {
+    interruptable_ptr<T> & m_ptr;
+    T *                    m_old_p;
+public:
+    scoped_set_interruptable_ptr(interruptable_ptr<T> & ptr, T * p):m_ptr(ptr) {
+        m_old_p = m_ptr.set(p);
+    }
+    ~scoped_set_interruptable_ptr() {
+        m_ptr.set(m_old_p);
+    }
+};
+}