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

fix(frontends/lean): universe levels associated with section variables should not be fixed in the section

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-04 07:13:19 -07:00
parent 5a927b6db4
commit e71d4548de
7 changed files with 72 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -109,10 +109,10 @@ static environment declare_var(parser & p, environment env,
}
/** \brief If we are in a section, then add the new local levels to it. */
static void update_section_local_levels(parser & p, level_param_names const & new_ls) {
static void update_section_local_levels(parser & p, level_param_names const & new_ls, bool is_variable) {
if (in_section_or_context(p.env())) {
for (auto const & l : new_ls)
p.add_local_level(l, mk_param_univ(l));
p.add_local_level(l, mk_param_univ(l), is_variable);
}
}
@ -169,7 +169,7 @@ environment variable_cmd_core(parser & p, variable_kind k) {
level_param_names new_ls;
list<expr> ctx = locals_to_context(type, p);
std::tie(type, new_ls) = p.elaborate_type(type, ctx);
update_section_local_levels(p, new_ls);
update_section_local_levels(p, new_ls, k == variable_kind::Variable);
return declare_var(p, p.env(), n, append(ls, new_ls), type, k, bi, pos);
}
environment variable_cmd(parser & p) {
@ -210,7 +210,7 @@ static environment variables_cmd_core(parser & p, variable_kind k) {
level_param_names new_ls;
expr new_type;
std::tie(new_type, new_ls) = p.elaborate_type(type, ctx);
update_section_local_levels(p, new_ls);
update_section_local_levels(p, new_ls, k == variable_kind::Variable);
new_ls = append(ls, new_ls);
env = declare_var(p, env, id, new_ls, new_type, k, bi, pos);
}
@ -360,9 +360,8 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque, boo
value = Fun_as_is(section_value_ps, value, p);
update_univ_parameters(ls_buffer, collect_univ_params(value, collect_univ_params(type)), p);
ls = to_list(ls_buffer.begin(), ls_buffer.end());
levels section_ls = collect_section_levels(ls, p);
while (!section_ps.empty() && p.is_section_variable(section_ps.back()))
section_ps.pop_back(); // we do not fix section variables
levels section_ls = collect_section_nonvar_levels(p, ls);
remove_section_variables(p, section_ps);
for (expr & param : section_ps)
param = mk_explicit(param);
expr ref = mk_implicit(mk_app(mk_explicit(mk_constant(real_n, section_ls)), section_ps));

9
src/frontends/lean/inductive_cmd.cpp
View file

@ -605,13 +605,10 @@ struct inductive_cmd_fn {
/** \brief Add aliases for the inductive datatype, introduction and elimination rules */
environment add_aliases(environment env, level_param_names const & ls, buffer<expr> const & section_params,
buffer<inductive_decl> const & decls) {
buffer<expr> section_params_only;
for (expr const & param : section_params) {
if (!m_p.is_section_variable(param))
section_params_only.push_back(param);
}
buffer<expr> section_params_only(section_params);
remove_section_variables(m_p, section_params_only);
// Create aliases/local refs
levels section_levels = collect_section_levels(ls, m_p);
levels section_levels = collect_section_nonvar_levels(m_p, ls);
for (auto & d : decls) {
name d_name = inductive_decl_name(d);
name d_short_name(d_name.get_string());

13
src/frontends/lean/parser.cpp
View file

@ -95,6 +95,7 @@ parser::parser(environment const & env, io_state const & ios,
if (s) {
m_local_level_decls = s->m_lds;
m_local_decls = s->m_eds;
m_level_variables = s->m_lvars;
m_variables = s->m_vars;
m_include_vars = s->m_include_vars;
m_parser_scope_stack = s->m_parser_scope_stack;
@ -408,7 +409,7 @@ void parser::push_local_scope(bool save_options) {
optional<options> opts;
if (save_options)
opts = m_ios.get_options();
m_parser_scope_stack = cons(parser_scope_stack_elem(opts, m_variables, m_include_vars),
m_parser_scope_stack = cons(parser_scope_stack_elem(opts, m_level_variables, m_variables, m_include_vars),
m_parser_scope_stack);
}
@ -421,17 +422,22 @@ void parser::pop_local_scope() {
m_ios.set_options(*s.m_options);
updt_options();
}
m_level_variables = s.m_level_variables;
m_variables = s.m_variables;
m_include_vars = s.m_include_vars;
m_parser_scope_stack = tail(m_parser_scope_stack);
}
void parser::add_local_level(name const & n, level const & l) {
void parser::add_local_level(name const & n, level const & l, bool is_variable) {
if (m_env.is_universe(n))
throw exception(sstream() << "invalid universe declaration, '" << n << "' shadows a global universe");
if (m_local_level_decls.contains(n))
throw exception(sstream() << "invalid universe declaration, '" << n << "' shadows a local universe");
m_local_level_decls.insert(n, l);
if (is_variable) {
lean_assert(is_param(l));
m_level_variables.insert(n);
}
}
void parser::add_local_expr(name const & n, expr const & p, bool is_variable) {
@ -1363,7 +1369,8 @@ void parser::save_snapshot() {
if (!m_snapshot_vector)
return;
if (m_snapshot_vector->empty() || static_cast<int>(m_snapshot_vector->back().m_line) != m_scanner.get_line())
m_snapshot_vector->push_back(snapshot(m_env, m_local_level_decls, m_local_decls, m_variables, m_include_vars,
m_snapshot_vector->push_back(snapshot(m_env, m_local_level_decls, m_local_decls,
m_level_variables, m_variables, m_include_vars,
m_ios.get_options(), m_parser_scope_stack, m_scanner.get_line()));
}

18
src/frontends/lean/parser.h
View file

@ -48,10 +48,11 @@ typedef environment local_environment;
/** \brief Extra data needed to be saved when we execute parser::push_local_scope */
struct parser_scope_stack_elem {
optional<options> m_options;
name_set m_level_variables;
name_set m_variables;
name_set m_include_vars;
parser_scope_stack_elem(optional<options> const & o, name_set const & vs, name_set const & ivs):
m_options(o), m_variables(vs), m_include_vars(ivs) {}
parser_scope_stack_elem(optional<options> const & o, name_set const & lvs, name_set const & vs, name_set const & ivs):
m_options(o), m_level_variables(lvs), m_variables(vs), m_include_vars(ivs) {}
};
typedef list<parser_scope_stack_elem> parser_scope_stack;
@ -60,17 +61,18 @@ struct snapshot {
environment m_env;
local_level_decls m_lds;
local_expr_decls m_eds;
name_set m_vars; // subset of m_eds that is tagged as section variables
name_set m_include_vars; // subset of m_eds that must be includes
name_set m_lvars; // subset of m_lds that is tagged as section level variable
name_set m_vars; // subset of m_eds that is tagged as section variable
name_set m_include_vars; // subset of m_eds that must be included
options m_options;
parser_scope_stack m_parser_scope_stack;
unsigned m_line;
snapshot():m_line(0) {}
snapshot(environment const & env, options const & o):m_env(env), m_options(o), m_line(1) {}
snapshot(environment const & env, local_level_decls const & lds, local_expr_decls const & eds,
name_set const & vars, name_set const & includes, options const & opts,
name_set const & lvars, name_set const & vars, name_set const & includes, options const & opts,
parser_scope_stack const & pss, unsigned line):
m_env(env), m_lds(lds), m_eds(eds), m_vars(vars), m_include_vars(includes),
m_env(env), m_lds(lds), m_eds(eds), m_lvars(lvars), m_vars(vars), m_include_vars(includes),
m_options(opts), m_parser_scope_stack(pss), m_line(line) {}
};
@ -88,6 +90,7 @@ class parser {
scanner::token_kind m_curr;
local_level_decls m_local_level_decls;
local_expr_decls m_local_decls;
name_set m_level_variables;
name_set m_variables; // subset of m_local_decls that is marked as variables
name_set m_include_vars; // subset of m_local_decls that is marked as include
parser_scope_stack m_parser_scope_stack;
@ -323,9 +326,10 @@ public:
expr parse_scoped_expr(buffer<expr> & ps, unsigned rbp = 0) { return parse_scoped_expr(ps.size(), ps.data(), rbp); }
struct local_scope { parser & m_p; environment m_env; local_scope(parser & p); ~local_scope(); };
void add_local_level(name const & n, level const & l);
void add_local_level(name const & n, level const & l, bool is_variable = false);
void add_local_expr(name const & n, expr const & p, bool is_variable = false);
void add_local(expr const & p) { return add_local_expr(local_pp_name(p), p); }
bool is_section_level_variable(name const & n) const { return m_level_variables.contains(n); }
bool is_section_variable(name const & n) const { return m_variables.contains(n); }
bool is_section_variable(expr const & e) const { return is_section_variable(local_pp_name(e)); }
void include_variable(name const & n) { m_include_vars.insert(n); }

16
src/frontends/lean/util.cpp
View file

@ -61,10 +61,10 @@ void sort_section_params(expr_struct_set const & locals, parser const & p, buffe
}
// Return the levels in \c ls that are defined in the section
levels collect_section_levels(level_param_names const & ls, parser & p) {
levels collect_section_nonvar_levels(parser & p, level_param_names const & ls) {
buffer<level> section_ls_buffer;
for (name const & l : ls) {
if (p.get_local_level_index(l))
if (p.get_local_level_index(l) && !p.is_section_level_variable(l))
section_ls_buffer.push_back(mk_param_univ(l));
else
break;
@ -86,6 +86,18 @@ void collect_section_locals(expr const & type, expr const & value, parser const
sort_section_params(ls, p, section_ps);
}
void remove_section_variables(parser const & p, buffer<expr> & ps) {
unsigned j = 0;
for (unsigned i = 0; i < ps.size(); i++) {
expr const & param = ps[i];
if (!is_local(param) || !p.is_section_variable(param)) {
ps[j] = param;
j++;
}
}
ps.shrink(j);
}
list<expr> locals_to_context(expr const & e, parser const & p) {
expr_struct_set ls;
collect_locals(e, ls);

6
src/frontends/lean/util.h
View file

@ -22,12 +22,14 @@ void check_atomic(name const & n);
void check_in_section_or_context(parser const & p);
bool is_root_namespace(name const & n);
name remove_root_prefix(name const & n);
/** \brief Return the levels in \c ls that are defined in the section. */
levels collect_section_levels(level_param_names const & ls, parser & p);
/** \brief Return the levels in \c ls that are defined in the section, but are not tagged as variables. */
levels collect_section_nonvar_levels(parser & p, level_param_names const & ls);
/** \brief Collect local (section) constants occurring in type and value, sort them, and store in section_ps */
void collect_section_locals(expr const & type, expr const & value, parser const & p, buffer<expr> & section_ps);
/** \brief Copy the local parameters to \c section_ps, then sort \c section_ps (using the order in which they were declared). */
void sort_section_params(expr_struct_set const & locals, parser const & p, buffer<expr> & section_ps);
/** \brief Remove from \c ps local constants that are tagged as section variables. */
void remove_section_variables(parser const & p, buffer<expr> & ps);
list<expr> locals_to_context(expr const & e, parser const & p);
/** \brief Fun(locals, e), but also propagate \c e position to result */
expr Fun(buffer<expr> const & locals, expr const & e, parser & p);

24
tests/lean/run/seclvl.lean Normal file
View file

@ -0,0 +1,24 @@
import logic
section
variables (A B C : Type)
definition foo := A → B
check foo A B
check foo B C
check foo A A
end
constants A B C : Type
check foo A B
check foo B C
check foo A A
section
variables (A B C : Type)
definition foo2 := A → B
check foo2 A B
check foo2 B C
check foo2 A A
end