From 555d26aa615db704b54df74cfd172c6cbe5995ce Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 19 Oct 2014 08:40:56 -0700 Subject: [PATCH] feat(frontends/lean/pp): take notation declarations into account when pretty printing TODO: support foldl/foldr and binders --- src/frontends/lean/builtin_cmds.cpp | 5 +- src/frontends/lean/pp.cpp | 281 +++++++++++++++--- src/frontends/lean/pp.h | 72 +++-- src/frontends/lean/pp_options.cpp | 1 + src/frontends/lean/pp_options.h | 1 + tests/lean/bug1.lean.expected.out | 6 +- tests/lean/calc1.lean.expected.out | 4 +- tests/lean/crash.lean.expected.out | 4 +- tests/lean/have1.lean.expected.out | 17 +- tests/lean/interactive/coe.input.expected.out | 2 +- .../lean/interactive/findp.input.expected.out | 8 +- tests/lean/interactive/in4.input.expected.out | 4 +- tests/lean/interactive/in5.input.expected.out | 2 +- tests/lean/interactive/t4.input.expected.out | 4 +- tests/lean/notation.lean | 18 ++ tests/lean/notation.lean.expected.out | 11 + tests/lean/show1.lean.expected.out | 14 +- tests/lean/t10.lean.expected.out | 6 +- tests/lean/t14.lean.expected.out | 4 +- tests/lean/t9.lean.expected.out | 4 +- tests/lean/tuple.lean.expected.out | 2 +- tests/lean/uni_bug1.lean.expected.out | 2 +- tests/lean/univ.lean.expected.out | 16 +- tests/lean/var2.lean.expected.out | 2 +- 24 files changed, 370 insertions(+), 120 deletions(-) create mode 100644 tests/lean/notation.lean create mode 100644 tests/lean/notation.lean.expected.out diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index c92d60c62..a0c6986cf 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -59,7 +59,10 @@ environment print_cmd(parser & p) { } else if (p.curr_is_token_or_id(get_raw_tk())) { p.next(); expr e = p.parse_expr(); - p.regular_stream() << e << endl; + io_state_stream out = p.regular_stream(); + options opts = out.get_options(); + opts = opts.update(get_pp_notation_option_name(), false); + out.update_options(opts) << e << endl; } else if (p.curr_is_token_or_id(get_options_tk())) { p.next(); p.regular_stream() << p.ios().get_options() << endl; diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index dbe65a8e0..da70bc8f5 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include "util/flet.h" #include "kernel/replace_fn.h" #include "kernel/free_vars.h" @@ -25,6 +26,7 @@ Author: Leonardo de Moura #include "frontends/lean/pp_options.h" #include "frontends/lean/token_table.h" #include "frontends/lean/builtin_exprs.h" +#include "frontends/lean/parser_config.h" namespace lean { static format * g_ellipsis_n_fmt = nullptr; @@ -211,11 +213,11 @@ auto pretty_fn::pp_coercion_fn(expr const & e, unsigned sz) -> result { } else { expr const & fn = app_fn(e); result res_fn = pp_coercion_fn(fn, sz-1); - format fn_fmt = res_fn.first; + format fn_fmt = res_fn.fmt(); if (m_implict && sz == 2 && has_implicit_args(fn)) fn_fmt = compose(*g_explicit_fmt, fn_fmt); result res_arg = pp_child(app_arg(e), max_bp()); - return mk_result(group(compose(fn_fmt, nest(m_indent, compose(line(), res_arg.first)))), max_bp()-1); + return result(max_bp()-1, group(compose(fn_fmt, nest(m_indent, compose(line(), res_arg.fmt()))))); } } @@ -232,8 +234,8 @@ auto pretty_fn::pp_coercion(expr const & e, unsigned bp) -> result { unsigned sz = args.size() - r->second; lean_assert(sz >= 2); auto r = pp_coercion_fn(e, sz); - if (r.second < bp) { - return mk_result(paren(r.first)); + if (r.rbp() < bp) { + return result(paren(r.fmt())); } else { return r; } @@ -242,8 +244,8 @@ auto pretty_fn::pp_coercion(expr const & e, unsigned bp) -> result { auto pretty_fn::pp_child_core(expr const & e, unsigned bp) -> result { result r = pp(e); - if (r.second < bp) { - return mk_result(paren(r.first)); + if (r.rbp() < bp) { + return result(paren(r.fmt())); } else { return r; } @@ -261,16 +263,16 @@ auto pretty_fn::pp_child(expr const & e, unsigned bp) -> result { auto pretty_fn::pp_var(expr const & e) -> result { unsigned vidx = var_idx(e); - return mk_result(compose(format("#"), format(vidx))); + return result(compose(format("#"), format(vidx))); } auto pretty_fn::pp_sort(expr const & e) -> result { if (m_env.impredicative() && e == mk_Prop()) { - return mk_result(format("Prop")); + return result(format("Prop")); } else if (m_universes) { - return mk_result(group(format("Type.{") + nest(6, pp_level(sort_level(e))) + format("}"))); + return result(group(format("Type.{") + nest(6, pp_level(sort_level(e))) + format("}"))); } else { - return mk_result(format("Type")); + return result(format("Type")); } } @@ -322,18 +324,18 @@ auto pretty_fn::pp_const(expr const & e) -> result { first = false; } r += format("}"); - return mk_result(group(r)); + return result(group(r)); } else { - return mk_result(format(n)); + return result(format(n)); } } auto pretty_fn::pp_meta(expr const & e) -> result { - return mk_result(compose(format("?"), format(mlocal_name(e)))); + return result(compose(format("?"), format(mlocal_name(e)))); } auto pretty_fn::pp_local(expr const & e) -> result { - return mk_result(format(local_pp_name(e))); + return result(format(local_pp_name(e))); } bool pretty_fn::has_implicit_args(expr const & f) { @@ -360,11 +362,11 @@ bool pretty_fn::has_implicit_args(expr const & f) { auto pretty_fn::pp_app(expr const & e) -> result { expr const & fn = app_fn(e); result res_fn = pp_child(fn, max_bp()-1); - format fn_fmt = res_fn.first; + format fn_fmt = res_fn.fmt(); if (m_implict && !is_app(fn) && has_implicit_args(fn)) fn_fmt = compose(*g_explicit_fmt, fn_fmt); result res_arg = pp_child(app_arg(e), max_bp()); - return mk_result(group(compose(fn_fmt, nest(m_indent, compose(line(), res_arg.first)))), max_bp()-1); + return result(max_bp()-1, group(compose(fn_fmt, nest(m_indent, compose(line(), res_arg.fmt()))))); } format pretty_fn::pp_binder_block(buffer const & names, expr const & type, binder_info const & bi) { @@ -378,7 +380,7 @@ format pretty_fn::pp_binder_block(buffer const & names, expr const & type, r += format(n); r += space(); } - r += compose(colon(), nest(m_indent, compose(line(), pp_child(type, 0).first))); + r += compose(colon(), nest(m_indent, compose(line(), pp_child(type, 0).fmt()))); if (bi.is_implicit()) r += format("}"); else if (bi.is_inst_implicit()) r += format("]"); else if (bi.is_strict_implicit() && m_unicode) r += format("⦄"); @@ -421,8 +423,8 @@ auto pretty_fn::pp_lambda(expr const & e) -> result { } format r = m_unicode ? *g_lambda_n_fmt : *g_lambda_fmt; r += pp_binders(locals); - r += compose(comma(), nest(m_indent, compose(line(), pp_child(b, 0).first))); - return mk_result(r, 0); + r += compose(comma(), nest(m_indent, compose(line(), pp_child(b, 0).fmt()))); + return result(0, r); } /** \brief Similar to #is_arrow, but only returns true if binder_info is the default one. @@ -436,8 +438,8 @@ auto pretty_fn::pp_pi(expr const & e) -> result { if (is_default_arrow(e)) { result lhs = pp_child(binding_domain(e), get_arrow_prec()); result rhs = pp_child(lift_free_vars(binding_body(e), 1), get_arrow_prec()-1); - format r = group(lhs.first + space() + (m_unicode ? *g_arrow_n_fmt : *g_arrow_fmt) + line() + rhs.first); - return mk_result(r, get_arrow_prec()-1); + format r = group(lhs.fmt() + space() + (m_unicode ? *g_arrow_n_fmt : *g_arrow_fmt) + line() + rhs.fmt()); + return result(get_arrow_prec()-1, r); } else { expr b = e; buffer locals; @@ -452,8 +454,8 @@ auto pretty_fn::pp_pi(expr const & e) -> result { else r = m_unicode ? *g_pi_n_fmt : *g_pi_fmt; r += pp_binders(locals); - r += compose(comma(), nest(m_indent, compose(line(), pp_child(b, 0).first))); - return mk_result(r, 0); + r += compose(comma(), nest(m_indent, compose(line(), pp_child(b, 0).fmt()))); + return result(0, r); } } @@ -470,9 +472,9 @@ auto pretty_fn::pp_have(expr const & e) -> result { expr local = p.second; expr body = p.first; name const & n = local_pp_name(local); - format type_fmt = pp_child(mlocal_type(local), 0).first; - format proof_fmt = pp_child(proof, 0).first; - format body_fmt = pp_child(body, 0).first; + format type_fmt = pp_child(mlocal_type(local), 0).fmt(); + format proof_fmt = pp_child(proof, 0).fmt(); + format body_fmt = pp_child(body, 0).fmt(); format r = *g_have_fmt + space() + format(n) + space(); if (binding_info(binding).is_contextual()) r += compose(*g_visible_fmt, space()); @@ -481,7 +483,7 @@ auto pretty_fn::pp_have(expr const & e) -> result { r += nest(m_indent, line() + proof_fmt + comma()); r = group(r); r += line() + body_fmt; - return mk_result(r, 0); + return result(0, r); } auto pretty_fn::pp_show(expr const & e) -> result { @@ -489,17 +491,17 @@ auto pretty_fn::pp_show(expr const & e) -> result { expr s = get_annotation_arg(e); expr proof = app_arg(s); expr type = binding_domain(app_fn(s)); - format type_fmt = pp_child(type, 0).first; - format proof_fmt = pp_child(proof, 0).first; + format type_fmt = pp_child(type, 0).fmt(); + format proof_fmt = pp_child(proof, 0).fmt(); format r = *g_show_fmt + space() + nest(5, type_fmt) + comma() + space() + *g_from_fmt; r = group(r); r += nest(m_indent, compose(line(), proof_fmt)); - return mk_result(group(r), 0); + return result(0, group(r)); } auto pretty_fn::pp_explicit(expr const & e) -> result { result res_arg = pp_child(get_explicit_arg(e), max_bp()); - return mk_result(compose(*g_explicit_fmt, res_arg.first), max_bp()); + return result(max_bp(), compose(*g_explicit_fmt, res_arg.fmt())); } auto pretty_fn::pp_macro(expr const & e) -> result { @@ -510,9 +512,9 @@ auto pretty_fn::pp_macro(expr const & e) -> result { // fix macro<->pp interface format r = compose(format("["), format(macro_def(e).get_name())); for (unsigned i = 0; i < macro_num_args(e); i++) - r += nest(m_indent, compose(line(), pp_child(macro_arg(e, i), max_bp()).first)); + r += nest(m_indent, compose(line(), pp_child(macro_arg(e, i), max_bp()).fmt())); r += format("]"); - return mk_result(group(r)); + return result(group(r)); } } @@ -544,26 +546,221 @@ auto pretty_fn::pp_let(expr e) -> result { format beg = i == 0 ? space() : line(); format sep = i < sz - 1 ? comma() : format(); format entry = format(n); - format v_fmt = pp_child(v, 0).first; + format v_fmt = pp_child(v, 0).fmt(); entry += space() + *g_assign_fmt + nest(m_indent, line() + v_fmt + sep); r += nest(3 + 1, beg + group(entry)); } - format b = pp_child(e, 0).first; + format b = pp_child(e, 0).fmt(); r += line() + *g_in_fmt + space() + nest(2 + 1, b); - return mk_result(r, 0); + return result(0, r); } auto pretty_fn::pp_num(mpz const & n) -> result { - return mk_result(format(n)); + return result(format(n)); +} + +bool pretty_fn::match(level const & p, level const & l) { + if (p == l) + return true; + if (m_universes) + return false; + if (is_placeholder(p)) + return true; + if (is_succ(p) && is_succ(l)) + return match(succ_of(p), succ_of(l)); + return false; +} + +bool pretty_fn::match(expr const & p, expr const & e, buffer> & args) { + if (is_explicit(p)) { + return match(get_explicit_arg(p), e, args); + } else if (is_var(p)) { + unsigned vidx = var_idx(p); + if (vidx >= args.size()) args.resize(vidx+1); + if (args[vidx]) + return *args[vidx] == e; + args[vidx] = e; + return true; + } else if (is_placeholder(p)) { + return true; + } else if (is_constant(p)) { + if (!is_constant(e)) + return false; + levels p_ls = const_levels(p); + levels e_ls = const_levels(p); + while (!is_nil(p_ls)) { + if (is_nil(e_ls)) + return false; // e must have at least as many arguments as p + if (!match(head(p_ls), head(e_ls))) + return false; + p_ls = tail(p_ls); + e_ls = tail(e_ls); + } + return true; + } else if (is_sort(p)) { + if (!is_sort(e)) + return false; + return match(sort_level(p), sort_level(e)); + } else if (is_app(e)) { + buffer p_args, e_args; + expr const & p_fn = get_app_args(p, p_args); + expr const & e_fn = get_app_args(e, e_args); + if (!match(p_fn, e_fn, args)) + return false; + bool expl = is_explicit(p); + if (expl) { + if (p_args.size() != e_args.size()) + return false; + for (unsigned i = 0; i < p_args.size(); i++) { + if (!match(p_args[i], e_args[i], args)) + return false; + } + return true; + } else { + try { + expr fn_type = m_tc.infer(e_fn).first; + unsigned j = 0; + for (unsigned i = 0; i < e_args.size(); i++) { + fn_type = m_tc.ensure_pi(fn_type).first; + if (is_explicit(binding_info(fn_type))) { + if (j >= p_args.size()) + return false; + if (!match(p_args[j], e_args[i], args)) + return false; + j++; + } + fn_type = instantiate(binding_body(fn_type), e_args[i]); + } + return j == p_args.size(); + } catch (exception&) { + return false; + } + } + } else { + return false; + } +} + +static unsigned get_some_precedence(token_table const & t, name const & tk) { + if (tk.is_atomic() && tk.is_string()) { + if (auto p = get_precedence(t, tk.get_string())) + return *p; + } else { + if (auto p = get_precedence(t, tk.to_string().c_str())) + return *p; + } + return 0; +} + +auto pretty_fn::pp_notation_child(expr const & e, unsigned lbp, unsigned rbp) -> result { + if (is_app(e) && !m_coercion && is_coercion(m_env, get_app_fn(e))) { + return pp_coercion(e, rbp); + } else { + result r = pp(e); + // std::cout << "e: " << e << "\n"; + // std::cout << "lbp: " << lbp << ", rbp: " << rbp << ", r.lbp(): " << r.lbp() << ", r.rbp(): " << r.rbp() << "\n\n"; + if (r.rbp() < lbp || r.lbp() <= rbp) { + return result(paren(r.fmt())); + } else { + return r; + } + } +} + +auto pretty_fn::pp_notation(notation_entry const & entry, buffer> & args) -> optional { + std::reverse(args.begin(), args.end()); + if (entry.is_numeral()) { + return some(result(format(entry.get_num()))); + } else { + using notation::transition; + buffer ts; + to_buffer(entry.get_transitions(), ts); + format fmt; + unsigned i = ts.size(); + unsigned last_rbp = max_bp()-1; + unsigned token_lbp = 0; + bool last = true; + while (i > 0) { + --i; + format curr; + notation::action const & a = ts[i].get_action(); + name const & tk = ts[i].get_token(); + switch (a.kind()) { + case notation::action_kind::Skip: + curr = format(tk); + if (last) + last_rbp = get_some_precedence(m_token_table, tk); + break; + case notation::action_kind::Expr: + if (args.empty() || !args.back()) { + return optional(); + } else { + expr e = *args.back(); + args.pop_back(); + result e_r = pp_notation_child(e, token_lbp, a.rbp()); + format e_fmt = e_r.fmt(); + curr = format(tk) + space() + e_fmt; + if (last) + last_rbp = a.rbp(); + } + break; + case notation::action_kind::Exprs: + case notation::action_kind::Binder: + case notation::action_kind::Binders: + case notation::action_kind::ScopedExpr: + // TODO(Leo) + return optional(); + case notation::action_kind::Ext: + case notation::action_kind::LuaExt: + return optional(); + } + token_lbp = get_some_precedence(m_token_table, tk); + if (last) { + fmt = curr; + last = false; + } else { + fmt = curr + space() + fmt; + } + } + unsigned first_lbp = token_lbp; + if (!entry.is_nud()) { + lean_assert(!last); + if (args.size() != 1 || !args.back()) + return optional(); + expr e = *args.back(); + args.pop_back(); + format e_fmt = pp_notation_child(e, token_lbp, 0).fmt(); + fmt = e_fmt + space() + fmt; + } + return optional(result(first_lbp, last_rbp, fmt)); + } +} + +auto pretty_fn::pp_notation(expr const & e) -> optional { + if (!m_notation || is_var(e)) + return optional(); + for (notation_entry const & entry : get_notation_entries(m_env, head_index(e))) { + if (!m_unicode && !entry.is_safe_ascii()) + continue; // ignore this notation declaration since unicode support is not enabled + buffer> args; + if (match(entry.get_expr(), e, args)) { + if (auto r = pp_notation(entry, args)) + return r; + } + } + return optional(); } auto pretty_fn::pp(expr const & e) -> result { if (m_depth > m_max_depth || m_num_steps > m_max_steps) - return mk_result(m_unicode ? *g_ellipsis_n_fmt : *g_ellipsis_fmt); + return result(m_unicode ? *g_ellipsis_n_fmt : *g_ellipsis_fmt); flet let_d(m_depth, m_depth+1); m_num_steps++; - if (is_placeholder(e)) return mk_result(*g_placeholder_fmt); + if (auto r = pp_notation(e)) + return *r; + + if (is_placeholder(e)) return result(*g_placeholder_fmt); if (is_show(e)) return pp_show(e); if (is_have(e)) return pp_have(e); if (is_let(e)) return pp_let(e); @@ -588,7 +785,7 @@ auto pretty_fn::pp(expr const & e) -> result { } pretty_fn::pretty_fn(environment const & env, options const & o): - m_env(env), m_tc(env) { + m_env(env), m_tc(env), m_token_table(get_token_table(env)) { set_options_core(o); m_meta_prefix = "M"; m_next_meta_idx = 1; @@ -597,9 +794,9 @@ pretty_fn::pretty_fn(environment const & env, options const & o): format pretty_fn::operator()(expr const & e) { m_depth = 0; m_num_steps = 0; if (m_beta) - return pp_child(purify(beta_reduce(e)), 0).first; + return pp_child(purify(beta_reduce(e)), 0).fmt(); else - return pp_child(purify(e), 0).first; + return pp_child(purify(e), 0).fmt(); } formatter_factory mk_pretty_formatter_factory() { diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h index 7da3d9d59..d48bf9831 100644 --- a/src/frontends/lean/pp.h +++ b/src/frontends/lean/pp.h @@ -14,43 +14,57 @@ Author: Leonardo de Moura #include "util/sexpr/format.h" #include "kernel/environment.h" #include "kernel/type_checker.h" +#include "frontends/lean/token_table.h" namespace lean { +class notation_entry; + class pretty_fn { public: - typedef pair result; + static unsigned max_bp() { return std::numeric_limits::max(); } + class result { + unsigned m_lbp; + unsigned m_rbp; + format m_fmt; + public: + result():m_lbp(max_bp()), m_rbp(max_bp()) {} + result(format const & fmt):m_lbp(max_bp()), m_rbp(max_bp()), m_fmt(fmt) {} + result(unsigned rbp, format const & fmt):m_lbp(max_bp()), m_rbp(rbp), m_fmt(fmt) {} + result(unsigned lbp, unsigned rbp, format const & fmt):m_lbp(lbp), m_rbp(rbp), m_fmt(fmt) {} + unsigned lbp() const { return m_lbp; } + unsigned rbp() const { return m_rbp; } + format const & fmt() const { return m_fmt; } + }; private: - environment m_env; - type_checker m_tc; - unsigned m_num_steps; - unsigned m_depth; - name m_meta_prefix; - unsigned m_next_meta_idx; - name_map m_purify_meta_table; - name_map m_purify_local_table; - name_set m_purify_used_locals; + environment m_env; + type_checker m_tc; + token_table const & m_token_table; + unsigned m_num_steps; + unsigned m_depth; + name m_meta_prefix; + unsigned m_next_meta_idx; + name_map m_purify_meta_table; + name_map m_purify_local_table; + name_set m_purify_used_locals; // cached configuration - options m_options; - unsigned m_indent; - unsigned m_max_depth; - unsigned m_max_steps; - bool m_implict; //!< if true show implicit arguments - bool m_unicode; //!< if true use unicode chars - bool m_coercion; //!< if true show coercions - bool m_notation; - bool m_universes; - bool m_full_names; - bool m_private_names; - bool m_metavar_args; - bool m_beta; + options m_options; + unsigned m_indent; + unsigned m_max_depth; + unsigned m_max_steps; + bool m_implict; //!< if true show implicit arguments + bool m_unicode; //!< if true use unicode chars + bool m_coercion; //!< if true show coercions + bool m_notation; + bool m_universes; + bool m_full_names; + bool m_private_names; + bool m_metavar_args; + bool m_beta; - unsigned max_bp() const { return std::numeric_limits::max(); } name mk_metavar_name(name const & m); name mk_local_name(name const & n, name const & suggested); level purify(level const & l); expr purify(expr const & e); - result mk_result(format const & e, unsigned rbp) const { return mk_pair(e, rbp); } - result mk_result(format const & e) const { return mk_result(e, max_bp()); } bool is_implicit(expr const & f); bool is_prop(expr const & e); bool has_implicit_args(expr const & f); @@ -60,6 +74,12 @@ private: format pp_binders(buffer const & locals); format pp_level(level const & l); + bool match(level const & p, level const & l); + bool match(expr const & p, expr const & e, buffer> & args); + result pp_notation_child(expr const & e, unsigned lbp, unsigned rbp); + optional pp_notation(notation_entry const & entry, buffer> & args); + optional pp_notation(expr const & e); + result pp_coercion_fn(expr const & e, unsigned sz); result pp_coercion(expr const & e, unsigned bp); result pp_child_core(expr const & e, unsigned bp); diff --git a/src/frontends/lean/pp_options.cpp b/src/frontends/lean/pp_options.cpp index 80217a064..a4c0a8dcf 100644 --- a/src/frontends/lean/pp_options.cpp +++ b/src/frontends/lean/pp_options.cpp @@ -120,6 +120,7 @@ void finalize_pp_options() { name const & get_pp_coercions_option_name() { return *g_pp_coercions; } name const & get_pp_full_names_option_name() { return *g_pp_full_names; } name const & get_pp_universes_option_name() { return *g_pp_universes; } +name const & get_pp_notation_option_name() { return *g_pp_notation; } unsigned get_pp_max_depth(options const & opts) { return opts.get_unsigned(*g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH); } unsigned get_pp_max_steps(options const & opts) { return opts.get_unsigned(*g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); } diff --git a/src/frontends/lean/pp_options.h b/src/frontends/lean/pp_options.h index 47de14641..f60718721 100644 --- a/src/frontends/lean/pp_options.h +++ b/src/frontends/lean/pp_options.h @@ -10,6 +10,7 @@ namespace lean { name const & get_pp_coercions_option_name(); name const & get_pp_full_names_option_name(); name const & get_pp_universes_option_name(); +name const & get_pp_notation_option_name(); unsigned get_pp_max_depth(options const & opts); unsigned get_pp_max_steps(options const & opts); diff --git a/tests/lean/bug1.lean.expected.out b/tests/lean/bug1.lean.expected.out index 34a891e26..778e130ba 100644 --- a/tests/lean/bug1.lean.expected.out +++ b/tests/lean/bug1.lean.expected.out @@ -9,11 +9,11 @@ bug1.lean:13:7: error: type mismatch at definition 'and_intro', has type p → q → (∀ (c : bool), (p → q → c) → c) but is expected to have type ∀ (p q : bool), - p → q → and p p + p → q → p ∧ p bug1.lean:17:7: error: type mismatch at definition 'and_intro', has type ∀ (p q : bool), p → q → (∀ (c : bool), (p → q → c) → c) but is expected to have type ∀ (p q : bool), - p → q → and q p -and_intro : ∀ (p q : bool), p → q → and p q + p → q → q ∧ p +and_intro : ∀ (p q : bool), p → q → p ∧ q diff --git a/tests/lean/calc1.lean.expected.out b/tests/lean/calc1.lean.expected.out index e18623b03..3788f01bf 100644 --- a/tests/lean/calc1.lean.expected.out +++ b/tests/lean/calc1.lean.expected.out @@ -1,4 +1,4 @@ -le_eq_trans a d e (le_trans a c d (eq_le_trans a b c H1 H2) H3) H4 : le a e +le_eq_trans a d e (le_trans a c d (eq_le_trans a b c H1 H2) H3) H4 : a ≤ e calc1.lean:38:10: error: invalid 'calc' expression, transitivity rule is not defined for current step -le_lt_trans b c d H2 H5 : lt b d +le_lt_trans b c d H2 H5 : b < d [choice (@le2_trans b d e (@le2_trans b c d H2 H3) H4) (@le_trans b d e (@le_trans b c d H2 H3) H4)] diff --git a/tests/lean/crash.lean.expected.out b/tests/lean/crash.lean.expected.out index 401a3e86c..7e21fe986 100644 --- a/tests/lean/crash.lean.expected.out +++ b/tests/lean/crash.lean.expected.out @@ -1,9 +1,9 @@ crash.lean:8:12: error: type mismatch at application - have H' : not P, from H, + have H' : ¬ P, from H, ?M_1 term H has type P but is expected to have type - not P + ¬ P diff --git a/tests/lean/have1.lean.expected.out b/tests/lean/have1.lean.expected.out index 4bb73aac7..37dd9aa36 100644 --- a/tests/lean/have1.lean.expected.out +++ b/tests/lean/have1.lean.expected.out @@ -1,9 +1,8 @@ -have e1 [visible] : eq a b, from H1, -have e2 : eq a c, from trans e1 H2, -have e3 : eq c a, from symm e2, -have e4 [visible] : eq b a, from symm e1, -have e5 : eq b c, from trans e4 e2, -have e6 : eq a a, from - trans H1 (trans H2 (trans (symm H2) (trans (symm H1) (trans H1 (trans H2 (trans (symm H2) (symm H1))))))), -trans e3 e2 : - eq c c +have e1 [visible] : a = b, from H1, +have e2 : a = c, from e1 ⬝ H2, +have e3 : c = a, from e2 ⁻¹, +have e4 [visible] : b = a, from e1 ⁻¹, +have e5 : b = c, from e4 ⬝ e2, +have e6 : a = a, from H1 ⬝ H2 ⬝ H2 ⁻¹ ⬝ H1 ⁻¹ ⬝ H1 ⬝ H2 ⬝ H2 ⁻¹ ⬝ H1 ⁻¹, +e3 ⬝ e2 : + c = c diff --git a/tests/lean/interactive/coe.input.expected.out b/tests/lean/interactive/coe.input.expected.out index 90c3026cc..23514d74c 100644 --- a/tests/lean/interactive/coe.input.expected.out +++ b/tests/lean/interactive/coe.input.expected.out @@ -2,7 +2,7 @@ -- ENDWAIT -- BEGININFO -- TYPE|5|16 -decidable (eq a b) +decidable (a = b) -- ACK -- SYNTH|5|16 int.has_decidable_eq a b diff --git a/tests/lean/interactive/findp.input.expected.out b/tests/lean/interactive/findp.input.expected.out index 58d75f863..69a75a3cd 100644 --- a/tests/lean/interactive/findp.input.expected.out +++ b/tests/lean/interactive/findp.input.expected.out @@ -4,8 +4,8 @@ false|Prop false.rec|∀ (C : Prop), false → C false_elim|false → ?c -not_false_trivial|not false -true_ne_false|not (eq true false) -p_ne_false|?p → ne ?p false -eq_false_elim|eq ?a false → not ?a +not_false_trivial|¬ false +true_ne_false|¬ true = false +p_ne_false|?p → ?p ≠ false +eq_false_elim|?a = false → ¬ ?a -- ENDFINDP diff --git a/tests/lean/interactive/in4.input.expected.out b/tests/lean/interactive/in4.input.expected.out index ae09779f3..914131697 100644 --- a/tests/lean/interactive/in4.input.expected.out +++ b/tests/lean/interactive/in4.input.expected.out @@ -2,7 +2,7 @@ -- ENDWAIT -- BEGININFO -- TYPE|9|0 -eq (tst.foo a b) (tst.foo a b) +tst.foo a b = tst.foo a b -- ACK -- IDENTIFIER|9|0 rfl @@ -17,7 +17,7 @@ rfl -- ENDWAIT -- BEGININFO -- TYPE|9|0 -eq (tst.foo a b) (tst.foo a b) +tst.foo a b = tst.foo a b -- ACK -- IDENTIFIER|9|0 rfl diff --git a/tests/lean/interactive/in5.input.expected.out b/tests/lean/interactive/in5.input.expected.out index 548b8df39..2f11a9c76 100644 --- a/tests/lean/interactive/in5.input.expected.out +++ b/tests/lean/interactive/in5.input.expected.out @@ -2,7 +2,7 @@ -- ENDWAIT -- BEGININFO -- TYPE|4|0 -A → B → and A B +A → B → A ∧ B -- ACK -- IDENTIFIER|4|0 and.intro diff --git a/tests/lean/interactive/t4.input.expected.out b/tests/lean/interactive/t4.input.expected.out index 99e8c4f46..b4de992dc 100644 --- a/tests/lean/interactive/t4.input.expected.out +++ b/tests/lean/interactive/t4.input.expected.out @@ -2,7 +2,7 @@ -- ENDWAIT -- BEGININFO -- TYPE|6|6 -(nat → Prop) → nat +(ℕ → Prop) → ℕ -- ACK -- IDENTIFIER|6|6 epsilon @@ -17,7 +17,7 @@ epsilon x -- ACK -- TYPE|6|21 -Type +Type₁ -- ACK -- IDENTIFIER|6|21 nat diff --git a/tests/lean/notation.lean b/tests/lean/notation.lean new file mode 100644 index 000000000..4db3d71cd --- /dev/null +++ b/tests/lean/notation.lean @@ -0,0 +1,18 @@ +import logic data.nat.basic +open num +constant b : num +check b + b + b +check true ∧ false ∧ true +check (true ∧ false) ∧ true +check 2 + (2 + 2) +check (2 + 2) + 2 +check 1 = (2 + 3)*2 +check 2 + 3 * 2 = 3 * 2 + 2 +check (true ∨ false) = (true ∨ false) ∧ true +check true ∧ (false ∨ true) +constant A : Type₁ +constant a : A +notation 1 := a +check a +open nat +check ℕ → ℕ diff --git a/tests/lean/notation.lean.expected.out b/tests/lean/notation.lean.expected.out new file mode 100644 index 000000000..81c54d25b --- /dev/null +++ b/tests/lean/notation.lean.expected.out @@ -0,0 +1,11 @@ +b + b + b : num +true ∧ false ∧ true : Prop +(true ∧ false) ∧ true : Prop +2 + (2 + 2) : num +2 + 2 + 2 : num +1 = (2 + 3) * 2 : Prop +2 + 3 * 2 = 3 * 2 + 2 : Prop +(true ∨ false) = (true ∨ false) ∧ true : Prop +true ∧ (false ∨ true) : Prop +1 : A +ℕ → ℕ : Type₁ diff --git a/tests/lean/show1.lean.expected.out b/tests/lean/show1.lean.expected.out index 415259862..4653b8060 100644 --- a/tests/lean/show1.lean.expected.out +++ b/tests/lean/show1.lean.expected.out @@ -1,8 +1,8 @@ -show eq a c, from eq.trans H1 H2 : eq a c +show a = c, from H1 ⬝ H2 : a = c ------------ -have e1 [visible] : eq a b, from H1, -have e2 : eq a c, from eq.trans e1 H2, -have e3 : eq c a, from eq.symm e2, -have e4 [visible] : eq b a, from eq.symm e1, -show eq b c, from eq.trans (eq.symm e1) e2 : - eq b c +have e1 [visible] : a = b, from H1, +have e2 : a = c, from e1 ⬝ H2, +have e3 : c = a, from e2 ⁻¹, +have e4 [visible] : b = a, from e1 ⁻¹, +show b = c, from e1 ⁻¹ ⬝ e2 : + b = c diff --git a/tests/lean/t10.lean.expected.out b/tests/lean/t10.lean.expected.out index 844082b21..53bd0c09b 100644 --- a/tests/lean/t10.lean.expected.out +++ b/tests/lean/t10.lean.expected.out @@ -1,6 +1,6 @@ -ite (and p q) (f x) y : N +if p ∧ q then f x else y : N t10.lean:14:6: error: type mismatch at application - ite (and p q) q + ite (p ∧ q) q term q has type @@ -9,4 +9,4 @@ but is expected to have type N cons x (cons y (cons z (cons x (cons y (cons y nil))))) : list cons x nil : list -nil : list +[ ] : list diff --git a/tests/lean/t14.lean.expected.out b/tests/lean/t14.lean.expected.out index 7d7753c38..0af9971a3 100644 --- a/tests/lean/t14.lean.expected.out +++ b/tests/lean/t14.lean.expected.out @@ -8,8 +8,8 @@ t14.lean:23:26: error: invalid 'open/export' command option, mixing explicit and a : A c : A A : Type -f a c : A -foo.f foo.a foo.c : foo.A +a * c : A +foo.a * foo.c : foo.A t14.lean:46:8: error: unknown identifier 'a' f a c : A t14.lean:52:9: error: unexpected token diff --git a/tests/lean/t9.lean.expected.out b/tests/lean/t9.lean.expected.out index e02d98ed3..82c3ec2fb 100644 --- a/tests/lean/t9.lean.expected.out +++ b/tests/lean/t9.lean.expected.out @@ -1,3 +1,3 @@ -add a (mul b a) : N +a + b * a : N t9.lean:16:7: error: invalid expression -add a (mul b a) : N +a + b * a : N diff --git a/tests/lean/tuple.lean.expected.out b/tests/lean/tuple.lean.expected.out index f14f0011e..f598af3c4 100644 --- a/tests/lean/tuple.lean.expected.out +++ b/tests/lean/tuple.lean.expected.out @@ -1 +1 @@ -tuple.{l_1} : Type.{max 1 l_1} → nat → Type.{max 1 l_1} +tuple.{l_1} : Type.{max 1 l_1} → ℕ → Type.{max 1 l_1} diff --git a/tests/lean/uni_bug1.lean.expected.out b/tests/lean/uni_bug1.lean.expected.out index 9cadb966b..ce4339851 100644 --- a/tests/lean/uni_bug1.lean.expected.out +++ b/tests/lean/uni_bug1.lean.expected.out @@ -1 +1 @@ -f 1 0 (Rtrue (pr1 (pair 1 0)) 0) : nat +f 1 0 (Rtrue (pr₁ (pair 1 0)) 0) : ℕ diff --git a/tests/lean/univ.lean.expected.out b/tests/lean/univ.lean.expected.out index ba9e87446..73483468e 100644 --- a/tests/lean/univ.lean.expected.out +++ b/tests/lean/univ.lean.expected.out @@ -1,13 +1,13 @@ univ.lean:5:9: error: solution computed by the elaborator forces a universe placeholder to be a fixed value, computed sort is - Type.{1} + Type₁ univ.lean:7:9: error: solution computed by the elaborator forces a universe placeholder to be a fixed value, computed sort is - Type.{1} -id Type num : Type -id Type num : Type + Type₁ +id Type₁ num : Type₁ +id Type₁ num : Type₁ univ.lean:13:9: error: solution computed by the elaborator forces a universe placeholder to be a fixed value, computed sort is - Type.{1} -id Type num : Type + Type₁ +id Type₁ num : Type₁ univ.lean:17:9: error: solution computed by the elaborator forces a universe placeholder to be a fixed value, computed sort is - Type.{2} + Type₂ univ.lean:19:9: error: solution computed by the elaborator forces a universe placeholder to be a fixed value, computed sort is - Type.{2} + Type₂ diff --git a/tests/lean/var2.lean.expected.out b/tests/lean/var2.lean.expected.out index 6ce049e99..743a819dc 100644 --- a/tests/lean/var2.lean.expected.out +++ b/tests/lean/var2.lean.expected.out @@ -1 +1 @@ -foo : Π (B : Type), B → (Π (A : Type), A → eq A B → Prop) +foo : Π (B : Type), B → (Π (A : Type), A → A = B → Prop)