Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(parser): AST tracking and export #608

Closed
wants to merge 6 commits into from
Closed

[Merged by Bors] - feat(parser): AST tracking and export #608

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
452ee6f
AST tracking and export
digama0 Jun 17, 2021
5df7df8
fix(vm_parser.cpp): restore nested context
digama0 Aug 5, 2021
0f8f772
feat(vm_parser): with_input size AST
digama0 Aug 6, 2021
fc5f119
fix(user_command): get AST for command parser
digama0 Aug 16, 2021
43f569a
fix(json.cpp): un-reverse json_of_name
digama0 Aug 23, 2021
8716276
fix warning
digama0 Aug 23, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
1 change: 1 addition & 0 deletions .gitignore
View file
Open in desktop
Expand Up @@ -3,6 +3,7 @@
.#*
*.olean
*.tlean
*.ast.json
*.lock
build
GPATH
Expand Down
111 changes: 79 additions & 32 deletions src/frontends/lean/brackets.cpp
View file
Open in desktop
Expand Up @@ -15,22 +15,24 @@ Author: Leonardo de Moura

namespace lean {
/* Parse rest of the subtype expression prefix '{' id ':' expr '\\' ... */
static expr parse_subtype(parser & p, pos_info const & pos, expr const & local) {
static expr parse_subtype(parser & p, pos_info const & pos, ast_data & parent, expr const & local) {
parser::local_scope scope(p);
p.add_local(local);
expr pred = p.parse_expr();
p.check_token_next(get_rcurly_tk(), "invalid subtype, '}' expected");
parent.push(p.get_id(pred));
bool use_cache = false;
pred = p.save_pos(Fun(local, pred, use_cache), pos);
expr subtype = p.save_pos(mk_constant(get_subtype_name()), pos);
return p.mk_app(subtype, pred, pos);
}

/* Parse rest of the set_of expression prefix '{' id ':' expr '|' ... */
static expr parse_set_of(parser & p, pos_info const & pos, expr const & local) {
static expr parse_set_of(parser & p, pos_info const & pos, ast_data & parent, expr const & local) {
parser::local_scope scope(p);
p.add_local(local);
expr pred = p.parse_expr();
parent.push(p.get_id(pred));
p.check_token_next(get_rcurly_tk(), "invalid set_of, '}' expected");
bool use_cache = false;
pred = p.save_pos(Fun(local, pred, use_cache), pos);
Expand All @@ -45,7 +47,8 @@ static expr parse_set_replacement(parser & p, pos_info const & pos, expr const &
// So we parse the binders, assemble an expression for the characteristic predicate,
// then use `patexpr_to_expr` to do the updating.
buffer<expr> params;
auto env = p.parse_binders(params, false);
auto& bis = p.new_ast("binders", p.pos());
auto env = p.parse_binders(&bis, params, false);
p.check_token_next(get_rcurly_tk(), "invalid set_replacement, '}' expected");

// The predicate will look like `λ _x, ∃ p_1, ∃ p_2, ..., hole_expr[p_1, p_2, ...] = _x`.
Expand All @@ -65,7 +68,9 @@ static expr parse_set_replacement(parser & p, pos_info const & pos, expr const &
// Update identifiers so globals are actually globals.
pred = p.patexpr_to_expr_core(pred);
// `{_x | ∃ p_1, ∃ p_2, ..., hole_expr[p_1, p_2, ...] = _x}`
return p.mk_app(mk_constant(get_set_of_name()), pred, pos);
pred = p.mk_app(mk_constant(get_set_of_name()), pred, pos);
p.set_ast_pexpr(p.new_ast("set_replacement", pos).push(p.get_id(hole_expr)).push(bis.m_id).m_id, pred);
return pred;
}

/* Create singletoncollection for '{' expr '}' */
Expand All @@ -77,12 +82,14 @@ static expr mk_singleton(parser & p, pos_info const & pos, expr const & e) {
static expr parse_fin_set(parser & p, pos_info const & pos, expr const & e) {
lean_assert(p.curr_is_token(get_comma_tk()) || p.curr_is_token(get_rcurly_tk()));
buffer<pair<pos_info, expr>> stack;
auto& data = p.new_ast("fin_set", pos).push(p.get_id(e));
stack.emplace_back(pos, e);
while (p.curr_is_token(get_comma_tk())) {
auto ins_pos = p.pos();
p.next();
if (p.curr_is_token(get_rcurly_tk())) break;
expr e2 = p.parse_expr();
data.push(p.get_id(e2));
stack.emplace_back(ins_pos, e2);
}
p.check_token_next(get_rcurly_tk(), "invalid explicit finite collection, '}' expected");
Expand All @@ -94,45 +101,61 @@ static expr parse_fin_set(parser & p, pos_info const & pos, expr const & e) {
expr insert = p.save_pos(mk_constant(get_has_insert_insert_name()), e2.first);
r = p.rec_save_pos(mk_app(insert, e2.second, r), e2.first);
}
p.set_ast_pexpr(data.m_id, r);
return r;
}

/* Parse rest of the sep expression '{' id '∈' ... */
static expr parse_sep(parser & p, pos_info const & pos, name const & id) {
static expr parse_sep(parser & p, pos_info const & pos, name const & id, ast_data & id_ast) {
expr s = p.parse_expr();
p.check_token_next(get_bar_tk(), "invalid sep expression, '|' expected");
parser::local_scope scope(p);
expr local = p.save_pos(mk_local(id, p.save_pos(mk_expr_placeholder(), pos)), pos);
p.add_local(local);
expr pred = p.parse_expr();
auto& data = p.new_ast("sep", pos).push(id_ast.m_id).push(p.get_id(s)).push(p.get_id(pred));
p.check_token_next(get_rcurly_tk(), "invalid sep expression, '}' expected");
bool use_cache = false;
pred = p.rec_save_pos(Fun(local, pred, use_cache), pos);
return p.rec_save_pos(mk_app(mk_constant(get_has_sep_sep_name()), pred, s), pos);
expr r = p.rec_save_pos(mk_app(mk_constant(get_has_sep_sep_name()), pred, s), pos);
p.set_ast_pexpr(data.m_id, r);
return r;
}

static expr parse_structure_instance_core(parser & p, optional<expr> const & src = {}, name const & S = {},
buffer<name> fns = {}, buffer<expr> fvs = {}) {
static expr parse_structure_instance_core(parser & p, pos_info const & pos, optional<expr> const & src = {},
name const & S = {}, ast_id S_ast = 0,
buffer<name> fns = {}, buffer<expr> fvs = {}, ast_data * _fields = nullptr) {
buffer<expr> sources;
bool catchall = false;
if (src)
ast_id catchall = 0;
auto& fields = _fields ? *_fields : p.new_ast("fields", pos);
auto& sources_ast = p.new_ast("sources", pos);
auto& data = p.new_ast("structinst", pos).push(S_ast);
ast_id src_id = 0;
if (src) {
sources.push_back(*src);
src_id = p.get_id(*src);
}
data.push(src_id).push(fields.m_id).push(sources_ast.m_id);
bool read_source = false;
while (!p.curr_is_token(get_rcurly_tk())) {
if (p.curr_is_token(get_dotdot_tk())) {
p.next();
if (p.curr_is_token(get_rcurly_tk())) {
// ", ...}"
catchall = true;
// ", ..}"
catchall = p.new_ast("..", p.pos()).m_id;
break;
}
// ", ...src"
// ", ..src"
sources.push_back(p.parse_expr());
sources_ast.push(p.get_id(sources.back()));
read_source = true;
} else if (!read_source) {
fns.push_back(p.check_id_next("invalid structure instance, identifier expected"));
ast_id id; name n;
std::tie(id, n) = p.check_id_next("invalid structure instance, identifier expected");
fns.push_back(n);
p.check_token_next(get_assign_tk(), "invalid structure instance, ':=' expected");
fvs.push_back(p.parse_expr());
fields.push(p.new_ast(":=", p.pos()).push(id).push(p.get_id(fvs.back())).m_id);
} else {
break;
}
Expand All @@ -143,26 +166,31 @@ static expr parse_structure_instance_core(parser & p, optional<expr> const & src
break;
}
}
data.push(catchall);
p.check_token_next(get_rcurly_tk(), "invalid structure instance, '}' expected");
return mk_structure_instance(S, fns, fvs, sources, catchall);
expr r = mk_structure_instance(S, fns, fvs, sources, catchall);
p.set_ast_pexpr(data.m_id, r);
return r;
}

/* Parse rest of the qualified structure instance prefix '{' S '.' ... */
static expr parse_qualified_structure_instance(parser & p, name S, pos_info const & S_pos) {
S = p.to_constant(S, "invalid structure name", S_pos);
return parse_structure_instance_core(p, none_expr(), S);
static expr parse_qualified_structure_instance(parser & p, pos_info const & pos, name S, ast_data & S_ast) {
S = p.to_constant(S, "invalid structure name", S_ast.m_start);
return parse_structure_instance_core(p, pos, none_expr(), S, S_ast.m_id);
}

/* Parse rest of the structure instance prefix '{' fname ... */
static expr parse_structure_instance(parser & p, name const & fname) {
static expr parse_structure_instance(parser & p, pos_info const & pos, name const & fname, ast_data & fn_ast) {
buffer<name> fns;
buffer<expr> fvs;
fns.push_back(fname);
p.check_token_next(get_assign_tk(), "invalid structure instance, ':=' expected");
fvs.push_back(p.parse_expr());
auto& fields = p.new_ast("fields", pos)
.push(p.new_ast(":=", fn_ast.m_start).push(fn_ast.m_id).push(p.get_id(fvs.back())).m_id);
if (p.curr_is_token(get_comma_tk()))
p.next();
return parse_structure_instance_core(p, none_expr(), name(), fns, fvs);
return parse_structure_instance_core(p, pos, none_expr(), name(), 0, fns, fvs, &fields);
}

static name * g_emptyc_or_emptys = nullptr;
Expand All @@ -175,42 +203,58 @@ expr parse_curly_bracket(parser & p, unsigned, expr const *, pos_info const & po
expr e;
if (p.curr_is_token(get_rcurly_tk())) {
p.next();
return p.save_pos(mk_constant(*g_emptyc_or_emptys), pos);
expr r = p.save_pos(mk_constant(*g_emptyc_or_emptys), pos);
p.set_ast_pexpr(p.new_ast("{}", pos).m_id, r);
return r;
} else if (p.curr_is_identifier()) {
auto id_pos = p.pos();
name id = p.get_name_val();
auto& id_ast = p.new_ast("ident", id_pos, id);
p.next();
if (p.curr_is_token(get_dslash_tk())) {
expr type = p.save_pos(mk_expr_placeholder(), id_pos);
expr local = p.save_pos(mk_local(id, type), id_pos);
p.next();
return parse_subtype(p, pos, local);
auto& data = p.new_ast("subtype", pos).push(id_ast.m_id).push(0);
expr r = parse_subtype(p, pos, data, local);
p.set_ast_pexpr(data.m_id, r);
return r;
} else if (p.curr_is_token(get_bar_tk())) {
expr type = p.save_pos(mk_expr_placeholder(), id_pos);
expr local = p.save_pos(mk_local(id, type), id_pos);
p.next();
return parse_set_of(p, pos, local);
auto& data = p.new_ast("set_of", pos).push(id_ast.m_id).push(0);
expr r = parse_set_of(p, pos, data, local);
p.set_ast_pexpr(data.m_id, r);
return r;

} else if (p.curr_is_token(get_colon_tk())) {
p.next();
expr type = p.parse_expr();
expr local = p.save_pos(mk_local(id, type), id_pos);
if (p.curr_is_token(get_bar_tk())) {
p.next();
return parse_set_of(p, pos, local);
auto& data = p.new_ast("set_of", pos).push(id_ast.m_id).push(p.get_id(type));
expr r = parse_set_of(p, pos, data, local);
p.set_ast_pexpr(data.m_id, r);
return r;
} else {
p.check_token_next(get_dslash_tk(), "invalid expression, '//' or '|' expected");
return parse_subtype(p, pos, local);
auto& data = p.new_ast("subtype", pos).push(id_ast.m_id).push(p.get_id(type));
expr r = parse_subtype(p, pos, data, local);
p.set_ast_pexpr(data.m_id, r);
return r;
}
} else if (p.curr_is_token(get_period_tk())) {
p.next();
return parse_qualified_structure_instance(p, id, id_pos);
return parse_qualified_structure_instance(p, pos, id, id_ast);
} else if (p.curr_is_token(get_assign_tk()) || p.curr_is_token(get_fieldarrow_tk())) {
return parse_structure_instance(p, id);
return parse_structure_instance(p, pos, id, id_ast);
} else if (p.curr_is_token(get_membership_tk()) || p.curr_is_token(get_in_tk())) {
p.next();
return parse_sep(p, pos, id);
return parse_sep(p, pos, id, id_ast);
} else {
expr left = p.id_to_expr(id, id_pos);
expr left = p.id_to_expr(id, id_ast);
unsigned rbp = 0;
while (rbp < p.curr_lbp()) {
left = p.parse_led(left);
Expand All @@ -231,14 +275,17 @@ expr parse_curly_bracket(parser & p, unsigned, expr const *, pos_info const & po
return parse_fin_set(p, pos, p.patexpr_to_expr_core(e));
} else {
p.maybe_throw_error({"invalid set replacement notation, ',', '}', or `|` expected", p.pos()});
return mk_singleton(p, pos, p.patexpr_to_expr_core(e));
ast_id id = p.new_ast("fin_set", pos).push(p.get_id(e)).m_id;
expr r = mk_singleton(p, pos, p.patexpr_to_expr_core(e));
p.set_ast_pexpr(id, r);
return r;
}
} else if (p.curr_is_token(get_period_tk())) {
p.next();
p.check_token_next(get_rcurly_tk(), "invalid empty structure instance, '}' expected");
return p.save_pos(mk_structure_instance(), pos);
} else if (p.curr_is_token(get_dotdot_tk())) {
return parse_structure_instance_core(p);
return parse_structure_instance_core(p, pos);
} else {
e = p.parse_expr();
}
Expand All @@ -249,7 +296,7 @@ expr parse_curly_bracket(parser & p, unsigned, expr const *, pos_info const & po
return parse_fin_set(p, pos, e);
} else if (p.curr_is_token(get_with_tk())) {
p.next();
return parse_structure_instance_core(p, some_expr(e));
return parse_structure_instance_core(p, pos, some_expr(e));
} else {
return p.parser_error_or_expr({"invalid '{' expression, ',', '}', '..', `//` or `|` expected", p.pos()});
}
Expand Down