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

fix(library/compiler/nat_value): add expand method, otherwise we may fail to type check terms using nat_value_macro

Browse source
This commit is contained in:
Leonardo de Moura 2016-05-13 12:50:28 -07:00
parent f75caddc35
commit 752c81a166
2 changed files with 24 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/library/compiler/nat_value.cpp
View file

@ -26,9 +26,29 @@ public:
virtual expr check_type(expr const &, abstract_type_context &, bool) const {
return *g_nat;
}
virtual optional<expr> expand(expr const &, abstract_type_context &) const {
return none_expr();
static expr convert(mpz const & n, expr const & one, expr const & add) {
if (n == 0) {
return mk_constant(get_nat_zero_name());
} else if (n == 1) {
return one;
} else {
expr r = convert(n/2, one, add);
r = mk_app(add, r, r);
if (n % mpz(2) == 1)
return mk_app(add, r, one);
else
return r;
}
}
virtual optional<expr> expand(expr const &, abstract_type_context &) const {
expr one = mk_app(mk_constant(get_nat_succ_name()), mk_constant(get_nat_zero_name()));
expr add = mk_constant(get_nat_add_name());
expr r = convert(m_value, one, add);
return optional<expr>(r);
}
virtual unsigned trust_level() const { return 0; }
virtual bool operator==(macro_definition_cell const & other) const {
nat_value_macro const * other_ptr = dynamic_cast<nat_value_macro const *>(&other);

4
src/library/compiler/preprocess.cpp
View file

@ -121,10 +121,10 @@ public:
v = expand_aux_recursors(m_env, v);
lean_assert(check(d, v));
lean_trace(name({"compiler", "expand_aux_recursors"}), tout() << "\n" << v << "\n";)
v = find_nat_values(m_env, v);
lean_assert(check(d, v));
v = mark_comp_irrelevant_subterms(m_env, v);
lean_assert(check(d, v));
v = find_nat_values(m_env, v);
lean_assert(check(d, v));
v = eta_expand(m_env, v);
lean_assert(check(d, v));
lean_trace(name({"compiler", "eta_expansion"}), tout() << "\n" << v << "\n";)