From c35108cf0df2ff85e54f777875ffd6cef5ff30aa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 10 Feb 2017 15:58:27 -0800 Subject: [PATCH] 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 | 10 +++++++ src/library/pp_options.h | 1 + src/library/tactic/eval.cpp | 4 ++- src/library/tactic/smt/smt_state.cpp | 2 +- src/library/tactic/tactic_state.cpp | 22 ++++----------- src/library/tactic/tactic_state.h | 2 -- tests/lean/1369.lean | 41 ++++++++++++++++++++++++++++ tests/lean/1369.lean.expected.out | 4 +++ 8 files changed, 66 insertions(+), 20 deletions(-) create mode 100644 tests/lean/1369.lean create mode 100644 tests/lean/1369.lean.expected.out diff --git a/src/library/pp_options.cpp b/src/library/pp_options.cpp index 2bd59b36e4..4323c45473 100644 --- a/src/library/pp_options.cpp +++ b/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 * 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); } } diff --git a/src/library/pp_options.h b/src/library/pp_options.h index 817f8a971d..03d7f8eb41 100644 --- a/src/library/pp_options.h +++ b/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(); diff --git a/src/library/tactic/eval.cpp b/src/library/tactic/eval.cpp index 5c0764e70a..b9ec36ad67 100644 --- a/src/library/tactic/eval.cpp +++ b/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)) { diff --git a/src/library/tactic/smt/smt_state.cpp b/src/library/tactic/smt/smt_state.cpp index c424804ee3..98ebf34502 100644 --- a/src/library/tactic/smt/smt_state.cpp +++ b/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(); diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index e26af592cd..ad2f706f58 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/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; } } diff --git a/src/library/tactic/tactic_state.h b/src/library/tactic/tactic_state.h index d16ee23da8..b04d24ab90 100644 --- a/src/library/tactic/tactic_state.h +++ b/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(); } diff --git a/tests/lean/1369.lean b/tests/lean/1369.lean new file mode 100644 index 0000000000..a932185544 --- /dev/null +++ b/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 diff --git a/tests/lean/1369.lean.expected.out b/tests/lean/1369.lean.expected.out new file mode 100644 index 0000000000..cab9fe1f33 --- /dev/null +++ b/tests/lean/1369.lean.expected.out @@ -0,0 +1,4 @@ +17 ≤ 555555 +⊢ 17 ≤ 555555 +?m_1 ≤ 555555 +⊢ ?m_1 ≤ 555555