-- |
-- Module:      Cantor.Huge
-- Copyright:   (c) 2020 Andrew Lelechenko
-- Licence:     MIT
-- Maintainer:  Andrew Lelechenko <andrew.lelechenko@gmail.com>

{-# LANGUAGE LambdaCase #-}

module Cantor.Huge
  ( Huge
  , pow
  , evalWith
  ) where

import Prelude hiding ((^^))
import Control.Exception
import Math.NumberTheory.Logarithms
import Math.NumberTheory.Roots
import Numeric.Natural

-- | Lazy huge numbers with an efficient 'Ord' instance.
data Huge
  = Nat Natural
  | Add Huge Huge
  | Mul Huge Huge
  | Pow Huge Huge

instance Show Huge where
  show :: Huge -> String
show = \case
    Nat Natural
n -> Natural -> String
forall a. Show a => a -> String
show Natural
n
    Add Huge
x Huge
y -> String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Huge -> String
forall a. Show a => a -> String
show Huge
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" + " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Huge -> String
forall a. Show a => a -> String
show Huge
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
    Mul Huge
x Huge
y -> String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Huge -> String
forall a. Show a => a -> String
show Huge
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" * " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Huge -> String
forall a. Show a => a -> String
show Huge
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
    Pow Huge
x Huge
y -> String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Huge -> String
forall a. Show a => a -> String
show Huge
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ^ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Huge -> String
forall a. Show a => a -> String
show Huge
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

instance Num Huge where
  + :: Huge -> Huge -> Huge
(+) = Huge -> Huge -> Huge
add
  * :: Huge -> Huge -> Huge
(*) = Huge -> Huge -> Huge
mul
  abs :: Huge -> Huge
abs = Huge -> Huge
forall a. a -> a
id
  signum :: Huge -> Huge
signum = Huge -> Huge -> Huge
forall a b. a -> b -> a
const Huge
1
  negate :: Huge -> Huge
negate = ArithException -> Huge -> Huge
forall a e. Exception e => e -> a
throw ArithException
Underflow
  fromInteger :: Integer -> Huge
fromInteger = Natural -> Huge
Nat (Natural -> Huge) -> (Integer -> Natural) -> Integer -> Huge
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Natural
forall a. Num a => Integer -> a
fromInteger

{-# RULES "Huge/pow" forall x p. x ^ p = x `pow` p #-}

add :: Huge -> Huge -> Huge
add :: Huge -> Huge -> Huge
add (Nat Natural
0) Huge
y = Huge
y
add Huge
x (Nat Natural
0) = Huge
x
-- add (Nat x) (Nat y) = Nat $ x + y
add Huge
x Huge
y = Huge -> Huge -> Huge
Add Huge
x Huge
y

mul :: Huge -> Huge -> Huge
mul :: Huge -> Huge -> Huge
mul (Nat Natural
0) Huge
_ = Natural -> Huge
Nat Natural
0
mul Huge
_ (Nat Natural
0) = Natural -> Huge
Nat Natural
0
mul (Nat Natural
1) Huge
y = Huge
y
mul Huge
x (Nat Natural
1) = Huge
x
-- mul (Nat x) (Nat y) = Nat $ x * y
mul Huge
x Huge
y = Huge -> Huge -> Huge
Mul Huge
x Huge
y

-- | Exponentiation.
pow :: Huge -> Huge -> Huge
pow :: Huge -> Huge -> Huge
pow Huge
_ (Nat Natural
0) = Natural -> Huge
Nat Natural
1
pow (Nat Natural
0) Huge
_ = Natural -> Huge
Nat Natural
0
pow Huge
x (Nat Natural
1) = Huge
x
pow (Nat Natural
1) Huge
_ = Natural -> Huge
Nat Natural
1
pow Huge
x Huge
y = Huge -> Huge -> Huge
Pow Huge
x Huge
y

-- | Convert 'Huge' to another numeric type,
-- using provided function for exponentiation.
evalWith :: Num a => (a -> a -> a) -> Huge -> a
evalWith :: (a -> a -> a) -> Huge -> a
evalWith a -> a -> a
(^^) = Huge -> a
go
  where
    go :: Huge -> a
go = \case
      Nat Natural
n   -> Natural -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n
      Add Huge
x Huge
y -> Huge -> a
go Huge
x a -> a -> a
forall a. Num a => a -> a -> a
+  Huge -> a
go Huge
y
      Mul Huge
x Huge
y -> Huge -> a
go Huge
x a -> a -> a
forall a. Num a => a -> a -> a
*  Huge -> a
go Huge
y
      Pow Huge
x Huge
y -> Huge -> a
go Huge
x a -> a -> a
^^ Huge -> a
go Huge
y

-- | Simply 'evalWith' '(^)'.
eval :: Huge -> Natural
eval :: Huge -> Natural
eval = (Natural -> Natural -> Natural) -> Huge -> Natural
forall a. Num a => (a -> a -> a) -> Huge -> a
evalWith Natural -> Natural -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
(^)

instance Eq Huge where
  Huge
x == :: Huge -> Huge -> Bool
== Huge
y = Huge
x Huge -> Huge -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Huge
y Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ

instance Ord Huge where
  Huge
x compare :: Huge -> Huge -> Ordering
`compare` Huge
y = Huge
x Huge -> Huge -> Ordering
`compareHuge` Huge
y

-- Assuming the second argument has been constructed
-- using smart constructors.
compareNat :: Natural -> Huge -> Ordering
compareNat :: Natural -> Huge -> Ordering
compareNat Natural
m = Huge -> Ordering
go
  where
    go :: Huge -> Ordering
go = \case
      Nat Natural
n -> Natural
m Natural -> Natural -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Natural
n
      Add Huge
x Huge
y
        | Nat Natural
n <- Huge
x -> if Natural
m Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< Natural
n then Ordering
LT else (Natural
m Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
n) Natural -> Huge -> Ordering
`compareNat` Huge
y
        | Nat Natural
n <- Huge
y -> if Natural
m Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< Natural
n then Ordering
LT else (Natural
m Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
n) Natural -> Huge -> Ordering
`compareNat` Huge
x
        | Huge -> Ordering
go Huge
x Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
LT -> Ordering
LT
        | Huge -> Ordering
go Huge
y Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
LT -> Ordering
LT
        | Huge
x Huge -> Huge -> Bool
forall a. Ord a => a -> a -> Bool
<= Huge
y     -> (Natural
m Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Huge -> Natural
eval Huge
x) Natural -> Huge -> Ordering
`compareNat` Huge
y
        | Bool
otherwise  -> (Natural
m Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Huge -> Natural
eval Huge
y) Natural -> Huge -> Ordering
`compareNat` Huge
x
      Mul Huge
x Huge
y
        | Nat Natural
n <- Huge
x -> if Natural
m Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< Natural
n then Ordering
LT else (Natural -> Natural -> (Natural, Perfectness))
-> Natural -> Natural -> Huge -> Ordering
unwrap Natural -> Natural -> (Natural, Perfectness)
quotPerf Natural
m Natural
n Huge
y
        | Nat Natural
n <- Huge
y -> if Natural
m Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< Natural
n then Ordering
LT else (Natural -> Natural -> (Natural, Perfectness))
-> Natural -> Natural -> Huge -> Ordering
unwrap Natural -> Natural -> (Natural, Perfectness)
quotPerf Natural
m Natural
n Huge
x
        | Huge -> Ordering
go Huge
x Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
/= Ordering
GT -> Ordering
LT
        | Huge -> Ordering
go Huge
y Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
/= Ordering
GT -> Ordering
LT
        | Huge
x Huge -> Huge -> Bool
forall a. Ord a => a -> a -> Bool
<= Huge
y     -> (Natural -> Natural -> (Natural, Perfectness))
-> Natural -> Natural -> Huge -> Ordering
unwrap Natural -> Natural -> (Natural, Perfectness)
quotPerf Natural
m (Huge -> Natural
eval Huge
x) Huge
y
        | Bool
otherwise  -> (Natural -> Natural -> (Natural, Perfectness))
-> Natural -> Natural -> Huge -> Ordering
unwrap Natural -> Natural -> (Natural, Perfectness)
quotPerf Natural
m (Huge -> Natural
eval Huge
y) Huge
x
      Pow Huge
x Huge
y
        | Nat Natural
n <- Huge
x -> if Natural
m Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< Natural
n then Ordering
LT else (Natural -> Natural -> (Natural, Perfectness))
-> Natural -> Natural -> Huge -> Ordering
unwrap Natural -> Natural -> (Natural, Perfectness)
logPerf  Natural
m Natural
n Huge
y
        | Nat Natural
n <- Huge
y -> if Natural
m Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< Natural
n then Ordering
LT else (Natural -> Natural -> (Natural, Perfectness))
-> Natural -> Natural -> Huge -> Ordering
unwrap Natural -> Natural -> (Natural, Perfectness)
rootPerf Natural
m Natural
n Huge
x
        | Huge -> Ordering
go Huge
x Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
/= Ordering
GT -> Ordering
LT
        | Huge -> Ordering
go Huge
y Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
/= Ordering
GT -> Ordering
LT
        | Huge
x Huge -> Huge -> Bool
forall a. Ord a => a -> a -> Bool
<= Huge
y     -> (Natural -> Natural -> (Natural, Perfectness))
-> Natural -> Natural -> Huge -> Ordering
unwrap Natural -> Natural -> (Natural, Perfectness)
logPerf  Natural
m (Huge -> Natural
eval Huge
x) Huge
y
        | Bool
otherwise  -> (Natural -> Natural -> (Natural, Perfectness))
-> Natural -> Natural -> Huge -> Ordering
unwrap Natural -> Natural -> (Natural, Perfectness)
rootPerf Natural
m (Huge -> Natural
eval Huge
y) Huge
x

data Perfectness = Perfect | Imperfect
  deriving (Perfectness -> Perfectness -> Bool
(Perfectness -> Perfectness -> Bool)
-> (Perfectness -> Perfectness -> Bool) -> Eq Perfectness
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Perfectness -> Perfectness -> Bool
$c/= :: Perfectness -> Perfectness -> Bool
== :: Perfectness -> Perfectness -> Bool
$c== :: Perfectness -> Perfectness -> Bool
Eq, Eq Perfectness
Eq Perfectness
-> (Perfectness -> Perfectness -> Ordering)
-> (Perfectness -> Perfectness -> Bool)
-> (Perfectness -> Perfectness -> Bool)
-> (Perfectness -> Perfectness -> Bool)
-> (Perfectness -> Perfectness -> Bool)
-> (Perfectness -> Perfectness -> Perfectness)
-> (Perfectness -> Perfectness -> Perfectness)
-> Ord Perfectness
Perfectness -> Perfectness -> Bool
Perfectness -> Perfectness -> Ordering
Perfectness -> Perfectness -> Perfectness
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Perfectness -> Perfectness -> Perfectness
$cmin :: Perfectness -> Perfectness -> Perfectness
max :: Perfectness -> Perfectness -> Perfectness
$cmax :: Perfectness -> Perfectness -> Perfectness
>= :: Perfectness -> Perfectness -> Bool
$c>= :: Perfectness -> Perfectness -> Bool
> :: Perfectness -> Perfectness -> Bool
$c> :: Perfectness -> Perfectness -> Bool
<= :: Perfectness -> Perfectness -> Bool
$c<= :: Perfectness -> Perfectness -> Bool
< :: Perfectness -> Perfectness -> Bool
$c< :: Perfectness -> Perfectness -> Bool
compare :: Perfectness -> Perfectness -> Ordering
$ccompare :: Perfectness -> Perfectness -> Ordering
$cp1Ord :: Eq Perfectness
Ord, Int -> Perfectness -> ShowS
[Perfectness] -> ShowS
Perfectness -> String
(Int -> Perfectness -> ShowS)
-> (Perfectness -> String)
-> ([Perfectness] -> ShowS)
-> Show Perfectness
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Perfectness] -> ShowS
$cshowList :: [Perfectness] -> ShowS
show :: Perfectness -> String
$cshow :: Perfectness -> String
showsPrec :: Int -> Perfectness -> ShowS
$cshowsPrec :: Int -> Perfectness -> ShowS
Show)

unwrap
  :: (Natural -> Natural -> (Natural, Perfectness))
  -> Natural
  -> Natural
  -> Huge
  -> Ordering
unwrap :: (Natural -> Natural -> (Natural, Perfectness))
-> Natural -> Natural -> Huge -> Ordering
unwrap Natural -> Natural -> (Natural, Perfectness)
f Natural
m Natural
n Huge
y = case Natural
m Natural -> Natural -> (Natural, Perfectness)
`f` Natural
n of
  (Natural
q, Perfectness
r) -> Natural
q Natural -> Huge -> Ordering
`compareNat` Huge
y Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> (Perfectness
r Perfectness -> Perfectness -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Perfectness
Perfect)

quotPerf :: Natural -> Natural -> (Natural, Perfectness)
quotPerf :: Natural -> Natural -> (Natural, Perfectness)
quotPerf Natural
m Natural
x = (Natural
q, Perfectness
r)
  where
    q :: Natural
q = Natural
m Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`quot` Natural
x
    r :: Perfectness
r = if Natural
q Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
x Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
m then Perfectness
Perfect else Perfectness
Imperfect

rootPerf :: Natural -> Natural -> (Natural, Perfectness)
rootPerf :: Natural -> Natural -> (Natural, Perfectness)
rootPerf Natural
m Natural
x = (Natural
q, Perfectness
r)
  where
    q :: Natural
q = Natural -> Natural -> Natural
forall a b. (Integral a, Integral b) => b -> a -> a
integerRoot Natural
x Natural
m
    r :: Perfectness
r = if Natural
q Natural -> Natural -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
^ Natural
x Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
m then Perfectness
Perfect else Perfectness
Imperfect

logPerf :: Natural -> Natural -> (Natural, Perfectness)
logPerf :: Natural -> Natural -> (Natural, Perfectness)
logPerf Natural
m Natural
x = (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
q, Perfectness
r)
  where
    q :: Int
q = Natural -> Natural -> Int
naturalLogBase Natural
x Natural
m
    r :: Perfectness
r = if Natural
x Natural -> Int -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
^ Int
q Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
m then Perfectness
Perfect else Perfectness
Imperfect

inverse :: Ordering -> Ordering
inverse :: Ordering -> Ordering
inverse = \case
  Ordering
LT -> Ordering
GT
  Ordering
EQ -> Ordering
EQ
  Ordering
GT -> Ordering
LT

-- Assuming both arguments have been constructed
-- using smart constructors.
compareHuge :: Huge -> Huge -> Ordering
Nat Natural
m   compareHuge :: Huge -> Huge -> Ordering
`compareHuge` Huge
z       = Natural -> Huge -> Ordering
compareNat Natural
m Huge
z
Huge
z       `compareHuge` Nat Natural
m   = Ordering -> Ordering
inverse (Ordering -> Ordering) -> Ordering -> Ordering
forall a b. (a -> b) -> a -> b
$ Natural -> Huge -> Ordering
compareNat Natural
m Huge
z
Add Huge
x Huge
y `compareHuge` Add Huge
u Huge
v = Huge -> Huge -> Huge -> Huge -> Ordering
compareAddAdd Huge
x Huge
y Huge
u Huge
v
Add Huge
x Huge
y `compareHuge` Mul Huge
u Huge
v = (Huge -> Huge -> Huge)
-> (Huge -> Huge -> Huge)
-> Huge
-> Huge
-> Huge
-> Huge
-> Ordering
compareAscNodes Huge -> Huge -> Huge
Add Huge -> Huge -> Huge
Mul Huge
x Huge
y Huge
u Huge
v
Add Huge
x Huge
y `compareHuge` Pow Huge
u Huge
v = (Huge -> Huge -> Huge)
-> (Huge -> Huge -> Huge)
-> Huge
-> Huge
-> Huge
-> Huge
-> Ordering
compareAscNodes Huge -> Huge -> Huge
Add Huge -> Huge -> Huge
Pow Huge
x Huge
y Huge
u Huge
v
Mul Huge
x Huge
y `compareHuge` Add Huge
u Huge
v = Ordering -> Ordering
inverse (Ordering -> Ordering) -> Ordering -> Ordering
forall a b. (a -> b) -> a -> b
$ (Huge -> Huge -> Huge)
-> (Huge -> Huge -> Huge)
-> Huge
-> Huge
-> Huge
-> Huge
-> Ordering
compareAscNodes Huge -> Huge -> Huge
Add Huge -> Huge -> Huge
Mul Huge
u Huge
v Huge
x Huge
y
Mul Huge
x Huge
y `compareHuge` Mul Huge
u Huge
v = Huge -> Huge -> Huge -> Huge -> Ordering
compareMulMul Huge
x Huge
y Huge
u Huge
v
Mul Huge
x Huge
y `compareHuge` Pow Huge
u Huge
v = (Huge -> Huge -> Huge)
-> (Huge -> Huge -> Huge)
-> Huge
-> Huge
-> Huge
-> Huge
-> Ordering
compareAscNodes Huge -> Huge -> Huge
Mul Huge -> Huge -> Huge
Pow Huge
x Huge
y Huge
u Huge
v
Pow Huge
x Huge
y `compareHuge` Add Huge
u Huge
v = Ordering -> Ordering
inverse (Ordering -> Ordering) -> Ordering -> Ordering
forall a b. (a -> b) -> a -> b
$ (Huge -> Huge -> Huge)
-> (Huge -> Huge -> Huge)
-> Huge
-> Huge
-> Huge
-> Huge
-> Ordering
compareAscNodes Huge -> Huge -> Huge
Add Huge -> Huge -> Huge
Pow Huge
u Huge
v Huge
x Huge
y
Pow Huge
x Huge
y `compareHuge` Mul Huge
u Huge
v = Ordering -> Ordering
inverse (Ordering -> Ordering) -> Ordering -> Ordering
forall a b. (a -> b) -> a -> b
$ (Huge -> Huge -> Huge)
-> (Huge -> Huge -> Huge)
-> Huge
-> Huge
-> Huge
-> Huge
-> Ordering
compareAscNodes Huge -> Huge -> Huge
Mul Huge -> Huge -> Huge
Pow Huge
u Huge
v Huge
x Huge
y
Pow Huge
x Huge
y `compareHuge` Pow Huge
u Huge
v = Huge -> Huge -> Huge -> Huge -> Ordering
comparePowPow Huge
x Huge
y Huge
u Huge
v

-- Compare Add vs. Mul, Add vs. Pow or Mul vs. Pow,
-- but not vice versa.
compareAscNodes
  :: (Huge -> Huge -> Huge)
  -> (Huge -> Huge -> Huge)
  -> Huge
  -> Huge
  -> Huge
  -> Huge
  -> Ordering
compareAscNodes :: (Huge -> Huge -> Huge)
-> (Huge -> Huge -> Huge)
-> Huge
-> Huge
-> Huge
-> Huge
-> Ordering
compareAscNodes Huge -> Huge -> Huge
fxy Huge -> Huge -> Huge
fuv Huge
x Huge
y Huge
u Huge
v =
  case (Huge
x Huge -> Huge -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Huge
u, Huge
x Huge -> Huge -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Huge
v, Huge
y Huge -> Huge -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Huge
u, Huge
y Huge -> Huge -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Huge
v) of
    (Ordering
LT,  Ordering
_,  Ordering
_, Ordering
LT) -> Ordering
LT
    ( Ordering
_, Ordering
LT, Ordering
LT,  Ordering
_) -> Ordering
LT

    (Ordering
GT, Ordering
GT,  Ordering
_,  Ordering
_) -> Ordering
uvSimpler
    (Ordering
GT,  Ordering
_,  Ordering
_, Ordering
GT) -> Ordering
uvSimpler
    ( Ordering
_, Ordering
GT, Ordering
GT,  Ordering
_) -> Ordering
uvSimpler
    ( Ordering
_,  Ordering
_, Ordering
GT, Ordering
GT) -> Ordering
uvSimpler

    (Ordering
LT,  Ordering
_, Ordering
LT,  Ordering
_) -> Ordering
xySimpler
    (Ordering
LT,  Ordering
_, Ordering
EQ,  Ordering
_) -> Ordering
xySimpler
    (Ordering
EQ,  Ordering
_, Ordering
LT,  Ordering
_) -> Ordering
xySimpler
    (Ordering
EQ,  Ordering
_, Ordering
EQ,  Ordering
_) -> Ordering
xySimpler

    ( Ordering
_, Ordering
LT,  Ordering
_, Ordering
LT) -> Ordering
xySimpler
    ( Ordering
_, Ordering
LT,  Ordering
_, Ordering
EQ) -> Ordering
xySimpler
    ( Ordering
_, Ordering
EQ,  Ordering
_, Ordering
LT) -> Ordering
xySimpler
    ( Ordering
_, Ordering
EQ,  Ordering
_, Ordering
EQ) -> Ordering
xySimpler
  where
    uvSimpler :: Ordering
uvSimpler = Ordering -> Ordering
inverse (Ordering -> Ordering) -> Ordering -> Ordering
forall a b. (a -> b) -> a -> b
$ Natural -> Huge -> Ordering
compareNat (Huge -> Natural
eval (Huge -> Huge -> Huge
fuv Huge
u Huge
v)) (Huge -> Huge -> Huge
fxy Huge
x Huge
y)
    xySimpler :: Ordering
xySimpler = Natural -> Huge -> Ordering
compareNat (Huge -> Natural
eval (Huge -> Huge -> Huge
fxy Huge
x Huge
y)) (Huge -> Huge -> Huge
fuv Huge
u Huge
v)

compareAddAdd :: Huge -> Huge -> Huge -> Huge -> Ordering
compareAddAdd :: Huge -> Huge -> Huge -> Huge -> Ordering
compareAddAdd Huge
x Huge
y Huge
u Huge
v =
  case (Huge
x Huge -> Huge -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Huge
u, Huge
x Huge -> Huge -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Huge
v, Huge
y Huge -> Huge -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Huge
u, Huge
y Huge -> Huge -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Huge
v) of
    (Ordering
EQ,  Ordering
_,  Ordering
_, Ordering
yv) -> Ordering
yv
    ( Ordering
_, Ordering
EQ, Ordering
yu,  Ordering
_) -> Ordering
yu
    ( Ordering
_, Ordering
xv, Ordering
EQ,  Ordering
_) -> Ordering
xv
    (Ordering
xu,  Ordering
_,  Ordering
_, Ordering
EQ) -> Ordering
xu

    (Ordering
GT,  Ordering
_,  Ordering
_, Ordering
GT) -> Ordering
GT
    ( Ordering
_, Ordering
GT, Ordering
GT,  Ordering
_) -> Ordering
GT
    (Ordering
LT,  Ordering
_,  Ordering
_, Ordering
LT) -> Ordering
LT
    ( Ordering
_, Ordering
LT, Ordering
LT,  Ordering
_) -> Ordering
LT

    -- x > u > y, x > v > y
    (Ordering
GT, Ordering
GT, Ordering
LT, Ordering
LT)
      | Huge
u Huge -> Huge -> Bool
forall a. Ord a => a -> a -> Bool
<= Huge
v    -> Huge
x Huge -> Huge -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Huge -> Huge -> Huge
Add (Natural -> Huge
Nat (Huge -> Natural
eval Huge
u Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Huge -> Natural
eval Huge
y)) Huge
v
      | Bool
otherwise -> Huge
x Huge -> Huge -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Huge -> Huge -> Huge
Add Huge
u (Natural -> Huge
Nat (Huge -> Natural
eval Huge
v Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Huge -> Natural
eval Huge
y))
    -- y > u > x, y > v > x
    (Ordering
LT, Ordering
LT, Ordering
GT, Ordering
GT)
      | Huge
u Huge -> Huge -> Bool
forall a. Ord a => a -> a -> Bool
<= Huge
v    -> Huge
y Huge -> Huge -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Huge -> Huge -> Huge
Add (Natural -> Huge
Nat (Huge -> Natural
eval Huge
u Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Huge -> Natural
eval Huge
x)) Huge
v
      | Bool
otherwise -> Huge
y Huge -> Huge -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Huge -> Huge -> Huge
Add Huge
u (Natural -> Huge
Nat (Huge -> Natural
eval Huge
v Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Huge -> Natural
eval Huge
x))
    -- u > x > v, u > y > v
    (Ordering
LT, Ordering
GT, Ordering
LT, Ordering
GT)
      | Huge
x Huge -> Huge -> Bool
forall a. Ord a => a -> a -> Bool
<= Huge
y    -> Huge -> Huge -> Huge
Add (Natural -> Huge
Nat (Huge -> Natural
eval Huge
x Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Huge -> Natural
eval Huge
v)) Huge
y Huge -> Huge -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Huge
u
      | Bool
otherwise -> Huge -> Huge -> Huge
Add Huge
x (Natural -> Huge
Nat (Huge -> Natural
eval Huge
y Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Huge -> Natural
eval Huge
v)) Huge -> Huge -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Huge
u
    -- v > x > u, v > y > u
    (Ordering
GT, Ordering
LT, Ordering
GT, Ordering
LT)
      | Huge
x Huge -> Huge -> Bool
forall a. Ord a => a -> a -> Bool
<= Huge
y    -> Huge -> Huge -> Huge
Add (Natural -> Huge
Nat (Huge -> Natural
eval Huge
x Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Huge -> Natural
eval Huge
u)) Huge
y Huge -> Huge -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Huge
v
      | Bool
otherwise -> Huge -> Huge -> Huge
Add Huge
x (Natural -> Huge
Nat (Huge -> Natural
eval Huge
y Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Huge -> Natural
eval Huge
u)) Huge -> Huge -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Huge
v

compareMulMul :: Huge -> Huge -> Huge -> Huge -> Ordering
compareMulMul :: Huge -> Huge -> Huge -> Huge -> Ordering
compareMulMul Huge
x Huge
y Huge
u Huge
v =
  case (Huge
x Huge -> Huge -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Huge
u, Huge
x Huge -> Huge -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Huge
v, Huge
y Huge -> Huge -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Huge
u, Huge
y Huge -> Huge -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Huge
v) of
    (Ordering
EQ,  Ordering
_,  Ordering
_, Ordering
yv) -> Ordering
yv
    ( Ordering
_, Ordering
EQ, Ordering
yu,  Ordering
_) -> Ordering
yu
    ( Ordering
_, Ordering
xv, Ordering
EQ,  Ordering
_) -> Ordering
xv
    (Ordering
xu,  Ordering
_,  Ordering
_, Ordering
EQ) -> Ordering
xu

    (Ordering
GT,  Ordering
_,  Ordering
_, Ordering
GT) -> Ordering
GT
    ( Ordering
_, Ordering
GT, Ordering
GT,  Ordering
_) -> Ordering
GT
    (Ordering
LT,  Ordering
_,  Ordering
_, Ordering
LT) -> Ordering
LT
    ( Ordering
_, Ordering
LT, Ordering
LT,  Ordering
_) -> Ordering
LT

    (Ordering
GT, Ordering
GT, Ordering
LT, Ordering
LT) -> Ordering
uvSimpler
    (Ordering
LT, Ordering
LT, Ordering
GT, Ordering
GT) -> Ordering
uvSimpler
    (Ordering
LT, Ordering
GT, Ordering
LT, Ordering
GT) -> Ordering
xySimpler
    (Ordering
GT, Ordering
LT, Ordering
GT, Ordering
LT) -> Ordering
xySimpler
  where
    uvSimpler :: Ordering
uvSimpler = Ordering -> Ordering
inverse (Ordering -> Ordering) -> Ordering -> Ordering
forall a b. (a -> b) -> a -> b
$ Natural -> Huge -> Ordering
compareNat (Huge -> Natural
eval (Huge -> Huge -> Huge
Mul Huge
u Huge
v)) (Huge -> Huge -> Huge
Mul Huge
x Huge
y)
    xySimpler :: Ordering
xySimpler = Natural -> Huge -> Ordering
compareNat (Huge -> Natural
eval (Huge -> Huge -> Huge
Mul Huge
x Huge
y)) (Huge -> Huge -> Huge
Mul Huge
u Huge
v)

comparePowPow :: Huge -> Huge -> Huge -> Huge -> Ordering
comparePowPow :: Huge -> Huge -> Huge -> Huge -> Ordering
comparePowPow Huge
x Huge
y Huge
u Huge
v = case (Huge
x Huge -> Huge -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Huge
u, Huge
y Huge -> Huge -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Huge
v) of
  (Ordering
EQ, Ordering
yv) -> Ordering
yv
  (Ordering
xu, Ordering
EQ) -> Ordering
xu
  (Ordering
LT, Ordering
LT) -> Ordering
LT
  (Ordering
GT, Ordering
GT) -> Ordering
GT
  (Ordering
LT, Ordering
GT) -> Ordering -> Ordering
inverse (Ordering -> Ordering) -> Ordering -> Ordering
forall a b. (a -> b) -> a -> b
$ Natural -> Huge -> Ordering
compareNat (Huge -> Natural
eval (Huge -> Huge -> Huge
Pow Huge
u Huge
v)) (Huge -> Huge -> Huge
Pow Huge
x Huge
y)
  (Ordering
GT, Ordering
LT) -> Natural -> Huge -> Ordering
compareNat (Huge -> Natural
eval (Huge -> Huge -> Huge
Pow Huge
x Huge
y)) (Huge -> Huge -> Huge
Pow Huge
u Huge
v)