diff --git a/src/library/pp_options.cpp b/src/library/pp_options.cpp index 89966c1fdd..5ebff3529f 100644 --- a/src/library/pp_options.cpp +++ b/src/library/pp_options.cpp @@ -71,6 +71,10 @@ Author: Leonardo de Moura #define LEAN_DEFAULT_PP_PRETERM false #endif +#ifndef LEAN_DEFAULT_PP_COMPACT_GOALS +#define LEAN_DEFAULT_PP_COMPACT_GOALS false +#endif + namespace lean { static name * g_pp_max_depth = nullptr; static name * g_pp_max_steps = nullptr; @@ -88,6 +92,7 @@ static name * g_pp_numerals = nullptr; static name * g_pp_abbreviations = nullptr; static name * g_pp_extra_spaces = nullptr; static name * g_pp_preterm = nullptr; +static name * g_pp_compact_goals = nullptr; static list * g_distinguishing_pp_options = nullptr; void initialize_pp_options() { @@ -107,6 +112,7 @@ void initialize_pp_options() { g_pp_abbreviations = new name{"pp", "abbreviations"}; g_pp_extra_spaces = new name{"pp", "extra_spaces"}; g_pp_preterm = new name{"pp", "preterm"}; + g_pp_compact_goals = new name({"pp", "compact_goals"}); register_unsigned_option(*g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH, "(pretty printer) maximum expression depth, after that it will use ellipsis"); register_unsigned_option(*g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS, @@ -141,6 +147,8 @@ void initialize_pp_options() { "(pretty printer) add space after prefix operators and before postfix ones"); register_bool_option(*g_pp_preterm, LEAN_DEFAULT_PP_PRETERM, "(pretty printer) assume the term is a preterm (i.e., a term before elaboration)"); + register_bool_option(*g_pp_compact_goals, LEAN_DEFAULT_PP_COMPACT_GOALS, + "(pretty printer) try to display goal in a single line when possible"); options universes_true(*g_pp_universes, true); options full_names_true(*g_pp_full_names, true); @@ -171,6 +179,7 @@ void finalize_pp_options() { delete g_pp_purify_metavars; delete g_pp_purify_locals; delete g_pp_beta; + delete g_pp_compact_goals; delete g_distinguishing_pp_options; } @@ -201,5 +210,7 @@ bool get_pp_numerals(options const & opts) { return opts.get_bool(*g_ bool get_pp_abbreviations(options const & opts) { return opts.get_bool(*g_pp_abbreviations, LEAN_DEFAULT_PP_ABBREVIATIONS); } bool get_pp_extra_spaces(options const & opts) { return opts.get_bool(*g_pp_extra_spaces, LEAN_DEFAULT_PP_EXTRA_SPACES); } bool get_pp_preterm(options const & opts) { return opts.get_bool(*g_pp_preterm, LEAN_DEFAULT_PP_PRETERM); } +bool get_pp_compact_goals(options const & o) { return o.get_bool(*g_pp_compact_goals, LEAN_DEFAULT_PP_COMPACT_GOALS); } + list const & get_distinguishing_pp_options() { return *g_distinguishing_pp_options; } } diff --git a/src/library/pp_options.h b/src/library/pp_options.h index 53bd083d9a..1783a3d552 100644 --- a/src/library/pp_options.h +++ b/src/library/pp_options.h @@ -34,6 +34,7 @@ bool get_pp_numerals(options const & opts); bool get_pp_abbreviations(options const & opts); bool get_pp_extra_spaces(options const & opts); bool get_pp_preterm(options const & opts); +bool get_pp_compact_goals(options const & opts); list const & get_distinguishing_pp_options(); void initialize_pp_options(); diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp index 51742915c4..4510ec8020 100644 --- a/src/library/tactic/goal.cpp +++ b/src/library/tactic/goal.cpp @@ -14,27 +14,11 @@ Author: Leonardo de Moura #include "kernel/abstract.h" #include "kernel/type_checker.h" #include "kernel/metavar.h" +#include "library/util.h" #include "library/kernel_bindings.h" #include "library/tactic/goal.h" -#ifndef LEAN_DEFAULT_PP_COMPACT_GOALS -#define LEAN_DEFAULT_PP_COMPACT_GOALS false -#endif - namespace lean { -static name * g_pp_compact_goals = nullptr; -void initialize_goal() { - g_pp_compact_goals = new name({"pp", "compact_goals"}); - register_bool_option(*g_pp_compact_goals, LEAN_DEFAULT_PP_COMPACT_GOALS, - "(pretty printer) try to display goal in a single line when possible"); -} -void finalize_goal() { - delete g_pp_compact_goals; -} -bool get_pp_compact_goals(options const & o) { - return o.get_bool(*g_pp_compact_goals, LEAN_DEFAULT_PP_COMPACT_GOALS); -} - local_context goal::to_local_context() const { buffer hyps; get_hyps(hyps); @@ -47,41 +31,9 @@ format goal::pp(formatter const & fmt) const { } format goal::pp(formatter const & fmt, substitution const & s) const { - substitution tmp_subst(s); - options const & opts = fmt.get_options(); - unsigned indent = get_pp_indent(opts); - bool unicode = get_pp_unicode(opts); - bool compact = get_pp_compact_goals(opts); - format turnstile = unicode ? format("\u22A2") /* ⊢ */ : format("|-"); - expr conclusion = m_type; - buffer tmp; - get_app_args(m_meta, tmp); - format r; - unsigned i = 0; - while (i < tmp.size()) { - if (i > 0) - r += compose(comma(), line()); - expr l = tmp[i]; - format ids = fmt(l); - expr t = tmp_subst.instantiate(mlocal_type(l)); - lean_assert(tmp.size() > 0); - while (i < tmp.size() - 1) { - expr l2 = tmp[i+1]; - expr t2 = tmp_subst.instantiate(mlocal_type(l2)); - if (t2 != t) - break; - ids += space() + fmt(l2); - i++; - } - r += group(ids + space() + colon() + nest(indent, line() + fmt(t))); - i++; - } - if (compact) - r = group(r); - r += line() + turnstile + space() + nest(indent, fmt(tmp_subst.instantiate(conclusion))); - if (compact) - r = group(r); - return r; + buffer hyps; + get_app_args(m_meta, hyps); + return format_goal(fmt, hyps, m_type, s); } expr goal::abstract(expr const & v) const { diff --git a/src/library/tactic/goal.h b/src/library/tactic/goal.h index f969623078..7feaea61f0 100644 --- a/src/library/tactic/goal.h +++ b/src/library/tactic/goal.h @@ -114,7 +114,4 @@ io_state_stream const & operator<<(io_state_stream const & out, goal const & g); UDATA_DEFS(goal) void open_goal(lua_State * L); - -void initialize_goal(); -void finalize_goal(); } diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index c4a4c7546b..58c1a6343e 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -34,7 +34,6 @@ Author: Leonardo de Moura namespace lean { void initialize_tactic_module() { - initialize_goal(); initialize_proof_state(); initialize_expr_to_tactic(); initialize_apply_tactic(); @@ -90,6 +89,5 @@ void finalize_tactic_module() { finalize_apply_tactic(); finalize_expr_to_tactic(); finalize_proof_state(); - finalize_goal(); } } diff --git a/src/library/tactic/util.cpp b/src/library/tactic/util.cpp index 16803ac40e..12db3551ef 100644 --- a/src/library/tactic/util.cpp +++ b/src/library/tactic/util.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "library/aliases.h" #include "library/constants.h" +#include "library/util.h" #include "library/tactic/util.h" #include "library/tactic/proof_state.h" @@ -29,39 +30,4 @@ bool is_tactic_namespace_open(environment const & env) { } return false; } - -pair update_meta(expr const & meta, substitution s) { - buffer args; - expr mvar = get_app_args(meta, args); - justification j; - auto p = s.instantiate_metavars(mlocal_type(mvar)); - mvar = update_mlocal(mvar, p.first); - j = p.second; - for (expr & arg : args) { - auto p = s.instantiate_metavars(mlocal_type(arg)); - arg = update_mlocal(arg, p.first); - j = mk_composite1(j, p.second); - } - return mk_pair(mk_app(mvar, args), j); -} - -expr instantiate_meta(expr const & meta, substitution & subst) { - lean_assert(is_meta(meta)); - buffer locals; - expr mvar = get_app_args(meta, locals); - mvar = update_mlocal(mvar, subst.instantiate_all(mlocal_type(mvar))); - for (auto & local : locals) - local = subst.instantiate_all(local); - return mk_app(mvar, locals); -} - -justification mk_failed_to_synthesize_jst(environment const & env, expr const & m) { - return mk_justification(m, [=](formatter const & fmt, substitution const & subst) { - substitution tmp(subst); - expr new_m = instantiate_meta(m, tmp); - expr new_type = type_checker(env).infer(new_m).first; - proof_state ps = to_proof_state(new_m, new_type, name_generator("dontcare")); - return format("failed to synthesize placeholder") + line() + ps.pp(fmt); - }); -} } diff --git a/src/library/tactic/util.h b/src/library/tactic/util.h index 3c921e0430..cfbd9eb506 100644 --- a/src/library/tactic/util.h +++ b/src/library/tactic/util.h @@ -9,17 +9,4 @@ Author: Leonardo de Moura namespace lean { /** \brief Return true iff the tactic namespace is open in given environment. */ bool is_tactic_namespace_open(environment const & env); - -/** \brief Instantiate metavariable application \c meta (?M ...) using \c subst */ -expr instantiate_meta(expr const & meta, substitution & subst); - -/** \brief Given a metavariable application (?m l_1 ... l_n), apply \c s to the types of - ?m and local constants l_i - Return the updated expression and a justification for all substitutions. -*/ -pair update_meta(expr const & meta, substitution s); - -/** \brief Return a 'failed to synthesize placholder' justification for the given - metavariable application \c m of the form (?m l_1 ... l_k) */ -justification mk_failed_to_synthesize_jst(environment const & env, expr const & m); } diff --git a/src/library/util.cpp b/src/library/util.cpp index 4a15b60976..464ae08370 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -16,6 +16,7 @@ Author: Leonardo de Moura #include "library/util.h" #include "library/constants.h" #include "library/unfold_macros.h" +#include "library/pp_options.h" namespace lean { bool is_standard(environment const & env) { @@ -766,6 +767,77 @@ public: } }; +format format_goal(formatter const & fmt, buffer const & hyps, expr const & conclusion, substitution const & s) { + substitution tmp_subst(s); + options const & opts = fmt.get_options(); + unsigned indent = get_pp_indent(opts); + bool unicode = get_pp_unicode(opts); + bool compact = get_pp_compact_goals(opts); + format turnstile = unicode ? format("\u22A2") /* ⊢ */ : format("|-"); + format r; + unsigned i = 0; + while (i < hyps.size()) { + if (i > 0) + r += compose(comma(), line()); + expr l = hyps[i]; + format ids = fmt(l); + expr t = tmp_subst.instantiate(mlocal_type(l)); + lean_assert(tmp.size() > 0); + while (i < hyps.size() - 1) { + expr l2 = hyps[i+1]; + expr t2 = tmp_subst.instantiate(mlocal_type(l2)); + if (t2 != t) + break; + ids += space() + fmt(l2); + i++; + } + r += group(ids + space() + colon() + nest(indent, line() + fmt(t))); + i++; + } + if (compact) + r = group(r); + r += line() + turnstile + space() + nest(indent, fmt(tmp_subst.instantiate(conclusion))); + if (compact) + r = group(r); + return r; +} + +pair update_meta(expr const & meta, substitution s) { + buffer args; + expr mvar = get_app_args(meta, args); + justification j; + auto p = s.instantiate_metavars(mlocal_type(mvar)); + mvar = update_mlocal(mvar, p.first); + j = p.second; + for (expr & arg : args) { + auto p = s.instantiate_metavars(mlocal_type(arg)); + arg = update_mlocal(arg, p.first); + j = mk_composite1(j, p.second); + } + return mk_pair(mk_app(mvar, args), j); +} + +expr instantiate_meta(expr const & meta, substitution & subst) { + lean_assert(is_meta(meta)); + buffer locals; + expr mvar = get_app_args(meta, locals); + mvar = update_mlocal(mvar, subst.instantiate_all(mlocal_type(mvar))); + for (auto & local : locals) + local = subst.instantiate_all(local); + return mk_app(mvar, locals); +} + +justification mk_failed_to_synthesize_jst(environment const & env, expr const & m) { + return mk_justification(m, [=](formatter const & fmt, substitution const & subst) { + substitution tmp(subst); + expr new_m = instantiate_meta(m, tmp); + expr new_type = type_checker(env).infer(new_m).first; + buffer hyps; + get_app_args(new_m, hyps); + return format("failed to synthesize placeholder") + line() + format_goal(fmt, hyps, new_type, subst); + }); +} + type_checker_ptr mk_type_checker(environment const & env, name_generator && ngen, name_predicate const & pred) { return std::unique_ptr(new type_checker(env, std::move(ngen), std::unique_ptr(new extra_opaque_converter(env, pred)))); diff --git a/src/library/util.h b/src/library/util.h index 23e330d01f..0f76988337 100644 --- a/src/library/util.h +++ b/src/library/util.h @@ -232,6 +232,25 @@ inline justification mk_type_mismatch_jst(expr const & v, expr const & v_type, e /** \brief Create a type checker and normalizer that treats any constant named \c n as opaque when pred(n) is true */ type_checker_ptr mk_type_checker(environment const & env, name_generator && ngen, name_predicate const & pred); +/** + \brief Generate the format object for hyps |- conclusion. + The given substitution is applied to all elements. +*/ +format format_goal(formatter const & fmt, buffer const & hyps, expr const & conclusion, substitution const & s); + +/** \brief Given a metavariable application (?m l_1 ... l_n), apply \c s to the types of + ?m and local constants l_i + Return the updated expression and a justification for all substitutions. +*/ +pair update_meta(expr const & meta, substitution s); + +/** \brief Instantiate metavariable application \c meta (?M ...) using \c subst */ +expr instantiate_meta(expr const & meta, substitution & subst); + +/** \brief Return a 'failed to synthesize placholder' justification for the given + metavariable application \c m of the form (?m l_1 ... l_k) */ +justification mk_failed_to_synthesize_jst(environment const & env, expr const & m); + void initialize_library_util(); void finalize_library_util(); }