Add abs/floor/ceil to double/float/mpq/mpfp

src/util/numerics/double.cpp

@@ -13,7 +13,7 @@ namespace lean {
 static thread_local mpfr_rnd_t g_rnd;
 
 void set_double_rnd(bool plus_inf) {
-    g_rnd = plus_inf ? MPFR_RNDU : MPFR_RNDD; 
+    g_rnd = plus_inf ? MPFR_RNDU : MPFR_RNDD;
 }
 
 
@@ -21,7 +21,10 @@ mpfr_rnd_t get_double_rnd() {
     return g_rnd;
 }
 
-void double_power(double & v, unsigned k) {
-    v = std::pow(v, k);
-}
+void double_power(double & v, unsigned k) { v = std::pow(v, k); }
+void double_abs(double & v)   { v = std::abs(v); }
+void double_ceil(double & v)  { v = std::ceil(v); }
+void double_floor(double & v) { v = std::floor(v); }
+
+
 };

src/util/numerics/double.h

@@ -15,6 +15,9 @@ namespace lean {
    numeric types.
 */
 void double_power(double & v, unsigned k);
+void double_abs(double & v);
+void double_ceil(double & v);
+void double_floor(double & v);
 
 // Macro to implement transcendental functions using MPFR
 #define LEAN_TRANS_DOUBLE_FUNC(f, v, rnd)              \
@@ -38,8 +41,17 @@ public:
     static void neg(double & v) { v = -v; }
     static void inv(double & v) { v = 1.0/v; }
     static void reset(double & v) { v = 0.0; }
-    // v <- v^k
+
     static void power(double & v, unsigned k) { double_power(v, k); }
+    static void abs(double & v) { double_abs(v); }
+    static void ceil(double & v) { double_ceil(v); }
+    static void floor(double & v) { double_floor(v); }
+    static double const & min(double const & v1, double const & v2) {
+        return v1 < v2 ? v1 : v2;
+    }
+    static double const & max(double const & v1, double const & v2) {
+        return v1 > v2 ? v1 : v2;
+    }
 
     // constants
     static const  double constexpr pi_l = (3373259426.0 + 273688.0 / (1<<21)) / (1<<30);

src/util/numerics/float.cpp

@@ -12,7 +12,9 @@ namespace lean {
 
 thread_local mpfr_rnd_t numeric_traits<float>::rnd = MPFR_RNDN;
 
-void float_power(double & v, unsigned k) {
-    v = std::pow(v, k);
-}
+void float_power(float & v, unsigned k) { v = std::pow(v, k); }
+void float_abs(float & v)   { v = std::abs(v); }
+void float_ceil(float & v)  { v = std::ceil(v); }
+void float_floor(float & v) { v = std::floor(v); }
+
 };

src/util/numerics/float.h

@@ -15,6 +15,9 @@ namespace lean {
    numeric types.
 */
 void float_power(float & v, unsigned k);
+void float_abs(float & v);
+void float_ceil(float & v);
+void float_floor(float & v);
 
 // Macro to implement transcendental functions using MPFR
 #define LEAN_TRANS_FLOAT_FUNC(f, v, rnd)        \
@@ -35,8 +38,18 @@ public:
     static void neg(float & v) { v = -v; }
     static void inv(float & v) { v = 1.0/v; }
     static void reset(float & v) { v = 0.0; }
-    // v <- v^k
+
     static void power(float & v, unsigned k) { float_power(v, k); }
+    static void abs(float & v) { float_abs(v); }
+    static void ceil(float & v) { float_ceil(v); }
+    static void floor(float & v) { float_floor(v); }
+
+    static float const & min(float const & v1, float const & v2) {
+        return v1 < v2 ? v1 : v2;
+    }
+    static float const & max(float const & v1, float const & v2) {
+        return v1 > v2 ? v1 : v2;
+    }
 
     // constants
     static const  float constexpr pi_l = 13176794.0f/(1<<22);

src/util/numerics/mpfp.h

@@ -502,10 +502,13 @@ public:
     static bool is_neg(mpfp const & v) { return v.is_neg(); }
     static void set_rounding(bool plus_inf) { set_mpfp_rnd(plus_inf); }
     static void neg(mpfp & v) { v.neg(); }
-//    static void inv(mpfp & v) { v.inv(); }
+    static void inv(mpfp & v) { v.inv(); }
     static void reset(mpfp & v) { v = 0.0; }
     // v <- v^k
     static void power(mpfp & v, unsigned k) { v.pow(k); }
+    static void abs(mpfp & v) { v.abs(); }
+    static void ceil(mpfp & v) { v.ceil(); }
+    static void floor(mpfp & v) { v.floor(); }
 
     // constants
     static mpfp pi_l;

src/util/numerics/mpq.h

@@ -221,8 +221,11 @@ public:
     static void neg(mpq & v) { v.neg(); }
     static void inv(mpq & v) { v.inv(); }
     static void reset(mpq & v) { v = 0; }
-    // v <- v^k
+
     static void power(mpq & v, unsigned k) { _power(v, v, k); }
+    static void abs(mpq & v) { v.abs(); }
+    static void ceil(mpq & v) { v.ceil(); }
+    static void floor(mpq & v) { v.floor(); }
 
     // constants
     static const  mpq pi_l;