{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE StandaloneDeriving #-}
{-|
    Module      :  AERN2.MP.WithCurrentPrec.Type
    Description :  Type wrapper setting default precision
    Copyright   :  (c) Michal Konecny
    License     :  BSD3

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

    Type wrapper setting default precision.

    Borrowed some tricks from https://github.com/ekmett/rounded/blob/master/src/Numeric/Rounded/Precision.hs
-}
module AERN2.MP.WithCurrentPrec.Type where

import MixedTypesNumPrelude
-- import Text.Printf

-- import Text.Printf
import Numeric.CollectErrors (NumErrors, CanTakeErrors(..))
-- import qualified Numeric.CollectErrors as CN

import Data.Proxy
import Data.Reflection
import GHC.TypeLits

import AERN2.MP

newtype WithCurrentPrec p t = WithCurrentPrec { WithCurrentPrec p t -> t
unWithCurrentPrec :: t }
    deriving (Int -> WithCurrentPrec p t -> ShowS
[WithCurrentPrec p t] -> ShowS
WithCurrentPrec p t -> String
(Int -> WithCurrentPrec p t -> ShowS)
-> (WithCurrentPrec p t -> String)
-> ([WithCurrentPrec p t] -> ShowS)
-> Show (WithCurrentPrec p t)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) t. Show t => Int -> WithCurrentPrec p t -> ShowS
forall k (p :: k) t. Show t => [WithCurrentPrec p t] -> ShowS
forall k (p :: k) t. Show t => WithCurrentPrec p t -> String
showList :: [WithCurrentPrec p t] -> ShowS
$cshowList :: forall k (p :: k) t. Show t => [WithCurrentPrec p t] -> ShowS
show :: WithCurrentPrec p t -> String
$cshow :: forall k (p :: k) t. Show t => WithCurrentPrec p t -> String
showsPrec :: Int -> WithCurrentPrec p t -> ShowS
$cshowsPrec :: forall k (p :: k) t. Show t => Int -> WithCurrentPrec p t -> ShowS
Show)

deriving instance (CanTakeErrors NumErrors t) => (CanTakeErrors NumErrors (WithCurrentPrec p t))
deriving instance (CanTestIsIntegerType t) => (CanTestIsIntegerType (WithCurrentPrec p t))

getCurrentPrecision :: (KnownNat p) => WithCurrentPrec p t -> Precision
getCurrentPrecision :: WithCurrentPrec p t -> Precision
getCurrentPrecision (WithCurrentPrec p t
_ :: (WithCurrentPrec p t)) =
    Precision -> Precision -> MinMaxType Precision Precision
forall t1 t2.
CanMinMaxAsymmetric t1 t2 =>
t1 -> t2 -> MinMaxType t1 t2
max (Integer -> Precision
prec Integer
2) (Precision -> Precision)
-> (Precision -> Precision) -> Precision -> Precision
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Precision -> Precision -> MinMaxType Precision Precision
forall t1 t2.
CanMinMaxAsymmetric t1 t2 =>
t1 -> t2 -> MinMaxType t1 t2
min Precision
maximumPrecision (Precision -> Precision) -> Precision -> Precision
forall a b. (a -> b) -> a -> b
$ Integer -> Precision
prec (Proxy p -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy p
forall a. HasCallStack => a
undefined :: Proxy p))

{-|

An existential type wrapper for convenient conversions, eg using aern2-real:

> _x :: KnownNat p => WithCurrentPrec (CN MPBall) p
> _x = undefined
>
> _r_x :: CReal
> _r_x = creal $ WithAnyPrec _x

-}
newtype WithAnyPrec t = WithAnyPrec (forall p. (KnownNat p) => WithCurrentPrec p t)

{-| 
    Run a WithCurrentPrec computation with a specific precision.
-}
runWithPrec :: Precision -> (forall p. (KnownNat p) => WithCurrentPrec p t) -> t
runWithPrec :: Precision
-> (forall (p :: Nat). KnownNat p => WithCurrentPrec p t) -> t
runWithPrec Precision
p (wfp :: (forall p. (KnownNat p) => WithCurrentPrec p t)) = 
    Integer -> (forall (n :: Nat). KnownNat n => Proxy n -> t) -> t
forall r.
Integer -> (forall (n :: Nat). KnownNat n => Proxy n -> r) -> r
reifyNat (Precision -> Integer
forall t. CanBeInteger t => t -> Integer
integer Precision
p) forall (n :: Nat). KnownNat n => Proxy n -> t
withNat
    where
    withNat :: KnownNat p => Proxy p -> t
    withNat :: Proxy p -> t
withNat (Proxy p
_ :: Proxy p) = 
        WithCurrentPrec p t -> t
forall k (p :: k) t. WithCurrentPrec p t -> t
unWithCurrentPrec (WithCurrentPrec p t
forall (p :: Nat). KnownNat p => WithCurrentPrec p t
wfp :: WithCurrentPrec p t)

instance (ConvertibleWithPrecision t1 t2, KnownNat p) => ConvertibleExactly t1 (WithCurrentPrec p t2) where
    safeConvertExactly :: t1 -> ConvertResult (WithCurrentPrec p t2)
safeConvertExactly t1
v = WithCurrentPrec p t2 -> ConvertResult (WithCurrentPrec p t2)
forall a b. b -> Either a b
Right WithCurrentPrec p t2
r
        where
        r :: WithCurrentPrec p t2
r = t2 -> WithCurrentPrec p t2
forall k (p :: k) t. t -> WithCurrentPrec p t
WithCurrentPrec (t2 -> WithCurrentPrec p t2) -> t2 -> WithCurrentPrec p t2
forall a b. (a -> b) -> a -> b
$ Precision -> t1 -> t2
forall t1 t2.
ConvertibleWithPrecision t1 t2 =>
Precision -> t1 -> t2
convertP (WithCurrentPrec p t2 -> Precision
forall (p :: Nat) t. KnownNat p => WithCurrentPrec p t -> Precision
getCurrentPrecision WithCurrentPrec p t2
r) t1
v

-- mpBallCP :: (CanBeMPBallP t, KnownNat p) => t -> WithCurrentPrec p MPBall
-- mpBallCP = convertExactly 

cnmpBallCP :: (CanBeMPBallP t, KnownNat p) => t -> WithCurrentPrec p (CN MPBall)
cnmpBallCP :: t -> WithCurrentPrec p (CN MPBall)
cnmpBallCP = (MPBall -> CN MPBall)
-> WithCurrentPrec p MPBall -> WithCurrentPrec p (CN MPBall)
forall k t1 t2 (p :: k).
(t1 -> t2) -> WithCurrentPrec p t1 -> WithCurrentPrec p t2
lift1 MPBall -> CN MPBall
forall v. v -> CN v
cn (WithCurrentPrec p MPBall -> WithCurrentPrec p (CN MPBall))
-> (t -> WithCurrentPrec p MPBall)
-> t
-> WithCurrentPrec p (CN MPBall)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> WithCurrentPrec p MPBall
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly 

lift1 :: (t1 -> t2) -> (WithCurrentPrec p t1) -> (WithCurrentPrec p t2)
lift1 :: (t1 -> t2) -> WithCurrentPrec p t1 -> WithCurrentPrec p t2
lift1 t1 -> t2
f (WithCurrentPrec t1
v1) = t2 -> WithCurrentPrec p t2
forall k (p :: k) t. t -> WithCurrentPrec p t
WithCurrentPrec (t1 -> t2
f t1
v1)

lift2 :: (p1 ~ p2) => (t1 -> t2 -> t3) -> (WithCurrentPrec p1 t1) -> (WithCurrentPrec p2 t2) -> (WithCurrentPrec p1 t3)
lift2 :: (t1 -> t2 -> t3)
-> WithCurrentPrec p1 t1
-> WithCurrentPrec p2 t2
-> WithCurrentPrec p1 t3
lift2 t1 -> t2 -> t3
f (WithCurrentPrec t1
v1) (WithCurrentPrec t2
v2) = t3 -> WithCurrentPrec p1 t3
forall k (p :: k) t. t -> WithCurrentPrec p t
WithCurrentPrec (t1 -> t2 -> t3
f t1
v1 t2
v2)

lift2P :: (p1 ~ p2) => (t1 -> t2 -> t3) -> (WithCurrentPrec p1 t1) -> (WithCurrentPrec p2 t2) -> t3
lift2P :: (t1 -> t2 -> t3)
-> WithCurrentPrec p1 t1 -> WithCurrentPrec p2 t2 -> t3
lift2P t1 -> t2 -> t3
f (WithCurrentPrec t1
v1) (WithCurrentPrec t2
v2) = t1 -> t2 -> t3
f t1
v1 t2
v2

lift1T :: (t1 -> t2 -> t3) -> (WithCurrentPrec p1 t1) -> t2 -> (WithCurrentPrec p1 t3)
lift1T :: (t1 -> t2 -> t3)
-> WithCurrentPrec p1 t1 -> t2 -> WithCurrentPrec p1 t3
lift1T t1 -> t2 -> t3
f (WithCurrentPrec t1
v1) t2
v2 = t3 -> WithCurrentPrec p1 t3
forall k (p :: k) t. t -> WithCurrentPrec p t
WithCurrentPrec (t1 -> t2 -> t3
f t1
v1 t2
v2)

lift1TP :: (t1 -> t2 -> t3) -> (WithCurrentPrec p1 t1) -> t2 -> t3
lift1TP :: (t1 -> t2 -> t3) -> WithCurrentPrec p1 t1 -> t2 -> t3
lift1TP t1 -> t2 -> t3
f (WithCurrentPrec t1
v1) t2
v2 = t1 -> t2 -> t3
f t1
v1 t2
v2

liftT1 :: (t1 -> t2 -> t3) -> t1 -> (WithCurrentPrec p2 t2) -> (WithCurrentPrec p1 t3)
liftT1 :: (t1 -> t2 -> t3)
-> t1 -> WithCurrentPrec p2 t2 -> WithCurrentPrec p1 t3
liftT1 t1 -> t2 -> t3
f t1
v1 (WithCurrentPrec t2
v2) = t3 -> WithCurrentPrec p1 t3
forall k (p :: k) t. t -> WithCurrentPrec p t
WithCurrentPrec (t1 -> t2 -> t3
f t1
v1 t2
v2)

liftT1P :: (t1 -> t2 -> t3) -> t1 -> (WithCurrentPrec p2 t2) -> t3
liftT1P :: (t1 -> t2 -> t3) -> t1 -> WithCurrentPrec p2 t2 -> t3
liftT1P t1 -> t2 -> t3
f t1
v1 (WithCurrentPrec t2
v2) = t1 -> t2 -> t3
f t1
v1 t2
v2