max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-05-20 15:30:06 -07:00
parent 22ae065d16
commit 5aff998aa3
1 changed files with 11 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
stage0/src/frontends/lean/brackets.cpp
View file

@ -11,6 +11,7 @@ Author: Leonardo de Moura
#include "frontends/lean/util.h"
#include "frontends/lean/tokens.h"
#include "frontends/lean/structure_instance.h"
#include "frontends/lean/typed_expr.h"
namespace lean {
/* Parse rest of the subtype expression prefix '{' id ':' expr '\\' ... */
@ -95,14 +96,17 @@ static expr parse_structure_instance_core(parser & p, optional<expr> const & src
break;
}
}
optional<expr> expected_type;
if (p.curr_is_token(get_colon_tk())) {
p.next();
expected_type = p.parse_expr();
}
p.check_token_next(get_rcurly_tk(), "invalid structure instance, '}' expected");
return mk_structure_instance(S, fns, fvs, sources, catchall);
}
/* 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);
expr r = mk_structure_instance(S, fns, fvs, sources, catchall);
if (expected_type)
return copy_pos(r, mk_typed_expr(*expected_type, r));
else
return r;
}
/* Parse rest of the structure instance prefix '{' fname ... */
@ -153,9 +157,6 @@ expr parse_curly_bracket(parser & p, unsigned, expr const *, pos_info const & po
p.check_token_next(get_dslash_tk(), "invalid expression, '//' or '|' expected");
return parse_subtype(p, pos, local);
}
} else if (p.curr_is_token(get_period_tk())) {
p.next();
return parse_qualified_structure_instance(p, id, id_pos);
} else if (p.curr_is_token(get_assign_tk())) {
return parse_structure_instance(p, id);
} else if (p.curr_is_token(get_membership_tk()) || p.curr_is_token(get_in_tk())) {