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

fix(frontends/lean): propagate position information

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-16 13:00:35 -07:00
parent 2312f43443
commit f1e3449aae
5 changed files with 28 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -74,6 +74,7 @@ static void update_parameters(buffer<name> & ls_buffer, name_set const & found,
}
environment variable_cmd_core(parser & p, bool is_axiom, binder_info const & bi) {
auto pos = p.pos();
name n = p.check_id_next("invalid declaration, identifier expected");
check_atomic(n);
buffer<name> ls_buffer;
@ -104,7 +105,7 @@ environment variable_cmd_core(parser & p, bool is_axiom, binder_info const & bi)
}
type = p.elaborate(type, ls);
if (in_section(p.env())) {
p.add_local_expr(n, mk_local(n, n, type), bi);
p.add_local_expr(n, p.save_pos(mk_local(n, n, type), pos), bi);
return p.env();
} else {
environment env = p.env();
@ -313,8 +314,13 @@ environment set_line_cmd(parser & p) {
return p.env();
}
environment exit_cmd(parser &) {
throw interrupt_parser();
}
cmd_table init_cmd_table() {
cmd_table r;
add_cmd(r, cmd_info("exit", "exit", exit_cmd));
add_cmd(r, cmd_info("print", "print a string", print_cmd));
add_cmd(r, cmd_info("universe", "declare a global universe level", universe_cmd));
add_cmd(r, cmd_info("section", "open a new section", section_cmd));

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

@ -48,11 +48,12 @@ static expr parse_let(parser & p, pos_info const & pos) {
if (p.parse_local_notation_decl()) {
return parse_let_body(p, pos);
} else {
name id = p.check_id_next("invalid let declaration, identifier expected");
auto pos = p.pos();
name id = p.check_id_next("invalid let declaration, identifier expected");
expr type, value;
if (p.curr_is_token(g_assign)) {
p.next();
type = mk_expr_placeholder();
type = p.save_pos(mk_expr_placeholder(), pos);
value = p.parse_expr();
} else if (p.curr_is_token(g_colon)) {
p.next();
@ -67,14 +68,14 @@ static expr parse_let(parser & p, pos_info const & pos) {
p.next();
type = p.parse_scoped_expr(ps, lenv);
} else {
type = mk_expr_placeholder();
type = p.save_pos(mk_expr_placeholder(), pos);
}
p.check_token_next(g_assign, "invalid let declaration, ':=' expected");
value = p.parse_scoped_expr(ps, lenv);
type = p.pi_abstract(ps, type);
value = p.lambda_abstract(ps, value);
}
expr l = mk_local(id, id, type);
expr l = p.save_pos(mk_local(id, id, type), pos);
p.add_local(l);
expr body = abstract(parse_let_body(p, pos), l);
return p.save_pos(mk_let(id, type, value, body), pos);

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

@ -538,7 +538,7 @@ void parser::parse_binder_block(buffer<parameter> & r, binder_info const & bi) {
}
for (auto p : names) {
expr arg_type = type ? *type : save_pos(mk_expr_placeholder(), p.first);
expr local = mk_local(p.second, p.second, arg_type);
expr local = save_pos(mk_local(p.second, p.second, arg_type), p.first);
add_local(local);
r.push_back(parameter(p.first, local, bi));
}
@ -604,6 +604,7 @@ expr parser::parse_notation(parse_table t, expr * left) {
buffer<expr> args;
buffer<parameter> ps;
local_environment lenv(m_env);
pos_info binder_pos;
if (left)
args.push_back(*left);
while (true) {
@ -649,24 +650,26 @@ expr parser::parse_notation(parse_table t, expr * left) {
break;
}
case notation::action_kind::Binder:
binder_pos = pos();
ps.push_back(parse_binder());
break;
case notation::action_kind::Binders:
binder_pos = pos();
lenv = parse_binders(ps);
break;
case notation::action_kind::ScopedExpr: {
expr r = parse_scoped_expr(ps, lenv, a.rbp());
if (is_var(a.get_rec(), 0)) {
r = abstract(ps, r, a.use_lambda_abstraction());
r = abstract(ps, r, a.use_lambda_abstraction(), binder_pos);
} else {
unsigned i = ps.size();
while (i > 0) {
--i;
expr const & l = ps[i].m_local;
if (a.use_lambda_abstraction())
r = Fun(l, r, ps[i].m_bi);
r = save_pos(Fun(l, r, ps[i].m_bi), binder_pos);
else
r = Pi(l, r, ps[i].m_bi);
r = save_pos(Pi(l, r, ps[i].m_bi), binder_pos);
args.push_back(r);
r = instantiate_rev(a.get_rec(), args.size(), args.data());
args.pop_back();
@ -816,7 +819,7 @@ expr parser::parse_scoped_expr(unsigned num_params, parameter const * ps, local_
}
}
expr parser::abstract(unsigned num_params, parameter const * ps, expr const & e, bool lambda) {
expr parser::abstract(unsigned num_params, parameter const * ps, expr const & e, bool lambda, pos_info const & p) {
buffer<expr> locals;
for (unsigned i = 0; i < num_params; i++)
locals.push_back(ps[i].m_local);
@ -831,6 +834,7 @@ expr parser::abstract(unsigned num_params, parameter const * ps, expr const & e,
r = mk_lambda(n, type, r, ps[i].m_bi);
else
r = mk_pi(n, type, r, ps[i].m_bi);
r = save_pos(r, p);
}
return r;
}

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

@ -206,10 +206,12 @@ public:
return parse_scoped_expr(num_params, ps, local_environment(m_env), rbp);
}
expr parse_scoped_expr(buffer<parameter> & ps, unsigned rbp = 0) { return parse_scoped_expr(ps.size(), ps.data(), rbp); }
expr abstract(unsigned num_params, parameter const * ps, expr const & e, bool lambda = true);
expr abstract(buffer<parameter> const & ps, expr const & e, bool lambda = true) { return abstract(ps.size(), ps.data(), e, lambda); }
expr lambda_abstract(buffer<parameter> const & ps, expr const & e) { return abstract(ps, e, true); }
expr pi_abstract(buffer<parameter> const & ps, expr const & e) { return abstract(ps, e, false); }
expr abstract(unsigned num_params, parameter const * ps, expr const & e, bool lambda, pos_info const & p);
expr abstract(buffer<parameter> const & ps, expr const & e, bool lambda, pos_info const & p) { return abstract(ps.size(), ps.data(), e, lambda, p); }
expr lambda_abstract(buffer<parameter> const & ps, expr const & e, pos_info const & p) { return abstract(ps, e, true, p); }
expr pi_abstract(buffer<parameter> const & ps, expr const & e, pos_info const & p) { return abstract(ps, e, false, p); }
expr lambda_abstract(buffer<parameter> const & ps, expr const & e) { return lambda_abstract(ps, e, pos_of(e)); }
expr pi_abstract(buffer<parameter> const & ps, expr const & e) { return pi_abstract(ps, e, pos_of(e)); }
tactic parse_tactic(unsigned rbp = 0);

2
src/frontends/lean/token_table.cpp
View file

@ -65,7 +65,7 @@ token_table init_token_table() {
"variables", "{variables}", "[variables]", "[private]", "[inline]", "abbreviation",
"evaluate", "check", "print", "end", "namespace", "section", "import",
"abbreviation", "inductive", "record", "structure", "module", "universe",
"precedence", "infixl", "infixr", "infix", "postfix", "notation", "#setline", nullptr};
"precedence", "infixl", "infixr", "infix", "postfix", "notation", "exit", "#setline", nullptr};
std::pair<char const *, char const *> aliases[] =
{{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},