{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
#if __GLASGOW_HASKELL__ >= 908
{-# LANGUAGE TypeAbstractions #-}
#endif
module Numeric.Data.Interval.Internal
(
IntervalBound (..),
Interval (MkInterval, UnsafeInterval),
mkInterval,
unsafeInterval,
SIntervalBound (..),
errMsg,
)
where
import Control.DeepSeq (NFData)
import Data.Kind (Type)
import Data.Maybe qualified as Maybe
import Data.Proxy (Proxy (Proxy))
import Data.Singletons as X
( Sing,
SingI (sing),
SingKind (Demote, fromSing, toSing),
SomeSing (SomeSing),
)
import Data.Text qualified as T
import Data.Text.Display (Display (displayBuilder))
import Data.Text.Lazy qualified as TL
import Data.Text.Lazy.Builder (Builder)
import Data.Text.Lazy.Builder qualified as TLB
import GHC.Generics (Generic)
import GHC.Records (HasField (getField))
import GHC.Show (showSpace)
import GHC.Stack (HasCallStack)
import GHC.TypeNats (KnownNat, Nat, SomeNat (SomeNat), natVal, someNatVal)
import Language.Haskell.TH.Syntax (Lift)
import Numeric.Algebra.MetricSpace (MetricSpace (diffR))
import Numeric.Convert.Integer (FromInteger (fromZ), ToInteger (toZ))
import Numeric.Convert.Rational (FromRational (fromQ), ToRational (toQ))
import Numeric.Convert.Real (FromReal (fromR), ToReal (toR))
import Optics.Core (A_Getter, LabelOptic (labelOptic), to)
type IntervalBound :: Type
data IntervalBound
=
Open Nat
|
Closed Nat
|
None
deriving stock
(
IntervalBound -> IntervalBound -> Bool
(IntervalBound -> IntervalBound -> Bool)
-> (IntervalBound -> IntervalBound -> Bool) -> Eq IntervalBound
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: IntervalBound -> IntervalBound -> Bool
== :: IntervalBound -> IntervalBound -> Bool
$c/= :: IntervalBound -> IntervalBound -> Bool
/= :: IntervalBound -> IntervalBound -> Bool
Eq,
(forall x. IntervalBound -> Rep IntervalBound x)
-> (forall x. Rep IntervalBound x -> IntervalBound)
-> Generic IntervalBound
forall x. Rep IntervalBound x -> IntervalBound
forall x. IntervalBound -> Rep IntervalBound x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. IntervalBound -> Rep IntervalBound x
from :: forall x. IntervalBound -> Rep IntervalBound x
$cto :: forall x. Rep IntervalBound x -> IntervalBound
to :: forall x. Rep IntervalBound x -> IntervalBound
Generic,
(forall (m :: Type -> Type). Quote m => IntervalBound -> m Exp)
-> (forall (m :: Type -> Type).
Quote m =>
IntervalBound -> Code m IntervalBound)
-> Lift IntervalBound
forall t.
(forall (m :: Type -> Type). Quote m => t -> m Exp)
-> (forall (m :: Type -> Type). Quote m => t -> Code m t) -> Lift t
forall (m :: Type -> Type). Quote m => IntervalBound -> m Exp
forall (m :: Type -> Type).
Quote m =>
IntervalBound -> Code m IntervalBound
$clift :: forall (m :: Type -> Type). Quote m => IntervalBound -> m Exp
lift :: forall (m :: Type -> Type). Quote m => IntervalBound -> m Exp
$cliftTyped :: forall (m :: Type -> Type).
Quote m =>
IntervalBound -> Code m IntervalBound
liftTyped :: forall (m :: Type -> Type).
Quote m =>
IntervalBound -> Code m IntervalBound
Lift,
Eq IntervalBound
Eq IntervalBound =>
(IntervalBound -> IntervalBound -> Ordering)
-> (IntervalBound -> IntervalBound -> Bool)
-> (IntervalBound -> IntervalBound -> Bool)
-> (IntervalBound -> IntervalBound -> Bool)
-> (IntervalBound -> IntervalBound -> Bool)
-> (IntervalBound -> IntervalBound -> IntervalBound)
-> (IntervalBound -> IntervalBound -> IntervalBound)
-> Ord IntervalBound
IntervalBound -> IntervalBound -> Bool
IntervalBound -> IntervalBound -> Ordering
IntervalBound -> IntervalBound -> IntervalBound
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: IntervalBound -> IntervalBound -> Ordering
compare :: IntervalBound -> IntervalBound -> Ordering
$c< :: IntervalBound -> IntervalBound -> Bool
< :: IntervalBound -> IntervalBound -> Bool
$c<= :: IntervalBound -> IntervalBound -> Bool
<= :: IntervalBound -> IntervalBound -> Bool
$c> :: IntervalBound -> IntervalBound -> Bool
> :: IntervalBound -> IntervalBound -> Bool
$c>= :: IntervalBound -> IntervalBound -> Bool
>= :: IntervalBound -> IntervalBound -> Bool
$cmax :: IntervalBound -> IntervalBound -> IntervalBound
max :: IntervalBound -> IntervalBound -> IntervalBound
$cmin :: IntervalBound -> IntervalBound -> IntervalBound
min :: IntervalBound -> IntervalBound -> IntervalBound
Ord,
Int -> IntervalBound -> ShowS
[IntervalBound] -> ShowS
IntervalBound -> String
(Int -> IntervalBound -> ShowS)
-> (IntervalBound -> String)
-> ([IntervalBound] -> ShowS)
-> Show IntervalBound
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> IntervalBound -> ShowS
showsPrec :: Int -> IntervalBound -> ShowS
$cshow :: IntervalBound -> String
show :: IntervalBound -> String
$cshowList :: [IntervalBound] -> ShowS
showList :: [IntervalBound] -> ShowS
Show
)
deriving anyclass
(
IntervalBound -> ()
(IntervalBound -> ()) -> NFData IntervalBound
forall a. (a -> ()) -> NFData a
$crnf :: IntervalBound -> ()
rnf :: IntervalBound -> ()
NFData
)
displayIntervalBounds :: IntervalBound -> IntervalBound -> Builder
displayIntervalBounds :: IntervalBound -> IntervalBound -> Builder
displayIntervalBounds IntervalBound
l IntervalBound
r =
[Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat
[ IntervalBound -> Builder
forall {a}. IsString a => IntervalBound -> a
bracketL IntervalBound
l,
IntervalBound -> Builder
valL IntervalBound
l,
Builder
", ",
IntervalBound -> Builder
valR IntervalBound
r,
IntervalBound -> Builder
forall {a}. IsString a => IntervalBound -> a
bracketR IntervalBound
r
]
where
valL :: IntervalBound -> Builder
valL (Open Nat
n) = Nat -> Builder
displayShow Nat
n
valL (Closed Nat
n) = Nat -> Builder
displayShow Nat
n
valL IntervalBound
None = Builder
"-\8734"
valR :: IntervalBound -> Builder
valR (Open Nat
n) = Nat -> Builder
displayShow Nat
n
valR (Closed Nat
n) = Nat -> Builder
displayShow Nat
n
valR IntervalBound
None = Builder
"\8734"
bracketL :: IntervalBound -> a
bracketL (Closed Nat
_) = a
"["
bracketL IntervalBound
_ = a
"("
bracketR :: IntervalBound -> a
bracketR (Closed Nat
_) = a
"]"
bracketR IntervalBound
_ = a
")"
displayShow :: Nat -> Builder
displayShow = String -> Builder
forall a. Display a => a -> Builder
displayBuilder (String -> Builder) -> (Nat -> String) -> Nat -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> String
forall a. Show a => a -> String
show
type SIntervalBound :: IntervalBound -> Type
data SIntervalBound (i :: IntervalBound) where
SOpen :: forall (n :: Nat). (KnownNat n) => SIntervalBound (Open n)
SClosed :: forall (n :: Nat). (KnownNat n) => SIntervalBound (Closed n)
SNone :: SIntervalBound None
deriving stock instance Show (SIntervalBound d)
type instance Sing = SIntervalBound
instance (KnownNat k) => SingI (Open k) where
sing :: Sing ('Open k)
sing = forall (n :: Nat). KnownNat n => SIntervalBound ('Open n)
SOpen @k
instance (KnownNat k) => SingI (Closed k) where
sing :: Sing ('Closed k)
sing = forall (n :: Nat). KnownNat n => SIntervalBound ('Closed n)
SClosed @k
instance SingI None where
sing :: Sing 'None
sing = Sing 'None
SIntervalBound 'None
SNone
instance SingKind IntervalBound where
type Demote IntervalBound = IntervalBound
fromSing :: forall (a :: IntervalBound). Sing a -> Demote IntervalBound
fromSing (SOpen @k) = Nat -> IntervalBound
Open (forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal @k Proxy n
forall {k} (t :: k). Proxy t
Proxy)
fromSing (SClosed @k) = Nat -> IntervalBound
Closed (forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal @k Proxy n
forall {k} (t :: k). Proxy t
Proxy)
fromSing Sing a
SIntervalBound a
SNone = Demote IntervalBound
IntervalBound
None
toSing :: Demote IntervalBound -> SomeSing IntervalBound
toSing (Open Nat
k) =
case Nat -> SomeNat
someNatVal Nat
k of
SomeNat @n Proxy n
_ -> Sing ('Open n) -> SomeSing IntervalBound
forall k (a :: k). Sing a -> SomeSing k
SomeSing (forall (n :: Nat). KnownNat n => SIntervalBound ('Open n)
SOpen @n)
toSing (Closed Nat
k) =
case Nat -> SomeNat
someNatVal Nat
k of
SomeNat @n Proxy n
_ -> Sing ('Closed n) -> SomeSing IntervalBound
forall k (a :: k). Sing a -> SomeSing k
SomeSing (forall (n :: Nat). KnownNat n => SIntervalBound ('Closed n)
SClosed @n)
toSing Demote IntervalBound
IntervalBound
None = Sing 'None -> SomeSing IntervalBound
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'None
SIntervalBound 'None
SNone
type Interval :: IntervalBound -> IntervalBound -> Type -> Type
newtype Interval (l :: IntervalBound) (r :: IntervalBound) (a :: Type)
= UnsafeInterval a
deriving stock
(
Interval l r a -> Interval l r a -> Bool
(Interval l r a -> Interval l r a -> Bool)
-> (Interval l r a -> Interval l r a -> Bool)
-> Eq (Interval l r a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (l :: IntervalBound) (r :: IntervalBound) a.
Eq a =>
Interval l r a -> Interval l r a -> Bool
$c== :: forall (l :: IntervalBound) (r :: IntervalBound) a.
Eq a =>
Interval l r a -> Interval l r a -> Bool
== :: Interval l r a -> Interval l r a -> Bool
$c/= :: forall (l :: IntervalBound) (r :: IntervalBound) a.
Eq a =>
Interval l r a -> Interval l r a -> Bool
/= :: Interval l r a -> Interval l r a -> Bool
Eq,
(forall x. Interval l r a -> Rep (Interval l r a) x)
-> (forall x. Rep (Interval l r a) x -> Interval l r a)
-> Generic (Interval l r a)
forall x. Rep (Interval l r a) x -> Interval l r a
forall x. Interval l r a -> Rep (Interval l r a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (l :: IntervalBound) (r :: IntervalBound) a x.
Rep (Interval l r a) x -> Interval l r a
forall (l :: IntervalBound) (r :: IntervalBound) a x.
Interval l r a -> Rep (Interval l r a) x
$cfrom :: forall (l :: IntervalBound) (r :: IntervalBound) a x.
Interval l r a -> Rep (Interval l r a) x
from :: forall x. Interval l r a -> Rep (Interval l r a) x
$cto :: forall (l :: IntervalBound) (r :: IntervalBound) a x.
Rep (Interval l r a) x -> Interval l r a
to :: forall x. Rep (Interval l r a) x -> Interval l r a
Generic,
(forall (m :: Type -> Type). Quote m => Interval l r a -> m Exp)
-> (forall (m :: Type -> Type).
Quote m =>
Interval l r a -> Code m (Interval l r a))
-> Lift (Interval l r a)
forall t.
(forall (m :: Type -> Type). Quote m => t -> m Exp)
-> (forall (m :: Type -> Type). Quote m => t -> Code m t) -> Lift t
forall (l :: IntervalBound) (r :: IntervalBound) a
(m :: Type -> Type).
(Lift a, Quote m) =>
Interval l r a -> m Exp
forall (l :: IntervalBound) (r :: IntervalBound) a
(m :: Type -> Type).
(Lift a, Quote m) =>
Interval l r a -> Code m (Interval l r a)
forall (m :: Type -> Type). Quote m => Interval l r a -> m Exp
forall (m :: Type -> Type).
Quote m =>
Interval l r a -> Code m (Interval l r a)
$clift :: forall (l :: IntervalBound) (r :: IntervalBound) a
(m :: Type -> Type).
(Lift a, Quote m) =>
Interval l r a -> m Exp
lift :: forall (m :: Type -> Type). Quote m => Interval l r a -> m Exp
$cliftTyped :: forall (l :: IntervalBound) (r :: IntervalBound) a
(m :: Type -> Type).
(Lift a, Quote m) =>
Interval l r a -> Code m (Interval l r a)
liftTyped :: forall (m :: Type -> Type).
Quote m =>
Interval l r a -> Code m (Interval l r a)
Lift,
Eq (Interval l r a)
Eq (Interval l r a) =>
(Interval l r a -> Interval l r a -> Ordering)
-> (Interval l r a -> Interval l r a -> Bool)
-> (Interval l r a -> Interval l r a -> Bool)
-> (Interval l r a -> Interval l r a -> Bool)
-> (Interval l r a -> Interval l r a -> Bool)
-> (Interval l r a -> Interval l r a -> Interval l r a)
-> (Interval l r a -> Interval l r a -> Interval l r a)
-> Ord (Interval l r a)
Interval l r a -> Interval l r a -> Bool
Interval l r a -> Interval l r a -> Ordering
Interval l r a -> Interval l r a -> Interval l r a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall (l :: IntervalBound) (r :: IntervalBound) a.
Ord a =>
Eq (Interval l r a)
forall (l :: IntervalBound) (r :: IntervalBound) a.
Ord a =>
Interval l r a -> Interval l r a -> Bool
forall (l :: IntervalBound) (r :: IntervalBound) a.
Ord a =>
Interval l r a -> Interval l r a -> Ordering
forall (l :: IntervalBound) (r :: IntervalBound) a.
Ord a =>
Interval l r a -> Interval l r a -> Interval l r a
$ccompare :: forall (l :: IntervalBound) (r :: IntervalBound) a.
Ord a =>
Interval l r a -> Interval l r a -> Ordering
compare :: Interval l r a -> Interval l r a -> Ordering
$c< :: forall (l :: IntervalBound) (r :: IntervalBound) a.
Ord a =>
Interval l r a -> Interval l r a -> Bool
< :: Interval l r a -> Interval l r a -> Bool
$c<= :: forall (l :: IntervalBound) (r :: IntervalBound) a.
Ord a =>
Interval l r a -> Interval l r a -> Bool
<= :: Interval l r a -> Interval l r a -> Bool
$c> :: forall (l :: IntervalBound) (r :: IntervalBound) a.
Ord a =>
Interval l r a -> Interval l r a -> Bool
> :: Interval l r a -> Interval l r a -> Bool
$c>= :: forall (l :: IntervalBound) (r :: IntervalBound) a.
Ord a =>
Interval l r a -> Interval l r a -> Bool
>= :: Interval l r a -> Interval l r a -> Bool
$cmax :: forall (l :: IntervalBound) (r :: IntervalBound) a.
Ord a =>
Interval l r a -> Interval l r a -> Interval l r a
max :: Interval l r a -> Interval l r a -> Interval l r a
$cmin :: forall (l :: IntervalBound) (r :: IntervalBound) a.
Ord a =>
Interval l r a -> Interval l r a -> Interval l r a
min :: Interval l r a -> Interval l r a -> Interval l r a
Ord
)
deriving anyclass
(
Interval l r a -> ()
(Interval l r a -> ()) -> NFData (Interval l r a)
forall a. (a -> ()) -> NFData a
forall (l :: IntervalBound) (r :: IntervalBound) a.
NFData a =>
Interval l r a -> ()
$crnf :: forall (l :: IntervalBound) (r :: IntervalBound) a.
NFData a =>
Interval l r a -> ()
rnf :: Interval l r a -> ()
NFData
)
instance HasField "unInterval" (Interval l r a) a where
getField :: Interval l r a -> a
getField (UnsafeInterval a
x) = a
x
instance
( k ~ A_Getter,
a ~ n,
b ~ n
) =>
LabelOptic "unInterval" k (Interval l r a) (Interval l r a) a b
where
labelOptic :: Optic k NoIx (Interval l r a) (Interval l r a) a b
labelOptic = (Interval l r a -> a) -> Getter (Interval l r a) a
forall s a. (s -> a) -> Getter s a
to (\(UnsafeInterval a
x) -> a
x)
{-# INLINE labelOptic #-}
instance
( Show a,
SingI l,
SingI r
) =>
Show (Interval l r a)
where
showsPrec :: Int -> Interval l r a -> ShowS
showsPrec Int
i (UnsafeInterval a
x) =
Bool -> ShowS -> ShowS
showParen
(Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11)
( String -> ShowS
showString String
"UnsafeInterval "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> IntervalBound -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 IntervalBound
left
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
showSpace
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> IntervalBound -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 IntervalBound
right
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
showSpace
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 a
x
)
where
(IntervalBound
left, IntervalBound
right) = forall (l :: IntervalBound) (r :: IntervalBound).
(SingI l, SingI r) =>
(IntervalBound, IntervalBound)
getInterval @l @r
instance
( Show a,
SingI l,
SingI r
) =>
Display (Interval l r a)
where
displayBuilder :: Interval l r a -> Builder
displayBuilder (UnsafeInterval a
x) =
[Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat
[ String -> Builder
forall a. Display a => a -> Builder
displayBuilder (String -> Builder) -> String -> Builder
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. Show a => a -> String
show a
x,
Builder
" ∈ ",
IntervalBound -> IntervalBound -> Builder
displayIntervalBounds IntervalBound
left IntervalBound
right
]
where
(IntervalBound
left, IntervalBound
right) = forall (l :: IntervalBound) (r :: IntervalBound).
(SingI l, SingI r) =>
(IntervalBound, IntervalBound)
getInterval @l @r
instance (MetricSpace a) => MetricSpace (Interval l r a) where
diffR :: Interval l r a -> Interval l r a -> Double
diffR (UnsafeInterval a
x) (UnsafeInterval a
y) = a -> a -> Double
forall s. MetricSpace s => s -> s -> Double
diffR a
x a
y
{-# INLINEABLE diffR #-}
instance
( FromInteger a,
Ord a,
SingI l,
SingI r,
Show a
) =>
FromInteger (Interval l r a)
where
fromZ :: HasCallStack => Integer -> Interval l r a
fromZ = a -> Interval l r a
forall (l :: IntervalBound) (r :: IntervalBound) a.
(FromInteger a, HasCallStack, Ord a, SingI l, SingI r, Show a) =>
a -> Interval l r a
unsafeInterval (a -> Interval l r a)
-> (Integer -> a) -> Integer -> Interval l r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> a
forall a. (FromInteger a, HasCallStack) => Integer -> a
fromZ
{-# INLINEABLE fromZ #-}
instance (ToInteger a) => ToInteger (Interval l r a) where
toZ :: HasCallStack => Interval l r a -> Integer
toZ (UnsafeInterval a
x) = a -> Integer
forall a. (ToInteger a, HasCallStack) => a -> Integer
toZ a
x
{-# INLINEABLE toZ #-}
instance
( FromRational a,
Ord a,
SingI l,
SingI r,
Show a
) =>
FromRational (Interval l r a)
where
fromQ :: HasCallStack => Rational -> Interval l r a
fromQ = a -> Interval l r a
forall (l :: IntervalBound) (r :: IntervalBound) a.
(FromInteger a, HasCallStack, Ord a, SingI l, SingI r, Show a) =>
a -> Interval l r a
unsafeInterval (a -> Interval l r a)
-> (Rational -> a) -> Rational -> Interval l r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> a
forall a. (FromRational a, HasCallStack) => Rational -> a
fromQ
{-# INLINEABLE fromQ #-}
instance (ToRational a) => ToRational (Interval l r a) where
toQ :: HasCallStack => Interval l r a -> Rational
toQ (UnsafeInterval a
x) = a -> Rational
forall a. (ToRational a, HasCallStack) => a -> Rational
toQ a
x
{-# INLINEABLE toQ #-}
instance
( FromReal a,
Ord a,
SingI l,
SingI r,
Show a
) =>
FromReal (Interval l r a)
where
fromR :: HasCallStack => Double -> Interval l r a
fromR = a -> Interval l r a
forall (l :: IntervalBound) (r :: IntervalBound) a.
(FromInteger a, HasCallStack, Ord a, SingI l, SingI r, Show a) =>
a -> Interval l r a
unsafeInterval (a -> Interval l r a) -> (Double -> a) -> Double -> Interval l r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> a
forall a. (FromReal a, HasCallStack) => Double -> a
fromR
{-# INLINEABLE fromR #-}
instance (ToReal a) => ToReal (Interval l r a) where
toR :: HasCallStack => Interval l r a -> Double
toR (UnsafeInterval a
x) = a -> Double
forall a. (ToReal a, HasCallStack) => a -> Double
toR a
x
{-# INLINEABLE toR #-}
pattern MkInterval :: a -> Interval l r a
pattern $mMkInterval :: forall {r} {a} {l :: IntervalBound} {r :: IntervalBound}.
Interval l r a -> (a -> r) -> ((# #) -> r) -> r
MkInterval x <- UnsafeInterval x
{-# COMPLETE MkInterval #-}
mkInterval ::
forall (l :: IntervalBound) (r :: IntervalBound) a.
( FromInteger a,
Ord a,
SingI l,
SingI r
) =>
a ->
Maybe (Interval l r a)
mkInterval :: forall (l :: IntervalBound) (r :: IntervalBound) a.
(FromInteger a, Ord a, SingI l, SingI r) =>
a -> Maybe (Interval l r a)
mkInterval a
x
| Bool
boundedLeft Bool -> Bool -> Bool
&& Bool
boundedRight = Interval l r a -> Maybe (Interval l r a)
forall a. a -> Maybe a
Just (a -> Interval l r a
forall (l :: IntervalBound) (r :: IntervalBound) a.
a -> Interval l r a
UnsafeInterval a
x)
| Bool
otherwise = Maybe (Interval l r a)
forall a. Maybe a
Nothing
where
boundedLeft :: Bool
boundedLeft :: Bool
boundedLeft = case forall {k} (a :: k). SingI a => Sing a
forall (a :: IntervalBound). SingI a => Sing a
sing @l of
Sing l
SIntervalBound l
SNone -> Bool
True
(SOpen @k) ->
let l' :: Nat
l' = forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal @k Proxy n
forall {k} (t :: k). Proxy t
Proxy
in a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> Integer -> a
forall a. (FromInteger a, HasCallStack) => Integer -> a
fromZ (Nat -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
l')
(SClosed @k) ->
let l' :: Nat
l' = forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal @k Proxy n
forall {k} (t :: k). Proxy t
Proxy
in a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer -> a
forall a. (FromInteger a, HasCallStack) => Integer -> a
fromZ (Nat -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
l')
boundedRight :: Bool
boundedRight :: Bool
boundedRight = case forall {k} (a :: k). SingI a => Sing a
forall (a :: IntervalBound). SingI a => Sing a
sing @r of
Sing r
SIntervalBound r
SNone -> Bool
True
(SOpen @k) ->
let r' :: Nat
r' = forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal @k Proxy n
forall {k} (t :: k). Proxy t
Proxy
in a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< Integer -> a
forall a. (FromInteger a, HasCallStack) => Integer -> a
fromZ (Nat -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
r')
(SClosed @k) ->
let r' :: Nat
r' = forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal @k Proxy n
forall {k} (t :: k). Proxy t
Proxy
in a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer -> a
forall a. (FromInteger a, HasCallStack) => Integer -> a
fromZ (Nat -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
r')
{-# INLINEABLE mkInterval #-}
unsafeInterval ::
forall (l :: IntervalBound) (r :: IntervalBound) a.
( FromInteger a,
HasCallStack,
Ord a,
SingI l,
SingI r,
Show a
) =>
a ->
Interval l r a
unsafeInterval :: forall (l :: IntervalBound) (r :: IntervalBound) a.
(FromInteger a, HasCallStack, Ord a, SingI l, SingI r, Show a) =>
a -> Interval l r a
unsafeInterval a
x = Interval l r a -> Maybe (Interval l r a) -> Interval l r a
forall a. a -> Maybe a -> a
Maybe.fromMaybe (String -> Interval l r a
forall a. HasCallStack => String -> a
error String
msg) (Maybe (Interval l r a) -> Interval l r a)
-> Maybe (Interval l r a) -> Interval l r a
forall a b. (a -> b) -> a -> b
$ a -> Maybe (Interval l r a)
forall (l :: IntervalBound) (r :: IntervalBound) a.
(FromInteger a, Ord a, SingI l, SingI r) =>
a -> Maybe (Interval l r a)
mkInterval a
x
where
msg :: String
msg = forall (l :: IntervalBound) (r :: IntervalBound) a.
(Show a, SingI l, SingI r) =>
a -> Builder -> String
errMsg @l @r a
x Builder
"unsafeInterval"
{-# INLINEABLE unsafeInterval #-}
errMsg ::
forall (l :: IntervalBound) (r :: IntervalBound) a.
( Show a,
SingI l,
SingI r
) =>
a ->
Builder ->
String
errMsg :: forall (l :: IntervalBound) (r :: IntervalBound) a.
(Show a, SingI l, SingI r) =>
a -> Builder -> String
errMsg a
x Builder
fnName =
Text -> String
T.unpack (Text -> String) -> Text -> String
forall a b. (a -> b) -> a -> b
$
LazyText -> Text
TL.toStrict (LazyText -> Text) -> LazyText -> Text
forall a b. (a -> b) -> a -> b
$
Builder -> LazyText
TLB.toLazyText Builder
msg
where
intervalStr :: Builder
intervalStr = IntervalBound -> IntervalBound -> Builder
displayIntervalBounds IntervalBound
left IntervalBound
right
(IntervalBound
left, IntervalBound
right) = forall (l :: IntervalBound) (r :: IntervalBound).
(SingI l, SingI r) =>
(IntervalBound, IntervalBound)
getInterval @l @r
msg :: Builder
msg =
[Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat
[ Builder
"Numeric.Data.Interval.",
Builder
fnName,
Builder
": Wanted value in ",
Builder
intervalStr,
Builder
", received: ",
String -> Builder
forall a. Display a => a -> Builder
displayBuilder (String -> Builder) -> String -> Builder
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. Show a => a -> String
show a
x
]
getInterval ::
forall (l :: IntervalBound) (r :: IntervalBound).
( SingI l,
SingI r
) =>
(IntervalBound, IntervalBound)
getInterval :: forall (l :: IntervalBound) (r :: IntervalBound).
(SingI l, SingI r) =>
(IntervalBound, IntervalBound)
getInterval = (Sing l -> Demote IntervalBound
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: IntervalBound). Sing a -> Demote IntervalBound
fromSing Sing l
left, Sing r -> Demote IntervalBound
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: IntervalBound). Sing a -> Demote IntervalBound
fromSing Sing r
right)
where
left :: Sing l
left = forall {k} (a :: k). SingI a => Sing a
forall (a :: IntervalBound). SingI a => Sing a
sing @l
right :: Sing r
right = forall {k} (a :: k). SingI a => Sing a
forall (a :: IntervalBound). SingI a => Sing a
sing @r