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

Reformat code (make formating more consistent)

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-07 08:17:33 -07:00
parent 58fef282c3
commit 722e2b0ed4
16 changed files with 107 additions and 204 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

111
src/interval/interval_def.h
View file

@ -146,8 +146,7 @@ void interval<T>::neg() {
if (is_upper_inf()) { if (is_upper_inf()) {
// (-oo, oo) case // (-oo, oo) case
// do nothing // do nothing
} } else {
else {
// (-oo, a| --> |-a, oo) // (-oo, a| --> |-a, oo)
swap(m_lower, m_upper); swap(m_lower, m_upper);
neg(m_lower); neg(m_lower);
@ -158,8 +157,7 @@ void interval<T>::neg() {
m_upper_inf = true; m_upper_inf = true;
m_upper_open = true; m_upper_open = true;
} }
} } else {
else {
if (is_upper_inf()) { if (is_upper_inf()) {
// |a, oo) --> (-oo, -a| // |a, oo) --> (-oo, -a|
swap(m_upper, m_lower); swap(m_upper, m_lower);
@ -170,8 +168,7 @@ void interval<T>::neg() {
reset(m_lower); reset(m_lower);
m_lower_inf = true; m_lower_inf = true;
m_lower_open = true; m_lower_open = true;
} } else {
else {
// |a, b| --> |-b, -a| // |a, b| --> |-b, -a|
swap(m_lower, m_upper); swap(m_lower, m_upper);
neg(m_lower); neg(m_lower);
@ -270,8 +267,7 @@ interval<T> & interval<T>::operator*=(interval<T> const & o) {
mul(new_l_val, new_l_kind, b, b_k, d, d_k); mul(new_l_val, new_l_kind, b, b_k, d, d_k);
round_to_plus_inf(); round_to_plus_inf();
mul(new_u_val, new_u_kind, a, a_k, c, c_k); mul(new_u_val, new_u_kind, a, a_k, c, c_k);
} } else if (i2.is_M()) {
else if (i2.is_M()) {
// a <= x <= b <= 0, y <= d, d > 0 --> a*d <= x*y (uses the fact that b is not positive) // a <= x <= b <= 0, y <= d, d > 0 --> a*d <= x*y (uses the fact that b is not positive)
// a <= x <= b <= 0, c <= y, c < 0 --> x*y <= a*c (uses the fact that b is not positive) // a <= x <= b <= 0, c <= y, c < 0 --> x*y <= a*c (uses the fact that b is not positive)
set_is_lower_open(a_o || d_o); set_is_lower_open(a_o || d_o);
@ -281,8 +277,7 @@ interval<T> & interval<T>::operator*=(interval<T> const & o) {
mul(new_l_val, new_l_kind, a, a_k, d, d_k); mul(new_l_val, new_l_kind, a, a_k, d, d_k);
round_to_plus_inf(); round_to_plus_inf();
mul(new_u_val, new_u_kind, a, a_k, c, c_k); mul(new_u_val, new_u_kind, a, a_k, c, c_k);
} } else {
else {
// a <= x <= b <= 0, 0 <= c <= y <= d --> a*d <= x*y (uses the fact that x is neg (b is not positive) or y is pos (c is not negative)) // a <= x <= b <= 0, 0 <= c <= y <= d --> a*d <= x*y (uses the fact that x is neg (b is not positive) or y is pos (c is not negative))
// x <= b <= 0, 0 <= c <= y --> x*y <= b*c // x <= b <= 0, 0 <= c <= y --> x*y <= b*c
lean_assert(i2.is_P()); lean_assert(i2.is_P());
@ -296,8 +291,7 @@ interval<T> & interval<T>::operator*=(interval<T> const & o) {
round_to_plus_inf(); round_to_plus_inf();
mul(new_u_val, new_u_kind, b, b_k, c, c_k); mul(new_u_val, new_u_kind, b, b_k, c, c_k);
} }
} } else if (i1.is_M()) {
else if (i1.is_M()) {
if (i2.is_N()) { if (i2.is_N()) {
// b > 0, x <= b, c <= y <= d <= 0 --> b*c <= x*y (uses the fact that d is not positive) // b > 0, x <= b, c <= y <= d <= 0 --> b*c <= x*y (uses the fact that d is not positive)
// a < 0, a <= x, c <= y <= d <= 0 --> x*y <= a*c (uses the fact that d is not positive) // a < 0, a <= x, c <= y <= d <= 0 --> x*y <= a*c (uses the fact that d is not positive)
@ -308,8 +302,7 @@ interval<T> & interval<T>::operator*=(interval<T> const & o) {
mul(new_l_val, new_l_kind, b, b_k, c, c_k); mul(new_l_val, new_l_kind, b, b_k, c, c_k);
round_to_plus_inf(); round_to_plus_inf();
mul(new_u_val, new_u_kind, a, a_k, c, c_k); mul(new_u_val, new_u_kind, a, a_k, c, c_k);
} } else if (i2.is_M()) {
else if (i2.is_M()) {
static thread_local T ad; xnumeral_kind ad_k; static thread_local T ad; xnumeral_kind ad_k;
static thread_local T bc; xnumeral_kind bc_k; static thread_local T bc; xnumeral_kind bc_k;
static thread_local T ac; xnumeral_kind ac_k; static thread_local T ac; xnumeral_kind ac_k;
@ -331,8 +324,7 @@ interval<T> & interval<T>::operator*=(interval<T> const & o) {
swap(new_l_val, ad); swap(new_l_val, ad);
new_l_kind = ad_k; new_l_kind = ad_k;
set_is_lower_open(ad_o); set_is_lower_open(ad_o);
} } else {
else {
swap(new_l_val, bc); swap(new_l_val, bc);
new_l_kind = bc_k; new_l_kind = bc_k;
set_is_lower_open(bc_o); set_is_lower_open(bc_o);
@ -343,14 +335,12 @@ interval<T> & interval<T>::operator*=(interval<T> const & o) {
swap(new_u_val, ac); swap(new_u_val, ac);
new_u_kind = ac_k; new_u_kind = ac_k;
set_is_upper_open(ac_o); set_is_upper_open(ac_o);
} } else {
else {
swap(new_u_val, bd); swap(new_u_val, bd);
new_u_kind = bd_k; new_u_kind = bd_k;
set_is_upper_open(bd_o); set_is_upper_open(bd_o);
} }
} } else {
else {
// a < 0, a <= x, 0 <= c <= y <= d --> a*d <= x*y (uses the fact that c is not negative) // a < 0, a <= x, 0 <= c <= y <= d --> a*d <= x*y (uses the fact that c is not negative)
// b > 0, x <= b, 0 <= c <= y <= d --> x*y <= b*d (uses the fact that c is not negative) // b > 0, x <= b, 0 <= c <= y <= d --> x*y <= b*d (uses the fact that c is not negative)
lean_assert(i2.is_P()); lean_assert(i2.is_P());
@ -363,8 +353,7 @@ interval<T> & interval<T>::operator*=(interval<T> const & o) {
round_to_plus_inf(); round_to_plus_inf();
mul(new_u_val, new_u_kind, b, b_k, d, d_k); mul(new_u_val, new_u_kind, b, b_k, d, d_k);
} }
} } else {
else {
lean_assert(i1.is_P()); lean_assert(i1.is_P());
if (i2.is_N()) { if (i2.is_N()) {
// 0 <= a <= x <= b, c <= y <= d <= 0 --> x*y <= b*c (uses the fact that x is pos (a is not neg) or y is neg (d is not pos)) // 0 <= a <= x <= b, c <= y <= d <= 0 --> x*y <= b*c (uses the fact that x is pos (a is not neg) or y is neg (d is not pos))
@ -378,8 +367,7 @@ interval<T> & interval<T>::operator*=(interval<T> const & o) {
mul(new_l_val, new_l_kind, b, b_k, c, c_k); mul(new_l_val, new_l_kind, b, b_k, c, c_k);
round_to_plus_inf(); round_to_plus_inf();
mul(new_u_val, new_u_kind, a, a_k, d, d_k); mul(new_u_val, new_u_kind, a, a_k, d, d_k);
} } else if (i2.is_M()) {
else if (i2.is_M()) {
// 0 <= a <= x <= b, c <= y --> b*c <= x*y (uses the fact that a is not negative) // 0 <= a <= x <= b, c <= y --> b*c <= x*y (uses the fact that a is not negative)
// 0 <= a <= x <= b, y <= d --> x*y <= b*d (uses the fact that a is not negative) // 0 <= a <= x <= b, y <= d --> x*y <= b*d (uses the fact that a is not negative)
set_is_lower_open(b_o || c_o); set_is_lower_open(b_o || c_o);
@ -389,8 +377,7 @@ interval<T> & interval<T>::operator*=(interval<T> const & o) {
mul(new_l_val, new_l_kind, b, b_k, c, c_k); mul(new_l_val, new_l_kind, b, b_k, c, c_k);
round_to_plus_inf(); round_to_plus_inf();
mul(new_u_val, new_u_kind, b, b_k, d, d_k); mul(new_u_val, new_u_kind, b, b_k, d, d_k);
} } else {
else {
lean_assert(i2.is_P()); lean_assert(i2.is_P());
// 0 <= a <= x, 0 <= c <= y --> a*c <= x*y // 0 <= a <= x, 0 <= c <= y --> a*c <= x*y
// x <= b, y <= d --> x*y <= b*d (uses the fact that x is pos (a is not negative) or y is pos (c is not negative)) // x <= b, y <= d --> x*y <= b*d (uses the fact that x is pos (a is not negative) or y is pos (c is not negative))
@ -424,8 +411,7 @@ interval<T> & interval<T>::operator/=(interval<T> const & o) {
if (i1.is_zero()) { if (i1.is_zero()) {
// 0/other = 0 if other != 0 // 0/other = 0 if other != 0
// do nothing // do nothing
} } else {
else {
T const & a = i1.m_lower; xnumeral_kind a_k = i1.lower_kind(); T const & a = i1.m_lower; xnumeral_kind a_k = i1.lower_kind();
T const & b = i1.m_upper; xnumeral_kind b_k = i1.upper_kind(); T const & b = i1.m_upper; xnumeral_kind b_k = i1.upper_kind();
T const & c = i2.m_lower; xnumeral_kind c_k = i2.lower_kind(); T const & c = i2.m_lower; xnumeral_kind c_k = i2.lower_kind();
@ -453,13 +439,11 @@ interval<T> & interval<T>::operator/=(interval<T> const & o) {
lean_assert(d_o); lean_assert(d_o);
reset(new_u_val); reset(new_u_val);
new_u_kind = XN_PLUS_INFINITY; new_u_kind = XN_PLUS_INFINITY;
} } else {
else {
round_to_plus_inf(); round_to_plus_inf();
div(new_u_val, new_u_kind, a, a_k, d, d_k); div(new_u_val, new_u_kind, a, a_k, d, d_k);
} }
} } else {
else {
// a <= x, a < 0, 0 < c <= y --> a/c <= x/y // a <= x, a < 0, 0 < c <= y --> a/c <= x/y
// x <= b <= 0, 0 < c <= y <= d --> x/y <= b/d // x <= b <= 0, 0 < c <= y <= d --> x/y <= b/d
lean_assert(i2.is_P1()); lean_assert(i2.is_P1());
@ -471,16 +455,14 @@ interval<T> & interval<T>::operator/=(interval<T> const & o) {
lean_assert(c_o); lean_assert(c_o);
reset(new_l_val); reset(new_l_val);
new_l_kind = XN_MINUS_INFINITY; new_l_kind = XN_MINUS_INFINITY;
} } else {
else {
round_to_minus_inf(); round_to_minus_inf();
div(new_l_val, new_l_kind, a, a_k, c, c_k); div(new_l_val, new_l_kind, a, a_k, c, c_k);
} }
round_to_plus_inf(); round_to_plus_inf();
div(new_u_val, new_u_kind, b, b_k, d, d_k); div(new_u_val, new_u_kind, b, b_k, d, d_k);
} }
} } else if (i1.is_M()) {
else if (i1.is_M()) {
if (i2.is_N1()) { if (i2.is_N1()) {
// 0 < a <= x <= b < 0, y <= d < 0 --> b/d <= x/y // 0 < a <= x <= b < 0, y <= d < 0 --> b/d <= x/y
// 0 < a <= x <= b < 0, y <= d < 0 --> x/y <= a/d // 0 < a <= x <= b < 0, y <= d < 0 --> x/y <= a/d
@ -493,15 +475,13 @@ interval<T> & interval<T>::operator/=(interval<T> const & o) {
reset(new_u_val); reset(new_u_val);
new_l_kind = XN_MINUS_INFINITY; new_l_kind = XN_MINUS_INFINITY;
new_u_kind = XN_PLUS_INFINITY; new_u_kind = XN_PLUS_INFINITY;
} } else {
else {
round_to_minus_inf(); round_to_minus_inf();
div(new_l_val, new_l_kind, b, b_k, d, d_k); div(new_l_val, new_l_kind, b, b_k, d, d_k);
round_to_plus_inf(); round_to_plus_inf();
div(new_u_val, new_u_kind, a, a_k, d, d_k); div(new_u_val, new_u_kind, a, a_k, d, d_k);
} }
} } else {
else {
// 0 < a <= x <= b < 0, 0 < c <= y --> a/c <= x/y // 0 < a <= x <= b < 0, 0 < c <= y --> a/c <= x/y
// 0 < a <= x <= b < 0, 0 < c <= y --> x/y <= b/c // 0 < a <= x <= b < 0, 0 < c <= y --> x/y <= b/c
lean_assert(i1.is_P1()); lean_assert(i1.is_P1());
@ -515,16 +495,14 @@ interval<T> & interval<T>::operator/=(interval<T> const & o) {
reset(new_u_val); reset(new_u_val);
new_l_kind = XN_MINUS_INFINITY; new_l_kind = XN_MINUS_INFINITY;
new_u_kind = XN_PLUS_INFINITY; new_u_kind = XN_PLUS_INFINITY;
} } else {
else {
round_to_minus_inf(); round_to_minus_inf();
div(new_l_val, new_l_kind, a, a_k, c, c_k); div(new_l_val, new_l_kind, a, a_k, c, c_k);
round_to_plus_inf(); round_to_plus_inf();
div(new_u_val, new_u_kind, b, b_k, c, c_k); div(new_u_val, new_u_kind, b, b_k, c, c_k);
} }
} }
} } else {
else {
lean_assert(i1.is_P()); lean_assert(i1.is_P());
if (i2.is_N1()) { if (i2.is_N1()) {
// b > 0, x <= b, c <= y <= d < 0 --> b/d <= x/y // b > 0, x <= b, c <= y <= d < 0 --> b/d <= x/y
@ -536,15 +514,13 @@ interval<T> & interval<T>::operator/=(interval<T> const & o) {
lean_assert(d_o); lean_assert(d_o);
reset(new_l_val); reset(new_l_val);
new_l_kind = XN_MINUS_INFINITY; new_l_kind = XN_MINUS_INFINITY;
} } else {
else {
round_to_minus_inf(); round_to_minus_inf();
div(new_l_val, new_l_kind, b, b_k, d, d_k); div(new_l_val, new_l_kind, b, b_k, d, d_k);
} }
round_to_plus_inf(); round_to_plus_inf();
div(new_u_val, new_u_kind, a, a_k, c, c_k); div(new_u_val, new_u_kind, a, a_k, c, c_k);
} } else {
else {
lean_assert(i2.is_P1()); lean_assert(i2.is_P1());
// 0 <= a <= x, 0 < c <= y <= d --> a/d <= x/y // 0 <= a <= x, 0 < c <= y <= d --> a/d <= x/y
// b > 0 x <= b, 0 < c <= y --> x/y <= b/c // b > 0 x <= b, 0 < c <= y --> x/y <= b/c
@ -557,8 +533,7 @@ interval<T> & interval<T>::operator/=(interval<T> const & o) {
lean_assert(c_o); lean_assert(c_o);
reset(new_u_val); reset(new_u_val);
new_u_kind = XN_PLUS_INFINITY; new_u_kind = XN_PLUS_INFINITY;
} } else {
else {
round_to_plus_inf(); round_to_plus_inf();
div(new_u_val, new_u_kind, b, b_k, c, c_k); div(new_u_val, new_u_kind, b, b_k, c, c_k);
} }
@ -599,8 +574,7 @@ void interval<T>::inv() {
reset(m_upper); reset(m_upper);
set_is_upper_inf(true); set_is_upper_inf(true);
set_is_upper_open(true); set_is_upper_open(true);
} } else {
else {
round_to_plus_inf(); round_to_plus_inf();
new_u_val = m_lower; new_u_val = m_lower;
inv(new_u_val); inv(new_u_val);
@ -612,8 +586,7 @@ void interval<T>::inv() {
swap(m_lower, new_l_val); swap(m_lower, new_l_val);
set_is_lower_inf(false); set_is_lower_inf(false);
set_is_lower_open(new_l_open); set_is_lower_open(new_l_open);
} } else if (is_N1()) {
else if (is_N1()) {
// x <= u < 0 --> 1/u <= 1/x // x <= u < 0 --> 1/u <= 1/x
// l <= x <= u < 0 --> 1/l <= 1/x (use lower and upper bounds) // l <= x <= u < 0 --> 1/l <= 1/x (use lower and upper bounds)
round_to_plus_inf(); round_to_plus_inf();
@ -629,8 +602,7 @@ void interval<T>::inv() {
reset(m_lower); reset(m_lower);
set_is_lower_open(true); set_is_lower_open(true);
set_is_lower_inf(true); set_is_lower_inf(true);
} } else {
else {
round_to_minus_inf(); round_to_minus_inf();
new_l_val = m_upper; new_l_val = m_upper;
inv(new_l_val); inv(new_l_val);
@ -642,8 +614,7 @@ void interval<T>::inv() {
swap(m_upper, new_u_val); swap(m_upper, new_u_val);
set_is_upper_inf(false); set_is_upper_inf(false);
set_is_upper_open(new_u_open); set_is_upper_open(new_u_open);
} } else {
else {
lean_unreachable(); lean_unreachable();
} }
lean_assert(check_invariant()); lean_assert(check_invariant());
@ -657,8 +628,7 @@ void interval<T>::power(unsigned n) {
// a^1 = a // a^1 = a
// nothing to be done // nothing to be done
return; return;
} } else if (n % 2 == 0) {
else if (n % 2 == 0) {
if (is_lower_pos()) { if (is_lower_pos()) {
// [l, u]^n = [l^n, u^n] if l > 0 // [l, u]^n = [l^n, u^n] if l > 0
// 0 < l <= x --> l^n <= x^n (lower bound guarantees that is positive) // 0 < l <= x --> l^n <= x^n (lower bound guarantees that is positive)
@ -671,8 +641,7 @@ void interval<T>::power(unsigned n) {
round_to_plus_inf(); round_to_plus_inf();
power(m_upper, n); power(m_upper, n);
} }
} } else if (is_upper_neg()) {
else if (is_upper_neg()) {
// [l, u]^n = [u^n, l^n] if u < 0 // [l, u]^n = [u^n, l^n] if u < 0
// l <= x <= u < 0 --> x^n <= l^n (use lower and upper bound -- need the fact that x is negative) // l <= x <= u < 0 --> x^n <= l^n (use lower and upper bound -- need the fact that x is negative)
// x <= u < 0 --> u^n <= x^n // x <= u < 0 --> u^n <= x^n
@ -688,15 +657,13 @@ void interval<T>::power(unsigned n) {
if (li) { if (li) {
reset(m_upper); reset(m_upper);
} } else {
else {
round_to_plus_inf(); round_to_plus_inf();
power(m_upper, n); power(m_upper, n);
} }
m_upper_inf = li; m_upper_inf = li;
m_upper_open = lo; m_upper_open = lo;
} } else {
else {
// [l, u]^n = [0, max{l^n, u^n}] otherwise // [l, u]^n = [0, max{l^n, u^n}] otherwise
// we need both bounds to justify upper bound // we need both bounds to justify upper bound
xnumeral_kind un1_kind = lower_kind(); xnumeral_kind un1_kind = lower_kind();
@ -713,8 +680,7 @@ void interval<T>::power(unsigned n) {
swap(m_upper, un1); swap(m_upper, un1);
m_upper_inf = (un1_kind == XN_PLUS_INFINITY); m_upper_inf = (un1_kind == XN_PLUS_INFINITY);
m_upper_open = m_lower_open; m_upper_open = m_lower_open;
} } else {
else {
swap(m_upper, un2); swap(m_upper, un2);
m_upper_inf = (un2_kind == XN_PLUS_INFINITY); m_upper_inf = (un2_kind == XN_PLUS_INFINITY);
} }
@ -723,8 +689,7 @@ void interval<T>::power(unsigned n) {
m_lower_inf = false; m_lower_inf = false;
m_lower_open = false; m_lower_open = false;
} }
} } else {
else {
// Remark: when n is odd x^n is monotonic. // Remark: when n is odd x^n is monotonic.
if (!m_lower_inf) if (!m_lower_inf)
power(m_lower, n); power(m_lower, n);
@ -745,8 +710,7 @@ T a_div_x_n(T a, T const & x, unsigned n, bool to_plus_inf) {
if (n == 1) { if (n == 1) {
numeric_traits<T>::set_rounding(to_plus_inf); numeric_traits<T>::set_rounding(to_plus_inf);
a /= x; a /= x;
} } else {
else {
static thread_local T tmp; static thread_local T tmp;
numeric_traits<T>::set_rounding(!to_plus_inf); numeric_traits<T>::set_rounding(!to_plus_inf);
tmp = x; tmp = x;
@ -764,8 +728,7 @@ bool interval<T>::check_invariant() const {
if (eq(m_lower, lower_kind(), m_upper, upper_kind())) { if (eq(m_lower, lower_kind(), m_upper, upper_kind())) {
lean_assert(!is_lower_open()); lean_assert(!is_lower_open());
lean_assert(!is_upper_open()); lean_assert(!is_upper_open());
} } else {
else {
lean_assert(lt(m_lower, lower_kind(), m_upper, upper_kind())); lean_assert(lt(m_lower, lower_kind(), m_upper, upper_kind()));
} }
return true; return true;

15
src/kernel/expr.cpp
View file

@ -50,8 +50,7 @@ expr mk_app(unsigned n, expr const * as) {
if (is_app(arg0)) { if (is_app(arg0)) {
n0 = num_args(arg0); n0 = num_args(arg0);
new_n = n + n0 - 1; new_n = n + n0 - 1;
} } else {
else {
new_n = n; new_n = n;
} }
char * mem = new char[sizeof(expr_app) + new_n*sizeof(expr)]; char * mem = new char[sizeof(expr_app) + new_n*sizeof(expr)];
@ -198,20 +197,22 @@ std::ostream & operator<<(std::ostream & out, expr const & a) {
case expr_kind::Eq: out << "(" << eq_lhs(a) << " = " << eq_rhs(a) << ")"; break; case expr_kind::Eq: out << "(" << eq_lhs(a) << " = " << eq_rhs(a) << ")"; break;
case expr_kind::Lambda: out << "(fun " << abst_name(a) << " : " << abst_domain(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: case expr_kind::Pi:
if (!is_arrow(a)) if (!is_arrow(a)) {
out << "(pi " << abst_name(a) << " : " << abst_domain(a) << ", " << abst_body(a) << ")"; out << "(pi " << abst_name(a) << " : " << abst_domain(a) << ", " << abst_body(a) << ")";
else if (!is_arrow(abst_domain(a))) } else if (!is_arrow(abst_domain(a))) {
out << abst_domain(a) << " -> " << abst_body(a); out << abst_domain(a) << " -> " << abst_body(a);
else } else {
out << "(" << abst_domain(a) << ") -> " << abst_body(a); out << "(" << abst_domain(a) << ") -> " << abst_body(a);
}
break; break;
case expr_kind::Let: out << "(let " << let_name(a) << " := " << let_value(a) << " in " << let_body(a) << ")"; break; case expr_kind::Let: out << "(let " << let_name(a) << " := " << let_value(a) << " in " << let_body(a) << ")"; break;
case expr_kind::Type: { case expr_kind::Type: {
level const & l = ty_level(a); level const & l = ty_level(a);
if (l == level()) if (l == level()) {
out << "Type"; out << "Type";
else } else {
out << "(Type " << ty_level(a) << ")"; out << "(Type " << ty_level(a) << ")";
}
break; break;
} }
case expr_kind::Value: to_value(a).display(out); break; case expr_kind::Value: to_value(a).display(out); break;

3
src/kernel/expr.h
View file

@ -441,8 +441,7 @@ template<typename F> expr update_abst(expr const & e, F f) {
if (!is_eqp(p.first, old_t) || !is_eqp(p.second, old_b)) { if (!is_eqp(p.first, old_t) || !is_eqp(p.second, old_b)) {
name const & n = abst_name(e); name const & n = abst_name(e);
return is_pi(e) ? mk_pi(n, p.first, p.second) : mk_lambda(n, p.first, p.second); return is_pi(e) ? mk_pi(n, p.first, p.second) : mk_lambda(n, p.first, p.second);
} } else {
else {
return e; return e;
} }
} }

6
src/kernel/free_vars.cpp
View file

@ -108,8 +108,7 @@ expr lower_free_vars(expr const & e, unsigned d) {
if (is_var(e) && var_idx(e) >= offset) { if (is_var(e) && var_idx(e) >= offset) {
lean_assert(var_idx(e) >= offset + d); lean_assert(var_idx(e) >= offset + d);
return mk_var(var_idx(e) - d); return mk_var(var_idx(e) - d);
} } else {
else {
return e; return e;
} }
}; };
@ -122,8 +121,7 @@ expr lift_free_vars(expr const & e, unsigned d) {
auto f = [=](expr const & e, unsigned offset) -> expr { auto f = [=](expr const & e, unsigned offset) -> expr {
if (is_var(e) && var_idx(e) >= offset) { if (is_var(e) && var_idx(e) >= offset) {
return mk_var(var_idx(e) + d); return mk_var(var_idx(e) + d);
} } else {
else {
return e; return e;
} }
}; };

3
src/kernel/level.cpp
View file

@ -121,8 +121,7 @@ level max(level const & l1, level const & l2) {
return max_core(to_max(l1), to_max(l1)); return max_core(to_max(l1), to_max(l1));
else else
return max_core(to_max(l1), l2); return max_core(to_max(l1), l2);
} } else {
else {
if (is_max(l2)) if (is_max(l2))
return max_core(l1, to_max(l2)); return max_core(l1, to_max(l2));
else else

3
src/kernel/normalize.cpp
View file

@ -157,8 +157,7 @@ class normalize_fn {
if (i == n - 1) if (i == n - 1)
return f; return f;
i++; i++;
} } else {
else {
buffer<expr> new_args; buffer<expr> new_args;
expr new_f = reify(f, k); expr new_f = reify(f, k);
new_args.push_back(new_f); new_args.push_back(new_f);

3
src/kernel/type_check.cpp
View file

@ -27,8 +27,7 @@ bool is_convertible_core(expr const & expected, expr const & given, environment
if (is_pi(*e) && is_pi(*g) && abst_domain(*e) == abst_domain(*g)) { if (is_pi(*e) && is_pi(*g) && abst_domain(*e) == abst_domain(*g)) {
e = &abst_body(*e); e = &abst_body(*e);
g = &abst_body(*g); g = &abst_body(*g);
} } else {
else {
return false; return false;
} }
} }

3
src/util/debug.cpp
View file

@ -96,8 +96,7 @@ void invoke_debugger() {
buffer << "gdb -nw /proc/" << getpid() << "/exe " << getpid(); buffer << "gdb -nw /proc/" << getpid() << "/exe " << getpid();
if (system(buffer.str().c_str()) == 0) { if (system(buffer.str().c_str()) == 0) {
std::cerr << "continuing the execution...\n"; std::cerr << "continuing the execution...\n";
} } else {
else {
std::cerr << "ERROR STARTING GDB...\n"; std::cerr << "ERROR STARTING GDB...\n";
// forcing seg fault. // forcing seg fault.
int * x = 0; int * x = 0;

3
src/util/escaped.cpp
View file

@ -16,8 +16,7 @@ char const * escaped::end() const {
if (!m_trim_nl || *it != '\n') { if (!m_trim_nl || *it != '\n') {
++it; ++it;
e = it; e = it;
} } else {
else {
++it; ++it;
} }
} }

15
src/util/name.cpp
View file

@ -166,8 +166,7 @@ bool operator==(name const & a, name const & b) {
if (i1->m_is_string) { if (i1->m_is_string) {
if (strcmp(i1->m_str, i2->m_str) != 0) if (strcmp(i1->m_str, i2->m_str) != 0)
return false; return false;
} } else {
else {
if (i1->m_k != i2->m_k) if (i1->m_k != i2->m_k)
return false; return false;
} }
@ -194,8 +193,7 @@ int cmp(name::imp * i1, name::imp * i2) {
int c = strcmp(i1->m_str, i2->m_str); int c = strcmp(i1->m_str, i2->m_str);
if (c != 0) if (c != 0)
return c; return c;
} } else if (i1->m_k != i2->m_k) {
else if (i1->m_k != i2->m_k) {
return i1->m_k < i2->m_k ? -1 : 1; return i1->m_k < i2->m_k ? -1 : 1;
} }
} }
@ -227,23 +225,20 @@ static unsigned num_digits(unsigned k) {
size_t name::size(char const * sep) const { size_t name::size(char const * sep) const {
if (m_ptr == nullptr) { if (m_ptr == nullptr) {
return strlen(anonymous_str); return strlen(anonymous_str);
} } else {
else {
imp * i = m_ptr; imp * i = m_ptr;
size_t sep_sz = strlen(sep); size_t sep_sz = strlen(sep);
size_t r = 0; size_t r = 0;
while (true) { while (true) {
if (i->m_is_string) { if (i->m_is_string) {
r += strlen(i->m_str); r += strlen(i->m_str);
} } else {
else {
r += num_digits(i->m_k); r += num_digits(i->m_k);
} }
if (i->m_prefix) { if (i->m_prefix) {
r += sep_sz; r += sep_sz;
i = i->m_prefix; i = i->m_prefix;
} } else {
else {
break; break;
} }
} }

82
src/util/numerics/mpbq.cpp
View file

@ -14,8 +14,7 @@ bool set(mpbq & a, mpq const & b) {
numerator(a.m_num, b); numerator(a.m_num, b);
a.m_k = 0; a.m_k = 0;
return true; return true;
} } else {
else {
static thread_local mpz d; static thread_local mpz d;
denominator(d, b); denominator(d, b);
unsigned shift; unsigned shift;
@ -24,8 +23,7 @@ bool set(mpbq & a, mpq const & b) {
a.m_k = shift; a.m_k = shift;
lean_assert(a == b); lean_assert(a == b);
return true; return true;
} } else {
else {
numerator(a.m_num, b); numerator(a.m_num, b);
a.m_k = d.log2() + 1; a.m_k = d.log2() + 1;
return false; return false;
@ -49,13 +47,12 @@ void mpbq::normalize() {
int cmp(mpbq const & a, mpbq const & b) { int cmp(mpbq const & a, mpbq const & b) {
static thread_local mpz tmp; static thread_local mpz tmp;
if (a.m_k == b.m_k) if (a.m_k == b.m_k) {
return cmp(a.m_num, b.m_num); return cmp(a.m_num, b.m_num);
else if (a.m_k < b.m_k) { } else if (a.m_k < b.m_k) {
mul2k(tmp, a.m_num, b.m_k - a.m_k); mul2k(tmp, a.m_num, b.m_k - a.m_k);
return cmp(tmp, b.m_num); return cmp(tmp, b.m_num);
} } else {
else {
lean_assert(a.m_k > b.m_k); lean_assert(a.m_k > b.m_k);
mul2k(tmp, b.m_num, a.m_k - b.m_k); mul2k(tmp, b.m_num, a.m_k - b.m_k);
return cmp(a.m_num, tmp); return cmp(a.m_num, tmp);
@ -66,8 +63,7 @@ int cmp(mpbq const & a, mpz const & b) {
static thread_local mpz tmp; static thread_local mpz tmp;
if (a.m_k == 0) { if (a.m_k == 0) {
return cmp(a.m_num, b); return cmp(a.m_num, b);
} } else {
else {
mul2k(tmp, b, a.m_k); mul2k(tmp, b, a.m_k);
return cmp(a.m_num, tmp); return cmp(a.m_num, tmp);
} }
@ -76,8 +72,7 @@ int cmp(mpbq const & a, mpz const & b) {
int cmp(mpbq const & a, mpq const & b) { int cmp(mpbq const & a, mpq const & b) {
if (a.is_integer() && b.is_integer()) { if (a.is_integer() && b.is_integer()) {
return -cmp(b, a.m_num); return -cmp(b, a.m_num);
} } else {
else {
static thread_local mpz tmp1; static thread_local mpz tmp1;
static thread_local mpz tmp2; static thread_local mpz tmp2;
// tmp1 <- numerator(a)*denominator(b) // tmp1 <- numerator(a)*denominator(b)
@ -91,13 +86,11 @@ int cmp(mpbq const & a, mpq const & b) {
mpbq & mpbq::operator+=(mpbq const & a) { mpbq & mpbq::operator+=(mpbq const & a) {
if (m_k == a.m_k) { if (m_k == a.m_k) {
m_num += a.m_num; m_num += a.m_num;
} } else if (m_k < a.m_k) {
else if (m_k < a.m_k) {
mul2k(m_num, m_num, a.m_k - m_k); mul2k(m_num, m_num, a.m_k - m_k);
m_k = a.m_k; m_k = a.m_k;
m_num += a.m_num; m_num += a.m_num;
} } else {
else {
lean_assert(m_k > a.m_k); lean_assert(m_k > a.m_k);
static thread_local mpz tmp; static thread_local mpz tmp;
mul2k(tmp, a.m_num, m_k - a.m_k); mul2k(tmp, a.m_num, m_k - a.m_k);
@ -111,8 +104,7 @@ template<typename T>
mpbq & mpbq::add_int(T const & a) { mpbq & mpbq::add_int(T const & a) {
if (m_k == 0) { if (m_k == 0) {
m_num += a; m_num += a;
} } else {
else {
lean_assert(m_k > 0); lean_assert(m_k > 0);
static thread_local mpz tmp; static thread_local mpz tmp;
tmp = a; tmp = a;
@ -128,13 +120,11 @@ mpbq & mpbq::operator+=(int a) { return add_int<int>(a); }
mpbq & mpbq::operator-=(mpbq const & a) { mpbq & mpbq::operator-=(mpbq const & a) {
if (m_k == a.m_k) { if (m_k == a.m_k) {
m_num -= a.m_num; m_num -= a.m_num;
} } else if (m_k < a.m_k) {
else if (m_k < a.m_k) {
mul2k(m_num, m_num, a.m_k - m_k); mul2k(m_num, m_num, a.m_k - m_k);
m_k = a.m_k; m_k = a.m_k;
m_num -= a.m_num; m_num -= a.m_num;
} } else {
else {
lean_assert(m_k > a.m_k); lean_assert(m_k > a.m_k);
static thread_local mpz tmp; static thread_local mpz tmp;
mul2k(tmp, a.m_num, m_k - a.m_k); mul2k(tmp, a.m_num, m_k - a.m_k);
@ -148,8 +138,7 @@ template<typename T>
mpbq & mpbq::sub_int(T const & a) { mpbq & mpbq::sub_int(T const & a) {
if (m_k == 0) { if (m_k == 0) {
m_num -= a; m_num -= a;
} } else {
else {
lean_assert(m_k > 0); lean_assert(m_k > 0);
static thread_local mpz tmp; static thread_local mpz tmp;
tmp = a; tmp = a;
@ -167,8 +156,7 @@ mpbq & mpbq::operator*=(mpbq const & a) {
if (m_k == 0 || a.m_k == 0) { if (m_k == 0 || a.m_k == 0) {
m_k += a.m_k; m_k += a.m_k;
normalize(); normalize();
} } else {
else {
m_k += a.m_k; m_k += a.m_k;
} }
return *this; return *this;
@ -196,11 +184,9 @@ int mpbq::magnitude_lb() const {
int s = m_num.sgn(); int s = m_num.sgn();
if (s < 0) { if (s < 0) {
return m_num.mlog2() - m_k + 1; return m_num.mlog2() - m_k + 1;
} } else if (s == 0) {
else if (s == 0) {
return 0; return 0;
} } else {
else {
lean_assert(s > 0); lean_assert(s > 0);
return m_num.log2() - m_k; return m_num.log2() - m_k;
} }
@ -210,11 +196,9 @@ int mpbq::magnitude_ub() const {
int s = m_num.sgn(); int s = m_num.sgn();
if (s < 0) { if (s < 0) {
return m_num.mlog2() - m_k; return m_num.mlog2() - m_k;
} } else if (s == 0) {
else if (s == 0) {
return 0; return 0;
} } else {
else {
lean_assert(s > 0); lean_assert(s > 0);
return m_num.log2() - m_k + 1; return m_num.log2() - m_k + 1;
} }
@ -223,8 +207,7 @@ int mpbq::magnitude_ub() const {
void mul2(mpbq & a) { void mul2(mpbq & a) {
if (a.m_k == 0) { if (a.m_k == 0) {
mul2k(a.m_num, a.m_num, 1); mul2k(a.m_num, a.m_num, 1);
} } else {
else {
a.m_k--; a.m_k--;
} }
} }
@ -235,8 +218,7 @@ void mul2k(mpbq & a, unsigned k) {
if (a.m_k < k) { if (a.m_k < k) {
mul2k(a.m_num, a.m_num, k - a.m_k); mul2k(a.m_num, a.m_num, k - a.m_k);
a.m_k = 0; a.m_k = 0;
} } else {
else {
lean_assert(a.m_k >= k); lean_assert(a.m_k >= k);
a.m_k -= k; a.m_k -= k;
} }
@ -250,13 +232,11 @@ bool root_lower(mpbq & a, mpbq const & b, unsigned n) {
a.m_k = b.m_k / n; a.m_k = b.m_k / n;
a.normalize(); a.normalize();
return r; return r;
} } else if (a.m_num.is_neg()) {
else if (a.m_num.is_neg()) {
a.m_k = b.m_k / n; a.m_k = b.m_k / n;
a.normalize(); a.normalize();
return false; return false;
} } else {
else {
a.m_k = b.m_k / n; a.m_k = b.m_k / n;
a.m_k++; a.m_k++;
a.normalize(); a.normalize();
@ -270,14 +250,12 @@ bool root_upper(mpbq & a, mpbq const & b, unsigned n) {
a.m_k = b.m_k / n; a.m_k = b.m_k / n;
a.normalize(); a.normalize();
return r; return r;
} } else if (a.m_num.is_neg()) {
else if (a.m_num.is_neg()) {
a.m_k = b.m_k / n; a.m_k = b.m_k / n;
a.m_k++; a.m_k++;
a.normalize(); a.normalize();
return false; return false;
} } else {
else {
a.m_k = b.m_k / n; a.m_k = b.m_k / n;
a.normalize(); a.normalize();
return false; return false;
@ -322,8 +300,7 @@ bool lt_1div2k(mpbq const & a, unsigned k) {
if (a.m_k <= k) { if (a.m_k <= k) {
// since a.m_num >= 1 // since a.m_num >= 1
return false; return false;
} } else {
else {
lean_assert(a.m_k > k); lean_assert(a.m_k > k);
static thread_local mpz tmp; static thread_local mpz tmp;
tmp = 1; tmp = 1;
@ -335,11 +312,9 @@ bool lt_1div2k(mpbq const & a, unsigned k) {
std::ostream & operator<<(std::ostream & out, mpbq const & v) { std::ostream & operator<<(std::ostream & out, mpbq const & v) {
if (v.m_k == 0) { if (v.m_k == 0) {
out << v.m_num; out << v.m_num;
} } else if (v.m_k == 1) {
else if (v.m_k == 1) {
out << v.m_num << "/2"; out << v.m_num << "/2";
} } else {
else {
out << v.m_num << "/2^" << v.m_k; out << v.m_num << "/2^" << v.m_k;
} }
return out; return out;
@ -349,8 +324,7 @@ void display_decimal(std::ostream & out, mpbq const & a, unsigned prec) {
if (a.is_integer()) { if (a.is_integer()) {
out << a.m_num; out << a.m_num;
return; return;
} } else {
else {
mpz two_k; mpz two_k;
mpz n1, v1; mpz n1, v1;
if (a.is_neg()) if (a.is_neg())

7
src/util/numerics/mpq.cpp
View file

@ -20,8 +20,7 @@ mpq & mpq::operator=(mpbq const & b) {
int cmp(mpq const & a, mpz const & b) { int cmp(mpq const & a, mpz const & b) {
if (a.is_integer()) { if (a.is_integer()) {
return mpz_cmp(mpq_numref(a.m_val), mpq::zval(b)); return mpz_cmp(mpq_numref(a.m_val), mpq::zval(b));
} } else {
else {
static thread_local mpz tmp; static thread_local mpz tmp;
mpz_mul(mpq::zval(tmp), mpq_denref(a.m_val), mpq::zval(b)); mpz_mul(mpq::zval(tmp), mpq_denref(a.m_val), mpq::zval(b));
return mpz_cmp(mpq_numref(a.m_val), mpq::zval(tmp)); return mpz_cmp(mpq_numref(a.m_val), mpq::zval(tmp));
@ -79,8 +78,7 @@ extern void display(std::ostream & out, __mpz_struct const * v);
std::ostream & operator<<(std::ostream & out, mpq const & v) { std::ostream & operator<<(std::ostream & out, mpq const & v) {
if (v.is_integer()) { if (v.is_integer()) {
display(out, mpq_numref(v.m_val)); display(out, mpq_numref(v.m_val));
} } else {
else {
display(out, mpq_numref(v.m_val)); display(out, mpq_numref(v.m_val));
out << "/"; out << "/";
display(out, mpq_denref(v.m_val)); display(out, mpq_denref(v.m_val));
@ -113,7 +111,6 @@ void display_decimal(std::ostream & out, mpq const & a, unsigned prec) {
} }
out << "?"; out << "?";
} }
} }
void pp(lean::mpq const & v) { std::cout << v << std::endl; } void pp(lean::mpq const & v) { std::cout << v << std::endl; }

6
src/util/numerics/mpz.cpp
View file

@ -35,8 +35,7 @@ bool mpz::is_power_of_two(unsigned & shift) const {
if (mpz_popcount(m_val) == 1) { if (mpz_popcount(m_val) == 1) {
shift = log2(); shift = log2();
return true; return true;
} } else {
else {
return false; return false;
} }
} }
@ -64,8 +63,7 @@ void display(std::ostream & out, __mpz_struct const * v) {
char buffer[1024]; char buffer[1024];
mpz_get_str(buffer, 10, v); mpz_get_str(buffer, 10, v);
out << buffer; out << buffer;
} } else {
else {
std::unique_ptr<char> buffer(new char[sz]); std::unique_ptr<char> buffer(new char[sz]);
mpz_get_str(buffer.get(), 10, v); mpz_get_str(buffer.get(), 10, v);
out << buffer.get(); out << buffer.get();

27
src/util/numerics/xnumeral.h
View file

@ -94,12 +94,10 @@ void add(T & r, xnumeral_kind & rk, T const & a, xnumeral_kind ak, T const & b,
if (ak != XN_NUMERAL) { if (ak != XN_NUMERAL) {
numeric_traits<T>::reset(r); numeric_traits<T>::reset(r);
rk = ak; rk = ak;
} } else if (bk != XN_NUMERAL) {
else if (bk != XN_NUMERAL) {
numeric_traits<T>::reset(r); numeric_traits<T>::reset(r);
rk = bk; rk = bk;
} } else {
else {
r = a + b; r = a + b;
rk = XN_NUMERAL; rk = XN_NUMERAL;
} }
@ -113,8 +111,7 @@ void sub(T & r, xnumeral_kind & rk, T const & a, xnumeral_kind ak, T const & b,
lean_assert(bk != ak); lean_assert(bk != ak);
numeric_traits<T>::reset(r); numeric_traits<T>::reset(r);
rk = ak; rk = ak;
} } else {
else {
switch (bk) { switch (bk) {
case XN_MINUS_INFINITY: case XN_MINUS_INFINITY:
numeric_traits<T>::reset(r); numeric_traits<T>::reset(r);
@ -137,15 +134,13 @@ void mul(T & r, xnumeral_kind & rk, T const & a, xnumeral_kind ak, T const & b,
if (is_zero(a, ak) || is_zero(b, bk)) { if (is_zero(a, ak) || is_zero(b, bk)) {
numeric_traits<T>::reset(r); numeric_traits<T>::reset(r);
rk = XN_NUMERAL; rk = XN_NUMERAL;
} } else if (is_infinite(ak) || is_infinite(bk)) {
else if (is_infinite(ak) || is_infinite(bk)) {
if (is_pos(a, ak) == is_pos(b, bk)) if (is_pos(a, ak) == is_pos(b, bk))
rk = XN_PLUS_INFINITY; rk = XN_PLUS_INFINITY;
else else
rk = XN_MINUS_INFINITY; rk = XN_MINUS_INFINITY;
numeric_traits<T>::reset(r); numeric_traits<T>::reset(r);
} } else {
else {
rk = XN_NUMERAL; rk = XN_NUMERAL;
r = a * b; r = a * b;
} }
@ -158,21 +153,18 @@ void div(T & r, xnumeral_kind & rk, T const & a, xnumeral_kind ak, T const & b,
lean_assert(!is_zero(b, bk)); lean_assert(!is_zero(b, bk));
numeric_traits<T>::reset(r); numeric_traits<T>::reset(r);
rk = XN_NUMERAL; rk = XN_NUMERAL;
} } else if (is_infinite(ak)) {
else if (is_infinite(ak)) {
lean_assert(!is_infinite(bk)); lean_assert(!is_infinite(bk));
if (is_pos(a, ak) == is_pos(b, bk)) if (is_pos(a, ak) == is_pos(b, bk))
rk = XN_PLUS_INFINITY; rk = XN_PLUS_INFINITY;
else else
rk = XN_MINUS_INFINITY; rk = XN_MINUS_INFINITY;
numeric_traits<T>::reset(r); numeric_traits<T>::reset(r);
} } else if (is_infinite(bk)) {
else if (is_infinite(bk)) {
lean_assert(!is_infinite(ak)); lean_assert(!is_infinite(ak));
numeric_traits<T>::reset(r); numeric_traits<T>::reset(r);
rk = XN_NUMERAL; rk = XN_NUMERAL;
} } else {
else {
rk = XN_NUMERAL; rk = XN_NUMERAL;
r = a / b; r = a / b;
} }
@ -200,8 +192,7 @@ template<typename T>
bool eq(T const & a, xnumeral_kind ak, T const & b, xnumeral_kind bk) { bool eq(T const & a, xnumeral_kind ak, T const & b, xnumeral_kind bk) {
if (ak == XN_NUMERAL) { if (ak == XN_NUMERAL) {
return bk == XN_NUMERAL && a == b; return bk == XN_NUMERAL && a == b;
} } else {
else {
return ak == bk; return ak == bk;
} }
} }

6
src/util/sexpr/sexpr.cpp
View file

@ -227,13 +227,11 @@ std::ostream & operator<<(std::ostream & out, sexpr const & s) {
curr = &tail(*curr); curr = &tail(*curr);
if (is_nil(*curr)) { if (is_nil(*curr)) {
break; break;
} } else if (!is_cons(*curr)) {
else if (!is_cons(*curr)) {
out << " . "; out << " . ";
out << *curr; out << *curr;
break; break;
} } else {
else {
out << " "; out << " ";
} }
} }

18
src/util/sexpr/sexpr_funcs.h
View file

@ -30,8 +30,7 @@ sexpr map(sexpr const & l, F f) {
lean_assert(is_list(l)); lean_assert(is_list(l));
if (is_nil(l)) { if (is_nil(l)) {
return l; return l;
} } else {
else {
lean_assert(is_cons(l)); lean_assert(is_cons(l));
return sexpr(f(head(l)), map(tail(l), f)); return sexpr(f(head(l)), map(tail(l), f));
} }
@ -44,8 +43,7 @@ sexpr filter(sexpr const & l, P p) {
lean_assert(is_list(l)); lean_assert(is_list(l));
if (is_nil(l)) { if (is_nil(l)) {
return l; return l;
} } else {
else {
lean_assert(is_cons(l)); lean_assert(is_cons(l));
if (p(head(l))) if (p(head(l)))
return sexpr(head(l), filter(tail(l), p)); return sexpr(head(l), filter(tail(l), p));
@ -61,8 +59,7 @@ T foldl(sexpr const & l, T init, BOP op) {
lean_assert(is_list(l)); lean_assert(is_list(l));
if (is_nil(l)) { if (is_nil(l)) {
return init; return init;
} } else {
else {
lean_assert(is_cons(l)); lean_assert(is_cons(l));
return foldl(tail(l), op(init, head(l)), op); return foldl(tail(l), op(init, head(l)), op);
} }
@ -75,8 +72,7 @@ T foldr(sexpr const & l, T init, BOP op) {
lean_assert(is_list(l)); lean_assert(is_list(l));
if (is_nil(l)) { if (is_nil(l)) {
return init; return init;
} } else {
else {
lean_assert(is_cons(l)); lean_assert(is_cons(l));
return op(head(l), foldr(tail(l), init, op)); return op(head(l), foldr(tail(l), init, op));
} }
@ -89,8 +85,7 @@ bool forall(sexpr const & l, P p) {
lean_assert(is_list(l)); lean_assert(is_list(l));
if (is_nil(l)) { if (is_nil(l)) {
return true; return true;
} } else {
else {
lean_assert(is_cons(l)); lean_assert(is_cons(l));
return p(head(l)) && forall(tail(l), p); return p(head(l)) && forall(tail(l), p);
} }
@ -103,8 +98,7 @@ bool contains(sexpr const & l, P p) {
lean_assert(is_list(l)); lean_assert(is_list(l));
if (is_nil(l)) { if (is_nil(l)) {
return false; return false;
} } else {
else {
lean_assert(is_cons(l)); lean_assert(is_cons(l));
return p(head(l)) || contains(tail(l), p); return p(head(l)) || contains(tail(l), p);
} }