{-# OPTIONS_GHC -Wno-orphans #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-|
    Module      :  AERN2.Real.Limit
    Description :  limits of CReal sequences
    Copyright   :  (c) Michal Konecny
    License     :  BSD3

    Maintainer  :  mikkonecny@gmail.com
    Stability   :  experimental
    Portability :  portable

    Limits of Cauchy Real sequences.
-}
module AERN2.Real.Limit where

import MixedTypesNumPrelude

-- import qualified Numeric.CollectErrors as CN

-- import Math.NumberTheory.Logarithms (integerLog2)

import AERN2.Real.Type
import AERN2.Limit
import AERN2.MP ( (+-) )

---------
-- limit
---------

instance HasLimits Rational CReal where
  type LimitType Rational CReal = CReal
  limit :: (Rational -> CReal) -> LimitType Rational CReal
limit Rational -> CReal
s = (Precision -> CN MPBall) -> CReal
crealFromPrecFunction Precision -> PlusMinusType (CN MPBall) Rational
Precision -> CN MPBall
withPrec
    where
    withPrec :: Precision -> PlusMinusType (CN MPBall) Rational
withPrec Precision
p = ((Rational -> CReal
s Rational
PowType Rational Integer
epsilon) CReal -> Precision -> ExtractedApproximation CReal Precision
forall e q.
CanExtractApproximation e q =>
e -> q -> ExtractedApproximation e q
? Precision
p) CN MPBall -> Rational -> PlusMinusType (CN MPBall) Rational
forall t1 t2. CanPlusMinus t1 t2 => t1 -> t2 -> PlusMinusType t1 t2
+- Rational
PowType Rational Integer
epsilon
      where
      epsilon :: PowType Rational Integer
epsilon = Rational
0.5 Rational -> Integer -> PowType Rational Integer
forall t1 t2. CanPow t1 t2 => t1 -> t2 -> PowType t1 t2
^ (Precision -> Integer
forall t. CanBeInteger t => t -> Integer
integer Precision
p)
    
instance HasLimits Integer CReal where
  type LimitType Integer CReal = CReal
  limit :: (Integer -> CReal) -> LimitType Integer CReal
limit Integer -> CReal
s = (Precision -> CN MPBall) -> CReal
crealFromPrecFunction Precision -> PlusMinusType (CN MPBall) Rational
Precision -> CN MPBall
withPrec
    where
    withPrec :: Precision -> PlusMinusType (CN MPBall) Rational
withPrec Precision
p = ((Integer -> CReal
s (Precision -> Integer
forall t. CanBeInteger t => t -> Integer
integer Precision
p)) CReal -> Precision -> ExtractedApproximation CReal Precision
forall e q.
CanExtractApproximation e q =>
e -> q -> ExtractedApproximation e q
? Precision
p) CN MPBall -> Rational -> PlusMinusType (CN MPBall) Rational
forall t1 t2. CanPlusMinus t1 t2 => t1 -> t2 -> PlusMinusType t1 t2
+- Rational
PowType Rational Integer
epsilon
      where
      epsilon :: PowType Rational Integer
epsilon = Rational
0.5 Rational -> Integer -> PowType Rational Integer
forall t1 t2. CanPow t1 t2 => t1 -> t2 -> PowType t1 t2
^ (Precision -> Integer
forall t. CanBeInteger t => t -> Integer
integer Precision
p)

instance HasLimits Int CReal where
  type LimitType Int CReal = CReal
  limit :: (Int -> CReal) -> LimitType Int CReal
limit Int -> CReal
s = (Integer -> CReal) -> LimitType Integer CReal
forall ix s. HasLimits ix s => (ix -> s) -> LimitType ix s
limit (Int -> CReal
s (Int -> CReal) -> (Integer -> Int) -> Integer -> CReal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Int
c)
    where
    c :: Integer -> Int
    c :: Integer -> Int
c = Integer -> Int
forall t. CanBeInt t => t -> Int
int

instance HasLimits Rational (CReal -> CReal) where
  type LimitType Rational (CReal -> CReal) = (CReal -> CReal)
  limit :: (Rational -> CReal -> CReal) -> LimitType Rational (CReal -> CReal)
limit Rational -> CReal -> CReal
fs CReal
x = (Precision -> CN MPBall) -> CReal
crealFromPrecFunction Precision -> PlusMinusType (CN MPBall) Rational
Precision -> CN MPBall
withPrec
    where
    withPrec :: Precision -> PlusMinusType (CN MPBall) Rational
withPrec Precision
p = ((Rational -> CReal -> CReal
fs Rational
PowType Rational Integer
epsilon CReal
x) CReal -> Precision -> ExtractedApproximation CReal Precision
forall e q.
CanExtractApproximation e q =>
e -> q -> ExtractedApproximation e q
? Precision
p) CN MPBall -> Rational -> PlusMinusType (CN MPBall) Rational
forall t1 t2. CanPlusMinus t1 t2 => t1 -> t2 -> PlusMinusType t1 t2
+- Rational
PowType Rational Integer
epsilon
      where
      epsilon :: PowType Rational Integer
epsilon = Rational
0.5 Rational -> Integer -> PowType Rational Integer
forall t1 t2. CanPow t1 t2 => t1 -> t2 -> PowType t1 t2
^ (Precision -> Integer
forall t. CanBeInteger t => t -> Integer
integer Precision
p)