From 5aff998aa3e4e0a3c5cee20b60e1a925a8448d52 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 May 2020 15:30:06 -0700 Subject: [PATCH] chore: update stage0 --- stage0/src/frontends/lean/brackets.cpp | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/stage0/src/frontends/lean/brackets.cpp b/stage0/src/frontends/lean/brackets.cpp index d115d55f1e..b2cf3001e7 100644 --- a/stage0/src/frontends/lean/brackets.cpp +++ b/stage0/src/frontends/lean/brackets.cpp @@ -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 const & src break; } } + optional 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())) {