From 09771fd24fd53331ff1997e7b8ec8f44ee378571 Mon Sep 17 00:00:00 2001
From: Max Horn <max@quendi.de>
Date: Tue, 22 Aug 2023 15:57:57 +0200
Subject: [PATCH] Add type `NegInf` representing negative infinity

Also expand the functionality of `PosInf` to match.
---
 src/HeckeMiscInfinity.jl       | 120 ++++++++++++++++++++++++++-------
 src/HeckeMiscInteger.jl        |   9 ---
 src/arb/arb.jl                 |   2 +
 src/flint/fmpq.jl              |   9 +++
 src/flint/fmpz.jl              |   4 ++
 test/HeckeMiscInfinity-test.jl | 103 ++++++++++++++++++----------
 test/arb/arb-test.jl           |   6 ++
 test/flint/fmpq-test.jl        |  20 +++++-
 test/flint/fmpz-test.jl        |  37 +++++++---
 9 files changed, 231 insertions(+), 79 deletions(-)

diff --git a/src/HeckeMiscInfinity.jl b/src/HeckeMiscInfinity.jl
index 93a1156d2..4ab7eff0b 100644
--- a/src/HeckeMiscInfinity.jl
+++ b/src/HeckeMiscInfinity.jl
@@ -1,57 +1,106 @@
-export PosInf, inf, IntExt, is_infinite
+export PosInf, NegInf, inf, IntExt, is_infinite
 
-# This is a type for positive infinity for use in valuations.
+"""
+    PosInf
+
+This singleton type represents positive infinity, as in: a value larger
+than any real number. For use in valuations and elsewhere.
 
+See [`NegInf`](@ref).
+"""
 struct PosInf
 end
 
-const inf = PosInf()
+"""
+    NegInf
+
+This singleton type represents negative infinity, as in: a value smaller
+than any real number. For use in valuations and elsewhere.
+
+See [`PosInf`](@ref).
+"""
+struct NegInf
+end
+
+# type union for convenience later on
+const AnyInf = Union{PosInf,NegInf}
 
-+(::Int, ::PosInf) = inf
+# another convenience type union
+# TODO: maybe deprecate this one, or at least rename it; the current one seems
+# somewhat arbitrary now that we also have negative infinity
+const IntExt = Union{Int,PosInf}
 
-+(::PosInf, ::Int) = inf
+const inf = PosInf() # TODO: for backwards compatibility; deprecate?
 
-+(::PosInf, ::PosInf) = inf
+#const infinity = PosInf()  # FIXME: can't have this as we already have `infinity(C::CalciumField)`
 
--(::PosInf, ::Int) = inf
+########################################
+#
+# basics
+#
+########################################
 
-Base.max(::Int, ::PosInf) = inf
+# match the hash values of Inf and -Inf, as we also compare equal to them
+Base.hash(::PosInf, h::UInt) = hash(Inf, h)
+Base.hash(::NegInf, h::UInt) = hash(-Inf, h)
 
-Base.max(::PosInf, ::Int) = inf
+Base.show(io::IO, ::PosInf) = print(io, "infinity") # FIXME: if we can't have `infinity` as a global, maybe better print as `inf`???
+Base.show(io::IO, ::NegInf) = print(io, "-infinity")
 
-Base.isless(::Int, ::PosInf) = true
+Base.one(::AnyInf) = 1
+Base.zero(::AnyInf) = 0
 
-Base.isless(x::Rational{Int}, ::PosInf) = denominator(x) != 0
+########################################
 
-Base.isless(::PosInf, ::PosInf) = false
+Base.signbit(::PosInf) = false
+Base.signbit(::NegInf) = true
 
-Base.isless(::PosInf, ::Int) = false
+Base.sign(::Type{Int}, ::PosInf) = +1
+Base.sign(::Type{Int}, ::NegInf) = -1
 
-Base.isless(::PosInf, ::Rational{Int}) = false
+########################################
+#
+# comparison
+#
+########################################
 
-Base.isfinite(::PosInf) = false
+Base.:(==)(inf1::AnyInf, inf2::AnyInf) = signbit(inf1) == signbit(inf2)
+Base.:(==)(x::AnyInf, y::Real) = isinf(y) && signbit(y) == signbit(x)
+Base.:(==)(y::Real, x::AnyInf) = x == y
 
-Base.isinf(::PosInf) = true
 
-Base.isone(::PosInf) = false
+Base.isless(x::Real, ::PosInf) = isfinite(x) || signbit(x)
+Base.isless(::PosInf, ::Real) = false
 
-Base.iszero(::PosInf) = false
+Base.isless(::Real, ::NegInf) = false
+Base.isless(::NegInf, x::Real) = isfinite(x) || !signbit(x)
 
-Base.one(::PosInf) = 1
+Base.isless(inf1::AnyInf, inf2::AnyInf) = signbit(inf1) && !signbit(inf2)
 
-Base.zero(::PosInf) = 0
 
-Base.isless(::PosInf, ::ZZRingElem) = false
+Base.isless(::PosInf, ::Union{ZZRingElem,QQFieldElem}) = false
+Base.isless(::Union{ZZRingElem,QQFieldElem}, ::PosInf) = true
 
-Base.isless(::ZZRingElem, ::PosInf) = true
+Base.isless(::NegInf, ::Union{ZZRingElem,QQFieldElem}) = true
+Base.isless(::Union{ZZRingElem,QQFieldElem}, ::NegInf) = false
 
-Base.isless(::PosInf, ::QQFieldElem) = false
+########################################
+#
+# other predicates
+#
+########################################
 
-Base.isless(::QQFieldElem, ::PosInf) = true
+Base.isfinite(::AnyInf) = false
+Base.isinf(::AnyInf) = true
 
-const IntExt = Union{Int,PosInf}
+Base.isone(::AnyInf) = false
+Base.iszero(::AnyInf) = false
 
 is_positive(::PosInf) = true
+is_positive(::NegInf) = false
+
+is_negative(::PosInf) = false
+is_negative(::NegInf) = true
 
 @doc raw"""
     is_infinite(x::Any) -> Bool
@@ -59,3 +108,24 @@ is_positive(::PosInf) = true
 Tests whether $x$ is infinite, by returning `!isfinite(x)`.
 """
 is_infinite(x::Any) = !isfinite(x)
+# TODO: should is_infinite become a synonym for `isinf` ???
+# TODO: this description is problematic for approximate types
+
+########################################
+#
+# arithmetic
+#
+########################################
+
+# unary minus
+Base.:-(::PosInf) = NegInf()
+Base.:-(::NegInf) = inf
+
+# binary operations
+Base.:+(::IntegerUnion, inf::AnyInf) = inf
+Base.:+(inf::AnyInf, ::IntegerUnion) = inf
+Base.:+(inf1::AnyInf, inf2::AnyInf) = signbit(inf1) == signbit(inf2) ? inf1 : error("inf - inf is undefined")
+
+Base.:-(inf::AnyInf, ::IntegerUnion) = inf
+Base.:-(::IntegerUnion, inf::AnyInf) = -inf
+Base.:-(inf1::AnyInf, inf2::AnyInf) = inf1 + (-inf2)
diff --git a/src/HeckeMiscInteger.jl b/src/HeckeMiscInteger.jl
index 8f978623b..c52599c78 100644
--- a/src/HeckeMiscInteger.jl
+++ b/src/HeckeMiscInteger.jl
@@ -253,15 +253,6 @@ function nbits(a::Integer)
     return ndigits(a, base=2)
 end
 
-@doc raw"""
-    isinteger(a::QQFieldElem) -> Bool
-
-Returns `true` iff the denominator of $a$ is one.
-"""
-function isinteger(a::QQFieldElem)
-    return isone(denominator(a))
-end
-
 function (::ZZRing)(x::Rational{Int})
     @assert denominator(x) == 1
     return ZZRingElem(numerator(x))
diff --git a/src/arb/arb.jl b/src/arb/arb.jl
index beac63f0a..464264282 100644
--- a/src/arb/arb.jl
+++ b/src/arb/arb.jl
@@ -638,6 +638,8 @@ function sign(::Type{Int}, x::arb)
   end
 end
 
+Base.signbit(x::arb) = signbit(sign(Int, x))
+
 ################################################################################
 #
 #  Unary operations
diff --git a/src/flint/fmpq.jl b/src/flint/fmpq.jl
index 49a081f24..b8fcba8b3 100644
--- a/src/flint/fmpq.jl
+++ b/src/flint/fmpq.jl
@@ -99,6 +99,8 @@ sign(a::QQFieldElem) = QQFieldElem(sign(numerator(a)))
 
 sign(::Type{Int}, a::QQFieldElem) = sign(Int, numerator(a))
 
+Base.signbit(a::QQFieldElem) = signbit(sign(Int, a))
+
 function abs(a::QQFieldElem)
    z = QQFieldElem()
    ccall((:fmpq_abs, libflint), Nothing, (Ref{QQFieldElem}, Ref{QQFieldElem}), z, a)
@@ -124,6 +126,13 @@ end
 
 is_unit(a::QQFieldElem) = !iszero(a)
 
+isinteger(a::QQFieldElem) = isone(denominator(a))
+
+isfinite(::QQFieldElem) = true
+
+isinf(::QQFieldElem) = false
+
+
 @doc raw"""
     height(a::QQFieldElem)
 
diff --git a/src/flint/fmpz.jl b/src/flint/fmpz.jl
index 21dba7a95..13bfd0f5a 100644
--- a/src/flint/fmpz.jl
+++ b/src/flint/fmpz.jl
@@ -179,6 +179,8 @@ sign(a::ZZRingElem) = ZZRingElem(ccall((:fmpz_sgn, libflint), Cint, (Ref{ZZRingE
 
 sign(::Type{Int}, a::ZZRingElem) = Int(ccall((:fmpz_sgn, libflint), Cint, (Ref{ZZRingElem},), a))
 
+Base.signbit(a::ZZRingElem) = signbit(sign(Int, a))
+
 @doc raw"""
     fits(::Type{Int}, a::ZZRingElem)
 
@@ -218,6 +220,8 @@ isinteger(::ZZRingElem) = true
 
 isfinite(::ZZRingElem) = true
 
+isinf(::ZZRingElem) = false
+
 @doc raw"""
     denominator(a::ZZRingElem)
 
diff --git a/test/HeckeMiscInfinity-test.jl b/test/HeckeMiscInfinity-test.jl
index a3358e5e2..5a87b6025 100644
--- a/test/HeckeMiscInfinity-test.jl
+++ b/test/HeckeMiscInfinity-test.jl
@@ -1,57 +1,88 @@
-@testset "PosInf basics" begin
+@testset "Inf basics" begin
 
     @test inf === PosInf()
+    @test -inf === NegInf()
+    @test -(-inf) === inf
 
     @test zero(inf) === 0
     @test one(inf) === 1
 
-end
+    @test zero(-inf) === 0
+    @test one(-inf) === 1
 
-@testset "PosInf arithmetic" begin
+    @test sign(Int, inf) === +1
+    @test sign(Int, -inf) === -1
 
-    @test inf + inf === inf
-    @test inf + 1 === inf
-    @test inf - 1 === inf
-    @test 1 + inf === inf
+    @test !signbit(inf)
+    @test signbit(-inf)
 
 end
 
-@testset "PosInf comparisons" begin
-
-    @test max(inf, inf) === inf
-    @test max(inf, 1) === inf
-    @test max(1, inf) === inf
-
-    @test 1 < inf
-    @test !(inf < 1)
-
-    @test ZZ(1) < inf
-    @test !(inf < ZZ(1))
+@testset "Inf arithmetic" begin
 
-    @test 1 // 2 < inf
-    @test !(inf < 1 // 2)
-
-    @test QQ(1 // 2) < inf
-    @test !(inf < QQ(1 // 2))
-
-    # one positive infinity is not less than infinity (though that does
-    # not necessarily mean that they are equal either)
-    @test !(inf < inf)
+    @test inf + inf === inf
+    @test inf - -inf === inf
+    @test -inf + -inf === -inf
+    @test -inf - inf === -inf
+
+    @test_throws ErrorException inf - inf
+    @test_throws ErrorException (-inf) - (-inf)
+
+    @testset "... with type $(typeof(x))" for x in [1, ZZ(1)]
+        @test inf + x === inf
+        @test x + inf === inf
+        @test inf - x === inf
+        @test x - inf === -inf
+
+        @test -inf + x === -inf
+        @test x + -inf === -inf
+        @test -inf - x === -inf
+        @test x - (-inf) === inf
+    end
+end
 
-    @test !(inf < 1 // 0)
-    @test !(1 // 0 < inf)
+@testset "Inf comparisons" begin
+
+    @testset "... against $x" for x in (1, ZZ(1), 1//2, QQ(1//2))
+        # we verify the following three objects are in the correct
+        # order with respect to isless and various other operations
+        ord = [ -inf, x, inf ]
+        for i in 1:length(ord), j in 1:length(ord)
+            @test min(ord[i], ord[j]) === ord[min(i, j)]
+            @test max(ord[i], ord[j]) === ord[max(i, j)]
+            @test isless(ord[i], ord[j]) === isless(i, j)
+            @test (ord[i] < ord[j]) === (i < j)
+            @test (ord[i] <= ord[j]) === (i <= j)
+            @test (ord[i] == ord[j]) === (i == j)
+        end
+    end
+
+    # verify that no positive infinity is less than any other
+    eqs = [ Inf, inf, 1//0 ]
+    for i in 1:length(eqs), j in 1:length(eqs)
+        @test !(eqs[i] < eqs[j])
+    end
+
+    # verify that no negative infinity is less than any other
+    eqs = [ -Inf, -inf, -1//0 ]
+    for i in 1:length(eqs), j in 1:length(eqs)
+        @test !(eqs[i] < eqs[j])
+    end
 
 end
 
-@testset "PosInf predicates" begin
+@testset "Inf predicates for $x" for x in [inf, -inf]
 
-    @test !isone(inf)
-    @test !isfinite(inf)
-    @test !iszero(inf)
+    @test !isone(x)
+    @test !isfinite(x)
+    @test !iszero(x)
 
-    @test isinf(inf)
-    @test is_infinite(inf)
-    @test is_positive(inf)
+    @test isinf(x)
+    @test is_infinite(x)
+    @test is_positive(x) == !signbit(x)
+    @test is_positive(x) == (x > 0)
+    @test is_negative(x) == signbit(x)
+    @test is_negative(x) == (x < 0)
 
 end
 
diff --git a/test/arb/arb-test.jl b/test/arb/arb-test.jl
index 4e1021c3c..dc48962d3 100644
--- a/test/arb/arb-test.jl
+++ b/test/arb/arb-test.jl
@@ -281,6 +281,12 @@ end
    b, i = unique_integer(RRR(2)^1000);
    b, i = unique_integer(RRR(2)^1000);
    b, i = unique_integer(RRR(2)^1000);
+
+   @test sign(Int, RR(2)) == 1
+   @test sign(Int, -RR(2)) == -1
+
+   @test !signbit(RR(2))
+   @test signbit(-RR(2))
 end
 
 @testset "arb.unsafe_ops" begin
diff --git a/test/flint/fmpq-test.jl b/test/flint/fmpq-test.jl
index 035f15f0e..82a2cb41c 100644
--- a/test/flint/fmpq-test.jl
+++ b/test/flint/fmpq-test.jl
@@ -132,13 +132,31 @@ end
    @test sign(Int, QQFieldElem()) == 0
    @test sign(Int, QQFieldElem(1, 7)) == 1
 
+   @test signbit(QQFieldElem(-2, 3))
+   @test !signbit(QQFieldElem())
+   @test !signbit(QQFieldElem(1, 7))
+
+   @test !isone(zero(R))
    @test isone(one(R))
 
    @test iszero(zero(R))
+   @test !iszero(one(R))
 
    @test is_unit(one(R))
-
    @test is_unit(QQFieldElem(1, 3))
+   @test !is_unit(QQFieldElem(0, 3))
+
+   @test isinteger(zero(R))
+   @test isinteger(one(R))
+   @test !isinteger(QQFieldElem(1, 3))
+
+   @test isfinite(zero(R))
+   @test isfinite(one(R))
+   @test isfinite(QQFieldElem(1, 3))
+
+   @test !isinf(zero(R))
+   @test !isinf(one(R))
+   @test !isinf(QQFieldElem(1, 3))
 
    @test deepcopy(QQFieldElem(2, 3)) == QQFieldElem(2, 3)
 
diff --git a/test/flint/fmpz-test.jl b/test/flint/fmpz-test.jl
index 8b91a4783..a9c3d4fda 100644
--- a/test/flint/fmpz-test.jl
+++ b/test/flint/fmpz-test.jl
@@ -143,15 +143,21 @@ end
    b = zero(ZZRing())
    c = zero(ZZRingElem)
 
-   @test isa(a, RingElem)
-
-   @test isa(b, RingElem)
-
-   @test isa(c, RingElem)
+   @test isa(a, ZZRingElem)
+   @test isa(b, ZZRingElem)
+   @test isa(c, ZZRingElem)
 
    @test sign(a) == 1
-
    @test sign(a) isa ZZRingElem
+   @test !signbit(a)
+
+   @test sign(-a) == -1
+   @test sign(-a) isa ZZRingElem
+   @test signbit(-a)
+
+   @test sign(b) == 0
+   @test sign(b) isa ZZRingElem
+   @test !signbit(b)
 
    @test fits(Int, a)
 
@@ -163,12 +169,12 @@ end
 
    @test is_unit(ZZRingElem(-1))
 
+   @test !iszero(a)
    @test iszero(b)
-
    @test zero(ZZRing()) == zero(ZZRingElem)
 
    @test isone(a)
-
+   @test !isone(b)
    @test one(ZZRing()) == one(ZZRingElem)
 
    @test numerator(ZZRingElem(12)) == ZZRingElem(12)
@@ -187,6 +193,21 @@ end
    @test iseven(x) == iseven(y)
    @test isodd(x) == isodd(y)
 
+   @test isinteger(a)
+   @test isinteger(b)
+   @test isinteger(x)
+   @test isinteger(y)
+
+   @test isfinite(a)
+   @test isfinite(b)
+   @test isfinite(x)
+   @test isfinite(y)
+
+   @test !isinf(a)
+   @test !isinf(b)
+   @test !isinf(x)
+   @test !isinf(y)
+
    @test characteristic(ZZ) == 0
 end