From 267545ca0c9cd34602ee3a8de0567b1ba6536c69 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 13 Jul 2015 19:13:41 -0400 Subject: [PATCH] feat(frontends/lean): parse 'with_options' tactical see issue #492 --- hott/init/tactic.hlean | 7 +-- library/init/tactic.lean | 5 +- src/emacs/lean-syntax.el | 2 +- src/frontends/lean/CMakeLists.txt | 2 +- src/frontends/lean/builtin_cmds.cpp | 18 ++----- src/frontends/lean/builtin_tactics.cpp | 22 ++++++--- .../lean/parse_with_options_tactic.cpp | 49 +++++++++++++++++++ .../lean/parse_with_options_tactic.h | 13 +++++ src/frontends/lean/token_table.cpp | 2 +- src/frontends/lean/util.cpp | 19 +++++++ src/frontends/lean/util.h | 3 ++ tests/lean/with_options.lean | 15 ++++++ tests/lean/with_options.lean.expected.out | 37 ++++++++++++++ 13 files changed, 163 insertions(+), 31 deletions(-) create mode 100644 src/frontends/lean/parse_with_options_tactic.cpp create mode 100644 src/frontends/lean/parse_with_options_tactic.h create mode 100644 tests/lean/with_options.lean create mode 100644 tests/lean/with_options.lean.expected.out diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index 6cf2a58d0..e7d4db9a1 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -94,14 +94,15 @@ definition krewrite_tac (e : expr_list) : tactic := builtin -- simp_tac is just a marker for the builtin 'simp' notation -- used to create instances of this tactic. -- Arguments: --- - d : bool.tt if top-down rewrite strategy --- - a : bool.tt if assumptions should be used -- - e : additional rewrites to be considered -- - n : add rewrites from the give namespaces -- - x : exclude the give global rewrites -- - t : tactic for discharging conditions -- - l : location -definition simp_tac (d a : bool) (e : expr_list) (n : identifier_list) (x : identifier_list) (t : option tactic) (l : expr) : tactic := builtin +definition simp_tac (e : expr_list) (n : identifier_list) (x : identifier_list) (t : option tactic) (l : expr) : tactic := builtin + +-- with_options_tac is just a marker for the builtin 'with_options' notation +definition with_options_tac (o : expr) (t : tactic) : tactic := builtin definition cases (h : expr) (ids : opt_identifier_list) : tactic := builtin diff --git a/library/init/tactic.lean b/library/init/tactic.lean index 389a7fffa..6539d9f45 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -94,8 +94,6 @@ definition krewrite_tac (e : expr_list) : tactic := builtin -- simp_tac is just a marker for the builtin 'simp' notation -- used to create instances of this tactic. -- Arguments: --- - d : bool.tt if top-down rewrite strategy --- - a : bool.tt if assumptions should be used -- - e : additional rewrites to be considered -- - n : add rewrites from the give namespaces -- - x : exclude the give global rewrites @@ -103,6 +101,9 @@ definition krewrite_tac (e : expr_list) : tactic := builtin -- - l : location definition simp_tac (d a : bool) (e : expr_list) (n : identifier_list) (x : identifier_list) (t : option tactic) (l : expr) : tactic := builtin +-- with_options_tac is just a marker for the builtin 'with_options' notation +definition with_options_tac (o : expr) (t : tactic) : tactic := builtin + definition cases (h : expr) (ids : opt_identifier_list) : tactic := builtin definition induction (h : expr) (rec : using_expr) (ids : opt_identifier_list) : tactic := builtin diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index ee42d8c40..c5eae4ab8 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -141,7 +141,7 @@ "xrewrite" "krewrite" "esimp" "unfold" "change" "check_expr" "contradiction" "exfalso" "split" "existsi" "constructor" "fconstructor" "left" "right" "injection" "congruence" "reflexivity" "symmetry" "transitivity" "state" "induction" "induction_using" - "substvars" "now")) + "substvars" "now" "with_options")) word-end) (1 'font-lock-constant-face)) ;; Types diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index d7e2d49df..a18a53b25 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -9,6 +9,6 @@ coercion_elaborator.cpp info_tactic.cpp init_module.cpp elaborator_context.cpp calc_proof_elaborator.cpp parse_tactic_location.cpp parse_rewrite_tactic.cpp builtin_tactics.cpp type_util.cpp elaborator_exception.cpp migrate_cmd.cpp local_ref_info.cpp -obtain_expr.cpp decl_attributes.cpp nested_declaration.cpp) +obtain_expr.cpp decl_attributes.cpp nested_declaration.cpp parse_with_options_tactic.cpp) target_link_libraries(lean_frontend ${LEAN_LIBS}) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 34fa28afb..0dbbfce8d 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -630,21 +630,9 @@ environment exit_cmd(parser & p) { } environment set_option_cmd(parser & p) { - auto id_pos = p.pos(); - name id = p.check_id_next("invalid set option, identifier (i.e., option name) expected"); - auto decl_it = get_option_declarations().find(id); - if (decl_it == get_option_declarations().end()) { - // add "lean" prefix - name lean_id = name("lean") + id; - decl_it = get_option_declarations().find(lean_id); - if (decl_it == get_option_declarations().end()) { - throw parser_error(sstream() << "unknown option '" << id - << "', type 'help options.' for list of available options", id_pos); - } else { - id = lean_id; - } - } - option_kind k = decl_it->second.kind(); + auto id_kind = parse_option_name(p, "invalid set option, identifier (i.e., option name) expected"); + name id = id_kind.first; + option_kind k = id_kind.second; if (k == BoolOption) { if (p.curr_is_token_or_id(get_true_tk())) p.set_option(id, true); diff --git a/src/frontends/lean/builtin_tactics.cpp b/src/frontends/lean/builtin_tactics.cpp index b652a9cb6..9359f43d2 100644 --- a/src/frontends/lean/builtin_tactics.cpp +++ b/src/frontends/lean/builtin_tactics.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "frontends/lean/tokens.h" #include "frontends/lean/parser.h" #include "frontends/lean/parse_rewrite_tactic.h" +#include "frontends/lean/parse_with_options_tactic.h" namespace lean { namespace notation { @@ -47,6 +48,10 @@ static expr parse_let_tactic(parser & p, unsigned, expr const *, pos_info const return p.save_pos(mk_let_tactic_expr(id, value), pos); } +static expr parse_with_options_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) { + return p.save_pos(parse_with_options_tactic(p), pos); +} + static expr parse_generalize_tactic(parser & p, unsigned, expr const *, pos_info const & pos) { expr e = p.parse_tactic_expr_arg(); name id; @@ -69,14 +74,15 @@ parse_table init_tactic_nud_table() { expr x0 = mk_var(0); parse_table r; r = r.add({transition("(", Expr), transition(")", mk_ext_action(parse_rparen))}, x0); - r = r.add({transition("rewrite", mk_ext_action(parse_rewrite_tactic_expr))}, x0); - r = r.add({transition("krewrite", mk_ext_action(parse_krewrite_tactic_expr))}, x0); - r = r.add({transition("xrewrite", mk_ext_action(parse_xrewrite_tactic_expr))}, x0); - r = r.add({transition("esimp", mk_ext_action(parse_esimp_tactic_expr))}, x0); - r = r.add({transition("generalize", mk_ext_action(parse_generalize_tactic))}, x0); - r = r.add({transition("unfold", mk_ext_action(parse_unfold_tactic_expr))}, x0); - r = r.add({transition("fold", mk_ext_action(parse_fold_tactic_expr))}, x0); - r = r.add({transition("let", mk_ext_action(parse_let_tactic))}, x0); + r = r.add({transition("rewrite", mk_ext_action(parse_rewrite_tactic_expr))}, x0); + r = r.add({transition("krewrite", mk_ext_action(parse_krewrite_tactic_expr))}, x0); + r = r.add({transition("xrewrite", mk_ext_action(parse_xrewrite_tactic_expr))}, x0); + r = r.add({transition("esimp", mk_ext_action(parse_esimp_tactic_expr))}, x0); + r = r.add({transition("generalize", mk_ext_action(parse_generalize_tactic))}, x0); + r = r.add({transition("unfold", mk_ext_action(parse_unfold_tactic_expr))}, x0); + r = r.add({transition("fold", mk_ext_action(parse_fold_tactic_expr))}, x0); + r = r.add({transition("let", mk_ext_action(parse_let_tactic))}, x0); + r = r.add({transition("with_options", mk_ext_action(parse_with_options_tactic_expr))}, x0); return r; } diff --git a/src/frontends/lean/parse_with_options_tactic.cpp b/src/frontends/lean/parse_with_options_tactic.cpp new file mode 100644 index 000000000..e5b0dc40d --- /dev/null +++ b/src/frontends/lean/parse_with_options_tactic.cpp @@ -0,0 +1,49 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "util/sexpr/option_declarations.h" +#include "library/tactic/with_options_tactic.h" +#include "frontends/lean/parser.h" +#include "frontends/lean/tokens.h" +#include "frontends/lean/util.h" + +namespace lean { +expr parse_with_options_tactic(parser & p) { + options o; + p.check_token_next(get_lbracket_tk(), "invalid 'with_options' tactical, '[' expected"); + while (true) { + auto id_kind = parse_option_name(p, "invalid 'with_options' tactical, identifier (i.e., option name) expected"); + name id = id_kind.first; + option_kind k = id_kind.second; + if (k == BoolOption) { + if (p.curr_is_token_or_id(get_true_tk())) + o = o.update(id, true); + else if (p.curr_is_token_or_id(get_false_tk())) + o = o.update(id, false); + else + throw parser_error("invalid Boolean option value, 'true' or 'false' expected", p.pos()); + p.next(); + } else if (k == StringOption) { + if (!p.curr_is_string()) + throw parser_error("invalid option value, given option is not a string", p.pos()); + o = o.update(id, p.get_str_val()); + p.next(); + } else if (k == DoubleOption) { + o = o.update(id, p.parse_double()); + } else if (k == UnsignedOption || k == IntOption) { + o = o.update(id, p.parse_small_nat()); + } else { + throw parser_error("invalid option value, 'true', 'false', string, integer or decimal value expected", p.pos()); + } + if (!p.curr_is_token(get_comma_tk())) + break; + p.next(); + } + p.check_token_next(get_rbracket_tk(), "invalid 'with_options' tactical, ']' expected"); + expr t = p.parse_tactic(get_max_prec()); + return mk_with_options_tactic_expr(o, t); +} +} diff --git a/src/frontends/lean/parse_with_options_tactic.h b/src/frontends/lean/parse_with_options_tactic.h new file mode 100644 index 000000000..b3b7f765a --- /dev/null +++ b/src/frontends/lean/parse_with_options_tactic.h @@ -0,0 +1,13 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "kernel/expr.h" + +namespace lean { +class parser; +expr parse_with_options_tactic(parser & p); +} diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 29b512c3b..fefde9c92 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -95,7 +95,7 @@ void init_token_table(token_table & t) { {"{|", g_max_prec}, {"|}", 0}, {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0}, {"using", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0}, {"with", 0}, {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {"xrewrite", 0}, {"krewrite", 0}, - {"esimp", 0}, {"fold", 0}, {"unfold", 0}, + {"esimp", 0}, {"fold", 0}, {"unfold", 0}, {"with_options", 0}, {"generalize", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", 0}, {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"begin+", g_max_prec}, {"abstract", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec}, diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index 694ac24c6..1677d559f 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include #include "util/sstream.h" +#include "util/sexpr/option_declarations.h" #include "kernel/abstract.h" #include "kernel/instantiate.h" #include "kernel/replace_fn.h" @@ -496,4 +497,22 @@ optional parse_priority(parser & p) { return optional(); } } + +pair parse_option_name(parser & p, char const * error_msg) { + auto id_pos = p.pos(); + name id = p.check_id_next(error_msg); + auto decl_it = get_option_declarations().find(id); + if (decl_it == get_option_declarations().end()) { + // add "lean" prefix + name lean_id = name("lean") + id; + decl_it = get_option_declarations().find(lean_id); + if (decl_it == get_option_declarations().end()) { + throw parser_error(sstream() << "unknown option '" << id + << "', type 'help options.' for list of available options", id_pos); + } else { + id = lean_id; + } + } + return mk_pair(id, decl_it->second.kind()); +} } diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h index a19f55274..b4170f044 100644 --- a/src/frontends/lean/util.h +++ b/src/frontends/lean/util.h @@ -112,4 +112,7 @@ expr postprocess(environment const & env, expr const & e); /** \brief Parse `[priority ]`. Return none if current token is not `[priority` */ optional parse_priority(parser & p); + +/** \brief Parse option name */ +pair parse_option_name(parser & p, char const * error_msg); } diff --git a/tests/lean/with_options.lean b/tests/lean/with_options.lean new file mode 100644 index 000000000..7b6bbb380 --- /dev/null +++ b/tests/lean/with_options.lean @@ -0,0 +1,15 @@ +example {A : Type} (a b c : A) : a = b → b = c → a = c := +begin + intro h₁ h₂, + with_options [pp.implicit true, pp.notation false] state; state, + with_options [pp.all true, pp.max_depth 1] state, + with_options [pp.notation false] state, + with_options [pp.notation false] (state; state), + substvars +end + +example {A : Type} (a b c : A) : a = b → b = c → a = c := +begin + intros, + with_options [] id, -- error +end diff --git a/tests/lean/with_options.lean.expected.out b/tests/lean/with_options.lean.expected.out new file mode 100644 index 000000000..d1badbeba --- /dev/null +++ b/tests/lean/with_options.lean.expected.out @@ -0,0 +1,37 @@ +with_options.lean:4:53: proof state +A : Type, +a b c : A, +h₁ : @eq A a b, +h₂ : @eq A b c +⊢ @eq A a c +with_options.lean:4:60: proof state +A : Type, +a b c : A, +h₁ : a = b, +h₂ : b = c +⊢ a = c +with_options.lean:5:45: proof state +A : Type.{l_1}, +a b c : A, +h₁ : … b, +h₂ : … c +⊢ … c +with_options.lean:6:35: proof state +A : Type, +a b c : A, +h₁ : eq a b, +h₂ : eq b c +⊢ eq a c +with_options.lean:7:36: proof state +A : Type, +a b c : A, +h₁ : eq a b, +h₂ : eq b c +⊢ eq a c +with_options.lean:7:43: proof state +A : Type, +a b c : A, +h₁ : eq a b, +h₂ : eq b c +⊢ eq a c +with_options.lean:14:16: error: invalid 'with_options' tactical, identifier (i.e., option name) expected