Add numeric_traits

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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)

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; }
+};
+
 }

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; }
+};
+
 }

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; }
+};
+
 }

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); }
+};
+
+}