feat(frontends/lean): add basic pretty printer

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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})

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();
 }
 

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<name> 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<expr> const & locals) {
+    unsigned num     = locals.size();
+    buffer<name> 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<expr> 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<expr> 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<unsigned> 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());
+}
+}

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 <utility>
+#include <limits>
+#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<format, unsigned> 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<name>     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<unsigned>::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<name> const & names, expr const & type, binder_info const & bi);
+    format pp_binders(buffer<expr> 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();
+}

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); }
+bool     get_pp_universes(options const & opts)  { return opts.get_bool(g_pp_universes, LEAN_DEFAULT_PP_UNIVERSES); }
 }

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);
 }

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<name> is_aliased(environment const & env, expr const & t);
 

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();

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

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

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)]

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

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)

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

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

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

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

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'

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:

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'

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

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)