From b970c964ff9c5277766708c56bf893300dbd800f Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Wed, 7 Aug 2013 19:30:38 -0700
Subject: [PATCH] Add transcendental functions to interval (still need to fill
 more...)

---
 src/interval/interval_def.h     | 141 ++++++++++++++++++++++++++++++++
 src/tests/interval/interval.cpp |   4 +-
 2 files changed, 143 insertions(+), 2 deletions(-)

diff --git a/src/interval/interval_def.h b/src/interval/interval_def.h
index 28fcda1ba..e9cbcc04c 100644
--- a/src/interval/interval_def.h
+++ b/src/interval/interval_def.h
@@ -756,5 +756,146 @@ void interval<T>::display(std::ostream & out) const {
     out << (m_upper_open ? ")" : "]");
 }
 
+template<typename T> void interval<T>::exp  () {
+    if(is_empty())
+        return;
+    if(m_lower_inf) {
+        numeric_traits<T>::reset(m_lower);
+    } else {
+        numeric_traits<T>::set_rounding(false);
+        numeric_traits<T>::exp(m_lower);
+    }
+    if(m_upper_inf) {
+        // Nothing to do
+    } else {
+        numeric_traits<T>::set_rounding(true);
+        numeric_traits<T>::exp(m_upper);
+    }
+    lean_assert(check_invariant());
+    return;
+}
+template<typename T> void interval<T>::exp2 () {
+    if(is_empty())
+        return;
+    if(m_lower_inf) {
+        numeric_traits<T>::reset(m_lower);
+    } else {
+        numeric_traits<T>::set_rounding(false);
+        numeric_traits<T>::exp2(m_lower);
+    }
+    if(m_upper_inf) {
+        // Nothing to do
+    } else {
+        numeric_traits<T>::set_rounding(true);
+        numeric_traits<T>::exp2(m_upper);
+    }
+    lean_assert(check_invariant());
+    return;
+}
+template<typename T> void interval<T>::exp10() {
+    if(is_empty())
+        return;
+    if(m_lower_inf) {
+        numeric_traits<T>::reset(m_lower);
+    } else {
+        numeric_traits<T>::set_rounding(false);
+        numeric_traits<T>::exp10(m_lower);
+    }
+    if(m_upper_inf) {
+        // Nothing to do
+    } else {
+        numeric_traits<T>::set_rounding(true);
+        numeric_traits<T>::exp10(m_upper);
+    }
+    lean_assert(check_invariant());
+    return;
+}
+template<typename T> void interval<T>::log  () {
+    if(is_empty())
+        return;
+    if(is_N0()) {
+        set_empty();
+        return;
+    }
+    if(is_lower_pos()) {
+        numeric_traits<T>::set_rounding(false);
+        numeric_traits<T>::log(m_lower);
+    } else {
+        numeric_traits<T>::reset(m_lower);
+        m_lower_inf = true;
+    }
+    if(m_upper_inf) {
+        // Nothing to do
+    } else {
+        numeric_traits<T>::set_rounding(true);
+        numeric_traits<T>::log(m_upper);
+    }
+    lean_assert(check_invariant());
+    return;
+}
+template<typename T> void interval<T>::log2 () {
+    if(is_empty())
+        return;
+    if(is_N0()) {
+        set_empty();
+        return;
+    }
+    if(is_lower_pos()) {
+        numeric_traits<T>::set_rounding(false);
+        numeric_traits<T>::log2(m_lower);
+    } else {
+        numeric_traits<T>::reset(m_lower);
+        m_lower_inf = true;
+    }
+    if(m_upper_inf) {
+        // Nothing to do
+    } else {
+        numeric_traits<T>::set_rounding(true);
+        numeric_traits<T>::log2(m_upper);
+    }
+    lean_assert(check_invariant());
+    return;
+}
+template<typename T> void interval<T>::log10() {
+    if(is_empty())
+        return;
+    if(is_N0()) {
+        set_empty();
+        return;
+    }
+    if(is_lower_pos()) {
+        numeric_traits<T>::set_rounding(false);
+        numeric_traits<T>::log10(m_lower);
+    } else {
+        numeric_traits<T>::reset(m_lower);
+        m_lower_inf = true;
+    }
+    if(m_upper_inf) {
+        // Nothing to do
+    } else {
+        numeric_traits<T>::set_rounding(true);
+        numeric_traits<T>::log10(m_upper);
+    }
+    lean_assert(check_invariant());
+    return;
+}
+template<typename T> void interval<T>::sin  () {
+    *this -= numeric_traits<T>::pi_half_lower();
+    cos();
+}
+template<typename T> void interval<T>::cos  () { /* TODO */ lean_unreachable(); return; }
+template<typename T> void interval<T>::tan  () { /* TODO */ lean_unreachable(); return; }
+template<typename T> void interval<T>::sec  () { /* TODO */ lean_unreachable(); return; }
+template<typename T> void interval<T>::csc  () { /* TODO */ lean_unreachable(); return; }
+template<typename T> void interval<T>::cot  () { /* TODO */ lean_unreachable(); return; }
+template<typename T> void interval<T>::asin () { /* TODO */ lean_unreachable(); return; }
+template<typename T> void interval<T>::acos () { /* TODO */ lean_unreachable(); return; }
+template<typename T> void interval<T>::atan () { /* TODO */ lean_unreachable(); return; }
+template<typename T> void interval<T>::sinh () { /* TODO */ lean_unreachable(); return; }
+template<typename T> void interval<T>::cosh () { /* TODO */ lean_unreachable(); return; }
+template<typename T> void interval<T>::tanh () { /* TODO */ lean_unreachable(); return; }
+template<typename T> void interval<T>::asinh() { /* TODO */ lean_unreachable(); return; }
+template<typename T> void interval<T>::acosh() { /* TODO */ lean_unreachable(); return; }
+template<typename T> void interval<T>::atanh() { /* TODO */ lean_unreachable(); return; }
 
 }
diff --git a/src/tests/interval/interval.cpp b/src/tests/interval/interval.cpp
index e1f5ad491..c8ae903ec 100644
--- a/src/tests/interval/interval.cpp
+++ b/src/tests/interval/interval.cpp
@@ -9,10 +9,12 @@ Author: Leonardo de Moura
 #include "test.h"
 #include "trace.h"
 #include "mpq.h"
+#include "mpfp.h"
 using namespace lean;
 
 typedef interval<mpq> qi;
 typedef interval<double> di;
+typedef interval<mpfp> fi;
 typedef std::vector<qi> qiv;
 
 qiv mk_some_intervals(int low, int hi) {
@@ -91,8 +93,6 @@ static void tst3() {
     std::cout << "power(" << i1 << ", 3) = " << power(i1, 3) << std::endl;
     std::cout << "exp(" << i1 << ") = "      << exp(i1) << std::endl;
     std::cout << "log(" << i1 << ") = "      << log(i1) << std::endl;
-    std::cout << "sin(" << i1 << ") = "      << sin(i1) << std::endl;
-    std::cout << "cos(" << i1 << ") = "      << cos(i1) << std::endl;
 }
 
 int main() {