From e971acabb0b68f3e4a7cfd77d5a79a4ab5b43b43 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 27 Jun 2017 18:17:18 -0700
Subject: [PATCH] feat(library/init/meta): handle auto_params and opt_params at
 apply tactic

---
 library/init/meta/tactic.lean          | 50 ++++++++++++++++----------
 src/library/tactic/apply_tactic.cpp    | 23 ------------
 tests/lean/apply_tac.lean              | 28 +++++++++++++++
 tests/lean/apply_tac.lean.expected.out |  1 +
 tests/lean/run/apply_auto_opt.lean     |  2 +-
 5 files changed, 62 insertions(+), 42 deletions(-)

diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 0a6898d09e..9863d414ee 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -363,9 +363,10 @@ structure apply_cfg :=
 (opt_param     := tt)
 /-- Apply the expression `e` to the main goal,
     the unification is performed using the transparency mode in `cfg`.
-    If cfg.approx is `tt`, then fallback to first-order unification, and approximate context during unification.
-    If cfg.all is `tt`, then all unassigned meta-variables are added as new goals.
-    If cfg.use_instances is `tt`, then use type class resolution to instantiate unassigned meta-variables.
+    If `cfg.approx` is `tt`, then fallback to first-order unification, and approximate context during unification.
+    `cfg.new_goals` specifies which unassigned metavariables become new goals, and their order.
+    If `cfg.instances` is `tt`, then use type class resolution to instantiate unassigned meta-variables.
+    The fields `cfg.auto_param` and `cfg.opt_param` are ignored by this tactic (See `tactic.apply`).
     It returns a list of all introduced meta variables, even the assigned ones. -/
 meta constant apply_core (e : expr) (cfg : apply_cfg := {}) : tactic (list expr)
 /- Create a fresh meta universe variable. -/
@@ -810,14 +811,38 @@ meta def done : tactic unit :=
 do n ← num_goals,
    when (n ≠ 0) (fail "done tactic failed, there are unsolved goals")
 
-meta def apply (e : expr) : tactic unit :=
-apply_core e >> return ()
+meta def apply_opt_param : tactic unit :=
+do `(opt_param %%t %%v) ← target,
+   exact v
+
+meta def apply_auto_param : tactic unit :=
+do `(auto_param %%type %%tac_name_expr) ← target,
+   change type,
+   tac_name ← eval_expr name tac_name_expr,
+   tac ← eval_expr (tactic unit) (expr.const tac_name []),
+   tac
+
+meta def has_opt_auto_param (ms : list expr) : tactic bool :=
+ms.mfoldl
+ (λ r m, do type ← infer_type m,
+            return $ r || type.is_napp_of `opt_param 2 || type.is_napp_of `auto_param 2)
+ ff
+
+private meta def try_apply_opt_auto_param (cfg : apply_cfg) (ms : list expr) : tactic unit :=
+when (cfg.auto_param || cfg.opt_param) $
+mwhen (has_opt_auto_param ms) $ do
+  gs ← get_goals,
+  ms.mfor' (λ m, set_goals [m] >> try apply_opt_param >> try apply_auto_param),
+  set_goals gs
+
+meta def apply (e : expr) (cfg : apply_cfg := {}) : tactic unit :=
+apply_core e cfg >>= try_apply_opt_auto_param cfg
 
 meta def fapply (e : expr) : tactic unit :=
-apply_core e {new_goals := new_goals.all} >> return ()
+apply e {new_goals := new_goals.all}
 
 meta def eapply (e : expr) : tactic unit :=
-apply_core e {new_goals := new_goals.non_dep_only} >> return ()
+apply e {new_goals := new_goals.non_dep_only}
 
 /-- Try to solve the main goal using type class resolution. -/
 meta def apply_instance : tactic unit :=
@@ -1044,17 +1069,6 @@ updateex_env $ λe, e.add_inductive n ls p ty is is_meta
 meta def add_meta_definition (n : name) (lvls : list name) (type value : expr) : tactic unit :=
 add_decl (declaration.defn n lvls type value reducibility_hints.abbrev ff)
 
-meta def apply_opt_param : tactic unit :=
-do `(opt_param %%t %%v) ← target,
-   exact v
-
-meta def apply_auto_param : tactic unit :=
-do `(auto_param %%type %%tac_name_expr) ← target,
-   change type,
-   tac_name ← eval_expr name tac_name_expr,
-   tac ← eval_expr (tactic unit) (expr.const tac_name []),
-   tac
-
 meta def rename (curr : name) (new : name) : tactic unit :=
 do h ← get_local curr,
    n ← revert h,
diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp
index e81e3eae0c..f17b33d31b 100644
--- a/src/library/tactic/apply_tactic.cpp
+++ b/src/library/tactic/apply_tactic.cpp
@@ -77,18 +77,6 @@ bool try_instance(type_context & ctx, expr const & meta, tactic_state const & s,
     return true;
 }
 
-bool try_auto_param(type_context & /* ctx */, expr const & /* meta */,
-                    tactic_state const & /* s */, vm_obj * /* out_error_obj */, char const * /* tac_name */) {
-    // TODO(Leo)
-    return true;
-}
-
-bool try_opt_param(type_context & /* ctx */, expr const & /* meta */,
-                   tactic_state const & /* s */, vm_obj * /* out_error_obj */, char const * /* tac_name */) {
-    // TODO(Leo)
-    return true;
-}
-
 /** \brief Given a sequence metas/goals: <tt>(?m_1 ...) (?m_2 ... ) ... (?m_k ...)</tt>,
     we say ?m_i is "redundant" if it occurs in the type of some ?m_j.
     This procedure removes from metas any redundant element. */
@@ -184,17 +172,6 @@ static optional<tactic_state> apply(type_context & ctx, expr e, apply_cfg const
                 return none_tactic_state();
         }
     }
-    /* Synthesize using auto_param and opt_param */
-    if (cfg.m_opt_param || cfg.m_auto_param) {
-        unsigned i = metas.size();
-        while (i > 0) {
-            --i;
-            if (cfg.m_opt_param && !try_opt_param(ctx, metas[i], s, out_error_obj, "apply"))
-                return none_tactic_state();
-            if (cfg.m_auto_param && !try_auto_param(ctx, metas[i], s, out_error_obj, "apply"))
-                return none_tactic_state();
-        }
-    }
     /* Collect unassigned meta-variables */
     buffer<expr> new_goals;
     for (auto m : metas) {
diff --git a/tests/lean/apply_tac.lean b/tests/lean/apply_tac.lean
index e07d2c7653..f991cfc046 100644
--- a/tests/lean/apply_tac.lean
+++ b/tests/lean/apply_tac.lean
@@ -38,3 +38,31 @@ begin
   apply le_refl,
   apply le_refl
 end
+
+def f (a := 10) : ℕ := a + 1
+
+def bla : nat :=
+begin
+  apply f -- uses opt_param for solving goal
+end
+
+example : bla = 11 :=
+rfl
+
+open tactic
+
+lemma foo {a b c : nat} (h₁ : a = b) (h₂ : b = c . assumption) : a = c :=
+eq.trans h₁ h₂
+
+example (a b c : nat) (h₁ : a = b) (h₂ : b = c) : a = c :=
+begin
+  apply foo h₁ -- uses auto_param for solving goal
+end
+
+lemma my_div_self (a : nat) (h : a ≠ 0 . assumption) : a / a = 1 :=
+sorry
+
+example (a : nat) (h : a ≠ 0) : a / a = 1 :=
+begin
+  apply my_div_self -- uses auto_param for solving goal
+end
diff --git a/tests/lean/apply_tac.lean.expected.out b/tests/lean/apply_tac.lean.expected.out
index 5cb81f17a9..df238c1475 100644
--- a/tests/lean/apply_tac.lean.expected.out
+++ b/tests/lean/apply_tac.lean.expected.out
@@ -16,3 +16,4 @@ a : ℕ
 ⊢ ?m_1 = a
 a : ℕ
 ⊢ a = a
+apply_tac.lean:62:0: warning: declaration 'my_div_self' uses sorry
diff --git a/tests/lean/run/apply_auto_opt.lean b/tests/lean/run/apply_auto_opt.lean
index d8109bc1d0..0827d2300b 100644
--- a/tests/lean/run/apply_auto_opt.lean
+++ b/tests/lean/run/apply_auto_opt.lean
@@ -6,7 +6,7 @@ a + b
 
 def val1 : nat :=
 begin
-  apply @p,
+  refine @p _ _,
   exact 2,
   apply_opt_param
 end