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

fix(frontends/lean/elaborator): conflict between (: t :) and (::) notations

Browse source 
It was preventing us from using `(::)`
This commit is contained in:
Leonardo de Moura 2017-03-12 09:29:16 -07:00
parent 89d0f1773e
commit c694dbd600
3 changed files with 25 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -924,6 +924,28 @@ static expr parse_lparen(parser_state & p, unsigned, expr const *, pos_info cons
}
}
static expr parse_lambda_cons(parser_state & p, unsigned, expr const *, pos_info const & pos) {
list<pair<transition, parse_table>> ts = p.led().find(get_dcolon_tk());
if (!ts || tail(ts) || !head(ts).second.is_accepting())
throw parser_error("invalid '(::)' notation, infix operator '::' has not been defined yet or is the prefix of another notation declaration", pos);
notation::action const & act = head(ts).first.get_action();
if (act.kind() != notation::action_kind::Expr)
throw parser_error("invalid '(::)' notation, declaration for operator '::' is not compatible with the `(::)` syntactic sugar", pos);
expr args[2];
buffer<expr> vars;
args[0] = mk_local(mk_fresh_name(), "_x", mk_expr_placeholder(), binder_info());
vars.push_back(args[0]);
args[1] = mk_local(mk_fresh_name(), "_y", mk_expr_placeholder(), binder_info());
vars.push_back(args[1]);
buffer<expr> cs;
for (notation::accepting const & acc : head(ts).second.is_accepting()) {
expr r = p.copy_with_new_pos(acc.get_expr(), pos);
r = p.save_pos(mk_infix_function(Fun(vars, instantiate_rev(r, 2, args), p)), pos);
cs.push_back(r);
}
return p.save_pos(mk_choice(cs.size(), cs.data()), pos);
}
parse_table init_nud_table() {
action Expr(mk_expr_action());
action Skip(mk_skip_action());
@ -947,6 +969,7 @@ parse_table init_nud_table() {
r = r.add({transition("%%", mk_ext_action(parse_antiquote_expr))}, x0);
r = r.add({transition("(:", Expr), transition(":)", mk_ext_action(parse_pattern))}, x0);
r = r.add({transition("()", mk_ext_action(parse_unit))}, x0);
r = r.add({transition("(::)", mk_ext_action(parse_lambda_cons))}, x0);
r = r.add({transition("fun", mk_ext_action(parse_lambda))}, 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);

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

@ -83,7 +83,7 @@ void init_token_table(token_table & t) {
{"do", 0}, {"if", 0}, {"then", 0}, {"else", 0}, {"by", 0}, {"hiding", 0}, {"replacing", 0}, {"renaming", 0},
{"from", 0}, {"(", g_max_prec}, {"`(", g_max_prec}, {"``(", g_max_prec},
{"```(", g_max_prec}, {"`[", g_max_prec}, {"`", g_max_prec},
{"%%", g_max_prec}, {"()", g_max_prec}, {")", 0}, {"'", 0},
{"%%", g_max_prec}, {"()", g_max_prec}, {"(::)", g_max_prec}, {")", 0}, {"'", 0},
{"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
{"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0},
{"Type", g_max_prec}, {"Type*", g_max_prec}, {"Sort", g_max_prec}, {"Sort*", g_max_prec},

1
tests/lean/run/lambda_cons.lean Normal file
View file

@ -0,0 +1 @@
#eval list.foldr (::) [] [1, 2, 3]