michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/pp): take notation declarations into account when pretty printing

Browse source 
TODO: support foldl/foldr and binders
This commit is contained in:
Leonardo de Moura 2014-10-19 08:40:56 -07:00
parent 8cfb3ae687
commit 555d26aa61
24 changed files with 370 additions and 120 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/frontends/lean/builtin_cmds.cpp
View file

@ -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;

281
src/frontends/lean/pp.cpp
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <algorithm>
#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<name> const & names, expr const & type, binder_info const & bi) {
@ -378,7 +380,7 @@ format pretty_fn::pp_binder_block(buffer<name> 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<expr> 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<optional<expr>> & 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<expr> 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<optional<expr>> & args) -> optional<result> {
std::reverse(args.begin(), args.end());
if (entry.is_numeral()) {
return some(result(format(entry.get_num())));
} else {
using notation::transition;
buffer<transition> 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<result>();
} 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<result>();
case notation::action_kind::Ext:
case notation::action_kind::LuaExt:
return optional<result>();
}
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<result>();
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>(result(first_lbp, last_rbp, fmt));
}
}
auto pretty_fn::pp_notation(expr const & e) -> optional<result> {
if (!m_notation || is_var(e))
return optional<result>();
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<optional<expr>> args;
if (match(entry.get_expr(), e, args)) {
if (auto r = pp_notation(entry, args))
return r;
}
}
return optional<result>();
}
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<unsigned> 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() {

72
src/frontends/lean/pp.h
View file

@ -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<format, unsigned> result;
static unsigned max_bp() { return std::numeric_limits<unsigned>::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<name> m_purify_meta_table;
name_map<name> 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<name> m_purify_meta_table;
name_map<name> 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<unsigned>::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<expr> 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<optional<expr>> & args);
result pp_notation_child(expr const & e, unsigned lbp, unsigned rbp);
optional<result> pp_notation(notation_entry const & entry, buffer<optional<expr>> & args);
optional<result> 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);

1
src/frontends/lean/pp_options.cpp
View file

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

1
src/frontends/lean/pp_options.h
View file

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

6
tests/lean/bug1.lean.expected.out
View file

@ -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

4
tests/lean/calc1.lean.expected.out
View file

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

4
tests/lean/crash.lean.expected.out
View file

@ -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

17
tests/lean/have1.lean.expected.out
View file

@ -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

2
tests/lean/interactive/coe.input.expected.out
View file

@ -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

8
tests/lean/interactive/findp.input.expected.out
View file

@ -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

4
tests/lean/interactive/in4.input.expected.out
View file

@ -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

2
tests/lean/interactive/in5.input.expected.out
View file

@ -2,7 +2,7 @@
-- ENDWAIT
-- BEGININFO
-- TYPE|4|0
A → B → and A B
A → B → A ∧ B
-- ACK
-- IDENTIFIER|4|0
and.intro

4
tests/lean/interactive/t4.input.expected.out
View file

@ -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

18
tests/lean/notation.lean Normal file
View file

@ -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 ℕ → ℕ

11
tests/lean/notation.lean.expected.out Normal file
View file

@ -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₁

14
tests/lean/show1.lean.expected.out
View file

@ -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

6
tests/lean/t10.lean.expected.out
View file

@ -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

4
tests/lean/t14.lean.expected.out
View file

@ -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

4
tests/lean/t9.lean.expected.out
View file

@ -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

2
tests/lean/tuple.lean.expected.out
View file

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

2
tests/lean/uni_bug1.lean.expected.out
View file

@ -1 +1 @@
f 1 0 (Rtrue (pr1 (pair 1 0)) 0) : nat
f 1 0 (Rtrue (pr₁ (pair 1 0)) 0) : ℕ

16
tests/lean/univ.lean.expected.out
View file

@ -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₂

2
tests/lean/var2.lean.expected.out
View file

@ -1 +1 @@
foo : Π (B : Type), B → (Π (A : Type), A → eq A B → Prop)
foo : Π (B : Type), B → (Π (A : Type), A → A = B → Prop)