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

fix(frontends/lean): fix 'let' annotation placement and pretty printer

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-26 21:00:22 -07:00
parent 206206060f
commit cf35c07786
3 changed files with 30 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/builtin_exprs.cpp
View file

@ -55,8 +55,8 @@ static expr parse_let_body(parser & p, pos_info const & pos) {
}
static expr mk_let(parser & p, name const & id, expr const & t, expr const & v, expr const & b, pos_info const & pos, binder_info const & bi) {
expr l = p.save_pos(mk_lambda(id, t, b, bi), pos);
return p.save_pos(mk_let_annotation(p.save_pos(mk_app(l, v), pos)), pos);
expr l = p.save_pos(mk_let_annotation(p.save_pos(mk_lambda(id, t, b, bi), pos)), pos);
return p.mk_app(l, v, pos);
}
static void parse_let_modifiers(parser & p, bool & is_fact, bool & is_opaque) {

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

@ -298,16 +298,17 @@ auto pretty_fn::pp_pi(expr const & e) -> result {
}
}
static bool is_let(expr const & e) {
return is_app(e) && is_let_annotation(app_fn(e));
}
auto pretty_fn::pp_let(expr e) -> result {
buffer<expr_pair> decls;
while (true) {
if (!is_let_annotation(e))
break;
e = get_annotation_arg(e);
if (!is_app(e) || !is_lambda(app_fn(e)))
if (!is_let(e))
break;
expr v = app_arg(e);
auto p = binding_body_fresh(app_fn(e), true);
auto p = binding_body_fresh(get_annotation_arg(app_fn(e)), true);
decls.emplace_back(p.second, v);
e = p.first;
}
@ -332,17 +333,13 @@ auto pretty_fn::pp_let(expr e) -> result {
}
auto pretty_fn::pp_macro(expr const & e) -> result {
if (is_let_annotation(e)) {
return pp_let(e);
} else {
// TODO(Leo): 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));
}
// TODO(Leo): 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 {
@ -353,6 +350,8 @@ auto pretty_fn::pp(expr const & e) -> result {
if (is_placeholder(e))
return mk_result(g_placeholder_fmt);
if (is_let(e))
return pp_let(e);
switch (e.kind()) {
case expr_kind::Var: return pp_var(e);

24
tests/lean/let1.lean.expected.out
View file

@ -14,17 +14,19 @@ in and_intro :
∀ (p q : Prop),
p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q
let1.lean:16:10: error: type mismatch at application
(λ (and_intro : ∀ (p q : Prop), p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) q p),
let and_elim_left : ∀ (p q : Prop),
(λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → p :=
λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q),
H p (λ (H1 : p) (H2 : q), H1),
and_elim_right : ∀ (p q : Prop),
(λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → q :=
λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q),
H q (λ (H1 : p) (H2 : q), H2)
in and_intro)
(λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c), H H1 H2)
let and_intro : ∀ (p q : Prop),
p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) q p :=
λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c),
H H1 H2,
and_elim_left : ∀ (p q : Prop),
(λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → p :=
λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q),
H p (λ (H1 : p) (H2 : q), H1),
and_elim_right : ∀ (p q : Prop),
(λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → q :=
λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q),
H q (λ (H1 : p) (H2 : q), H2)
in and_intro
expected type:
∀ (p q : Prop),
p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) q p