From be61fb056610a5ffae88c6b2ccaf298639f7b56d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 29 Jul 2015 17:54:35 -0700 Subject: [PATCH] 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 | 2 +- library/data/real/division.lean | 2 + src/emacs/lean-syntax.el | 2 +- src/frontends/lean/builtin_cmds.cpp | 3 + src/frontends/lean/decl_cmds.cpp | 70 ++++++++++++--------- src/frontends/lean/parser.cpp | 3 +- src/frontends/lean/parser.h | 7 +++ src/frontends/lean/tokens.cpp | 4 ++ src/frontends/lean/tokens.h | 1 + src/frontends/lean/tokens.txt | 1 + tests/lean/noncomp_theory.lean | 20 ++++++ tests/lean/noncomp_theory.lean.expected.out | 5 ++ 12 files changed, 86 insertions(+), 34 deletions(-) create mode 100644 tests/lean/noncomp_theory.lean create mode 100644 tests/lean/noncomp_theory.lean.expected.out diff --git a/library/data/real/default.lean b/library/data/real/default.lean index 1940618c4..21e4a435f 100644 --- a/library/data/real/default.lean +++ b/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 diff --git a/library/data/real/division.lean b/library/data/real/division.lean index 93b0ac3d7..0de4feab4 100644 --- a/library/data/real/division.lean +++ b/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 diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 111d9b8c8..909c6b2ef 100644 --- a/src/emacs/lean-syntax.el +++ b/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" diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 6e94b47fb..4fe7ebb17 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/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(); diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index b0c57af82..fd4512080 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/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)) { - auto reason = get_noncomputable_reason(m_env, real_n); - lean_assert(reason); - if (m_p.in_theorem_queue(*reason)) { - throw exception(sstream() << "definition '" << n << "' was marked as noncomputable because '" << *reason - << "' is still in theorem queue (solution: use command 'reveal " << *reason << "'"); - } else { - throw exception(sstream() << "definition '" << n - << "' is noncomputable, it depends on '" << *reason << "'"); + if (!m_p.ignore_noncomputable()) { + if (!m_is_noncomputable && is_marked_noncomputable(m_env, real_n)) { + auto reason = get_noncomputable_reason(m_env, real_n); + lean_assert(reason); + if (m_p.in_theorem_queue(*reason)) { + throw exception(sstream() << "definition '" << n << "' was marked as noncomputable because '" << *reason + << "' is still in theorem queue (solution: use command 'reveal " << *reason << "'"); + } else { + 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; - bool is_protected = false; - if (p.curr_is_token(get_private_tk())) { - is_private = true; + if (p.curr_is_token_or_id(get_theory_tk())) { 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; + p.set_ignore_noncomputable(); + return p.env(); } 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) { diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index fb206762f..189f5c951 100644 --- a/src/frontends/lean/parser.cpp +++ b/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"); } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index e6648461b..bd4e5f8b7 100644 --- a/src/frontends/lean/parser.h +++ b/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); } diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index e05fbd198..c212c5d06 100644 --- a/src/frontends/lean/tokens.cpp +++ b/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; } } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index 6ea041b5e..e8d58538a 100644 --- a/src/frontends/lean/tokens.h +++ b/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(); } diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt index f1b4e3aec..0d50302bf 100644 --- a/src/frontends/lean/tokens.txt +++ b/src/frontends/lean/tokens.txt @@ -148,3 +148,4 @@ metaclasses metaclasses inductive inductive this this noncomputable noncomputable +theory theory diff --git a/tests/lean/noncomp_theory.lean b/tests/lean/noncomp_theory.lean new file mode 100644 index 000000000..efdac7d96 --- /dev/null +++ b/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 diff --git a/tests/lean/noncomp_theory.lean.expected.out b/tests/lean/noncomp_theory.lean.expected.out new file mode 100644 index 000000000..4742251fe --- /dev/null +++ b/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