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

fix(library/equations_compiler,frontends/lean): private name support and alias generation for auxialiary declarations

Browse source 
fixes #1804

Remark: now, all auxiliary definitions in a private declaration share
the same "private" prefix.
This commit is contained in:
Leonardo de Moura 2017-09-11 16:34:29 -07:00
parent d82df26ff0
commit d428eca8a7
22 changed files with 563 additions and 188 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/frontends/lean/builtin_cmds.cpp
View file

@ -179,8 +179,21 @@ environment end_scoped_cmd(parser & p) {
}
}
/* Auxiliary class to setup private naming scope for transient commands such as #check/#reduce/#eval and run_cmd */
class transient_cmd_scope {
environment m_env;
private_name_scope m_prv_scope;
public:
transient_cmd_scope(parser & p):
m_env(p.env()),
m_prv_scope(true, m_env) {
p.set_env(m_env);
}
};
environment check_cmd(parser & p) {
expr e; level_param_names ls;
transient_cmd_scope cmd_scope(p);
std::tie(e, ls) = parse_local_expr(p, "_check");
type_checker tc(p.env(), true, false);
expr type = tc.check(e, ls);
@ -200,6 +213,7 @@ environment check_cmd(parser & p) {
}
environment reduce_cmd(parser & p) {
transient_cmd_scope cmd_scope(p);
bool whnf = false;
if (p.curr_is_token(get_whnf_tk())) {
p.next();
@ -401,6 +415,7 @@ static expr convert_metavars(metavar_context & ctx, expr const & e) {
}
static environment unify_cmd(parser & p) {
transient_cmd_scope cmd_scope(p);
environment const & env = p.env();
expr e1; level_param_names ls1;
std::tie(e1, ls1) = parse_local_expr(p, "_unify");
@ -432,6 +447,7 @@ static environment compile_cmd(parser & p) {
}
static environment eval_cmd(parser & p) {
transient_cmd_scope cmd_scope(p);
auto pos = p.pos();
expr e; level_param_names ls;
std::tie(e, ls) = parse_local_expr(p, "_eval", /* relaxed */ false);
@ -536,7 +552,7 @@ environment add_key_equivalence_cmd(parser & p) {
}
static environment run_command_cmd(parser & p) {
/* initial state for executing the tactic */
transient_cmd_scope cmd_scope(p);
module::scope_pos_info scope_pos(p.pos());
environment env = p.env();
options opts = p.get_options();

12
src/frontends/lean/builtin_exprs.cpp
View file

@ -186,10 +186,10 @@ static expr parse_let(parser_state & p, pos_info const & pos, bool in_do_block)
for (expr const & l : new_locals)
p.add_local(l);
expr body = parse_let_body(p, pos, in_do_block);
match_definition_scope match_scope;
match_definition_scope match_scope(p.env());
expr fn = p.save_pos(mk_local(mk_fresh_name(), *g_let_match_name, mk_expr_placeholder(), mk_rec_info(true)), pos);
expr eqn = Fun(fn, Fun(new_locals, p.save_pos(mk_equation(p.rec_save_pos(mk_app(fn, lhs), pos), body), pos), p), p);
equations_header h = mk_equations_header(match_scope.get_name());
equations_header h = mk_equations_header(match_scope.get_name(), match_scope.get_actual_name());
expr eqns = p.save_pos(mk_equations(h, 1, &eqn), pos);
return p.save_pos(mk_app(eqns, value), pos);
}
@ -319,7 +319,7 @@ static expr parse_do(parser_state & p, bool has_braces) {
} else {
// must introduce a "fake" match
auto pos = ps[i];
match_definition_scope match_scope;
match_definition_scope match_scope(p.env());
expr fn = p.save_pos(mk_local(mk_fresh_name(), *g_do_match_name, mk_expr_placeholder(), mk_rec_info(true)), pos);
buffer<expr> locals;
to_buffer(lhss_locals[i], locals);
@ -342,7 +342,7 @@ static expr parse_do(parser_state & p, bool has_braces) {
ignore_if_unused),
pos), p), p);
eqs.push_back(else_eq);
equations_header h = mk_equations_header(match_scope.get_name());
equations_header h = mk_equations_header(match_scope.get_name(), match_scope.get_actual_name());
expr eqns = p.save_pos(mk_equations(h, eqs.size(), eqs.data()), pos);
expr local = mk_local("_p", mk_expr_placeholder());
expr match = p.mk_app(eqns, local, pos);
@ -744,10 +744,10 @@ static expr parse_lambda_constructor(parser_state & p, pos_info const & ini_pos)
} else {
body = parse_lambda_core(p, ini_pos);
}
match_definition_scope match_scope;
match_definition_scope match_scope(p.env());
expr fn = p.save_pos(mk_local(mk_fresh_name(), *g_lambda_match_name, mk_expr_placeholder(), mk_rec_info(true)), pos);
expr eqn = Fun(fn, Fun(locals, p.save_pos(mk_equation(p.rec_save_pos(mk_app(fn, pattern), pos), body), pos), p), p);
equations_header h = mk_equations_header(match_scope.get_name());
equations_header h = mk_equations_header(match_scope.get_name(), match_scope.get_actual_name());
expr x = p.rec_save_pos(mk_local(mk_fresh_name(), "_x", mk_expr_placeholder(), binder_info()), pos);
bool use_cache = false;
return p.rec_save_pos(Fun(x, mk_app(mk_equations(h, 1, &eqn), x), use_cache), pos);

61
src/frontends/lean/decl_cmds.cpp
View file

@ -190,6 +190,25 @@ static bool curr_is_binder_annotation(parser & p) {
p.curr_is_token(get_ldcurly_tk()) || p.curr_is_token(get_lbracket_tk());
}
/* Auxiliary class to setup naming scopes for a variable/parameter/constant/axiom command.
We need the private_name_scope because the type may contain match-expressions.
These match expressions produce private definitions, and we need to make sure
they use the same infrastructure we use for definitions/theorems.
*/
class var_decl_scope {
environment m_env;
declaration_info_scope m_info_scope;
private_name_scope m_prv_scope;
public:
var_decl_scope(parser & p, decl_modifiers const & mods):
m_env(p.env()),
m_info_scope(p, decl_cmd_kind::Var, mods),
m_prv_scope(true, m_env) {
p.set_env(m_env);
}
};
static environment variable_cmd_core(parser & p, variable_kind k, cmd_meta const & meta) {
check_variable_kind(p, k);
auto pos = p.pos();
@ -202,6 +221,7 @@ static environment variable_cmd_core(parser & p, variable_kind k, cmd_meta const
expr type;
buffer<name> ls_buffer;
if (bi && bi->is_inst_implicit() && (k == variable_kind::Parameter || k == variable_kind::Variable)) {
var_decl_scope var_scope(p, meta.m_modifiers);
/* instance implicit */
if (p.curr_is_identifier()) {
auto n_pos = p.pos();
@ -244,6 +264,7 @@ static environment variable_cmd_core(parser & p, variable_kind k, cmd_meta const
type = p.parse_expr();
}
} else {
var_decl_scope var_scope(p, meta.m_modifiers);
/* non instance implicit cases */
if (p.curr_is_token(get_lcurly_tk()) && (k == variable_kind::Parameter || k == variable_kind::Variable))
throw parser_error("invalid declaration, only constants/axioms can be universe polymorphic", p.pos());
@ -301,12 +322,30 @@ static environment parameter_cmd(parser & p, cmd_meta const & meta) {
return variable_cmd_core(p, variable_kind::Parameter, meta);
}
/*
Remark: we currently do not support declarations such as:
parameters P Q : match ... end
User should use
parameter P : match ... end
parameter Q : match ... end
instead.
*/
static void ensure_no_match_in_variables_cmd(pos_info const & pos) {
if (used_match_idx()) {
throw parser_error("match-expressions are not supported in `parameters/variables/constants` commands "
"(solution use `parameter/variable/constant` commands)", pos);
}
}
static environment variables_cmd_core(parser & p, variable_kind k, cmd_meta const & meta) {
check_variable_kind(p, k);
auto pos = p.pos();
module::scope_pos_info scope_pos(pos);
environment env = p.env();
declaration_info_scope d_scope(p, decl_cmd_kind::Var, meta.m_modifiers);
optional<binder_info> bi = parse_binder_info(p, k);
buffer<name> ids;
optional<parser::local_scope> scope1;
@ -322,6 +361,7 @@ static environment variables_cmd_core(parser & p, variable_kind k, cmd_meta cons
p.next();
ids.push_back(id);
type = p.parse_expr();
ensure_no_match_in_variables_cmd(pos);
} else if (p.curr_is_token(get_rbracket_tk())) {
/* annotation update: variables [decA] */
p.parse_close_binder_info(bi);
@ -329,7 +369,7 @@ static environment variables_cmd_core(parser & p, variable_kind k, cmd_meta cons
if (curr_is_binder_annotation(p))
return variables_cmd_core(p, k, meta);
else
return env;
return p.env();
} else {
/* anonymous : variables [decidable A] */
expr left = p.id_to_expr(id, id_pos);
@ -340,12 +380,14 @@ static environment variables_cmd_core(parser & p, variable_kind k, cmd_meta cons
}
ids.push_back(id);
type = left;
ensure_no_match_in_variables_cmd(pos);
}
} else {
/* anonymous : variables [forall x y, decidable (x = y)] */
name id = p.mk_anonymous_inst_name();
ids.push_back(id);
type = p.parse_expr();
ensure_no_match_in_variables_cmd(pos);
}
} else {
/* non instance implicit cases */
@ -367,7 +409,7 @@ static environment variables_cmd_core(parser & p, variable_kind k, cmd_meta cons
if (curr_is_binder_annotation(p))
return variables_cmd_core(p, k, meta);
else
return env;
return p.env();
} else {
throw parser_error("invalid variables/constants/axioms declaration, ':' expected", pos);
}
@ -375,9 +417,10 @@ static environment variables_cmd_core(parser & p, variable_kind k, cmd_meta cons
if (k == variable_kind::Constant || k == variable_kind::Axiom)
scope1.emplace(p);
type = p.parse_expr();
ensure_no_match_in_variables_cmd(pos);
}
p.parse_close_binder_info(bi);
environment env = p.env();
level_param_names ls = to_level_param_names(collect_univ_params(type));
list<expr> ctx = p.locals_to_context();
for (auto id : ids) {
@ -419,13 +462,13 @@ static environment axioms_cmd(parser & p, cmd_meta const & meta) {
}
static environment definition_cmd(parser & p, cmd_meta const & meta) {
return definition_cmd_core(p, def_cmd_kind::Definition, meta);
return definition_cmd_core(p, decl_cmd_kind::Definition, meta);
}
static environment theorem_cmd(parser & p, cmd_meta const & meta) {
return definition_cmd_core(p, def_cmd_kind::Theorem, meta);
return definition_cmd_core(p, decl_cmd_kind::Theorem, meta);
}
static environment example_cmd(parser & p, cmd_meta const & meta) {
return definition_cmd_core(p, def_cmd_kind::Example, meta);
return definition_cmd_core(p, decl_cmd_kind::Example, meta);
}
static environment instance_cmd(parser & p, cmd_meta const & _meta) {
auto meta = _meta;
@ -436,7 +479,7 @@ static environment instance_cmd(parser & p, cmd_meta const & _meta) {
if (meta.m_modifiers.m_is_mutual)
throw exception("invalid 'mutual' modifier for instance command");
meta.m_modifiers.m_is_protected = true;
return definition_cmd_core(p, def_cmd_kind::Instance, meta);
return definition_cmd_core(p, decl_cmd_kind::Instance, meta);
}
static environment modifiers_cmd(parser & p, cmd_meta const & _meta) {

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

@ -14,6 +14,7 @@ Author: Leonardo de Moura
#include "library/trace.h"
#include "library/placeholder.h"
#include "library/protected.h"
#include "library/private.h"
#include "library/aliases.h"
#include "library/explicit.h"
#include "library/reducible.h"
@ -121,6 +122,8 @@ pair<expr, decl_attributes> parse_inner_header(parser & p, name const & c_expect
if (c_expected != n)
throw parser_error(sstream() << "invalid mutual declaration, '" << c_expected << "' expected",
id_pos);
/* Remark: if this is a private definition, the private prefix must have been set
before invoking this procedure. */
declaration_name_scope scope(n);
p.check_token_next(get_colon_tk(), "invalid mutual declaration, ':' expected");
return mk_pair(p.parse_expr(), attrs);
@ -356,7 +359,8 @@ environment add_alias(environment const & env, bool is_protected, name const & c
}
struct definition_info {
name m_prefix;
name m_prefix; // prefix for local names
name m_actual_prefix; // actual prefix used to create kernel declaration names. m_prefix and m_actual_prefix are different for scoped/private declarations.
bool m_is_private{true}; // pattern matching outside of definitions should generate private names
bool m_is_meta{false};
bool m_is_noncomputable{false};
@ -367,19 +371,23 @@ struct definition_info {
MK_THREAD_LOCAL_GET_DEF(definition_info, get_definition_info);
declaration_info_scope::declaration_info_scope(name const & ns, def_cmd_kind kind, decl_modifiers const & modifiers) {
declaration_info_scope::declaration_info_scope(name const & ns, decl_cmd_kind kind, decl_modifiers const & modifiers) {
definition_info & info = get_definition_info();
lean_assert(info.m_prefix.is_anonymous());
info.m_prefix = modifiers.m_is_private ? name() : ns;
info.m_prefix = name(); // prefix is used to create local name
/* Remark: if info.m_actual_prefix is not `anonymous`, then it has already been set using private_name_scope */
if (info.m_actual_prefix.is_anonymous()) {
info.m_actual_prefix = ns;
}
info.m_is_private = modifiers.m_is_private;
info.m_is_meta = modifiers.m_is_meta;
info.m_is_noncomputable = modifiers.m_is_noncomputable;
info.m_is_lemma = kind == Theorem;
info.m_aux_lemmas = kind != Theorem && !modifiers.m_is_meta;
info.m_is_lemma = kind == decl_cmd_kind::Theorem;
info.m_aux_lemmas = kind != decl_cmd_kind::Theorem && !modifiers.m_is_meta;
info.m_next_match_idx = 1;
}
declaration_info_scope::declaration_info_scope(parser const & p, def_cmd_kind kind, decl_modifiers const & modifiers):
declaration_info_scope::declaration_info_scope(parser const & p, decl_cmd_kind kind, decl_modifiers const & modifiers):
declaration_info_scope(get_namespace(p.env()), kind, modifiers) {}
declaration_info_scope::~declaration_info_scope() {
@ -390,10 +398,11 @@ bool declaration_info_scope::gen_aux_lemmas() const {
return get_definition_info().m_aux_lemmas;
}
equations_header mk_equations_header(list<name> const & ns) {
equations_header mk_equations_header(list<name> const & ns, list<name> const & actual_ns) {
equations_header h;
h.m_num_fns = length(ns);
h.m_fn_names = ns;
h.m_fn_actual_names = actual_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;
@ -402,8 +411,8 @@ equations_header mk_equations_header(list<name> const & ns) {
return h;
}
equations_header mk_equations_header(name const & n) {
return mk_equations_header(to_list(n));
equations_header mk_equations_header(name const & n, name const & actual_n) {
return mk_equations_header(to_list(n), to_list(actual_n));
}
/* Auxiliary function for creating names for auxiliary declarations.
@ -424,35 +433,73 @@ bool used_match_idx() {
declaration_name_scope::declaration_name_scope() {
definition_info & info = get_definition_info();
m_old_prefix = info.m_prefix;
m_old_actual_prefix = info.m_actual_prefix;
m_old_next_match_idx = info.m_next_match_idx;
info.m_next_match_idx = 1;
}
void declaration_name_scope::set_name(name const & n) {
lean_assert(m_name.is_anonymous());
definition_info & info = get_definition_info();
info.m_prefix = mk_decl_name(info.m_prefix, n);
m_name = info.m_prefix;
definition_info & info = get_definition_info();
info.m_prefix = mk_decl_name(info.m_prefix, n);
info.m_actual_prefix = mk_decl_name(info.m_actual_prefix, n);
m_name = info.m_prefix;
m_actual_name = info.m_actual_prefix;
}
declaration_name_scope::declaration_name_scope(name const & n) {
definition_info & info = get_definition_info();
m_old_prefix = info.m_prefix;
m_old_actual_prefix = info.m_actual_prefix;
m_old_next_match_idx = info.m_next_match_idx;
info.m_prefix = mk_decl_name(info.m_prefix, n);
info.m_actual_prefix = mk_decl_name(info.m_actual_prefix, n);
info.m_next_match_idx = 1;
m_name = info.m_prefix;
m_actual_name = info.m_actual_prefix;
}
declaration_name_scope::~declaration_name_scope() {
definition_info & info = get_definition_info();
info.m_prefix = m_old_prefix;
info.m_actual_prefix = m_old_actual_prefix;
info.m_next_match_idx = m_old_next_match_idx;
}
match_definition_scope::match_definition_scope() {
private_name_scope::private_name_scope(bool is_private, environment & env) {
definition_info & info = get_definition_info();
m_name = mk_decl_name(info.m_prefix, name("_match").append_after(info.m_next_match_idx));
info.m_next_match_idx++;
m_old_actual_prefix = info.m_prefix;
m_old_is_private = info.m_is_private;
if (is_private) {
name prv_prefix;
std::tie(env, prv_prefix) = mk_private_prefix(env);
info.m_is_private = true;
info.m_actual_prefix = prv_prefix;
}
}
private_name_scope::~private_name_scope() {
definition_info & info = get_definition_info();
info.m_actual_prefix = m_old_actual_prefix;
info.m_is_private = m_old_is_private;
}
match_definition_scope::match_definition_scope(environment const & env) {
definition_info & info = get_definition_info();
while (true) {
m_name = mk_decl_name(info.m_prefix, name("_match").append_after(info.m_next_match_idx));
m_actual_name = mk_decl_name(info.m_actual_prefix, name("_match").append_after(info.m_next_match_idx));
info.m_next_match_idx++;
if (empty(get_expr_aliases(env, m_name))) {
/* Make sure we don't introduce aliases.
This is important when match-expressions are used in several parameters in a section.
Example:
parameter P : match ... end
parameter Q : match ... end
*/
break;
}
}
}
}

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

@ -13,7 +13,7 @@ namespace lean {
class parser;
class elaborator;
enum def_cmd_kind { Theorem, Definition, Example, Instance };
enum class decl_cmd_kind { Theorem, Definition, Example, Instance, Var };
struct decl_modifiers {
bool m_is_private{false};
@ -29,11 +29,13 @@ struct decl_modifiers {
/** \brief In Lean, declarations may contain nested definitions.
This object is used to propagate relevant flags to
nested definitions. */
nested definitions.
It is used to set/restore the thread local information. */
class declaration_info_scope {
declaration_info_scope(name const & ns, def_cmd_kind kind, decl_modifiers const & modifiers);
declaration_info_scope(name const & ns, decl_cmd_kind kind, decl_modifiers const & modifiers);
public:
declaration_info_scope(parser const & p, def_cmd_kind kind, decl_modifiers const & modifiers);
declaration_info_scope(parser const & p, decl_cmd_kind kind, decl_modifiers const & modifiers);
~declaration_info_scope();
bool gen_aux_lemmas() const;
};
@ -42,23 +44,46 @@ public:
naming prefix for nested definitions. */
class declaration_name_scope {
name m_name;
name m_old_prefix;
name m_actual_name;
name m_old_prefix; /* save current user facing prefix */
name m_old_actual_prefix; /* save current prefix */
unsigned m_old_next_match_idx;
/* Remark: the operation prefix + name in the following constructors and methods tries to avoid propagating
the string `_main` into names. That is, `foo._main` + `bla` is `foo.bla`. */
public:
/* Save the current prefix and match_idx, and set m_name to current prefix + n. */
declaration_name_scope(name const & n);
/* Save the current prefix and match_idx, and reset get_definition_info().m_next_match_idx. */
declaration_name_scope();
~declaration_name_scope();
/* Set m_name to current prefix + n. This method is used when the constructor declaration_name_scope
has been used. */
void set_name(name const & n);
/* Restore prefix and match_idx. */
~declaration_name_scope();
name const & get_name() const { return m_name; }
name const & get_actual_name() const { return m_actual_name; }
};
/** \brief Auxiliary scope for setting m_actual_prefix.
It is used with declaration_name_scope. */
class private_name_scope {
name m_old_actual_prefix; /* save current prefix */
bool m_old_is_private;
public:
/* Remark: If is_private == false, then this auxiliary scope is a no-op. */
private_name_scope(bool is_private, environment & env);
~private_name_scope();
};
/** \brief Auxiliary scope to compute the name for a nested match expression.
In Lean, we create auxiliary declarations for match expressions. */
class match_definition_scope {
name m_name;
name m_actual_name;
public:
match_definition_scope();
match_definition_scope(environment const & env);
name const & get_name() const { return m_name; }
name const & get_actual_name() const { return m_actual_name; }
};
/** \brief Return true if the current scope used match-expressions */
@ -128,8 +153,8 @@ environment add_alias(environment const & env, bool is_protected, name const & c
/** \brief Create an equations header for the given function names.
It uses the information set using declaration_info_scope */
equations_header mk_equations_header(list<name> const & fn_names);
equations_header mk_equations_header(name const & fn_name);
equations_header mk_equations_header(list<name> const & fn_names, list<name> const & fn_actual_names);
equations_header mk_equations_header(name const & fn_name, name const & fn_actual_name);
expr replace_locals_preserving_pos_info(expr const & e, buffer<expr> const & from, buffer<expr> const & to);
expr replace_local_preserving_pos_info(expr const & e, expr const & from, expr const & to);

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

@ -83,13 +83,14 @@ optional<expr> parse_using_well_founded(parser & p) {
}
}
expr mk_equations(parser & p, buffer<expr> const & fns, buffer<name> const & fn_full_names, buffer<expr> const & eqs,
expr mk_equations(parser & p, buffer<expr> const & fns,
buffer<name> const & fn_full_names, buffer<name> const & fn_prv_names, buffer<expr> const & eqs,
optional<expr> const & wf_tacs, pos_info const & pos) {
buffer<expr> new_eqs;
for (expr const & eq : eqs) {
new_eqs.push_back(Fun(fns, eq, p));
}
equations_header h = mk_equations_header(to_list(fn_full_names));
equations_header h = mk_equations_header(to_list(fn_full_names), to_list(fn_prv_names));
if (wf_tacs) {
return p.save_pos(mk_equations(h, new_eqs.size(), new_eqs.data(), *wf_tacs), pos);
} else {
@ -97,11 +98,12 @@ expr mk_equations(parser & p, buffer<expr> const & fns, buffer<name> const & fn_
}
}
expr mk_equations(parser & p, expr const & fn, name const & full_name, buffer<expr> const & eqs,
expr mk_equations(parser & p, expr const & fn, name const & full_name, name const & full_prv_name, buffer<expr> const & eqs,
optional<expr> const & wf_tacs, pos_info const & pos) {
buffer<expr> fns; fns.push_back(fn);
buffer<name> full_names; full_names.push_back(full_name);
return mk_equations(p, fns, full_names, eqs, wf_tacs, pos);
buffer<name> full_prv_names; full_prv_names.push_back(full_prv_name);
return mk_equations(p, fns, full_names, full_prv_names, eqs, wf_tacs, pos);
}
void check_valid_end_of_equations(parser & p) {
@ -114,19 +116,23 @@ void check_valid_end_of_equations(parser & p) {
}
}
expr parse_mutual_definition(parser & p, buffer<name> & lp_names, buffer<expr> & fns, buffer<expr> & params) {
static expr parse_mutual_definition(parser & p, buffer<name> & lp_names, buffer<expr> & fns, buffer<name> & prv_names,
buffer<expr> & params) {
parser::local_scope scope1(p);
auto header_pos = p.pos();
buffer<expr> pre_fns;
parse_mutual_header(p, lp_names, pre_fns, params);
buffer<expr> eqns;
buffer<name> full_names;
buffer<name> full_actual_names;
for (expr const & pre_fn : pre_fns) {
// TODO(leo, dhs): make use of attributes
expr fn_type = parse_inner_header(p, mlocal_pp_name(pre_fn)).first;
declaration_name_scope scope2(mlocal_pp_name(pre_fn));
declaration_name_scope scope3("_main");
full_names.push_back(scope3.get_name());
full_actual_names.push_back(scope3.get_actual_name());
prv_names.push_back(scope2.get_actual_name());
if (p.curr_is_token(get_period_tk())) {
auto period_pos = p.pos();
p.next();
@ -146,7 +152,7 @@ expr parse_mutual_definition(parser & p, buffer<name> & lp_names, buffer<expr> &
for (expr & eq : eqns) {
eq = replace_locals_preserving_pos_info(eq, pre_fns, fns);
}
expr r = mk_equations(p, fns, full_names, eqns, wf_tacs, header_pos);
expr r = mk_equations(p, fns, full_names, full_actual_names, eqns, wf_tacs, header_pos);
collect_implicit_locals(p, lp_names, params, r);
return r;
}
@ -170,21 +176,6 @@ static void finalize_definition(elaborator & elab, buffer<expr> const & params,
lp_names.append(implicit_lp_names);
}
static pair<environment, name> mk_real_name(environment const & env, name const & c_name, bool is_private, pos_info const & pos) {
environment new_env = env;
name c_real_name;
if (is_private) {
unsigned h = hash(pos.first, pos.second);
auto env_n = add_private_name(new_env, c_name, optional<unsigned>(h));
new_env = env_n.first;
c_real_name = env_n.second;
} else {
name const & ns = get_namespace(env);
c_real_name = ns + c_name;
}
return mk_pair(new_env, c_real_name);
}
static expr fix_rec_fn_name(expr const & e, name const & c_name, name const & c_real_name) {
return replace(e, [&](expr const & m, unsigned) {
if (is_rec_fn_macro(m) && get_rec_fn_name(m) == c_name) {
@ -241,12 +232,17 @@ static environment compile_decl(parser & p, environment const & env,
}
static pair<environment, name>
declare_definition(parser & p, environment const & env, def_cmd_kind kind, buffer<name> const & lp_names,
name const & c_name, expr type, optional<expr> val, task<expr> const & proof, cmd_meta const & meta,
declare_definition(parser & p, environment const & env, decl_cmd_kind kind, buffer<name> const & lp_names,
name const & c_name, name const & prv_name, expr type, optional<expr> val, task<expr> const & proof, cmd_meta const & meta,
pos_info const & pos) {
auto env_n = mk_real_name(env, c_name, meta.m_modifiers.m_is_private, pos);
environment new_env = env_n.first;
name c_real_name = env_n.second;
name c_real_name;
environment new_env = env;
if (has_private_prefix(new_env, prv_name)) {
new_env = register_private_name(new_env, c_name, prv_name);
c_real_name = prv_name;
} else {
c_real_name = get_namespace(env) + c_name;
}
if (val && meta.m_modifiers.m_is_meta) {
/* TODO(Leo): fix fix_rec_fn_name for mutual definitions.
We currently do not support meta mutual definitions. Thus, this is not currently an issue. */
@ -260,7 +256,7 @@ declare_definition(parser & p, environment const & env, def_cmd_kind kind, buffe
bool use_conv_opt = true;
bool is_trusted = !meta.m_modifiers.m_is_meta;
auto def =
!val ? mk_theorem(c_real_name, to_list(lp_names), type, proof) : (kind == Theorem ?
!val ? mk_theorem(c_real_name, to_list(lp_names), type, proof) : (kind == decl_cmd_kind::Theorem ?
mk_theorem(c_real_name, to_list(lp_names), type, *val) :
mk_definition(new_env, c_real_name, to_list(lp_names), type, *val, use_conv_opt, is_trusted));
auto cdef = check(p, new_env, c_name, def, pos);
@ -463,14 +459,17 @@ static environment copy_equation_lemmas(environment const & env, name const & d_
return copy_equation_lemmas(env, d_names);
}
static environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, cmd_meta const & meta) {
static environment mutual_definition_cmd_core(parser & p, decl_cmd_kind kind, cmd_meta const & meta) {
buffer<name> lp_names;
buffer<expr> fns, params;
declaration_info_scope scope(p, kind, meta.m_modifiers);
auto header_pos = p.pos();
/* TODO(Leo): allow a different doc string for each function in a mutual definition. */
optional<std::string> doc_string = meta.m_doc_string;
expr val = parse_mutual_definition(p, lp_names, fns, params);
environment env = p.env();
private_name_scope prv_scope(meta.m_modifiers.m_is_private, env);
buffer<name> prv_names;
expr val = parse_mutual_definition(p, lp_names, fns, prv_names, params);
if (meta.m_modifiers.m_is_meta) {
throw exception("support for mutual meta definitions has not been implemented yet");
@ -481,7 +480,7 @@ static environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, cmd
return p.env();
bool recover_from_errors = true;
elaborator elab(p.env(), p.get_options(), get_namespace(p.env()) + mlocal_pp_name(fns[0]), metavar_context(), local_context(), recover_from_errors);
elaborator elab(env, p.get_options(), get_namespace(env) + mlocal_pp_name(fns[0]), metavar_context(), local_context(), recover_from_errors);
buffer<expr> new_params;
elaborate_params(elab, params, new_params);
val = replace_locals_preserving_pos_info(val, params, new_params);
@ -492,6 +491,7 @@ static environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, cmd
return p.env();
}
unsigned num_defs = get_equations_result_size(val);
lean_assert(num_defs == prv_names.size());
lean_assert(fns.size() == num_defs);
buffer<name> new_d_names;
/* Define functions */
@ -502,7 +502,7 @@ static environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, cmd
environment env = elab.env();
name c_name = mlocal_name(fns[i]);
name c_real_name;
std::tie(env, c_real_name) = declare_definition(p, env, kind, lp_names, c_name,
std::tie(env, c_real_name) = declare_definition(p, env, kind, lp_names, c_name, prv_names[i],
curr_type, some_expr(curr), {}, meta, header_pos);
env = add_local_ref(p, env, c_name, c_real_name, lp_names, params);
new_d_names.push_back(c_real_name);
@ -517,8 +517,15 @@ static environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, cmd
return elab.env();
}
static expr_pair parse_definition(parser & p, buffer<name> & lp_names, buffer<expr> & params,
bool is_example, bool is_instance, bool is_meta) {
/* Return tuple (fn, val, actual_name) where
- fn is a local constant with the user name + type
- val is the actual definition
- actual_name for the kernel declaration.
Note that mlocal_pp_name(fn) and actual_name are different for scoped/private declarations.
*/
static std::tuple<expr, expr, name> parse_definition(parser & p, buffer<name> & lp_names, buffer<expr> & params,
bool is_example, bool is_instance, bool is_meta) {
parser::local_scope scope1(p);
auto header_pos = p.pos();
declaration_name_scope scope2;
@ -535,7 +542,7 @@ static expr_pair parse_definition(parser & p, buffer<name> & lp_names, buffer<ex
expr eqn = copy_tag(val, mk_equation(fn, val));
buffer<expr> eqns;
eqns.push_back(eqn);
val = mk_equations(p, fn, scope2.get_name(), eqns, {}, header_pos);
val = mk_equations(p, fn, scope2.get_name(), scope2.get_actual_name(), eqns, {}, header_pos);
} else {
val = p.parse_expr();
}
@ -555,12 +562,12 @@ static expr_pair parse_definition(parser & p, buffer<name> & lp_names, buffer<ex
check_valid_end_of_equations(p);
}
optional<expr> wf_tacs = parse_using_well_founded(p);
val = mk_equations(p, fn, scope2.get_name(), eqns, wf_tacs, header_pos);
val = mk_equations(p, fn, scope2.get_name(), scope2.get_actual_name(), eqns, wf_tacs, header_pos);
} else {
val = p.parser_error_or_expr({"invalid definition, '|' or ':=' expected", p.pos()});
}
collect_implicit_locals(p, lp_names, params, {mlocal_type(fn), val});
return mk_pair(fn, val);
return std::make_tuple(fn, val, scope2.get_actual_name());
}
static void replace_params(buffer<expr> const & params, buffer<expr> const & new_params, expr & fn, expr & val) {
@ -579,15 +586,15 @@ static expr_pair elaborate_theorem(elaborator & elab, expr const & fn, expr val)
return elab.elaborate_with_type(val, mk_as_is(fn_type));
}
static expr_pair elaborate_definition_core(elaborator & elab, def_cmd_kind kind, expr const & fn, expr const & val) {
if (kind == Theorem) {
static expr_pair elaborate_definition_core(elaborator & elab, decl_cmd_kind kind, expr const & fn, expr const & val) {
if (kind == decl_cmd_kind::Theorem) {
return elaborate_theorem(elab, fn, val);
} else {
return elab.elaborate_with_type(val, mlocal_type(fn));
}
}
static expr_pair elaborate_definition(parser & p, elaborator & elab, def_cmd_kind kind, expr const & fn, expr const & val, pos_info const & pos) {
static expr_pair elaborate_definition(parser & p, elaborator & elab, decl_cmd_kind kind, expr const & fn, expr const & val, pos_info const & pos) {
if (p.profiling()) {
xtimeit timer(get_profiling_threshold(p.get_options()), [&](second_duration duration) {
auto msg = p.mk_message(pos, INFORMATION);
@ -765,24 +772,27 @@ static bool is_rfl_preexpr(expr const & e) {
return is_constant(e, get_rfl_name());
}
environment single_definition_cmd_core(parser & p, def_cmd_kind kind, cmd_meta meta) {
environment single_definition_cmd_core(parser & p, decl_cmd_kind kind, cmd_meta meta) {
buffer<name> lp_names;
buffer<expr> params;
expr fn, val;
auto header_pos = p.pos();
module::scope_pos_info scope_pos(header_pos);
declaration_info_scope scope(p, kind, meta.m_modifiers);
bool is_example = (kind == def_cmd_kind::Example);
bool is_instance = (kind == def_cmd_kind::Instance);
bool aux_lemmas = scope.gen_aux_lemmas();
bool is_rfl = false;
environment env = p.env();
private_name_scope prv_scope(meta.m_modifiers.m_is_private, env);
bool is_example = (kind == decl_cmd_kind::Example);
bool is_instance = (kind == decl_cmd_kind::Instance);
bool aux_lemmas = scope.gen_aux_lemmas();
bool is_rfl = false;
if (is_instance)
meta.m_attrs.set_attribute(p.env(), "instance");
std::tie(fn, val) = parse_definition(p, lp_names, params, is_example, is_instance, meta.m_modifiers.m_is_meta);
meta.m_attrs.set_attribute(env, "instance");
name prv_name;
std::tie(fn, val, prv_name) = parse_definition(p, lp_names, params, is_example, is_instance, meta.m_modifiers.m_is_meta);
auto begin_pos = p.cmd_pos();
auto end_pos = p.pos();
scope_log_tree lt(logtree().mk_child({}, (get_namespace(p.env()) + mlocal_pp_name(fn)).to_string(),
scope_log_tree lt(logtree().mk_child({}, (get_namespace(env) + mlocal_pp_name(fn)).to_string(),
{logtree().get_location().m_file_name, {begin_pos, end_pos}}));
// skip elaboration of definitions during reparsing
@ -790,7 +800,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, cmd_meta m
return p.env();
bool recover_from_errors = true;
elaborator elab(p.env(), p.get_options(), get_namespace(p.env()) + mlocal_pp_name(fn), metavar_context(), local_context(), recover_from_errors);
elaborator elab(env, p.get_options(), get_namespace(env) + mlocal_pp_name(fn), metavar_context(), local_context(), recover_from_errors);
buffer<expr> new_params;
elaborate_params(elab, params, new_params);
elab.set_instance_fingerprint();
@ -802,7 +812,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, cmd_meta m
bool eqns = false;
name c_name = mlocal_name(fn);
pair<environment, name> env_n;
if (kind == Theorem) {
if (kind == decl_cmd_kind::Theorem) {
is_rfl = is_rfl_preexpr(val);
type = elab.elaborate_type(mlocal_type(fn));
elab.ensure_no_unassigned_metavars(type);
@ -823,8 +833,8 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, cmd_meta m
new_fn, val, thm_finfo, is_rfl, type,
mctx, lctx, pos_provider, use_info_manager, file_name);
}), log_tree::ElaborationLevel);
env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, type, opt_val, proof, meta, header_pos);
} else if (kind == Example) {
env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, prv_name, type, opt_val, proof, meta, header_pos);
} else if (kind == decl_cmd_kind::Example) {
auto env = p.env();
auto opts = p.get_options();
auto lp_name_list = to_list(lp_names);
@ -854,7 +864,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, cmd_meta m
val = get_equations_result(val, 0);
}
finalize_definition(elab, new_params, type, val, lp_names, meta.m_modifiers.m_is_meta);
env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, type, some_expr(val),
env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, prv_name, type, some_expr(val),
{}, meta, header_pos);
}
environment new_env = env_n.first;
@ -864,9 +874,9 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, cmd_meta m
if (eqns && aux_lemmas) {
new_env = copy_equation_lemmas(new_env, c_real_name);
}
if (!eqns && !meta.m_modifiers.m_is_meta && (kind == Definition || kind == Instance)) {
if (!eqns && !meta.m_modifiers.m_is_meta && (kind == decl_cmd_kind::Definition || kind == decl_cmd_kind::Instance)) {
unsigned arity = new_params.size();
new_env = mk_simple_equation_lemma_for(new_env, p.get_options(), meta.m_modifiers.m_is_private, c_real_name, arity);
new_env = mk_simple_equation_lemma_for(new_env, p.get_options(), meta.m_modifiers.m_is_private, c_name, c_real_name, arity);
}
/* Apply attributes last */
return meta.m_attrs.apply(new_env, p.ios(), c_real_name);
@ -886,7 +896,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, cmd_meta m
}
}
environment definition_cmd_core(parser & p, def_cmd_kind kind, cmd_meta const & meta) {
environment definition_cmd_core(parser & p, decl_cmd_kind kind, cmd_meta const & meta) {
if (meta.m_modifiers.m_is_mutual)
return mutual_definition_cmd_core(p, kind, meta);
else

2
src/frontends/lean/definition_cmds.h
View file

@ -10,7 +10,7 @@ Author: Leonardo de Moura
#include "frontends/lean/decl_util.h"
namespace lean {
environment definition_cmd_core(parser & p, def_cmd_kind k, cmd_meta const & meta);
environment definition_cmd_core(parser & p, decl_cmd_kind k, cmd_meta const & meta);
environment ensure_decl_namespaces(environment const & env, name const & full_n);
}

4
src/frontends/lean/match_expr.cpp
View file

@ -21,8 +21,8 @@ bool is_match_binder_name(name const & n) { return n == *g_match_name; }
/** \brief Use equations compiler infrastructure to implement match-with */
expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos) {
parser::local_scope scope1(p);
match_definition_scope scope2;
equations_header header = mk_equations_header(scope2.get_name());
match_definition_scope scope2(p.env());
equations_header header = mk_equations_header(scope2.get_name(), scope2.get_actual_name());
buffer<expr> eqns;
buffer<expr> ts;
try {

23
src/frontends/lean/structure_cmd.cpp
View file

@ -274,6 +274,7 @@ struct structure_cmd_fn {
buffer<bool> m_private_parents;
name m_mk;
name m_mk_short;
name m_private_prefix;
pos_info m_mk_pos;
implicit_infer_kind m_mk_infer;
buffer<field_decl> m_fields;
@ -302,6 +303,8 @@ struct structure_cmd_fn {
throw exception("only attribute [class] accepted for structures");
}
bool is_private() const { return m_meta_info.m_modifiers.m_is_private; }
/** \brief Parse structure name and (optional) universe parameters */
void parse_decl_name() {
m_name_pos = m_p.pos();
@ -313,11 +316,10 @@ struct structure_cmd_fn {
m_explicit_universe_params = false;
}
m_given_name = m_p.check_decl_id_next("invalid 'structure', identifier expected");
if (m_meta_info.m_modifiers.m_is_private) {
unsigned h = hash(m_name_pos.first, m_name_pos.second);
auto env_n = add_private_name(m_env, m_given_name, optional<unsigned>(h));
m_env = env_n.first;
m_name = env_n.second;
if (is_private()) {
std::tie(m_env, m_private_prefix) = mk_private_prefix(m_env);
m_name = m_private_prefix + m_given_name;
m_env = register_private_name(m_env, m_given_name, m_name);
} else {
m_name = m_namespace + m_given_name;
}
@ -1019,7 +1021,7 @@ struct structure_cmd_fn {
levels rec_ctx_levels;
if (!is_nil(m_ctx_levels))
rec_ctx_levels = levels(mk_level_placeholder(), m_ctx_levels);
if (m_meta_info.m_modifiers.m_is_private) {
if (is_private()) {
name given_rec_name = name(m_given_name, n.get_string());
m_env = ::lean::add_alias(m_p, m_env, given_rec_name, n, rec_ctx_levels, m_ctx_locals);
} else {
@ -1091,6 +1093,12 @@ struct structure_cmd_fn {
args.push_back(local);
}
name decl_name = name(m_name + field.get_name(), "_default");
name decl_prv_name;
if (is_private()) {
decl_prv_name = name(m_private_prefix + m_given_name + field.get_name(), "_default");
} else {
decl_prv_name = decl_name;
}
/* TODO(Leo): add helper function for adding definition.
It should unfold_untrusted_macros */
expr decl_type = unfold_untrusted_macros(m_env, Pi(args, type));
@ -1103,8 +1111,7 @@ struct structure_cmd_fn {
declaration new_decl = mk_definition_inferring_trusted(m_env, decl_name, decl_lvls,
decl_type, decl_value, reducibility_hints::mk_abbreviation());
m_env = module::add(m_env, check(m_env, new_decl));
m_env = mk_simple_equation_lemma_for(m_env, m_p.get_options(),
m_meta_info.m_modifiers.m_is_private, decl_name, args.size());
m_env = mk_simple_equation_lemma_for(m_env, m_p.get_options(), is_private(), decl_name, decl_prv_name, args.size());
m_env = set_reducible(m_env, decl_name, reducible_status::Reducible, true);
}
}

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

@ -1406,10 +1406,12 @@ eqn_compiler_result mk_nonrec(environment & env, options const & opts, metavar_c
congruence closure modules make them "believe" that this is
a dependent function.
*/
expr fn_type = get_fn_type_from_eqns(eqns);
expr fn_type = get_fn_type_from_eqns(eqns);
name fn_name = head(header.m_fn_names);
name fn_actual_name = head(header.m_fn_actual_names);
expr fn;
std::tie(env, fn) = mk_aux_definition(env, opts, mctx, lctx, header, head(header.m_fn_names), fn_type, R.m_fn);
name fn_name = const_name(get_app_fn(fn));
std::tie(env, fn) = mk_aux_definition(env, opts, mctx, lctx, header,
fn_name, fn_actual_name, fn_type, R.m_fn);
unsigned eqn_idx = 1;
type_context ctx2(env, opts, mctx, lctx, transparency_mode::Semireducible);
for (expr type : R.m_lemmas) {
@ -1425,7 +1427,7 @@ eqn_compiler_result mk_nonrec(environment & env, options const & opts, metavar_c
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,
env = mk_equation_lemma(env, opts, mctx, ctx2.lctx(), fn_name, fn_actual_name,
eqn_idx, header.m_is_private, locals.as_buffer(), new_lhs, rhs);
eqn_idx++;
}

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

@ -43,6 +43,7 @@ bool operator==(equations_header const & h1, equations_header const & h2) {
return
h1.m_num_fns == h2.m_num_fns &&
h1.m_fn_names == h2.m_fn_names &&
h1.m_fn_actual_names == h2.m_fn_actual_names &&
h1.m_is_private == h2.m_is_private &&
h1.m_is_lemma == h2.m_is_lemma &&
h1.m_is_meta == h2.m_is_meta &&
@ -64,6 +65,7 @@ public:
s << *g_equations_opcode << m_header.m_num_fns << m_header.m_is_private << m_header.m_is_meta
<< m_header.m_is_noncomputable << m_header.m_is_lemma << m_header.m_aux_lemmas;
write_list(s, m_header.m_fn_names);
write_list(s, m_header.m_fn_actual_names);
}
virtual bool operator==(macro_definition_cell const & other) const override {
if (auto other_ptr = dynamic_cast<equations_macro_cell const *>(&other)) {
@ -272,6 +274,7 @@ void initialize_equations() {
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);
h.m_fn_actual_names = read_list<name>(d);
if (num == 0 || h.m_num_fns == 0)
throw corrupted_stream_exception();
if (!is_lambda_equation(args[num-1]) && !is_lambda_no_equation(args[num-1])) {

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

@ -32,7 +32,8 @@ 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 */
list<name> m_fn_names; /* local names for functions */
list<name> m_fn_actual_names; /* Full qualified name and/or private name */
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 */

24
src/library/equations_compiler/pack_mutual.cpp
View file

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#include "kernel/instantiate.h"
#include "library/constants.h"
#include "library/trace.h"
#include "library/private.h"
#include "library/app_builder.h"
#include "library/type_context.h"
#include "library/locals.h"
@ -150,17 +151,25 @@ struct pack_mutual_fn {
buffer<expr> domains;
buffer<expr> codomains;
level codomains_lvl;
equations_header header = get_equations_header(e);
name new_fn_name("_mutual");
name new_fn_actual_name;
if (header.m_is_private) {
new_fn_actual_name = name(*get_private_prefix(m_ctx.env(), head(header.m_fn_actual_names)), "_mutual");
} else {
new_fn_actual_name = "_mutual";
}
for (unsigned fidx = 0; fidx < ues.get_num_fns(); fidx++) {
expr const & fn = ues.get_fn(fidx);
new_fn_name = new_fn_name + mlocal_pp_name(fn);
new_fn_name = new_fn_name + mlocal_pp_name(fn);
new_fn_actual_name = new_fn_actual_name + mlocal_pp_name(fn);
lean_assert(ues.get_arity_of(fidx) == 1);
expr fn_type = m_ctx.relaxed_whnf(m_ctx.infer(fn));
expr fn_type = m_ctx.relaxed_whnf(m_ctx.infer(fn));
lean_assert(is_pi(fn_type));
domains.push_back(binding_domain(fn_type));
expr y = locals.push_local("_s", binding_domain(fn_type));
expr c = instantiate(binding_body(fn_type), y);
level c_lvl = get_level(m_ctx, c);
expr y = locals.push_local("_s", binding_domain(fn_type));
expr c = instantiate(binding_body(fn_type), y);
level c_lvl = get_level(m_ctx, c);
if (fidx == 0) {
codomains_lvl = c_lvl;
} else if (!m_ctx.is_def_eq(mk_sort(c_lvl), mk_sort(codomains_lvl))) {
@ -178,8 +187,9 @@ struct pack_mutual_fn {
trace_debug_mutual(tout() << "new function " << new_fn_name << " : " << new_fn_type << "\n";);
equations_header new_header = get_equations_header(e);
new_header.m_fn_names = to_list(new_fn_name);
new_header.m_num_fns = 1;
new_header.m_fn_names = to_list(new_fn_name);
new_header.m_fn_actual_names = to_list(new_fn_actual_name);
new_header.m_num_fns = 1;
replace_fns replacer(m_ctx, ues, new_fn);

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

@ -708,7 +708,9 @@ struct structural_rec_fn {
} else {
expr r;
std::tie(m_env, r) = mk_aux_definition(m_env, m_opts, m_mctx, m_lctx, m_header,
head(m_header.m_fn_names), m_fn_type, new_fn);
head(m_header.m_fn_names),
head(m_header.m_fn_actual_names),
m_fn_type, new_fn);
return r;
}
}
@ -926,7 +928,6 @@ struct structural_rec_fn {
}
void mk_lemmas(expr const & fn, list<expr> const & lemmas) {
name const & fn_name = const_name(get_app_fn(fn));
unsigned eqn_idx = 1;
type_context ctx = mk_type_context();
for (expr type : lemmas) {
@ -951,7 +952,9 @@ struct structural_rec_fn {
if (local != F)
new_locals.push_back(local);
}
m_env = mk_equation_lemma(m_env, m_opts, m_mctx, ctx.lctx(), fn_name,
name const & fn_name = head(m_header.m_fn_names);
name const & fn_actual_name = head(m_header.m_fn_actual_names);
m_env = mk_equation_lemma(m_env, m_opts, m_mctx, ctx.lctx(), fn_name, fn_actual_name,
eqn_idx, m_header.m_is_private, new_locals, new_lhs, new_rhs);
eqn_idx++;
}

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

@ -12,6 +12,7 @@ Author: Leonardo de Moura
#include "kernel/scope_pos_info_provider.h"
#include "kernel/free_vars.h"
#include "library/util.h"
#include "library/aliases.h"
#include "library/trace.h"
#include "library/app_builder.h"
#include "library/private.h"
@ -256,14 +257,6 @@ local_context erase_inaccessible_annotations(local_context const & lctx) {
return r;
}
static pair<environment, name> mk_def_name(environment const & env, bool is_private, name const & c) {
if (is_private) {
return mk_private_name(env, c);
} else {
return mk_pair(env, c);
}
}
static void throw_mk_aux_definition_error(local_context const & lctx, name const & c, expr const & type, expr const & value, exception & ex) {
sstream strm;
strm << "equation compiler failed to create auxiliary declaration '" << c << "'";
@ -274,7 +267,7 @@ static void throw_mk_aux_definition_error(local_context const & lctx, name const
}
pair<environment, expr> mk_aux_definition(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,
equations_header const & header, name const & c, expr const & type, expr const & value) {
equations_header const & header, name const & c, name const & actual_c, expr const & type, expr const & value) {
lean_trace("eqn_compiler", tout() << "declaring auxiliary definition\n" << c << " : " << type << "\n";);
environment new_env = env;
expr new_type = type;
@ -284,8 +277,11 @@ pair<environment, expr> mk_aux_definition(environment const & env, options const
new_type = zeta_expand(lctx, new_type);
new_value = zeta_expand(lctx, new_value);
}
name new_c;
std::tie(new_env, new_c) = mk_def_name(env, header.m_is_private, c);
name new_c = actual_c;
if (header.m_is_private) {
new_env = register_private_name(env, c, actual_c);
new_env = add_expr_alias(new_env, c, actual_c);
}
expr r;
try {
std::tie(new_env, r) = header.m_is_lemma ?
@ -330,10 +326,12 @@ static pair<environment, expr> abstract_rhs_nested_proofs(environment const & en
}
static environment add_equation_lemma(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,
bool is_private, name const & f_name, name const & eqn_name, expr const & type, expr const & value) {
bool is_private, name const & f_name, name const & eqn_name, name const & eqn_actual_name, expr const & type, expr const & value) {
environment new_env = env;
name new_eqn_name;
std::tie(new_env, new_eqn_name) = mk_def_name(env, is_private, eqn_name);
name new_eqn_name = eqn_actual_name;
if (is_private) {
new_env = register_private_name(env, eqn_name, eqn_actual_name);
}
expr r;
expr new_type = erase_inaccessible_annotations(type);
expr new_value = value;
@ -701,25 +699,26 @@ static expr cleanup_equation_rhs(expr const & rhs) {
}
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,
name const & f_name, name const & f_actual_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 proof = prove_eqn_lemma(ctx, Hs, lhs, rhs);
expr new_rhs = cleanup_equation_rhs(rhs);
expr type = ctx.mk_pi(Hs, mk_eq(ctx, lhs, new_rhs));
name eqn_name = mk_equation_name(f_name, eqn_idx);
return add_equation_lemma(env, opts, mctx, lctx, is_private, f_name, eqn_name, type, proof);
expr proof = prove_eqn_lemma(ctx, Hs, lhs, rhs);
expr new_rhs = cleanup_equation_rhs(rhs);
expr type = ctx.mk_pi(Hs, mk_eq(ctx, lhs, new_rhs));
name eqn_name = mk_equation_name(f_name, eqn_idx);
name eqn_actual_name = mk_equation_name(f_actual_name, eqn_idx);
return add_equation_lemma(env, opts, mctx, lctx, is_private, f_name, eqn_name, eqn_actual_name, type, proof);
}
environment mk_simple_equation_lemma_for(environment const & env, options const & opts, bool is_private, name const & c, unsigned arity) {
environment mk_simple_equation_lemma_for(environment const & env, options const & opts, bool is_private, name const & c, name const & c_actual, unsigned arity) {
if (!env.find(get_eq_name())) return env;
if (!get_eqn_compiler_lemmas(opts)) return env;
declaration d = env.get(c);
declaration d = env.get(c_actual);
type_context ctx(env, transparency_mode::All);
expr type = d.get_type();
expr value = d.get_value();
expr lhs = mk_constant(c, param_names_to_levels(d.get_univ_params()));
expr lhs = mk_constant(c_actual, param_names_to_levels(d.get_univ_params()));
type_context::tmp_locals locals(ctx);
for (unsigned i = 0; i < arity; i++) {
type = ctx.relaxed_whnf(type);
@ -731,10 +730,11 @@ environment mk_simple_equation_lemma_for(environment const & env, options const
type = instantiate(binding_body(type), x);
value = instantiate(binding_body(value), x);
}
name eqn_name = mk_equation_name(c, 1);
expr eqn_type = locals.mk_pi(mk_eq(ctx, lhs, value));
expr eqn_proof = locals.mk_lambda(mk_eq_refl(ctx, lhs));
return add_equation_lemma(env, opts, metavar_context(), ctx.lctx(), is_private, c, eqn_name, eqn_type, eqn_proof);
name eqn_name = mk_equation_name(c, 1);
name eqn_actual_name = mk_equation_name(c_actual, 1);
expr eqn_type = locals.mk_pi(mk_eq(ctx, lhs, value));
expr eqn_proof = locals.mk_lambda(mk_eq_refl(ctx, lhs));
return add_equation_lemma(env, opts, metavar_context(), ctx.lctx(), is_private, c_actual, eqn_name, eqn_actual_name, eqn_type, eqn_proof);
}
bool is_name_value(expr const & e) {

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

@ -82,11 +82,17 @@ bool has_inaccessible_annotation(expr const & e);
/* See comment at library/local_context.h */
local_context erase_inaccessible_annotations(local_context const & lctx);
pair<environment, expr> mk_aux_definition(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,
equations_header const & header, name const & n, expr const & type, expr const & value);
/* Create an auxiliary definition.
Remark: `n` is the local name, and `actual_n` the kernel unique name.
`n` and `actual_n` are different for scoped/private declarations.
*/
pair<environment, expr> mk_aux_definition(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,
equations_header const & header, name const & n, name const & actual_n, expr const & type, expr const & value);
/* Create an equation lemma #eqn_idx for f_name/f_actual_name. */
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,
name const & f_name, name const & f_actual_name, unsigned eqn_idx, bool is_private,
buffer<expr> const & Hs, expr const & lhs, expr const & rhs);
/* Create an equational lemma for definition c based on its value.
@ -97,8 +103,13 @@ environment mk_equation_lemma(environment const & env, options const & opts, met
The proof is by reflexivity.
This function is used to make sure we have equations for all definitions. */
environment mk_simple_equation_lemma_for(environment const & env, options const & opts, bool is_private, name const & c, unsigned arity);
This function is used to make sure we have equations for all definitions.
Remark: `c` is the local name, and `c_actual` the kernel unique name.
`c` and `c_actual` are different for scoped/private declarations.
*/
environment mk_simple_equation_lemma_for(environment const & env, options const & opts, bool is_private, name const & c, name const & c_actual, unsigned arity);
name mk_equation_name(name const & f_name, unsigned eqn_idx);

38
src/library/equations_compiler/wf_rec.cpp
View file

@ -277,7 +277,8 @@ struct wf_rec_fn {
expr fn_type = ctx.infer(fn);
expr r;
std::tie(m_env, r) = mk_aux_definition(m_env, m_opts, m_mctx, m_lctx, header,
head(header.m_fn_names), fn_type, fn);
head(header.m_fn_names), head(header.m_fn_actual_names),
fn_type, fn);
return r;
}
@ -314,8 +315,8 @@ struct wf_rec_fn {
return mk_lemma_rhs_fn(ctx, fn, F)(rhs);
}
void mk_lemmas(expr const & fn, list<expr> const & lemmas) {
name const & fn_name = const_name(get_app_fn(fn));
void mk_lemmas(name const & fn_name, expr const & fn, list<expr> const & lemmas) {
name const & fn_prv_name = const_name(get_app_fn(fn));
unsigned eqn_idx = 1;
type_context ctx = mk_type_context();
for (expr type : lemmas) {
@ -331,7 +332,7 @@ struct wf_rec_fn {
expr new_lhs = mk_app(fn, app_arg(lhs));
expr new_rhs = mk_lemma_rhs(ctx, fn, rhs);
trace_debug_wf_aux(tout() << "aux equation [" << eqn_idx << "]:\n" << new_lhs << "\n=\n" << new_rhs << "\n";);
m_env = mk_equation_lemma(m_env, m_opts, m_mctx, ctx.lctx(), fn_name,
m_env = mk_equation_lemma(m_env, m_opts, m_mctx, ctx.lctx(), fn_name, fn_prv_name,
eqn_idx, m_header.m_is_private, locals.as_buffer(), new_lhs, new_rhs);
eqn_idx++;
}
@ -427,7 +428,8 @@ struct wf_rec_fn {
eqn_compiler_result unpack(expr const & packed_fn, expr const & eqns_before_pack,
list<list<expr>> const & counter_example_args) {
equations_header const & header = get_equations_header(eqns_before_pack);
list<name> fn_names = header.m_fn_names;
list<name> fn_names = header.m_fn_names;
list<name> fn_actual_names = header.m_fn_actual_names;
type_context ctx = mk_type_context();
buffer<expr> result_fns;
expr packed_fn_type = ctx.relaxed_whnf(ctx.infer(packed_fn));
@ -445,14 +447,17 @@ struct wf_rec_fn {
expr arg = args.push_local_from_binding(it);
it = instantiate(binding_body(it), arg);
}
expr sigma_mk = mk_sigma(ctx, 0, args.as_buffer()).first;
expr packed_arg = mk_mutual_arg(ctx, sigma_mk, fidx, num_fns, packed_domain);
expr fn_val = args.mk_lambda(mk_app(packed_fn, packed_arg));
name fn_name = head(fn_names);
fn_names = tail(fn_names);
expr sigma_mk = mk_sigma(ctx, 0, args.as_buffer()).first;
expr packed_arg = mk_mutual_arg(ctx, sigma_mk, fidx, num_fns, packed_domain);
expr fn_val = args.mk_lambda(mk_app(packed_fn, packed_arg));
name fn_name = head(fn_names);
name fn_actual_name = head(fn_actual_names);
fn_names = tail(fn_names);
fn_actual_names = tail(fn_actual_names);
trace_debug_wf(tout() << fn_name << " := " << fn_val << "\n";);
expr r;
std::tie(m_env, r) = mk_aux_definition(m_env, m_opts, m_mctx, m_lctx, header, fn_name, fn_type, fn_val);
std::tie(m_env, r) = mk_aux_definition(m_env, m_opts, m_mctx, m_lctx, header, fn_name, fn_actual_name,
fn_type, fn_val);
result_fns.push_back(r);
}
ctx.set_env(m_env);
@ -530,9 +535,10 @@ struct wf_rec_fn {
if (header.m_num_fns > 1) {
eqns = pack_mutual(eqns);
} else {
equations_header new_header = header;
new_header.m_fn_names = to_list(name(head(header.m_fn_names), "_pack"));
eqns = update_equations(eqns, new_header);
equations_header new_header = header;
new_header.m_fn_names = to_list(name(head(header.m_fn_names), "_pack"));
new_header.m_fn_actual_names = to_list(name(head(header.m_fn_actual_names), "_pack"));
eqns = update_equations(eqns, new_header);
}
/* Retrieve well founded relation */
@ -556,7 +562,9 @@ struct wf_rec_fn {
trace_debug_wf(tout() << "after mk_fix\n" << fn << " :\n " << mk_type_context().infer(fn) << "\n";);
if (m_header.m_aux_lemmas) {
lean_assert(!m_header.m_is_meta);
mk_lemmas(fn, r.m_lemmas);
equations_header const & header = get_equations_header(eqns);
name const & fn_name = head(header.m_fn_names);
mk_lemmas(fn_name, fn, r.m_lemmas);
}
return unpack(fn, before_pack, r.m_counter_examples);

100
src/library/private.cpp
View file

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#include <utility>
#include <string>
#include "util/hash.h"
#include "util/sstream.h"
#include "library/private.h"
#include "library/module.h"
#include "library/fingerprint.h"
@ -15,6 +16,9 @@ namespace lean {
struct private_ext : public environment_extension {
unsigned m_counter;
name_map<name> m_inv_map; // map: hidden-name -> user-name
/* We store private prefixes to make sure register_private_name is used correctly.
This information does not need to be stored in .olean files. */
name_set m_private_prefixes;
private_ext():m_counter(0) {}
};
@ -60,21 +64,26 @@ struct private_modification : public modification {
}
};
// Make sure the mapping "hidden-name r ==> user-name n" is preserved when we close sections and
// export .olean files.
/* Make sure the mapping "hidden-name r ==> user-name n" is preserved when we close sections and
export .olean files. */
static environment preserve_private_data(environment const & env, name const & r, name const & n) {
return module::add(env, std::make_shared<private_modification>(n, r));
}
pair<environment, name> add_private_name(environment const & env, name const & n, optional<unsigned> const & extra_hash) {
private_ext ext = get_extension(env);
unsigned h = hash(n.hash(), ext.m_counter);
uint64 f = get_fingerprint(env);
h = hash(h, static_cast<unsigned>(f >> 32));
h = hash(h, static_cast<unsigned>(f));
static name mk_private_name_core(environment const & env, name const & n, optional<unsigned> const & extra_hash) {
private_ext const & ext = get_extension(env);
unsigned h = hash(n.hash(), ext.m_counter);
uint64 f = get_fingerprint(env);
h = hash(h, static_cast<unsigned>(f >> 32));
h = hash(h, static_cast<unsigned>(f));
if (extra_hash)
h = hash(h, *extra_hash);
name r = name(*g_private, h) + n;
return name(*g_private, h) + n;
}
pair<environment, name> add_private_name(environment const & env, name const & n, optional<unsigned> const & extra_hash) {
name r = mk_private_name_core(env, n, extra_hash);
private_ext ext = get_extension(env);
ext.m_inv_map.insert(r, n);
ext.m_counter++;
environment new_env = update(env, ext);
@ -82,6 +91,69 @@ pair<environment, name> add_private_name(environment const & env, name const & n
return mk_pair(new_env, r);
}
static unsigned mk_extra_hash_using_pos() {
unsigned h = 31;
if (auto pinfo = get_pos_info_provider()) {
h = hash(pinfo->get_some_pos().first, pinfo->get_some_pos().second);
char const * fname = pinfo->get_file_name();
h = hash_str(strlen(fname), fname, h);
}
return h;
}
pair<environment, name> mk_private_name(environment const & env, name const & c) {
return add_private_name(env, c, optional<unsigned>(mk_extra_hash_using_pos()));
}
pair<environment, name> mk_private_prefix(environment const & env, optional<unsigned> const & extra_hash) {
name r = mk_private_name_core(env, name(), extra_hash);
private_ext ext = get_extension(env);
ext.m_private_prefixes.insert(r);
ext.m_counter++;
environment new_env = update(env, ext);
return mk_pair(new_env, r);
}
pair<environment, name> mk_private_prefix(environment const & env) {
return mk_private_prefix(env, optional<unsigned>(mk_extra_hash_using_pos()));
}
static optional<name> get_private_prefix(private_ext const & ext, name n) {
while (true) {
if (ext.m_private_prefixes.contains(n))
return optional<name>(n);
if (n.is_atomic())
return optional<name>();
n = n.get_prefix();
}
}
/* Return true iff a prefix of `n` is registered as a private prefix in `ext` */
static bool has_private_prefix(private_ext const & ext, name n) {
return static_cast<bool>(get_private_prefix(ext, n));
}
optional<name> get_private_prefix(environment const & env, name const & n) {
private_ext const & ext = get_extension(env);
return get_private_prefix(ext, n);
}
bool has_private_prefix(environment const & env, name const & n) {
private_ext const & ext = get_extension(env);
return has_private_prefix(ext, n);
}
environment register_private_name(environment const & env, name const & n, name const & prv_n) {
private_ext ext = get_extension(env);
if (!has_private_prefix(ext, prv_n)) {
/* TODO(Leo): consider using an assertion */
throw exception(sstream() << "failed to register private name '" << prv_n << "', prefix has not been registered");
}
ext.m_inv_map.insert(prv_n, n);
environment new_env = update(env, ext);
return preserve_private_data(new_env, prv_n, n);
}
optional<name> hidden_to_user_name(environment const & env, name const & n) {
auto it = get_extension(env).m_inv_map.find(n);
return it ? optional<name>(*it) : optional<name>();
@ -91,16 +163,6 @@ bool is_private(environment const & env, name const & n) {
return static_cast<bool>(hidden_to_user_name(env, n));
}
pair<environment, name> mk_private_name(environment const & env, name const & c) {
unsigned h = 31;
if (auto pinfo = get_pos_info_provider()) {
h = hash(pinfo->get_some_pos().first, pinfo->get_some_pos().second);
char const * fname = pinfo->get_file_name();
h = hash_str(strlen(fname), fname, h);
}
return add_private_name(env, c, optional<unsigned>(h));
}
void initialize_private() {
g_ext = new private_ext_reg();
g_private = new name("_private");

19
src/library/private.h
View file

@ -32,9 +32,28 @@ optional<name> hidden_to_user_name(environment const & env, name const & n);
bool is_private(environment const & env, name const & n);
pair<environment, name> mk_private_prefix(environment const & env, name const & n, optional<unsigned> const & base_hash);
/* Create a private name based on \c c and get_pos_info_provider(), and register it using \c add_private_name */
pair<environment, name> mk_private_name(environment const & env, name const & c);
/* Create a private prefix that is going to be use to generate many private names.
This function registers the private prefix in the environment. */
pair<environment, name> mk_private_prefix(environment const & env, optional<unsigned> const & extra_hash);
/* Similar to the previous function, but generate an extra_hash using get_pos_info_provider */
pair<environment, name> mk_private_prefix(environment const & env);
/* Register a \c n as the name for private name \c prv_n. \c prv_n must have been constructed using
a prefix returned by \c mk_private_prefix. */
environment register_private_name(environment const & env, name const & n, name const & prv_n);
/* Return true iff a prefix of `n` is registered as a private prefix in the given environment. */
bool has_private_prefix(environment const & env, name const & n);
/* Return some name iff a prefix of `n` is registered as a private prefix in the given environment. */
optional<name> get_private_prefix(environment const & env, name const & n);
void initialize_private();
void finalize_private();
}

62
tests/lean/run/1804a.lean Normal file
View file

@ -0,0 +1,62 @@
section
parameter P : match unit.star with
| unit.star := true
end
include P
example : false :=
begin
dsimp [_match_1] at P,
guard_hyp P := true,
admit
end
end
section
parameter P : match unit.star with
| unit.star := true
end
include P
example : false :=
begin
dsimp [_match_1] at P,
guard_hyp P := true,
admit
end
end
section
parameter P : match unit.star with
| unit.star := true
end
parameter Q : match unit.star with
| unit.star := true
end
section
include P
example : false :=
begin
dsimp [_match_1] at P,
guard_hyp P := true,
admit
end
end
section
include Q
example : false :=
begin
dsimp [_match_2] at Q,
guard_hyp Q := true,
admit
end
end
end

41
tests/lean/run/1804b.lean Normal file
View file

@ -0,0 +1,41 @@
namespace bla
private def foo (x : nat) : nat :=
match x with
| 0 := 1
| _ := 2
end
example (a : nat) (h : a = foo 0) : a = 1 :=
begin
simp [foo] at h,
guard_hyp h := a = 1,
exact h
end
example (a b : nat) (p : b = 0) (h : a = foo b) : a = 1 :=
begin
simp [foo] at h,
simp [p] at h,
simp [foo._match_1] at h,
guard_hyp h := a = 1,
exact h
end
example (a b : nat) (p : b = 0) (h : a = foo b) : a = 1 :=
begin
simp [foo] at h,
simp [p] at h,
simp [foo] at h,
guard_hyp h := a = 1,
exact h
end
example (a b : nat) (p : b = 0) (h : a = foo b) : a = 1 :=
begin
simp [foo, p] at h,
guard_hyp h := a = 1,
exact h
end
end bla

7
tests/lean/run/let3.lean
View file

@ -1,4 +1,3 @@
definition p1 := (10, 20, 30)
definition v1 : nat :=
@ -44,3 +43,9 @@ in c + d
example : v3 = 50 :=
rfl
#check
(let (a, b, c) := p1 in a + b : nat) -- We have to provide the type.
#reduce
(let (a, b, c) := p1 in a + b : nat) -- We have to provide the type.