From 5c991f8fbfbdf8a3b451d44be361571db74b6359 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 3 Feb 2014 20:10:26 -0800 Subject: [PATCH] feat(frontends/lean): parse and pretty print tuples/pairs This commit also fixes a bug in the type checker when processing dependent pairs. Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser_expr.cpp | 31 ++++++++++++++++++++++++++++++ src/frontends/lean/parser_imp.h | 1 + src/frontends/lean/pp.cpp | 25 ++++++++++++++++++++++++ src/kernel/kernel_exception.cpp | 2 +- src/kernel/type_checker.cpp | 7 ++++--- tests/lean/sig2.lean | 12 ++++++++++++ tests/lean/sig2.lean.expected.out | 24 +++++++++++++++++++++++ 7 files changed, 98 insertions(+), 4 deletions(-) create mode 100644 tests/lean/sig2.lean create mode 100644 tests/lean/sig2.lean.expected.out diff --git a/src/frontends/lean/parser_expr.cpp b/src/frontends/lean/parser_expr.cpp index b4179d9b6f..e55fa17ec6 100644 --- a/src/frontends/lean/parser_expr.cpp +++ b/src/frontends/lean/parser_expr.cpp @@ -853,6 +853,36 @@ expr parser_imp::parse_type(bool level_expected) { } } +expr parser_imp::parse_tuple() { + auto p = pos(); + next(); + buffer args; + args.push_back(parse_expr()); + while (curr_is_comma()) { + next(); + args.push_back(parse_expr()); + } + unsigned num = args.size(); + if (num < 3) + throw parser_error("invalid tuple/pair, it must have at least three arguments", p); + expr t = args[num-1]; + if (num == 3) { + return save(mk_pair(args[num-3], args[num-2], t), p); + } else { + expr r = save(mk_pair(args[num-3], args[num-2], save(mk_placeholder(), p)), p); + unsigned i = num-3; + while (true) { + lean_assert(i > 0); + --i; + if (i == 0) { + return save(mk_pair(args[0], r, t), p); + } else { + r = save(mk_pair(args[i], r, save(mk_placeholder(), p)), p); + } + } + } +} + /** \brief Parse \c _ a hole that must be filled by the elaborator. */ expr parser_imp::parse_placeholder() { auto p = pos(); @@ -965,6 +995,7 @@ expr parser_imp::parse_nud() { case scanner::token::Placeholder: return parse_placeholder(); case scanner::token::Type: return parse_type(false); case scanner::token::Have: return parse_have_expr(); + case scanner::token::Tuple: return parse_tuple(); case scanner::token::By: return parse_by_expr(); default: throw parser_error("invalid expression, unexpected token", pos()); diff --git a/src/frontends/lean/parser_imp.h b/src/frontends/lean/parser_imp.h index 1f269334c4..2c003d1afc 100644 --- a/src/frontends/lean/parser_imp.h +++ b/src/frontends/lean/parser_imp.h @@ -305,6 +305,7 @@ private: expr parse_exists(); expr parse_let(); expr parse_type(bool level_expected); + expr parse_tuple(); tactic parse_tactic_macro(name tac_id, pos_info const & p); expr parse_have_expr(); expr parse_calc(); diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index c21c926d99..86cb1800ff 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -76,6 +76,7 @@ static format g_ellipsis_n_fmt= highlight(format("\u2026")); static format g_ellipsis_fmt = highlight(format("...")); static format g_let_fmt = highlight_keyword(format("let")); static format g_in_fmt = highlight_keyword(format("in")); +static format g_tuple_fmt = highlight_keyword(format("tuple")); static format g_assign_fmt = highlight_keyword(format(":=")); static format g_geq_fmt = format("\u2265"); static format g_lift_fmt = highlight_keyword(format("lift")); @@ -267,6 +268,7 @@ class pp_fn { else return false; case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let: + case expr_kind::Sigma: case expr_kind::Pair: case expr_kind::Proj: return false; } return false; @@ -1112,6 +1114,28 @@ class pp_fn { } } + result pp_tuple(expr a, unsigned depth) { + buffer args; + args.push_back(pair_first(a)); + while (is_pair(pair_second(a))) { + a = pair_second(a); + args.push_back(pair_first(a)); + } + args.push_back(pair_second(a)); + args.push_back(pair_type(a)); + unsigned indent = 6; + format r_format = g_tuple_fmt; + unsigned r_weight = 1; + for (unsigned i = 0; i < args.size(); i++) { + auto arg_r = pp_child(args[i], depth); + if (i > 0) + r_format += comma(); + r_format += nest(indent, compose(line(), arg_r.first)); + r_weight += arg_r.second; + } + return result(group(r_format), r_weight); + } + result pp(expr const & e, unsigned depth, bool main = false) { check_system("pretty printer"); if (!is_atomic(e) && (m_num_steps > m_max_steps || depth > m_max_depth)) { @@ -1148,6 +1172,7 @@ class pp_fn { case expr_kind::Type: r = pp_type(e); break; case expr_kind::Let: r = pp_let(e, depth); break; case expr_kind::MetaVar: r = pp_metavar(e, depth); break; + case expr_kind::Pair: r = pp_tuple(e, depth); break; } } if (!main && m_extra_lets && has_several_occs(e) && r.second > m_alias_min_weight) { diff --git a/src/kernel/kernel_exception.cpp b/src/kernel/kernel_exception.cpp index 85d4d326c8..3a31ac54c4 100644 --- a/src/kernel/kernel_exception.cpp +++ b/src/kernel/kernel_exception.cpp @@ -71,7 +71,7 @@ format pair_type_mismatch_exception::pp(formatter const & fmt, options const & o r += compose(line(), format("Pair type:")); r += nest(indent, compose(line(), fmt(ctx, m_sig_type, false, opts))); r += line(); - r += format("Arguments type:"); + r += format("Argument type:"); r += nest(indent, compose(line(), fmt(ctx, m_arg_type, false, opts))); return r; } diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 380a4fe2c7..6315d21bac 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -273,16 +273,17 @@ class type_checker::imp { return pair_type(e); } else { expr const & t = pair_type(e); - expr sig = check_sigma(infer_type_core(t, ctx), e, ctx); + expr sig = check_sigma(t, t, ctx); expr f_t = infer_type_core(pair_first(e), ctx); expr s_t = infer_type_core(pair_second(e), ctx); auto mk_fst_justification = [&]() { return mk_pair_type_match_justification(ctx, e, true); }; if (!is_convertible(f_t, abst_domain(sig), ctx, mk_fst_justification)) throw pair_type_mismatch_exception(env(), ctx, e, true, f_t, sig); auto mk_snd_justification = [&]() { return mk_pair_type_match_justification(ctx, e, false); }; - expr expected = instantiate(abst_body(sig), f_t); - if (!is_convertible(s_t, expected, ctx, mk_snd_justification)) + expr expected = instantiate(abst_body(sig), pair_first(e)); + if (!is_convertible(s_t, expected, ctx, mk_snd_justification)) { throw pair_type_mismatch_exception(env(), ctx, e, false, s_t, sig); + } return sig; } case expr_kind::Proj: { diff --git a/tests/lean/sig2.lean b/tests/lean/sig2.lean new file mode 100644 index 0000000000..74c9f6ad47 --- /dev/null +++ b/tests/lean/sig2.lean @@ -0,0 +1,12 @@ +check sig x : Nat, x > 0 +check tuple 10, 20, (Nat # Nat) +check tuple 10, true, (Nat # Nat) +check tuple true, 20, (Nat # Nat) +check tuple true, 20, (Bool # Nat) +check tuple true, true, (Bool # Bool) +check tuple true, true, (Bool ⨯ Bool) +variable a : Nat +axiom Ha : 1 ≤ a +definition NZ : Type := sig x : Nat, 1 ≤ x +check NZ +check tuple a, Ha, NZ diff --git a/tests/lean/sig2.lean.expected.out b/tests/lean/sig2.lean.expected.out new file mode 100644 index 0000000000..f0c559fae7 --- /dev/null +++ b/tests/lean/sig2.lean.expected.out @@ -0,0 +1,24 @@ + Set: pp::colors + Set: pp::unicode +sig x : ℕ, x > 0 : Type +tuple 10, 20, (ℕ ⨯ ℕ) : ℕ ⨯ ℕ +sig2.lean:3:6: error: type mismatch in the 2nd argument of the pair + tuple 10, ⊤, (ℕ ⨯ ℕ) +Pair type: + ℕ ⨯ ℕ +Argument type: + Bool +sig2.lean:4:6: error: type mismatch in the 1st argument of the pair + tuple ⊤, 20, (ℕ ⨯ ℕ) +Pair type: + ℕ ⨯ ℕ +Argument type: + Bool +tuple ⊤, 20, (Bool ⨯ ℕ) : Bool ⨯ ℕ +tuple ⊤, ⊤, (Bool ⨯ Bool) : Bool ⨯ Bool +tuple ⊤, ⊤, (Bool ⨯ Bool) : Bool ⨯ Bool + Assumed: a + Assumed: Ha + Defined: NZ +NZ : Type +tuple a, Ha, NZ : sig x : ℕ, 1 ≤ x