fix(library/tactic): fixes #1369

- `eval_expr` instantiate assigned metavariables occuring in the input
  expression.
- Rename pp.instantiate_goal_mvars to pp.instantiate_mvars
- `format_expr` also instantiates assigned metavariables before pretty printing
  when pp.instantiate_mvars is set to true.

src/library/pp_options.cpp

@@ -108,6 +108,9 @@ Author: Leonardo de Moura
 #define LEAN_DEFAULT_PP_STRUCTURE_PROJECTIONS true
 #endif
 
+#ifndef LEAN_DEFAULT_PP_INSTANTIATE_MVARS
+#define LEAN_DEFAULT_PP_INSTANTIATE_MVARS true
+#endif
 
 namespace lean {
 static name * g_pp_max_depth         = nullptr;
@@ -134,6 +137,7 @@ static name * g_pp_delayed_abstraction = nullptr;
 static name * g_pp_structure_instances = nullptr;
 static name * g_pp_structure_instances_qualifier = nullptr;
 static name * g_pp_structure_projections    = nullptr;
+static name * g_pp_instantiate_mvars = nullptr;
 static name * g_pp_all               = nullptr;
 static list<options> * g_distinguishing_pp_options = nullptr;
 
@@ -163,6 +167,7 @@ void initialize_pp_options() {
     g_pp_structure_instances = new name{"pp", "structure_instances"};
     g_pp_structure_instances_qualifier = new name{"pp", "structure_instances_qualifier"};
     g_pp_structure_projections = new name{"pp", "structure_projections"};
+    g_pp_instantiate_mvars = new name{"pp", "instantiate_mvars"};
 
     register_unsigned_option(*g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH,
                              "(pretty printer) maximum expression depth, after that it will use ellipsis");
@@ -219,6 +224,9 @@ void initialize_pp_options() {
     register_bool_option(*g_pp_all, LEAN_DEFAULT_PP_ALL,
                          "(pretty printer) display coercions, implicit parameters, proof terms, fully qualified names, universes, "
                          "and disable beta reduction and notation during pretty printing");
+    register_bool_option(*g_pp_instantiate_mvars, LEAN_DEFAULT_PP_INSTANTIATE_MVARS,
+                         "(pretty printer) instantiate assigned metavariables before pretty printing terms and goals");
+
     options universes_true(*g_pp_universes, true);
     options full_names_true(*g_pp_full_names, true);
     options implicit_true(*g_pp_implicit, true);
@@ -261,6 +269,7 @@ void finalize_pp_options() {
     delete g_pp_structure_projections;
     delete g_pp_all;
     delete g_pp_delayed_abstraction;
+    delete g_pp_instantiate_mvars;
     delete g_distinguishing_pp_options;
 }
 
@@ -303,5 +312,6 @@ bool     get_pp_delayed_abstraction(options const & opts) { return opts.get_bool
 bool     get_pp_structure_instances(options const & opts) { return opts.get_bool(*g_pp_structure_instances, LEAN_DEFAULT_PP_STRUCTURE_INSTANCES); }
 bool     get_pp_structure_instances_qualifier(options const & opts) { return opts.get_bool(*g_pp_structure_instances_qualifier, LEAN_DEFAULT_PP_STRUCTURE_INSTANCES_QUALIFIER); }
 bool     get_pp_structure_projections(options const & opts) { return opts.get_bool(*g_pp_structure_projections, LEAN_DEFAULT_PP_STRUCTURE_PROJECTIONS); }
+bool     get_pp_instantiate_mvars(options const & o)    { return o.get_bool(*g_pp_instantiate_mvars, LEAN_DEFAULT_PP_INSTANTIATE_MVARS); }
 bool     get_pp_all(options const & opts)               { return opts.get_bool(*g_pp_all, LEAN_DEFAULT_PP_ALL); }
 }

src/library/pp_options.h

@@ -46,6 +46,7 @@ bool     get_pp_delayed_abstraction(options const & opts);
 bool     get_pp_structure_instances(options const & opts);
 bool     get_pp_structure_instances_qualifier(options const & opts);
 bool     get_pp_structure_projections(options const & opts);
+bool     get_pp_instantiate_mvars(options const & o);
 bool     get_pp_all(options const & opts);
 
 void initialize_pp_options();

src/library/tactic/eval.cpp

@@ -12,8 +12,10 @@ Author: Leonardo de Moura
 #include "library/tactic/tactic_state.h"
 
 namespace lean {
-static vm_obj eval(expr const & A, expr const & a, tactic_state const & s) {
+static vm_obj eval(expr const & A, expr a, tactic_state const & s) {
     LEAN_TACTIC_TRY;
+    metavar_context mctx = s.mctx();
+    a = mctx.instantiate_mvars(a);
     if (has_local(a) || !closed(a))
         return mk_tactic_exception("invalid eval_expr, expression must be closed", s);
     if (is_constant(a)) {

src/library/tactic/smt/smt_state.cpp

@@ -609,7 +609,7 @@ static format pp_equivalences(type_context & ctx, cc_state const & ccs, formatte
 format smt_goal_to_format(smt_goal sg, tactic_state const & ts) {
     lean_assert(ts.goals());
     options opts               = ts.get_options().update_if_undef(get_pp_purify_locals_name(), false);
-    bool inst_mvars            = get_pp_instantiate_goal_mvars(opts);
+    bool inst_mvars            = get_pp_instantiate_mvars(opts);
     bool unicode               = get_pp_unicode(opts);
     unsigned indent            = get_pp_indent(opts);
     metavar_decl decl          = *ts.get_main_goal_decl();

src/library/tactic/tactic_state.cpp

@@ -35,17 +35,7 @@ Author: Leonardo de Moura
 #include "library/compiler/vm_compiler.h"
 #include "library/tactic/tactic_state.h"
 
-#ifndef LEAN_DEFAULT_PP_INSTANTIATE_GOAL_MVARS
-#define LEAN_DEFAULT_PP_INSTANTIATE_GOAL_MVARS true
-#endif
-
 namespace lean {
-static name * g_pp_instantiate_goal_mvars = nullptr;
-
-unsigned get_pp_instantiate_goal_mvars(options const & o) {
-    return o.get_unsigned(*g_pp_instantiate_goal_mvars, LEAN_DEFAULT_PP_INSTANTIATE_GOAL_MVARS);
-}
-
 void tactic_state_cell::dealloc() {
     delete this;
 }
@@ -158,7 +148,7 @@ format tactic_state::pp_expr(formatter_factory const & fmtf, expr const & e) con
 
 format tactic_state::pp_goal(formatter_factory const & fmtf, expr const & g) const {
     options opts               = get_options().update_if_undef(get_pp_purify_locals_name(), false);
-    bool inst_mvars            = get_pp_instantiate_goal_mvars(opts);
+    bool inst_mvars            = get_pp_instantiate_mvars(opts);
     metavar_decl decl          = mctx().get_metavar_decl(g);
     local_context lctx         = decl.get_context();
     metavar_context mctx_tmp   = mctx();
@@ -252,7 +242,11 @@ vm_obj tactic_state_to_format(vm_obj const & s) {
 }
 
 format pp_expr(tactic_state const & s, expr const & e) {
-    return s.pp_expr(e);
+    expr new_e      = e;
+    bool inst_mvars = get_pp_instantiate_mvars(s.get_options());
+    if (inst_mvars)
+        new_e       = metavar_context(s.mctx()).instantiate_mvars(e);
+    return s.pp_expr(new_e);
 }
 
 format pp_indented_expr(tactic_state const & s, expr const & e) {
@@ -841,12 +835,8 @@ void initialize_tactic_state() {
     DECLARE_VM_BUILTIN(name({"tactic", "open_namespaces"}),      tactic_open_namespaces);
     DECLARE_VM_BUILTIN(name({"tactic", "decl_name"}),            tactic_decl_name);
     DECLARE_VM_BUILTIN(name({"tactic", "add_aux_decl"}),         tactic_add_aux_decl);
-    g_pp_instantiate_goal_mvars = new name{"pp", "instantiate_goal_mvars"};
-    register_bool_option(*g_pp_instantiate_goal_mvars, LEAN_DEFAULT_PP_INSTANTIATE_GOAL_MVARS,
-                         "(pretty printer) instantiate assigned metavariables before pretty printing goals");
 }
 
 void finalize_tactic_state() {
-    delete g_pp_instantiate_goal_mvars;
 }
 }

src/library/tactic/tactic_state.h

@@ -174,8 +174,6 @@ type_context mk_type_context_for(vm_obj const & s, vm_obj const & m);
 #define LEAN_TACTIC_TRY try {
 #define LEAN_TACTIC_CATCH(S) } catch (exception const & ex) { return mk_tactic_exception(ex, S); }
 
-unsigned get_pp_instantiate_goal_mvars(options const & o);
-
 void initialize_tactic_state();
 void finalize_tactic_state();
 }

tests/lean/1369.lean

@@ -0,0 +1,41 @@
+open nat
+open tactic
+
+meta def match_le (e : expr) : tactic (expr × expr) :=
+match expr.is_le e with
+| (some r) := return r
+| none     := tactic.fail "expression is not a leq"
+end
+
+meta def nat_lit_le : tactic unit := do
+  (base_e, bound_e) ← tactic.target >>= match_le,
+  base  ← tactic.eval_expr ℕ base_e,
+  skip
+
+example : 17 ≤ 555555 :=
+begin
+  nat_lit_le,
+  admit
+end
+
+example : { k : ℕ // k ≤ 555555 } :=
+begin
+  refine subtype.tag _ _,
+  exact 17,
+  target >>= trace,
+  trace_state,
+  nat_lit_le,
+  admit
+end
+
+set_option pp.instantiate_mvars false
+
+example : { k : ℕ // k ≤ 555555 } :=
+begin
+  refine subtype.tag _ _,
+  exact 17,
+  target >>= trace,
+  trace_state,
+  nat_lit_le,
+  admit
+end

tests/lean/1369.lean.expected.out

@@ -0,0 +1,4 @@
+17 ≤ 555555
+⊢ 17 ≤ 555555
+?m_1 ≤ 555555
+⊢ ?m_1 ≤ 555555