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

fix(frontends/lean): tactic + variables bug, fixes #315

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-09 14:43:22 -08:00
parent eff3c6b774
commit 3aac26d658
5 changed files with 19 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1102,10 +1102,11 @@ expr parser::id_to_expr(name const & id, pos_info const & p) {
save_overload(*r);
}
if (!r) {
if (m_undef_id_behavior == undef_id_behavior::AssumeConstant)
if (m_undef_id_behavior == undef_id_behavior::AssumeConstant) {
r = save_pos(mk_constant(get_namespace(m_env) + id, ls), p);
else if (m_undef_id_behavior == undef_id_behavior::AssumeLocal)
} else if (m_undef_id_behavior == undef_id_behavior::AssumeLocal) {
r = save_pos(mk_local(id, mk_expr_placeholder()), p);
}
}
if (!r)
throw parser_error(sstream() << "unknown identifier '" << id << "'", p);

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

@ -360,6 +360,7 @@ public:
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_local_decl(expr const & l) const { return is_local(l) && m_local_decls.contains(local_pp_name(l)); }
bool is_local_level_variable(name const & n) const { return m_level_variables.contains(n); }
bool is_local_variable(name const & n) const { return m_variables.contains(n); }
bool is_local_variable(expr const & e) const { return is_local_variable(local_pp_name(e)); }

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

@ -47,8 +47,11 @@ name remove_root_prefix(name const & n) {
// Sort local names by order of occurrence, and copy the associated parameters to ps
void sort_locals(expr_struct_set const & locals, parser const & p, buffer<expr> & ps) {
for (expr const & l : locals)
ps.push_back(l);
for (expr const & l : locals) {
// we only copy the locals that are in p's local context
if (p.is_local_decl(l))
ps.push_back(l);
}
std::sort(ps.begin(), ps.end(), [&](expr const & p1, expr const & p2) {
bool is_var1 = p.is_local_variable(p1);
bool is_var2 = p.is_local_variable(p2);

8
tests/lean/tactic_var_bug.lean Normal file
View file

@ -0,0 +1,8 @@
import tools.tactic logic.prop
variable p : Prop
definition foo (q : Prop) : q → true :=
begin
intro r,
apply true.intro
end

2
tests/lean/tactic_var_bug.lean.expected.out Normal file
View file

@ -0,0 +1,2 @@
type: Pi (q : notation_info (no_info Prop)) (a : q), true
value: fun (q : notation_info (no_info Prop)), (by (begin_end (tactic.and_then (begin_end_element (tactic.intro r)) (begin_end_element (tactic.apply true.intro)))))