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

feat(frontends/lean/builtin_cmds): use type_context to implement #reduce command

Browse source
This commit is contained in:
Leonardo de Moura 2018-01-09 16:40:41 -08:00
parent 0c5c1a27c6
commit 60be2bf2aa
5 changed files with 18 additions and 65 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -222,13 +222,12 @@ environment reduce_cmd(parser & p) {
expr e; level_param_names ls;
std::tie(e, ls) = parse_local_expr(p, "_reduce");
expr r;
type_context ctx(p.env(), p.get_options(), metavar_context(), local_context(), transparency_mode::All);
if (whnf) {
type_checker tc(p.env(), true, false);
r = tc.whnf(e);
r = ctx.whnf(e);
} else {
type_checker tc(p.env(), true, false);
bool eta = false;
r = normalize(tc, e, eta);
r = normalize(ctx, e, eta);
}
auto out = p.mk_message(p.cmd_pos(), p.pos(), INFORMATION);
out.set_caption("reduce result") << r;

1
src/library/normalize.cpp
View file

@ -112,7 +112,6 @@ class normalize_fn {
}
expr normalize(expr e) {
// TODO(Leo): smart_reduction doesn't seem to work with normalize
check_system("normalize");
if (!m_pred(e))
return e;

5
tests/lean/smart_unfolding.lean Normal file
View file

@ -0,0 +1,5 @@
constant n : nat
#reduce n + (nat.succ n)
set_option type_context.smart_unfolding false
#reduce n + (nat.succ n)

8
tests/lean/smart_unfolding.lean.expected.out Normal file
View file

@ -0,0 +1,8 @@
nat.succ (nat.add n n)
nat.succ
((nat.rec ⟨λ (a : ℕ), a, punit.star⟩
(λ (n : ℕ)
(ih : pprod (ℕ → ℕ) (nat.rec punit (λ (n : ℕ) (ih : Type), pprod (pprod (ℕ → ℕ) ih) punit) n)),
⟨λ (a : ℕ), nat.succ (ih.fst a), ⟨ih, punit.star⟩⟩)
n).fst
n)

62
tests/lean/whnf.lean.expected.out
View file

@ -1,62 +1,4 @@
succ
((⟨nat.rec
⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ),
(λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1),
nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), id_rhs ℕ a)
(λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (succ a_1)),
id_rhs ℕ (succ ((_F.fst).fst a)))
_F)
a_1
a
_F)
0
punit.star,
punit.star⟩
(λ (n : ℕ) (ih : pprod ((λ (a : ℕ), ℕ → ℕ) n) (nat.below (λ (a : ℕ), ℕ → ℕ) n)),
⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ),
(λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1),
nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), id_rhs ℕ a)
(λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (succ a_1)),
id_rhs ℕ (succ ((_F.fst).fst a)))
_F)
a_1
a
_F)
(succ n)
⟨ih, punit.star⟩,
⟨ih, punit.star⟩⟩)
0,
punit.star⟩.fst).fst
2)
succ (nat.add 2 0)
3
succ
((⟨nat.rec
⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ),
(λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1),
nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), id_rhs ℕ a)
(λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (succ a_1)),
id_rhs ℕ (succ ((_F.fst).fst a)))
_F)
a_1
a
_F)
0
punit.star,
punit.star⟩
(λ (n : ℕ) (ih : pprod ((λ (a : ℕ), ℕ → ℕ) n) (nat.below (λ (a : ℕ), ℕ → ℕ) n)),
⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ),
(λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1),
nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), id_rhs ℕ a)
(λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (succ a_1)),
id_rhs ℕ (succ ((_F.fst).fst a)))
_F)
a_1
a
_F)
(succ n)
⟨ih, punit.star⟩,
⟨ih, punit.star⟩⟩)
0,
punit.star⟩.fst).fst
a)
succ (nat.add a 0)
succ a