{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_HADDOCK not-home #-}

module I.Rational () where

import Control.Monad
import Data.Constraint
import Data.Maybe
import Data.Proxy
import Data.Type.Ord
import GHC.TypeLits qualified as L
import GHC.Real
import KindRational (type (/))
import KindRational qualified as KR
import Prelude hiding (min, max, div, succ, pred)
import Prelude qualified as P
import Unsafe.Coerce (unsafeCoerce)

import I.Internal

--------------------------------------------------------------------------------

type instance MinL P.Rational = 'Nothing
type instance MaxR P.Rational = 'Nothing

instance forall l r.
  ( IntervalCtx    P.Rational ('Just '( 'True, l)) ('Just '( 'True, r))
  ) => Interval    P.Rational ('Just '( 'True, l)) ('Just '( 'True, r)) where
  type IntervalCtx P.Rational ('Just '( 'True, l)) ('Just '( 'True, r)) =
    (KR.KnownRational l, KR.KnownRational r, l <= r)
  type MinI P.Rational ('Just '( 'True, l)) ('Just '( 'True, r)) = l
  type MaxI P.Rational ('Just '( 'True, l)) ('Just '( 'True, r)) = r
  inhabitant :: I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
inhabitant = I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
forall x (l :: L x) (r :: R x). Known x l r (MinI x l r) => I x l r
min
  from :: Rational
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'True, r)))
from = \Rational
x -> Rational -> I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
forall x (l :: L x) (r :: R x). x -> I x l r
unsafest Rational
x I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
-> Maybe ()
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'True, r)))
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Rational
l Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
<= Rational
x Bool -> Bool -> Bool
&& Rational
x Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
<= Rational
r)
    where l :: Rational
l = Proxy l -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @l)
          r :: Rational
r = Proxy r -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @r)
  negate' :: I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'True, r)))
negate' = Rational
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'True, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (Rational
 -> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'True, r))))
-> (I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
    -> Rational)
-> I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'True, r)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Rational
forall a. Num a => a -> a
P.negate (Rational -> Rational)
-> (I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
    -> Rational)
-> I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
-> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I Rational ('Just '( 'True, l)) ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap
  recip' :: I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'True, r)))
recip' I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
x = case I Rational ('Just '( 'True, l)) ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
x of Integer
n :% Integer
d -> Rational
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'True, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (Integer
d Integer -> Integer -> Rational
forall a. a -> a -> Ratio a
:% Integer
n)
  I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
a plus' :: I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
-> I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'True, r)))
`plus'` I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
b = Rational
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'True, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational ('Just '( 'True, l)) ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ I Rational ('Just '( 'True, l)) ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
b)
  I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
a mult' :: I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
-> I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'True, r)))
`mult'` I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
b = Rational
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'True, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational ('Just '( 'True, l)) ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* I Rational ('Just '( 'True, l)) ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
b)
  I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
a minus' :: I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
-> I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'True, r)))
`minus'` I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
b = Rational
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'True, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational ('Just '( 'True, l)) ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- I Rational ('Just '( 'True, l)) ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
b)
  I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
a div' :: I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
-> I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'True, r)))
`div'` I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
b = do Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (I Rational ('Just '( 'True, l)) ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
b Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
/= Rational
0)
                  Rational
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'True, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational ('Just '( 'True, l)) ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
a Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ I Rational ('Just '( 'True, l)) ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
b)

instance forall l r.
  ( IntervalCtx    P.Rational ('Just '( 'True, l)) ('Just '( 'False, r))
  ) => Interval    P.Rational ('Just '( 'True, l)) ('Just '( 'False, r)) where
  type IntervalCtx P.Rational ('Just '( 'True, l)) ('Just '( 'False, r)) =
    (KR.KnownRational l, KR.KnownRational r, l < r)
  type MinI P.Rational ('Just '( 'True, l)) ('Just '( 'False, r)) = l
  inhabitant :: I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
inhabitant = I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
forall x (l :: L x) (r :: R x). Known x l r (MinI x l r) => I x l r
min
  from :: Rational
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'False, r)))
from = \Rational
x -> Rational -> I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
forall x (l :: L x) (r :: R x). x -> I x l r
unsafest Rational
x I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
-> Maybe ()
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'False, r)))
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Rational
l Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
<= Rational
x Bool -> Bool -> Bool
&& Rational
x Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
< Rational
r)
    where l :: Rational
l = Proxy l -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @l)
          r :: Rational
r = Proxy r -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @r)
  negate' :: I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'False, r)))
negate' = Rational
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'False, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (Rational
 -> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'False, r))))
-> (I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
    -> Rational)
-> I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'False, r)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Rational
forall a. Num a => a -> a
P.negate (Rational -> Rational)
-> (I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
    -> Rational)
-> I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
-> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I Rational ('Just '( 'True, l)) ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap
  recip' :: I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'False, r)))
recip' I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
x = case I Rational ('Just '( 'True, l)) ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
x of Integer
n :% Integer
d -> Rational
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'False, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (Integer
d Integer -> Integer -> Rational
forall a. a -> a -> Ratio a
:% Integer
n)
  I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
a plus' :: I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
-> I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'False, r)))
`plus'` I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
b = Rational
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'False, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational ('Just '( 'True, l)) ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ I Rational ('Just '( 'True, l)) ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
b)
  I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
a mult' :: I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
-> I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'False, r)))
`mult'` I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
b = Rational
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'False, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational ('Just '( 'True, l)) ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* I Rational ('Just '( 'True, l)) ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
b)
  I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
a minus' :: I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
-> I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'False, r)))
`minus'` I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
b = Rational
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'False, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational ('Just '( 'True, l)) ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- I Rational ('Just '( 'True, l)) ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
b)
  I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
a div' :: I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
-> I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'False, r)))
`div'` I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
b = do Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (I Rational ('Just '( 'True, l)) ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
b Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
/= Rational
0)
                  Rational
-> Maybe (I Rational ('Just '( 'True, l)) ('Just '( 'False, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational ('Just '( 'True, l)) ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
a Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ I Rational ('Just '( 'True, l)) ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
b)

instance forall l.
  ( IntervalCtx    P.Rational ('Just '( 'True, l)) 'Nothing
  ) => Interval    P.Rational ('Just '( 'True, l)) 'Nothing where
  type IntervalCtx P.Rational ('Just '( 'True, l)) 'Nothing = KR.KnownRational l
  type MinI P.Rational ('Just '( 'True, l)) 'Nothing = l
  inhabitant :: I Rational ('Just '( 'True, l)) 'Nothing
inhabitant = I Rational ('Just '( 'True, l)) 'Nothing
forall x (l :: L x) (r :: R x). Known x l r (MinI x l r) => I x l r
min
  from :: Rational -> Maybe (I Rational ('Just '( 'True, l)) 'Nothing)
from = \Rational
x -> Rational -> I Rational ('Just '( 'True, l)) 'Nothing
forall x (l :: L x) (r :: R x). x -> I x l r
unsafest Rational
x I Rational ('Just '( 'True, l)) 'Nothing
-> Maybe () -> Maybe (I Rational ('Just '( 'True, l)) 'Nothing)
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Rational
l Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
<= Rational
x)
    where l :: Rational
l = Proxy l -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @l)
  negate' :: I Rational ('Just '( 'True, l)) 'Nothing
-> Maybe (I Rational ('Just '( 'True, l)) 'Nothing)
negate' = Rational -> Maybe (I Rational ('Just '( 'True, l)) 'Nothing)
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (Rational -> Maybe (I Rational ('Just '( 'True, l)) 'Nothing))
-> (I Rational ('Just '( 'True, l)) 'Nothing -> Rational)
-> I Rational ('Just '( 'True, l)) 'Nothing
-> Maybe (I Rational ('Just '( 'True, l)) 'Nothing)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Rational
forall a. Num a => a -> a
P.negate (Rational -> Rational)
-> (I Rational ('Just '( 'True, l)) 'Nothing -> Rational)
-> I Rational ('Just '( 'True, l)) 'Nothing
-> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I Rational ('Just '( 'True, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap
  recip' :: I Rational ('Just '( 'True, l)) 'Nothing
-> Maybe (I Rational ('Just '( 'True, l)) 'Nothing)
recip' I Rational ('Just '( 'True, l)) 'Nothing
x = case I Rational ('Just '( 'True, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) 'Nothing
x of Integer
n :% Integer
d -> Rational -> Maybe (I Rational ('Just '( 'True, l)) 'Nothing)
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (Integer
d Integer -> Integer -> Rational
forall a. a -> a -> Ratio a
:% Integer
n)
  I Rational ('Just '( 'True, l)) 'Nothing
a plus' :: I Rational ('Just '( 'True, l)) 'Nothing
-> I Rational ('Just '( 'True, l)) 'Nothing
-> Maybe (I Rational ('Just '( 'True, l)) 'Nothing)
`plus'` I Rational ('Just '( 'True, l)) 'Nothing
b = Rational -> Maybe (I Rational ('Just '( 'True, l)) 'Nothing)
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational ('Just '( 'True, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) 'Nothing
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ I Rational ('Just '( 'True, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) 'Nothing
b)
  I Rational ('Just '( 'True, l)) 'Nothing
a mult' :: I Rational ('Just '( 'True, l)) 'Nothing
-> I Rational ('Just '( 'True, l)) 'Nothing
-> Maybe (I Rational ('Just '( 'True, l)) 'Nothing)
`mult'` I Rational ('Just '( 'True, l)) 'Nothing
b = Rational -> Maybe (I Rational ('Just '( 'True, l)) 'Nothing)
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational ('Just '( 'True, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) 'Nothing
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* I Rational ('Just '( 'True, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) 'Nothing
b)
  I Rational ('Just '( 'True, l)) 'Nothing
a minus' :: I Rational ('Just '( 'True, l)) 'Nothing
-> I Rational ('Just '( 'True, l)) 'Nothing
-> Maybe (I Rational ('Just '( 'True, l)) 'Nothing)
`minus'` I Rational ('Just '( 'True, l)) 'Nothing
b = Rational -> Maybe (I Rational ('Just '( 'True, l)) 'Nothing)
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational ('Just '( 'True, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) 'Nothing
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- I Rational ('Just '( 'True, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) 'Nothing
b)
  I Rational ('Just '( 'True, l)) 'Nothing
a div' :: I Rational ('Just '( 'True, l)) 'Nothing
-> I Rational ('Just '( 'True, l)) 'Nothing
-> Maybe (I Rational ('Just '( 'True, l)) 'Nothing)
`div'` I Rational ('Just '( 'True, l)) 'Nothing
b = do Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (I Rational ('Just '( 'True, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) 'Nothing
b Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
/= Rational
0)
                  Rational -> Maybe (I Rational ('Just '( 'True, l)) 'Nothing)
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational ('Just '( 'True, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) 'Nothing
a Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ I Rational ('Just '( 'True, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) 'Nothing
b)


instance forall l r.
  ( IntervalCtx    P.Rational ('Just '( 'False, l)) ('Just '( 'True, r))
  ) => Interval    P.Rational ('Just '( 'False, l)) ('Just '( 'True, r)) where
  type IntervalCtx P.Rational ('Just '( 'False, l)) ('Just '( 'True, r)) =
    (KR.KnownRational l, KR.KnownRational r, l < r)
  type MaxI P.Rational ('Just '( 'False, l)) ('Just '( 'True, r)) = r
  inhabitant :: I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
inhabitant = I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
forall x (l :: L x) (r :: R x). Known x l r (MaxI x l r) => I x l r
max
  from :: Rational
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'True, r)))
from = \Rational
x -> Rational -> I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
forall x (l :: L x) (r :: R x). x -> I x l r
unsafest Rational
x I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
-> Maybe ()
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'True, r)))
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Rational
l Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
< Rational
x Bool -> Bool -> Bool
&& Rational
x Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
<= Rational
r)
    where l :: Rational
l = Proxy l -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @l)
          r :: Rational
r = Proxy r -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @r)
  negate' :: I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'True, r)))
negate' = Rational
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'True, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (Rational
 -> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'True, r))))
-> (I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
    -> Rational)
-> I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'True, r)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Rational
forall a. Num a => a -> a
P.negate (Rational -> Rational)
-> (I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
    -> Rational)
-> I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
-> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I Rational ('Just '( 'False, l)) ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap
  recip' :: I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'True, r)))
recip' I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
x = case I Rational ('Just '( 'False, l)) ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
x of Integer
n :% Integer
d -> Rational
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'True, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (Integer
d Integer -> Integer -> Rational
forall a. a -> a -> Ratio a
:% Integer
n)
  I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
a plus' :: I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
-> I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'True, r)))
`plus'` I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
b = Rational
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'True, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational ('Just '( 'False, l)) ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ I Rational ('Just '( 'False, l)) ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
b)
  I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
a mult' :: I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
-> I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'True, r)))
`mult'` I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
b = Rational
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'True, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational ('Just '( 'False, l)) ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* I Rational ('Just '( 'False, l)) ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
b)
  I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
a minus' :: I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
-> I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'True, r)))
`minus'` I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
b = Rational
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'True, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational ('Just '( 'False, l)) ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- I Rational ('Just '( 'False, l)) ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
b)
  I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
a div' :: I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
-> I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'True, r)))
`div'` I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
b = do Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (I Rational ('Just '( 'False, l)) ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
b Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
/= Rational
0)
                  Rational
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'True, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational ('Just '( 'False, l)) ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
a Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ I Rational ('Just '( 'False, l)) ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
b)

instance forall r.
  ( IntervalCtx    P.Rational 'Nothing ('Just '( 'True, r))
  ) => Interval    P.Rational 'Nothing ('Just '( 'True, r)) where
  type IntervalCtx P.Rational 'Nothing ('Just '( 'True, r)) = KR.KnownRational r
  type MaxI P.Rational 'Nothing ('Just '( 'True, r)) = r
  inhabitant :: I Rational 'Nothing ('Just '( 'True, r))
inhabitant = I Rational 'Nothing ('Just '( 'True, r))
forall x (l :: L x) (r :: R x). Known x l r (MaxI x l r) => I x l r
max
  from :: Rational -> Maybe (I Rational 'Nothing ('Just '( 'True, r)))
from = \Rational
x -> Rational -> I Rational 'Nothing ('Just '( 'True, r))
forall x (l :: L x) (r :: R x). x -> I x l r
unsafest Rational
x I Rational 'Nothing ('Just '( 'True, r))
-> Maybe () -> Maybe (I Rational 'Nothing ('Just '( 'True, r)))
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Rational
x Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
<= Rational
r)
    where r :: Rational
r = Proxy r -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @r)
  negate' :: I Rational 'Nothing ('Just '( 'True, r))
-> Maybe (I Rational 'Nothing ('Just '( 'True, r)))
negate' = Rational -> Maybe (I Rational 'Nothing ('Just '( 'True, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (Rational -> Maybe (I Rational 'Nothing ('Just '( 'True, r))))
-> (I Rational 'Nothing ('Just '( 'True, r)) -> Rational)
-> I Rational 'Nothing ('Just '( 'True, r))
-> Maybe (I Rational 'Nothing ('Just '( 'True, r)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Rational
forall a. Num a => a -> a
P.negate (Rational -> Rational)
-> (I Rational 'Nothing ('Just '( 'True, r)) -> Rational)
-> I Rational 'Nothing ('Just '( 'True, r))
-> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I Rational 'Nothing ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap
  recip' :: I Rational 'Nothing ('Just '( 'True, r))
-> Maybe (I Rational 'Nothing ('Just '( 'True, r)))
recip' I Rational 'Nothing ('Just '( 'True, r))
x = case I Rational 'Nothing ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing ('Just '( 'True, r))
x of Integer
n :% Integer
d -> Rational -> Maybe (I Rational 'Nothing ('Just '( 'True, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (Integer
d Integer -> Integer -> Rational
forall a. a -> a -> Ratio a
:% Integer
n)
  I Rational 'Nothing ('Just '( 'True, r))
a plus' :: I Rational 'Nothing ('Just '( 'True, r))
-> I Rational 'Nothing ('Just '( 'True, r))
-> Maybe (I Rational 'Nothing ('Just '( 'True, r)))
`plus'` I Rational 'Nothing ('Just '( 'True, r))
b = Rational -> Maybe (I Rational 'Nothing ('Just '( 'True, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational 'Nothing ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing ('Just '( 'True, r))
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ I Rational 'Nothing ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing ('Just '( 'True, r))
b)
  I Rational 'Nothing ('Just '( 'True, r))
a mult' :: I Rational 'Nothing ('Just '( 'True, r))
-> I Rational 'Nothing ('Just '( 'True, r))
-> Maybe (I Rational 'Nothing ('Just '( 'True, r)))
`mult'` I Rational 'Nothing ('Just '( 'True, r))
b = Rational -> Maybe (I Rational 'Nothing ('Just '( 'True, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational 'Nothing ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing ('Just '( 'True, r))
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* I Rational 'Nothing ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing ('Just '( 'True, r))
b)
  I Rational 'Nothing ('Just '( 'True, r))
a minus' :: I Rational 'Nothing ('Just '( 'True, r))
-> I Rational 'Nothing ('Just '( 'True, r))
-> Maybe (I Rational 'Nothing ('Just '( 'True, r)))
`minus'` I Rational 'Nothing ('Just '( 'True, r))
b = Rational -> Maybe (I Rational 'Nothing ('Just '( 'True, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational 'Nothing ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing ('Just '( 'True, r))
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- I Rational 'Nothing ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing ('Just '( 'True, r))
b)
  I Rational 'Nothing ('Just '( 'True, r))
a div' :: I Rational 'Nothing ('Just '( 'True, r))
-> I Rational 'Nothing ('Just '( 'True, r))
-> Maybe (I Rational 'Nothing ('Just '( 'True, r)))
`div'` I Rational 'Nothing ('Just '( 'True, r))
b = do Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (I Rational 'Nothing ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing ('Just '( 'True, r))
b Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
/= Rational
0)
                  Rational -> Maybe (I Rational 'Nothing ('Just '( 'True, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational 'Nothing ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing ('Just '( 'True, r))
a Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ I Rational 'Nothing ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing ('Just '( 'True, r))
b)

instance forall l r.
  ( IntervalCtx    P.Rational ('Just '( 'False, l)) ('Just '( 'False, r))
  ) => Interval    P.Rational ('Just '( 'False, l)) ('Just '( 'False, r)) where
  type IntervalCtx P.Rational ('Just '( 'False, l)) ('Just '( 'False, r)) =
    (KR.KnownRational l, KR.KnownRational r, l < r)
  inhabitant :: I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
inhabitant = -- halfway between l and r
    let l' :: Rational
l' = Proxy l -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @l)
        r' :: Rational
r' = Proxy r -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @r)
    in Rational -> I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Rational
l' Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ (Rational
r' Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
l') Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ Rational
2)
  from :: Rational
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'False, r)))
from = \Rational
x -> Rational -> I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
forall x (l :: L x) (r :: R x). x -> I x l r
unsafest Rational
x I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
-> Maybe ()
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'False, r)))
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Rational
l Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
< Rational
x Bool -> Bool -> Bool
&& Rational
x Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
< Rational
r)
    where l :: Rational
l = Proxy l -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @l)
          r :: Rational
r = Proxy r -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @r)
  negate' :: I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'False, r)))
negate' = Rational
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'False, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (Rational
 -> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'False, r))))
-> (I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
    -> Rational)
-> I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'False, r)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Rational
forall a. Num a => a -> a
P.negate (Rational -> Rational)
-> (I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
    -> Rational)
-> I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
-> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I Rational ('Just '( 'False, l)) ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap
  recip' :: I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'False, r)))
recip' I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
x = case I Rational ('Just '( 'False, l)) ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
x of Integer
n :% Integer
d -> Rational
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'False, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (Integer
d Integer -> Integer -> Rational
forall a. a -> a -> Ratio a
:% Integer
n)
  I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
a plus' :: I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
-> I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'False, r)))
`plus'` I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
b = Rational
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'False, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational ('Just '( 'False, l)) ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ I Rational ('Just '( 'False, l)) ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
b)
  I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
a mult' :: I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
-> I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'False, r)))
`mult'` I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
b = Rational
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'False, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational ('Just '( 'False, l)) ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* I Rational ('Just '( 'False, l)) ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
b)
  I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
a minus' :: I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
-> I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'False, r)))
`minus'` I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
b = Rational
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'False, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational ('Just '( 'False, l)) ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- I Rational ('Just '( 'False, l)) ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
b)
  I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
a div' :: I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
-> I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'False, r)))
`div'` I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
b = do Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (I Rational ('Just '( 'False, l)) ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
b Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
/= Rational
0)
                  Rational
-> Maybe (I Rational ('Just '( 'False, l)) ('Just '( 'False, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational ('Just '( 'False, l)) ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
a Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ I Rational ('Just '( 'False, l)) ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
b)

instance forall r.
  ( IntervalCtx    P.Rational 'Nothing ('Just '( 'False, r))
  ) => Interval    P.Rational 'Nothing ('Just '( 'False, r)) where
  type IntervalCtx P.Rational 'Nothing ('Just '( 'False, r)) =
    KR.KnownRational r
  inhabitant :: I Rational 'Nothing ('Just '( 'False, r))
inhabitant = Rational -> I Rational 'Nothing ('Just '( 'False, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Proxy r -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @r) Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
1)
  from :: Rational -> Maybe (I Rational 'Nothing ('Just '( 'False, r)))
from = \Rational
x -> Rational -> I Rational 'Nothing ('Just '( 'False, r))
forall x (l :: L x) (r :: R x). x -> I x l r
unsafest Rational
x I Rational 'Nothing ('Just '( 'False, r))
-> Maybe () -> Maybe (I Rational 'Nothing ('Just '( 'False, r)))
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Rational
x Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
< Rational
r)
    where r :: Rational
r = Proxy r -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @r)
  negate' :: I Rational 'Nothing ('Just '( 'False, r))
-> Maybe (I Rational 'Nothing ('Just '( 'False, r)))
negate' = Rational -> Maybe (I Rational 'Nothing ('Just '( 'False, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (Rational -> Maybe (I Rational 'Nothing ('Just '( 'False, r))))
-> (I Rational 'Nothing ('Just '( 'False, r)) -> Rational)
-> I Rational 'Nothing ('Just '( 'False, r))
-> Maybe (I Rational 'Nothing ('Just '( 'False, r)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Rational
forall a. Num a => a -> a
P.negate (Rational -> Rational)
-> (I Rational 'Nothing ('Just '( 'False, r)) -> Rational)
-> I Rational 'Nothing ('Just '( 'False, r))
-> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I Rational 'Nothing ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap
  recip' :: I Rational 'Nothing ('Just '( 'False, r))
-> Maybe (I Rational 'Nothing ('Just '( 'False, r)))
recip' I Rational 'Nothing ('Just '( 'False, r))
x = case I Rational 'Nothing ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing ('Just '( 'False, r))
x of Integer
n :% Integer
d -> Rational -> Maybe (I Rational 'Nothing ('Just '( 'False, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (Integer
d Integer -> Integer -> Rational
forall a. a -> a -> Ratio a
:% Integer
n)
  I Rational 'Nothing ('Just '( 'False, r))
a plus' :: I Rational 'Nothing ('Just '( 'False, r))
-> I Rational 'Nothing ('Just '( 'False, r))
-> Maybe (I Rational 'Nothing ('Just '( 'False, r)))
`plus'` I Rational 'Nothing ('Just '( 'False, r))
b = Rational -> Maybe (I Rational 'Nothing ('Just '( 'False, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational 'Nothing ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing ('Just '( 'False, r))
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ I Rational 'Nothing ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing ('Just '( 'False, r))
b)
  I Rational 'Nothing ('Just '( 'False, r))
a mult' :: I Rational 'Nothing ('Just '( 'False, r))
-> I Rational 'Nothing ('Just '( 'False, r))
-> Maybe (I Rational 'Nothing ('Just '( 'False, r)))
`mult'` I Rational 'Nothing ('Just '( 'False, r))
b = Rational -> Maybe (I Rational 'Nothing ('Just '( 'False, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational 'Nothing ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing ('Just '( 'False, r))
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* I Rational 'Nothing ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing ('Just '( 'False, r))
b)
  I Rational 'Nothing ('Just '( 'False, r))
a minus' :: I Rational 'Nothing ('Just '( 'False, r))
-> I Rational 'Nothing ('Just '( 'False, r))
-> Maybe (I Rational 'Nothing ('Just '( 'False, r)))
`minus'` I Rational 'Nothing ('Just '( 'False, r))
b = Rational -> Maybe (I Rational 'Nothing ('Just '( 'False, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational 'Nothing ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing ('Just '( 'False, r))
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- I Rational 'Nothing ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing ('Just '( 'False, r))
b)
  I Rational 'Nothing ('Just '( 'False, r))
a div' :: I Rational 'Nothing ('Just '( 'False, r))
-> I Rational 'Nothing ('Just '( 'False, r))
-> Maybe (I Rational 'Nothing ('Just '( 'False, r)))
`div'` I Rational 'Nothing ('Just '( 'False, r))
b = do Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (I Rational 'Nothing ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing ('Just '( 'False, r))
b Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
/= Rational
0)
                  Rational -> Maybe (I Rational 'Nothing ('Just '( 'False, r)))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational 'Nothing ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing ('Just '( 'False, r))
a Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ I Rational 'Nothing ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing ('Just '( 'False, r))
b)

instance forall l.
  ( IntervalCtx    P.Rational ('Just '( 'False, l)) 'Nothing
  ) => Interval    P.Rational ('Just '( 'False, l)) 'Nothing where
  type IntervalCtx P.Rational ('Just '( 'False, l)) 'Nothing =
    KR.KnownRational l
  inhabitant :: I Rational ('Just '( 'False, l)) 'Nothing
inhabitant = Rational -> I Rational ('Just '( 'False, l)) 'Nothing
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Proxy l -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @l) Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ Rational
1)
  from :: Rational -> Maybe (I Rational ('Just '( 'False, l)) 'Nothing)
from = \Rational
x -> Rational -> I Rational ('Just '( 'False, l)) 'Nothing
forall x (l :: L x) (r :: R x). x -> I x l r
unsafest Rational
x I Rational ('Just '( 'False, l)) 'Nothing
-> Maybe () -> Maybe (I Rational ('Just '( 'False, l)) 'Nothing)
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Rational
l Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
< Rational
x)
    where l :: Rational
l = Proxy l -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @l)
  negate' :: I Rational ('Just '( 'False, l)) 'Nothing
-> Maybe (I Rational ('Just '( 'False, l)) 'Nothing)
negate' = Rational -> Maybe (I Rational ('Just '( 'False, l)) 'Nothing)
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (Rational -> Maybe (I Rational ('Just '( 'False, l)) 'Nothing))
-> (I Rational ('Just '( 'False, l)) 'Nothing -> Rational)
-> I Rational ('Just '( 'False, l)) 'Nothing
-> Maybe (I Rational ('Just '( 'False, l)) 'Nothing)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Rational
forall a. Num a => a -> a
P.negate (Rational -> Rational)
-> (I Rational ('Just '( 'False, l)) 'Nothing -> Rational)
-> I Rational ('Just '( 'False, l)) 'Nothing
-> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I Rational ('Just '( 'False, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap
  recip' :: I Rational ('Just '( 'False, l)) 'Nothing
-> Maybe (I Rational ('Just '( 'False, l)) 'Nothing)
recip' I Rational ('Just '( 'False, l)) 'Nothing
x = case I Rational ('Just '( 'False, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) 'Nothing
x of Integer
n :% Integer
d -> Rational -> Maybe (I Rational ('Just '( 'False, l)) 'Nothing)
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (Integer
d Integer -> Integer -> Rational
forall a. a -> a -> Ratio a
:% Integer
n)
  I Rational ('Just '( 'False, l)) 'Nothing
a plus' :: I Rational ('Just '( 'False, l)) 'Nothing
-> I Rational ('Just '( 'False, l)) 'Nothing
-> Maybe (I Rational ('Just '( 'False, l)) 'Nothing)
`plus'` I Rational ('Just '( 'False, l)) 'Nothing
b = Rational -> Maybe (I Rational ('Just '( 'False, l)) 'Nothing)
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational ('Just '( 'False, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) 'Nothing
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ I Rational ('Just '( 'False, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) 'Nothing
b)
  I Rational ('Just '( 'False, l)) 'Nothing
a mult' :: I Rational ('Just '( 'False, l)) 'Nothing
-> I Rational ('Just '( 'False, l)) 'Nothing
-> Maybe (I Rational ('Just '( 'False, l)) 'Nothing)
`mult'` I Rational ('Just '( 'False, l)) 'Nothing
b = Rational -> Maybe (I Rational ('Just '( 'False, l)) 'Nothing)
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational ('Just '( 'False, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) 'Nothing
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* I Rational ('Just '( 'False, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) 'Nothing
b)
  I Rational ('Just '( 'False, l)) 'Nothing
a minus' :: I Rational ('Just '( 'False, l)) 'Nothing
-> I Rational ('Just '( 'False, l)) 'Nothing
-> Maybe (I Rational ('Just '( 'False, l)) 'Nothing)
`minus'` I Rational ('Just '( 'False, l)) 'Nothing
b = Rational -> Maybe (I Rational ('Just '( 'False, l)) 'Nothing)
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational ('Just '( 'False, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) 'Nothing
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- I Rational ('Just '( 'False, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) 'Nothing
b)
  I Rational ('Just '( 'False, l)) 'Nothing
a div' :: I Rational ('Just '( 'False, l)) 'Nothing
-> I Rational ('Just '( 'False, l)) 'Nothing
-> Maybe (I Rational ('Just '( 'False, l)) 'Nothing)
`div'` I Rational ('Just '( 'False, l)) 'Nothing
b = do Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (I Rational ('Just '( 'False, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) 'Nothing
b Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
/= Rational
0)
                  Rational -> Maybe (I Rational ('Just '( 'False, l)) 'Nothing)
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Rational ('Just '( 'False, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) 'Nothing
a Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ I Rational ('Just '( 'False, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) 'Nothing
b)

instance Interval P.Rational 'Nothing 'Nothing where
  inhabitant :: I Rational 'Nothing 'Nothing
inhabitant = I Rational 'Nothing 'Nothing
forall x (l :: L x) (r :: R x). Zero x l r => I x l r
zero
  from :: Rational -> Maybe (I Rational 'Nothing 'Nothing)
from = I Rational 'Nothing 'Nothing
-> Maybe (I Rational 'Nothing 'Nothing)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (I Rational 'Nothing 'Nothing
 -> Maybe (I Rational 'Nothing 'Nothing))
-> (Rational -> I Rational 'Nothing 'Nothing)
-> Rational
-> Maybe (I Rational 'Nothing 'Nothing)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> I Rational 'Nothing 'Nothing
Rational -> I Rational (MinL Rational) (MaxR Rational)
forall x.
Interval x (MinL x) (MaxR x) =>
x -> I x (MinL x) (MaxR x)
wrap
  negate' :: I Rational 'Nothing 'Nothing
-> Maybe (I Rational 'Nothing 'Nothing)
negate' = I Rational 'Nothing 'Nothing
-> Maybe (I Rational 'Nothing 'Nothing)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (I Rational 'Nothing 'Nothing
 -> Maybe (I Rational 'Nothing 'Nothing))
-> (I Rational 'Nothing 'Nothing -> I Rational 'Nothing 'Nothing)
-> I Rational 'Nothing 'Nothing
-> Maybe (I Rational 'Nothing 'Nothing)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> I Rational 'Nothing 'Nothing
Rational -> I Rational (MinL Rational) (MaxR Rational)
forall x.
Interval x (MinL x) (MaxR x) =>
x -> I x (MinL x) (MaxR x)
wrap (Rational -> I Rational 'Nothing 'Nothing)
-> (I Rational 'Nothing 'Nothing -> Rational)
-> I Rational 'Nothing 'Nothing
-> I Rational 'Nothing 'Nothing
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Rational
forall a. Num a => a -> a
P.negate (Rational -> Rational)
-> (I Rational 'Nothing 'Nothing -> Rational)
-> I Rational 'Nothing 'Nothing
-> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I Rational 'Nothing 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap
  recip' :: I Rational 'Nothing 'Nothing
-> Maybe (I Rational 'Nothing 'Nothing)
recip' I Rational 'Nothing 'Nothing
x = case I Rational 'Nothing 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing 'Nothing
x of Integer
n :% Integer
d -> Rational -> Maybe (I Rational 'Nothing 'Nothing)
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (Integer
d Integer -> Integer -> Rational
forall a. a -> a -> Ratio a
:% Integer
n)
  I Rational 'Nothing 'Nothing
a plus' :: I Rational 'Nothing 'Nothing
-> I Rational 'Nothing 'Nothing
-> Maybe (I Rational 'Nothing 'Nothing)
`plus'` I Rational 'Nothing 'Nothing
b = I Rational 'Nothing 'Nothing
-> Maybe (I Rational 'Nothing 'Nothing)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (I Rational 'Nothing 'Nothing
a I Rational 'Nothing 'Nothing
-> I Rational 'Nothing 'Nothing -> I Rational 'Nothing 'Nothing
forall x (l :: L x) (r :: R x).
Plus x l r =>
I x l r -> I x l r -> I x l r
`plus` I Rational 'Nothing 'Nothing
b)
  I Rational 'Nothing 'Nothing
a mult' :: I Rational 'Nothing 'Nothing
-> I Rational 'Nothing 'Nothing
-> Maybe (I Rational 'Nothing 'Nothing)
`mult'` I Rational 'Nothing 'Nothing
b = I Rational 'Nothing 'Nothing
-> Maybe (I Rational 'Nothing 'Nothing)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (I Rational 'Nothing 'Nothing
a I Rational 'Nothing 'Nothing
-> I Rational 'Nothing 'Nothing -> I Rational 'Nothing 'Nothing
forall x (l :: L x) (r :: R x).
Mult x l r =>
I x l r -> I x l r -> I x l r
`mult` I Rational 'Nothing 'Nothing
b)
  I Rational 'Nothing 'Nothing
a minus' :: I Rational 'Nothing 'Nothing
-> I Rational 'Nothing 'Nothing
-> Maybe (I Rational 'Nothing 'Nothing)
`minus'` I Rational 'Nothing 'Nothing
b = I Rational 'Nothing 'Nothing
-> Maybe (I Rational 'Nothing 'Nothing)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (I Rational 'Nothing 'Nothing
a I Rational 'Nothing 'Nothing
-> I Rational 'Nothing 'Nothing -> I Rational 'Nothing 'Nothing
forall x (l :: L x) (r :: R x).
Minus x l r =>
I x l r -> I x l r -> I x l r
`minus` I Rational 'Nothing 'Nothing
b)
  I Rational 'Nothing 'Nothing
a div' :: I Rational 'Nothing 'Nothing
-> I Rational 'Nothing 'Nothing
-> Maybe (I Rational 'Nothing 'Nothing)
`div'` I Rational 'Nothing 'Nothing
b = do Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (I Rational 'Nothing 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing 'Nothing
b Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
/= Rational
0)
                  I Rational 'Nothing 'Nothing
-> Maybe (I Rational 'Nothing 'Nothing)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rational -> I Rational (MinL Rational) (MaxR Rational)
forall x.
Interval x (MinL x) (MaxR x) =>
x -> I x (MinL x) (MaxR x)
wrap (I Rational 'Nothing 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing 'Nothing
a Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ I Rational 'Nothing 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing 'Nothing
b))

--------------------------------------------------------------------------------

instance (Interval Rational ('Just '( 'True, l)) ('Just '( 'True, r)))
  => Clamp         Rational ('Just '( 'True, l)) ('Just '( 'True, r))

instance (Interval Rational ('Just '( 'True, l)) 'Nothing)
  => Clamp         Rational ('Just '( 'True, l)) 'Nothing where
  clamp :: Rational -> I Rational ('Just '( 'True, l)) 'Nothing
clamp = \case
    Rational
x | Rational
x Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
<= I Rational ('Just '( 'True, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) 'Nothing
min_ -> I Rational ('Just '( 'True, l)) 'Nothing
min_
      | Bool
otherwise -> Rational -> I Rational ('Just '( 'True, l)) 'Nothing
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe Rational
x
    where min_ :: I Rational ('Just '( 'True, l)) 'Nothing
min_ = I Rational ('Just '( 'True, l)) 'Nothing
forall x (l :: L x) (r :: R x). Known x l r (MinI x l r) => I x l r
min

instance (Interval Rational 'Nothing ('Just '( 'True, r)))
  => Clamp         Rational 'Nothing ('Just '( 'True, r)) where
  clamp :: Rational -> I Rational 'Nothing ('Just '( 'True, r))
clamp = \case
    Rational
x | Rational
x Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
>= I Rational 'Nothing ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing ('Just '( 'True, r))
max_ -> I Rational 'Nothing ('Just '( 'True, r))
max_
      | Bool
otherwise -> Rational -> I Rational 'Nothing ('Just '( 'True, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe Rational
x
    where max_ :: I Rational 'Nothing ('Just '( 'True, r))
max_ = I Rational 'Nothing ('Just '( 'True, r))
forall x (l :: L x) (r :: R x). Known x l r (MaxI x l r) => I x l r
max

instance (Interval Rational 'Nothing 'Nothing)
  => Clamp         Rational 'Nothing 'Nothing where
  clamp :: Rational -> I Rational 'Nothing 'Nothing
clamp = Rational -> I Rational 'Nothing 'Nothing
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe

--------------------------------------------------------------------------------

-- OO
instance
  ( Interval Rational ('Just '( 'False, ld)) ('Just '( 'False, rd))
  , Interval Rational ('Just '( 'False, lu)) ('Just '( 'False, ru))
  , lu <= ld
  , rd <= ru )
  => Up Rational ('Just '( 'False, ld)) ('Just '( 'False, rd))
                 ('Just '( 'False, lu)) ('Just '( 'False, ru))

-- OC
instance
  ( Interval Rational ('Just '( 'False, ld)) ('Just '( ird  , rd))
  , Interval Rational ('Just '( 'False, lu)) ('Just '( 'True, ru))
  , lu <= ld
  , rd <= ru )
  => Up Rational ('Just '( 'False, ld)) ('Just '( ird  , rd))
                 ('Just '( 'False, lu)) ('Just '( 'True, ru))

-- OU
instance
  ( Interval Rational ('Just '( 'False, ld)) yrd
  , Interval Rational ('Just '( 'False, lu)) 'Nothing
  , lu <= ld )
  => Up Rational ('Just '( 'False, ld)) yrd
                 ('Just '( 'False, lu)) 'Nothing

-- CO
instance
  ( Interval Rational ('Just '( ild  , ld)) ('Just '( 'False, rd))
  , Interval Rational ('Just '( 'True, lu)) ('Just '( 'False, ru))
  , lu <= ld
  , rd <= ru )
  => Up Rational ('Just '( ild  , ld)) ('Just '( 'False, rd))
                 ('Just '( 'True, lu)) ('Just '( 'False, ru))

-- CC
instance
  ( Interval Rational ('Just '( ild  , ld)) ('Just '( ird  , rd))
  , Interval Rational ('Just '( 'True, lu)) ('Just '( 'True, ru))
  , lu <= ld
  , rd <= ru )
  => Up Rational ('Just '( ild  , ld)) ('Just '( ird  , rd))
                 ('Just '( 'True, lu)) ('Just '( 'True, ru))

-- CU
instance
  ( Interval Rational ('Just '( ild  , ld)) yrd
  , Interval Rational ('Just '( 'True, lu)) 'Nothing
  , lu <= ld )
  => Up Rational ('Just '( ild  , ld)) yrd
                 ('Just '( 'True, lu)) 'Nothing

-- UO
instance
  ( Interval Rational yld      ('Just '( 'False, rd))
  , Interval Rational 'Nothing ('Just '( 'False, ru))
  , ru <= rd )
  => Up Rational yld      ('Just '( 'False, rd))
                 'Nothing ('Just '( 'False, ru))

-- UC
instance
  ( Interval Rational yld      ('Just '( ird  , rd))
  , Interval Rational 'Nothing ('Just '( 'True, ru))
  , ru <= rd )
  => Up Rational yld      ('Just '( ird  , rd))
                 'Nothing ('Just '( 'True, ru))

-- UU
instance
  ( Interval Rational yld      yrd
  , Interval Rational 'Nothing 'Nothing )
  => Up Rational yld      yrd
                 'Nothing 'Nothing

--------------------------------------------------------------------------------


instance forall t l r.
  ( Interval P.Rational ('Just '( 'True, l)) ('Just '( 'True, r))
  , KnownCtx P.Rational ('Just '( 'True, l)) ('Just '( 'True, r)) t
  ) => Known P.Rational ('Just '( 'True, l)) ('Just '( 'True, r)) t where
  type KnownCtx P.Rational ('Just '( 'True, l)) ('Just '( 'True, r)) t =
    (KR.KnownRational t, l <= t, t <= r)
  known' :: Proxy t -> I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
known' = Rational -> I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Rational -> I Rational ('Just '( 'True, l)) ('Just '( 'True, r)))
-> (Proxy t -> Rational)
-> Proxy t
-> I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy t -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal

instance forall t l r.
  ( Interval P.Rational ('Just '( 'True, l)) ('Just '( 'False, r))
  , KnownCtx P.Rational ('Just '( 'True, l)) ('Just '( 'False, r)) t
  ) => Known P.Rational ('Just '( 'True, l)) ('Just '( 'False, r)) t where
  type KnownCtx P.Rational ('Just '( 'True, l)) ('Just '( 'False, r)) t =
    (KR.KnownRational t, l <= t, t < r)
  known' :: Proxy t -> I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
known' = Rational -> I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Rational -> I Rational ('Just '( 'True, l)) ('Just '( 'False, r)))
-> (Proxy t -> Rational)
-> Proxy t
-> I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy t -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal

instance forall t l.
  ( Interval P.Rational ('Just '( 'True, l)) 'Nothing
  , KnownCtx P.Rational ('Just '( 'True, l)) 'Nothing t
  ) => Known P.Rational ('Just '( 'True, l)) 'Nothing t where
  type KnownCtx P.Rational ('Just '( 'True, l)) 'Nothing t =
    (KR.KnownRational t, l <= t)
  known' :: Proxy t -> I Rational ('Just '( 'True, l)) 'Nothing
known' = Rational -> I Rational ('Just '( 'True, l)) 'Nothing
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Rational -> I Rational ('Just '( 'True, l)) 'Nothing)
-> (Proxy t -> Rational)
-> Proxy t
-> I Rational ('Just '( 'True, l)) 'Nothing
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy t -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal

instance forall t l r.
  ( Interval P.Rational ('Just '( 'False, l)) ('Just '( 'True, r))
  , KnownCtx P.Rational ('Just '( 'False, l)) ('Just '( 'True, r)) t
  ) => Known P.Rational ('Just '( 'False, l)) ('Just '( 'True, r)) t where
  type KnownCtx P.Rational ('Just '( 'False, l)) ('Just '( 'True, r)) t =
    (KR.KnownRational t, l < t, t <= r)
  known' :: Proxy t -> I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
known' = Rational -> I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Rational -> I Rational ('Just '( 'False, l)) ('Just '( 'True, r)))
-> (Proxy t -> Rational)
-> Proxy t
-> I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy t -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal

instance forall t l.
  ( Interval P.Rational ('Just '( 'False, l)) 'Nothing
  , KnownCtx P.Rational ('Just '( 'False, l)) 'Nothing t
  ) => Known P.Rational ('Just '( 'False, l)) 'Nothing t where
  type KnownCtx P.Rational ('Just '( 'False, l)) 'Nothing t =
    (KR.KnownRational t, l < t)
  known' :: Proxy t -> I Rational ('Just '( 'False, l)) 'Nothing
known' = Rational -> I Rational ('Just '( 'False, l)) 'Nothing
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Rational -> I Rational ('Just '( 'False, l)) 'Nothing)
-> (Proxy t -> Rational)
-> Proxy t
-> I Rational ('Just '( 'False, l)) 'Nothing
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy t -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal

instance forall t r.
  ( Interval P.Rational 'Nothing ('Just '( 'True, r))
  , KnownCtx P.Rational 'Nothing ('Just '( 'True, r)) t
  ) => Known P.Rational 'Nothing ('Just '( 'True, r)) t where
  type KnownCtx P.Rational 'Nothing ('Just '( 'True, r)) t =
    (KR.KnownRational t, t <= r)
  known' :: Proxy t -> I Rational 'Nothing ('Just '( 'True, r))
known' = Rational -> I Rational 'Nothing ('Just '( 'True, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Rational -> I Rational 'Nothing ('Just '( 'True, r)))
-> (Proxy t -> Rational)
-> Proxy t
-> I Rational 'Nothing ('Just '( 'True, r))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy t -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal

instance forall t r.
  ( Interval P.Rational 'Nothing ('Just '( 'False, r))
  , KnownCtx P.Rational 'Nothing ('Just '( 'False, r)) t
  ) => Known P.Rational 'Nothing ('Just '( 'False, r)) t where
  type KnownCtx P.Rational 'Nothing ('Just '( 'False, r)) t =
    (KR.KnownRational t, t < r)
  known' :: Proxy t -> I Rational 'Nothing ('Just '( 'False, r))
known' = Rational -> I Rational 'Nothing ('Just '( 'False, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Rational -> I Rational 'Nothing ('Just '( 'False, r)))
-> (Proxy t -> Rational)
-> Proxy t
-> I Rational 'Nothing ('Just '( 'False, r))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy t -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal

instance forall t l r.
  ( Interval P.Rational ('Just '( 'False, l)) ('Just '( 'False, r))
  , KnownCtx P.Rational ('Just '( 'False, l)) ('Just '( 'False, r)) t
  ) => Known P.Rational ('Just '( 'False, l)) ('Just '( 'False, r)) t where
  type KnownCtx P.Rational ('Just '( 'False, l)) ('Just '( 'False, r)) t =
    (KR.KnownRational t, l < t, t < r)
  known' :: Proxy t -> I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
known' = Rational -> I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Rational
 -> I Rational ('Just '( 'False, l)) ('Just '( 'False, r)))
-> (Proxy t -> Rational)
-> Proxy t
-> I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy t -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal

instance forall t.
  ( KnownCtx P.Rational 'Nothing 'Nothing t
  ) => Known P.Rational 'Nothing 'Nothing t where
  type KnownCtx P.Rational 'Nothing 'Nothing t = KR.KnownRational t
  known' :: Proxy t -> I Rational 'Nothing 'Nothing
known' = Rational -> I Rational 'Nothing 'Nothing
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Rational -> I Rational 'Nothing 'Nothing)
-> (Proxy t -> Rational) -> Proxy t -> I Rational 'Nothing 'Nothing
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy t -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal

--------------------------------------------------------------------------------

instance forall l r.
  ( Interval P.Rational ('Just '( 'True, l)) ('Just '( 'True, r))
  ) => With  P.Rational ('Just '( 'True, l)) ('Just '( 'True, r)) where
  with :: forall b.
I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
-> (forall (t :: T Rational).
    Known Rational ('Just '( 'True, l)) ('Just '( 'True, r)) t =>
    Proxy t -> b)
-> b
with I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
x forall (t :: T Rational).
Known Rational ('Just '( 'True, l)) ('Just '( 'True, r)) t =>
Proxy t -> b
g = case Rational -> SomeRational
KR.someRationalVal (I Rational ('Just '( 'True, l)) ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
x) of
    KR.SomeRational (Proxy n
pt :: Proxy t) ->
      b -> Maybe b -> b
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> b
forall a. HasCallStack => [Char] -> a
error [Char]
"I.with(Rational): impossible") (Maybe b -> b) -> Maybe b -> b
forall a b. (a -> b) -> a -> b
$ do
        Dict
  (Assert
     (OrdCond
        (CmpRational_ (Normalize l) (Normalize n)) 'True 'True 'False)
     (TypeError ...))
Dict <- forall (a :: Rational) (b :: Rational).
(KnownRational a, KnownRational b) =>
Maybe (Dict (a <= b))
le @l @t
        Dict
  (Assert
     (OrdCond
        (CmpRational_ (Normalize n) (Normalize r)) 'True 'True 'False)
     (TypeError ...))
Dict <- forall (a :: Rational) (b :: Rational).
(KnownRational a, KnownRational b) =>
Maybe (Dict (a <= b))
le @t @r
        b -> Maybe b
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proxy n -> b
forall (t :: T Rational).
Known Rational ('Just '( 'True, l)) ('Just '( 'True, r)) t =>
Proxy t -> b
g Proxy n
Proxy n
pt)

instance forall l r.
  ( Interval P.Rational ('Just '( 'True, l)) ('Just '( 'False, r))
  ) => With  P.Rational ('Just '( 'True, l)) ('Just '( 'False, r)) where
  with :: forall b.
I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
-> (forall (t :: T Rational).
    Known Rational ('Just '( 'True, l)) ('Just '( 'False, r)) t =>
    Proxy t -> b)
-> b
with I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
x forall (t :: T Rational).
Known Rational ('Just '( 'True, l)) ('Just '( 'False, r)) t =>
Proxy t -> b
g = case Rational -> SomeRational
KR.someRationalVal (I Rational ('Just '( 'True, l)) ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
x) of
    KR.SomeRational (Proxy n
pt :: Proxy t) ->
      b -> Maybe b -> b
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> b
forall a. HasCallStack => [Char] -> a
error [Char]
"I.with(Rational): impossible") (Maybe b -> b) -> Maybe b -> b
forall a b. (a -> b) -> a -> b
$ do
        Dict
  (Assert
     (OrdCond
        (CmpRational_ (Normalize l) (Normalize n)) 'True 'True 'False)
     (TypeError ...))
Dict <- forall (a :: Rational) (b :: Rational).
(KnownRational a, KnownRational b) =>
Maybe (Dict (a <= b))
le @l @t
        Dict
  (Assert
     (OrdCond
        (CmpRational_ (Normalize n) (Normalize r)) 'True 'False 'False)
     (TypeError ...))
Dict <- forall (a :: Rational) (b :: Rational).
(KnownRational a, KnownRational b) =>
Maybe (Dict (a < b))
lt @t @r
        b -> Maybe b
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proxy n -> b
forall (t :: T Rational).
Known Rational ('Just '( 'True, l)) ('Just '( 'False, r)) t =>
Proxy t -> b
g Proxy n
Proxy n
pt)

instance forall l.
  ( Interval P.Rational ('Just '( 'True, l)) 'Nothing
  ) => With  P.Rational ('Just '( 'True, l)) 'Nothing where
  with :: forall b.
I Rational ('Just '( 'True, l)) 'Nothing
-> (forall (t :: T Rational).
    Known Rational ('Just '( 'True, l)) 'Nothing t =>
    Proxy t -> b)
-> b
with I Rational ('Just '( 'True, l)) 'Nothing
x forall (t :: T Rational).
Known Rational ('Just '( 'True, l)) 'Nothing t =>
Proxy t -> b
g = case Rational -> SomeRational
KR.someRationalVal (I Rational ('Just '( 'True, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'True, l)) 'Nothing
x) of
    KR.SomeRational (Proxy n
pt :: Proxy t) ->
      b -> Maybe b -> b
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> b
forall a. HasCallStack => [Char] -> a
error [Char]
"I.with(Rational): impossible") (Maybe b -> b) -> Maybe b -> b
forall a b. (a -> b) -> a -> b
$ do
        Dict
  (Assert
     (OrdCond
        (CmpRational_ (Normalize l) (Normalize n)) 'True 'True 'False)
     (TypeError ...))
Dict <- forall (a :: Rational) (b :: Rational).
(KnownRational a, KnownRational b) =>
Maybe (Dict (a <= b))
le @l @t
        b -> Maybe b
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proxy n -> b
forall (t :: T Rational).
Known Rational ('Just '( 'True, l)) 'Nothing t =>
Proxy t -> b
g Proxy n
Proxy n
pt)

instance forall l.
  ( Interval P.Rational ('Just '( 'False, l)) 'Nothing
  ) => With  P.Rational ('Just '( 'False, l)) 'Nothing where
  with :: forall b.
I Rational ('Just '( 'False, l)) 'Nothing
-> (forall (t :: T Rational).
    Known Rational ('Just '( 'False, l)) 'Nothing t =>
    Proxy t -> b)
-> b
with I Rational ('Just '( 'False, l)) 'Nothing
x forall (t :: T Rational).
Known Rational ('Just '( 'False, l)) 'Nothing t =>
Proxy t -> b
g = case Rational -> SomeRational
KR.someRationalVal (I Rational ('Just '( 'False, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) 'Nothing
x) of
    KR.SomeRational (Proxy n
pt :: Proxy t) ->
      b -> Maybe b -> b
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> b
forall a. HasCallStack => [Char] -> a
error [Char]
"I.with(Rational): impossible") (Maybe b -> b) -> Maybe b -> b
forall a b. (a -> b) -> a -> b
$ do
        Dict
  (Assert
     (OrdCond
        (CmpRational_ (Normalize l) (Normalize n)) 'True 'False 'False)
     (TypeError ...))
Dict <- forall (a :: Rational) (b :: Rational).
(KnownRational a, KnownRational b) =>
Maybe (Dict (a < b))
lt @l @t
        b -> Maybe b
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proxy n -> b
forall (t :: T Rational).
Known Rational ('Just '( 'False, l)) 'Nothing t =>
Proxy t -> b
g Proxy n
Proxy n
pt)

instance forall l r.
  ( Interval P.Rational ('Just '( 'False, l)) ('Just '( 'True, r))
  ) => With  P.Rational ('Just '( 'False, l)) ('Just '( 'True, r)) where
  with :: forall b.
I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
-> (forall (t :: T Rational).
    Known Rational ('Just '( 'False, l)) ('Just '( 'True, r)) t =>
    Proxy t -> b)
-> b
with I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
x forall (t :: T Rational).
Known Rational ('Just '( 'False, l)) ('Just '( 'True, r)) t =>
Proxy t -> b
g = case Rational -> SomeRational
KR.someRationalVal (I Rational ('Just '( 'False, l)) ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
x) of
    KR.SomeRational (Proxy n
pt :: Proxy t) ->
      b -> Maybe b -> b
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> b
forall a. HasCallStack => [Char] -> a
error [Char]
"I.with(Rational): impossible") (Maybe b -> b) -> Maybe b -> b
forall a b. (a -> b) -> a -> b
$ do
        Dict
  (Assert
     (OrdCond
        (CmpRational_ (Normalize l) (Normalize n)) 'True 'False 'False)
     (TypeError ...))
Dict <- forall (a :: Rational) (b :: Rational).
(KnownRational a, KnownRational b) =>
Maybe (Dict (a < b))
lt @l @t
        Dict
  (Assert
     (OrdCond
        (CmpRational_ (Normalize n) (Normalize r)) 'True 'True 'False)
     (TypeError ...))
Dict <- forall (a :: Rational) (b :: Rational).
(KnownRational a, KnownRational b) =>
Maybe (Dict (a <= b))
le @t @r
        b -> Maybe b
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proxy n -> b
forall (t :: T Rational).
Known Rational ('Just '( 'False, l)) ('Just '( 'True, r)) t =>
Proxy t -> b
g Proxy n
Proxy n
pt)

instance forall r.
  ( Interval P.Rational 'Nothing ('Just '( 'True, r))
  ) => With  P.Rational 'Nothing ('Just '( 'True, r)) where
  with :: forall b.
I Rational 'Nothing ('Just '( 'True, r))
-> (forall (t :: T Rational).
    Known Rational 'Nothing ('Just '( 'True, r)) t =>
    Proxy t -> b)
-> b
with I Rational 'Nothing ('Just '( 'True, r))
x forall (t :: T Rational).
Known Rational 'Nothing ('Just '( 'True, r)) t =>
Proxy t -> b
g = case Rational -> SomeRational
KR.someRationalVal (I Rational 'Nothing ('Just '( 'True, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing ('Just '( 'True, r))
x) of
    KR.SomeRational (Proxy n
pt :: Proxy t) ->
      b -> Maybe b -> b
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> b
forall a. HasCallStack => [Char] -> a
error [Char]
"I.with(Rational): impossible") (Maybe b -> b) -> Maybe b -> b
forall a b. (a -> b) -> a -> b
$ do
        Dict
  (Assert
     (OrdCond
        (CmpRational_ (Normalize n) (Normalize r)) 'True 'True 'False)
     (TypeError ...))
Dict <- forall (a :: Rational) (b :: Rational).
(KnownRational a, KnownRational b) =>
Maybe (Dict (a <= b))
le @t @r
        b -> Maybe b
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proxy n -> b
forall (t :: T Rational).
Known Rational 'Nothing ('Just '( 'True, r)) t =>
Proxy t -> b
g Proxy n
Proxy n
pt)

instance forall l r.
  ( Interval P.Rational ('Just '( 'False, l)) ('Just '( 'False, r))
  ) => With  P.Rational ('Just '( 'False, l)) ('Just '( 'False, r)) where
  with :: forall b.
I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
-> (forall (t :: T Rational).
    Known Rational ('Just '( 'False, l)) ('Just '( 'False, r)) t =>
    Proxy t -> b)
-> b
with I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
x forall (t :: T Rational).
Known Rational ('Just '( 'False, l)) ('Just '( 'False, r)) t =>
Proxy t -> b
g = case Rational -> SomeRational
KR.someRationalVal (I Rational ('Just '( 'False, l)) ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
x) of
    KR.SomeRational (Proxy n
pt :: Proxy t) ->
      b -> Maybe b -> b
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> b
forall a. HasCallStack => [Char] -> a
error [Char]
"I.with(Rational): impossible") (Maybe b -> b) -> Maybe b -> b
forall a b. (a -> b) -> a -> b
$ do
        Dict
  (Assert
     (OrdCond
        (CmpRational_ (Normalize l) (Normalize n)) 'True 'False 'False)
     (TypeError ...))
Dict <- forall (a :: Rational) (b :: Rational).
(KnownRational a, KnownRational b) =>
Maybe (Dict (a < b))
lt @l @t
        Dict
  (Assert
     (OrdCond
        (CmpRational_ (Normalize n) (Normalize r)) 'True 'False 'False)
     (TypeError ...))
Dict <- forall (a :: Rational) (b :: Rational).
(KnownRational a, KnownRational b) =>
Maybe (Dict (a < b))
lt @t @r
        b -> Maybe b
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proxy n -> b
forall (t :: T Rational).
Known Rational ('Just '( 'False, l)) ('Just '( 'False, r)) t =>
Proxy t -> b
g Proxy n
Proxy n
pt)

instance forall r.
  ( Interval P.Rational 'Nothing ('Just '( 'False, r))
  ) => With  P.Rational 'Nothing ('Just '( 'False, r)) where
  with :: forall b.
I Rational 'Nothing ('Just '( 'False, r))
-> (forall (t :: T Rational).
    Known Rational 'Nothing ('Just '( 'False, r)) t =>
    Proxy t -> b)
-> b
with I Rational 'Nothing ('Just '( 'False, r))
x forall (t :: T Rational).
Known Rational 'Nothing ('Just '( 'False, r)) t =>
Proxy t -> b
g = case Rational -> SomeRational
KR.someRationalVal (I Rational 'Nothing ('Just '( 'False, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing ('Just '( 'False, r))
x) of
    KR.SomeRational (Proxy n
pt :: Proxy t) ->
      b -> Maybe b -> b
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> b
forall a. HasCallStack => [Char] -> a
error [Char]
"I.with(Rational): impossible") (Maybe b -> b) -> Maybe b -> b
forall a b. (a -> b) -> a -> b
$ do
        Dict
  (Assert
     (OrdCond
        (CmpRational_ (Normalize n) (Normalize r)) 'True 'False 'False)
     (TypeError ...))
Dict <- forall (a :: Rational) (b :: Rational).
(KnownRational a, KnownRational b) =>
Maybe (Dict (a < b))
lt @t @r
        b -> Maybe b
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proxy n -> b
forall (t :: T Rational).
Known Rational 'Nothing ('Just '( 'False, r)) t =>
Proxy t -> b
g Proxy n
Proxy n
pt)

instance With P.Rational 'Nothing 'Nothing where
  with :: forall b.
I Rational 'Nothing 'Nothing
-> (forall (t :: T Rational).
    Known Rational 'Nothing 'Nothing t =>
    Proxy t -> b)
-> b
with I Rational 'Nothing 'Nothing
x forall (t :: T Rational).
Known Rational 'Nothing 'Nothing t =>
Proxy t -> b
g = case Rational -> SomeRational
KR.someRationalVal (I Rational 'Nothing 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing 'Nothing
x) of
    KR.SomeRational (Proxy n
pt :: Proxy t) -> Proxy n -> b
forall (t :: T Rational).
Known Rational 'Nothing 'Nothing t =>
Proxy t -> b
g Proxy n
Proxy n
pt

--------------------------------------------------------------------------------

instance
  ( Interval P.Rational ('Just '(il, l)) 'Nothing, 0/1 <= l
  ) => Plus  P.Rational ('Just '(il, l)) 'Nothing where
  I Rational ('Just '(il, l)) 'Nothing
a plus :: I Rational ('Just '(il, l)) 'Nothing
-> I Rational ('Just '(il, l)) 'Nothing
-> I Rational ('Just '(il, l)) 'Nothing
`plus` I Rational ('Just '(il, l)) 'Nothing
b = Rational -> I Rational ('Just '(il, l)) 'Nothing
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (I Rational ('Just '(il, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '(il, l)) 'Nothing
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ I Rational ('Just '(il, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '(il, l)) 'Nothing
b)

instance
  ( Interval P.Rational 'Nothing ('Just '(ir, r)), r <= 0/1
  ) => Plus  P.Rational 'Nothing ('Just '(ir, r)) where
  I Rational 'Nothing ('Just '(ir, r))
a plus :: I Rational 'Nothing ('Just '(ir, r))
-> I Rational 'Nothing ('Just '(ir, r))
-> I Rational 'Nothing ('Just '(ir, r))
`plus` I Rational 'Nothing ('Just '(ir, r))
b = Rational -> I Rational 'Nothing ('Just '(ir, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (I Rational 'Nothing ('Just '(ir, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing ('Just '(ir, r))
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ I Rational 'Nothing ('Just '(ir, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing ('Just '(ir, r))
b)

instance Plus P.Rational 'Nothing 'Nothing where
  I Rational 'Nothing 'Nothing
a plus :: I Rational 'Nothing 'Nothing
-> I Rational 'Nothing 'Nothing -> I Rational 'Nothing 'Nothing
`plus` I Rational 'Nothing 'Nothing
b = Rational -> I Rational 'Nothing 'Nothing
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (I Rational 'Nothing 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing 'Nothing
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ I Rational 'Nothing 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing 'Nothing
b)

--------------------------------------------------------------------------------

instance
  ( Interval P.Rational ('Just '(il, l)) 'Nothing, 1/1 <= l
  ) => Mult  P.Rational ('Just '(il, l)) 'Nothing where
  I Rational ('Just '(il, l)) 'Nothing
a mult :: I Rational ('Just '(il, l)) 'Nothing
-> I Rational ('Just '(il, l)) 'Nothing
-> I Rational ('Just '(il, l)) 'Nothing
`mult` I Rational ('Just '(il, l)) 'Nothing
b = Rational -> I Rational ('Just '(il, l)) 'Nothing
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (I Rational ('Just '(il, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '(il, l)) 'Nothing
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* I Rational ('Just '(il, l)) 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '(il, l)) 'Nothing
b)

instance
  ( Interval P.Rational ('Just '(il, l)) ('Just '(ir, r)), 0/1 <= l, r <= 1/1
  ) => Mult  P.Rational ('Just '(il, l)) ('Just '(ir, r)) where
  I Rational ('Just '(il, l)) ('Just '(ir, r))
a mult :: I Rational ('Just '(il, l)) ('Just '(ir, r))
-> I Rational ('Just '(il, l)) ('Just '(ir, r))
-> I Rational ('Just '(il, l)) ('Just '(ir, r))
`mult` I Rational ('Just '(il, l)) ('Just '(ir, r))
b = Rational -> I Rational ('Just '(il, l)) ('Just '(ir, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (I Rational ('Just '(il, l)) ('Just '(ir, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '(il, l)) ('Just '(ir, r))
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* I Rational ('Just '(il, l)) ('Just '(ir, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '(il, l)) ('Just '(ir, r))
b)

instance Mult P.Rational 'Nothing 'Nothing where
  I Rational 'Nothing 'Nothing
a mult :: I Rational 'Nothing 'Nothing
-> I Rational 'Nothing 'Nothing -> I Rational 'Nothing 'Nothing
`mult` I Rational 'Nothing 'Nothing
b = Rational -> I Rational 'Nothing 'Nothing
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (I Rational 'Nothing 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing 'Nothing
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* I Rational 'Nothing 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing 'Nothing
b)

--------------------------------------------------------------------------------

instance
  ( 0/1 < l, r <= 1/1
  , Interval P.Rational ('Just '(il, l)) ('Just '(ir, r))
  ) => Div   P.Rational ('Just '(il, l)) ('Just '(ir, r)) where
  I Rational ('Just '(il, l)) ('Just '(ir, r))
a div :: I Rational ('Just '(il, l)) ('Just '(ir, r))
-> I Rational ('Just '(il, l)) ('Just '(ir, r))
-> I Rational ('Just '(il, l)) ('Just '(ir, r))
`div` I Rational ('Just '(il, l)) ('Just '(ir, r))
b = Rational -> I Rational ('Just '(il, l)) ('Just '(ir, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (I Rational ('Just '(il, l)) ('Just '(ir, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '(il, l)) ('Just '(ir, r))
a Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ I Rational ('Just '(il, l)) ('Just '(ir, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational ('Just '(il, l)) ('Just '(ir, r))
b)

--------------------------------------------------------------------------------

instance Minus P.Rational 'Nothing 'Nothing where
  I Rational 'Nothing 'Nothing
a minus :: I Rational 'Nothing 'Nothing
-> I Rational 'Nothing 'Nothing -> I Rational 'Nothing 'Nothing
`minus` I Rational 'Nothing 'Nothing
b = Rational -> I Rational 'Nothing 'Nothing
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (I Rational 'Nothing 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing 'Nothing
a Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- I Rational 'Nothing 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Rational 'Nothing 'Nothing
b)

--------------------------------------------------------------------------------

instance
  ( l <= 0/1, 0/1 <= r
  , Interval P.Rational ('Just '( 'True, l)) ('Just '( 'True, r))
  ) => Zero  P.Rational ('Just '( 'True, l)) ('Just '( 'True, r)) where
  zero :: I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
zero = Rational -> I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe Rational
0

instance
  ( l <= 0/1, 0/1 < r
  , Interval P.Rational ('Just '( 'True, l)) ('Just '( 'False, r))
  ) => Zero  P.Rational ('Just '( 'True, l)) ('Just '( 'False, r)) where
  zero :: I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
zero = Rational -> I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe Rational
0

instance
  ( l < 0/1, 0/1 <= r
  , Interval P.Rational ('Just '( 'False, l)) ('Just '( 'True, r))
  ) => Zero  P.Rational ('Just '( 'False, l)) ('Just '( 'True, r)) where
  zero :: I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
zero = Rational -> I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe Rational
0

instance
  ( Interval P.Rational ('Just '( 'True, l)) 'Nothing, l <= 0/1
  ) => Zero  P.Rational ('Just '( 'True, l)) 'Nothing where
  zero :: I Rational ('Just '( 'True, l)) 'Nothing
zero = Rational -> I Rational ('Just '( 'True, l)) 'Nothing
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe Rational
0

instance
  ( Interval P.Rational ('Just '( 'False, l)) 'Nothing, l < 0/1
  ) => Zero P.Rational ('Just '( 'False, l)) 'Nothing where
  zero :: I Rational ('Just '( 'False, l)) 'Nothing
zero = Rational -> I Rational ('Just '( 'False, l)) 'Nothing
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe Rational
0

instance
  ( Interval P.Rational 'Nothing ('Just '( 'True, r)), 0/1 <= r
  ) => Zero  P.Rational 'Nothing ('Just '( 'True, r)) where
  zero :: I Rational 'Nothing ('Just '( 'True, r))
zero = Rational -> I Rational 'Nothing ('Just '( 'True, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe Rational
0

instance
  ( Interval P.Rational 'Nothing ('Just '( 'False, r)), 0/1 < r
  ) => Zero  P.Rational 'Nothing ('Just '( 'False, r)) where
  zero :: I Rational 'Nothing ('Just '( 'False, r))
zero = Rational -> I Rational 'Nothing ('Just '( 'False, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe Rational
0

instance
  ( l < 0/1, 0/1 < r
  , Interval P.Rational ('Just '( 'False, l)) ('Just '( 'False, r))
  ) => Zero  P.Rational ('Just '( 'False, l)) ('Just '( 'False, r)) where
  zero :: I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
zero = Rational -> I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe Rational
0

instance Zero P.Rational 'Nothing 'Nothing where
  zero :: I Rational 'Nothing 'Nothing
zero = Rational -> I Rational 'Nothing 'Nothing
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe Rational
0

--------------------------------------------------------------------------------

instance
  ( l <= 1/1, 1/1 <= r
  , Interval P.Rational ('Just '( 'True, l)) ('Just '( 'True, r))
  ) => One   P.Rational ('Just '( 'True, l)) ('Just '( 'True, r)) where
  one :: I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
one = Rational -> I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe Rational
1

instance
  ( l <= 1/1, 1/1 < r
  , Interval P.Rational ('Just '( 'True, l)) ('Just '( 'False, r))
  ) => One   P.Rational ('Just '( 'True, l)) ('Just '( 'False, r)) where
  one :: I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
one = Rational -> I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe Rational
1

instance
  ( l < 1/1, 1/1 <= r
  , Interval P.Rational ('Just '( 'False, l)) ('Just '( 'True, r))
  ) => One   P.Rational ('Just '( 'False, l)) ('Just '( 'True, r)) where
  one :: I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
one = Rational -> I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe Rational
1

instance
  ( Interval P.Rational ('Just '( 'True, l)) 'Nothing, l <= 1/1
  ) => One   P.Rational ('Just '( 'True, l)) 'Nothing where
  one :: I Rational ('Just '( 'True, l)) 'Nothing
one = Rational -> I Rational ('Just '( 'True, l)) 'Nothing
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe Rational
1

instance
  ( Interval P.Rational ('Just '( 'False, l)) 'Nothing, l < 1/1
  ) => One   P.Rational ('Just '( 'False, l)) 'Nothing where
  one :: I Rational ('Just '( 'False, l)) 'Nothing
one = Rational -> I Rational ('Just '( 'False, l)) 'Nothing
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe Rational
1

instance
  ( Interval P.Rational 'Nothing ('Just '( 'True, r)), 1/1 <= r
  ) => One   P.Rational 'Nothing ('Just '( 'True, r)) where
  one :: I Rational 'Nothing ('Just '( 'True, r))
one = Rational -> I Rational 'Nothing ('Just '( 'True, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe Rational
1

instance
  ( Interval P.Rational 'Nothing ('Just '( 'False, r)), 1/1 < r
  ) => One   P.Rational 'Nothing ('Just '( 'False, r)) where
  one :: I Rational 'Nothing ('Just '( 'False, r))
one = Rational -> I Rational 'Nothing ('Just '( 'False, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe Rational
1

instance
  ( l < 1/1, 1/1 < r
  , Interval P.Rational ('Just '( 'False, l)) ('Just '( 'False, r))
  ) => One   P.Rational ('Just '( 'False, l)) ('Just '( 'False, r)) where
  one :: I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
one = Rational -> I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe Rational
1

instance One P.Rational 'Nothing 'Nothing where
  one :: I Rational 'Nothing 'Nothing
one = Rational -> I Rational 'Nothing 'Nothing
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe Rational
1

--------------------------------------------------------------------------------

instance
  ( l KR.== KR.Negate r
  , Zero      P.Rational ('Just '(i, l)) ('Just '(i, r))
  ) => Negate P.Rational ('Just '(i, l)) ('Just '(i, r)) where
  negate :: I Rational ('Just '(i, l)) ('Just '(i, r))
-> I Rational ('Just '(i, l)) ('Just '(i, r))
negate = Rational -> I Rational ('Just '(i, l)) ('Just '(i, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Rational -> I Rational ('Just '(i, l)) ('Just '(i, r)))
-> (I Rational ('Just '(i, l)) ('Just '(i, r)) -> Rational)
-> I Rational ('Just '(i, l)) ('Just '(i, r))
-> I Rational ('Just '(i, l)) ('Just '(i, r))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Rational
forall a. Num a => a -> a
P.negate (Rational -> Rational)
-> (I Rational ('Just '(i, l)) ('Just '(i, r)) -> Rational)
-> I Rational ('Just '(i, l)) ('Just '(i, r))
-> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I Rational ('Just '(i, l)) ('Just '(i, r)) -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap

instance Negate P.Rational 'Nothing 'Nothing where
  negate :: I Rational 'Nothing 'Nothing -> I Rational 'Nothing 'Nothing
negate = Rational -> I Rational 'Nothing 'Nothing
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Rational -> I Rational 'Nothing 'Nothing)
-> (I Rational 'Nothing 'Nothing -> Rational)
-> I Rational 'Nothing 'Nothing
-> I Rational 'Nothing 'Nothing
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Rational
forall a. Num a => a -> a
P.negate (Rational -> Rational)
-> (I Rational 'Nothing 'Nothing -> Rational)
-> I Rational 'Nothing 'Nothing
-> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I Rational 'Nothing 'Nothing -> Rational
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap

--------------------------------------------------------------------------------

instance
  ( Interval Rational ('Just '( 'True, l)) ('Just '( 'True, r))
  ) => Shove Rational ('Just '( 'True, l)) ('Just '( 'True, r)) where
  shove :: Rational -> I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
shove | Rational
d Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
0    = \Rational
_ -> I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
forall x (l :: L x) (r :: R x). Known x l r (MinI x l r) => I x l r
min
        | Bool
otherwise = \Rational
x ->
          let t :: Rational
t = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
P.min (Integer -> Integer
forall a. Num a => a -> a
abs (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
x)) (Integer -> Integer
forall a. Num a => a -> a
abs (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
x))
                Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
P.max (Integer -> Integer
forall a. Num a => a -> a
abs (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
x)) (Integer -> Integer
forall a. Num a => a -> a
abs (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
x))
          in Rational -> I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Rational -> I Rational ('Just '( 'True, l)) ('Just '( 'True, r)))
-> Rational -> I Rational ('Just '( 'True, l)) ('Just '( 'True, r))
forall a b. (a -> b) -> a -> b
$ if Rational
x Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
< Rational
0 then Rational
r Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
d Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Rational
t else Rational
l Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ Rational
d Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Rational
t
    where
      l :: Rational
l = Proxy l -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @l)
      r :: Rational
r = Proxy r -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @r)
      d :: Rational
d = Rational
r Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
l

instance
  ( Interval Rational ('Just '( 'True, l)) ('Just '( 'False, r))
  ) => Shove Rational ('Just '( 'True, l)) ('Just '( 'False, r)) where
  shove :: Rational -> I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
shove = \Rational
x -> let t :: Rational
t = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
P.min (Integer -> Integer
forall a. Num a => a -> a
abs (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
x)) (Integer -> Integer
forall a. Num a => a -> a
abs (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
x))
                      Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
P.max (Integer -> Integer
forall a. Num a => a -> a
abs (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
x)) (Integer -> Integer
forall a. Num a => a -> a
abs (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
x))
                in Rational -> I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Rational -> I Rational ('Just '( 'True, l)) ('Just '( 'False, r)))
-> Rational
-> I Rational ('Just '( 'True, l)) ('Just '( 'False, r))
forall a b. (a -> b) -> a -> b
$ if Rational
x Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
< Rational
0 then Rational
r1 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
d1 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Rational
t else Rational
l0 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ Rational
d1 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Rational
t
    where
      l0 :: Rational
l0 = Proxy l -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @l)
      r0 :: Rational
r0 = Proxy r -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @r)
      d0 :: Rational
d0 = Rational
r0 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
l0
      p0 :: Rational
p0 = Rational
d0 Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ Rational
1000
      r1 :: Rational
r1 = Rational
r0 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
p0
      d1 :: Rational
d1 = Rational
r1 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
l0

instance Interval Rational ('Just '( 'True, l)) 'Nothing
  => Shove Rational ('Just '( 'True, l)) 'Nothing where
  shove :: Rational -> I Rational ('Just '( 'True, l)) 'Nothing
shove = \Rational
x -> Rational -> I Rational ('Just '( 'True, l)) 'Nothing
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (if Rational
l Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
<= Rational
x then Rational
x else Rational
l Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ (Rational
l Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
x))
    where l :: Rational
l = Proxy l -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @l)

instance
  ( Interval Rational ('Just '( 'False, l)) ('Just '( 'True, r))
  ) => Shove Rational ('Just '( 'False, l)) ('Just '( 'True, r)) where
  shove :: Rational -> I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
shove = \Rational
x -> let t :: Rational
t = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
P.min (Integer -> Integer
forall a. Num a => a -> a
abs (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
x)) (Integer -> Integer
forall a. Num a => a -> a
abs (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
x))
                      Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
P.max (Integer -> Integer
forall a. Num a => a -> a
abs (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
x)) (Integer -> Integer
forall a. Num a => a -> a
abs (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
x))
                in Rational -> I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Rational -> I Rational ('Just '( 'False, l)) ('Just '( 'True, r)))
-> Rational
-> I Rational ('Just '( 'False, l)) ('Just '( 'True, r))
forall a b. (a -> b) -> a -> b
$ if Rational
x Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
< Rational
0 then Rational
r0 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
d1 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Rational
t else Rational
l1 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ Rational
d1 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Rational
t
    where
      l0 :: Rational
l0 = Proxy l -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @l)
      r0 :: Rational
r0 = Proxy r -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @r)
      d0 :: Rational
d0 = Rational
r0 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
l0
      p0 :: Rational
p0 = Rational
d0 Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ Rational
1000
      l1 :: Rational
l1 = Rational
l0 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ Rational
p0
      d1 :: Rational
d1 = Rational
r0 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
l1

instance
  ( Interval Rational ('Just '( 'False, l)) ('Just '( 'False, r))
  ) => Shove Rational ('Just '( 'False, l)) ('Just '( 'False, r)) where
  shove :: Rational -> I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
shove = \Rational
x -> let t :: Rational
t = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
P.min (Integer -> Integer
forall a. Num a => a -> a
abs (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
x)) (Integer -> Integer
forall a. Num a => a -> a
abs (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
x))
                      Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
P.max (Integer -> Integer
forall a. Num a => a -> a
abs (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
x)) (Integer -> Integer
forall a. Num a => a -> a
abs (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
x))
                in Rational -> I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Rational
 -> I Rational ('Just '( 'False, l)) ('Just '( 'False, r)))
-> Rational
-> I Rational ('Just '( 'False, l)) ('Just '( 'False, r))
forall a b. (a -> b) -> a -> b
$ if Rational
x Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
<= Rational
0 then Rational
r1 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
d1 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Rational
t else Rational
l1 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ Rational
d1 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Rational
t
    where
      l0 :: Rational
l0 = Proxy l -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @l)
      r0 :: Rational
r0 = Proxy r -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @r)
      d0 :: Rational
d0 = Rational
r0 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
l0
      p0 :: Rational
p0 = Rational
d0 Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ Rational
1000
      l1 :: Rational
l1 = Rational
l0 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ Rational
p0
      r1 :: Rational
r1 = Rational
r0 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
p0
      d1 :: Rational
d1 = Rational
r1 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
l1

instance
  ( Interval Rational ('Just '( 'False, l)) 'Nothing
  ) => Shove Rational ('Just '( 'False, l)) 'Nothing where
  shove :: Rational -> I Rational ('Just '( 'False, l)) 'Nothing
shove = \Rational
x -> Rational -> I Rational ('Just '( 'False, l)) 'Nothing
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Rational -> I Rational ('Just '( 'False, l)) 'Nothing)
-> Rational -> I Rational ('Just '( 'False, l)) 'Nothing
forall a b. (a -> b) -> a -> b
$ if Rational
x Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
<= Rational
l then Rational
l Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ (Rational
l Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
x) Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ Rational
1 else Rational
x
    where l :: Rational
l = Proxy l -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @l)

instance
  ( Interval Rational 'Nothing ('Just '( 'True, r))
  ) => Shove Rational 'Nothing ('Just '( 'True, r)) where
  shove :: Rational -> I Rational 'Nothing ('Just '( 'True, r))
shove = \Rational
x -> Rational -> I Rational 'Nothing ('Just '( 'True, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Rational -> I Rational 'Nothing ('Just '( 'True, r)))
-> Rational -> I Rational 'Nothing ('Just '( 'True, r))
forall a b. (a -> b) -> a -> b
$ if Rational
r Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
< Rational
x then Rational
r Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- (Rational
x Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
r) else Rational
x
    where r :: Rational
r = Proxy r -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @r)

instance
  ( Interval Rational 'Nothing ('Just '( 'False, r))
  ) => Shove Rational 'Nothing ('Just '( 'False, r)) where
  shove :: Rational -> I Rational 'Nothing ('Just '( 'False, r))
shove = \Rational
x -> Rational -> I Rational 'Nothing ('Just '( 'False, r))
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Rational -> I Rational 'Nothing ('Just '( 'False, r)))
-> Rational -> I Rational 'Nothing ('Just '( 'False, r))
forall a b. (a -> b) -> a -> b
$ if Rational
r Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
<= Rational
x then Rational
r Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- (Rational
x Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
r) Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
1 else Rational
x
    where r :: Rational
r = Proxy r -> Rational
forall (r :: Rational) (proxy :: Rational -> *).
KnownRational r =>
proxy r -> Rational
KR.rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @r)

instance Shove Rational 'Nothing 'Nothing where
  shove :: Rational -> I Rational 'Nothing 'Nothing
shove = Rational -> I Rational 'Nothing 'Nothing
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe

--------------------------------------------------------------------------------

lt :: forall (a :: KR.Rational) (b :: KR.Rational)
   .  (KR.KnownRational a, KR.KnownRational b)
   => Maybe (Dict (a < b))
lt :: forall (a :: Rational) (b :: Rational).
(KnownRational a, KnownRational b) =>
Maybe (Dict (a < b))
lt = case Proxy a -> Proxy b -> OrderingI a b
forall (a :: Rational) (b :: Rational) (proxy1 :: Rational -> *)
       (proxy2 :: Rational -> *).
(KnownRational a, KnownRational b) =>
proxy1 a -> proxy2 b -> OrderingI a b
KR.cmpRational (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @a) (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @b) of
  OrderingI a b
L.LTI -> Dict (a < b) -> Maybe (Dict (a < b))
forall a. a -> Maybe a
Just (Dict (a < b) -> Maybe (Dict (a < b)))
-> Dict (a < b) -> Maybe (Dict (a < b))
forall a b. (a -> b) -> a -> b
$ Dict (() :: Constraint) -> Dict (() :: Constraint)
forall a b. a -> b
unsafeCoerce (forall (a :: Constraint). a => Dict a
Dict @())
  OrderingI a b
L.EQI -> Maybe (Dict (TypeError ...))
Maybe (Dict (a < b))
forall a. Maybe a
Nothing
  OrderingI a b
L.GTI -> Maybe (Dict (TypeError ...))
Maybe (Dict (a < b))
forall a. Maybe a
Nothing

le :: forall (a :: KR.Rational) (b :: KR.Rational)
   .  (KR.KnownRational a, KR.KnownRational b)
   => Maybe (Dict (a <= b))
le :: forall (a :: Rational) (b :: Rational).
(KnownRational a, KnownRational b) =>
Maybe (Dict (a <= b))
le = case Proxy a -> Proxy b -> OrderingI a b
forall (a :: Rational) (b :: Rational) (proxy1 :: Rational -> *)
       (proxy2 :: Rational -> *).
(KnownRational a, KnownRational b) =>
proxy1 a -> proxy2 b -> OrderingI a b
KR.cmpRational (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @a) (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @b) of
  OrderingI a b
L.LTI -> Dict (a <= b) -> Maybe (Dict (a <= b))
forall a. a -> Maybe a
Just (Dict (a <= b) -> Maybe (Dict (a <= b)))
-> Dict (a <= b) -> Maybe (Dict (a <= b))
forall a b. (a -> b) -> a -> b
$ Dict (() :: Constraint) -> Dict (() :: Constraint)
forall a b. a -> b
unsafeCoerce (forall (a :: Constraint). a => Dict a
Dict @())
  OrderingI a b
L.EQI -> Dict (a <= b) -> Maybe (Dict (a <= b))
forall a. a -> Maybe a
Just (Dict (a <= b) -> Maybe (Dict (a <= b)))
-> Dict (a <= b) -> Maybe (Dict (a <= b))
forall a b. (a -> b) -> a -> b
$ Dict (() :: Constraint) -> Dict (() :: Constraint)
forall a b. a -> b
unsafeCoerce (forall (a :: Constraint). a => Dict a
Dict @())
  OrderingI a b
L.GTI -> Maybe (Dict (TypeError ...))
Maybe (Dict (a <= b))
forall a. Maybe a
Nothing