From ea04414058eb6ac43b0892840b703e3db40ea19e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 16 Aug 2015 18:21:29 -0700 Subject: [PATCH] feat(frontends/lean): allow user to overload notation containing foldr/foldl and/or scoped expressions see new tests for a summary of new features see issue #800 --- src/frontends/lean/builtin_cmds.cpp | 2 +- src/frontends/lean/parse_table.cpp | 90 +++++--- src/frontends/lean/parse_table.h | 26 ++- src/frontends/lean/parser.cpp | 216 +++++++++++++------ src/frontends/lean/parser.h | 5 +- tests/lean/binder_overload.lean | 11 + tests/lean/binder_overload.lean.expected.out | 7 + tests/lean/nary_overload.lean | 21 ++ tests/lean/nary_overload.lean.expected.out | 5 + tests/lean/nary_overload2.lean | 17 ++ tests/lean/nary_overload2.lean.expected.out | 5 + tests/lean/run/list_vector_overload.lean | 10 + 12 files changed, 305 insertions(+), 110 deletions(-) create mode 100644 tests/lean/binder_overload.lean create mode 100644 tests/lean/binder_overload.lean.expected.out create mode 100644 tests/lean/nary_overload.lean create mode 100644 tests/lean/nary_overload.lean.expected.out create mode 100644 tests/lean/nary_overload2.lean create mode 100644 tests/lean/nary_overload2.lean.expected.out create mode 100644 tests/lean/run/list_vector_overload.lean diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 98b9a7920..794037ba0 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -181,7 +181,7 @@ static bool print_parse_table(parser const & p, parse_table const & t, bool nud, os = os.update(get_pp_preterm_name(), true); ios.set_options(os); optional tt(get_token_table(p.env())); - t.for_each([&](unsigned num, notation::transition const * ts, list> const & overloads) { + t.for_each([&](unsigned num, notation::transition const * ts, list const & overloads) { if (uses_some_token(num, ts, tokens)) { io_state_stream out = regular(p.env(), ios); if (tactic_table) diff --git a/src/frontends/lean/parse_table.cpp b/src/frontends/lean/parse_table.cpp index 7b8d2e49a..539755d58 100644 --- a/src/frontends/lean/parse_table.cpp +++ b/src/frontends/lean/parse_table.cpp @@ -194,6 +194,24 @@ bool action::is_equal(action const & a) const { } lean_unreachable(); // LCOV_EXCL_LINE } +// Similar to is_equal, but ignores information that is "irrelevant" for parsing. +// For example, for Exprs actions, get_rec and get_initial are not relevant when parsing the input stream. +// We only need them when we reach an accepting state. +bool action::is_equivalent(action const & a) const { + if (kind() != a.kind()) + return false; + switch (kind()) { + case action_kind::Exprs: + return + rbp() == a.rbp() && + get_sep() == a.get_sep() && + get_terminator() == a.get_terminator(); + case action_kind::ScopedExpr: + return rbp() == a.rbp(); + default: + return is_equal(a); + } +} void action::display(io_state_stream & out) const { switch (kind()) { case action_kind::Skip: out << "skip"; break; @@ -216,15 +234,13 @@ void action::display(io_state_stream & out) const { out << "(fold" << (is_fold_right() ? "r" : "l"); if (get_terminator()) out << "*"; - out << " " << rbp() << " " << get_rec(); - if (get_initial()) - out << " " << *get_initial(); + out << " " << rbp() << " `" << get_sep() << "`"; if (get_terminator()) - out << *get_terminator(); + out << " `" << *get_terminator() << "`"; out << ")"; break; case action_kind::ScopedExpr: - out << "(scoped " << rbp() << " " << get_rec() << ")"; + out << "(scoped " << rbp() << ")"; break; } } @@ -303,7 +319,7 @@ transition replace(transition const & t, std::function const struct parse_table::cell { bool m_nud; - list> m_accept; + list m_accept; name_map>> m_children; MK_LEAN_RC(); // Declare m_rc counter void dealloc() { delete this; } @@ -326,7 +342,7 @@ list> parse_table::find(name const & tk) const { return list>(); } -list> const & parse_table::is_accepting() const { +list const & parse_table::is_accepting() const { return m_ptr->m_accept; } @@ -358,40 +374,47 @@ static void validate_transitions(bool nud, unsigned num, transition const * ts, throw exception("invalid notation declaration, expression template has more free variables than arguments"); } -static list> insert(list> const & l, unsigned priority, expr const & a) { +static list insert(list const & l, unsigned priority, list const & p, expr const & a) { if (!l) { - return to_list(mk_pair(priority, a)); - } else if (priority <= head(l).first) { - return cons(mk_pair(priority, a), l); + return to_list(accepting(priority, p, a)); + } else if (priority <= head(l).get_prio()) { + return cons(accepting(priority, p, a), l); } else { - return cons(head(l), insert(tail(l), priority, a)); + return cons(head(l), insert(tail(l), priority, p, a)); } } parse_table parse_table::add_core(unsigned num, transition const * ts, expr const & a, - unsigned priority, bool overload) const { + unsigned priority, bool overload, buffer & post_buffer) const { parse_table r(new cell(*m_ptr)); if (num == 0) { + list postponed = to_list(post_buffer); if (!overload) { - r.m_ptr->m_accept = to_list(mk_pair(priority, a)); + r.m_ptr->m_accept = to_list(accepting(priority, postponed, a)); } else { - auto new_accept = filter(r.m_ptr->m_accept, [&](pair const & p) { return p.second != a; }); - r.m_ptr->m_accept = insert(new_accept, priority, a); + auto new_accept = filter(r.m_ptr->m_accept, [&](accepting const & p) { + return p.get_expr() != a || p.get_postponed() != postponed; + }); + r.m_ptr->m_accept = insert(new_accept, priority, postponed, a); } } else { list> const * it = r.m_ptr->m_children.find(ts->get_token()); + action const & ts_act = ts->get_action(); + action_kind k = ts_act.kind(); + if (k == action_kind::Exprs || k == action_kind::ScopedExpr) + post_buffer.push_back(ts_act); parse_table new_child; if (it) { // TODO(Leo): support multiple actions action const & act = head(*it).first; parse_table const & child = head(*it).second; - if (act.is_equal(ts->get_action())) { - new_child = child.add_core(num-1, ts+1, a, priority, overload); + if (act.is_equivalent(ts_act)) { + new_child = child.add_core(num-1, ts+1, a, priority, overload, post_buffer); } else { - new_child = parse_table().add_core(num-1, ts+1, a, priority, overload); + new_child = parse_table().add_core(num-1, ts+1, a, priority, overload, post_buffer); } } else { - new_child = parse_table().add_core(num-1, ts+1, a, priority, overload); + new_child = parse_table().add_core(num-1, ts+1, a, priority, overload, post_buffer); } r.m_ptr->m_children.insert(ts->get_token(), to_list(mk_pair(ts->get_action(), new_child))); } @@ -461,14 +484,15 @@ optional get_head_index(unsigned num, transition const * ts, expr co } parse_table parse_table::add(unsigned num, transition const * ts, expr const & a, unsigned priority, bool overload) const { + buffer postponed; expr new_a = annotate_macro_subterms(a); validate_transitions(is_nud(), num, ts, new_a); - return add_core(num, ts, new_a, priority, overload); + return add_core(num, ts, new_a, priority, overload, postponed); } void parse_table::for_each(buffer & ts, std::function> const &)> const & fn) const { + list const &)> const & fn) const { if (!is_nil(m_ptr->m_accept)) fn(ts.size(), ts.data(), m_ptr->m_accept); m_ptr->m_children.for_each([&](name const & k, list> const & lst) { @@ -481,7 +505,7 @@ void parse_table::for_each(buffer & ts, } void parse_table::for_each(std::function> const &)> const & fn) const { + list const &)> const & fn) const { buffer tmp; for_each(tmp, fn); } @@ -490,9 +514,9 @@ parse_table parse_table::merge(parse_table const & s, bool overload) const { if (is_nud() != s.is_nud()) throw exception("invalid parse table merge, tables have different kinds"); parse_table r(*this); - s.for_each([&](unsigned num, transition const * ts, list> const & accept) { - for (pair const & p : accept) { - r = r.add(num, ts, p.second, p.first, overload); + s.for_each([&](unsigned num, transition const * ts, list const & accept) { + for (accepting const & acc : accept) { + r = r.add(num, ts, acc.get_expr(), acc.get_prio(), overload); } }); return r; @@ -500,7 +524,7 @@ parse_table parse_table::merge(parse_table const & s, bool overload) const { bool parse_table::is_nud() const { return m_ptr->m_nud; } -void display(io_state_stream & out, unsigned num, transition const * ts, list> const & es, bool nud, +void display(io_state_stream & out, unsigned num, transition const * ts, list const & es, bool nud, optional const & tt) { if (!nud) out << "_ "; @@ -525,24 +549,24 @@ void display(io_state_stream & out, unsigned num, transition const * ts, list> tmp; + buffer tmp; to_buffer(es, tmp); out << "\n"; unsigned i = tmp.size(); while (i > 0) { --i; out << " | "; - if (tmp[i].first != LEAN_DEFAULT_NOTATION_PRIORITY) - out << "[priority " << tmp[i].first << "] "; - out << tmp[i].second << "\n"; + if (tmp[i].get_prio() != LEAN_DEFAULT_NOTATION_PRIORITY) + out << "[priority " << tmp[i].get_prio() << "] "; + out << tmp[i].get_expr() << "\n"; } } } void parse_table::display(io_state_stream & out, optional const & tt) const { - for_each([&](unsigned num, transition const * ts, list> const & es) { + for_each([&](unsigned num, transition const * ts, list const & es) { ::lean::notation::display(out, num, ts, es, is_nud(), tt); }); } diff --git a/src/frontends/lean/parse_table.h b/src/frontends/lean/parse_table.h index e14f4718e..8b66f74f3 100644 --- a/src/frontends/lean/parse_table.h +++ b/src/frontends/lean/parse_table.h @@ -86,6 +86,8 @@ public: std::string const & get_lua_fn() const; bool is_equal(action const & a) const; + bool is_equivalent(action const & a) const; + void display(io_state_stream & out) const; /** \brief Return true iff the action is not Ext or LuaExt */ @@ -129,7 +131,19 @@ inline bool operator!=(transition const & t1, transition const & t2) { /** \brief Apply \c f to expressions embedded in the given transition */ transition replace(transition const & t, std::function const & f); -void display(io_state_stream & out, unsigned num, transition const * ts, list> const & es, bool nud, +class accepting { + unsigned m_prio; + list m_postponed; // exprs and scoped_expr actions + expr m_expr; // resulting expression +public: + accepting(unsigned prio, list const & post, expr const & e): + m_prio(prio), m_postponed(post), m_expr(e) {} + unsigned get_prio() const { return m_prio; } + list const & get_postponed() const { return m_postponed; } + expr const & get_expr() const { return m_expr; } +}; + +void display(io_state_stream & out, unsigned num, transition const * ts, list const & es, bool nud, optional const & tt); /** @@ -140,9 +154,9 @@ class parse_table { struct cell; cell * m_ptr; explicit parse_table(cell * c); - parse_table add_core(unsigned num, transition const * ts, expr const & a, unsigned priority, bool overload) const; + parse_table add_core(unsigned num, transition const * ts, expr const & a, unsigned priority, bool overload, buffer & postponed) const; void for_each(buffer & ts, std::function> const &)> const & fn) const; + list const &)> const & fn) const; public: parse_table(bool nud = true); parse_table(parse_table const & s); @@ -156,10 +170,10 @@ public: parse_table add(std::initializer_list const & ts, expr const & a) const { return add(ts.size(), ts.begin(), a, LEAN_DEFAULT_NOTATION_PRIORITY, true); } - parse_table merge(parse_table const & s, bool overload) const; + parse_table merge(parse_table const & s, bool overload) const;\ list> find(name const & tk) const; - list> const & is_accepting() const; - void for_each(std::function> const &)> const & fn) const; + list const & is_accepting() const; + void for_each(std::function const &)> const & fn) const; void display(io_state_stream & out, optional const & tk) const; }; diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index a64733075..4a01edf86 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1069,13 +1069,126 @@ bool parser::parse_local_notation_decl(buffer * nentries) { } } +void parser::process_postponed(buffer const & args, bool is_left, + buffer const & kinds, + buffer> const & nargs, + buffer const & ps, + buffer> const & scoped_info, + list const & postponed, + pos_info const & p, + buffer & new_args) { + unsigned args_idx = 0; + if (is_left) { + new_args.push_back(args[0]); + args_idx = 1; + } + unsigned kinds_idx = 0; + unsigned nargs_idx = 0; + unsigned scoped_idx = 0; + list it = postponed; + for (; kinds_idx < kinds.size(); kinds_idx++, args_idx++) { + auto k = kinds[kinds_idx]; + switch (k) { + case notation::action_kind::Exprs: { + if (!it || head(it).kind() != k || nargs_idx >= nargs.size()) + throw exception("ill-formed parsing tables"); + notation::action const & a = head(it); + buffer r_args; + to_buffer(nargs[nargs_idx], r_args); + nargs_idx++; + expr rec = copy_with_new_pos(a.get_rec(), p); + expr r; + if (a.is_fold_right()) { + if (a.get_initial()) { + r = instantiate_rev(copy_with_new_pos(*a.get_initial(), p), new_args.size(), new_args.data()); + } else { + r = r_args.back(); + r_args.pop_back(); + } + unsigned i = r_args.size(); + while (i > 0) { + --i; + new_args.push_back(r_args[i]); + new_args.push_back(r); + r = instantiate_rev(rec, new_args.size(), new_args.data()); + new_args.pop_back(); new_args.pop_back(); + } + } else { + unsigned fidx = 0; + if (a.get_initial()) { + r = instantiate_rev(copy_with_new_pos(*a.get_initial(), p), new_args.size(), new_args.data()); + } else { + r = r_args[0]; + fidx++; + } + for (unsigned i = fidx; i < r_args.size(); i++) { + new_args.push_back(r_args[i]); + new_args.push_back(r); + r = instantiate_rev(rec, new_args.size(), new_args.data()); + new_args.pop_back(); new_args.pop_back(); + } + } + new_args.push_back(r); + it = tail(it); + break; + } + case notation::action_kind::ScopedExpr: { + if (!it || head(it).kind() != k || scoped_idx >= scoped_info.size()) + throw exception("ill-formed parsing tables"); + expr r = args[args_idx]; + notation::action const & a = head(it); + bool no_cache = false; + unsigned ps_sz = scoped_info[scoped_idx].first; + pos_info binder_pos = scoped_info[scoped_idx].second; + scoped_idx++; + if (is_var(a.get_rec(), 0)) { + if (a.use_lambda_abstraction()) + r = Fun(ps_sz, ps.data(), r, no_cache); + else + r = Pi(ps_sz, ps.data(), r, no_cache); + r = rec_save_pos(r, binder_pos); + } else { + expr rec = copy_with_new_pos(a.get_rec(), p); + unsigned i = ps_sz; + while (i > 0) { + --i; + expr const & l = ps[i]; + if (a.use_lambda_abstraction()) + r = Fun(l, r, no_cache); + else + r = Pi(l, r, no_cache); + r = save_pos(r, binder_pos); + new_args.push_back(r); + r = instantiate_rev(rec, new_args.size(), new_args.data()); + new_args.pop_back(); + } + } + new_args.push_back(r); + it = tail(it); + break; + } + default: + new_args.push_back(args[args_idx]); + break; + } + } +} + expr parser::parse_notation_core(parse_table t, expr * left, bool as_tactic) { lean_assert(curr() == scanner::token_kind::Keyword); auto p = pos(); if (m_info_manager) m_info_manager->add_symbol_info(p.first, p.second, get_token_info().token()); - buffer args; - buffer ps; + buffer args; + buffer kinds; + buffer> nargs; // nary args + buffer ps; + buffer> scoped_info; // size of ps and binder_pos for scoped_exprs + // Invariants: + // args.size() == kinds.size() if not left + // args.size() == kinds.size()+1 if left + // nargs.size() == number of Exprs in kinds + // scoped_info.size() == number of Scoped_Exprs in kinds local_environment lenv(m_env); pos_info binder_pos; if (left) @@ -1095,6 +1208,7 @@ expr parser::parse_notation_core(parse_table t, expr * left, bool as_tactic) { case notation::action_kind::Expr: next(); args.push_back(parse_expr_or_tactic(a.rbp(), as_tactic)); + kinds.push_back(a.kind()); break; case notation::action_kind::Exprs: { next(); @@ -1114,39 +1228,9 @@ expr parser::parse_notation_core(parse_table t, expr * left, bool as_tactic) { throw parser_error(sstream() << "invalid composite expression, '" << *terminator << "' expected", pos()); } } - expr rec = copy_with_new_pos(a.get_rec(), p); - expr r; - if (a.is_fold_right()) { - if (a.get_initial()) { - r = instantiate_rev(copy_with_new_pos(*a.get_initial(), p), args.size(), args.data()); - } else { - r = r_args.back(); - r_args.pop_back(); - } - unsigned i = r_args.size(); - while (i > 0) { - --i; - args.push_back(r_args[i]); - args.push_back(r); - r = instantiate_rev(rec, args.size(), args.data()); - args.pop_back(); args.pop_back(); - } - } else { - unsigned fidx = 0; - if (a.get_initial()) { - r = instantiate_rev(copy_with_new_pos(*a.get_initial(), p), args.size(), args.data()); - } else { - r = r_args[0]; - fidx++; - } - for (unsigned i = fidx; i < r_args.size(); i++) { - args.push_back(r_args[i]); - args.push_back(r); - r = instantiate_rev(rec, args.size(), args.data()); - args.pop_back(); args.pop_back(); - } - } - args.push_back(r); + args.push_back(expr()); // placeholder + kinds.push_back(a.kind()); + nargs.push_back(to_list(r_args)); break; } case notation::action_kind::Binder: @@ -1162,30 +1246,9 @@ expr parser::parse_notation_core(parse_table t, expr * left, bool as_tactic) { case notation::action_kind::ScopedExpr: { next(); expr r = parse_scoped_expr(ps, lenv, a.rbp()); - bool no_cache = false; - if (is_var(a.get_rec(), 0)) { - if (a.use_lambda_abstraction()) - r = Fun(ps, r, no_cache); - else - r = Pi(ps, r, no_cache); - r = rec_save_pos(r, binder_pos); - } else { - expr rec = copy_with_new_pos(a.get_rec(), p); - unsigned i = ps.size(); - while (i > 0) { - --i; - expr const & l = ps[i]; - if (a.use_lambda_abstraction()) - r = Fun(l, r, no_cache); - else - r = Pi(l, r, no_cache); - r = save_pos(r, binder_pos); - args.push_back(r); - r = instantiate_rev(rec, args.size(), args.data()); - args.pop_back(); - } - } args.push_back(r); + kinds.push_back(a.kind()); + scoped_info.push_back(mk_pair(ps.size(), binder_pos)); break; } case notation::action_kind::LuaExt: @@ -1207,17 +1270,18 @@ expr parser::parse_notation_core(parse_table t, expr * left, bool as_tactic) { throw parser_error(sstream() << "failed to use notation implemented in Lua, value returned by function '" << a.get_lua_fn() << "' is not an expression", p); args.push_back(rec_save_pos(to_expr(L, -1), p)); + kinds.push_back(a.kind()); lua_pop(L, 1); }); break; case notation::action_kind::Ext: args.push_back(a.get_parse_fn()(*this, args.size(), args.data(), p)); + kinds.push_back(a.kind()); break; } - t = head(r).second; // TODO(Leo): } - list> const & as = t.is_accepting(); + list const & as = t.is_accepting(); save_overload_notation(as, p); if (is_nil(as)) { if (p == pos()) @@ -1225,16 +1289,28 @@ expr parser::parse_notation_core(parse_table t, expr * left, bool as_tactic) { else throw parser_error(sstream() << "invalid expression starting at " << p.first << ":" << p.second, pos()); } + lean_assert(left || args.size() == kinds.size()); + lean_assert(!left || args.size() == kinds.size() + 1); buffer cs; - for (pair const & a : as) { - expr r = copy_with_new_pos(a.second, p); - if (args.empty()) { - // Notation does not have arguments. Thus, the info-manager should treat is as a single thing. - r = mk_notation_info(r, r.get_tag()); + for (notation::accepting const & a : as) { + expr r = copy_with_new_pos(a.get_expr(), p); + list const & postponed = a.get_postponed(); + if (postponed) { + buffer new_args; + process_postponed(args, left, kinds, nargs, ps, scoped_info, postponed, p, new_args); + lean_assert(!args.empty()); + r = instantiate_rev(r, new_args.size(), new_args.data()); + cs.push_back(r); } else { - r = instantiate_rev(r, args.size(), args.data()); + lean_assert(nargs.empty() && ps_sz.empty()); + if (args.empty()) { + // Notation does not have arguments. Thus, the info-manager should treat is as a single thing. + r = mk_notation_info(r, r.get_tag()); + } else { + r = instantiate_rev(r, args.size(), args.data()); + } + cs.push_back(r); } - cs.push_back(r); } expr r = save_pos(mk_choice(cs.size(), cs.data()), p); save_type_info(r); @@ -2110,10 +2186,12 @@ void parser::save_overload_notation(list const & as, pos_info const & p) { return; m_info_manager->add_overload_notation_info(p.first, p.second, as); } -void parser::save_overload_notation(list> const & as, pos_info const & p) { +void parser::save_overload_notation(list const & as, pos_info const & p) { if (!m_info_manager || length(as) <= 1) return; - list new_as = map2, std::function const &)>>(as, [](pair const & p) { return p.second; }); + list new_as = + map2> + (as, [](notation::accepting const & p) { return p.get_expr(); }); save_overload_notation(new_as, p); } void parser::save_identifier_info(pos_info const & p, name const & full_id) { diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index b4f57004a..01c8794cf 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -202,6 +202,9 @@ class parser { void parse_script(bool as_expr = false); bool parse_commands(); unsigned curr_lbp_core(bool as_tactic) const; + void process_postponed(buffer const & args, bool is_left, buffer const & kinds, + buffer> const & nargs, buffer const & ps, buffer> const & scoped_info, + list const & postponed, pos_info const & p, buffer & new_args); expr parse_notation_core(parse_table t, expr * left, bool as_tactic); expr parse_expr_or_tactic(unsigned rbp, bool as_tactic) { return as_tactic ? parse_tactic(rbp) : parse_expr(rbp); @@ -234,7 +237,7 @@ class parser { void save_snapshot(); void save_overload(expr const & e); void save_overload_notation(list const & as, pos_info const & p); - void save_overload_notation(list> const & as, pos_info const & p); + void save_overload_notation(list const & as, pos_info const & p); void save_type_info(expr const & e); void save_pre_info_data(); void save_identifier_info(pos_info const & p, name const & full_id); diff --git a/tests/lean/binder_overload.lean b/tests/lean/binder_overload.lean new file mode 100644 index 000000000..56266e0e5 --- /dev/null +++ b/tests/lean/binder_overload.lean @@ -0,0 +1,11 @@ +import data.set data.finset +open nat set finset + +constant S : set nat +constant s : finset nat + +check {x ∈ S | x > 0} +check {x ∈ s | x > 0} +set_option pp.all true +check {x ∈ S | x > 0} +check {x ∈ s | x > 0} diff --git a/tests/lean/binder_overload.lean.expected.out b/tests/lean/binder_overload.lean.expected.out new file mode 100644 index 000000000..743b02443 --- /dev/null +++ b/tests/lean/binder_overload.lean.expected.out @@ -0,0 +1,7 @@ +{x : ℕ ∈ S| x > 0} : set ℕ +{x : ℕ ∈ s| x > 0} : finset ℕ +@set.sep.{1} nat (λ (x : nat), nat.gt x (nat.of_num 0)) S : set.{1} nat +@finset.sep.{1} nat (λ (a b : nat), nat.has_decidable_eq a b) (λ (x : nat), nat.gt x (nat.of_num 0)) + (λ (a : nat), nat.decidable_ge a (nat.succ (nat.of_num 0))) + s : + finset.{1} nat diff --git a/tests/lean/nary_overload.lean b/tests/lean/nary_overload.lean new file mode 100644 index 000000000..97fe35e85 --- /dev/null +++ b/tests/lean/nary_overload.lean @@ -0,0 +1,21 @@ +prelude + +constant vec.{l} : Type.{l} → Type.{l} +constant lst.{l} : Type.{l} → Type.{l} +constant vec.nil {A : Type} : vec A +constant lst.nil {A : Type} : lst A +constant vec.cons {A : Type} : A → vec A → vec A +constant lst.cons {A : Type} : A → lst A → lst A + +notation `[` l:(foldr `,` (h t, vec.cons h t) vec.nil `]`) := l +notation `[` l:(foldr `,` (h t, lst.cons h t) lst.nil `]`) := l + +constant A : Type.{1} +variables a b c : A + +check [a, b, c] +check ([a, b, c] : vec A) +check ([a, b, c] : lst A) +set_option pp.all true +check ([a, b, c] : vec A) +check ([a, b, c] : lst A) diff --git a/tests/lean/nary_overload.lean.expected.out b/tests/lean/nary_overload.lean.expected.out new file mode 100644 index 000000000..1ee8f792e --- /dev/null +++ b/tests/lean/nary_overload.lean.expected.out @@ -0,0 +1,5 @@ +[a, b, c] : vec A +[a, b, c] : vec A +[a, b, c] : lst A +@vec.cons.{1} A a (@vec.cons.{1} A b (@vec.cons.{1} A c (@vec.nil.{1} A))) : vec.{1} A +@lst.cons.{1} A a (@lst.cons.{1} A b (@lst.cons.{1} A c (@lst.nil.{1} A))) : lst.{1} A diff --git a/tests/lean/nary_overload2.lean b/tests/lean/nary_overload2.lean new file mode 100644 index 000000000..483cc9271 --- /dev/null +++ b/tests/lean/nary_overload2.lean @@ -0,0 +1,17 @@ +import data.list data.examples.vector +open nat list vector + +check [1, 2, 3] +check ([1, 2, 3] : vector nat _) +check ([1, 2, 3] : list nat) +check (#list [1, 2, 3]) +check (#vector [1, 2, 3]) + +example : (#vector [1, 2, 3]) = [1, 2, 3] := +rfl + +example : (#vector [1, 2, 3]) = ([1, 2, 3] : vector nat _) := +rfl + +example : (#list [1, 2, 3]) = ([1, 2, 3] : list nat) := +rfl diff --git a/tests/lean/nary_overload2.lean.expected.out b/tests/lean/nary_overload2.lean.expected.out new file mode 100644 index 000000000..d331da9b6 --- /dev/null +++ b/tests/lean/nary_overload2.lean.expected.out @@ -0,0 +1,5 @@ +[1, 2, 3] : list num +[1, 2, 3] : vector ℕ 3 +[1, 2, 3] : list ℕ +[1, 2, 3] : list num +[1, 2, 3] : vector num 3 diff --git a/tests/lean/run/list_vector_overload.lean b/tests/lean/run/list_vector_overload.lean new file mode 100644 index 000000000..49f481620 --- /dev/null +++ b/tests/lean/run/list_vector_overload.lean @@ -0,0 +1,10 @@ +import data.list data.examples.vector +open list vector nat + +variables (A : Type) (a b c : A) + +check [a, b, c] +check (#list [a, b, c]) +check (#vector [a, b, c]) +check ([a, b, c] : vector A _) +check ([a, b, c] : list A)