max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/util, library/pp_options): add pp.goal.max_hypotheses

Browse source 
This commit also renames pp.compact_goals ==> pp.goal.compact
This commit is contained in:
Leonardo de Moura 2015-12-30 12:38:03 -08:00
parent 23836f53bb
commit ba2cdc848a
3 changed files with 27 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/library/pp_options.cpp
View file

@ -67,8 +67,12 @@ Author: Leonardo de Moura
#define LEAN_DEFAULT_PP_PRETERM false
#endif
#ifndef LEAN_DEFAULT_PP_COMPACT_GOALS
#define LEAN_DEFAULT_PP_COMPACT_GOALS false
#ifndef LEAN_DEFAULT_PP_GOAL_COMPACT
#define LEAN_DEFAULT_PP_GOAL_COMPACT false
#endif
#ifndef LEAN_DEFAULT_PP_GOAL_MAX_HYPS
#define LEAN_DEFAULT_PP_GOAL_MAX_HYPS 200
#endif
#ifndef LEAN_DEFAULT_PP_ALL
@ -91,7 +95,8 @@ static name * g_pp_beta = nullptr;
static name * g_pp_numerals = nullptr;
static name * g_pp_abbreviations = nullptr;
static name * g_pp_preterm = nullptr;
static name * g_pp_compact_goals = nullptr;
static name * g_pp_goal_compact = nullptr;
static name * g_pp_goal_max_hyps = nullptr;
static name * g_pp_all = nullptr;
static list<options> * g_distinguishing_pp_options = nullptr;
@ -112,7 +117,9 @@ void initialize_pp_options() {
g_pp_abbreviations = new name{"pp", "abbreviations"};
g_pp_preterm = new name{"pp", "preterm"};
g_pp_all = new name{"pp", "all"};
g_pp_compact_goals = new name{"pp", "compact_goals"};
g_pp_goal_compact = new name{"pp", "goal", "compact"};
g_pp_goal_max_hyps = new name{"pp", "goal", "max_hypotheses"};
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,
@ -145,8 +152,10 @@ void initialize_pp_options() {
"(pretty printer) display abbreviations (i.e., revert abbreviation expansion when pretty printing)");
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,
register_bool_option(*g_pp_goal_compact, LEAN_DEFAULT_PP_GOAL_COMPACT,
"(pretty printer) try to display goal in a single line when possible");
register_unsigned_option(*g_pp_goal_max_hyps, LEAN_DEFAULT_PP_GOAL_MAX_HYPS,
"(pretty printer) maximum number of hypotheses to be displayed");
register_bool_option(*g_pp_all, LEAN_DEFAULT_PP_ALL,
"(pretty printer) display coercions, implicit parameters, fully qualified names, universes, "
"and disable abbreviations, beta reduction and notation during pretty printing");
@ -178,7 +187,8 @@ 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_pp_goal_compact;
delete g_pp_goal_max_hyps;
delete g_pp_all;
delete g_distinguishing_pp_options;
}
@ -211,7 +221,8 @@ bool get_pp_beta(options const & opts) { return opts.get_bool(*g_
bool get_pp_numerals(options const & opts) { return opts.get_bool(*g_pp_numerals, LEAN_DEFAULT_PP_NUMERALS); }
bool get_pp_abbreviations(options const & opts) { return opts.get_bool(*g_pp_abbreviations, LEAN_DEFAULT_PP_ABBREVIATIONS); }
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 & opts) { return opts.get_bool(*g_pp_compact_goals, LEAN_DEFAULT_PP_COMPACT_GOALS); }
bool get_pp_goal_compact(options const & opts) { return opts.get_bool(*g_pp_goal_compact, LEAN_DEFAULT_PP_GOAL_COMPACT); }
unsigned get_pp_goal_max_hyps(options const & opts) { return opts.get_unsigned(*g_pp_goal_max_hyps, LEAN_DEFAULT_PP_GOAL_MAX_HYPS); }
bool get_pp_all(options const & opts) { return opts.get_bool(*g_pp_all, LEAN_DEFAULT_PP_ALL); }
list<options> const & get_distinguishing_pp_options() { return *g_distinguishing_pp_options; }

3
src/library/pp_options.h
View file

@ -35,7 +35,8 @@ bool get_pp_purify_locals(options const & opts);
bool get_pp_numerals(options const & opts);
bool get_pp_abbreviations(options const & opts);
bool get_pp_preterm(options const & opts);
bool get_pp_compact_goals(options const & opts);
bool get_pp_goal_compact(options const & opts);
unsigned get_pp_goal_max_hyps(options const & opts);
bool get_pp_all(options const & opts);
list<options> const & get_distinguishing_pp_options();

10
src/library/util.cpp
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <algorithm>
#include "kernel/find_fn.h"
#include "kernel/instantiate.h"
#include "kernel/error_msgs.h"
@ -918,11 +919,12 @@ format format_goal(formatter const & _fmt, buffer<expr> const & hyps, expr const
formatter fmt = _fmt.update_options(opts);
unsigned indent = get_pp_indent(opts);
bool unicode = get_pp_unicode(opts);
bool compact = get_pp_compact_goals(opts);
bool compact = get_pp_goal_compact(opts);
unsigned max_hs = get_pp_goal_max_hyps(opts);
format turnstile = unicode ? format("\u22A2") /* ⊢ */ : format("|-");
format r;
unsigned i = hyps.size();
bool first = true;
unsigned i = std::min(max_hs, hyps.size());
bool first = true;
while (i > 0) {
i--;
expr l = hyps[i];
@ -943,6 +945,8 @@ format format_goal(formatter const & _fmt, buffer<expr> const & hyps, expr const
r = compose(comma(), line()) + r;
r = group(ids + space() + colon() + nest(indent, line() + fmt(t))) + r;
}
if (hyps.size() > max_hs)
r = r + compose(comma(), line()) + format("... (set pp.goal.max_hypotheses to display remaining hypotheses)");
if (compact)
r = group(r);
r += line() + turnstile + space() + nest(indent, fmt(tmp_subst.instantiate(conclusion)));