From f1d931252110fe806d85c50c38752dd6cd78b975 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 18 Oct 2013 14:41:18 -0700
Subject: [PATCH] feat(numerics/zpz): add numeric_traits for zpz numerals

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/util/numerics/power.h |  5 +++--
 src/util/numerics/zpz.cpp |  5 +++++
 src/util/numerics/zpz.h   | 17 +++++++++++++++++
 3 files changed, 25 insertions(+), 2 deletions(-)

diff --git a/src/util/numerics/power.h b/src/util/numerics/power.h
index ce8d94a0a..fbc28dab8 100644
--- a/src/util/numerics/power.h
+++ b/src/util/numerics/power.h
@@ -12,8 +12,9 @@ namespace lean {
 template<typename T>
 T power(T const & a, unsigned k) {
     unsigned mask = 1;
-    T power = a;
-    T b     = 1;
+    T power(a);
+    T b(a);
+    b = 1;
     while (mask <= k) {
         if (mask & k)
             b *= power;
diff --git a/src/util/numerics/zpz.cpp b/src/util/numerics/zpz.cpp
index ae175479b..27dbd9e99 100644
--- a/src/util/numerics/zpz.cpp
+++ b/src/util/numerics/zpz.cpp
@@ -18,4 +18,9 @@ void zpz::inv() {
     gcdext(g, a, b, static_cast<int64>(m_value), static_cast<int64>(m_p));
     m_value = remainder(a, static_cast<int64>(m_p));
 }
+
+static zpz g_zero;
+zpz const & numeric_traits<zpz>::zero() {
+    return g_zero;
+}
 }
diff --git a/src/util/numerics/zpz.h b/src/util/numerics/zpz.h
index 7b41ef562..80261f0e7 100644
--- a/src/util/numerics/zpz.h
+++ b/src/util/numerics/zpz.h
@@ -9,6 +9,8 @@ Author: Leonardo de Moura
 #include "util/int64.h"
 #include "util/numerics/remainder.h"
 #include "util/numerics/primes.h"
+#include "util/numerics/power.h"
+#include "util/numerics/numeric_traits.h"
 
 namespace lean {
 /**
@@ -98,4 +100,19 @@ public:
 
     friend std::ostream & operator<<(std::ostream & out, zpz const & z) { out << z.m_value; return out; }
 };
+
+template<>
+class numeric_traits<zpz> {
+public:
+    static bool precise() { return true; }
+    static bool is_zero(zpz const & v) { return v == 0; }
+    static bool is_pos(zpz const & v)  { return v > 0; }
+    static bool is_neg(zpz const & )  { return false; }
+    static void set_rounding(bool ) {}
+    static void neg(zpz & v)   { v.neg(); }
+    static void reset(zpz & v) { v = 0; }
+    // v <- v^k
+    static void power(zpz & v, unsigned k) { v = lean::power(v, k); }
+    static zpz const & zero();
+};
 }