From 645e7483028be2f03f0bd6931db95db7aa9c1602 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 5 Jan 2014 22:53:03 -0800 Subject: [PATCH] feat(frontends/lean): add 'using' command Signed-off-by: Leonardo de Moura --- examples/lean/even.lean | 19 ++++----- src/frontends/lean/parser_cmds.cpp | 57 ++++++++++++++++++++++++++- src/frontends/lean/parser_expr.cpp | 63 ++++++++++++++++-------------- src/frontends/lean/parser_imp.h | 3 ++ 4 files changed, 102 insertions(+), 40 deletions(-) diff --git a/examples/lean/even.lean b/examples/lean/even.lean index c1127afdc..a3c7511d8 100644 --- a/examples/lean/even.lean +++ b/examples/lean/even.lean @@ -1,9 +1,10 @@ -import macros. +import macros +using Nat -- In this example, we prove two simple theorems about even/odd numbers. -- First, we define the predicates even and odd. -definition even (a : Nat) := ∃ b, a = 2*b. -definition odd (a : Nat) := ∃ b, a = 2*b + 1. +definition even (a : Nat) := ∃ b, a = 2*b +definition odd (a : Nat) := ∃ b, a = 2*b + 1 -- Prove that the sum of two even numbers is even. -- @@ -34,7 +35,7 @@ theorem EvenPlusEven {a b : Nat} (H1 : even a) (H2 : even b) : even (a + b) exists::intro (w1 + w2) (calc a + b = 2*w1 + b : { Hw1 } ... = 2*w1 + 2*w2 : { Hw2 } - ... = 2*(w1 + w2) : symm (Nat::distribute 2 w1 w2)). + ... = 2*(w1 + w2) : symm (distribute 2 w1 w2)) -- In the following example, we omit the arguments for Nat::PlusAssoc, Refl and Nat::Distribute. -- Lean can infer them automatically. @@ -53,19 +54,19 @@ theorem OddPlusOne {a : Nat} (H : odd a) : even (a + 1) := obtain (w : Nat) (Hw : a = 2*w + 1), from H, exists::intro (w + 1) (calc a + 1 = 2*w + 1 + 1 : { Hw } - ... = 2*w + (1 + 1) : symm (Nat::plus::assoc _ _ _) + ... = 2*w + (1 + 1) : symm (plus::assoc _ _ _) ... = 2*w + 2*1 : refl _ - ... = 2*(w + 1) : symm (Nat::distribute _ _ _)). + ... = 2*(w + 1) : symm (distribute _ _ _)) -- The following command displays the proof object produced by Lean after -- expanding macros, and infering implicit/missing arguments. -print environment 2. +print environment 2 -- By default, Lean does not display implicit arguments. -- The following command will force it to display them. -set::option pp::implicit true. +set::option pp::implicit true -print environment 2. +print environment 2 -- As an exercise, prove that the sum of two odd numbers is even, -- and other similar theorems. diff --git a/src/frontends/lean/parser_cmds.cpp b/src/frontends/lean/parser_cmds.cpp index 90fa18c35..fa6ee1ebe 100644 --- a/src/frontends/lean/parser_cmds.cpp +++ b/src/frontends/lean/parser_cmds.cpp @@ -51,12 +51,13 @@ static name g_scope_kwd("scope"); static name g_builtin_kwd("builtin"); static name g_namespace_kwd("namespace"); static name g_end_kwd("end"); +static name g_using_kwd("using"); /** \brief Table/List with all builtin command keywords */ static list g_command_keywords = {g_definition_kwd, g_variable_kwd, g_variables_kwd, g_theorem_kwd, g_axiom_kwd, g_universe_kwd, g_eval_kwd, g_check_kwd, g_infix_kwd, g_infixl_kwd, g_infixr_kwd, g_notation_kwd, g_set_option_kwd, g_set_opaque_kwd, g_env_kwd, g_options_kwd, g_import_kwd, g_help_kwd, g_coercion_kwd, g_exit_kwd, g_print_kwd, g_pop_kwd, g_scope_kwd, g_alias_kwd, g_builtin_kwd, - g_namespace_kwd, g_end_kwd}; + g_namespace_kwd, g_end_kwd, g_using_kwd}; // ========================================== list const & parser_imp::get_command_keywords() { @@ -618,7 +619,8 @@ void parser_imp::parse_help() { << " set::opaque [id] [bool] set the given definition as opaque/transparent" << endl << " theorem [id] : [type] := [expr] define a new theorem" << endl << " variable [id] : [type] declare/postulate an element of the given type" << endl - << " universe [id] [level] declare a new universe variable that is >= the given level" << endl; + << " universe [id] [level] declare a new universe variable that is >= the given level" << endl + << " using [id]_1 [id]_2? create an alias for object starting with the prefix [id]_1 using the [id]_2" << endl; #if !defined(LEAN_WINDOWS) regular(m_io_state) << "Type Ctrl-D to exit" << endl; #endif @@ -707,6 +709,7 @@ void parser_imp::parse_scope() { next(); m_scope_kinds.push_back(scope_kind::Scope); reset_env(m_env->mk_child()); + m_using_decls.push(); } void parser_imp::parse_pop() { @@ -719,6 +722,7 @@ void parser_imp::parse_pop() { throw parser_error("main scope cannot be removed", m_last_cmd_pos); m_scope_kinds.pop_back(); reset_env(m_env->parent()); + m_using_decls.pop(); } void parser_imp::parse_namespace() { @@ -726,6 +730,7 @@ void parser_imp::parse_namespace() { name id = check_identifier_next("invalid namespace declaration, identifier expected"); m_scope_kinds.push_back(scope_kind::Namespace); m_namespace_prefixes.push_back(m_namespace_prefixes.back() + id); + m_using_decls.push(); } void parser_imp::parse_end() { @@ -754,6 +759,52 @@ void parser_imp::parse_end() { throw parser_error("invalid end namespace command, there are no open namespaces", m_last_cmd_pos); m_namespace_prefixes.pop_back(); } + m_using_decls.pop(); +} + +static name replace_prefix(name const & n, name const & prefix, name const & new_prefix) { + if (n == prefix) + return new_prefix; + name p = replace_prefix(n.get_prefix(), prefix, new_prefix); + if (n.is_string()) + return name(p, n.get_string()); + else + return name(p, n.get_numeral()); +} + +void parser_imp::parse_using() { + next(); + name prefix = check_identifier_next("invalid using command, identifier expected"); + name new_prefix; + if (curr_is_identifier()) { + new_prefix = curr_name(); + next(); + } + buffer> to_add; + for (auto it = m_env->begin_objects(); it != m_env->end_objects(); ++it) { + if (it->has_type() && it->has_name() && !is_hidden_object(*it) && is_prefix_of(prefix, it->get_name())) { + auto n = replace_prefix(it->get_name(), prefix, new_prefix); + if (!n.is_anonymous()) + to_add.emplace_back(n, mk_constant(it->get_name())); + } + } + for (auto p : to_add) { + auto n = p.first; + if (m_verbose) { + auto it = m_using_decls.find(n); + if (it != m_using_decls.end()) + diagnostic(m_io_state) << "warning: " << n << " will shadow " << it->second << endl; + auto obj = m_env->find_object(n); + if (obj) + diagnostic(m_io_state) << "warning: " << n << " will shadow " << obj->get_name() << endl; + } + m_using_decls.insert(n, p.second); + } + if (m_verbose) + regular(m_io_state) << " Using: " << prefix; + if (new_prefix) + regular(m_io_state) << " as " << new_prefix; + regular(m_io_state) << endl; } /** \brief Parse a Lean command. */ @@ -814,6 +865,8 @@ bool parser_imp::parse_command() { parse_namespace(); } else if (cmd_id == g_end_kwd) { parse_end(); + } else if (cmd_id == g_using_kwd) { + parse_using(); } else if (m_cmd_macros && m_cmd_macros->find(cmd_id) != m_cmd_macros->end()) { parse_cmd_macro(cmd_id, m_last_cmd_pos); } else { diff --git a/src/frontends/lean/parser_expr.cpp b/src/frontends/lean/parser_expr.cpp index d15660334..65e848df8 100644 --- a/src/frontends/lean/parser_expr.cpp +++ b/src/frontends/lean/parser_expr.cpp @@ -247,40 +247,45 @@ expr parser_imp::parse_mixfixc(operator_info const & op) { } expr parser_imp::get_name_ref(name const & id, pos_info const & p, bool implicit_args) { - lean_assert(!m_namespace_prefixes.empty()); - auto it = m_namespace_prefixes.end(); - auto begin = m_namespace_prefixes.begin(); - while (it != begin) { - --it; - name nid = *it + id; - optional obj = m_env->find_object(nid); - if (obj) { - object_kind k = obj->kind(); - if (k == object_kind::Definition || k == object_kind::Postulate || k == object_kind::Builtin) { - if (implicit_args && has_implicit_arguments(m_env, obj->get_name())) { - std::vector const & imp_args = get_implicit_arguments(m_env, obj->get_name()); - buffer args; - pos_info p = pos(); - expr f = (k == object_kind::Builtin) ? obj->get_value() : mk_constant(obj->get_name()); - args.push_back(save(f, p)); - for (unsigned i = 0; i < imp_args.size(); i++) { - if (imp_args[i]) { - args.push_back(save(mk_placeholder(), pos())); - } else { - args.push_back(parse_expr(g_app_precedence)); + auto it = m_using_decls.find(id); + if (it != m_using_decls.end()) { + return it->second; + } else { + lean_assert(!m_namespace_prefixes.empty()); + auto it = m_namespace_prefixes.end(); + auto begin = m_namespace_prefixes.begin(); + while (it != begin) { + --it; + name nid = *it + id; + optional obj = m_env->find_object(nid); + if (obj) { + object_kind k = obj->kind(); + if (k == object_kind::Definition || k == object_kind::Postulate || k == object_kind::Builtin) { + if (implicit_args && has_implicit_arguments(m_env, obj->get_name())) { + std::vector const & imp_args = get_implicit_arguments(m_env, obj->get_name()); + buffer args; + pos_info p = pos(); + expr f = (k == object_kind::Builtin) ? obj->get_value() : mk_constant(obj->get_name()); + args.push_back(save(f, p)); + for (unsigned i = 0; i < imp_args.size(); i++) { + if (imp_args[i]) { + args.push_back(save(mk_placeholder(), pos())); + } else { + args.push_back(parse_expr(g_app_precedence)); + } } + return mk_app(args); + } else if (k == object_kind::Builtin) { + return obj->get_value(); + } else { + return mk_constant(obj->get_name()); } - return mk_app(args); - } else if (k == object_kind::Builtin) { - return obj->get_value(); } else { - return mk_constant(obj->get_name()); + throw parser_error(sstream() << "invalid object reference, object '" << nid << "' is not an expression.", p); } - } else { - throw parser_error(sstream() << "invalid object reference, object '" << nid << "' is not an expression.", p); + } else if (!m_check_identifiers) { + return mk_constant(nid); } - } else if (!m_check_identifiers) { - return mk_constant(nid); } } throw parser_error(sstream() << "unknown identifier '" << id << "'", p); diff --git a/src/frontends/lean/parser_imp.h b/src/frontends/lean/parser_imp.h index 2f22729fb..367c8bc85 100644 --- a/src/frontends/lean/parser_imp.h +++ b/src/frontends/lean/parser_imp.h @@ -55,6 +55,7 @@ class parser_imp { typedef name_map builtins; typedef expr_map expr_pos_info; typedef expr_map tactic_hints; // a mapping from placeholder to tactic + typedef scoped_map using_decls; environment m_env; io_state m_io_state; scanner m_scanner; @@ -72,6 +73,7 @@ class parser_imp { pos_info m_last_cmd_pos; pos_info m_last_script_pos; tactic_hints m_tactic_hints; + using_decls m_using_decls; std::vector m_namespace_prefixes; enum class scope_kind { Scope, Namespace }; std::vector m_scope_kinds; @@ -417,6 +419,7 @@ private: void parse_builtin(); void parse_namespace(); void parse_end(); + void parse_using(); bool parse_command(); /*@}*/