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

Rename abst_type to abst_domain

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-03 11:31:42 -07:00
parent e1e3e6b2d6
commit 2972bdfec3
8 changed files with 35 additions and 35 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/kernel/deep_copy.cpp
View file

@ -32,8 +32,8 @@ class deep_copy_fn {
r = app(new_args.size(), new_args.data());
break;
}
case expr_kind::Lambda: r = lambda(abst_name(a), apply(abst_type(a)), apply(abst_body(a))); break;
case expr_kind::Pi: r = pi(abst_name(a), apply(abst_type(a)), apply(abst_body(a))); break;
case expr_kind::Lambda: r = lambda(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))); break;
case expr_kind::Pi: r = pi(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))); break;
}
if (sh)
m_cache.insert(std::make_pair(a.raw(), r));

22
src/kernel/expr.cpp
View file

@ -76,7 +76,7 @@ expr app(unsigned n, expr const * as) {
expr_abstraction::expr_abstraction(expr_kind k, name const & n, expr const & t, expr const & b):
expr_cell(k, ::lean::hash(t.hash(), b.hash())),
m_name(n),
m_type(t),
m_domain(t),
m_body(b) {
}
expr_lambda::expr_lambda(name const & n, expr const & t, expr const & e):
@ -134,7 +134,7 @@ class eq_fn {
case expr_kind::Pi:
// Lambda and Pi
// Remark: we ignore get_abs_name because we want alpha-equivalence
return apply(abst_type(a), abst_type(b)) && apply(abst_body(a), abst_body(b));
return apply(abst_domain(a), abst_domain(b)) && apply(abst_body(a), abst_body(b));
case expr_kind::Type: return ty_level(a) == ty_level(b);
case expr_kind::Numeral: return num_value(a) == num_value(b);
}
@ -168,14 +168,14 @@ std::ostream & operator<<(std::ostream & out, expr const & a) {
}
out << ")";
break;
case expr_kind::Lambda: out << "(fun (" << abst_name(a) << " : " << abst_type(a) << ") " << abst_body(a) << ")"; break;
case expr_kind::Lambda: out << "(fun (" << abst_name(a) << " : " << abst_domain(a) << ") " << abst_body(a) << ")"; break;
case expr_kind::Pi:
if (!is_arrow(a))
out << "(pi (" << abst_name(a) << " : " << abst_type(a) << ") " << abst_body(a) << ")";
else if (!is_arrow(abst_type(a)))
out << abst_type(a) << " -> " << abst_body(a);
out << "(pi (" << abst_name(a) << " : " << abst_domain(a) << ") " << abst_body(a) << ")";
else if (!is_arrow(abst_domain(a)))
out << abst_domain(a) << " -> " << abst_body(a);
else
out << "(" << abst_type(a) << ") -> " << abst_body(a);
out << "(" << abst_domain(a) << ") -> " << abst_body(a);
break;
case expr_kind::Type: {
level const & l = ty_level(a);
@ -197,8 +197,8 @@ expr copy(expr const & a) {
case expr_kind::Type: return type(ty_level(a));
case expr_kind::Numeral: return numeral(num_value(a));
case expr_kind::App: return app(num_args(a), begin_args(a));
case expr_kind::Lambda: return lambda(abst_name(a), abst_type(a), abst_body(a));
case expr_kind::Pi: return pi(abst_name(a), abst_type(a), abst_body(a));
case expr_kind::Lambda: return lambda(abst_name(a), abst_domain(a), abst_body(a));
case expr_kind::Pi: return pi(abst_name(a), abst_domain(a), abst_body(a));
}
lean_unreachable();
return expr();
@ -227,7 +227,7 @@ lean::format pp_aux(lean::expr const & a) {
paren(format{
format(abst_name(a)),
format(" : "),
pp_aux(abst_type(a))}),
pp_aux(abst_domain(a))}),
format(" "),
pp_aux(abst_body(a))});
case expr_kind::Pi:
@ -236,7 +236,7 @@ lean::format pp_aux(lean::expr const & a) {
paren(format{
format(abst_name(a)),
format(" : "),
pp_aux(abst_type(a))}),
pp_aux(abst_domain(a))}),
format(" "),
pp_aux(abst_body(a))});
case expr_kind::Type:

16
src/kernel/expr.h
View file

@ -71,7 +71,7 @@ private:
expr_cell * m_ptr;
explicit expr(expr_cell * ptr):m_ptr(ptr) {}
public:
expr():m_ptr(0) {}
expr():m_ptr(nullptr) {}
expr(expr const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
expr(expr && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
~expr() { if (m_ptr) m_ptr->dec_ref(); }
@ -144,13 +144,13 @@ public:
/** \brief Super class for lambda abstraction and pi (functional spaces). */
class expr_abstraction : public expr_cell {
name m_name;
expr m_type;
expr m_domain;
expr m_body;
public:
expr_abstraction(expr_kind k, name const & n, expr const & t, expr const & e);
name const & get_name() const { return m_name; }
expr const & get_type() const { return m_type; }
expr const & get_body() const { return m_body; }
name const & get_name() const { return m_name; }
expr const & get_domain() const { return m_domain; }
expr const & get_body() const { return m_body; }
};
/** \brief Lambda abstractions */
class expr_lambda : public expr_abstraction {
@ -258,7 +258,7 @@ inline unsigned const_pos(expr_cell * e) { return to_constant(e)
inline unsigned num_args(expr_cell * e) { return to_app(e)->get_num_args(); }
inline expr const & arg(expr_cell * e, unsigned idx) { return to_app(e)->get_arg(idx); }
inline name const & abst_name(expr_cell * e) { return to_abstraction(e)->get_name(); }
inline expr const & abst_type(expr_cell * e) { return to_abstraction(e)->get_type(); }
inline expr const & abst_domain(expr_cell * e) { return to_abstraction(e)->get_domain(); }
inline expr const & abst_body(expr_cell * e) { return to_abstraction(e)->get_body(); }
inline level const & ty_level(expr_cell * e) { return to_type(e)->get_level(); }
inline mpz const & num_value(expr_cell * e) { return to_numeral(e)->get_num(); }
@ -274,7 +274,7 @@ inline expr const & arg(expr const & e, unsigned idx) { return to_app(e)->ge
inline expr const * begin_args(expr const & e) { return to_app(e)->begin_args(); }
inline expr const * end_args(expr const & e) { return to_app(e)->end_args(); }
inline name const & abst_name(expr const & e) { return to_abstraction(e)->get_name(); }
inline expr const & abst_type(expr const & e) { return to_abstraction(e)->get_type(); }
inline expr const & abst_domain(expr const & e) { return to_abstraction(e)->get_domain(); }
inline expr const & abst_body(expr const & e) { return to_abstraction(e)->get_body(); }
inline level const & ty_level(expr const & e) { return to_type(e)->get_level(); }
inline mpz const & num_value(expr const & e) { return to_numeral(e)->get_num(); }
@ -357,7 +357,7 @@ template<typename F> expr update_app(expr const & e, F f) {
}
template<typename F> expr update_abst(expr const & e, F f) {
static_assert(std::is_same<typename std::result_of<F(expr const &, expr const &)>::type,
std::pair<expr, expr>>::value,
std::pair<expr, expr>>::value,
"update_abst: return type of f is not pair<expr, expr>");
expr const & old_t = abst_type(e);
expr const & old_b = abst_body(e);

2
src/kernel/free_vars.cpp
View file

@ -52,7 +52,7 @@ protected:
break;
case expr_kind::Lambda:
case expr_kind::Pi:
result = apply(abst_type(e), offset) || apply(abst_body(e), offset + 1);
result = apply(abst_domain(e), offset) || apply(abst_body(e), offset + 1);
break;
}

4
src/kernel/normalize.cpp
View file

@ -74,7 +74,7 @@ class normalize_fn {
expr reify_closure(expr const & a, stack const & c, unsigned k) {
lean_assert(is_lambda(a));
expr new_t = reify(normalize(abst_type(a), c, k), k);
expr new_t = reify(normalize(abst_domain(a), c, k), k);
expr new_b = reify(normalize(abst_body(a), extend(c, value(k)), k+1), k+1);
return lambda(abst_name(a), new_t, new_b);
#if 0
@ -156,7 +156,7 @@ class normalize_fn {
case expr_kind::Lambda:
return value(a, c);
case expr_kind::Pi: {
expr new_t = reify(normalize(abst_type(a), c, k), k);
expr new_t = reify(normalize(abst_domain(a), c, k), k);
expr new_b = reify(normalize(abst_body(a), extend(c, value(k)), k+1), k+1);
return value(pi(abst_name(a), new_t, new_b));
}}

12
src/kernel/type_check.cpp
View file

@ -90,7 +90,7 @@ class infer_type_fn {
while (true) {
expr const & c = arg(e, i);
expr c_t = infer_type(c, ctx);
check_type(e, i, abst_type(f_t), c_t, ctx);
check_type(e, i, abst_domain(f_t), c_t, ctx);
// Remark: if f_t is an arrow, we don't have to call normalize and
// lower_free_vars
f_t = normalize(abst_body(f_t), ctx, c);
@ -103,13 +103,13 @@ class infer_type_fn {
}
}
case expr_kind::Lambda: {
infer_universe(abst_type(e), ctx);
expr t = infer_type(abst_body(e), extend(ctx, abst_name(e), abst_type(e)));
return pi(abst_name(e), abst_type(e), t);
infer_universe(abst_domain(e), ctx);
expr t = infer_type(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)));
return pi(abst_name(e), abst_domain(e), t);
}
case expr_kind::Pi: {
level l1 = infer_universe(abst_type(e), ctx);
level l2 = infer_universe(abst_body(e), extend(ctx, abst_name(e), abst_type(e)));
level l1 = infer_universe(abst_domain(e), ctx);
level l2 = infer_universe(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)));
return type(max(l1, l2));
}
case expr_kind::Numeral:

8
src/tests/kernel/expr.cpp
View file

@ -75,7 +75,7 @@ unsigned depth1(expr const & e) {
return m + 1;
}
case expr_kind::Lambda: case expr_kind::Pi:
return std::max(depth1(abst_type(e)), depth1(abst_body(e))) + 1;
return std::max(depth1(abst_domain(e)), depth1(abst_body(e))) + 1;
}
return 0;
}
@ -91,7 +91,7 @@ unsigned depth2(expr const & e) {
[](unsigned m, expr const & arg){ return std::max(depth2(arg), m); })
+ 1;
case expr_kind::Lambda: case expr_kind::Pi:
return std::max(depth2(abst_type(e)), depth2(abst_body(e))) + 1;
return std::max(depth2(abst_domain(e)), depth2(abst_body(e))) + 1;
}
return 0;
}
@ -117,7 +117,7 @@ unsigned depth3(expr const & e) {
break;
}
case expr_kind::Lambda: case expr_kind::Pi:
todo.push_back(std::make_pair(&abst_type(e), c));
todo.push_back(std::make_pair(&abst_domain(e), c));
todo.push_back(std::make_pair(&abst_body(e), c));
break;
}
@ -174,7 +174,7 @@ unsigned count_core(expr const & a, expr_set & s) {
return std::accumulate(begin_args(a), end_args(a), 1,
[&](unsigned sum, expr const & arg){ return sum + count_core(arg, s); });
case expr_kind::Lambda: case expr_kind::Pi:
return count_core(abst_type(a), s) + count_core(abst_body(a), s) + 1;
return count_core(abst_domain(a), s) + count_core(abst_body(a), s) + 1;
}
return 0;
}

2
src/tests/kernel/normalize.cpp
View file

@ -63,7 +63,7 @@ unsigned count_core(expr const & a, expr_set & s) {
return std::accumulate(begin_args(a), end_args(a), 1,
[&](unsigned sum, expr const & arg){ return sum + count_core(arg, s); });
case expr_kind::Lambda: case expr_kind::Pi:
return count_core(abst_type(a), s) + count_core(abst_body(a), s) + 1;
return count_core(abst_domain(a), s) + count_core(abst_body(a), s) + 1;
}
return 0;
}