max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(frontends/lean/elaborator): chaining for anonymous constructors

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-04 15:08:25 -07:00
parent 8b05fba6ef
commit befe2d96e1
4 changed files with 30 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#pragma once
#include "frontends/lean/parse_table.h"
namespace lean {
expr mk_anonymous_constructor(expr const & e);
bool is_anonymous_constructor(expr const & e);
expr const & get_anonymous_constructor_arg(expr const & e);
parse_table get_builtin_nud_table();

16
src/frontends/lean/elaborator.cpp
View file

@ -1133,7 +1133,7 @@ expr elaborator::visit_by(expr const & e, optional<expr> const & expected_type)
expr elaborator::visit_anonymous_constructor(expr const & e, optional<expr> const & expected_type) {
lean_assert(is_anonymous_constructor(e));
buffer<expr> args;
get_app_args(get_anonymous_constructor_arg(e), args);
expr const & c = get_app_args(get_anonymous_constructor_arg(e), args);
if (!expected_type)
throw elaborator_exception(e, "invalid constructor ⟨...⟩, expected type must be known");
expr I = get_app_fn(m_ctx.relaxed_whnf(instantiate_mvars(*expected_type)));
@ -1147,6 +1147,20 @@ expr elaborator::visit_anonymous_constructor(expr const & e, optional<expr> cons
get_intro_rule_names(m_env, I_name, c_names);
if (c_names.size() != 1)
throw elaborator_exception(e, sstream() << "invalid constructor ⟨...⟩, '" << I_name << "' must have only one constructor");
expr type = m_env.get(c_names[0]).get_type();
unsigned num_explicit = 0;
while (is_pi(type)) {
if (is_explicit(binding_info(type)))
num_explicit++;
type = binding_body(type);
}
if (num_explicit > 1 && args.size() > num_explicit) {
unsigned num_extra = args.size() - num_explicit;
expr rest = copy_tag(e, mk_app(c, num_extra + 1, args.data() + num_explicit - 1));
rest = copy_tag(e, mk_anonymous_constructor(rest));
args.shrink(num_explicit);
args.back() = rest;
}
expr new_e = copy_tag(e, mk_app(mk_constant(c_names[0]), args));
return visit(new_e, expected_type);
}

10
tests/lean/anc1.lean
View file

@ -22,6 +22,11 @@ check λ (A B C : Prop),
show B ∧ A ∧ C ∧ A, from
⟨Hb, ⟨Ha, ⟨Hc, Ha⟩⟩⟩
check λ (A B C : Prop),
assume (Ha : A) (Hb : B) (Hc : C),
show B ∧ A ∧ C ∧ A, from
⟨Hb, Ha, Hc, Ha⟩
check λ (A B C : Prop),
assume (Ha : A) (Hb : B) (Hc : C),
show ((B ∧ true) ∧ A) ∧ (C ∧ A), from
@ -36,3 +41,8 @@ check λ (A : Type) (P : A → Prop) (Q : A → Prop),
take (a : A) (b : A), assume (H1 : P a) (H2 : Q b),
show ∃ x y, P x ∧ Q y, from
⟨a, ⟨b, ⟨H1, H2⟩⟩⟩
check λ (A : Type) (P : A → Prop) (Q : A → Prop),
take (a : A) (b : A), assume (H1 : P a) (H2 : Q b),
show ∃ x y, P x ∧ Q y, from
⟨a, b, H1, H2⟩

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

@ -4,6 +4,8 @@ sigma.mk 1 sorry : Σ x, x > 0
show true, from true.intro : true
Exists.intro 1 (λ a, nat.no_confusion a) : ∃ x, 1 ≠ 0
λ A B C Ha Hb Hc, show B ∧ A, from and.intro Hb Ha : ∀ A B C, A → B → C → B ∧ A
λ A B C Ha Hb Hc, show B ∧ A ∧ C ∧ A, from and.intro Hb (and.intro Ha (and.intro Hc Ha)) :
∀ A B C, A → B → C → B ∧ A ∧ C ∧ A
λ A B C Ha Hb Hc, show B ∧ A ∧ C ∧ A, from and.intro Hb (and.intro Ha (and.intro Hc Ha)) :
∀ A B C, A → B → C → B ∧ A ∧ C ∧ A
λ A B C Ha Hb Hc,
@ -13,3 +15,5 @@ Exists.intro 1 (λ a, nat.no_confusion a) : ∃ x, 1 ≠ 0
∀ A P Q a, P a → Q a → (∃ x, P x ∧ Q x)
λ A P Q a b H1 H2, show ∃ x y, P x ∧ Q y, from Exists.intro a (Exists.intro b (and.intro H1 H2)) :
∀ A P Q a b, P a → Q b → (∃ x y, P x ∧ Q y)
λ A P Q a b H1 H2, show ∃ x y, P x ∧ Q y, from Exists.intro a (Exists.intro b (and.intro H1 H2)) :
∀ A P Q a b, P a → Q b → (∃ x y, P x ∧ Q y)