{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE StandaloneDeriving #-}
module AERN2.MP.WithCurrentPrec.Type where
import MixedTypesNumPrelude
import Numeric.CollectErrors (NumErrors, CanTakeErrors(..))
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)
newtype WithAnyPrec t = WithAnyPrec (forall p. (KnownNat p) => WithCurrentPrec t 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