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

feat(frontends/lean/parser): add parse_qualified_expr

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-16 12:42:42 -08:00
parent 6c07ca5d41
commit 13660cfecd
3 changed files with 39 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -384,51 +384,36 @@ static expr parse_ite(parser & p, expr const & c, pos_info const & pos) {
expr t = p.parse_expr(g_then_else_prec);
p.check_token_next(get_else_tk(), "invalid 'if-then-else' expression, 'else' expected");
expr e = p.parse_expr(g_then_else_prec);
return mk_app(mk_constant(*g_ite), c, t, e);
return p.save_pos(mk_app(mk_constant(*g_ite), c, t, e), pos);
}
static expr parse_dite(parser & p, name const & H_name, pos_info const & pos) {
if (!p.env().find(*g_dite))
throw parser_error("invalid use of (dependent) 'if-then-else' expression, environment does "
"not contain 'dite' definition", pos);
expr c = p.parse_expr();
static expr parse_dite(parser & p, name const & H_name, expr const & c, pos_info const & pos) {
p.check_token_next(get_then_tk(), "invalid 'if-then-else' expression, 'then' expected");
expr t, e;
{
parser::local_scope scope(p);
expr H = mk_local(H_name, c);
p.add_local(H);
t = Fun(H, p.parse_expr(g_then_else_prec));
auto pos = p.pos();
t = p.save_pos(Fun(H, p.parse_expr(g_then_else_prec)), pos);
}
p.check_token_next(get_else_tk(), "invalid 'if-then-else' expression, 'else' expected");
{
parser::local_scope scope(p);
expr H = mk_local(H_name, mk_app(*g_not, c));
p.add_local(H);
e = Fun(H, p.parse_expr(g_then_else_prec));
auto pos = p.pos();
e = p.save_pos(Fun(H, p.parse_expr(g_then_else_prec)), pos);
}
return mk_app(mk_constant(*g_dite), c, t, e);
return p.save_pos(mk_app(p.save_pos(mk_constant(*g_dite), pos), c, t, e), pos);
}
static expr parse_if_then_else(parser & p, unsigned, expr const *, pos_info const & pos) {
if (p.curr_is_identifier()) {
auto id_pos = p.pos();
name id = p.get_name_val();
p.next();
if (p.curr_is_token(get_colon_tk())) {
p.next();
return parse_dite(p, id, pos);
} else {
expr e = p.id_to_expr(id, id_pos);
while (!p.curr_is_token(get_then_tk())) {
e = p.parse_led(e);
}
return parse_ite(p, e, pos);
}
} else {
expr c = p.parse_expr();
return parse_ite(p, c, pos);
}
pair<optional<name>, expr> ie = p.parse_qualified_expr();
if (ie.first)
return parse_dite(p, *ie.first, ie.second, pos);
else
return parse_ite(p, ie.second, pos);
}
static expr parse_calc_expr(parser & p, unsigned, expr const *, pos_info const &) {

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

@ -1247,6 +1247,26 @@ expr parser::parse_expr(unsigned rbp) {
return left;
}
pair<optional<name>, expr> parser::parse_qualified_expr(unsigned rbp) {
if (curr_is_identifier()) {
auto id_pos = pos();
name id = get_name_val();
next();
if (curr_is_token(get_colon_tk())) {
next();
return mk_pair(optional<name>(id), parse_expr(rbp));
} else {
expr left = id_to_expr(id, id_pos);
while (rbp < curr_lbp()) {
left = parse_led(left);
}
return mk_pair(optional<name>(), left);
}
} else {
return mk_pair(optional<name>(), parse_expr(rbp));
}
}
expr parser::parse_scoped_expr(unsigned num_ps, expr const * ps, local_environment const & lenv, unsigned rbp) {
local_scope scope(*this);
m_env = lenv;

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

@ -352,6 +352,13 @@ public:
expr id_to_expr(name const & id, pos_info const & p);
expr parse_expr(unsigned rbp = 0);
/**
\brief Parse an (optionally) qualified expression.
If the input is of the form <id> : <expr>, then return the pair (some(id), expr).
Otherwise, parse the next expression and return (none, expr).
*/
pair<optional<name>, expr> parse_qualified_expr(unsigned rbp = 0);
expr parse_led(expr left);
expr parse_scoped_expr(unsigned num_params, expr const * ps, local_environment const & lenv, unsigned rbp = 0);
expr parse_scoped_expr(buffer<expr> const & ps, local_environment const & lenv, unsigned rbp = 0) {