From 2ef7b9be2f16bcdf5601b0c2be89de05f7eb0aea Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 9 Jul 2014 01:12:36 -0700 Subject: [PATCH] feat(frontends/lean): add basic pretty printer Signed-off-by: Leonardo de Moura --- src/frontends/lean/CMakeLists.txt | 2 +- src/frontends/lean/builtin_cmds.cpp | 7 +- src/frontends/lean/pp.cpp | 327 +++++++++++++++++++ src/frontends/lean/pp.h | 75 +++++ src/frontends/lean/pp_options.cpp | 30 +- src/frontends/lean/pp_options.h | 3 +- src/library/aliases.h | 1 - src/shell/lean.cpp | 3 +- tests/lean/alias.lean.expected.out | 10 +- tests/lean/bug1.lean.expected.out | 20 +- tests/lean/calc1.lean.expected.out | 2 +- tests/lean/interactive/t3.input.expected.out | 4 +- tests/lean/let1.lean.expected.out | 41 ++- tests/lean/t11.lean.expected.out | 6 +- tests/lean/t12.lean.expected.out | 2 +- tests/lean/t13.lean.expected.out | 4 +- tests/lean/t14.lean.expected.out | 18 +- tests/lean/t3.lean.expected.out | 20 +- tests/lean/t4.lean.expected.out | 32 +- tests/lean/t5.lean.expected.out | 6 +- tests/lean/t6.lean.expected.out | 6 +- tests/lean/t7.lean.expected.out | 11 +- 22 files changed, 534 insertions(+), 96 deletions(-) create mode 100644 src/frontends/lean/pp.cpp create mode 100644 src/frontends/lean/pp.h diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index 69bd8f4bd..44078360e 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -4,6 +4,6 @@ parser_pos_provider.cpp builtin_cmds.cpp builtin_exprs.cpp interactive.cpp notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp inductive_cmd.cpp elaborator.cpp dependencies.cpp parser_bindings.cpp proof_qed_ext.cpp -class.cpp pp_options.cpp tactic_hint.cpp) +class.cpp pp_options.cpp tactic_hint.cpp pp.cpp) target_link_libraries(lean_frontend ${LEAN_LIBS}) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index a98735e61..12d0e845e 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -90,7 +90,12 @@ environment check_cmd(parser & p) { std::tie(e, new_ls) = p.elaborate_relaxed(e); auto tc = mk_type_checker_with_hints(p.env(), p.mk_ngen()); expr type = tc->check(e, append(ls, new_ls)); - p.regular_stream() << e << " : " << type << endl; + + formatter fmt = p.ios().get_formatter(); + options opts = p.ios().get_options(); + unsigned indent = get_pp_indent(opts); + format r = group(format{fmt(p.env(), e, opts), space(), colon(), nest(indent, compose(line(), fmt(p.env(), type, opts)))}); + p.regular_stream() << mk_pair(r, opts) << endl; return p.env(); } diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp new file mode 100644 index 000000000..444a6e15d --- /dev/null +++ b/src/frontends/lean/pp.cpp @@ -0,0 +1,327 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "util/flet.h" +#include "kernel/replace_fn.h" +#include "kernel/free_vars.h" +#include "library/aliases.h" +#include "library/scoped_ext.h" +#include "library/coercion.h" +#include "frontends/lean/pp.h" +#include "frontends/lean/pp_options.h" +#include "frontends/lean/token_table.h" + +namespace lean { +static format g_ellipsis_n_fmt= highlight(format("\u2026")); +static format g_ellipsis_fmt = highlight(format("...")); +static format g_lambda_n_fmt = highlight_keyword(format("\u03BB")); +static format g_lambda_fmt = highlight_keyword(format("fun")); +static format g_forall_n_fmt = highlight_keyword(format("\u2200")); +static format g_forall_fmt = highlight_keyword(format("forall")); +static format g_pi_n_fmt = highlight_keyword(format("Π")); +static format g_pi_fmt = highlight_keyword(format("Pi")); +static format g_arrow_n_fmt = highlight_keyword(format("\u2192")); +static format g_arrow_fmt = highlight_keyword(format("->")); + +name pretty_fn::mk_metavar_name(name const & m) { + if (auto it = m_purify_meta_table.find(m)) + return *it; + name new_m = m_meta_prefix.append_after(m_next_meta_idx); + m_next_meta_idx++; + m_purify_meta_table.insert(m, new_m); + return new_m; +} + +name pretty_fn::mk_local_name(name const & m) { + unsigned i = 1; + name r = m; + while (m_purify_locals.contains(r)) { + r = m.append_after(i); + i++; + } + m_purify_locals.insert(r); + return r; +} + +level pretty_fn::purify(level const & l) { + if (!m_universes || !has_meta(l)) + return l; + return replace(l, [&](level const & l) { + if (!has_meta(l)) + return some_level(l); + if (is_meta(l)) + return some_level(mk_meta_univ(mk_metavar_name(meta_id(l)))); + return none_level(); + }); +} + +/** \brief Make sure that all metavariables have reasonable names, + and for all local constants l1 l2, local_pp_name(l1) != local_pp_name(l2). + + \remark pretty_fn will create new local constants when pretty printing, + but it will make sure that the new constants will not produce collisions. +*/ +expr pretty_fn::purify(expr const & e) { + if (!has_expr_metavar(e) && !has_local(e) && (!m_universes || !has_univ_metavar(e))) + return e; + return replace(e, [&](expr const & e, unsigned) { + if (!has_expr_metavar(e) && !has_local(e) && (!m_universes || !has_univ_metavar(e))) + return some_expr(e); + else if (is_metavar(e)) + return some_expr(mk_metavar(mk_metavar_name(mlocal_name(e)), mlocal_type(e))); + else if (is_local(e)) + return some_expr(mk_local(mlocal_name(e), mk_local_name(local_pp_name(e)), mlocal_type(e), local_info(e))); + else if (is_constant(e)) + return some_expr(update_constant(e, map(const_levels(e), [&](level const & l) { return purify(l); }))); + else if (is_sort(e)) + return some_expr(update_sort(e, purify(sort_level(e)))); + else + return none_expr(); + }); +} + +void pretty_fn::set_options(options const & o) { + m_indent = get_pp_indent(o); + m_max_depth = get_pp_max_depth(o); + m_max_steps = get_pp_max_steps(o); + m_implict = get_pp_implicit(o); + m_unicode = get_pp_unicode(o); + m_coercion = get_pp_coercion(o); + m_notation = get_pp_notation(o); + m_universes = get_pp_universes(o); +} + +format pretty_fn::pp_level(level const & l) { + return ::lean::pp(l, m_unicode, m_indent); +} + +bool pretty_fn::is_implicit(expr const & f) { + if (m_implict) + return false; // showing implicit arguments + try { + binder_info bi = binding_info(m_tc.ensure_pi(m_tc.infer(f))); + return bi.is_implicit() || bi.is_strict_implicit(); + } catch (...) { + return false; + } +} + +bool pretty_fn::is_prop(expr const & e) { + try { + return m_env.impredicative() && m_tc.is_prop(e); + } catch (...) { + return false; + } +} + +auto pretty_fn::pp_child(expr const & e, unsigned bp) -> result { + if (is_app(e) && is_implicit(app_fn(e))) { + return pp_child(app_fn(e), bp); + } else if (is_app(e) && !m_coercion && is_coercion(m_env, get_app_fn(e))) { + return pp_child(app_arg(e), bp); // TODO(Fix): this is not correct for coercions to function-class + } else { + result r = pp(e); + if (r.second < bp) { + return mk_result(paren(r.first)); + } else { + return r; + } + } +} + +auto pretty_fn::pp_var(expr const & e) -> result { + unsigned vidx = var_idx(e); + return mk_result(compose(format("#"), format(vidx))); +} + +auto pretty_fn::pp_sort(expr const & e) -> result { + if (m_env.impredicative() && e == Bool) { + return mk_result(format("Bool")); + } else if (m_universes) { + return mk_result(group(format({format("Type.{"), nest(6, pp_level(sort_level(e))), format("}")}))); + } else { + return mk_result(format("Type")); + } +} + +auto pretty_fn::pp_const(expr const & e) -> result { + name n = const_name(e); + if (auto it = is_aliased(m_env, mk_constant(n))) { // TODO(Leo): fix is_aliased should get a name as argument + n = *it; + } else { + for (name const & ns : get_namespaces(m_env)) { + name new_n = n.replace_prefix(ns, name()); + if (new_n != n) { + n = new_n; + break; + } + } + } + if (m_universes) { + format r = compose(format(n), format(".{")); + for (auto const & l : const_levels(e)) { + format l_fmt = pp_level(l); + if (is_max(l) || is_imax(l)) + l_fmt = paren(l_fmt); + r += nest(m_indent, compose(line(), l_fmt)); + } + r += format("}"); + return mk_result(group(r)); + } else { + return mk_result(format(n)); + } +} + +auto pretty_fn::pp_meta(expr const & e) -> result { + return mk_result(compose(format("?"), format(mlocal_name(e)))); +} + +auto pretty_fn::pp_local(expr const & e) -> result { + return mk_result(format(local_pp_name(e))); +} + +auto pretty_fn::pp_app(expr const & e) -> result { + result res_fn = pp_child(app_fn(e), max_bp()-1); + result res_arg = pp_child(app_arg(e), max_bp()); + return mk_result(group(compose(res_fn.first, nest(m_indent, compose(line(), res_arg.first)))), max_bp()-1); +} + +format pretty_fn::pp_binder_block(buffer const & names, expr const & type, binder_info const & bi) { + format r; + if (bi.is_implicit()) r += format("{"); + else if (bi.is_cast()) r += format("["); + else if (bi.is_strict_implicit() && m_unicode) r += format("⦃"); + else if (bi.is_strict_implicit() && !m_unicode) r += format("{{"); + else r += format("("); + for (name const & n : names) { + r += format(n); + r += space(); + } + r += compose(colon(), nest(m_indent, compose(line(), pp_child(type, 0).first))); + if (bi.is_implicit()) r += format("}"); + else if (bi.is_cast()) r += format("]"); + else if (bi.is_strict_implicit() && m_unicode) r += format("⦄"); + else if (bi.is_strict_implicit() && !m_unicode) r += format("}}"); + else r += format(")"); + return group(r); +} + +format pretty_fn::pp_binders(buffer const & locals) { + unsigned num = locals.size(); + buffer names; + expr local = locals[0]; + expr type = mlocal_type(local); + binder_info bi = local_info(local); + names.push_back(local_pp_name(local)); + format r; + for (unsigned i = 1; i < num; i++) { + expr local = locals[i]; + if (mlocal_type(local) == type && local_info(local) == bi) { + names.push_back(local_pp_name(local)); + } else { + r += group(compose(line(), pp_binder_block(names, type, bi))); + names.clear(); + type = mlocal_type(local); + bi = local_info(local); + names.push_back(local_pp_name(local)); + } + } + r += group(compose(line(), pp_binder_block(names, type, bi))); + return r; +} + +auto pretty_fn::pp_lambda(expr const & e) -> result { + expr b = e; + buffer locals; + while (is_lambda(b)) { + auto p = binding_body_fresh(b, true); + locals.push_back(p.second); + b = p.first; + } + 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); +} + +auto pretty_fn::pp_pi(expr const & e) -> result { + if (is_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(format{lhs.first, space(), m_unicode ? g_arrow_n_fmt : g_arrow_fmt, line(), rhs.first}); + return mk_result(r, get_arrow_prec()-1); + } else { + expr b = e; + buffer locals; + while (is_pi(b) && !is_arrow(b)) { + auto p = binding_body_fresh(b, true); + locals.push_back(p.second); + b = p.first; + } + format r; + if (is_prop(b)) + r = m_unicode ? g_forall_n_fmt : g_forall_fmt; + 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); + } +} + +auto pretty_fn::pp_macro(expr const & e) -> result { + // TODO(Leo): handle let, have macro annotations + // 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 += format("]"); + return mk_result(group(r)); +} + +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); + flet let_d(m_depth, m_depth+1); + m_num_steps++; + + switch (e.kind()) { + case expr_kind::Var: return pp_var(e); + case expr_kind::Sort: return pp_sort(e); + case expr_kind::Constant: return pp_const(e); + case expr_kind::Meta: return pp_meta(e); + case expr_kind::Local: return pp_local(e); + case expr_kind::App: return pp_app(e); + case expr_kind::Lambda: return pp_lambda(e); + case expr_kind::Pi: return pp_pi(e); + case expr_kind::Macro: return pp_macro(e); + } + lean_unreachable(); // LCOV_EXCL_LINE +} + +pretty_fn::pretty_fn(environment const & env, options const & o): + m_env(env), m_tc(env) { + set_options(o); + m_meta_prefix = "M"; + m_next_meta_idx = 1; +} + +format pretty_fn::operator()(expr const & e) { + return pp_child(purify(e), 0).first; +} + +class pretty_formatter_cell : public formatter_cell { +public: + /** \brief Format the given expression. */ + virtual format operator()(environment const & env, expr const & e, options const & o) const { + return pretty_fn(env, o)(e); + } +}; + +formatter mk_pretty_formatter() { + return mk_formatter(pretty_formatter_cell()); +} +} diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h new file mode 100644 index 000000000..bf86075ca --- /dev/null +++ b/src/frontends/lean/pp.h @@ -0,0 +1,75 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include +#include "util/name_map.h" +#include "util/name_set.h" +#include "util/sexpr/options.h" +#include "util/sexpr/format.h" +#include "kernel/environment.h" +#include "kernel/type_checker.h" + +namespace lean { +class pretty_fn { +public: + typedef std::pair result; +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_set m_purify_locals; + // cached configuration + 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; + + void set_options(options const & o); + + unsigned max_bp() const { return std::numeric_limits::max(); } + name mk_metavar_name(name const & m); + name mk_local_name(name const & m); + 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); + + format pp_binder_block(buffer const & names, expr const & type, binder_info const & bi); + format pp_binders(buffer const & locals); + format pp_level(level const & l); + + result pp_child(expr const & e, unsigned bp); + result pp_var(expr const & e); + result pp_sort(expr const & e); + result pp_const(expr const & e); + result pp_meta(expr const & e); + result pp_local(expr const & e); + result pp_app(expr const & e); + result pp_lambda(expr const & e); + result pp_pi(expr const & e); + result pp_macro(expr const & e); + +public: + pretty_fn(environment const & env, options const & o); + result pp(expr const & e); + + format operator()(expr const & e); +}; + +formatter mk_pretty_formatter(); +} diff --git a/src/frontends/lean/pp_options.cpp b/src/frontends/lean/pp_options.cpp index caf939908..9a68822f1 100644 --- a/src/frontends/lean/pp_options.cpp +++ b/src/frontends/lean/pp_options.cpp @@ -26,12 +26,8 @@ Author: Leonardo de Moura #define LEAN_DEFAULT_PP_COERCION false #endif -#ifndef LEAN_DEFAULT_PP_EXTRA_LETS -#define LEAN_DEFAULT_PP_EXTRA_LETS true -#endif - -#ifndef LEAN_DEFAULT_PP_ALIAS_MIN_WEIGHT -#define LEAN_DEFAULT_PP_ALIAS_MIN_WEIGHT 20 +#ifndef LEAN_DEFAULT_PP_UNIVERSES +#define LEAN_DEFAULT_PP_UNIVERSES false #endif namespace lean { @@ -40,8 +36,7 @@ static name g_pp_max_steps {"lean", "pp", "max_steps"}; static name g_pp_notation {"lean", "pp", "notation"}; static name g_pp_implicit {"lean", "pp", "implicit"}; static name g_pp_coercion {"lean", "pp", "coercion"}; -static name g_pp_extra_lets {"lean", "pp", "extra_lets"}; -static name g_pp_alias_min_weight {"lean", "pp", "alias_min_weight"}; +static name g_pp_universes {"lean", "pp", "universes"}; RegisterUnsignedOption(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH, "(lean pretty printer) maximum expression depth, after that it will use ellipsis"); @@ -53,16 +48,13 @@ RegisterBoolOption(g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT, "(lean pretty printer) display implicit parameters"); RegisterBoolOption(g_pp_coercion, LEAN_DEFAULT_PP_COERCION, "(lean pretty printer) display coercions"); -RegisterBoolOption(g_pp_extra_lets, LEAN_DEFAULT_PP_EXTRA_LETS, - "(lean pretty printer) introduce extra let expressions when displaying shared terms"); -RegisterUnsignedOption(g_pp_alias_min_weight, LEAN_DEFAULT_PP_ALIAS_MIN_WEIGHT, - "(lean pretty printer) mimimal weight (approx. size) of a term to be considered a shared term"); +RegisterBoolOption(g_pp_coercion, LEAN_DEFAULT_PP_UNIVERSES, + "(lean pretty printer) display universes"); -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); } -bool get_pp_notation(options const & opts) { return opts.get_bool(g_pp_notation, LEAN_DEFAULT_PP_NOTATION); } -bool get_pp_implicit(options const & opts) { return opts.get_bool(g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT); } -bool get_pp_coercion(options const & opts) { return opts.get_bool(g_pp_coercion, LEAN_DEFAULT_PP_COERCION); } -bool get_pp_extra_lets(options const & opts) { return opts.get_bool(g_pp_extra_lets, LEAN_DEFAULT_PP_EXTRA_LETS); } -unsigned get_pp_alias_min_weight(options const & opts) { return opts.get_unsigned(g_pp_alias_min_weight, LEAN_DEFAULT_PP_ALIAS_MIN_WEIGHT); } +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); } +bool get_pp_notation(options const & opts) { return opts.get_bool(g_pp_notation, LEAN_DEFAULT_PP_NOTATION); } +bool get_pp_implicit(options const & opts) { return opts.get_bool(g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT); } +bool get_pp_coercion(options const & opts) { return opts.get_bool(g_pp_coercion, LEAN_DEFAULT_PP_COERCION); } +bool get_pp_universes(options const & opts) { return opts.get_bool(g_pp_universes, LEAN_DEFAULT_PP_UNIVERSES); } } diff --git a/src/frontends/lean/pp_options.h b/src/frontends/lean/pp_options.h index 470a0a9b7..18f2b6495 100644 --- a/src/frontends/lean/pp_options.h +++ b/src/frontends/lean/pp_options.h @@ -12,6 +12,5 @@ unsigned get_pp_max_steps(options const & opts); bool get_pp_notation(options const & opts); bool get_pp_implicit(options const & opts); bool get_pp_coercion(options const & opts); -bool get_pp_extra_lets(options const & opts); -unsigned get_pp_alias_min_weight(options const & opts); +bool get_pp_universes(options const & opts); } diff --git a/src/library/aliases.h b/src/library/aliases.h index 6e4e9de99..536087927 100644 --- a/src/library/aliases.h +++ b/src/library/aliases.h @@ -18,7 +18,6 @@ environment add_alias(environment const & env, name const & a, expr const & e); */ environment add_decl_alias(environment const & env, name const & a, expr const & e); - /** \brief If \c t is aliased in \c env, then return its name. Otherwise, return none. */ optional is_aliased(environment const & env, expr const & t); diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index e90ca6ad4..5096d6e71 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -26,6 +26,7 @@ Author: Leonardo de Moura #include "library/io_state_stream.h" #include "library/error_handling/error_handling.h" #include "frontends/lean/parser.h" +#include "frontends/lean/pp.h" #include "frontends/lean/interactive.h" #include "frontends/lean/dependencies.h" #include "frontends/lua/register_modules.h" @@ -194,7 +195,7 @@ int main(int argc, char ** argv) { } environment env = mode == lean_mode::Standard ? mk_environment(trust_lvl) : mk_hott_environment(trust_lvl); - io_state ios(lean::mk_simple_formatter()); + io_state ios(lean::mk_pretty_formatter()); if (quiet) ios.set_option("verbose", false); script_state S = lean::get_thread_script_state(); diff --git a/tests/lean/alias.lean.expected.out b/tests/lean/alias.lean.expected.out index 7a9e1b3aa..d5c8f8fd8 100644 --- a/tests/lean/alias.lean.expected.out +++ b/tests/lean/alias.lean.expected.out @@ -1,5 +1,5 @@ -(choice N1.foo N2.foo) a b -(choice N2.foo N1.foo) a b -(choice N1.foo N2.foo) a b -(choice N1.foo N2.foo) a b -(choice N2.foo N1.foo) a b +[choice foo foo] a b +[choice foo foo] a b +[choice foo foo] a b +[choice foo foo] a b +[choice foo foo] a b diff --git a/tests/lean/bug1.lean.expected.out b/tests/lean/bug1.lean.expected.out index 962bdf903..8372fa6c9 100644 --- a/tests/lean/bug1.lean.expected.out +++ b/tests/lean/bug1.lean.expected.out @@ -1,13 +1,19 @@ bug1.lean:9:7: error: type mismatch at definition 'and_intro', expected type - Pi (p : bool) (q : bool) (H1 : p) (H2 : q), a + ∀ (p q : bool), + p → q → a given type: - Pi (p : bool) (q : bool) (H1 : p) (H2 : q) (c : bool) (H : p -> q -> c), c + ∀ (p q : bool), + p → q → (∀ (c : bool), (p → q → c) → c) bug1.lean:13:7: error: type mismatch at definition 'and_intro', expected type - Pi (p : bool) (q : bool) (H1 : p) (H2 : q), (and p p) + ∀ (p q : bool), + p → q → and p p given type: - Pi (p : bool) (q : bool) (H1 : p) (H2 : q) (c : bool) (H : p -> q -> c), c + ∀ (p q : bool), + p → q → (∀ (c : bool), (p → q → c) → c) bug1.lean:17:7: error: type mismatch at definition 'and_intro', expected type - Pi (p : bool) (q : bool) (H1 : p) (H2 : q), (and q p) + ∀ (p q : bool), + p → q → and q p given type: - Pi (p : bool) (q : bool) (H1 : p) (H2 : q) (c : bool) (H : p -> q -> c), c -and_intro : Pi (p : bool) (q : bool) (H1 : p) (H2 : q), (and p q) + ∀ (p q : bool), + p → q → (∀ (c : bool), (p → q → c) → c) +and_intro : ∀ (p q : bool), p → q → and p q diff --git a/tests/lean/calc1.lean.expected.out b/tests/lean/calc1.lean.expected.out index 7d67c62a1..3dc100662 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 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 -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) +[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/interactive/t3.input.expected.out b/tests/lean/interactive/t3.input.expected.out index a54274fe6..411dab390 100644 --- a/tests/lean/interactive/t3.input.expected.out +++ b/tests/lean/interactive/t3.input.expected.out @@ -1,3 +1,3 @@ -fun (A : Type.{l_1}), A : Type.{l_1} -> Type.{l_1} -fun (A : Type.{l_1}), A : Type.{l_1} -> Type.{l_1} +λ (A : Type), A : Type → Type +λ (A : Type), A : Type → Type done diff --git a/tests/lean/let1.lean.expected.out b/tests/lean/let1.lean.expected.out index b572d9e92..95ea7fb12 100644 --- a/tests/lean/let1.lean.expected.out +++ b/tests/lean/let1.lean.expected.out @@ -1,7 +1,40 @@ -let and_intro : Pi (p : Bool) (q : Bool) (H1 : p) (H2 : q), ((fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q) := fun (p : Bool) (q : Bool) (H1 : p) (H2 : q) (c : Bool) (H : p -> q -> c), (H H1 H2) in (let and_elim_left : Pi (p : Bool) (q : Bool) (H : (fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q), p := fun (p : Bool) (q : Bool) (H : (fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q), (H p (fun (H1 : p) (H2 : q), H1)) in (let and_elim_right : Pi (p : Bool) (q : Bool) (H : (fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q), q := fun (p : Bool) (q : Bool) (H : (fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q), (H q (fun (H1 : p) (H2 : q), H2)) in and_intro)) : Pi (p : Bool) (q : Bool) (H1 : p) (H2 : q), ((fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q) +[let + ((λ (and_intro : ∀ (p q : Bool), p → q → (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q), + [let + ((λ + (and_elim_left : ∀ (p q : Bool), (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q → p), + [let + ((λ + (and_elim_right : + ∀ (p q : Bool), + (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q → q), + and_intro) + (λ (p q : Bool) (H : (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q), + H q (λ (H1 : p) (H2 : q), H2)))]) + (λ (p q : Bool) (H : (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q), + H p (λ (H1 : p) (H2 : q), H1)))]) + (λ (p q : Bool) (H1 : p) (H2 : q) (c : Bool) (H : p → q → c), H H1 H2))] : + ∀ (p q : Bool), + p → q → (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q let1.lean:17:20: error: type mismatch at application - (fun (and_intro : Pi (p : Bool) (q : Bool) (H1 : p) (H2 : q), ((fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) q p)), (let and_elim_left : Pi (p : Bool) (q : Bool) (H : (fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q), p := fun (p : Bool) (q : Bool) (H : (fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q), (H p (fun (H1 : p) (H2 : q), H1)) in (let and_elim_right : Pi (p : Bool) (q : Bool) (H : (fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q), q := fun (p : Bool) (q : Bool) (H : (fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q), (H q (fun (H1 : p) (H2 : q), H2)) in and_intro))) (fun (p : Bool) (q : Bool) (H1 : p) (H2 : q) (c : Bool) (H : p -> q -> c), (H H1 H2)) + (λ (and_intro : ∀ (p q : Bool), p → q → (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) q p), + [let + ((λ + (and_elim_left : ∀ (p q : Bool), (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q → p), + [let + ((λ + (and_elim_right : + ∀ (p q : Bool), + (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q → q), + and_intro) + (λ (p q : Bool) (H : (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q), + H q (λ (H1 : p) (H2 : q), H2)))]) + (λ (p q : Bool) (H : (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q), + H p (λ (H1 : p) (H2 : q), H1)))]) + (λ (p q : Bool) (H1 : p) (H2 : q) (c : Bool) (H : p → q → c), H H1 H2) expected type: - Pi (p : Bool) (q : Bool) (H1 : p) (H2 : q), ((fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) q p) + ∀ (p q : Bool), + p → q → (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) q p given type: - Pi (p : Bool) (q : Bool) (H1 : p) (H2 : q) (c : Bool) (H : p -> q -> c), c + ∀ (p q : Bool), + p → q → (∀ (c : Bool), (p → q → c) → c) diff --git a/tests/lean/t11.lean.expected.out b/tests/lean/t11.lean.expected.out index 61324a16d..18d187d6d 100644 --- a/tests/lean/t11.lean.expected.out +++ b/tests/lean/t11.lean.expected.out @@ -1,3 +1,3 @@ -Exists (fun (x : A), (p x)) : bool -Exists (fun (x : A), (Exists (fun (y : A), (q x y)))) : bool -fun (x : A), x : A -> A +Exists (λ (x : A), p x) : bool +Exists (λ (x : A), Exists (λ (y : A), q x y)) : bool +λ (x : A), x : A → A diff --git a/tests/lean/t12.lean.expected.out b/tests/lean/t12.lean.expected.out index 38caafa9c..0d908e700 100644 --- a/tests/lean/t12.lean.expected.out +++ b/tests/lean/t12.lean.expected.out @@ -1,2 +1,2 @@ -fun (f : N -> N -> N) (g : N -> N -> N) (x : N) (y : N), (f x (g x y)) : (N -> N -> N) -> (N -> N -> N) -> N -> N -> N +λ (f g : N → N → N) (x y : N), f x (g x y) : (N → N → N) → (N → N → N) → N → N → N t12.lean:7:7: error: invalid expression diff --git a/tests/lean/t13.lean.expected.out b/tests/lean/t13.lean.expected.out index 8de24fc76..e49c755af 100644 --- a/tests/lean/t13.lean.expected.out +++ b/tests/lean/t13.lean.expected.out @@ -1,2 +1,2 @@ -choice (g a b) (f a b) -fun (h : A -> A -> A), (h a b) : (A -> A -> A) -> A +[choice (g a b) (f a b)] +λ (h : A → A → A), h a b : (A → A → A) → A diff --git a/tests/lean/t14.lean.expected.out b/tests/lean/t14.lean.expected.out index ad15c6eb8..ed4d9b374 100644 --- a/tests/lean/t14.lean.expected.out +++ b/tests/lean/t14.lean.expected.out @@ -1,15 +1,15 @@ -foo.a : foo.A -foo.x : foo.A +b : A +y : A t14.lean:13:8: error: unknown identifier 'c' -foo.a : foo.A -foo.x : foo.A +a : foo.A +x : foo.A t14.lean:20:8: error: unknown identifier 'c' t14.lean:24:27: error: invalid 'using' command option, mixing explicit and implicit 'using' options -foo.a : foo.A -foo.c : foo.A -foo.A : Type -foo.f foo.a foo.c : foo.A +a : A +c : A +A : Type +f a c : A foo.f foo.a foo.c : foo.A t14.lean:47:8: error: unknown identifier 'a' -foo.f foo.a foo.c : foo.A +f a c : A t14.lean:53:9: error: unexpected token diff --git a/tests/lean/t3.lean.expected.out b/tests/lean/t3.lean.expected.out index 97aea5de3..5f450be55 100644 --- a/tests/lean/t3.lean.expected.out +++ b/tests/lean/t3.lean.expected.out @@ -1,17 +1,17 @@ -Type.{u} -Type.{tst.v} -Type.{tst.v} -Type.{tst.v} +Type +Type +Type +Type t3.lean:9:16: error: unknown universe 'v' -Type.{z} +Type t3.lean:14:16: error: unknown universe 'z' t3.lean:16:2: error: invalid namespace declaration, a namespace cannot be declared inside a section -Type.{tst.v} -Type.{u} -Type.{tst.foo.U} +Type +Type +Type t3.lean:26:10: error: invalid namespace declaration, atomic identifier expected t3.lean:27:1: error: invalid declaration name 'full.name.U', identifier must be atomic -Type.{tst.v} -Type.{tst.foo.U} +Type +Type t3.lean:35:2: error: universe level alias 'u' shadows existing global universe level t3.lean:37:16: error: unknown universe 'bla.u' diff --git a/tests/lean/t4.lean.expected.out b/tests/lean/t4.lean.expected.out index 6d7530aae..3fe0caa25 100644 --- a/tests/lean/t4.lean.expected.out +++ b/tests/lean/t4.lean.expected.out @@ -1,23 +1,23 @@ N : Type a : N -Bool -> Bool : Type -F.{2} : Type.{2} -> Type.{2} -F.{u} : Type.{u} -> Type.{u} -f : N -> N -> N -len.{1} : Pi (A : Type) (n : N) (v : vec.{1} A n), N -fun (B : Bool), (B -> B) : Bool -> Bool -fun (A : Type.{l_1}), (A -> A) : Type.{l_1} -> Type.{l_1} -fun {C : Type.{l_2}}, C : Type.{l_2} -> Type.{l_2} +Bool → Bool : Type +F : Type → Type +F : Type → Type +f : N → N → N +len : Π (A : Type) (n : N), vec A n → N +λ (B : Bool), B → B : Bool → Bool +λ (A : Type), A → A : Type → Type +λ (C : Type), C : Type → Type t4.lean:25:6: error: unknown identifier 'A' -R.{1 0} : Type -> Bool -fun (x : N) (y : N), x : N -> N -> N -choice N tst.N -tst.N +R : Type → Bool +λ (x y : N), x : N → N → N +[choice N N] N -foo.M -tst.M : Type.{2} -foo.M : Type.{3} -foo.M : Type.{3} +N +M +tst.M : Type +foo.M : Type +M : Type t4.lean:48:6: error: unknown identifier 'M' ok Declarations: diff --git a/tests/lean/t5.lean.expected.out b/tests/lean/t5.lean.expected.out index 41a6910fd..479afd373 100644 --- a/tests/lean/t5.lean.expected.out +++ b/tests/lean/t5.lean.expected.out @@ -1,5 +1,5 @@ -g : N -> N -foo.h : N -private.3156207665.q : N +g : N → N +h : N +q : N foo.h : N t5.lean:13:6: error: unknown identifier 'q' diff --git a/tests/lean/t6.lean.expected.out b/tests/lean/t6.lean.expected.out index aa99a3557..335ec2e2c 100644 --- a/tests/lean/t6.lean.expected.out +++ b/tests/lean/t6.lean.expected.out @@ -1,3 +1,3 @@ -id.{2} ?M.1 : ?M.1 -> ?M.1 -refl.{1} ?M.1 : (?M.1 -> ?M.1 -> Bool) -> Bool -symm.{1} ?M.1 : (?M.1 -> ?M.1 -> Bool) -> Bool +id : ?M_1 → ?M_1 +refl : (?M_1 → ?M_1 → Bool) → Bool +symm : (?M_1 → ?M_1 → Bool) → Bool diff --git a/tests/lean/t7.lean.expected.out b/tests/lean/t7.lean.expected.out index 17c5581e4..8a0bf77d7 100644 --- a/tests/lean/t7.lean.expected.out +++ b/tests/lean/t7.lean.expected.out @@ -1,5 +1,6 @@ -id.{2} ?M.1 : ?M.1 -> ?M.1 -trans.{1} ?M.1 : (?M.1 -> ?M.1 -> Bool) -> Bool -symm.{1} ?M.1 : (?M.1 -> ?M.1 -> Bool) -> Bool -equivalence.{1} ?M.1 : (?M.1 -> ?M.1 -> Bool) -> Bool -fun {A : Type.{l_1}} (R : A -> A -> Bool), (and (and (private.3808308840.refl.{l_1} A R) (symm.{l_1} A R)) (trans.{l_1} A R)) +id : ?M_1 → ?M_1 +trans : (?M_1 → ?M_1 → Bool) → Bool +symm : (?M_1 → ?M_1 → Bool) → Bool +equivalence : (?M_1 → ?M_1 → Bool) → Bool +λ (A : Type) (R : A → A → Bool), + and (and (refl R) (symm R)) (trans R)