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

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

module I.Natural () where

import Control.Monad
import Data.Bits
import Data.Constraint
import Data.Maybe
import Data.Proxy
import Data.Type.Ord
import Numeric.Natural (Natural)
import GHC.TypeNats qualified as N
import KindInteger (type (/=))
import Prelude hiding (min, max, div, succ)

import I.Internal

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

type instance MinL Natural = MinT Natural
type instance MaxR Natural = 'Nothing

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

instance forall l r.
  ( IntervalCtx    Natural l ('Just r)
  ) => Interval    Natural l ('Just r) where
  type IntervalCtx Natural l ('Just r) =
    ( N.KnownNat l
    , N.KnownNat r
    , MinT Natural <= l
    , l <= r )
  type MinI Natural l ('Just r) = l
  type MaxI Natural l ('Just r) = r
  inhabitant :: I Natural l ('Just r)
inhabitant = I Natural l ('Just r)
forall x (l :: L x) (r :: R x). Known x l r (MinI x l r) => I x l r
min
  from :: Natural -> Maybe (I Natural l ('Just r))
from = \Natural
x -> Natural -> I Natural l ('Just r)
forall x (l :: L x) (r :: R x). x -> I x l r
unsafest Natural
x I Natural l ('Just r) -> Maybe () -> Maybe (I Natural l ('Just 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 (Natural
l Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= Natural
x Bool -> Bool -> Bool
&& Natural
x Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= Natural
r)
    where l :: Natural
l = Proxy l -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
N.natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l)
          r :: Natural
r = Proxy r -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
N.natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r)
  I Natural l ('Just r)
a plus' :: I Natural l ('Just r)
-> I Natural l ('Just r) -> Maybe (I Natural l ('Just r))
`plus'` I Natural l ('Just r)
b = Natural -> Maybe (I Natural l ('Just r))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Natural l ('Just r) -> Natural
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Natural l ('Just r)
a Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ I Natural l ('Just r) -> Natural
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Natural l ('Just r)
b)
  I Natural l ('Just r)
a mult' :: I Natural l ('Just r)
-> I Natural l ('Just r) -> Maybe (I Natural l ('Just r))
`mult'` I Natural l ('Just r)
b = Natural -> Maybe (I Natural l ('Just r))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Natural l ('Just r) -> Natural
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Natural l ('Just r)
a Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* I Natural l ('Just r) -> Natural
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Natural l ('Just r)
b)
  I Natural l ('Just r)
a minus' :: I Natural l ('Just r)
-> I Natural l ('Just r) -> Maybe (I Natural l ('Just r))
`minus'` I Natural l ('Just r)
b = Natural -> Maybe (I Natural l ('Just r))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (Natural -> Maybe (I Natural l ('Just r)))
-> Maybe Natural -> Maybe (I Natural l ('Just r))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Integer -> Maybe Natural
forall a b.
(Integral a, Integral b, Bits a, Bits b) =>
a -> Maybe b
toIntegralSized (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger (I Natural l ('Just r) -> Natural
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Natural l ('Just r)
a) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-
                                           Natural -> Integer
forall a. Integral a => a -> Integer
toInteger (I Natural l ('Just r) -> Natural
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Natural l ('Just r)
b))
  I Natural l ('Just r)
a div' :: I Natural l ('Just r)
-> I Natural l ('Just r) -> Maybe (I Natural l ('Just r))
`div'` I Natural l ('Just r)
b = do Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (I Natural l ('Just r) -> Natural
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Natural l ('Just r)
b Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
/= Natural
0)
                  (Natural
q, Natural
0) <- (Natural, Natural) -> Maybe (Natural, Natural)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Natural, Natural) -> Maybe (Natural, Natural))
-> (Natural, Natural) -> Maybe (Natural, Natural)
forall a b. (a -> b) -> a -> b
$ Natural -> Natural -> (Natural, Natural)
forall a. Integral a => a -> a -> (a, a)
divMod (I Natural l ('Just r) -> Natural
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Natural l ('Just r)
a) (I Natural l ('Just r) -> Natural
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Natural l ('Just r)
b)
                  Natural -> Maybe (I Natural l ('Just r))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from Natural
q

instance forall l.
  ( IntervalCtx    Natural l 'Nothing
  ) => Interval    Natural l 'Nothing where
  type IntervalCtx Natural l 'Nothing = (N.KnownNat l, MinT Natural <= l)
  type MinI Natural l 'Nothing = l
  inhabitant :: I Natural l 'Nothing
inhabitant = I Natural l 'Nothing
forall x (l :: L x) (r :: R x). Known x l r (MinI x l r) => I x l r
min
  from :: Natural -> Maybe (I Natural l 'Nothing)
from = \Natural
x -> Natural -> I Natural l 'Nothing
forall x (l :: L x) (r :: R x). x -> I x l r
unsafest Natural
x I Natural l 'Nothing -> Maybe () -> Maybe (I Natural 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 (Natural
l Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= Natural
x)
    where l :: Natural
l = Proxy l -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
N.natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l)
  I Natural l 'Nothing
a plus' :: I Natural l 'Nothing
-> I Natural l 'Nothing -> Maybe (I Natural l 'Nothing)
`plus'` I Natural l 'Nothing
b = I Natural l 'Nothing -> Maybe (I Natural l 'Nothing)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (I Natural l 'Nothing
a I Natural l 'Nothing
-> I Natural l 'Nothing -> I Natural l '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 Natural l 'Nothing
b)
  I Natural l 'Nothing
a mult' :: I Natural l 'Nothing
-> I Natural l 'Nothing -> Maybe (I Natural l 'Nothing)
`mult'` I Natural l 'Nothing
b = I Natural l 'Nothing -> Maybe (I Natural l 'Nothing)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (I Natural l 'Nothing
a I Natural l 'Nothing
-> I Natural l 'Nothing -> I Natural l '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 Natural l 'Nothing
b)
  I Natural l 'Nothing
a minus' :: I Natural l 'Nothing
-> I Natural l 'Nothing -> Maybe (I Natural l 'Nothing)
`minus'` I Natural l 'Nothing
b = Natural -> Maybe (I Natural l 'Nothing)
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (Natural -> Maybe (I Natural l 'Nothing))
-> Maybe Natural -> Maybe (I Natural l 'Nothing)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Integer -> Maybe Natural
forall a b.
(Integral a, Integral b, Bits a, Bits b) =>
a -> Maybe b
toIntegralSized (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger (I Natural l 'Nothing -> Natural
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Natural l 'Nothing
a) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-
                                           Natural -> Integer
forall a. Integral a => a -> Integer
toInteger (I Natural l 'Nothing -> Natural
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Natural l 'Nothing
b))
  I Natural l 'Nothing
a div' :: I Natural l 'Nothing
-> I Natural l 'Nothing -> Maybe (I Natural l 'Nothing)
`div'` I Natural l 'Nothing
b = do Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (I Natural l 'Nothing -> Natural
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Natural l 'Nothing
b Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
/= Natural
0)
                  (Natural
q, Natural
0) <- (Natural, Natural) -> Maybe (Natural, Natural)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Natural, Natural) -> Maybe (Natural, Natural))
-> (Natural, Natural) -> Maybe (Natural, Natural)
forall a b. (a -> b) -> a -> b
$ Natural -> Natural -> (Natural, Natural)
forall a. Integral a => a -> a -> (a, a)
divMod (I Natural l 'Nothing -> Natural
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Natural l 'Nothing
a) (I Natural l 'Nothing -> Natural
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Natural l 'Nothing
b)
                  Natural -> Maybe (I Natural l 'Nothing)
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from Natural
q

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

instance
  ( Interval Natural l ('Just r)
  ) => Clamp Natural l ('Just r)

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

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

instance
  ( lu <= ld, rd <= ru
  , Interval Natural ld ('Just rd)
  , Interval Natural               lu ('Just ru) )
  => Up      Natural ld ('Just rd) lu ('Just ru)

instance
  ( lu <= ld
  , Interval Natural ld yrd
  , Interval Natural        lu 'Nothing
  ) => Up    Natural ld yrd lu 'Nothing

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

instance forall l r t.
  ( Interval    Natural l ('Just r)
  , KnownCtx    Natural l ('Just r) t
  ) => Known    Natural l ('Just r) t where
  type KnownCtx Natural l ('Just r) t = (N.KnownNat t, l <= t, t <= r)
  known' :: Proxy t -> I Natural l ('Just r)
known' = Natural -> I Natural l ('Just r)
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Natural -> I Natural l ('Just r))
-> (Proxy t -> Natural) -> Proxy t -> I Natural l ('Just r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy t -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
N.natVal

instance forall t l.
  ( Interval    Natural l 'Nothing
  , KnownCtx    Natural l 'Nothing t
  ) => Known    Natural l 'Nothing t where
  type KnownCtx Natural l 'Nothing t = (N.KnownNat t, l <= t)
  known' :: Proxy t -> I Natural l 'Nothing
known' = Natural -> I Natural l 'Nothing
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Natural -> I Natural l 'Nothing)
-> (Proxy t -> Natural) -> Proxy t -> I Natural l 'Nothing
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy t -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
N.natVal

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

instance forall l r.
  ( Interval Natural l ('Just r)
  ) => With  Natural l ('Just r) where
  with :: forall b.
I Natural l ('Just r)
-> (forall (t :: T Natural).
    Known Natural l ('Just r) t =>
    Proxy t -> b)
-> b
with I Natural l ('Just r)
x forall (t :: T Natural).
Known Natural l ('Just r) t =>
Proxy t -> b
g = case Natural -> SomeNat
N.someNatVal (I Natural l ('Just r) -> Natural
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Natural l ('Just r)
x) of
    N.SomeNat (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(Natural): impossible") (Maybe b -> b) -> Maybe b -> b
forall a b. (a -> b) -> a -> b
$ do
        Dict
  (Assert (OrdCond (CmpNat l n) 'True 'True 'False) (TypeError ...))
Dict <- forall (a :: Natural) (b :: Natural).
(KnownNat a, KnownNat b) =>
Maybe (Dict (a <= b))
leNatural @l @t
        Dict
  (Assert (OrdCond (CmpNat n r) 'True 'True 'False) (TypeError ...))
Dict <- forall (a :: Natural) (b :: Natural).
(KnownNat a, KnownNat b) =>
Maybe (Dict (a <= b))
leNatural @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 Natural).
Known Natural l ('Just r) t =>
Proxy t -> b
g Proxy n
Proxy n
pt)

instance forall l.
  ( Interval Natural l 'Nothing
  ) => With  Natural l 'Nothing where
  with :: forall b.
I Natural l 'Nothing
-> (forall (t :: T Natural).
    Known Natural l 'Nothing t =>
    Proxy t -> b)
-> b
with I Natural l 'Nothing
x forall (t :: T Natural). Known Natural l 'Nothing t => Proxy t -> b
g = case Natural -> SomeNat
N.someNatVal (I Natural l 'Nothing -> Natural
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Natural l 'Nothing
x) of
    N.SomeNat (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(Natural): impossible") (Maybe b -> b) -> Maybe b -> b
forall a b. (a -> b) -> a -> b
$ do
        Dict
  (Assert (OrdCond (CmpNat l n) 'True 'True 'False) (TypeError ...))
Dict <- forall (a :: Natural) (b :: Natural).
(KnownNat a, KnownNat b) =>
Maybe (Dict (a <= b))
leNatural @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 Natural). Known Natural l 'Nothing t => Proxy t -> b
g Proxy n
Proxy n
pt)

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

instance
  ( Interval    Natural l ('Just r), l /= r
  ) => Discrete Natural l ('Just r) where
  pred' :: I Natural l ('Just r) -> Maybe (I Natural l ('Just r))
pred' I Natural l ('Just r)
i = Natural -> I Natural l ('Just r)
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (I Natural l ('Just r) -> Natural
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Natural l ('Just r)
i Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1) I Natural l ('Just r) -> Maybe () -> Maybe (I Natural l ('Just 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 (I Natural l ('Just r)
forall x (l :: L x) (r :: R x). Known x l r (MinI x l r) => I x l r
min I Natural l ('Just r) -> I Natural l ('Just r) -> Bool
forall a. Ord a => a -> a -> Bool
< I Natural l ('Just r)
i)
  succ' :: I Natural l ('Just r) -> Maybe (I Natural l ('Just r))
succ' I Natural l ('Just r)
i = Natural -> I Natural l ('Just r)
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (I Natural l ('Just r) -> Natural
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Natural l ('Just r)
i Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
1) I Natural l ('Just r) -> Maybe () -> Maybe (I Natural l ('Just 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 (I Natural l ('Just r)
i I Natural l ('Just r) -> I Natural l ('Just r) -> Bool
forall a. Ord a => a -> a -> Bool
< I Natural l ('Just r)
forall x (l :: L x) (r :: R x). Known x l r (MaxI x l r) => I x l r
max)

instance
  ( Interval    Natural l 'Nothing
  ) => Discrete Natural l 'Nothing where
  pred' :: I Natural l 'Nothing -> Maybe (I Natural l 'Nothing)
pred' I Natural l 'Nothing
i = Natural -> I Natural l 'Nothing
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (I Natural l 'Nothing -> Natural
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Natural l 'Nothing
i Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1) I Natural l 'Nothing -> Maybe () -> Maybe (I Natural 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 (I Natural l 'Nothing
forall x (l :: L x) (r :: R x). Known x l r (MinI x l r) => I x l r
min I Natural l 'Nothing -> I Natural l 'Nothing -> Bool
forall a. Ord a => a -> a -> Bool
< I Natural l 'Nothing
i)
  succ' :: I Natural l 'Nothing -> Maybe (I Natural l 'Nothing)
succ' = I Natural l 'Nothing -> Maybe (I Natural l 'Nothing)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (I Natural l 'Nothing -> Maybe (I Natural l 'Nothing))
-> (I Natural l 'Nothing -> I Natural l 'Nothing)
-> I Natural l 'Nothing
-> Maybe (I Natural l 'Nothing)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I Natural l 'Nothing -> I Natural l 'Nothing
forall x (l :: L x) (r :: R x). Succ x l r => I x l r -> I x l r
succ

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

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

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

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

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

instance
  ( Discrete Natural l 'Nothing
  ) => Succ  Natural l 'Nothing where
  succ :: I Natural l 'Nothing -> I Natural l 'Nothing
succ I Natural l 'Nothing
i = Natural -> I Natural l 'Nothing
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (I Natural l 'Nothing -> Natural
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Natural l 'Nothing
i Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
1)

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

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

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

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

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

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

instance
  ( Interval Natural l ('Just r)
  ) => Shove Natural l ('Just r) where
  shove :: Natural -> I Natural l ('Just r)
shove = \Natural
x -> Natural -> I Natural l ('Just r)
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Natural -> I Natural l ('Just r))
-> Natural -> I Natural l ('Just r)
forall a b. (a -> b) -> a -> b
$ Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
mod Natural
x (Natural
r Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
l Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
1) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
l
    where l :: Natural
l = I Natural l ('Just r) -> Natural
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap (forall x (l :: L x) (r :: R x). Known x l r (MinI x l r) => I x l r
min @Natural @l @('Just r))
          r :: Natural
r = I Natural l ('Just r) -> Natural
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap (forall x (l :: L x) (r :: R x). Known x l r (MaxI x l r) => I x l r
max @Natural @l @('Just r))

instance
  ( Interval Natural l 'Nothing
  ) => Shove Natural l 'Nothing where
  shove :: Natural -> I Natural l 'Nothing
shove = \Natural
x -> Natural -> I Natural l 'Nothing
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Natural -> I Natural l 'Nothing)
-> Natural -> I Natural l 'Nothing
forall a b. (a -> b) -> a -> b
$ if Natural
x Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< Natural
l then Natural
l Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ (Natural
l Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
x) else Natural
x
    where l :: Natural
l = I Natural l 'Nothing -> Natural
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap (forall x (l :: L x) (r :: R x). Known x l r (MinI x l r) => I x l r
min @Natural @l @'Nothing)