feat(frontends/lean/elaborator): add "noncomputable theory" command, display "noncomputable" when printing definitions

When the command "noncomputable theory" is used, Lean will not sign an
error when a noncomputable definition is not marked as noncomputable

library/data/real/default.lean

@@ -3,4 +3,4 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Robert Y. Lewis
 -/
-import .basic .order
+import .basic .order .division .complete

library/data/real/division.lean

@@ -678,4 +678,6 @@ section migrate_algebra
       divide → divide, max → max, min → min
 end migrate_algebra
 
+infix / := divide
+
 end real

src/emacs/lean-syntax.el

@@ -10,7 +10,7 @@
 (defconst lean-keywords
   '("import" "prelude" "tactic_hint" "protected" "private" "noncomputable" "definition" "renaming"
     "hiding" "exposing" "parameter" "parameters" "begin" "begin+" "proof" "qed" "conjecture" "constant" "constants"
-    "hypothesis" "lemma" "corollary" "variable" "variables" "premise" "premises"
+    "hypothesis" "lemma" "corollary" "variable" "variables" "premise" "premises" "theory"
     "print" "theorem" "example" "abbreviation" "abstract"
     "open" "as" "export" "override" "axiom" "axioms" "inductive" "with" "structure" "record" "universe" "universes"
     "alias" "help" "environment" "options" "precedence" "reserve"

src/frontends/lean/builtin_cmds.cpp

@@ -25,6 +25,7 @@ Author: Leonardo de Moura
 #include "library/reducible.h"
 #include "library/normalize.h"
 #include "library/print.h"
+#include "library/noncomputable.h"
 #include "library/class.h"
 #include "library/flycheck.h"
 #include "library/abbreviation.h"
@@ -313,6 +314,8 @@ static void print_recursor_info(parser & p) {
 
 bool print_constant(parser & p, char const * kind, declaration const & d, bool is_def = false) {
     io_state_stream out = p.regular_stream();
+    if (d.is_definition() && is_marked_noncomputable(p.env(), d.get_name()))
+        out << "noncomputable ";
     if (is_protected(p.env(), d.get_name()))
         out << "protected ";
     out << kind << " " << d.get_name();

src/frontends/lean/decl_cmds.cpp

@@ -866,19 +866,21 @@ class definition_cmd_fn {
 
     void register_decl(name const & n, name const & real_n, expr const & type) {
         if (m_kind != Example) {
-            if (!m_is_noncomputable && is_marked_noncomputable(m_env, real_n)) {
+            if (!m_p.ignore_noncomputable()) {
-                auto reason = get_noncomputable_reason(m_env, real_n);
+                if (!m_is_noncomputable && is_marked_noncomputable(m_env, real_n)) {
-                lean_assert(reason);
+                    auto reason = get_noncomputable_reason(m_env, real_n);
-                if (m_p.in_theorem_queue(*reason)) {
+                    lean_assert(reason);
-                    throw exception(sstream() << "definition '" << n << "' was marked as noncomputable because '" << *reason
+                    if (m_p.in_theorem_queue(*reason)) {
-                                    << "' is still in theorem queue (solution: use command 'reveal " << *reason << "'");
+                        throw exception(sstream() << "definition '" << n << "' was marked as noncomputable because '" << *reason
-                } else {
+                                        << "' is still in theorem queue (solution: use command 'reveal " << *reason << "'");
-                    throw exception(sstream() << "definition '" << n
+                    } else {
-                                    << "' is noncomputable, it depends on '" << *reason << "'");
+                        throw exception(sstream() << "definition '" << n
+                                        << "' is noncomputable, it depends on '" << *reason << "'");
+                    }
+                }
+                if (m_is_noncomputable && !is_marked_noncomputable(m_env, real_n)) {
+                    throw exception(sstream() << "definition '" << n << "' was incorrectly marked as noncomputable");
                 }
-            }
-            if (m_is_noncomputable && !is_marked_noncomputable(m_env, real_n)) {
-                throw exception(sstream() << "definition '" << n << "' was incorrectly marked as noncomputable");
             }
             // TODO(Leo): register aux_decls
             if (!m_is_private)
@@ -1176,28 +1178,34 @@ static environment protected_definition_cmd(parser & p) {
     }
 }
 static environment noncomputable_cmd(parser & p) {
-    bool is_private   = false;
+    if (p.curr_is_token_or_id(get_theory_tk())) {
-    bool is_protected = false;
-    if (p.curr_is_token(get_private_tk())) {
-        is_private = true;
         p.next();
-    } else if (p.curr_is_token(get_protected_tk())) {
+        p.set_ignore_noncomputable();
-        is_protected = true;
+        return p.env();
-        p.next();
-    }
-    def_cmd_kind kind = Definition;
-    if (p.curr_is_token_or_id(get_definition_tk())) {
-        p.next();
-    } else if (p.curr_is_token_or_id(get_abbreviation_tk())) {
-        p.next();
-        kind = Abbreviation;
-    } else if (p.curr_is_token_or_id(get_theorem_tk())) {
-        p.next();
-        kind       = Theorem;
     } else {
-        throw parser_error("invalid 'noncomputable' definition/theorem, 'definition' or 'theorem' expected", p.pos());
+        bool is_private   = false;
+        bool is_protected = false;
+        if (p.curr_is_token(get_private_tk())) {
+            is_private = true;
+            p.next();
+        } else if (p.curr_is_token(get_protected_tk())) {
+            is_protected = true;
+            p.next();
+        }
+        def_cmd_kind kind = Definition;
+        if (p.curr_is_token_or_id(get_definition_tk())) {
+            p.next();
+        } else if (p.curr_is_token_or_id(get_abbreviation_tk())) {
+            p.next();
+            kind = Abbreviation;
+        } else if (p.curr_is_token_or_id(get_theorem_tk())) {
+            p.next();
+            kind       = Theorem;
+        } else {
+            throw parser_error("invalid 'noncomputable' definition/theorem, 'definition' or 'theorem' expected", p.pos());
+        }
+        return definition_cmd_core(p, kind, is_private, is_protected, true);
     }
-    return definition_cmd_core(p, kind, is_private, is_protected, true);
 }
 
 static environment include_cmd_core(parser & p, bool include) {

src/frontends/lean/parser.cpp

@@ -126,6 +126,7 @@ parser::parser(environment const & env, io_state const & ios,
     m_snapshot_vector(sv), m_info_manager(im), m_cache(nullptr), m_index(nullptr) {
     m_local_decls_size_at_beg_cmd = 0;
     m_in_backtick = false;
+    m_ignore_noncomputable = false;
     m_profile     = ios.get_options().get_bool("profile", false);
     init_stop_at(ios.get_options());
     if (num_threads > 1 && m_profile)
@@ -1942,7 +1943,7 @@ void parser::add_delayed_theorem(certified_declaration const & cd) {
 void parser::replace_theorem(certified_declaration const & thm) {
     m_env = m_env.replace(thm);
     name const & thm_name = thm.get_declaration().get_name();
-    if (!check_computable(m_env, thm_name)) {
+    if (!m_ignore_noncomputable && !check_computable(m_env, thm_name)) {
         throw exception(sstream() << "declaration '" << thm_name
                         << "' was marked as a theorem, but it is a noncomputable definition");
     }

src/frontends/lean/parser.h

@@ -151,6 +151,10 @@ class parser {
     bool                   m_stop_at; // if true, then parser stops execution after the given line and column is reached
     unsigned               m_stop_at_line;
 
+    // If the following flag is true we do not raise error messages
+    // noncomputable definitions not tagged as noncomputable.
+    bool                   m_ignore_noncomputable;
+
     void display_warning_pos(unsigned line, unsigned pos);
     void display_error_pos(unsigned line, unsigned pos);
     void display_error_pos(pos_info p);
@@ -264,6 +268,9 @@ public:
            info_manager * im = nullptr, keep_theorem_mode tmode = keep_theorem_mode::All);
     ~parser();
 
+    bool ignore_noncomputable() const { return m_ignore_noncomputable; }
+    void set_ignore_noncomputable() { m_ignore_noncomputable = true; }
+
     unsigned curr_expr_lbp() const { return curr_lbp_core(false); }
     unsigned curr_tactic_lbp() const { return curr_lbp_core(true); }
 

src/frontends/lean/tokens.cpp

@@ -153,6 +153,7 @@ static name const * g_metaclasses_tk = nullptr;
 static name const * g_inductive_tk = nullptr;
 static name const * g_this_tk = nullptr;
 static name const * g_noncomputable_tk = nullptr;
+static name const * g_theory_tk = nullptr;
 void initialize_tokens() {
     g_period_tk = new name{"."};
     g_placeholder_tk = new name{"_"};
@@ -304,6 +305,7 @@ void initialize_tokens() {
     g_inductive_tk = new name{"inductive"};
     g_this_tk = new name{"this"};
     g_noncomputable_tk = new name{"noncomputable"};
+    g_theory_tk = new name{"theory"};
 }
 void finalize_tokens() {
     delete g_period_tk;
@@ -456,6 +458,7 @@ void finalize_tokens() {
     delete g_inductive_tk;
     delete g_this_tk;
     delete g_noncomputable_tk;
+    delete g_theory_tk;
 }
 name const & get_period_tk() { return *g_period_tk; }
 name const & get_placeholder_tk() { return *g_placeholder_tk; }
@@ -607,4 +610,5 @@ name const & get_metaclasses_tk() { return *g_metaclasses_tk; }
 name const & get_inductive_tk() { return *g_inductive_tk; }
 name const & get_this_tk() { return *g_this_tk; }
 name const & get_noncomputable_tk() { return *g_noncomputable_tk; }
+name const & get_theory_tk() { return *g_theory_tk; }
 }

src/frontends/lean/tokens.h

@@ -155,4 +155,5 @@ name const & get_metaclasses_tk();
 name const & get_inductive_tk();
 name const & get_this_tk();
 name const & get_noncomputable_tk();
+name const & get_theory_tk();
 }

src/frontends/lean/tokens.txt

@@ -148,3 +148,4 @@ metaclasses  metaclasses
 inductive    inductive
 this         this
 noncomputable noncomputable
+theory       theory

tests/lean/noncomp_theory.lean

@@ -0,0 +1,20 @@
+import data.real
+open real
+
+definition f (a b : real) := (a + a) / b -- ERROR f is noncomputable
+
+noncomputable definition f (a b : real) := (a + a) / b -- ERROR f is noncomputable
+
+noncomputable theory
+
+definition g (a b : real) := (a + a) / b
+
+definition h (a b : real) := (a - a) / b
+
+definition f₂ (a b : real) := (a * a) / b
+
+definition r (a : nat) := a
+
+print g -- g is still marked as noncomputable
+
+print r

tests/lean/noncomp_theory.lean.expected.out

@@ -0,0 +1,5 @@
+noncomp_theory.lean:4:0: error: definition 'f' is noncomputable, it depends on 'real.divide'
+noncomputable definition g : ℝ → ℝ → ℝ :=
+λ (a : ℝ), divide (a + a)
+definition r : ℕ → ℕ :=
+λ (a : ℕ), a