{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Numeric.Rounded.Hardware.Interval.ElementaryFunctions where
import Control.Exception (assert)
import Numeric.Rounded.Hardware.Internal
import Numeric.Rounded.Hardware.Interval.Class

sqrtI :: (IsInterval i, RoundedSqrt (EndPoint i)) => i -> i
sqrtI :: forall i. (IsInterval i, RoundedSqrt (EndPoint i)) => i -> i
sqrtI = forall i.
IsInterval i =>
(Rounded 'TowardNegInf (EndPoint i)
 -> Rounded 'TowardInf (EndPoint i) -> i)
-> i -> i
withEndPoints forall a b. (a -> b) -> a -> b
$ \Rounded 'TowardNegInf (EndPoint i)
x Rounded 'TowardInf (EndPoint i)
y -> case forall a.
RoundedSqrt a =>
Rounded 'TowardNegInf a
-> Rounded 'TowardInf a
-> (Rounded 'TowardNegInf a, Rounded 'TowardInf a)
intervalSqrt Rounded 'TowardNegInf (EndPoint i)
x Rounded 'TowardInf (EndPoint i)
y of (Rounded 'TowardNegInf (EndPoint i)
u, Rounded 'TowardInf (EndPoint i)
v) -> forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval Rounded 'TowardNegInf (EndPoint i)
u Rounded 'TowardInf (EndPoint i)
v
{-# INLINE sqrtI #-}

expP :: forall i. (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RealFloatConstants (EndPoint i), RoundedFractional (EndPoint i)) => EndPoint i -> i
expP :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
EndPoint i -> i
expP EndPoint i
x | forall a. RealFloat a => a -> Bool
isInfinite EndPoint i
x = if EndPoint i
x forall a. Ord a => a -> a -> Bool
> EndPoint i
0
                        then forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval (forall (r :: RoundingMode) a. a -> Rounded r a
Rounded forall a. RealFloatConstants a => a
maxFinite) (forall (r :: RoundingMode) a. a -> Rounded r a
Rounded forall a. RealFloatConstants a => a
positiveInfinity)
                        else forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval (forall (r :: RoundingMode) a. a -> Rounded r a
Rounded EndPoint i
0) (forall (r :: RoundingMode) a. a -> Rounded r a
Rounded forall a. RealFloatConstants a => a
minPositive)
expP EndPoint i
x = let a :: Integer
a = forall a b. (RealFrac a, Integral b) => a -> b
round EndPoint i
x
             b :: EndPoint i
b = EndPoint i
x forall a. Num a => a -> a -> a
- forall a. Num a => Integer -> a
fromInteger Integer
a -- -1/2 <= b && b <= 1/2
             b' :: i
b' = forall i. IsInterval i => EndPoint i -> i
singleton EndPoint i
b
             series :: Int -> i -> i
             series :: Int -> i -> i
series Int
n i
acc | Int
n forall a. Eq a => a -> a -> Bool
== Int
0 = i
acc
                          | Bool
otherwise = Int -> i -> i
series (Int
nforall a. Num a => a -> a -> a
-Int
1) forall a b. (a -> b) -> a -> b
$ i
1 forall a. Num a => a -> a -> a
+ i
acc forall a. Num a => a -> a -> a
* i
b' forall a. Fractional a => a -> a -> a
/ forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n
         in forall a. (?callStack::CallStack) => Bool -> a -> a
assert (forall a. Num a => Integer -> a
fromInteger Integer
a forall a. Num a => a -> a -> a
+ EndPoint i
b forall a. Eq a => a -> a -> Bool
== EndPoint i
x Bool -> Bool -> Bool
&& forall a. Num a => a -> a
abs EndPoint i
b forall a. Ord a => a -> a -> Bool
<= EndPoint i
0.5) forall a b. (a -> b) -> a -> b
$
            (forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval forall a. RealFloatConstants a => Rounded 'TowardNegInf a
exp1_down forall a. RealFloatConstants a => Rounded 'TowardInf a
exp1_up)forall a b. (Fractional a, Integral b) => a -> b -> a
^^Integer
a forall a. Num a => a -> a -> a
* Int -> i -> i
series Int
15 (forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval forall a. RealFloatConstants a => Rounded 'TowardNegInf a
expm1_2_down forall a. RealFloatConstants a => Rounded 'TowardInf a
exp1_2_up)
{-# INLINABLE expP #-}

expI :: (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RealFloatConstants (EndPoint i), RoundedFractional (EndPoint i)) => i -> i
expI :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
i -> i
expI = forall i.
IsInterval i =>
(Rounded 'TowardNegInf (EndPoint i)
 -> Rounded 'TowardInf (EndPoint i) -> i)
-> i -> i
withEndPoints (\(Rounded EndPoint i
x) (Rounded EndPoint i
y) -> forall i. IsInterval i => i -> i -> i
hull (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
EndPoint i -> i
expP EndPoint i
x) (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
EndPoint i -> i
expP EndPoint i
y)) -- increasing
{-# INLINABLE expI #-}

expm1P :: forall i. (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RealFloatConstants (EndPoint i), RoundedFractional (EndPoint i)) => EndPoint i -> i
expm1P :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
EndPoint i -> i
expm1P EndPoint i
x | -EndPoint i
0.5 forall a. Ord a => a -> a -> Bool
<= EndPoint i
x Bool -> Bool -> Bool
&& EndPoint i
x forall a. Ord a => a -> a -> Bool
<= EndPoint i
0.5 = let b' :: i
b' = forall i. IsInterval i => EndPoint i -> i
singleton EndPoint i
x
                                       series :: Int -> i -> i
                                       series :: Int -> i -> i
series Int
n i
acc | Int
n forall a. Eq a => a -> a -> Bool
== Int
1 = i
acc forall a. Num a => a -> a -> a
* i
b'
                                                    | Bool
otherwise = Int -> i -> i
series (Int
nforall a. Num a => a -> a -> a
-Int
1) forall a b. (a -> b) -> a -> b
$ i
1 forall a. Num a => a -> a -> a
+ i
acc forall a. Num a => a -> a -> a
* i
b' forall a. Fractional a => a -> a -> a
/ forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n
                                   in Int -> i -> i
series Int
15 (forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval forall a. RealFloatConstants a => Rounded 'TowardNegInf a
expm1_2_down forall a. RealFloatConstants a => Rounded 'TowardInf a
exp1_2_up)
         | Bool
otherwise = forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
EndPoint i -> i
expP EndPoint i
x forall a. Num a => a -> a -> a
- i
1
{-# INLINABLE expm1P #-}

expm1I :: (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RealFloatConstants (EndPoint i), RoundedFractional (EndPoint i)) => i -> i
expm1I :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
i -> i
expm1I = forall i.
IsInterval i =>
(Rounded 'TowardNegInf (EndPoint i)
 -> Rounded 'TowardInf (EndPoint i) -> i)
-> i -> i
withEndPoints (\(Rounded EndPoint i
x) (Rounded EndPoint i
y) -> forall i. IsInterval i => i -> i -> i
hull (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
EndPoint i -> i
expm1P EndPoint i
x) (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
EndPoint i -> i
expm1P EndPoint i
y)) -- increasing
{-# INLINABLE expm1I #-}

logP :: forall i. (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RealFloatConstants (EndPoint i)) => EndPoint i -> i
logP :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i)) =>
EndPoint i -> i
logP EndPoint i
x
  | forall a. RealFloat a => a -> Integer
floatRadix (forall a. (?callStack::CallStack) => a
undefined :: EndPoint i) forall a. Eq a => a -> a -> Bool
/= Integer
2 = forall a. (?callStack::CallStack) => [Char] -> a
error [Char]
"Unsupported float radix"
  | EndPoint i
x forall a. Ord a => a -> a -> Bool
< EndPoint i
0 = forall a. (?callStack::CallStack) => [Char] -> a
error [Char]
"Negative logarithm"
  | EndPoint i
x forall a. Eq a => a -> a -> Bool
== EndPoint i
0 = forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval (forall (r :: RoundingMode) a. a -> Rounded r a
Rounded forall a. RealFloatConstants a => a
negativeInfinity) (forall (r :: RoundingMode) a. a -> Rounded r a
Rounded (-forall a. RealFloatConstants a => a
maxFinite))
  | forall a. RealFloat a => a -> Bool
isInfinite EndPoint i
x = forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval (forall (r :: RoundingMode) a. a -> Rounded r a
Rounded forall a. RealFloatConstants a => a
maxFinite) (forall (r :: RoundingMode) a. a -> Rounded r a
Rounded forall a. RealFloatConstants a => a
positiveInfinity)
  | forall a. RealFloat a => a -> Bool
isNaN EndPoint i
x = forall a. (?callStack::CallStack) => [Char] -> a
error [Char]
"NaN"
  | Bool
otherwise = let m :: Integer
                    n :: Int
                    (Integer
m,Int
n) = forall a. RealFloat a => a -> (Integer, Int)
decodeFloat EndPoint i
x
                    -- x = m * 2^n, 2^(d-1) <= m < 2^d
                    -- x = (m * 2^(-d)) * 2^(n+d)
                    -- x = 2^a * b, a \in {.. -1.5, -1, -0.5, 0, 0.5, 1, 1.5 ..}, 1/\sqrt{2} < b < \sqrt{2}
                    a0, b, bm1 :: i
                    a0 :: i
a0 = forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
n forall a. Num a => a -> a -> a
+ Int
d) -- fromIntegral (exponent x)
                    x' :: EndPoint i
                    x' :: EndPoint i
x' = forall a. RealFloat a => Integer -> Int -> a
encodeFloat Integer
m (- Int
d) -- significand x
                    -- 0.5 <= x' < 1
                    (i
a,i
b) | EndPoint i
0.5 forall a. Ord a => a -> a -> Bool
<= EndPoint i
x' Bool -> Bool -> Bool
&& EndPoint i
x' forall a. Ord a => a -> a -> Bool
<= forall (r :: RoundingMode) a. Rounded r a -> a
getRounded forall a. RealFloatConstants a => Rounded 'TowardNegInf a
two_minus_sqrt2_down = (i
a0 forall a. Num a => a -> a -> a
- i
1, forall i. IsInterval i => EndPoint i -> i
singleton EndPoint i
x' forall a. Num a => a -> a -> a
* i
2) -- 1/2 <= x <= 2 - sqrt 2 => 1 <= 2*x <= 4 - 2 * sqrt 2
                          | forall (r :: RoundingMode) a. Rounded r a -> a
getRounded forall a. RealFloatConstants a => Rounded 'TowardInf a
two_minus_sqrt2_up forall a. Ord a => a -> a -> Bool
<= EndPoint i
x' Bool -> Bool -> Bool
&& EndPoint i
x' forall a. Ord a => a -> a -> Bool
<= EndPoint i
2 forall a. Num a => a -> a -> a
* forall (r :: RoundingMode) a. Rounded r a -> a
getRounded forall a. RealFloatConstants a => Rounded 'TowardNegInf a
sqrt2m1_down = (i
a0 forall a. Num a => a -> a -> a
- i
0.5, forall i. IsInterval i => EndPoint i -> i
singleton EndPoint i
x' forall a. Num a => a -> a -> a
* i
sqrt2_iv) -- 2 - sqrt2 <= x <= 2 * sqrt 2 - 2, 2 * sqrt 2 - 2 <= sqrt 2 * x <= 4 - 2 * sqrt 2
                          | EndPoint i
2 forall a. Num a => a -> a -> a
* forall (r :: RoundingMode) a. Rounded r a -> a
getRounded forall a. RealFloatConstants a => Rounded 'TowardInf a
sqrt2m1_up forall a. Ord a => a -> a -> Bool
<= EndPoint i
x' Bool -> Bool -> Bool
&& EndPoint i
x' forall a. Ord a => a -> a -> Bool
< EndPoint i
1 = (i
a0, forall i. IsInterval i => EndPoint i -> i
singleton EndPoint i
x') -- 2 * sqrt 2 - 2 <= x
                          | Bool
otherwise = forall a. (?callStack::CallStack) => [Char] -> a
error [Char]
"interval log: internal error"
                    -- 2 * sqrt 2 - 2 <= b <= 4 - 2 * sqrt 2
                    -- 2 * sqrt 2 - 3 <= b-1 <= 3 - 2 * sqrt 2
                    bm1 :: i
bm1 = i
b forall a. Num a => a -> a -> a
- i
1
                    series :: Int -> i -> i
                    series :: Int -> i -> i
series Int
k i
acc | Int
k forall a. Eq a => a -> a -> Bool
== Int
0 = i
bm1 forall a. Num a => a -> a -> a
* i
acc
                                 | Bool
otherwise = Int -> i -> i
series (Int
kforall a. Num a => a -> a -> a
-Int
1) forall a b. (a -> b) -> a -> b
$ forall a. Fractional a => a -> a
recip (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
k) forall a. Num a => a -> a -> a
- i
bm1 forall a. Num a => a -> a -> a
* i
acc
                in i
a forall a. Num a => a -> a -> a
* i
log2_iv forall a. Num a => a -> a -> a
+ Int -> i -> i
series Int
21 (forall i. IsInterval i => i -> i -> i
hull i
1 i
b forall a b. (Fractional a, Integral b) => a -> b -> a
^^ (-Int
22 :: Int) forall a. Num a => a -> a -> a
* i
bm1 forall a. Fractional a => a -> a -> a
/ forall a. Num a => Integer -> a
fromInteger Integer
22)
  where
    d :: Int
d = forall a. RealFloat a => a -> Int
floatDigits (forall a. (?callStack::CallStack) => a
undefined :: EndPoint i)
    log2_iv :: i -- log_e 2
    log2_iv :: i
log2_iv = forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval forall a. RealFloatConstants a => Rounded 'TowardNegInf a
log2_down forall a. RealFloatConstants a => Rounded 'TowardInf a
log2_up
    sqrt2_iv :: i -- sqrt 2
    sqrt2_iv :: i
sqrt2_iv = forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval forall a. RealFloatConstants a => Rounded 'TowardNegInf a
sqrt2_down forall a. RealFloatConstants a => Rounded 'TowardInf a
sqrt2_up
{-# INLINABLE logP #-}

logI :: (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RealFloatConstants (EndPoint i)) => i -> i
logI :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i)) =>
i -> i
logI = forall i.
IsInterval i =>
(Rounded 'TowardNegInf (EndPoint i)
 -> Rounded 'TowardInf (EndPoint i) -> i)
-> i -> i
withEndPoints (\(Rounded EndPoint i
x) (Rounded EndPoint i
y) -> forall i. IsInterval i => i -> i -> i
hull (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i)) =>
EndPoint i -> i
logP EndPoint i
x) (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i)) =>
EndPoint i -> i
logP EndPoint i
y)) -- increasing
{-# INLINABLE logI #-}

log1pP :: forall i. (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RealFloatConstants (EndPoint i)) => EndPoint i -> i
log1pP :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i)) =>
EndPoint i -> i
log1pP EndPoint i
x | - forall (r :: RoundingMode) a. Rounded r a -> a
getRounded forall a. RealFloatConstants a => Rounded 'TowardNegInf a
three_minus_2sqrt2_down forall a. Ord a => a -> a -> Bool
<= EndPoint i
x Bool -> Bool -> Bool
&& EndPoint i
x forall a. Ord a => a -> a -> Bool
<= forall (r :: RoundingMode) a. Rounded r a -> a
getRounded forall a. RealFloatConstants a => Rounded 'TowardNegInf a
three_minus_2sqrt2_down =
             let x' :: i
                 x' :: i
x' = forall i. IsInterval i => EndPoint i -> i
singleton EndPoint i
x
                 series :: Int -> i -> i
                 series :: Int -> i -> i
series Int
k i
acc | Int
k forall a. Eq a => a -> a -> Bool
== Int
0 = i
x' forall a. Num a => a -> a -> a
* i
acc
                              | Bool
otherwise = Int -> i -> i
series (Int
kforall a. Num a => a -> a -> a
-Int
1) forall a b. (a -> b) -> a -> b
$ forall a. Fractional a => a -> a
recip (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
k) forall a. Num a => a -> a -> a
- i
x' forall a. Num a => a -> a -> a
* i
acc
             in Int -> i -> i
series Int
21 (forall i. IsInterval i => i -> i -> i
hull i
1 (i
x' forall a. Num a => a -> a -> a
+ i
1) forall a b. (Fractional a, Integral b) => a -> b -> a
^^ (-Int
22 :: Int) forall a. Num a => a -> a -> a
* i
x' forall a. Fractional a => a -> a -> a
/ forall a. Num a => Integer -> a
fromInteger Integer
22)
         | Bool
otherwise = forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i)) =>
i -> i
logI (forall i. IsInterval i => EndPoint i -> i
singleton EndPoint i
x forall a. Num a => a -> a -> a
+ i
1)
{-# INLINABLE log1pP #-}

log1pI :: (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RealFloatConstants (EndPoint i)) => i -> i
log1pI :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i)) =>
i -> i
log1pI = forall i.
IsInterval i =>
(Rounded 'TowardNegInf (EndPoint i)
 -> Rounded 'TowardInf (EndPoint i) -> i)
-> i -> i
withEndPoints (\(Rounded EndPoint i
x) (Rounded EndPoint i
y) -> forall i. IsInterval i => i -> i -> i
hull (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i)) =>
EndPoint i -> i
log1pP EndPoint i
x) (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i)) =>
EndPoint i -> i
log1pP EndPoint i
y)) -- increasing
{-# INLINABLE log1pI #-}

-- abs x <= pi / 4
sin_small :: forall i. (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RoundedRing (EndPoint i), RealFloatConstants (EndPoint i)) => i -> i
sin_small :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
sin_small i
x = let xx :: i
xx = i
x forall a. Num a => a -> a -> a
* i
x
                  series :: Int -> i -> i
                  series :: Int -> i -> i
series Int
k i
acc | Int
k forall a. Eq a => a -> a -> Bool
== Int
0 = i
x forall a. Num a => a -> a -> a
* i
acc
                               | Bool
otherwise = Int -> i -> i
series (Int
kforall a. Num a => a -> a -> a
-Int
2) forall a b. (a -> b) -> a -> b
$ i
1 forall a. Num a => a -> a -> a
- i
xx forall a. Num a => a -> a -> a
* i
acc forall a. Fractional a => a -> a -> a
/ forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
k forall a. Num a => a -> a -> a
* (Int
kforall a. Num a => a -> a -> a
+Int
1))
              in Int -> i -> i
series Int
18 (forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval (-Rounded 'TowardNegInf (EndPoint i)
1) Rounded 'TowardInf (EndPoint i)
1)
{-# INLINABLE sin_small #-}

-- abs x <= pi / 4
cos_small :: forall i. (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RoundedRing (EndPoint i), RealFloatConstants (EndPoint i)) => i -> i
cos_small :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
cos_small i
x = let xx :: i
xx = i
x forall a. Num a => a -> a -> a
* i
x
                  series :: Int -> i -> i
                  series :: Int -> i -> i
series Int
k i
acc | Int
k forall a. Eq a => a -> a -> Bool
== Int
1 = i
acc
                               | Bool
otherwise = Int -> i -> i
series (Int
kforall a. Num a => a -> a -> a
-Int
2) forall a b. (a -> b) -> a -> b
$ i
1 forall a. Num a => a -> a -> a
- i
xx forall a. Num a => a -> a -> a
* i
acc forall a. Fractional a => a -> a -> a
/ forall a b. (Integral a, Num b) => a -> b
fromIntegral ((Int
kforall a. Num a => a -> a -> a
-Int
1) forall a. Num a => a -> a -> a
* (Int
kforall a. Num a => a -> a -> a
-Int
2))
              in Int -> i -> i
series Int
17 (forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval (-Rounded 'TowardNegInf (EndPoint i)
1) Rounded 'TowardInf (EndPoint i)
1)
{-# INLINABLE cos_small #-}

-- -pi <= x <= pi
-- x should be a small interval
sinP :: forall i. (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RoundedRing (EndPoint i), RealFloatConstants (EndPoint i)) => i -> i
sinP :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
sinP i
x | i
x forall i. IsInterval i => i -> i -> Bool
`weaklyLess` - i
three_pi_iv forall a. Fractional a => a -> a -> a
/ i
4 = - forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
sin_small (i
x forall a. Num a => a -> a -> a
+ i
pi_iv) -- -pi <= x <= -3/4*pi
       | i
x forall i. IsInterval i => i -> i -> Bool
`weaklyLess` - i
pi_iv forall a. Fractional a => a -> a -> a
/ i
2 = - forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
cos_small (- i
pi_iv forall a. Fractional a => a -> a -> a
/ i
2 forall a. Num a => a -> a -> a
- i
x) -- -3/4*pi <= x <= -pi/2
       | i
x forall i. IsInterval i => i -> i -> Bool
`weaklyLess` - i
pi_iv forall a. Fractional a => a -> a -> a
/ i
4 = - forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
cos_small (i
x forall a. Num a => a -> a -> a
+ i
pi_iv forall a. Fractional a => a -> a -> a
/ i
2) -- -pi <= x <= -pi/4
       | i
x forall i. IsInterval i => i -> i -> Bool
`weaklyLess` i
0 = - forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
sin_small (- i
x)
       | i
x forall i. IsInterval i => i -> i -> Bool
`weaklyLess` i
pi_iv forall a. Fractional a => a -> a -> a
/ i
4 = forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
sin_small i
x
       | i
x forall i. IsInterval i => i -> i -> Bool
`weaklyLess` i
pi_iv forall a. Fractional a => a -> a -> a
/ i
2 = forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
cos_small (i
pi_iv forall a. Fractional a => a -> a -> a
/ i
2 forall a. Num a => a -> a -> a
- i
x)
       | i
x forall i. IsInterval i => i -> i -> Bool
`weaklyLess` i
three_pi_iv forall a. Fractional a => a -> a -> a
/ i
4 = forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
cos_small (i
x forall a. Num a => a -> a -> a
- i
pi_iv forall a. Fractional a => a -> a -> a
/ i
2)
       | Bool
otherwise = forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
sin_small (i
pi_iv forall a. Num a => a -> a -> a
- i
x)
  where
    pi_iv :: i
    pi_iv :: i
pi_iv = forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval forall a. RealFloatConstants a => Rounded 'TowardNegInf a
pi_down forall a. RealFloatConstants a => Rounded 'TowardInf a
pi_up
    three_pi_iv :: i
    three_pi_iv :: i
three_pi_iv = forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval forall a. RealFloatConstants a => Rounded 'TowardNegInf a
three_pi_down forall a. RealFloatConstants a => Rounded 'TowardInf a
three_pi_up
    -- TODO: Is `weaklyLess` okay?
{-# INLINABLE sinP #-}

-- -pi <= x <= pi
-- x should be a small interval
cosP :: forall i. (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RoundedRing (EndPoint i), RealFloatConstants (EndPoint i)) => i -> i
cosP :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
cosP i
x | i
x forall i. IsInterval i => i -> i -> Bool
`weaklyLess` - i
three_pi_iv forall a. Fractional a => a -> a -> a
/ i
4 = - forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
cos_small (i
x forall a. Num a => a -> a -> a
+ i
pi_iv) -- -pi <= x <= -3/4*pi
       | i
x forall i. IsInterval i => i -> i -> Bool
`weaklyLess` - i
pi_iv forall a. Fractional a => a -> a -> a
/ i
2 = - forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
sin_small (- i
pi_iv forall a. Fractional a => a -> a -> a
/ i
2 forall a. Num a => a -> a -> a
- i
x) -- -3/4*pi <= x <= -pi/2
       | i
x forall i. IsInterval i => i -> i -> Bool
`weaklyLess` - i
pi_iv forall a. Fractional a => a -> a -> a
/ i
4 = forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
sin_small (i
x forall a. Num a => a -> a -> a
+ i
pi_iv forall a. Fractional a => a -> a -> a
/ i
2) -- -pi <= x <= -pi/4
       | i
x forall i. IsInterval i => i -> i -> Bool
`weaklyLess` i
0 = forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
cos_small (- i
x)
       | i
x forall i. IsInterval i => i -> i -> Bool
`weaklyLess` i
pi_iv forall a. Fractional a => a -> a -> a
/ i
4 = forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
cos_small i
x
       | i
x forall i. IsInterval i => i -> i -> Bool
`weaklyLess` i
pi_iv forall a. Fractional a => a -> a -> a
/ i
2 = forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
sin_small (i
pi_iv forall a. Fractional a => a -> a -> a
/ i
2 forall a. Num a => a -> a -> a
- i
x)
       | i
x forall i. IsInterval i => i -> i -> Bool
`weaklyLess` i
three_pi_iv forall a. Fractional a => a -> a -> a
/ i
4 = - forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
sin_small (i
x forall a. Num a => a -> a -> a
- i
pi_iv forall a. Fractional a => a -> a -> a
/ i
2)
       | Bool
otherwise = - forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
cos_small (i
pi_iv forall a. Num a => a -> a -> a
- i
x)
  where
    pi_iv :: i
    pi_iv :: i
pi_iv = forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval forall a. RealFloatConstants a => Rounded 'TowardNegInf a
pi_down forall a. RealFloatConstants a => Rounded 'TowardInf a
pi_up
    three_pi_iv :: i
    three_pi_iv :: i
three_pi_iv = forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval forall a. RealFloatConstants a => Rounded 'TowardNegInf a
three_pi_down forall a. RealFloatConstants a => Rounded 'TowardInf a
three_pi_up
    -- TODO: Is `weaklyLess` okay?
{-# INLINABLE cosP #-}

sinI :: forall i. (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RoundedRing (EndPoint i), RealFloatConstants (EndPoint i)) => i -> i
sinI :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
sinI i
t = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall i.
IsInterval i =>
(Rounded 'TowardNegInf (EndPoint i)
 -> Rounded 'TowardInf (EndPoint i) -> i)
-> i -> i
withEndPoints i
t forall a b. (a -> b) -> a -> b
$ \(Rounded EndPoint i
x) (Rounded EndPoint i
y) ->
  if forall a. RealFloat a => a -> Bool
isInfinite EndPoint i
x Bool -> Bool -> Bool
|| forall a. RealFloat a => a -> Bool
isInfinite EndPoint i
y
  then i
wholeRange
  else forall a b c. (a -> b -> c) -> b -> a -> c
flip forall i.
IsInterval i =>
(Rounded 'TowardNegInf (EndPoint i)
 -> Rounded 'TowardInf (EndPoint i) -> i)
-> i -> i
withEndPoints (forall i. IsInterval i => EndPoint i -> i
singleton EndPoint i
x forall a. Fractional a => a -> a -> a
/ (i
2 forall a. Num a => a -> a -> a
* i
pi_iv)) forall a b. (a -> b) -> a -> b
$ \(Rounded EndPoint i
x0) (Rounded EndPoint i
_) ->
    let n :: Integer
n = forall a b. (RealFrac a, Integral b) => a -> b
round EndPoint i
x0
        t' :: i
t' = i
t forall a. Num a => a -> a -> a
- i
2 forall a. Num a => a -> a -> a
* i
pi_iv forall a. Num a => a -> a -> a
* forall a. Num a => Integer -> a
fromInteger Integer
n
    in forall a b c. (a -> b -> c) -> b -> a -> c
flip forall i.
IsInterval i =>
(Rounded 'TowardNegInf (EndPoint i)
 -> Rounded 'TowardInf (EndPoint i) -> i)
-> i -> i
withEndPoints i
t' forall a b. (a -> b) -> a -> b
$ \(Rounded EndPoint i
x') (Rounded EndPoint i
y') ->
      if EndPoint i
y' forall a. Num a => a -> a -> a
- EndPoint i
x' forall a. Ord a => a -> a -> Bool
>= forall (r :: RoundingMode) a. Rounded r a -> a
getRounded (Rounded 'TowardInf (EndPoint i)
2 forall a. Num a => a -> a -> a
* forall a. RealFloatConstants a => Rounded 'TowardInf a
pi_up)
      then i
wholeRange
      else -- -pi <= x' <= pi, x' <= y' <= 3 * pi
        let include_minus_1 :: Bool
include_minus_1 = i
minus_half_pi_iv forall i. IsInterval i => i -> i -> Bool
`subset` i
t' Bool -> Bool -> Bool
|| i
three_pi_2_iv forall i. IsInterval i => i -> i -> Bool
`subset` i
t'
            include_plus_1 :: Bool
include_plus_1 = i
pi_iv forall a. Fractional a => a -> a -> a
/ i
2 forall i. IsInterval i => i -> i -> Bool
`subset` i
t' Bool -> Bool -> Bool
|| i
five_pi_2_iv forall i. IsInterval i => i -> i -> Bool
`subset` i
t'
            u :: i
u = forall i. IsInterval i => i -> i -> i
hull (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
sinP forall a b. (a -> b) -> a -> b
$ forall i. IsInterval i => EndPoint i -> i
singleton EndPoint i
x') forall a b. (a -> b) -> a -> b
$ forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
sinP (if EndPoint i
y forall a. Ord a => a -> a -> Bool
<= forall (r :: RoundingMode) a. Rounded r a -> a
getRounded forall a. RealFloatConstants a => Rounded 'TowardNegInf a
pi_down then forall i. IsInterval i => EndPoint i -> i
singleton EndPoint i
y' else forall i. IsInterval i => EndPoint i -> i
singleton EndPoint i
y' forall a. Num a => a -> a -> a
- i
2 forall a. Num a => a -> a -> a
* i
pi_iv)
            v :: i
v | Bool
include_minus_1 = forall i. IsInterval i => i -> i -> i
hull (-i
1) i
u
              | Bool
otherwise = i
u
            w :: i
w | Bool
include_plus_1 = forall i. IsInterval i => i -> i -> i
hull i
1 i
v
              | Bool
otherwise = i
v
        in forall i. IsInterval i => i -> i -> i
intersection i
wholeRange i
w
  where
    pi_iv :: i
    pi_iv :: i
pi_iv = forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval forall a. RealFloatConstants a => Rounded 'TowardNegInf a
pi_down forall a. RealFloatConstants a => Rounded 'TowardInf a
pi_up
    minus_half_pi_iv :: i
    minus_half_pi_iv :: i
minus_half_pi_iv = - i
pi_iv forall a. Fractional a => a -> a -> a
/ i
2
    three_pi_2_iv :: i
    three_pi_2_iv :: i
three_pi_2_iv = forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval forall a. RealFloatConstants a => Rounded 'TowardNegInf a
three_pi_down forall a. RealFloatConstants a => Rounded 'TowardInf a
three_pi_up forall a. Fractional a => a -> a -> a
/ i
2
    five_pi_2_iv :: i
    five_pi_2_iv :: i
five_pi_2_iv = forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval forall a. RealFloatConstants a => Rounded 'TowardNegInf a
five_pi_down forall a. RealFloatConstants a => Rounded 'TowardInf a
five_pi_up forall a. Fractional a => a -> a -> a
/ i
2
    wholeRange :: i
    wholeRange :: i
wholeRange = forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval (-Rounded 'TowardNegInf (EndPoint i)
1) Rounded 'TowardInf (EndPoint i)
1
{-# INLINABLE sinI #-}

cosI :: forall i. (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RoundedRing (EndPoint i), RealFloatConstants (EndPoint i)) => i -> i
cosI :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
cosI i
t = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall i.
IsInterval i =>
(Rounded 'TowardNegInf (EndPoint i)
 -> Rounded 'TowardInf (EndPoint i) -> i)
-> i -> i
withEndPoints i
t forall a b. (a -> b) -> a -> b
$ \(Rounded EndPoint i
x) (Rounded EndPoint i
y) ->
  if forall a. RealFloat a => a -> Bool
isInfinite EndPoint i
x Bool -> Bool -> Bool
|| forall a. RealFloat a => a -> Bool
isInfinite EndPoint i
y
  then i
wholeRange
  else forall a b c. (a -> b -> c) -> b -> a -> c
flip forall i.
IsInterval i =>
(Rounded 'TowardNegInf (EndPoint i)
 -> Rounded 'TowardInf (EndPoint i) -> i)
-> i -> i
withEndPoints (forall i. IsInterval i => EndPoint i -> i
singleton EndPoint i
x forall a. Fractional a => a -> a -> a
/ (i
2 forall a. Num a => a -> a -> a
* i
pi_iv)) forall a b. (a -> b) -> a -> b
$ \(Rounded EndPoint i
x0) (Rounded EndPoint i
_) ->
    let n :: Integer
n = forall a b. (RealFrac a, Integral b) => a -> b
round EndPoint i
x0
        t' :: i
t' = i
t forall a. Num a => a -> a -> a
- i
2 forall a. Num a => a -> a -> a
* i
pi_iv forall a. Num a => a -> a -> a
* forall a. Num a => Integer -> a
fromInteger Integer
n
    in forall a b c. (a -> b -> c) -> b -> a -> c
flip forall i.
IsInterval i =>
(Rounded 'TowardNegInf (EndPoint i)
 -> Rounded 'TowardInf (EndPoint i) -> i)
-> i -> i
withEndPoints i
t' forall a b. (a -> b) -> a -> b
$ \(Rounded EndPoint i
x') (Rounded EndPoint i
y') ->
      if EndPoint i
y' forall a. Num a => a -> a -> a
- EndPoint i
x' forall a. Ord a => a -> a -> Bool
>= forall (r :: RoundingMode) a. Rounded r a -> a
getRounded (Rounded 'TowardInf (EndPoint i)
2 forall a. Num a => a -> a -> a
* forall a. RealFloatConstants a => Rounded 'TowardInf a
pi_up)
      then i
wholeRange
      else -- -pi <= x' <= pi, x' <= y' <= 3 * pi
        let include_minus_1 :: Bool
include_minus_1 = -i
pi_iv forall i. IsInterval i => i -> i -> Bool
`subset` i
t' Bool -> Bool -> Bool
|| i
pi_iv forall i. IsInterval i => i -> i -> Bool
`subset` i
t' Bool -> Bool -> Bool
|| i
three_pi_iv forall i. IsInterval i => i -> i -> Bool
`subset` i
t'
            include_plus_1 :: Bool
include_plus_1 = i
0 forall i. IsInterval i => i -> i -> Bool
`subset` i
t' Bool -> Bool -> Bool
|| i
2 forall a. Num a => a -> a -> a
* i
pi_iv forall i. IsInterval i => i -> i -> Bool
`subset` i
t'
            u :: i
u = forall i. IsInterval i => i -> i -> i
hull (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
cosP forall a b. (a -> b) -> a -> b
$ forall i. IsInterval i => EndPoint i -> i
singleton EndPoint i
x') forall a b. (a -> b) -> a -> b
$ forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
cosP (if EndPoint i
y forall a. Ord a => a -> a -> Bool
<= forall (r :: RoundingMode) a. Rounded r a -> a
getRounded forall a. RealFloatConstants a => Rounded 'TowardNegInf a
pi_down then forall i. IsInterval i => EndPoint i -> i
singleton EndPoint i
y' else forall i. IsInterval i => EndPoint i -> i
singleton EndPoint i
y' forall a. Num a => a -> a -> a
- i
2 forall a. Num a => a -> a -> a
* i
pi_iv)
            v :: i
v | Bool
include_minus_1 = forall i. IsInterval i => i -> i -> i
hull (-i
1) i
u
              | Bool
otherwise = i
u
            w :: i
w | Bool
include_plus_1 = forall i. IsInterval i => i -> i -> i
hull i
1 i
v
              | Bool
otherwise = i
v
        in forall i. IsInterval i => i -> i -> i
intersection i
wholeRange i
w
  where
    pi_iv :: i
    pi_iv :: i
pi_iv = forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval forall a. RealFloatConstants a => Rounded 'TowardNegInf a
pi_down forall a. RealFloatConstants a => Rounded 'TowardInf a
pi_up
    three_pi_iv :: i
    three_pi_iv :: i
three_pi_iv = forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval forall a. RealFloatConstants a => Rounded 'TowardNegInf a
three_pi_down forall a. RealFloatConstants a => Rounded 'TowardInf a
three_pi_up
    wholeRange :: i
    wholeRange :: i
wholeRange = forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval (-Rounded 'TowardNegInf (EndPoint i)
1) Rounded 'TowardInf (EndPoint i)
1
{-# INLINABLE cosI #-}

tanI :: forall i. (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RoundedRing (EndPoint i), RealFloatConstants (EndPoint i)) => i -> i
tanI :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
tanI i
t = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall i.
IsInterval i =>
(Rounded 'TowardNegInf (EndPoint i)
 -> Rounded 'TowardInf (EndPoint i) -> i)
-> i -> i
withEndPoints i
t forall a b. (a -> b) -> a -> b
$ \(Rounded EndPoint i
x) (Rounded EndPoint i
y) ->
  if forall a. RealFloat a => a -> Bool
isInfinite EndPoint i
x Bool -> Bool -> Bool
|| forall a. RealFloat a => a -> Bool
isInfinite EndPoint i
y
  then i
wholeRange
  else forall a b c. (a -> b -> c) -> b -> a -> c
flip forall i.
IsInterval i =>
(Rounded 'TowardNegInf (EndPoint i)
 -> Rounded 'TowardInf (EndPoint i) -> i)
-> i -> i
withEndPoints (i
t forall a. Fractional a => a -> a -> a
/ i
pi_iv) forall a b. (a -> b) -> a -> b
$ \(Rounded EndPoint i
x0) (Rounded EndPoint i
_) ->
    let n :: Integer
n = forall a b. (RealFrac a, Integral b) => a -> b
round EndPoint i
x0 -- abs (x - n) <= 1/2
        t' :: i
t' = i
t forall a. Num a => a -> a -> a
- i
pi_iv forall a. Num a => a -> a -> a
* forall a. Num a => Integer -> a
fromInteger Integer
n
    in forall a b c. (a -> b -> c) -> b -> a -> c
flip forall i.
IsInterval i =>
(Rounded 'TowardNegInf (EndPoint i)
 -> Rounded 'TowardInf (EndPoint i) -> i)
-> i -> i
withEndPoints i
t' forall a b. (a -> b) -> a -> b
$ \(Rounded EndPoint i
x') (Rounded EndPoint i
y') ->
      -- -pi/2 < x' < pi/2
      if EndPoint i
y' forall a. Ord a => a -> a -> Bool
>= forall (r :: RoundingMode) a. Rounded r a -> a
getRounded forall a. RealFloatConstants a => Rounded 'TowardInf a
pi_up forall a. Fractional a => a -> a -> a
/ EndPoint i
2
      then i
wholeRange
      else let lb :: i
lb = forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
sinP (forall i. IsInterval i => EndPoint i -> i
singleton EndPoint i
x') forall a. Fractional a => a -> a -> a
/ forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
cosP (forall i. IsInterval i => EndPoint i -> i
singleton EndPoint i
x')
               ub :: i
ub = forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
sinP (forall i. IsInterval i => EndPoint i -> i
singleton EndPoint i
y') forall a. Fractional a => a -> a -> a
/ forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
cosP (forall i. IsInterval i => EndPoint i -> i
singleton EndPoint i
y')
               -- lb <= ub
           in forall i. IsInterval i => i -> i -> i
hull i
lb i
ub -- increasing in (-pi/2,pi/2)
  where
    pi_iv :: i
    pi_iv :: i
pi_iv = forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval forall a. RealFloatConstants a => Rounded 'TowardNegInf a
pi_down forall a. RealFloatConstants a => Rounded 'TowardInf a
pi_up
    wholeRange :: i
    wholeRange :: i
wholeRange = forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval (forall (r :: RoundingMode) a. a -> Rounded r a
Rounded forall a. RealFloatConstants a => a
negativeInfinity) (forall (r :: RoundingMode) a. a -> Rounded r a
Rounded forall a. RealFloatConstants a => a
positiveInfinity)
{-# INLINABLE tanI #-}

-- abs x <= 1 / (1 + sqrt 2) = sqrt 2 - 1
atan_small :: forall i. (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RoundedRing (EndPoint i), RealFloatConstants (EndPoint i)) => i -> i
atan_small :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
atan_small i
x = let n :: Int
n = Int
39 -- odd
               in Int -> i -> i
series Int
n (forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval (-Rounded 'TowardNegInf (EndPoint i)
1) Rounded 'TowardInf (EndPoint i)
1 forall a. Fractional a => a -> a -> a
/ forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n)
  where
    xx :: i
xx = i
x forall a. Num a => a -> a -> a
* i
x
    series :: Int -> i -> i
    series :: Int -> i -> i
series Int
k i
acc | Int
k forall a. Eq a => a -> a -> Bool
== Int
1 = i
x forall a. Num a => a -> a -> a
* i
acc
                 | Bool
otherwise = Int -> i -> i
series (Int
kforall a. Num a => a -> a -> a
-Int
2) forall a b. (a -> b) -> a -> b
$ forall a. Fractional a => a -> a
recip (forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
kforall a. Num a => a -> a -> a
-Int
2)) forall a. Num a => a -> a -> a
- i
xx forall a. Num a => a -> a -> a
* i
acc
{-# INLINABLE atan_small #-}

atanP :: forall i. (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RoundedRing (EndPoint i), RealFloatConstants (EndPoint i)) => EndPoint i -> i
atanP :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
EndPoint i -> i
atanP EndPoint i
x |   forall (r :: RoundingMode) a. Rounded r a -> a
getRounded (Rounded 'TowardInf (EndPoint i)
1 forall a. Num a => a -> a -> a
+ forall a. RealFloatConstants a => Rounded 'TowardInf a
sqrt2_up)   forall a. Ord a => a -> a -> Bool
<= EndPoint i
x =   i
pi_iv forall a. Fractional a => a -> a -> a
/ i
2 forall a. Num a => a -> a -> a
- forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
atan_small (forall a. Fractional a => a -> a
recip i
x')
        |   forall (r :: RoundingMode) a. Rounded r a -> a
getRounded forall a. RealFloatConstants a => Rounded 'TowardInf a
sqrt2m1_up       forall a. Ord a => a -> a -> Bool
<= EndPoint i
x =   i
pi_iv forall a. Fractional a => a -> a -> a
/ i
4 forall a. Num a => a -> a -> a
+ forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
atan_small ((i
x' forall a. Num a => a -> a -> a
- i
1) forall a. Fractional a => a -> a -> a
/ (i
x' forall a. Num a => a -> a -> a
+ i
1))
        | - forall (r :: RoundingMode) a. Rounded r a -> a
getRounded forall a. RealFloatConstants a => Rounded 'TowardNegInf a
sqrt2m1_down     forall a. Ord a => a -> a -> Bool
<= EndPoint i
x =               forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
atan_small i
x'
        | - forall (r :: RoundingMode) a. Rounded r a -> a
getRounded (forall a. RealFloatConstants a => Rounded 'TowardNegInf a
sqrt2_down forall a. Num a => a -> a -> a
+ Rounded 'TowardNegInf (EndPoint i)
1) forall a. Ord a => a -> a -> Bool
<= EndPoint i
x = - i
pi_iv forall a. Fractional a => a -> a -> a
/ i
4 forall a. Num a => a -> a -> a
+ forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
atan_small ((i
1 forall a. Num a => a -> a -> a
+ i
x') forall a. Fractional a => a -> a -> a
/ (i
1 forall a. Num a => a -> a -> a
- i
x'))
        |   Bool
otherwise                        = - i
pi_iv forall a. Fractional a => a -> a -> a
/ i
2 forall a. Num a => a -> a -> a
- forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
atan_small (forall a. Fractional a => a -> a
recip i
x')
  where
    x' :: i
x' = forall i. IsInterval i => EndPoint i -> i
singleton EndPoint i
x
    pi_iv :: i
    pi_iv :: i
pi_iv = forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval forall a. RealFloatConstants a => Rounded 'TowardNegInf a
pi_down forall a. RealFloatConstants a => Rounded 'TowardInf a
pi_up
{-# INLINABLE atanP #-}

atanI :: forall i. (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RoundedRing (EndPoint i), RealFloatConstants (EndPoint i)) => i -> i
atanI :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
atanI = forall i.
IsInterval i =>
(Rounded 'TowardNegInf (EndPoint i)
 -> Rounded 'TowardInf (EndPoint i) -> i)
-> i -> i
withEndPoints (\(Rounded EndPoint i
x) (Rounded EndPoint i
y) -> forall i. IsInterval i => i -> i -> i
hull (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
EndPoint i -> i
atanP EndPoint i
x) (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
EndPoint i -> i
atanP EndPoint i
y)) -- increasing
{-# INLINABLE atanI #-}

asinP :: forall i. (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RoundedRing (EndPoint i), RoundedSqrt (EndPoint i), RealFloatConstants (EndPoint i)) => EndPoint i -> i
asinP :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RoundedSqrt (EndPoint i), RealFloatConstants (EndPoint i)) =>
EndPoint i -> i
asinP EndPoint i
x | EndPoint i
x forall a. Ord a => a -> a -> Bool
< -EndPoint i
1 Bool -> Bool -> Bool
|| EndPoint i
1 forall a. Ord a => a -> a -> Bool
< EndPoint i
x = forall a. (?callStack::CallStack) => [Char] -> a
error [Char]
"asin"
        | EndPoint i
x forall a. Eq a => a -> a -> Bool
== -EndPoint i
1 = - i
pi_iv forall a. Fractional a => a -> a -> a
/ i
2
        | EndPoint i
x forall a. Eq a => a -> a -> Bool
== EndPoint i
1  =   i
pi_iv forall a. Fractional a => a -> a -> a
/ i
2
        | Bool
otherwise = forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
atanI (i
x' forall a. Fractional a => a -> a -> a
/ forall i. (IsInterval i, RoundedSqrt (EndPoint i)) => i -> i
sqrtI (i
1 forall a. Num a => a -> a -> a
- i
x'forall a. Num a => a -> a -> a
*i
x')) -- TODO: Use sqrt ((1+x')*(1-x')) when |x| is near 1
  where
    x' :: i
x' = forall i. IsInterval i => EndPoint i -> i
singleton EndPoint i
x
    pi_iv :: i
    pi_iv :: i
pi_iv = forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval forall a. RealFloatConstants a => Rounded 'TowardNegInf a
pi_down forall a. RealFloatConstants a => Rounded 'TowardInf a
pi_up
{-# INLINABLE asinP #-}

asinI :: forall i. (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RoundedRing (EndPoint i), RoundedSqrt (EndPoint i), RealFloatConstants (EndPoint i)) => i -> i
asinI :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RoundedSqrt (EndPoint i), RealFloatConstants (EndPoint i)) =>
i -> i
asinI = forall i.
IsInterval i =>
(Rounded 'TowardNegInf (EndPoint i)
 -> Rounded 'TowardInf (EndPoint i) -> i)
-> i -> i
withEndPoints (\(Rounded EndPoint i
x) (Rounded EndPoint i
y) -> forall i. IsInterval i => i -> i -> i
hull (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RoundedSqrt (EndPoint i), RealFloatConstants (EndPoint i)) =>
EndPoint i -> i
asinP EndPoint i
x) (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RoundedSqrt (EndPoint i), RealFloatConstants (EndPoint i)) =>
EndPoint i -> i
asinP EndPoint i
y)) -- increasing
{-# INLINABLE asinI #-}

acosP :: forall i. (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RoundedRing (EndPoint i), RoundedSqrt (EndPoint i), RealFloatConstants (EndPoint i)) => EndPoint i -> i
acosP :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RoundedSqrt (EndPoint i), RealFloatConstants (EndPoint i)) =>
EndPoint i -> i
acosP EndPoint i
x | EndPoint i
x forall a. Ord a => a -> a -> Bool
< -EndPoint i
1 Bool -> Bool -> Bool
|| EndPoint i
1 forall a. Ord a => a -> a -> Bool
< EndPoint i
x = forall a. (?callStack::CallStack) => [Char] -> a
error [Char]
"asin"
        | EndPoint i
x forall a. Eq a => a -> a -> Bool
== -EndPoint i
1 = i
pi_iv
        | EndPoint i
x forall a. Eq a => a -> a -> Bool
== EndPoint i
1  = i
0
        | Bool
otherwise = case i
x' forall a. Fractional a => a -> a -> a
/ forall i. (IsInterval i, RoundedSqrt (EndPoint i)) => i -> i
sqrtI (i
1 forall a. Num a => a -> a -> a
- i
x'forall a. Num a => a -> a -> a
*i
x') of  -- TODO: Use sqrt ((1+x')*(1-x')) when |x| is near 1
                        i
y' |   i
one_plus_sqrt2  forall i. IsInterval i => i -> i -> Bool
`weaklyLess` i
y' -> forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
atan_small (forall a. Fractional a => a -> a
recip i
y')
                           |   i
sqrt2_minus_one forall i. IsInterval i => i -> i -> Bool
`weaklyLess` i
y' -> i
pi_iv forall a. Fractional a => a -> a -> a
/ i
4 forall a. Num a => a -> a -> a
- forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
atan_small ((i
y' forall a. Num a => a -> a -> a
- i
1) forall a. Fractional a => a -> a -> a
/ (i
y' forall a. Num a => a -> a -> a
+ i
1))
                           | - i
sqrt2_minus_one forall i. IsInterval i => i -> i -> Bool
`weaklyLess` i
y' -> i
pi_iv forall a. Fractional a => a -> a -> a
/ i
2 forall a. Num a => a -> a -> a
-  forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
atan_small i
y'
                           | - i
one_plus_sqrt2  forall i. IsInterval i => i -> i -> Bool
`weaklyLess` i
y' -> i
three_pi_iv forall a. Fractional a => a -> a -> a
/ i
4 forall a. Num a => a -> a -> a
- forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
atan_small ((i
1 forall a. Num a => a -> a -> a
+ i
y') forall a. Fractional a => a -> a -> a
/ (i
1 forall a. Num a => a -> a -> a
- i
y'))
                           |   Bool
otherwise                       -> i
pi_iv forall a. Num a => a -> a -> a
+ forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RealFloatConstants (EndPoint i)) =>
i -> i
atan_small (forall a. Fractional a => a -> a
recip i
y')
                      -- == pi_iv / 2 - atanI y'
  where
    x' :: i
x' = forall i. IsInterval i => EndPoint i -> i
singleton EndPoint i
x
    pi_iv :: i
    pi_iv :: i
pi_iv = forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval forall a. RealFloatConstants a => Rounded 'TowardNegInf a
pi_down forall a. RealFloatConstants a => Rounded 'TowardInf a
pi_up
    three_pi_iv :: i
    three_pi_iv :: i
three_pi_iv = forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval forall a. RealFloatConstants a => Rounded 'TowardNegInf a
three_pi_down forall a. RealFloatConstants a => Rounded 'TowardInf a
three_pi_up
    one_plus_sqrt2 :: i
    one_plus_sqrt2 :: i
one_plus_sqrt2 = i
1 forall a. Num a => a -> a -> a
+ forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval forall a. RealFloatConstants a => Rounded 'TowardNegInf a
sqrt2_down forall a. RealFloatConstants a => Rounded 'TowardInf a
sqrt2_up
    sqrt2_minus_one :: i
    sqrt2_minus_one :: i
sqrt2_minus_one = forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval forall a. RealFloatConstants a => Rounded 'TowardNegInf a
sqrt2m1_down forall a. RealFloatConstants a => Rounded 'TowardInf a
sqrt2m1_up
{-# INLINABLE acosP #-}

acosI :: forall i. (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RoundedRing (EndPoint i), RoundedSqrt (EndPoint i), RealFloatConstants (EndPoint i)) => i -> i
acosI :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RoundedSqrt (EndPoint i), RealFloatConstants (EndPoint i)) =>
i -> i
acosI = forall i.
IsInterval i =>
(Rounded 'TowardNegInf (EndPoint i)
 -> Rounded 'TowardInf (EndPoint i) -> i)
-> i -> i
withEndPoints (\(Rounded EndPoint i
x) (Rounded EndPoint i
y) -> forall i. IsInterval i => i -> i -> i
hull (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RoundedSqrt (EndPoint i), RealFloatConstants (EndPoint i)) =>
EndPoint i -> i
acosP EndPoint i
x) (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RoundedRing (EndPoint i),
 RoundedSqrt (EndPoint i), RealFloatConstants (EndPoint i)) =>
EndPoint i -> i
acosP EndPoint i
y)) -- decreasing
{-# INLINABLE acosI #-}

sinhP :: (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RealFloatConstants (EndPoint i), RoundedFractional (EndPoint i)) => EndPoint i -> i
sinhP :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
EndPoint i -> i
sinhP EndPoint i
x | EndPoint i
x forall a. Ord a => a -> a -> Bool
>= EndPoint i
0 = let y :: i
y = forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
EndPoint i -> i
expP EndPoint i
x
                   in (i
y forall a. Num a => a -> a -> a
- forall a. Fractional a => a -> a
recip i
y) forall a. Fractional a => a -> a -> a
/ i
2
        | Bool
otherwise = let y :: i
y = forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
EndPoint i -> i
expP (- EndPoint i
x)
                      in (forall a. Fractional a => a -> a
recip i
y forall a. Num a => a -> a -> a
- i
y) forall a. Fractional a => a -> a -> a
/ i
2
        -- TODO: precision when x ~ 0
{-# INLINABLE sinhP #-}

sinhI :: (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RealFloatConstants (EndPoint i), RoundedFractional (EndPoint i)) => i -> i
sinhI :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
i -> i
sinhI = forall i.
IsInterval i =>
(Rounded 'TowardNegInf (EndPoint i)
 -> Rounded 'TowardInf (EndPoint i) -> i)
-> i -> i
withEndPoints (\(Rounded EndPoint i
x) (Rounded EndPoint i
y) -> forall i. IsInterval i => i -> i -> i
hull (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
EndPoint i -> i
sinhP EndPoint i
x) (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
EndPoint i -> i
sinhP EndPoint i
y)) -- increasing
{-# INLINABLE sinhI #-}

coshP :: (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RealFloatConstants (EndPoint i), RoundedFractional (EndPoint i)) => EndPoint i -> i
coshP :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
EndPoint i -> i
coshP EndPoint i
x | EndPoint i
x forall a. Ord a => a -> a -> Bool
>= EndPoint i
0 = let y :: i
y = forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
EndPoint i -> i
expP EndPoint i
x
                   in (i
y forall a. Num a => a -> a -> a
+ forall a. Fractional a => a -> a
recip i
y) forall a. Fractional a => a -> a -> a
/ i
2
        | Bool
otherwise = let y :: i
y = forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
EndPoint i -> i
expP (- EndPoint i
x)
                      in (forall a. Fractional a => a -> a
recip i
y forall a. Num a => a -> a -> a
+ i
y) forall a. Fractional a => a -> a -> a
/ i
2
{-# INLINABLE coshP #-}

coshI :: (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RealFloatConstants (EndPoint i), RoundedFractional (EndPoint i)) => i -> i
coshI :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
i -> i
coshI = forall i.
IsInterval i =>
(Rounded 'TowardNegInf (EndPoint i)
 -> Rounded 'TowardInf (EndPoint i) -> i)
-> i -> i
withEndPoints forall a b. (a -> b) -> a -> b
$ \(Rounded EndPoint i
x) (Rounded EndPoint i
y) ->
                          let z :: i
z = forall i. IsInterval i => i -> i -> i
hull (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
EndPoint i -> i
coshP EndPoint i
x) (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
EndPoint i -> i
coshP EndPoint i
y)
                          in if EndPoint i
x forall a. Ord a => a -> a -> Bool
<= EndPoint i
0 Bool -> Bool -> Bool
&& EndPoint i
0 forall a. Ord a => a -> a -> Bool
<= EndPoint i
y
                             then forall i. IsInterval i => i -> i -> i
hull i
0 i
z
                             else i
z
{-# INLINABLE coshI #-}

tanhP :: (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RealFloatConstants (EndPoint i), RoundedFractional (EndPoint i)) => EndPoint i -> i
tanhP :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
EndPoint i -> i
tanhP EndPoint i
x | -EndPoint i
0.5 forall a. Ord a => a -> a -> Bool
<= EndPoint i
x Bool -> Bool -> Bool
&& EndPoint i
x forall a. Ord a => a -> a -> Bool
<= EndPoint i
0.5 = forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
EndPoint i -> i
sinhP EndPoint i
x forall a. Fractional a => a -> a -> a
/ forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
EndPoint i -> i
coshP EndPoint i
x
        | EndPoint i
0 forall a. Ord a => a -> a -> Bool
< EndPoint i
x = i
1 forall a. Num a => a -> a -> a
- i
2 forall a. Fractional a => a -> a -> a
/ (i
1 forall a. Num a => a -> a -> a
+ forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
EndPoint i -> i
expP (EndPoint i
2 forall a. Num a => a -> a -> a
* EndPoint i
x)) -- assuming 2*x is exact
        | Bool
otherwise = i
2 forall a. Fractional a => a -> a -> a
/ (i
1 forall a. Num a => a -> a -> a
+ forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
EndPoint i -> i
expP (- EndPoint i
2 forall a. Num a => a -> a -> a
* EndPoint i
x)) forall a. Num a => a -> a -> a
- i
1 -- assuming 2*x is exact
{-# INLINABLE tanhP #-}

tanhI :: (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RealFloatConstants (EndPoint i), RoundedFractional (EndPoint i)) => i -> i
tanhI :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
i -> i
tanhI = forall i.
IsInterval i =>
(Rounded 'TowardNegInf (EndPoint i)
 -> Rounded 'TowardInf (EndPoint i) -> i)
-> i -> i
withEndPoints forall a b. (a -> b) -> a -> b
$ \(Rounded EndPoint i
x) (Rounded EndPoint i
y) -> forall i. IsInterval i => i -> i -> i
hull (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
EndPoint i -> i
tanhP EndPoint i
x) (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedFractional (EndPoint i)) =>
EndPoint i -> i
tanhP EndPoint i
y) -- increasing
{-# INLINABLE tanhI #-}

asinhP :: (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RealFloatConstants (EndPoint i), RoundedSqrt (EndPoint i)) => EndPoint i -> i
asinhP :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedSqrt (EndPoint i)) =>
EndPoint i -> i
asinhP EndPoint i
x = let x' :: i
x' = forall i. IsInterval i => EndPoint i -> i
singleton EndPoint i
x
           in forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i)) =>
i -> i
logI (i
x' forall a. Num a => a -> a -> a
+ forall i. (IsInterval i, RoundedSqrt (EndPoint i)) => i -> i
sqrtI (i
1 forall a. Num a => a -> a -> a
+ i
x' forall a b. (Num a, Integral b) => a -> b -> a
^ (Int
2 :: Int)))
-- TODO: precision when x ~ 0
{-# INLINABLE asinhP #-}

asinhI :: (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RealFloatConstants (EndPoint i), RoundedSqrt (EndPoint i)) => i -> i
asinhI :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedSqrt (EndPoint i)) =>
i -> i
asinhI = forall i.
IsInterval i =>
(Rounded 'TowardNegInf (EndPoint i)
 -> Rounded 'TowardInf (EndPoint i) -> i)
-> i -> i
withEndPoints forall a b. (a -> b) -> a -> b
$ \(Rounded EndPoint i
x) (Rounded EndPoint i
y) -> forall i. IsInterval i => i -> i -> i
hull (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedSqrt (EndPoint i)) =>
EndPoint i -> i
asinhP EndPoint i
x) (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedSqrt (EndPoint i)) =>
EndPoint i -> i
asinhP EndPoint i
y) -- increasing
{-# INLINABLE asinhI #-}

acoshP :: (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RealFloatConstants (EndPoint i), RoundedSqrt (EndPoint i)) => EndPoint i -> i
acoshP :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedSqrt (EndPoint i)) =>
EndPoint i -> i
acoshP EndPoint i
x | EndPoint i
x forall a. Ord a => a -> a -> Bool
< EndPoint i
1 = forall a. (?callStack::CallStack) => [Char] -> a
error [Char]
"acosh: domain"
         | Bool
otherwise = let x' :: i
x' = forall i. IsInterval i => EndPoint i -> i
singleton EndPoint i
x
                       in forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i)) =>
i -> i
logI (i
x' forall a. Num a => a -> a -> a
+ forall i. (IsInterval i, RoundedSqrt (EndPoint i)) => i -> i
sqrtI (i
x' forall a b. (Num a, Integral b) => a -> b -> a
^ (Int
2 :: Int) forall a. Num a => a -> a -> a
- i
1))
-- TODO: precision when x ~ 1
{-# INLINABLE acoshP #-}

acoshI :: (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RealFloatConstants (EndPoint i), RoundedSqrt (EndPoint i)) => i -> i
acoshI :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedSqrt (EndPoint i)) =>
i -> i
acoshI = forall i.
IsInterval i =>
(Rounded 'TowardNegInf (EndPoint i)
 -> Rounded 'TowardInf (EndPoint i) -> i)
-> i -> i
withEndPoints forall a b. (a -> b) -> a -> b
$ \(Rounded EndPoint i
x) (Rounded EndPoint i
y) -> forall i. IsInterval i => i -> i -> i
hull (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedSqrt (EndPoint i)) =>
EndPoint i -> i
acoshP EndPoint i
x) (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i),
 RoundedSqrt (EndPoint i)) =>
EndPoint i -> i
acoshP EndPoint i
y) -- increasing
{-# INLINABLE acoshI #-}

atanhP :: (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RealFloatConstants (EndPoint i)) => EndPoint i -> i
atanhP :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i)) =>
EndPoint i -> i
atanhP EndPoint i
x | EndPoint i
x forall a. Ord a => a -> a -> Bool
< -EndPoint i
1 Bool -> Bool -> Bool
|| EndPoint i
1 forall a. Ord a => a -> a -> Bool
< EndPoint i
x = forall a. (?callStack::CallStack) => [Char] -> a
error [Char]
"atanh: domain"
         | EndPoint i
x forall a. Eq a => a -> a -> Bool
== -EndPoint i
1 = - forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval (forall (r :: RoundingMode) a. a -> Rounded r a
Rounded forall a. RealFloatConstants a => a
maxFinite) (forall (r :: RoundingMode) a. a -> Rounded r a
Rounded forall a. RealFloatConstants a => a
positiveInfinity)
         | EndPoint i
x forall a. Eq a => a -> a -> Bool
== EndPoint i
1 = forall i.
IsInterval i =>
Rounded 'TowardNegInf (EndPoint i)
-> Rounded 'TowardInf (EndPoint i) -> i
makeInterval (forall (r :: RoundingMode) a. a -> Rounded r a
Rounded forall a. RealFloatConstants a => a
maxFinite) (forall (r :: RoundingMode) a. a -> Rounded r a
Rounded forall a. RealFloatConstants a => a
positiveInfinity)
         | Bool
otherwise = let x' :: i
x' = forall i. IsInterval i => EndPoint i -> i
singleton EndPoint i
x
                       in forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i)) =>
i -> i
logI ((i
1 forall a. Num a => a -> a -> a
+ i
x') forall a. Fractional a => a -> a -> a
/ (i
1 forall a. Num a => a -> a -> a
- i
x')) forall a. Fractional a => a -> a -> a
/ i
2
{-# INLINABLE atanhP #-}

atanhI :: (IsInterval i, Fractional i, Eq (EndPoint i), RealFloat (EndPoint i), RealFloatConstants (EndPoint i)) => i -> i
atanhI :: forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i)) =>
i -> i
atanhI = forall i.
IsInterval i =>
(Rounded 'TowardNegInf (EndPoint i)
 -> Rounded 'TowardInf (EndPoint i) -> i)
-> i -> i
withEndPoints forall a b. (a -> b) -> a -> b
$ \(Rounded EndPoint i
x) (Rounded EndPoint i
y) -> forall i. IsInterval i => i -> i -> i
hull (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i)) =>
EndPoint i -> i
atanhP EndPoint i
x) (forall i.
(IsInterval i, Fractional i, Eq (EndPoint i),
 RealFloat (EndPoint i), RealFloatConstants (EndPoint i)) =>
EndPoint i -> i
atanhP EndPoint i
y) -- increasing
{-# INLINABLE atanhI #-}