From d0245c4c2f9dfdcc89991ac396e1dfaece2628fb Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Tue, 11 Jul 2017 22:53:18 +0100
Subject: [PATCH] fix(library/vm/vm_int): unformly unbox small ints

---
 src/library/vm/vm_int.cpp | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/library/vm/vm_int.cpp b/src/library/vm/vm_int.cpp
index c6e4b6c5b1..c1b03c081b 100644
--- a/src/library/vm/vm_int.cpp
+++ b/src/library/vm/vm_int.cpp
@@ -27,7 +27,7 @@ inline unsigned to_unsigned(int n) {
 }
 
 inline  int of_unsigned(unsigned n) {
-    return static_cast<int>(n << 1) >> 1;
+    return static_cast<int>(n << 1) / 2;
 }
 
 vm_obj mk_vm_int(int n) {
@@ -100,7 +100,7 @@ vm_obj int_add(vm_obj const & a1, vm_obj const & a2) {
     if (is_simple(a1) && is_simple(a2)) {
         return mk_vm_int(to_small_int(a1) + to_small_int(a2));
     } else {
-        return mk_vm_mpz(to_mpz1(a1) + to_mpz2(a2));
+        return mk_vm_int(to_mpz1(a1) + to_mpz2(a2));
     }
 }
 
@@ -111,7 +111,7 @@ vm_obj int_mul(vm_obj const & a1, vm_obj const & a2) {
             return mk_vm_simple(to_unsigned(r));
         }
     }
-    return mk_vm_mpz(to_mpz1(a1) * to_mpz2(a2));
+    return mk_vm_int(to_mpz1(a1) * to_mpz2(a2));
 }
 
 vm_obj int_quot(vm_obj const & a1, vm_obj const & a2) {
@@ -185,7 +185,7 @@ vm_obj int_land(vm_obj const & a1, vm_obj const & a2) {
     if (LEAN_LIKELY(is_simple(a1) && is_simple(a2))) {
         return mk_vm_int(to_small_int(a1) & to_small_int(a2));
     } else {
-        return mk_vm_mpz(to_mpz1(a1) & to_mpz2(a2));
+        return mk_vm_int(to_mpz1(a1) & to_mpz2(a2));
     }
 }
 
@@ -193,7 +193,7 @@ vm_obj int_lor(vm_obj const & a1, vm_obj const & a2) {
     if (LEAN_LIKELY(is_simple(a1) && is_simple(a2))) {
         return mk_vm_int(to_small_int(a1) | to_small_int(a2));
     } else {
-        return mk_vm_mpz(to_mpz1(a1) | to_mpz2(a2));
+        return mk_vm_int(to_mpz1(a1) | to_mpz2(a2));
     }
 }
 
@@ -201,7 +201,7 @@ vm_obj int_lxor(vm_obj const & a1, vm_obj const & a2) {
     if (LEAN_LIKELY(is_simple(a1) && is_simple(a2))) {
         return mk_vm_int(to_small_int(a1) ^ to_small_int(a2));
     } else {
-        return mk_vm_mpz(to_mpz1(a1) ^ to_mpz2(a2));
+        return mk_vm_int(to_mpz1(a1) ^ to_mpz2(a2));
     }
 }
 
@@ -209,7 +209,7 @@ vm_obj int_lnot(vm_obj const & a) {
     if (LEAN_LIKELY(is_simple(a))) {
         return mk_vm_int(~to_small_int(a));
     } else {
-        return mk_vm_mpz(~to_mpz1(a));
+        return mk_vm_int(~to_mpz1(a));
     }
 }
 
@@ -217,7 +217,7 @@ vm_obj int_ldiff(vm_obj const & a1, vm_obj const & a2) {
     if (LEAN_LIKELY(is_simple(a1) && is_simple(a2))) {
         return mk_vm_int(to_small_int(a1) & ~to_small_int(a2));
     } else {
-        return mk_vm_mpz(to_mpz1(a1) & ~to_mpz2(a2));
+        return mk_vm_int(to_mpz1(a1) & ~to_mpz2(a2));
     }
 }