diff --git a/src/interval/interval_def.h b/src/interval/interval_def.h index bd03d56a4b..37849c65de 100644 --- a/src/interval/interval_def.h +++ b/src/interval/interval_def.h @@ -997,17 +997,12 @@ template void interval::log10() { return; } template void interval::sin() { - if(is_empty()) - return; - *this -= numeric_traits::pi_half_lower(); cos(); lean_assert(check_invariant()); return; } template void interval::cos () { - if(is_empty()) - return; if(m_lower_inf || m_upper_inf) { // cos([-oo, c]) = [-1.0, +1.0] // cos([c, +oo]) = [-1.0, +1.0] @@ -1069,9 +1064,45 @@ template void interval::cos () { m_upper = 1.0; lean_assert(check_invariant()); return; - } +} + +template void interval::tan() { + if(m_lower_inf || m_upper_inf) { + // tan([-oo, c]) = [-oo, +oo] + // tan([c, +oo]) = [-oo, +oo] + numeric_traits::reset(m_lower); + numeric_traits::reset(m_upper); + m_lower_open = m_upper_open = true; + m_lower_inf = m_upper_inf = true; + lean_assert(check_invariant()); + return; + } + + T const pi = numeric_traits::pi(); + T const pi_half_lower = numeric_traits::pi_half_lower(); + T const pi_half_upper = numeric_traits::pi_half_upper(); + fmod(pi); + + if (m_lower >= pi_half_lower) { + *this -= pi; + } + if (m_lower <= - pi_half_lower || m_upper >= pi_half_lower) { + numeric_traits::reset(m_lower); + numeric_traits::reset(m_upper); + m_lower_open = m_upper_open = true; + m_lower_inf = m_upper_inf = true; + lean_assert(check_invariant()); + return; + } else { + numeric_traits::set_rounding(false); + numeric_traits::tan(m_lower); + numeric_traits::set_rounding(true); + numeric_traits::tan(m_upper); + lean_assert(check_invariant()); + return; + } +} -template void interval::tan () { /* TODO */ lean_unreachable(); return; } template void interval::sec () { /* TODO */ lean_unreachable(); return; } template void interval::csc () { /* TODO */ lean_unreachable(); return; } template void interval::cot () { /* TODO */ lean_unreachable(); return; }