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 <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
5e5ab1429d
commit
5c991f8fbf
7 changed files with 98 additions and 4 deletions
|
|
@ -853,6 +853,36 @@ expr parser_imp::parse_type(bool level_expected) {
|
|||
}
|
||||
}
|
||||
|
||||
expr parser_imp::parse_tuple() {
|
||||
auto p = pos();
|
||||
next();
|
||||
buffer<expr> 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());
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
|
|
|||
|
|
@ -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<expr> 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) {
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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: {
|
||||
|
|
|
|||
12
tests/lean/sig2.lean
Normal file
12
tests/lean/sig2.lean
Normal file
|
|
@ -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
|
||||
24
tests/lean/sig2.lean.expected.out
Normal file
24
tests/lean/sig2.lean.expected.out
Normal file
|
|
@ -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
|
||||
Loading…
Reference in a new issue