From 7dbd87e382b25cae09f8fa3989514f9c762e3a3f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 18 Jul 2013 17:39:44 -0700
Subject: [PATCH] Add numeric_traits

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/numerics/CMakeLists.txt   |  2 +-
 src/numerics/mpbq.h           | 11 +++++++++++
 src/numerics/mpq.h            | 12 ++++++++++++
 src/numerics/mpz.h            | 12 ++++++++++++
 src/numerics/numeric_traits.h | 32 ++++++++++++++++++++++++++++++++
 5 files changed, 68 insertions(+), 1 deletion(-)
 create mode 100644 src/numerics/numeric_traits.h

diff --git a/src/numerics/CMakeLists.txt b/src/numerics/CMakeLists.txt
index f7b25f1305..10131dce81 100644
--- a/src/numerics/CMakeLists.txt
+++ b/src/numerics/CMakeLists.txt
@@ -1 +1 @@
-add_library(numerics gmp_init.cpp mpz.cpp mpq.cpp mpbq.cpp)
+add_library(numerics gmp_init.cpp mpz.cpp mpq.cpp mpbq.cpp numeric_traits.cpp)
diff --git a/src/numerics/mpbq.h b/src/numerics/mpbq.h
index 63cba376f5..5eaf44383c 100644
--- a/src/numerics/mpbq.h
+++ b/src/numerics/mpbq.h
@@ -243,4 +243,15 @@ public:
     };
 };
 
+template<>
+class numeric_traits<mpbq> {
+public:
+    static bool is_zero(mpbq const &  v) { return v.is_zero(); }
+    static bool is_pos(mpbq const & v) { return v.is_pos(); }
+    static bool is_neg(mpbq const & v) { return v.is_neg(); }
+    static void set_rounding(bool plus_inf) {}
+    static void neg(mpbq & v) { v.neg(); }
+    static void reset(mpbq & v) { v = 0; }
+};
+
 }
diff --git a/src/numerics/mpq.h b/src/numerics/mpq.h
index cd7ec5aa4a..654ba934ca 100644
--- a/src/numerics/mpq.h
+++ b/src/numerics/mpq.h
@@ -208,4 +208,16 @@ public:
 
 };
 
+template<>
+class numeric_traits<mpq> {
+public:
+    static bool is_zero(mpq const &  v) { return v.is_zero(); }
+    static bool is_pos(mpq const & v) { return v.is_pos(); }
+    static bool is_neg(mpq const & v) { return v.is_neg(); }
+    static void set_rounding(bool plus_inf) {}
+    static void neg(mpq & v) { v.neg(); }
+    static void inv(mpq & v) { v.inv(); }
+    static void reset(mpq & v) { v = 0; }
+};
+
 }
diff --git a/src/numerics/mpz.h b/src/numerics/mpz.h
index ddd3259d1c..18825ebb04 100644
--- a/src/numerics/mpz.h
+++ b/src/numerics/mpz.h
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <iostream>
 #include <gmp.h>
 #include "debug.h"
+#include "numeric_traits.h"
 
 namespace lean {
 class mpq;
@@ -217,4 +218,15 @@ public:
     friend std::ostream & operator<<(std::ostream & out, mpz const & v); 
 };
 
+template<>
+class numeric_traits<mpz> {
+public:
+    static bool is_zero(mpz const & v) { return v.is_zero(); }
+    static bool is_pos(mpz const & v) { return v.is_pos(); }
+    static bool is_neg(mpz const & v) { return v.is_neg(); }
+    static void set_rounding(bool plus_inf) {}
+    static void neg(mpz & v) { v.neg(); }
+    static void reset(mpz & v) { v = 0; }
+};
+
 }
diff --git a/src/numerics/numeric_traits.h b/src/numerics/numeric_traits.h
new file mode 100644
index 0000000000..214f5e71b4
--- /dev/null
+++ b/src/numerics/numeric_traits.h
@@ -0,0 +1,32 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved. 
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura 
+*/
+#pragma once
+
+namespace lean {
+
+template<typename T>
+class numeric_traits {
+};
+
+void set_processor_rounding(bool plus_inf);
+void double_power(double & v, unsigned k);
+
+template<>
+class numeric_traits<double> {
+public:
+    static bool is_zero(double v) { return v == 0.0; }
+    static bool is_pos(double v) { return v > 0.0; }
+    static bool is_neg(double v) { return v < 0.0; }
+    static void set_rounding(bool plus_inf) { set_processor_rounding(plus_inf); }
+    static void neg(double & v) { v = -v; }
+    static void inv(double & v) { v = 1.0/v; }
+    static void reset(double & v) { v = 0.0; }
+    // b <- b^k
+    static void power(double & v, unsigned k) { double_power(v, k); }
+};
+
+}