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

Rename abst_expr -> abst_body

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-07-23 21:49:19 -07:00
parent 9fd88e6e27
commit ed6d6483fe
5 changed files with 19 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/kernel/expr.cpp
View file

@ -74,11 +74,11 @@ expr app(unsigned n, expr const * as) {
return r; return r;
} }
expr_abstraction::expr_abstraction(expr_kind k, name const & n, expr const & t, expr const & e): expr_abstraction::expr_abstraction(expr_kind k, name const & n, expr const & t, expr const & b):
expr_cell(k, ::lean::hash(t.hash(), e.hash())), expr_cell(k, ::lean::hash(t.hash(), b.hash())),
m_name(n), m_name(n),
m_type(t), m_type(t),
m_expr(e) { m_body(b) {
} }
expr_lambda::expr_lambda(name const & n, expr const & t, expr const & e): expr_lambda::expr_lambda(name const & n, expr const & t, expr const & e):
expr_abstraction(expr_kind::Lambda, n, t, e) {} expr_abstraction(expr_kind::Lambda, n, t, e) {}
@ -147,7 +147,7 @@ public:
case expr_kind::Pi: case expr_kind::Pi:
// Lambda and Pi // Lambda and Pi
// Remark: we ignore get_abs_name because we want alpha-equivalence // Remark: we ignore get_abs_name because we want alpha-equivalence
return apply(abst_type(a), abst_type(b)) && apply(abst_expr(a), abst_expr(b)); return apply(abst_type(a), abst_type(b)) && apply(abst_body(a), abst_body(b));
case expr_kind::Prop: lean_unreachable(); return true; case expr_kind::Prop: lean_unreachable(); return true;
case expr_kind::Type: case expr_kind::Type:
if (ty_num_vars(a) != ty_num_vars(b)) if (ty_num_vars(a) != ty_num_vars(b))
@ -184,8 +184,8 @@ std::ostream & operator<<(std::ostream & out, expr const & a) {
} }
out << ")"; out << ")";
break; break;
case expr_kind::Lambda: out << "(fun (" << abst_name(a) << " : " << abst_type(a) << ") " << abst_expr(a) << ")"; break; case expr_kind::Lambda: out << "(fun (" << abst_name(a) << " : " << abst_type(a) << ") " << abst_body(a) << ")"; break;
case expr_kind::Pi: out << "(pi (" << abst_name(a) << " : " << abst_type(a) << ") " << abst_expr(a) << ")"; break; case expr_kind::Pi: out << "(pi (" << abst_name(a) << " : " << abst_type(a) << ") " << abst_body(a) << ")"; break;
case expr_kind::Prop: out << "Prop"; break; case expr_kind::Prop: out << "Prop"; break;
case expr_kind::Type: out << "Type"; break; case expr_kind::Type: out << "Type"; break;
case expr_kind::Numeral: out << num_value(a); break; case expr_kind::Numeral: out << num_value(a); break;

8
src/kernel/expr.h
View file

@ -172,12 +172,12 @@ public:
class expr_abstraction : public expr_cell { class expr_abstraction : public expr_cell {
name m_name; name m_name;
expr m_type; expr m_type;
expr m_expr; expr m_body;
public: public:
expr_abstraction(expr_kind k, name const & n, expr const & t, expr const & e); expr_abstraction(expr_kind k, name const & n, expr const & t, expr const & e);
name const & get_name() const { return m_name; } name const & get_name() const { return m_name; }
expr const & get_type() const { return m_type; } expr const & get_type() const { return m_type; }
expr const & get_expr() const { return m_expr; } expr const & get_body() const { return m_body; }
}; };
// 5. Lambda // 5. Lambda
class expr_lambda : public expr_abstraction { class expr_lambda : public expr_abstraction {
@ -299,7 +299,7 @@ inline unsigned num_args(expr_cell * e) { return to_app(e)->get_
inline expr const & arg(expr_cell * e, unsigned idx) { return to_app(e)->get_arg(idx); } 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 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_type(expr_cell * e) { return to_abstraction(e)->get_type(); }
inline expr const & abst_expr(expr_cell * e) { return to_abstraction(e)->get_expr(); } inline expr const & abst_body(expr_cell * e) { return to_abstraction(e)->get_body(); }
inline unsigned ty_num_vars(expr_cell * e) { return to_type(e)->size(); } inline unsigned ty_num_vars(expr_cell * e) { return to_type(e)->size(); }
inline uvar const & ty_var(expr_cell * e, unsigned idx) { return to_type(e)->get_var(idx); } inline uvar const & ty_var(expr_cell * e, unsigned idx) { return to_type(e)->get_var(idx); }
inline mpz const & num_value(expr_cell * e) { return to_numeral(e)->get_num(); } inline mpz const & num_value(expr_cell * e) { return to_numeral(e)->get_num(); }
@ -315,7 +315,7 @@ inline expr const * begin_args(expr const & e) { return to_app(e)->beg
inline expr const * end_args(expr const & e) { return to_app(e)->end_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 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_type(expr const & e) { return to_abstraction(e)->get_type(); }
inline expr const & abst_expr(expr const & e) { return to_abstraction(e)->get_expr(); } inline expr const & abst_body(expr const & e) { return to_abstraction(e)->get_body(); }
inline unsigned ty_num_vars(expr const & e) { return to_type(e)->size(); } inline unsigned ty_num_vars(expr const & e) { return to_type(e)->size(); }
inline uvar const & ty_var(expr const & e, unsigned idx) { return to_type(e)->get_var(idx); } inline uvar const & ty_var(expr const & e, unsigned idx) { return to_type(e)->get_var(idx); }
inline mpz const & num_value(expr const & e) { return to_numeral(e)->get_num(); } inline mpz const & num_value(expr const & e) { return to_numeral(e)->get_num(); }

2
src/kernel/free_vars.cpp
View file

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

8
src/kernel/max_sharing.cpp
View file

@ -58,12 +58,12 @@ public:
case expr_kind::Lambda: case expr_kind::Lambda:
case expr_kind::Pi: { case expr_kind::Pi: {
expr const & old_t = abst_type(a); expr const & old_t = abst_type(a);
expr const & old_e = abst_expr(a); expr const & old_b = abst_body(a);
expr t = apply(old_t); expr t = apply(old_t);
expr e = apply(old_e); expr b = apply(old_b);
if (!eqp(t, old_t) || !eqp(e, old_e)) { if (!eqp(t, old_t) || !eqp(b, old_b)) {
name const & n = abst_name(a); name const & n = abst_name(a);
expr r = is_pi(a) ? pi(n, t, e) : lambda(n, t, e); expr r = is_pi(a) ? pi(n, t, b) : lambda(n, t, b);
cache(r); cache(r);
return r; return r;
} }

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

@ -53,7 +53,7 @@ unsigned depth1(expr const & e) {
return m + 1; return m + 1;
} }
case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Lambda: case expr_kind::Pi:
return std::max(depth1(abst_type(e)), depth1(abst_expr(e))) + 1; return std::max(depth1(abst_type(e)), depth1(abst_body(e))) + 1;
} }
return 0; return 0;
} }
@ -69,7 +69,7 @@ unsigned depth2(expr const & e) {
[](unsigned m, expr const & arg){ return std::max(depth2(arg), m); }) [](unsigned m, expr const & arg){ return std::max(depth2(arg), m); })
+ 1; + 1;
case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Lambda: case expr_kind::Pi:
return std::max(depth2(abst_type(e)), depth2(abst_expr(e))) + 1; return std::max(depth2(abst_type(e)), depth2(abst_body(e))) + 1;
} }
return 0; return 0;
} }
@ -96,7 +96,7 @@ unsigned depth3(expr const & e) {
} }
case expr_kind::Lambda: case expr_kind::Pi: 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_type(e), c));
todo.push_back(std::make_pair(&abst_expr(e), c)); todo.push_back(std::make_pair(&abst_body(e), c));
break; break;
} }
} }
@ -152,7 +152,7 @@ unsigned count_core(expr const & a, expr_set & s) {
return std::accumulate(begin_args(a), end_args(a), 1, return std::accumulate(begin_args(a), end_args(a), 1,
[&](unsigned sum, expr const & arg){ return sum + count_core(arg, s); }); [&](unsigned sum, expr const & arg){ return sum + count_core(arg, s); });
case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Lambda: case expr_kind::Pi:
return count_core(abst_type(a), s) + count_core(abst_expr(a), s) + 1; return count_core(abst_type(a), s) + count_core(abst_body(a), s) + 1;
} }
return 0; return 0;
} }