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

feat(frontends/lean): add Type' as notation for Type.{_+1}

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-10 13:28:36 +01:00
parent d9b2801eeb
commit 313c7066e7
4 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -31,10 +31,14 @@ static expr parse_Type(parser & p, unsigned, expr const *, pos_info const & pos)
p.check_token_next(g_rcurly, "invalid Type expression, '}' expected");
return p.save_pos(mk_sort(l), pos);
} else {
return p.save_pos(p.mk_Type(), pos);
return p.save_pos(mk_sort(mk_level_placeholder()), pos);
}
}
static expr parse_Type_prime(parser & p, unsigned, expr const *, pos_info const & pos) {
return p.save_pos(mk_sort(mk_succ(mk_level_placeholder())), pos);
}
static expr parse_let(parser & p, pos_info const & pos);
static expr parse_let_body(parser & p, pos_info const & pos) {
if (p.curr_is_token(g_comma)) {
@ -329,6 +333,7 @@ parse_table init_nud_table() {
r = r.add({transition("fun", Binders), transition(",", mk_scoped_expr_action(x0))}, x0);
r = r.add({transition("Pi", Binders), transition(",", mk_scoped_expr_action(x0, 0, false))}, x0);
r = r.add({transition("Type", mk_ext_action(parse_Type))}, x0);
r = r.add({transition("Type'", mk_ext_action(parse_Type_prime))}, x0);
r = r.add({transition("let", mk_ext_action(parse_let_expr))}, x0);
r = r.add({transition("calc", mk_ext_action(parse_calc_expr))}, x0);
r = r.add({transition("#", mk_ext_action(parse_overwrite_notation))}, x0);

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

@ -464,10 +464,6 @@ level parser::parse_level(unsigned rbp) {
return left;
}
expr parser::mk_Type() {
return mk_sort(mk_level_placeholder());
}
std::tuple<expr, level_param_names> parser::elaborate_relaxed(expr const & e) {
parser_pos_provider pp = get_pos_provider();
return ::lean::elaborate(m_env, m_local_level_decls, m_ios, e, &pp, false);

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

@ -241,7 +241,6 @@ public:
unsigned get_local_index(name const & n) const;
/** \brief Return the local parameter named \c n */
expr const * get_local(name const & n) const { return m_local_decls.find(n); }
expr mk_Type();
/**
\brief By default, when the parser finds a unknown identifier, it signs an error.

4
src/frontends/lean/token_table.cpp
View file

@ -67,8 +67,8 @@ token_table init_token_table() {
std::pair<char const *, unsigned> builtin[] =
{{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"have", 0}, {"show", 0}, {"by", 0}, {"then", 0},
{"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
{"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"|", 0}, {"!", 0}, {"with", 0},
{"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0},
{"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"Type'", g_max_prec},
{"|", 0}, {"!", 0}, {"with", 0}, {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0},
{"(*", 0}, {"(--", 0}, {"proof", 0}, {"qed", 0}, {"@", g_max_prec}, {"including", 0},
{"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}};