{-# 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 [CN t]

instance Show t => Show (CSequence t) where
  show :: CSequence t -> String
show (CSequence [CN t]
s) = 
    String
"{?(prec " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> (Integer -> String
forall a. Show a => a -> String
show (Integer -> String) -> Integer -> String
forall a b. (a -> b) -> a -> b
$ Precision -> Integer
forall t. CanBeInteger t => t -> Integer
integer Precision
p) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"): " 
    String -> ShowS
forall a. Semigroup a => a -> a -> a
<> (CN t -> String
forall a. Show a => a -> String
show (CN t -> String) -> CN t -> String
forall a b. (a -> b) -> a -> b
$ [CN t]
s [CN t] -> Integer -> CN t
forall n a. CanBeInteger n => [a] -> n -> a
!! Integer
cseqShowDefaultIndex) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"}"
    where
    p :: Precision
p = [Precision]
cseqPrecisions [Precision] -> Integer -> Precision
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) = CN t -> Bool
forall t. CanTestIsIntegerType t => t -> Bool
isIntegerType ([CN t] -> CN t
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 :: (CN t1 -> CN t2) -> CSequence t1 -> CSequence t2
lift1 CN t1 -> CN t2
f (CSequence [CN t1]
a1) = [CN t2] -> CSequence t2
forall t. [CN t] -> CSequence t
CSequence ((CN t1 -> CN t2) -> [CN t1] -> [CN t2]
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 :: (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) = [CN t3] -> CSequence t3
forall t. [CN t] -> CSequence t
CSequence ((CN t1 -> CN t2 -> CN t3) -> [CN t1] -> [CN t2] -> [CN t3]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith CN t1 -> CN t2 -> CN t3
f [CN t1]
a1 [CN t2]
a2)

lift1T :: (CN t1 -> t2 -> CN t3) -> CSequence t1 -> t2 -> CSequence t3
lift1T :: (CN t1 -> t2 -> CN t3) -> CSequence t1 -> t2 -> CSequence t3
lift1T CN t1 -> t2 -> CN t3
f (CSequence [CN t1]
a1) t2
a2 = [CN t3] -> CSequence t3
forall t. [CN t] -> CSequence t
CSequence ((CN t1 -> CN t3) -> [CN t1] -> [CN t3]
forall a b. (a -> b) -> [a] -> [b]
map ((CN t1 -> t2 -> CN t3) -> t2 -> CN t1 -> CN t3
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 :: (t1 -> CN t2 -> CN t3) -> t1 -> CSequence t2 -> CSequence t3
liftT1 t1 -> CN t2 -> CN t3
f t1
a1 (CSequence [CN t2]
a2) = [CN t3] -> CSequence t3
forall t. [CN t] -> CSequence t
CSequence ((CN t2 -> CN t3) -> [CN t2] -> [CN t3]
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 (Precision -> Bool) -> [Precision] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
List.findIndex (Precision -> Precision -> OrderCompareType Precision Precision
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
>= Precision
p) [Precision]
cseqPrecisions of
    Maybe Int
Nothing -> String -> Integer
forall a. HasCallStack => String -> a
error (String -> Integer) -> String -> Integer
forall a b. (a -> b) -> a -> b
$ String
"unable to find index for precision " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Precision -> String
forall a. Show a => a -> String
show Precision
p
    Just Int
i -> Int -> Integer
forall t. CanBeInteger t => t -> Integer
integer Int
i

cseqFromPrecFunction :: (Precision -> CN b) -> CSequence b
cseqFromPrecFunction :: (Precision -> CN b) -> CSequence b
cseqFromPrecFunction Precision -> CN b
withP = [CN b] -> CSequence b
forall t. [CN t] -> CSequence t
CSequence ([CN b] -> CSequence b) -> [CN b] -> CSequence b
forall a b. (a -> b) -> a -> b
$ (Precision -> CN b) -> [Precision] -> [CN 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 (p :: Nat). KnownNat p => WithCurrentPrec p (CN b))
-> CSequence b
cseqFromWithCurrentPrec (withCurrentP :: (forall p. (KnownNat p) => WithCurrentPrec p (CN b))) = 
  [CN b] -> CSequence b
forall t. [CN t] -> CSequence t
CSequence ([CN b] -> CSequence b) -> [CN b] -> CSequence b
forall a b. (a -> b) -> a -> b
$ (Precision -> CN b) -> [Precision] -> [CN b]
forall a b. (a -> b) -> [a] -> [b]
map Precision -> CN b
withP [Precision]
cseqPrecisions
  where
  withP :: Precision -> CN b
withP Precision
p = Precision
-> (forall (p :: Nat). KnownNat p => WithCurrentPrec p (CN b))
-> CN b
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

{- Error handling -}

instance CN.CanTakeErrors CN.NumErrors (CSequence t) where
  takeErrors :: NumErrors -> CSequence t -> CSequence t
takeErrors NumErrors
es (CSequence [CN t]
s) = [CN t] -> CSequence t
forall t. [CN t] -> CSequence t
CSequence ([CN t] -> CSequence t) -> [CN t] -> CSequence t
forall a b. (a -> b) -> a -> b
$ (CN t -> CN t) -> [CN t] -> [CN t]
forall a b. (a -> b) -> [a] -> [b]
map (NumErrors -> CN t -> CN t
forall es t. CanTakeErrors es t => es -> t -> t
CN.takeErrors NumErrors
es) [CN t]
s
  takeErrorsNoValue :: NumErrors -> CSequence t
takeErrorsNoValue NumErrors
es = [CN t] -> CSequence t
forall t. [CN t] -> CSequence t
CSequence ([CN t] -> CSequence t) -> [CN t] -> CSequence t
forall a b. (a -> b) -> a -> b
$ CN t -> [CN t]
forall a. a -> [a]
repeat (NumErrors -> CN t
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) = [CN t] -> CSequence t
forall t. [CN t] -> CSequence t
CSequence ([CN t] -> CSequence t) -> [CN t] -> CSequence t
forall a b. (a -> b) -> a -> b
$ (CN t -> CN t) -> [CN t] -> [CN t]
forall a b. (a -> b) -> [a] -> [b]
map CN t -> CN t
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 :: t -> CReal
creal = t -> CReal
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly

crealFromPrecFunction :: (Precision -> CN MPBall) -> CReal
crealFromPrecFunction :: (Precision -> CN MPBall) -> CReal
crealFromPrecFunction = (Precision -> CN MPBall) -> CReal
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 (p :: Nat). KnownNat p => WithCurrentPrec p (CN MPBall))
-> CReal
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
? :: e -> q -> ExtractedApproximation 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 ([CN t] -> CN t) -> [CN t] -> CN t
forall a b. (a -> b) -> a -> b
$ Integer -> [CN t] -> [CN t]
forall n a. CanBeInteger n => n -> [a] -> [a]
drop (Precision -> Integer
cseqIndexForPrecision Precision
p Integer -> Integer -> SubType Integer Integer
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) 
      | CN t -> Bool
forall es. CanTestErrorsCertain es => es -> Bool
CN.hasCertainError CN t
bCN = CN t
bCN
      | CN t -> Accuracy
forall a. HasAccuracy a => a -> Accuracy
getAccuracy CN t
bCN Accuracy -> Accuracy -> OrderCompareType Accuracy Accuracy
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 [] =
        NumError -> CN t
forall v. NumError -> CN v
CN.noValueNumErrorPotential (NumError -> CN t) -> NumError -> CN t
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 [CN t] -> Integer -> CN t
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 = CN MPBall -> ConvertResult (CN MPBall)
forall a b. b -> Either a b
Right (CN MPBall -> ConvertResult (CN MPBall))
-> CN MPBall -> ConvertResult (CN MPBall)
forall a b. (a -> b) -> a -> b
$ CReal
r CReal -> Precision -> ExtractedApproximation CReal Precision
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 = CReal -> ConvertResult CReal
forall a b. b -> Either a b
Right

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

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

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

instance ConvertibleExactly Dyadic CReal where
  safeConvertExactly :: Dyadic -> ConvertResult CReal
safeConvertExactly = Rational -> ConvertResult CReal
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> ConvertResult t2
safeConvertExactly (Rational -> ConvertResult CReal)
-> (Dyadic -> Rational) -> Dyadic -> ConvertResult CReal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dyadic -> Rational
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) = CReal -> ConvertResult CReal
forall a b. b -> Either a b
Right (CReal -> ConvertResult CReal) -> CReal -> ConvertResult CReal
forall a b. (a -> b) -> a -> b
$ (forall (p :: Nat). KnownNat p => WithCurrentPrec p (CN MPBall))
-> CReal
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 = Rational -> CReal
forall t. CanBeCReal t => t -> CReal
creal Rational
1.0

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

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