michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library,library/tactic): move auxiliary procedures from tactic to library

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-01 16:19:55 -07:00
parent 9fc7bc6d25
commit 8a89588079
9 changed files with 108 additions and 105 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/library/pp_options.cpp
View file

@ -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<options> * 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<options> const & get_distinguishing_pp_options() { return *g_distinguishing_pp_options; }
}

1
src/library/pp_options.h
View file

@ -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<options> const & get_distinguishing_pp_options();
void initialize_pp_options();

56
src/library/tactic/goal.cpp
View file

@ -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<expr> 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<expr> 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<expr> hyps;
get_app_args(m_meta, hyps);
return format_goal(fmt, hyps, m_type, s);
}
expr goal::abstract(expr const & v) const {

3
src/library/tactic/goal.h
View file

@ -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();
}

2
src/library/tactic/init_module.cpp
View file

@ -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();
}
}

36
src/library/tactic/util.cpp
View file

@ -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<expr, justification> update_meta(expr const & meta, substitution s) {
buffer<expr> 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<expr> 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);
});
}
}

13
src/library/tactic/util.h
View file

@ -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<expr, justification> 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);
}

72
src/library/util.cpp
View file

@ -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<expr> 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<expr, justification> update_meta(expr const & meta, substitution s) {
buffer<expr> 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<expr> 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<expr> 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<type_checker>(new type_checker(env, std::move(ngen),
std::unique_ptr<converter>(new extra_opaque_converter(env, pred))));

19
src/library/util.h
View file

@ -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 <tt>hyps |- conclusion</tt>.
The given substitution is applied to all elements.
*/
format format_goal(formatter const & fmt, buffer<expr> 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<expr, justification> 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();
}