{-# OPTIONS_GHC -Wno-orphans #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-|
    Module      :  AERN2.Real.Type
    Description :  The type of constructive real numbers
    Copyright   :  (c) Michal Konecny
    License     :  BSD3

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

    The type of constructive real numbers using convergent sequences of intervals.
-}
module AERN2.Real.Type where

import MixedTypesNumPrelude
-- import qualified Prelude as P

import qualified Numeric.CollectErrors as CN

import qualified Data.List as List

import AERN2.MP
import AERN2.MP.Dyadic

import AERN2.MP.WithCurrentPrec
import GHC.TypeNats

-- import AERN2.MP.Accuracy

{- Convergent partial sequences -}

newtype CSequence t = CSequence { forall t. CSequence t -> [CN t]
unCSequence :: [CN t] }

instance Show t => Show (CSequence t) where
  show :: CSequence t -> String
show (CSequence [CN t]
s) = 
    String
"{?(prec " forall a. Semigroup a => a -> a -> a
<> (forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall t. CanBeInteger t => t -> Integer
integer Precision
p) forall a. Semigroup a => a -> a -> a
<> String
"): " 
    forall a. Semigroup a => a -> a -> a
<> (forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ [CN t]
s forall n a. CanBeInteger n => [a] -> n -> a
!! Integer
cseqShowDefaultIndex) forall a. Semigroup a => a -> a -> a
<> String
"}"
    where
    p :: Precision
p = [Precision]
cseqPrecisions forall n a. CanBeInteger n => [a] -> n -> a
!! Integer
cseqShowDefaultIndex

instance (CanTestIsIntegerType t) => CanTestIsIntegerType (CSequence t) where
  isIntegerType :: CSequence t -> Bool
isIntegerType (CSequence [CN t]
s) = forall t. CanTestIsIntegerType t => t -> Bool
isIntegerType (forall a. [a] -> a
head [CN t]
s)

cseqShowDefaultIndex :: Integer
cseqShowDefaultIndex :: Integer
cseqShowDefaultIndex = Integer
7

lift1 :: (CN t1 -> CN t2) -> CSequence t1 -> CSequence t2
lift1 :: forall t1 t2. (CN t1 -> CN t2) -> CSequence t1 -> CSequence t2
lift1 CN t1 -> CN t2
f (CSequence [CN t1]
a1) = forall t. [CN t] -> CSequence t
CSequence (forall a b. (a -> b) -> [a] -> [b]
map CN t1 -> CN t2
f [CN t1]
a1)

lift2 :: (CN t1 -> CN t2 -> CN t3) -> CSequence t1 -> CSequence t2 -> CSequence t3
lift2 :: forall t1 t2 t3.
(CN t1 -> CN t2 -> CN t3)
-> CSequence t1 -> CSequence t2 -> CSequence t3
lift2 CN t1 -> CN t2 -> CN t3
f (CSequence [CN t1]
a1) (CSequence [CN t2]
a2) = forall t. [CN t] -> CSequence t
CSequence (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith CN t1 -> CN t2 -> CN t3
f [CN t1]
a1 [CN t2]
a2)

lift2LeftFirst :: (CN t1 -> CN t2 -> CN t3) -> CSequence t1 -> CSequence t2 -> CSequence t3
lift2LeftFirst :: forall t1 t2 t3.
(CN t1 -> CN t2 -> CN t3)
-> CSequence t1 -> CSequence t2 -> CSequence t3
lift2LeftFirst CN t1 -> CN t2 -> CN t3
f (CSequence [CN t1]
a1) CSequence t2
s2 = forall t. [CN t] -> CSequence t
CSequence (forall a b. (a -> b) -> [a] -> [b]
map (CN t1, Integer) -> CN t3
f' forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [CN t1]
a1 [Integer
0..])
  where
  f' :: (CN t1, Integer) -> CN t3
f' (CN t1
b1, Integer
i) = CN t1 -> CN t2 -> CN t3
f CN t1
b1 (forall t. CSequence t -> [CN t]
unCSequence CSequence t2
s2 forall n a. CanBeInteger n => [a] -> n -> a
!! Integer
i)

lift1T :: (CN t1 -> t2 -> CN t3) -> CSequence t1 -> t2 -> CSequence t3
lift1T :: forall t1 t2 t3.
(CN t1 -> t2 -> CN t3) -> CSequence t1 -> t2 -> CSequence t3
lift1T CN t1 -> t2 -> CN t3
f (CSequence [CN t1]
a1) t2
a2 = forall t. [CN t] -> CSequence t
CSequence (forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> b -> a -> c
flip CN t1 -> t2 -> CN t3
f t2
a2) [CN t1]
a1)

liftT1 :: (t1 -> CN t2 -> CN t3) -> t1 -> CSequence t2 -> CSequence t3
liftT1 :: forall t1 t2 t3.
(t1 -> CN t2 -> CN t3) -> t1 -> CSequence t2 -> CSequence t3
liftT1 t1 -> CN t2 -> CN t3
f t1
a1 (CSequence [CN t2]
a2) = forall t. [CN t] -> CSequence t
CSequence (forall a b. (a -> b) -> [a] -> [b]
map (t1 -> CN t2 -> CN t3
f t1
a1) [CN t2]
a2)

cseqPrecisions :: [Precision]
cseqPrecisions :: [Precision]
cseqPrecisions = Precision -> [Precision]
standardPrecisions (Integer -> Precision
prec Integer
10)

cseqIndexForPrecision :: Precision -> Integer
cseqIndexForPrecision :: Precision -> Integer
cseqIndexForPrecision Precision
p =
  case forall a. (a -> Bool) -> [a] -> Maybe Int
List.findIndex (forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
>= Precision
p) [Precision]
cseqPrecisions of
    Maybe Int
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"unable to find index for precision " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Precision
p
    Just Int
i -> forall t. CanBeInteger t => t -> Integer
integer Int
i

cseqFromPrecFunction :: (Precision -> CN b) -> CSequence b
cseqFromPrecFunction :: forall b. (Precision -> CN b) -> CSequence b
cseqFromPrecFunction Precision -> CN b
withP = forall t. [CN t] -> CSequence t
CSequence forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Precision -> CN b
withP [Precision]
cseqPrecisions

cseqFromWithCurrentPrec :: (forall p. (KnownNat p) => WithCurrentPrec p (CN b)) -> CSequence b
cseqFromWithCurrentPrec :: forall b.
(forall (p :: Nat). KnownNat p => WithCurrentPrec p (CN b))
-> CSequence b
cseqFromWithCurrentPrec (forall (p :: Nat). KnownNat p => WithCurrentPrec p (CN b)
withCurrentP :: (forall p. (KnownNat p) => WithCurrentPrec p (CN b))) = 
  forall t. [CN t] -> CSequence t
CSequence forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Precision -> CN b
withP [Precision]
cseqPrecisions
  where
  withP :: Precision -> CN b
withP Precision
p = forall t.
Precision
-> (forall (p :: Nat). KnownNat p => WithCurrentPrec p t) -> t
runWithPrec Precision
p forall (p :: Nat). KnownNat p => WithCurrentPrec p (CN b)
withCurrentP :: CN b

unsafeApproximationExtension :: (CSequence b -> t) -> (CN b -> t)
unsafeApproximationExtension :: forall b t. (CSequence b -> t) -> CN b -> t
unsafeApproximationExtension CSequence b -> t
f CN b
b = CSequence b -> t
f (forall t. [CN t] -> CSequence t
CSequence forall a b. (a -> b) -> a -> b
$ forall a. a -> [a]
repeat CN b
b) 
  -- a sequence that does not converge unless b is exact
  -- (eg a fake real number given by an interval)

{- Error handling -}

instance CN.CanTakeErrors CN.NumErrors (CSequence t) where
  takeErrors :: NumErrors -> CSequence t -> CSequence t
takeErrors NumErrors
es (CSequence [CN t]
s) = forall t. [CN t] -> CSequence t
CSequence forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall es t. CanTakeErrors es t => es -> t -> t
CN.takeErrors NumErrors
es) [CN t]
s
  takeErrorsNoValue :: NumErrors -> CSequence t
takeErrorsNoValue NumErrors
es = forall t. [CN t] -> CSequence t
CSequence forall a b. (a -> b) -> a -> b
$ forall a. a -> [a]
repeat (forall es t. CanTakeErrors es t => es -> t
CN.takeErrorsNoValue NumErrors
es)

instance CN.CanClearPotentialErrors (CSequence t) where
  clearPotentialErrors :: CSequence t -> CSequence t
clearPotentialErrors (CSequence [CN t]
s) = forall t. [CN t] -> CSequence t
CSequence forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall cnt. CanClearPotentialErrors cnt => cnt -> cnt
clearPotentialErrors [CN t]
s

{- Cauchy real numbers -}

type CReal = CSequence MPBall

type HasCReals t = ConvertibleExactly CReal t

type CanBeCReal t = ConvertibleExactly t CReal

creal :: (CanBeCReal t) => t -> CReal
creal :: forall t. CanBeCReal t => t -> CReal
creal = forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly

crealFromPrecFunction :: (Precision -> CN MPBall) -> CReal
crealFromPrecFunction :: (Precision -> CN MPBall) -> CReal
crealFromPrecFunction = forall b. (Precision -> CN b) -> CSequence b
cseqFromPrecFunction

crealFromWithCurrentPrec :: (forall p. (KnownNat p) => WithCurrentPrec p (CN MPBall)) -> CSequence MPBall
crealFromWithCurrentPrec :: (forall (p :: Nat). KnownNat p => WithCurrentPrec p (CN MPBall))
-> CReal
crealFromWithCurrentPrec = forall b.
(forall (p :: Nat). KnownNat p => WithCurrentPrec p (CN b))
-> CSequence b
cseqFromWithCurrentPrec

{- Extracting approximations -}

class CanExtractApproximation e q where
  type ExtractedApproximation e q
  {-| Get an approximation of an exact value using the given query -}
  extractApproximation :: e {-^ exact value -} -> q {-^ query -} -> ExtractedApproximation e q

infix 1 ?

(?) :: CanExtractApproximation e q => e -> q -> ExtractedApproximation e q
? :: forall e q.
CanExtractApproximation e q =>
e -> q -> ExtractedApproximation e q
(?) = forall e q.
CanExtractApproximation e q =>
e -> q -> ExtractedApproximation e q
extractApproximation

instance (HasAccuracy t) => CanExtractApproximation (CSequence t) Accuracy where
  type ExtractedApproximation (CSequence t) Accuracy = CN t
  extractApproximation :: CSequence t
-> Accuracy -> ExtractedApproximation (CSequence t) Accuracy
extractApproximation (CSequence [CN t]
s) Accuracy
ac = 
    [CN t] -> CN t
aux forall a b. (a -> b) -> a -> b
$ forall n a. CanBeInteger n => n -> [a] -> [a]
drop (Precision -> Integer
cseqIndexForPrecision Precision
p forall t1 t2. CanSub t1 t2 => t1 -> t2 -> SubType t1 t2
- Integer
1) [CN t]
s
    where    
    p :: Precision
p = 
      case Accuracy
ac of 
        Accuracy
Exact -> Precision
defaultPrecision
        Accuracy
NoInformation -> Integer -> Precision
prec Integer
2
        Accuracy
_ -> Accuracy -> Precision
ac2prec Accuracy
ac
    aux :: [CN t] -> CN t
aux (CN t
bCN : [CN t]
rest) 
      | forall es. CanTestErrorsCertain es => es -> Bool
CN.hasCertainError CN t
bCN = CN t
bCN
      | forall a. HasAccuracy a => a -> Accuracy
getAccuracy CN t
bCN forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
>= Accuracy
ac = CN t
bCN
      | Bool
otherwise = [CN t] -> CN t
aux [CN t]
rest
    aux [] =
        forall v. NumError -> CN v
CN.noValueNumErrorPotential forall a b. (a -> b) -> a -> b
$ 
          String -> NumError
CN.NumError String
"failed to find an approximation with sufficient accuracy"
  
instance CanExtractApproximation (CSequence t) Precision where
  type ExtractedApproximation (CSequence t) Precision = CN t
  extractApproximation :: CSequence t
-> Precision -> ExtractedApproximation (CSequence t) Precision
extractApproximation (CSequence [CN t]
s) Precision
p =
    [CN t]
s forall n a. CanBeInteger n => [a] -> n -> a
!! (Precision -> Integer
cseqIndexForPrecision Precision
p)

instance ConvertibleWithPrecision CReal (CN MPBall) where
  safeConvertP :: Precision -> CReal -> ConvertResult (CN MPBall)
safeConvertP Precision
p CReal
r = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ CReal
r forall e q.
CanExtractApproximation e q =>
e -> q -> ExtractedApproximation e q
? Precision
p

-- {- exact conversions -}

instance ConvertibleExactly CReal CReal where
  safeConvertExactly :: CReal -> ConvertResult CReal
safeConvertExactly = forall a b. b -> Either a b
Right

instance ConvertibleExactly Rational CReal where
  safeConvertExactly :: Rational -> ConvertResult CReal
safeConvertExactly Rational
x =
    forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ (Precision -> CN MPBall) -> CReal
crealFromPrecFunction (forall v. v -> CN v
cn forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall t. CanBeMPBallP t => Precision -> t -> MPBall
mpBallP Rational
x)

instance ConvertibleExactly Integer CReal where
  safeConvertExactly :: Integer -> ConvertResult CReal
safeConvertExactly = forall t1 t2. ConvertibleExactly t1 t2 => t1 -> ConvertResult t2
safeConvertExactly forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. CanBeRational t => t -> Rational
rational

instance ConvertibleExactly Int CReal where
  safeConvertExactly :: Int -> ConvertResult CReal
safeConvertExactly = forall t1 t2. ConvertibleExactly t1 t2 => t1 -> ConvertResult t2
safeConvertExactly forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. CanBeRational t => t -> Rational
rational

instance ConvertibleExactly Dyadic CReal where
  safeConvertExactly :: Dyadic -> ConvertResult CReal
safeConvertExactly = forall t1 t2. ConvertibleExactly t1 t2 => t1 -> ConvertResult t2
safeConvertExactly forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. CanBeRational t => t -> Rational
rational

instance ConvertibleExactly (WithAnyPrec (CN MPBall)) CReal where
  safeConvertExactly :: WithAnyPrec (CN MPBall) -> ConvertResult CReal
safeConvertExactly (WithAnyPrec forall (p :: Nat). KnownNat p => WithCurrentPrec p (CN MPBall)
wcp) = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall b.
(forall (p :: Nat). KnownNat p => WithCurrentPrec p (CN b))
-> CSequence b
cseqFromWithCurrentPrec forall (p :: Nat). KnownNat p => WithCurrentPrec p (CN MPBall)
wcp

_example1 :: CReal
_example1 :: CReal
_example1 = forall t. CanBeCReal t => t -> CReal
creal Rational
1.0

_example2 :: CN MPBall
_example2 :: CN MPBall
_example2 = (forall t. CanBeCReal t => t -> CReal
creal forall a b. (a -> b) -> a -> b
$ Integer
1forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/Integer
3) forall e q.
CanExtractApproximation e q =>
e -> q -> ExtractedApproximation e q
? (forall t. ConvertibleExactly t Accuracy => t -> Accuracy
bits Integer
100)

_example3 :: CN MPBall
_example3 :: CN MPBall
_example3 = forall t1 t2.
ConvertibleWithPrecision t1 t2 =>
Precision -> t1 -> t2
convertP (Integer -> Precision
prec Integer
100) (forall t. CanBeCReal t => t -> CReal
creal forall a b. (a -> b) -> a -> b
$ Integer
1forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/Integer
3)