fix(frontends/lean): intro tactic + universe variables, fixes #362
This commit is contained in:
parent
fca97d5bb2
commit
0443c1e70c
5 changed files with 39 additions and 1 deletions
|
@ -407,7 +407,7 @@ static environment definition_cmd_core(parser & p, def_cmd_kind kind, bool is_op
|
|||
new_locals.append(locals);
|
||||
erase_local_binder_info(new_locals);
|
||||
value = Fun_as_is(new_locals, value, p);
|
||||
update_univ_parameters(ls_buffer, collect_univ_params(value, collect_univ_params(type)), p);
|
||||
update_univ_parameters(ls_buffer, collect_univ_params_ignoring_tactics(value, collect_univ_params_ignoring_tactics(type)), p);
|
||||
remove_local_vars(p, locals);
|
||||
ls = to_list(ls_buffer.begin(), ls_buffer.end());
|
||||
levels local_ls = collect_local_nonvar_levels(p, ls);
|
||||
|
|
|
@ -108,6 +108,28 @@ void collect_locals(expr const & type, expr const & value, parser const & p, buf
|
|||
sort_locals(ls, p, ctx_ps);
|
||||
}
|
||||
|
||||
name_set collect_univ_params_ignoring_tactics(expr const & e, name_set const & ls) {
|
||||
if (!has_param_univ(e)) {
|
||||
return ls;
|
||||
} else {
|
||||
name_set r = ls;
|
||||
for_each(e, [&](expr const & e, unsigned) {
|
||||
if (!has_param_univ(e)) {
|
||||
return false;
|
||||
} else if (is_by(e)) {
|
||||
return false; // do not visit children
|
||||
} else if (is_sort(e)) {
|
||||
collect_univ_params_core(sort_level(e), r);
|
||||
} else if (is_constant(e)) {
|
||||
for (auto const & l : const_levels(e))
|
||||
collect_univ_params_core(l, r);
|
||||
}
|
||||
return true;
|
||||
});
|
||||
return r;
|
||||
}
|
||||
}
|
||||
|
||||
void remove_local_vars(parser const & p, buffer<expr> & locals) {
|
||||
unsigned j = 0;
|
||||
for (unsigned i = 0; i < locals.size(); i++) {
|
||||
|
|
|
@ -28,6 +28,7 @@ name remove_root_prefix(name const & n);
|
|||
levels collect_local_nonvar_levels(parser & p, level_param_names const & ls);
|
||||
/** \brief Collect local constants occurring in \c type and \c value, sort them, and store in ctx_ps */
|
||||
void collect_locals(expr const & type, expr const & value, parser const & p, buffer<expr> & ctx_ps);
|
||||
name_set collect_univ_params_ignoring_tactics(expr const & e, name_set const & ls = name_set());
|
||||
/** \brief Copy the local names to \c ps, then sort \c ps (using the order in which they were declared). */
|
||||
void sort_locals(expr_struct_set const & locals, parser const & p, buffer<expr> & ps);
|
||||
/** \brief Remove from \c ps local constants that are tagged as variables. */
|
||||
|
|
|
@ -9,6 +9,7 @@ Author: Leonardo de Moura
|
|||
#include "kernel/expr.h"
|
||||
#include "kernel/expr_sets.h"
|
||||
namespace lean {
|
||||
void collect_univ_params_core(level const & l, name_set & r);
|
||||
name_set collect_univ_params(expr const & e, name_set const & ls = name_set());
|
||||
void collect_locals(expr const & e, expr_struct_set & ls);
|
||||
level_param_names to_level_param_names(name_set const & ls);
|
||||
|
|
14
tests/lean/run/362.lean
Normal file
14
tests/lean/run/362.lean
Normal file
|
@ -0,0 +1,14 @@
|
|||
variables {a : Type}
|
||||
|
||||
definition foo (A : Type) : A → A :=
|
||||
begin
|
||||
intro a, assumption
|
||||
end
|
||||
|
||||
(*
|
||||
local d = get_env():find("foo")
|
||||
assert(#d:univ_params() == 1)
|
||||
*)
|
||||
|
||||
set_option pp.universes true
|
||||
check foo
|
Loading…
Reference in a new issue