{-# 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

class HasCurrentPrecision p where
    getCurrentPrecision :: proxy p -> Precision

instance KnownNat n => HasCurrentPrecision n where
    getCurrentPrecision :: proxy n -> Precision
getCurrentPrecision proxy n
p = 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 n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy n
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 t p)

-- data PrecAdd10 (p :: *)

-- instance (HasCurrentPrecision p) => HasCurrentPrecision (PrecAdd10 p) where
--     isPrecision (_ :: proxy _) = 10 + isPrecision (undefined :: proxy p)

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

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

runWithPrec :: Precision -> (forall n. (KnownNat n) => WithCurrentPrec t n) -> t
runWithPrec :: Precision
-> (forall (n :: Nat). KnownNat n => WithCurrentPrec t n) -> t
runWithPrec Precision
p (wfp :: (forall n. (KnownNat n) => WithCurrentPrec t n)) = 
    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 n => Proxy n -> t
    withNat :: Proxy n -> t
withNat (Proxy n
_ :: Proxy n) = 
        WithCurrentPrec t n -> t
forall t k (p :: k). WithCurrentPrec t p -> t
unWithCurrentPrec (WithCurrentPrec t n
forall (n :: Nat). KnownNat n => WithCurrentPrec t n
wfp :: WithCurrentPrec t n)

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

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

lift2P :: (p1 ~ p2) => (t1 -> t2 -> t3) -> (WithCurrentPrec t1 p1) -> (WithCurrentPrec t2 p2) -> t3
lift2P :: (t1 -> t2 -> t3)
-> WithCurrentPrec t1 p1 -> WithCurrentPrec t2 p2 -> 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 t1 p1) -> t2 -> (WithCurrentPrec t3 p1)
lift1T :: (t1 -> t2 -> t3)
-> WithCurrentPrec t1 p1 -> t2 -> WithCurrentPrec t3 p1
lift1T t1 -> t2 -> t3
f (WithCurrentPrec t1
v1) t2
v2 = t3 -> WithCurrentPrec t3 p1
forall k t (p :: k). t -> WithCurrentPrec t p
WithCurrentPrec (t1 -> t2 -> t3
f t1
v1 t2
v2)

lift1TP :: (t1 -> t2 -> t3) -> (WithCurrentPrec t1 p1) -> t2 -> t3
lift1TP :: (t1 -> t2 -> t3) -> WithCurrentPrec t1 p1 -> 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 t2 p2) -> (WithCurrentPrec t3 p1)
liftT1 :: (t1 -> t2 -> t3)
-> t1 -> WithCurrentPrec t2 p2 -> WithCurrentPrec t3 p1
liftT1 t1 -> t2 -> t3
f t1
v1 (WithCurrentPrec t2
v2) = t3 -> WithCurrentPrec t3 p1
forall k t (p :: k). t -> WithCurrentPrec t p
WithCurrentPrec (t1 -> t2 -> t3
f t1
v1 t2
v2)

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

mpBallCP :: (CanBeMPBallP t, KnownNat p) => t -> WithCurrentPrec (CN MPBall) p
mpBallCP :: t -> WithCurrentPrec (CN MPBall) p
mpBallCP t
v = WithCurrentPrec (CN MPBall) p
r 
    where
    r :: WithCurrentPrec (CN MPBall) p
r = CN MPBall -> WithCurrentPrec (CN MPBall) p
forall k t (p :: k). t -> WithCurrentPrec t p
WithCurrentPrec (CN MPBall -> WithCurrentPrec (CN MPBall) p)
-> CN MPBall -> WithCurrentPrec (CN MPBall) p
forall a b. (a -> b) -> a -> b
$ MPBall -> CN MPBall
forall v. v -> CN v
cn (MPBall -> CN MPBall) -> MPBall -> CN MPBall
forall a b. (a -> b) -> a -> b
$ Precision -> t -> MPBall
forall t. CanBeMPBallP t => Precision -> t -> MPBall
mpBallP (WithCurrentPrec (CN MPBall) p -> Precision
forall k (p :: k) (proxy :: k -> *).
HasCurrentPrecision p =>
proxy p -> Precision
getCurrentPrecision WithCurrentPrec (CN MPBall) p
r) t
v