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

refactor(frontends/lean): remove m_pos field from parameter object

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-19 13:13:32 -07:00
parent 2954d10df5
commit 2cc8172d61
2 changed files with 6 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/frontends/lean/parameter.h
View file

@ -10,11 +10,10 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
struct parameter { struct parameter {
pos_info m_pos;
expr m_local; expr m_local;
binder_info m_bi; binder_info m_bi;
parameter(pos_info const & p, expr const & l, binder_info const & bi): parameter(expr const & l, binder_info const & bi):
m_pos(p), m_local(l), m_bi(bi) {} m_local(l), m_bi(bi) {}
parameter():m_pos(0, 0) {} parameter() {}
}; };
} }

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

@ -358,7 +358,7 @@ void parser::add_local_level(name const & n, level const & l) {
} }
void parser::add_local_expr(name const & n, expr const & e, binder_info const & bi) { void parser::add_local_expr(name const & n, expr const & e, binder_info const & bi) {
m_local_decls.insert(n, parameter(pos(), e, bi)); m_local_decls.insert(n, parameter(e, bi));
} }
void parser::add_local(expr const & e) { void parser::add_local(expr const & e) {
@ -566,7 +566,7 @@ parameter parser::parse_binder_core(binder_info const & bi) {
} else { } else {
type = save_pos(mk_expr_placeholder(), p); type = save_pos(mk_expr_placeholder(), p);
} }
return parameter(p, save_pos(mk_local(id, type), p), bi); return parameter(save_pos(mk_local(id, type), p), bi);
} }
parameter parser::parse_binder() { parameter parser::parse_binder() {
@ -610,7 +610,7 @@ void parser::parse_binder_block(buffer<parameter> & r, binder_info const & bi) {
expr arg_type = type ? *type : save_pos(mk_expr_placeholder(), p.first); expr arg_type = type ? *type : save_pos(mk_expr_placeholder(), p.first);
expr local = save_pos(mk_local(p.second, arg_type), p.first); expr local = save_pos(mk_local(p.second, arg_type), p.first);
add_local(local); add_local(local);
r.push_back(parameter(p.first, local, bi)); r.push_back(parameter(local, bi));
} }
} }