feat(frontends/lean): parse 'with_options' tactical

see issue #492

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
 

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

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

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})

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();
+    auto id_kind = parse_option_name(p, "invalid set option, identifier (i.e., option name) expected");
-    name id = p.check_id_next("invalid set option, identifier (i.e., option name) expected");
+    name id       = id_kind.first;
-    auto decl_it = get_option_declarations().find(id);
+    option_kind k = id_kind.second;
-    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();
     if (k == BoolOption) {
         if (p.curr_is_token_or_id(get_true_tk()))
             p.set_option(id, true);

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("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("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("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("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("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("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("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("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;
 }
 

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);
+}
+}

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);
+}

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},

src/frontends/lean/util.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <algorithm>
 #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<unsigned> parse_priority(parser & p) {
         return optional<unsigned>();
     }
 }
+
+pair<name, option_kind> 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());
+}
 }

src/frontends/lean/util.h

@@ -112,4 +112,7 @@ expr postprocess(environment const & env, expr const & e);
 
 /** \brief Parse `[priority <num>]`. Return none if current token is not `[priority` */
 optional<unsigned> parse_priority(parser & p);
+
+/** \brief Parse option name */
+pair<name, option_kind> parse_option_name(parser & p, char const * error_msg);
 }

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

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