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

feat(library/equations_compiler): add mk_nonrec

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-08 14:06:42 -07:00
parent dcc314c109
commit 96fa8856bc
11 changed files with 96 additions and 42 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
src/frontends/lean/decl_util.cpp
View file

@ -268,6 +268,7 @@ struct definition_info {
name m_prefix;
bool m_is_private{false};
bool m_is_meta{false};
bool m_is_noncomputable{false};
bool m_is_lemma{false};
bool m_aux_lemmas{false};
unsigned m_next_match_idx{1};
@ -276,19 +277,20 @@ struct definition_info {
MK_THREAD_LOCAL_GET_DEF(definition_info, get_definition_info);
declaration_info_scope::declaration_info_scope(environment const & env, bool is_private, bool is_meta,
bool is_lemma, bool aux_lemmas) {
bool is_noncomputable, bool is_lemma, bool aux_lemmas) {
definition_info & info = get_definition_info();
lean_assert(info.m_prefix.is_anonymous());
info.m_prefix = is_private ? name() : get_namespace(env);
info.m_is_private = is_private;
info.m_is_meta = is_meta;
info.m_is_lemma = is_lemma;
info.m_aux_lemmas = aux_lemmas;
info.m_prefix = is_private ? name() : get_namespace(env);
info.m_is_private = is_private;
info.m_is_meta = is_meta;
info.m_is_noncomputable = is_noncomputable;
info.m_is_lemma = is_lemma;
info.m_aux_lemmas = aux_lemmas;
info.m_next_match_idx = 1;
}
declaration_info_scope::declaration_info_scope(environment const & env, bool is_private, def_cmd_kind k):
declaration_info_scope(env, is_private, k == MetaDefinition, k == Theorem, k == Definition) {}
declaration_info_scope::declaration_info_scope(environment const & env, bool is_private, bool is_noncomputable, def_cmd_kind k):
declaration_info_scope(env, is_private, k == MetaDefinition, is_noncomputable, k == Theorem, k == Definition) {}
declaration_info_scope::~declaration_info_scope() {
definition_info & info = get_definition_info();
@ -297,12 +299,13 @@ declaration_info_scope::~declaration_info_scope() {
equations_header mk_equations_header(list<name> const & ns) {
equations_header h;
h.m_num_fns = length(ns);
h.m_fn_names = ns;
h.m_is_private = get_definition_info().m_is_private;
h.m_is_meta = get_definition_info().m_is_meta;
h.m_is_lemma = get_definition_info().m_is_lemma;
h.m_aux_lemmas = get_definition_info().m_aux_lemmas;
h.m_num_fns = length(ns);
h.m_fn_names = ns;
h.m_is_private = get_definition_info().m_is_private;
h.m_is_meta = get_definition_info().m_is_meta;
h.m_is_noncomputable = get_definition_info().m_is_noncomputable;
h.m_is_lemma = get_definition_info().m_is_lemma;
h.m_aux_lemmas = get_definition_info().m_aux_lemmas;
return h;
}

4
src/frontends/lean/decl_util.h
View file

@ -77,8 +77,8 @@ environment add_local_ref(parser & p, environment const & env, name const & c_na
nested definitions. */
class declaration_info_scope {
public:
declaration_info_scope(environment const & env, bool is_private, bool is_meta, bool is_lemma, bool aux_lemmas);
declaration_info_scope(environment const & env, bool is_private, def_cmd_kind k);
declaration_info_scope(environment const & env, bool is_private, bool is_meta, bool is_noncomputable, bool is_lemma, bool aux_lemmas);
declaration_info_scope(environment const & env, bool is_private, bool is_noncomputable, def_cmd_kind k);
~declaration_info_scope();
};

6
src/frontends/lean/definition_cmds.cpp
View file

@ -130,11 +130,11 @@ expr parse_mutual_definition(parser & p, buffer<name> & lp_names, buffer<expr> &
return r;
}
environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, bool is_private, bool /* is_protected */, bool /* is_noncomputable */,
environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, bool is_private, bool /* is_protected */, bool is_noncomputable,
decl_attributes /* attrs */) {
buffer<name> lp_names;
buffer<expr> fns, params;
declaration_info_scope scope(p.env(), is_private, kind);
declaration_info_scope scope(p.env(), is_private, is_noncomputable, kind);
expr val = parse_mutual_definition(p, lp_names, fns, params);
if (p.used_sorry()) p.declare_sorry();
elaborator elab(p.env(), p.get_options(), metavar_context(), local_context());
@ -333,7 +333,7 @@ environment xdefinition_cmd_core(parser & p, def_cmd_kind kind, bool is_private,
buffer<expr> params;
expr fn, val;
auto header_pos = p.pos();
declaration_info_scope scope(p.env(), is_private, kind);
declaration_info_scope scope(p.env(), is_private, is_noncomputable, kind);
std::tie(fn, val) = parse_definition(p, lp_names, params, kind == def_cmd_kind::Example);
if (p.used_sorry()) p.declare_sorry();
elaborator elab(p.env(), p.get_options(), metavar_context(), local_context());

2
src/library/equations_compiler/compiler.cpp
View file

@ -22,7 +22,7 @@ expr compile_equations(environment & env, options const & opts, metavar_context
trace_compiler(tout() << "recursive: " << is_recursive_eqns(ctx, eqns) << "\n";);
if (equations_num_fns(eqns) == 1) {
if (!is_recursive_eqns(ctx, eqns)) {
return elim_match(env, opts, mctx, lctx, eqns).m_fn;
return mk_nonrec(env, opts, mctx, lctx, eqns);
} else if (optional<expr> r = try_structural_rec(env, opts, mctx, lctx, eqns)) {
return *r;
}

32
src/library/equations_compiler/elim_match.cpp
View file

@ -1151,6 +1151,38 @@ elim_match_result elim_match(environment & env, options const & opts, metavar_co
return r;
}
expr mk_nonrec(environment & env, options const & opts, metavar_context & mctx,
local_context const & lctx, expr const & eqns) {
equations_header header = get_equations_header(eqns);
auto R = elim_match(env, opts, mctx, lctx, eqns);
type_context ctx1(env, opts, mctx, lctx, transparency_mode::Semireducible);
expr fn_type = ctx1.infer(R.m_fn);
expr fn;
std::tie(env, fn) = mk_aux_definition(env, mctx, lctx, header.m_is_private, header.m_is_lemma, header.m_is_noncomputable,
head(header.m_fn_names), fn_type, R.m_fn);
name fn_name = const_name(get_app_fn(fn));
unsigned eqn_idx = 1;
type_context ctx2(env, opts, mctx, lctx, transparency_mode::Semireducible);
for (expr type : R.m_lemmas) {
type_context::tmp_locals locals(ctx2);
type = ctx2.relaxed_whnf(type);
while (is_pi(type)) {
expr local = locals.push_local_from_binding(type);
type = instantiate(binding_body(type), local);
}
lean_assert(is_eq(type));
expr lhs = app_arg(app_fn(type));
expr rhs = app_arg(type);
buffer<expr> lhs_args;
get_app_args(lhs, lhs_args);
expr new_lhs = mk_app(fn, lhs_args);
env = mk_equation_lemma(env, opts, mctx, ctx2.lctx(), fn_name,
eqn_idx, header.m_is_private, locals.as_buffer(), new_lhs, rhs);
eqn_idx++;
}
return fn;
}
void initialize_elim_match() {
register_trace_class({"eqn_compiler", "elim_match"});
register_trace_class({"debug", "eqn_compiler", "elim_match"});

2
src/library/equations_compiler/elim_match.h
View file

@ -13,6 +13,8 @@ struct elim_match_result {
elim_match_result(expr const & fn, list<expr> const & lemmas):m_fn(fn), m_lemmas(lemmas) {}
};
elim_match_result elim_match(environment & env, options const & opts, metavar_context & mctx, local_context const & lctx, expr const & eqns);
expr mk_nonrec(environment & env, options const & opts, metavar_context & mctx,
local_context const & lctx, expr const & eqns);
void initialize_elim_match();
void finalize_elim_match();
}

5
src/library/equations_compiler/equations.cpp
View file

@ -51,7 +51,7 @@ public:
virtual optional<expr> expand(expr const &, abstract_type_context &) const { throw_eqs_ex(); }
virtual void write(serializer & s) const {
s << *g_equations_opcode << m_header.m_num_fns << m_header.m_is_private << m_header.m_is_meta
<< m_header.m_is_lemma << m_header.m_aux_lemmas;
<< m_header.m_is_noncomputable << m_header.m_is_lemma << m_header.m_aux_lemmas;
write_list(s, m_header.m_fn_names);
}
equations_header const & get_header() const { return m_header; }
@ -229,7 +229,8 @@ void initialize_equations() {
register_macro_deserializer(*g_equations_opcode,
[](deserializer & d, unsigned num, expr const * args) {
equations_header h;
d >> h.m_num_fns >> h.m_is_private >> h.m_is_meta >> h.m_is_lemma >> h.m_aux_lemmas;
d >> h.m_num_fns >> h.m_is_private >> h.m_is_meta >> h.m_is_noncomputable
>> h.m_is_lemma >> h.m_aux_lemmas;
h.m_fn_names = read_list<name>(d);
if (num == 0 || h.m_num_fns == 0)
throw corrupted_stream_exception();

13
src/library/equations_compiler/equations.h
View file

@ -28,12 +28,13 @@ expr mk_inaccessible(expr const & e);
bool is_inaccessible(expr const & e);
struct equations_header {
unsigned m_num_fns{0}; /* number of functions being defined */
list<name> m_fn_names; /* names for functions */
bool m_is_private{false}; /* if true, it must be a private definition */
bool m_is_lemma{false}; /* if true, equations are defining a lemma */
bool m_is_meta{false}; /* the auxiliary declarations should be tagged as meta */
bool m_aux_lemmas{false}; /* if true, we must create equation lemmas and induction principle */
unsigned m_num_fns{0}; /* number of functions being defined */
list<name> m_fn_names; /* names for functions */
bool m_is_private{false}; /* if true, it must be a private definition */
bool m_is_lemma{false}; /* if true, equations are defining a lemma */
bool m_is_meta{false}; /* the auxiliary declarations should be tagged as meta */
bool m_is_noncomputable{false}; /* if true, equation is not computable and code should not be generated */
bool m_aux_lemmas{false}; /* if true, we must create equation lemmas and induction principle */
equations_header() {}
equations_header(unsigned num_fns):m_num_fns(num_fns) {}
};

2
src/library/equations_compiler/structural_rec.cpp
View file

@ -610,7 +610,7 @@ struct structural_rec_fn {
} else {
expr r;
std::tie(m_env, r) = mk_aux_definition(m_env, m_mctx, m_lctx, m_header.m_is_private, m_header.m_is_lemma,
head(m_header.m_fn_names), m_fn_type, new_fn);
m_header.m_is_noncomputable, head(m_header.m_fn_names), m_fn_type, new_fn);
return r;
}
}

39
src/library/equations_compiler/util.cpp
View file

@ -28,13 +28,22 @@ Author: Leonardo de Moura
#define LEAN_DEFAULT_EQN_COMPILER_DSIMP true
#endif
#ifndef LEAN_DEFAULT_EQN_COMPILER_LEMMAS
#define LEAN_DEFAULT_EQN_COMPILER_LEMMAS true
#endif
namespace lean {
static name * g_eqn_compiler_dsimp = nullptr;
static name * g_eqn_compiler_dsimp = nullptr;
static name * g_eqn_compiler_lemmas = nullptr;
static bool get_eqn_compiler_dsimp(options const & o) {
return o.get_bool(*g_eqn_compiler_dsimp, LEAN_DEFAULT_EQN_COMPILER_DSIMP);
}
static bool get_eqn_compiler_lemmas(options const & o) {
return o.get_bool(*g_eqn_compiler_lemmas, LEAN_DEFAULT_EQN_COMPILER_LEMMAS);
}
[[ noreturn ]] void throw_ill_formed_eqns() {
throw exception("ill-formed match/equations expression");
}
@ -228,7 +237,8 @@ static pair<environment, name> mk_def_name(environment const & env, bool is_priv
}
pair<environment, expr> mk_aux_definition(environment const & env, metavar_context const & mctx, local_context const & lctx,
bool is_private, bool is_lemma, name const & c, expr const & type, expr const & value) {
bool is_private, bool is_lemma, bool is_noncomputable,
name const & c, expr const & type, expr const & value) {
environment new_env = env;
name new_c;
std::tie(new_env, new_c) = mk_def_name(env, is_private, c);
@ -236,7 +246,7 @@ pair<environment, expr> mk_aux_definition(environment const & env, metavar_conte
std::tie(new_env, r) = is_lemma ?
mk_aux_lemma(new_env, mctx, lctx, new_c, type, value) :
mk_aux_definition(new_env, mctx, lctx, new_c, type, value);
if (!is_lemma) {
if (!is_lemma && !is_noncomputable) {
try {
declaration d = new_env.get(new_c);
new_env = vm_compile(new_env, d);
@ -397,7 +407,14 @@ static expr prove_eqn_lemma_core(type_context & ctx, buffer<expr> const & Hs, ex
expr const & c = ite_args[0];
expr c_lhs, c_rhs;
lean_verify(is_eq(c, c_lhs, c_rhs));
if (ctx.is_def_eq(c_lhs, c_rhs)) {
if (auto H = find_if_neg_hypothesis(ctx, c, Hs)) {
expr lhs_else = ite_args[4];
expr A = ite_args[2];
level A_lvl = get_level(ctx, A);
expr H1 = mk_app(mk_constant(get_if_neg_name(), {A_lvl}), {c, ite_args[1], *H, A, ite_args[3], lhs_else});
expr H2 = prove_eqn_lemma_core(ctx, Hs, lhs_else, rhs);
return mk_app(mk_constant(get_eq_trans_name(), {A_lvl}), {A, lhs, lhs_else, rhs, H1, H2});
} else if (ctx.is_def_eq(c_lhs, c_rhs)) {
expr H = mk_eq_refl(ctx, c_lhs);
expr lhs_then = ite_args[3];
expr A = ite_args[2];
@ -406,13 +423,6 @@ static expr prove_eqn_lemma_core(type_context & ctx, buffer<expr> const & Hs, ex
expr H2 = prove_eqn_lemma_core(ctx, Hs, lhs_then, rhs);
expr eq_trans = mk_constant(get_eq_trans_name(), {A_lvl});
return mk_app(eq_trans, {A, lhs, lhs_then, rhs, H1, H2});
} else if (auto H = find_if_neg_hypothesis(ctx, c, Hs)) {
expr lhs_else = ite_args[4];
expr A = ite_args[2];
level A_lvl = get_level(ctx, A);
expr H1 = mk_app(mk_constant(get_if_neg_name(), {A_lvl}), {c, ite_args[1], *H, A, ite_args[3], lhs_else});
expr H2 = prove_eqn_lemma_core(ctx, Hs, lhs_else, rhs);
return mk_app(mk_constant(get_eq_trans_name(), {A_lvl}), {A, lhs, lhs_else, rhs, H1, H2});
}
}
@ -439,6 +449,7 @@ static expr prove_eqn_lemma(type_context & ctx, buffer<expr> const & Hs, expr co
environment mk_equation_lemma(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,
name const & f_name, unsigned eqn_idx, bool is_private,
buffer<expr> const & Hs, expr const & lhs, expr const & rhs) {
if (!get_eqn_compiler_lemmas(opts)) return env;
type_context ctx(env, opts, mctx, lctx, transparency_mode::Semireducible);
expr type = ctx.mk_pi(Hs, mk_eq(ctx, lhs, rhs));
expr proof = prove_eqn_lemma(ctx, Hs, lhs, rhs);
@ -447,14 +458,18 @@ environment mk_equation_lemma(environment const & env, options const & opts, met
}
void initialize_eqn_compiler_util() {
g_eqn_compiler_dsimp = new name{"eqn_compiler", "dsimp"};
g_eqn_compiler_dsimp = new name{"eqn_compiler", "dsimp"};
g_eqn_compiler_lemmas = new name{"eqn_compiler", "lemmas"};
register_bool_option(*g_eqn_compiler_dsimp, LEAN_DEFAULT_EQN_COMPILER_DSIMP,
"(equation compiler) use defeq simplifier to cleanup types of "
"automatically synthesized equational lemmas");
register_bool_option(*g_eqn_compiler_lemmas, LEAN_DEFAULT_EQN_COMPILER_LEMMAS,
"(equation compiler) generate equation lemmas and induction principle");
g_eqn_sanitizer_token = register_defeq_simp_attribute("eqn_sanitizer");
}
void finalize_eqn_compiler_util() {
delete g_eqn_compiler_dsimp;
delete g_eqn_compiler_lemmas;
}
}

2
src/library/equations_compiler/util.h
View file

@ -76,7 +76,7 @@ expr erase_inaccessible_annotations(expr const & e);
list<expr> erase_inaccessible_annotations(list<expr> const & es);
pair<environment, expr> mk_aux_definition(environment const & env, metavar_context const & mctx, local_context const & lctx,
bool is_private, bool is_lemma, name const & c, expr const & type, expr const & value);
bool is_private, bool is_lemma, bool is_noncomputable, name const & n, expr const & type, expr const & value);
environment mk_equation_lemma(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,
name const & f_name, unsigned eqn_idx, bool is_private,