From e68007a72782f376218d043ff338859b6ddf2ac8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 20 Oct 2014 17:10:16 -0700
Subject: [PATCH] fix(frontends/lean/builtin_tactics): adjust tactics
 precedence

---
 library/tools/tactic.lean              | 13 ++++---------
 src/frontends/lean/builtin_tactics.cpp |  4 +++-
 tests/lean/run/beginend2.lean          |  7 +++----
 tests/lean/run/tactic28.lean           |  2 +-
 4 files changed, 11 insertions(+), 15 deletions(-)

diff --git a/library/tools/tactic.lean b/library/tools/tactic.lean
index 4bdf8e102..251f9b60d 100644
--- a/library/tools/tactic.lean
+++ b/library/tools/tactic.lean
@@ -39,15 +39,10 @@ opaque definition beta        : tactic := builtin
 opaque definition unfold      {B : Type} (b : B) : tactic := builtin
 opaque definition exact       {B : Type} (b : B) : tactic := builtin
 opaque definition trace       (s : string) : tactic := builtin
-precedence `;`:200
-infixl ; := and_then
--- [ t_1 | ... | t_n ] notation
-notation `[` h:100 `|` r:(foldl 100 `|` (e r, or_else r e) h) `]` := r
--- [ t_1 || ... || t_n ] notation
-notation `[` h:100 `||` r:(foldl 100 `||` (e r, par r e) h) `]` := r
-definition try         (t : tactic) : tactic := [ t | id ]
-notation `?` t:max     := try t
-definition repeat1     (t : tactic) : tactic := t ; !t
+infixl `;`:15 := and_then
+notation `[` h:10 `|`:10 r:(foldl 10 `|` (e r, or_else r e) h) `]` := r
+definition try         (t : tactic) : tactic := [t | id]
+definition repeat1     (t : tactic) : tactic := t ; repeat t
 definition focus       (t : tactic) : tactic := focus_at t 0
 definition determ      (t : tactic) : tactic := at_most t 1
 
diff --git a/src/frontends/lean/builtin_tactics.cpp b/src/frontends/lean/builtin_tactics.cpp
index 837c40d96..fb962e8bc 100644
--- a/src/frontends/lean/builtin_tactics.cpp
+++ b/src/frontends/lean/builtin_tactics.cpp
@@ -10,13 +10,15 @@ Author: Leonardo de Moura
 #include "frontends/lean/parser.h"
 #include "frontends/lean/parse_table.h"
 
+#define LEAN_APPLY_RBP 16 // it should be bigger than `;` (and_then) precedence
+
 namespace lean {
 using notation::transition;
 using notation::mk_ext_action;
 
 static expr parse_apply(parser & p, unsigned, expr const *, pos_info const & pos) {
     parser::no_undef_id_error_scope scope(p);
-    expr e = p.parse_expr(std::numeric_limits<unsigned>::max());
+    expr e = p.parse_expr(LEAN_APPLY_RBP);
     return p.save_pos(mk_apply_tactic_macro(e), pos);
 }
 
diff --git a/tests/lean/run/beginend2.lean b/tests/lean/run/beginend2.lean
index 9febd3358..fdd32ed1d 100644
--- a/tests/lean/run/beginend2.lean
+++ b/tests/lean/run/beginend2.lean
@@ -6,8 +6,7 @@ open path (induction_on)
 definition concat_whisker2 {A} {x y z : A} (p p' : x ≈ y) (q q' : y ≈ z) (a : p ≈ p') (b : q ≈ q') :
   (whiskerR a q) @ (whiskerL p' b) ≈ (whiskerL p b) @ (whiskerR a q') :=
 begin
-  apply (induction_on b),
-  apply (induction_on a),
-  apply ((concat_1p _)^),
+  apply induction_on b,
+  apply induction_on a,
+  apply (concat_1p _)^,
 end
-exit
diff --git a/tests/lean/run/tactic28.lean b/tests/lean/run/tactic28.lean
index 669722659..a68d58e77 100644
--- a/tests/lean/run/tactic28.lean
+++ b/tests/lean/run/tactic28.lean
@@ -12,7 +12,7 @@ theorem inl_inhabited {A : Type} (B : Type) (H : inhabited A) : inhabited (sum A
 theorem inr_inhabited (A : Type) {B : Type} (H : inhabited B) : inhabited (sum A B)
 := inhabited.destruct H (λ b, inhabited.mk (sum.inr A b))
 
-infixl `..`:100 := append
+infixl `..`:10 := append
 
 definition my_tac := repeat (trace "iteration"; state;
                               (  apply @inl_inhabited; trace "used inl"