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

feat(frontends/lean): add 'using' syntax sugar for adding expressions to the goal's context

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-20 11:18:53 -07:00
parent 5c17411a86
commit 16412daf39
4 changed files with 56 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -20,6 +20,7 @@ static name g_colon(":");
static name g_assign(":=");
static name g_comma(",");
static name g_from("from");
static name g_using("using");
static name g_by("by");
static expr parse_Type(parser & p, unsigned, expr const *, pos_info const & pos) {
@ -102,33 +103,66 @@ static expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) {
static expr parse_proof(parser & p, expr const & prop) {
if (p.curr_is_token(g_from)) {
// parse: 'from' expr
p.next();
return p.parse_expr();
} else if (p.curr_is_token(g_by)) {
// parse: 'by' tactic
auto pos = p.pos();
p.next();
tactic t = p.parse_tactic();
expr r = p.save_pos(mk_expr_placeholder(some_expr(prop)), pos);
p.save_hint(r, t);
return r;
} else if (p.curr_is_token(g_using)) {
// parse: 'using' locals* ',' proof
auto using_pos = p.pos();
p.next();
parser::local_scope scope(p);
buffer<expr> locals;
while (!p.curr_is_token(g_comma)) {
auto id_pos = p.pos();
expr l = p.parse_expr();
if (!is_local(l))
throw parser_error("invalid 'using' declaration for 'have', local expected", id_pos);
p.add_local(l);
locals.push_back(l);
}
p.next(); // consume ','
expr pr = parse_proof(p, prop);
unsigned i = locals.size();
while (i > 0) {
--i;
expr l = locals[i];
pr = p.save_pos(Fun(l, pr), using_pos);
pr = p.save_pos(pr(l), using_pos);
}
return pr;
} else {
throw parser_error("invalid expression, 'by' or 'from' expected", p.pos());
throw parser_error("invalid expression, 'by', 'using' or 'from' expected", p.pos());
}
}
static expr parse_have(parser & p, unsigned, expr const *, pos_info const & pos) {
name id = p.check_id_next("invalid 'have' declaration, identifier expected");
p.check_token_next(g_colon, "invalid 'have' declaration, ':' expected");
expr prop = p.parse_expr();
auto id_pos = p.pos();
name id = p.check_id_next("invalid 'have' declaration, identifier expected");
expr prop;
if (p.curr_is_token(g_colon)) {
p.next();
prop = p.parse_expr();
} else {
prop = p.save_pos(mk_expr_placeholder(), id_pos);
}
p.check_token_next(g_comma, "invalid 'have' declaration, ',' expected");
expr proof = parse_proof(p, prop);
p.check_token_next(g_comma, "invalid 'have' declaration, ',' expected");
parser::local_scope scope(p);
expr l = p.save_pos(mk_local(id, prop), pos);
p.add_local(l);
binder_info bi = mk_contextual_info(false);
p.add_local(l, bi);
expr body = abstract(p.parse_expr(), l);
// remark: mk_contextual_info(false) informs the elaborator that prop should not occur inside metavariables.
expr r = p.save_pos(mk_lambda(id, prop, body, mk_contextual_info(false)), pos);
expr r = p.save_pos(mk_lambda(id, prop, body, bi), pos);
return p.save_pos(mk_app(r, proof), pos);
}

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

@ -357,13 +357,17 @@ void parser::add_local_level(name const & n, level const & l) {
m_local_level_decls.insert(n, l);
}
void parser::add_local_expr(name const & n, expr const & e, binder_info const & bi) {
m_local_decls.insert(n, parameter(e, bi));
void parser::add_local_expr(name const & n, parameter const & p) {
m_local_decls.insert(n, p);
}
void parser::add_local(expr const & e) {
void parser::add_local_expr(name const & n, expr const & e, binder_info const & bi) {
add_local_expr(n, parameter(e, bi));
}
void parser::add_local(expr const & e, binder_info const & bi) {
lean_assert(is_local(e));
add_local_expr(local_pp_name(e), e);
add_local_expr(local_pp_name(e), e, bi);
}
unsigned parser::get_local_level_index(name const & n) const {
@ -609,7 +613,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 = save_pos(mk_local(p.second, arg_type), p.first);
add_local(local);
add_local_expr(p.second, parameter(local, bi));
r.push_back(parameter(local, bi));
}
}
@ -898,7 +902,7 @@ expr parser::parse_scoped_expr(unsigned num_params, parameter const * ps, local_
local_scope scope(*this);
m_env = lenv;
for (unsigned i = 0; i < num_params; i++)
add_local(ps[i].m_local);
add_local(ps[i].m_local, ps[i].m_bi);
return parse_expr(rbp);
}
}

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

@ -224,8 +224,9 @@ public:
struct local_scope { parser & m_p; environment m_env; local_scope(parser & p); ~local_scope(); };
void add_local_level(name const & n, level const & l);
void add_local_expr(name const & n, parameter const & p);
void add_local_expr(name const & n, expr const & e, binder_info const & bi = binder_info());
void add_local(expr const & t);
void add_local(expr const & e, binder_info const & bi = binder_info());
/** \brief Position of the local level declaration named \c n in the sequence of local level decls. */
unsigned get_local_level_index(name const & n) const;
/** \brief Position of the local declaration named \c n in the sequence of local decls. */

4
src/kernel/formatter.cpp
View file

@ -127,6 +127,8 @@ struct print_expr_fn {
out() << "{";
else if (binding_info(e).is_cast())
out() << "[";
else if (!binding_info(e).is_contextual())
out() << "[[";
else
out() << "(";
out() << n << " : ";
@ -135,6 +137,8 @@ struct print_expr_fn {
out() << "}";
else if (binding_info(e).is_cast())
out() << "]";
else if (!binding_info(e).is_contextual())
out() << "]]";
else
out() << ")";
e = p.first;