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

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

module I.Integer () where

import Control.Monad
import Data.Constraint
import Data.Maybe
import Data.Proxy
import Data.Type.Ord
import KindInteger qualified as K
import KindInteger (type (/=))
import Prelude hiding (min, max, div, succ, pred)
import Prelude qualified as P

import I.Internal

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

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

instance forall l r.
  ( IntervalCtx    P.Integer ('Just l) ('Just r)
  ) => Interval    P.Integer ('Just l) ('Just r) where
  type IntervalCtx P.Integer ('Just l) ('Just r) =
    (K.KnownInteger l, K.KnownInteger r, l <= r)
  type MinI P.Integer ('Just l) ('Just r) = l
  type MaxI P.Integer ('Just l) ('Just r) = r
  inhabitant :: I Integer ('Just l) ('Just r)
inhabitant = I Integer ('Just 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 :: Integer -> Maybe (I Integer ('Just l) ('Just r))
from = \Integer
x -> Integer -> I Integer ('Just l) ('Just r)
forall x (l :: L x) (r :: R x). x -> I x l r
unsafest Integer
x I Integer ('Just l) ('Just r)
-> Maybe () -> Maybe (I Integer ('Just 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 (Integer
l Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
x Bool -> Bool -> Bool
&& Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
r)
    where l :: Integer
l = Proxy l -> Integer
forall (i :: Integer) (proxy :: Integer -> *).
KnownInteger i =>
proxy i -> Integer
K.integerVal (forall {k} (t :: k). Proxy t
forall (t :: Integer). Proxy t
Proxy @l)
          r :: Integer
r = Proxy r -> Integer
forall (i :: Integer) (proxy :: Integer -> *).
KnownInteger i =>
proxy i -> Integer
K.integerVal (forall {k} (t :: k). Proxy t
forall (t :: Integer). Proxy t
Proxy @r)
  negate' :: I Integer ('Just l) ('Just r)
-> Maybe (I Integer ('Just l) ('Just r))
negate' = Integer -> Maybe (I Integer ('Just l) ('Just r))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (Integer -> Maybe (I Integer ('Just l) ('Just r)))
-> (I Integer ('Just l) ('Just r) -> Integer)
-> I Integer ('Just l) ('Just r)
-> Maybe (I Integer ('Just l) ('Just r))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
forall a. Num a => a -> a
P.negate (Integer -> Integer)
-> (I Integer ('Just l) ('Just r) -> Integer)
-> I Integer ('Just l) ('Just r)
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I Integer ('Just l) ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap
  I Integer ('Just l) ('Just r)
a plus' :: I Integer ('Just l) ('Just r)
-> I Integer ('Just l) ('Just r)
-> Maybe (I Integer ('Just l) ('Just r))
`plus'` I Integer ('Just l) ('Just r)
b = Integer -> Maybe (I Integer ('Just l) ('Just r))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Integer ('Just l) ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) ('Just r)
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ I Integer ('Just l) ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) ('Just r)
b)
  I Integer ('Just l) ('Just r)
a mult' :: I Integer ('Just l) ('Just r)
-> I Integer ('Just l) ('Just r)
-> Maybe (I Integer ('Just l) ('Just r))
`mult'` I Integer ('Just l) ('Just r)
b = Integer -> Maybe (I Integer ('Just l) ('Just r))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Integer ('Just l) ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) ('Just r)
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* I Integer ('Just l) ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) ('Just r)
b)
  I Integer ('Just l) ('Just r)
a minus' :: I Integer ('Just l) ('Just r)
-> I Integer ('Just l) ('Just r)
-> Maybe (I Integer ('Just l) ('Just r))
`minus'` I Integer ('Just l) ('Just r)
b = Integer -> Maybe (I Integer ('Just l) ('Just r))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Integer ('Just l) ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) ('Just r)
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- I Integer ('Just l) ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) ('Just r)
b)
  I Integer ('Just l) ('Just r)
a div' :: I Integer ('Just l) ('Just r)
-> I Integer ('Just l) ('Just r)
-> Maybe (I Integer ('Just l) ('Just r))
`div'` I Integer ('Just l) ('Just r)
b = do Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (I Integer ('Just l) ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) ('Just r)
b Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0)
                  let (Integer
q, Integer
m) = Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod (I Integer ('Just l) ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) ('Just r)
a) (I Integer ('Just l) ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) ('Just r)
b)
                  Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0)
                  Integer -> Maybe (I Integer ('Just l) ('Just r))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from Integer
q

instance forall l.
  ( IntervalCtx    P.Integer ('Just l) 'Nothing
  ) => Interval    P.Integer ('Just l) 'Nothing where
  type IntervalCtx P.Integer ('Just l) 'Nothing = K.KnownInteger l
  type MinI P.Integer ('Just l) 'Nothing = l
  inhabitant :: I Integer ('Just l) 'Nothing
inhabitant = I Integer ('Just l) 'Nothing
forall x (l :: L x) (r :: R x). Known x l r (MinI x l r) => I x l r
min
  from :: Integer -> Maybe (I Integer ('Just l) 'Nothing)
from = \Integer
x -> Integer -> I Integer ('Just l) 'Nothing
forall x (l :: L x) (r :: R x). x -> I x l r
unsafest Integer
x I Integer ('Just l) 'Nothing
-> Maybe () -> Maybe (I Integer ('Just 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 (Integer
l Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
x)
    where l :: Integer
l = Proxy l -> Integer
forall (i :: Integer) (proxy :: Integer -> *).
KnownInteger i =>
proxy i -> Integer
K.integerVal (forall {k} (t :: k). Proxy t
forall (t :: Integer). Proxy t
Proxy @l)
  negate' :: I Integer ('Just l) 'Nothing
-> Maybe (I Integer ('Just l) 'Nothing)
negate' = Integer -> Maybe (I Integer ('Just l) 'Nothing)
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (Integer -> Maybe (I Integer ('Just l) 'Nothing))
-> (I Integer ('Just l) 'Nothing -> Integer)
-> I Integer ('Just l) 'Nothing
-> Maybe (I Integer ('Just l) 'Nothing)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
forall a. Num a => a -> a
P.negate (Integer -> Integer)
-> (I Integer ('Just l) 'Nothing -> Integer)
-> I Integer ('Just l) 'Nothing
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I Integer ('Just l) 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap
  I Integer ('Just l) 'Nothing
a plus' :: I Integer ('Just l) 'Nothing
-> I Integer ('Just l) 'Nothing
-> Maybe (I Integer ('Just l) 'Nothing)
`plus'` I Integer ('Just l) 'Nothing
b = Integer -> Maybe (I Integer ('Just l) 'Nothing)
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Integer ('Just l) 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) 'Nothing
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ I Integer ('Just l) 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) 'Nothing
b)
  I Integer ('Just l) 'Nothing
a mult' :: I Integer ('Just l) 'Nothing
-> I Integer ('Just l) 'Nothing
-> Maybe (I Integer ('Just l) 'Nothing)
`mult'` I Integer ('Just l) 'Nothing
b = Integer -> Maybe (I Integer ('Just l) 'Nothing)
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Integer ('Just l) 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) 'Nothing
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* I Integer ('Just l) 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) 'Nothing
b)
  I Integer ('Just l) 'Nothing
a minus' :: I Integer ('Just l) 'Nothing
-> I Integer ('Just l) 'Nothing
-> Maybe (I Integer ('Just l) 'Nothing)
`minus'` I Integer ('Just l) 'Nothing
b = Integer -> Maybe (I Integer ('Just l) 'Nothing)
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Integer ('Just l) 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) 'Nothing
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- I Integer ('Just l) 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) 'Nothing
b)
  I Integer ('Just l) 'Nothing
a div' :: I Integer ('Just l) 'Nothing
-> I Integer ('Just l) 'Nothing
-> Maybe (I Integer ('Just l) 'Nothing)
`div'` I Integer ('Just l) 'Nothing
b = do Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (I Integer ('Just l) 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) 'Nothing
b Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0)
                  let (Integer
q, Integer
m) = Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod (I Integer ('Just l) 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) 'Nothing
a) (I Integer ('Just l) 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) 'Nothing
b)
                  Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0)
                  Integer -> Maybe (I Integer ('Just l) 'Nothing)
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from Integer
q

instance forall r.
  ( IntervalCtx    P.Integer 'Nothing ('Just r)
  ) => Interval    P.Integer 'Nothing ('Just r) where
  type IntervalCtx P.Integer 'Nothing ('Just r) = K.KnownInteger r
  type MaxI P.Integer 'Nothing ('Just r) = r
  inhabitant :: I Integer 'Nothing ('Just r)
inhabitant = I Integer 'Nothing ('Just r)
forall x (l :: L x) (r :: R x). Known x l r (MaxI x l r) => I x l r
max
  from :: Integer -> Maybe (I Integer 'Nothing ('Just r))
from = \Integer
x -> Integer -> I Integer 'Nothing ('Just r)
forall x (l :: L x) (r :: R x). x -> I x l r
unsafest Integer
x I Integer 'Nothing ('Just r)
-> Maybe () -> Maybe (I Integer 'Nothing ('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 (Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
r)
    where r :: Integer
r = Proxy r -> Integer
forall (i :: Integer) (proxy :: Integer -> *).
KnownInteger i =>
proxy i -> Integer
K.integerVal (forall {k} (t :: k). Proxy t
forall (t :: Integer). Proxy t
Proxy @r)
  negate' :: I Integer 'Nothing ('Just r)
-> Maybe (I Integer 'Nothing ('Just r))
negate' = Integer -> Maybe (I Integer 'Nothing ('Just r))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (Integer -> Maybe (I Integer 'Nothing ('Just r)))
-> (I Integer 'Nothing ('Just r) -> Integer)
-> I Integer 'Nothing ('Just r)
-> Maybe (I Integer 'Nothing ('Just r))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
forall a. Num a => a -> a
P.negate (Integer -> Integer)
-> (I Integer 'Nothing ('Just r) -> Integer)
-> I Integer 'Nothing ('Just r)
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I Integer 'Nothing ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap
  I Integer 'Nothing ('Just r)
a plus' :: I Integer 'Nothing ('Just r)
-> I Integer 'Nothing ('Just r)
-> Maybe (I Integer 'Nothing ('Just r))
`plus'` I Integer 'Nothing ('Just r)
b = Integer -> Maybe (I Integer 'Nothing ('Just r))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Integer 'Nothing ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer 'Nothing ('Just r)
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ I Integer 'Nothing ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer 'Nothing ('Just r)
b)
  I Integer 'Nothing ('Just r)
a mult' :: I Integer 'Nothing ('Just r)
-> I Integer 'Nothing ('Just r)
-> Maybe (I Integer 'Nothing ('Just r))
`mult'` I Integer 'Nothing ('Just r)
b = Integer -> Maybe (I Integer 'Nothing ('Just r))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Integer 'Nothing ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer 'Nothing ('Just r)
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* I Integer 'Nothing ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer 'Nothing ('Just r)
b)
  I Integer 'Nothing ('Just r)
a minus' :: I Integer 'Nothing ('Just r)
-> I Integer 'Nothing ('Just r)
-> Maybe (I Integer 'Nothing ('Just r))
`minus'` I Integer 'Nothing ('Just r)
b = Integer -> Maybe (I Integer 'Nothing ('Just r))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (I Integer 'Nothing ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer 'Nothing ('Just r)
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- I Integer 'Nothing ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer 'Nothing ('Just r)
b)
  I Integer 'Nothing ('Just r)
a div' :: I Integer 'Nothing ('Just r)
-> I Integer 'Nothing ('Just r)
-> Maybe (I Integer 'Nothing ('Just r))
`div'` I Integer 'Nothing ('Just r)
b = do Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (I Integer 'Nothing ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer 'Nothing ('Just r)
b Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0)
                  let (Integer
q, Integer
m) = Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod (I Integer 'Nothing ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer 'Nothing ('Just r)
a) (I Integer 'Nothing ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer 'Nothing ('Just r)
b)
                  Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0)
                  Integer -> Maybe (I Integer 'Nothing ('Just r))
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from Integer
q

instance Interval P.Integer 'Nothing 'Nothing where
  inhabitant :: I Integer 'Nothing 'Nothing
inhabitant = I Integer 'Nothing 'Nothing
forall x (l :: L x) (r :: R x). Zero x l r => I x l r
zero
  from :: Integer -> Maybe (I Integer 'Nothing 'Nothing)
from = I Integer 'Nothing 'Nothing -> Maybe (I Integer 'Nothing 'Nothing)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (I Integer 'Nothing 'Nothing
 -> Maybe (I Integer 'Nothing 'Nothing))
-> (Integer -> I Integer 'Nothing 'Nothing)
-> Integer
-> Maybe (I Integer 'Nothing 'Nothing)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> I Integer 'Nothing 'Nothing
Integer -> I Integer (MinL Integer) (MaxR Integer)
forall x.
Interval x (MinL x) (MaxR x) =>
x -> I x (MinL x) (MaxR x)
wrap
  negate' :: I Integer 'Nothing 'Nothing -> Maybe (I Integer 'Nothing 'Nothing)
negate' = I Integer 'Nothing 'Nothing -> Maybe (I Integer 'Nothing 'Nothing)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (I Integer 'Nothing 'Nothing
 -> Maybe (I Integer 'Nothing 'Nothing))
-> (I Integer 'Nothing 'Nothing -> I Integer 'Nothing 'Nothing)
-> I Integer 'Nothing 'Nothing
-> Maybe (I Integer 'Nothing 'Nothing)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> I Integer 'Nothing 'Nothing
Integer -> I Integer (MinL Integer) (MaxR Integer)
forall x.
Interval x (MinL x) (MaxR x) =>
x -> I x (MinL x) (MaxR x)
wrap (Integer -> I Integer 'Nothing 'Nothing)
-> (I Integer 'Nothing 'Nothing -> Integer)
-> I Integer 'Nothing 'Nothing
-> I Integer 'Nothing 'Nothing
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
forall a. Num a => a -> a
P.negate (Integer -> Integer)
-> (I Integer 'Nothing 'Nothing -> Integer)
-> I Integer 'Nothing 'Nothing
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I Integer 'Nothing 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap
  I Integer 'Nothing 'Nothing
a plus' :: I Integer 'Nothing 'Nothing
-> I Integer 'Nothing 'Nothing
-> Maybe (I Integer 'Nothing 'Nothing)
`plus'` I Integer 'Nothing 'Nothing
b = I Integer 'Nothing 'Nothing -> Maybe (I Integer 'Nothing 'Nothing)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (I Integer 'Nothing 'Nothing
a I Integer 'Nothing 'Nothing
-> I Integer 'Nothing 'Nothing -> I Integer '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 Integer 'Nothing 'Nothing
b)
  I Integer 'Nothing 'Nothing
a mult' :: I Integer 'Nothing 'Nothing
-> I Integer 'Nothing 'Nothing
-> Maybe (I Integer 'Nothing 'Nothing)
`mult'` I Integer 'Nothing 'Nothing
b = I Integer 'Nothing 'Nothing -> Maybe (I Integer 'Nothing 'Nothing)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (I Integer 'Nothing 'Nothing
a I Integer 'Nothing 'Nothing
-> I Integer 'Nothing 'Nothing -> I Integer '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 Integer 'Nothing 'Nothing
b)
  I Integer 'Nothing 'Nothing
a minus' :: I Integer 'Nothing 'Nothing
-> I Integer 'Nothing 'Nothing
-> Maybe (I Integer 'Nothing 'Nothing)
`minus'` I Integer 'Nothing 'Nothing
b = I Integer 'Nothing 'Nothing -> Maybe (I Integer 'Nothing 'Nothing)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (I Integer 'Nothing 'Nothing
a I Integer 'Nothing 'Nothing
-> I Integer 'Nothing 'Nothing -> I Integer '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 Integer 'Nothing 'Nothing
b)
  I Integer 'Nothing 'Nothing
a div' :: I Integer 'Nothing 'Nothing
-> I Integer 'Nothing 'Nothing
-> Maybe (I Integer 'Nothing 'Nothing)
`div'` I Integer 'Nothing 'Nothing
b = do Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (I Integer 'Nothing 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer 'Nothing 'Nothing
b Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0)
                  let (Integer
q, Integer
m) = Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod (I Integer 'Nothing 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer 'Nothing 'Nothing
a) (I Integer 'Nothing 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer 'Nothing 'Nothing
b)
                  Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0)
                  Integer -> Maybe (I Integer 'Nothing 'Nothing)
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from Integer
q

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

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

instance
  ( Interval Integer ('Just l) 'Nothing
  ) => Clamp Integer ('Just l) 'Nothing where
  clamp :: Integer -> I Integer ('Just l) 'Nothing
clamp = \case
    Integer
x | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= I Integer ('Just l) 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) 'Nothing
min_ -> I Integer ('Just l) 'Nothing
min_
      | Bool
otherwise -> Integer -> I Integer ('Just l) 'Nothing
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI Integer
x
    where min_ :: I Integer ('Just l) 'Nothing
min_ = I Integer ('Just 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 Integer 'Nothing ('Just r)
  ) => Clamp Integer 'Nothing ('Just r) where
  clamp :: Integer -> I Integer 'Nothing ('Just r)
clamp = \case
    Integer
x | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= I Integer 'Nothing ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer 'Nothing ('Just r)
max_ -> I Integer 'Nothing ('Just r)
max_
      | Bool
otherwise -> Integer -> I Integer 'Nothing ('Just r)
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI Integer
x
    where max_ :: I Integer 'Nothing ('Just r)
max_ = I Integer 'Nothing ('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 Integer 'Nothing 'Nothing
  ) => Clamp Integer 'Nothing 'Nothing where
  clamp :: Integer -> I Integer 'Nothing 'Nothing
clamp = Integer -> I Integer 'Nothing 'Nothing
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI

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

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

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

instance
  ( rd <= ru
  , Interval Integer yld ('Just rd)
  , Interval Integer 'Nothing ('Just ru)
  ) => Up    Integer yld ('Just rd) 'Nothing ('Just ru)

instance
  ( Interval Integer yld yrd
  , Interval Integer 'Nothing 'Nothing )
  => Up Integer yld yrd 'Nothing 'Nothing

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

instance forall l r t.
  ( Interval    P.Integer ('Just l) ('Just r)
  , KnownCtx    P.Integer ('Just l) ('Just r) t
  ) => Known    P.Integer ('Just l) ('Just r) t where
  type KnownCtx P.Integer ('Just l) ('Just r) t =
    (K.KnownInteger t, l <= t, t <= r)
  known' :: Proxy t -> I Integer ('Just l) ('Just r)
known' = Integer -> I Integer ('Just l) ('Just r)
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI (Integer -> I Integer ('Just l) ('Just r))
-> (Proxy t -> Integer) -> Proxy t -> I Integer ('Just l) ('Just r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy t -> Integer
forall (i :: Integer) (proxy :: Integer -> *).
KnownInteger i =>
proxy i -> Integer
K.integerVal

instance forall t l.
  ( Interval    P.Integer ('Just l) 'Nothing
  , KnownCtx    P.Integer ('Just l) 'Nothing t
  ) => Known    P.Integer ('Just l) 'Nothing t where
  type KnownCtx P.Integer ('Just l) 'Nothing t = (K.KnownInteger t, l <= t)
  known' :: Proxy t -> I Integer ('Just l) 'Nothing
known' = Integer -> I Integer ('Just l) 'Nothing
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI (Integer -> I Integer ('Just l) 'Nothing)
-> (Proxy t -> Integer) -> Proxy t -> I Integer ('Just l) 'Nothing
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy t -> Integer
forall (i :: Integer) (proxy :: Integer -> *).
KnownInteger i =>
proxy i -> Integer
K.integerVal

instance forall t r.
  ( Interval    P.Integer 'Nothing ('Just r)
  , KnownCtx    P.Integer 'Nothing ('Just r) t
  ) => Known    P.Integer 'Nothing ('Just r) t where
  type KnownCtx P.Integer 'Nothing ('Just r) t = (K.KnownInteger t, t <= r)
  known' :: Proxy t -> I Integer 'Nothing ('Just r)
known' = Integer -> I Integer 'Nothing ('Just r)
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI (Integer -> I Integer 'Nothing ('Just r))
-> (Proxy t -> Integer) -> Proxy t -> I Integer 'Nothing ('Just r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy t -> Integer
forall (i :: Integer) (proxy :: Integer -> *).
KnownInteger i =>
proxy i -> Integer
K.integerVal

instance forall t.
  ( KnownCtx    P.Integer 'Nothing 'Nothing t
  ) => Known    P.Integer 'Nothing 'Nothing t where
  type KnownCtx P.Integer 'Nothing 'Nothing t = K.KnownInteger t
  known' :: Proxy t -> I Integer 'Nothing 'Nothing
known' = Integer -> I Integer 'Nothing 'Nothing
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI (Integer -> I Integer 'Nothing 'Nothing)
-> (Proxy t -> Integer) -> Proxy t -> I Integer 'Nothing 'Nothing
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy t -> Integer
forall (i :: Integer) (proxy :: Integer -> *).
KnownInteger i =>
proxy i -> Integer
K.integerVal

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

instance forall l r.
  ( Interval P.Integer ('Just l) ('Just r)
  ) => With  P.Integer ('Just l) ('Just r) where
  with :: forall b.
I Integer ('Just l) ('Just r)
-> (forall (t :: T Integer).
    Known Integer ('Just l) ('Just r) t =>
    Proxy t -> b)
-> b
with I Integer ('Just l) ('Just r)
x forall (t :: T Integer).
Known Integer ('Just l) ('Just r) t =>
Proxy t -> b
g = case Integer -> SomeInteger
K.someIntegerVal (I Integer ('Just l) ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) ('Just r)
x) of
    K.SomeInteger (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(Integer): impossible") (Maybe b -> b) -> Maybe b -> b
forall a b. (a -> b) -> a -> b
$ do
        Dict
  (Assert
     (OrdCond
        (CmpInteger_ (Normalize l) (Normalize n)) 'True 'True 'False)
     (TypeError ...))
Dict <- forall (a :: Integer) (b :: Integer).
(KnownInteger a, KnownInteger b) =>
Maybe (Dict (a <= b))
leInteger @l @t
        Dict
  (Assert
     (OrdCond
        (CmpInteger_ (Normalize n) (Normalize r)) 'True 'True 'False)
     (TypeError ...))
Dict <- forall (a :: Integer) (b :: Integer).
(KnownInteger a, KnownInteger b) =>
Maybe (Dict (a <= b))
leInteger @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 Integer).
Known Integer ('Just l) ('Just r) t =>
Proxy t -> b
g Proxy n
Proxy n
pt)

instance forall l.
  ( Interval P.Integer ('Just l) 'Nothing
  ) => With  P.Integer ('Just l) 'Nothing where
  with :: forall b.
I Integer ('Just l) 'Nothing
-> (forall (t :: T Integer).
    Known Integer ('Just l) 'Nothing t =>
    Proxy t -> b)
-> b
with I Integer ('Just l) 'Nothing
x forall (t :: T Integer).
Known Integer ('Just l) 'Nothing t =>
Proxy t -> b
g = case Integer -> SomeInteger
K.someIntegerVal (I Integer ('Just l) 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) 'Nothing
x) of
    K.SomeInteger (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(Integer): impossible") (Maybe b -> b) -> Maybe b -> b
forall a b. (a -> b) -> a -> b
$ do
        Dict
  (Assert
     (OrdCond
        (CmpInteger_ (Normalize l) (Normalize n)) 'True 'True 'False)
     (TypeError ...))
Dict <- forall (a :: Integer) (b :: Integer).
(KnownInteger a, KnownInteger b) =>
Maybe (Dict (a <= b))
leInteger @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 Integer).
Known Integer ('Just l) 'Nothing t =>
Proxy t -> b
g Proxy n
Proxy n
pt)

instance forall r.
  ( Interval P.Integer 'Nothing ('Just r)
  ) => With  P.Integer 'Nothing ('Just r) where
  with :: forall b.
I Integer 'Nothing ('Just r)
-> (forall (t :: T Integer).
    Known Integer 'Nothing ('Just r) t =>
    Proxy t -> b)
-> b
with I Integer 'Nothing ('Just r)
x forall (t :: T Integer).
Known Integer 'Nothing ('Just r) t =>
Proxy t -> b
g = case Integer -> SomeInteger
K.someIntegerVal (I Integer 'Nothing ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer 'Nothing ('Just r)
x) of
    K.SomeInteger (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(Integer): impossible") (Maybe b -> b) -> Maybe b -> b
forall a b. (a -> b) -> a -> b
$ do
        Dict
  (Assert
     (OrdCond
        (CmpInteger_ (Normalize n) (Normalize r)) 'True 'True 'False)
     (TypeError ...))
Dict <- forall (a :: Integer) (b :: Integer).
(KnownInteger a, KnownInteger b) =>
Maybe (Dict (a <= b))
leInteger @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 Integer).
Known Integer 'Nothing ('Just r) t =>
Proxy t -> b
g Proxy n
Proxy n
pt)

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

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

instance
  ( Interval    P.Integer ('Just l) ('Just r), l /= r
  ) => Discrete P.Integer ('Just l) ('Just r) where
  pred' :: I Integer ('Just l) ('Just r)
-> Maybe (I Integer ('Just l) ('Just r))
pred' I Integer ('Just l) ('Just r)
i = Integer -> I Integer ('Just l) ('Just r)
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI (I Integer ('Just l) ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) ('Just r)
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) I Integer ('Just l) ('Just r)
-> Maybe () -> Maybe (I Integer ('Just 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 Integer ('Just 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 Integer ('Just l) ('Just r)
-> I Integer ('Just l) ('Just r) -> Bool
forall a. Ord a => a -> a -> Bool
< I Integer ('Just l) ('Just r)
i)
  succ' :: I Integer ('Just l) ('Just r)
-> Maybe (I Integer ('Just l) ('Just r))
succ' I Integer ('Just l) ('Just r)
i = Integer -> I Integer ('Just l) ('Just r)
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI (I Integer ('Just l) ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) ('Just r)
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) I Integer ('Just l) ('Just r)
-> Maybe () -> Maybe (I Integer ('Just 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 Integer ('Just l) ('Just r)
i I Integer ('Just l) ('Just r)
-> I Integer ('Just l) ('Just r) -> Bool
forall a. Ord a => a -> a -> Bool
< I Integer ('Just 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    P.Integer ('Just l) 'Nothing
  ) => Discrete P.Integer ('Just l) 'Nothing where
  pred' :: I Integer ('Just l) 'Nothing
-> Maybe (I Integer ('Just l) 'Nothing)
pred' I Integer ('Just l) 'Nothing
i = Integer -> I Integer ('Just l) 'Nothing
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI (I Integer ('Just l) 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) 'Nothing
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) I Integer ('Just l) 'Nothing
-> Maybe () -> Maybe (I Integer ('Just 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 Integer ('Just l) 'Nothing
forall x (l :: L x) (r :: R x). Known x l r (MinI x l r) => I x l r
min I Integer ('Just l) 'Nothing
-> I Integer ('Just l) 'Nothing -> Bool
forall a. Ord a => a -> a -> Bool
< I Integer ('Just l) 'Nothing
i)
  succ' :: I Integer ('Just l) 'Nothing
-> Maybe (I Integer ('Just l) 'Nothing)
succ' = I Integer ('Just l) 'Nothing
-> Maybe (I Integer ('Just l) 'Nothing)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (I Integer ('Just l) 'Nothing
 -> Maybe (I Integer ('Just l) 'Nothing))
-> (I Integer ('Just l) 'Nothing -> I Integer ('Just l) 'Nothing)
-> I Integer ('Just l) 'Nothing
-> Maybe (I Integer ('Just l) 'Nothing)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I Integer ('Just l) 'Nothing -> I Integer ('Just 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    P.Integer 'Nothing ('Just r)
  ) => Discrete P.Integer 'Nothing ('Just r) where
  pred' :: I Integer 'Nothing ('Just r)
-> Maybe (I Integer 'Nothing ('Just r))
pred' = I Integer 'Nothing ('Just r)
-> Maybe (I Integer 'Nothing ('Just r))
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (I Integer 'Nothing ('Just r)
 -> Maybe (I Integer 'Nothing ('Just r)))
-> (I Integer 'Nothing ('Just r) -> I Integer 'Nothing ('Just r))
-> I Integer 'Nothing ('Just r)
-> Maybe (I Integer 'Nothing ('Just r))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I Integer 'Nothing ('Just r) -> I Integer 'Nothing ('Just r)
forall x (l :: L x) (r :: R x). Pred x l r => I x l r -> I x l r
pred
  succ' :: I Integer 'Nothing ('Just r)
-> Maybe (I Integer 'Nothing ('Just r))
succ' I Integer 'Nothing ('Just r)
i = Integer -> I Integer 'Nothing ('Just r)
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI (I Integer 'Nothing ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer 'Nothing ('Just r)
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) I Integer 'Nothing ('Just r)
-> Maybe () -> Maybe (I Integer 'Nothing ('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 Integer 'Nothing ('Just r)
i I Integer 'Nothing ('Just r)
-> I Integer 'Nothing ('Just r) -> Bool
forall a. Ord a => a -> a -> Bool
< I Integer 'Nothing ('Just r)
forall x (l :: L x) (r :: R x). Known x l r (MaxI x l r) => I x l r
max)

instance Discrete P.Integer 'Nothing 'Nothing where
  pred' :: I Integer 'Nothing 'Nothing -> Maybe (I Integer 'Nothing 'Nothing)
pred'  = I Integer 'Nothing 'Nothing -> Maybe (I Integer 'Nothing 'Nothing)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (I Integer 'Nothing 'Nothing
 -> Maybe (I Integer 'Nothing 'Nothing))
-> (I Integer 'Nothing 'Nothing -> I Integer 'Nothing 'Nothing)
-> I Integer 'Nothing 'Nothing
-> Maybe (I Integer 'Nothing 'Nothing)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I Integer 'Nothing 'Nothing -> I Integer 'Nothing 'Nothing
forall x (l :: L x) (r :: R x). Pred x l r => I x l r -> I x l r
pred
  succ' :: I Integer 'Nothing 'Nothing -> Maybe (I Integer 'Nothing 'Nothing)
succ'  = I Integer 'Nothing 'Nothing -> Maybe (I Integer 'Nothing 'Nothing)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (I Integer 'Nothing 'Nothing
 -> Maybe (I Integer 'Nothing 'Nothing))
-> (I Integer 'Nothing 'Nothing -> I Integer 'Nothing 'Nothing)
-> I Integer 'Nothing 'Nothing
-> Maybe (I Integer 'Nothing 'Nothing)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I Integer 'Nothing 'Nothing -> I Integer 'Nothing 'Nothing
forall x (l :: L x) (r :: R x). Succ x l r => I x l r -> I x l r
succ

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

instance
  ( Discrete P.Integer 'Nothing r
  ) => Pred  P.Integer 'Nothing r where
  pred :: I Integer 'Nothing r -> I Integer 'Nothing r
pred I Integer 'Nothing r
i = Integer -> I Integer 'Nothing r
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI (I Integer 'Nothing r -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer 'Nothing r
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)

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

instance
  ( Discrete P.Integer l 'Nothing
  ) => Succ  P.Integer l 'Nothing where
  succ :: I Integer l 'Nothing -> I Integer l 'Nothing
succ I Integer l 'Nothing
i = Integer -> I Integer l 'Nothing
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI (I Integer l 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer l 'Nothing
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)

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

instance
  ( Interval P.Integer ('Just l) 'Nothing, K.P 0 <= l
  ) => Plus  P.Integer ('Just l) 'Nothing where
  I Integer ('Just l) 'Nothing
a plus :: I Integer ('Just l) 'Nothing
-> I Integer ('Just l) 'Nothing -> I Integer ('Just l) 'Nothing
`plus` I Integer ('Just l) 'Nothing
b = Integer -> I Integer ('Just l) 'Nothing
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI (I Integer ('Just l) 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) 'Nothing
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ I Integer ('Just l) 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) 'Nothing
b)

instance
  ( Interval P.Integer 'Nothing ('Just r), r <= K.P 0
  ) => Plus  P.Integer 'Nothing ('Just r) where
  I Integer 'Nothing ('Just r)
a plus :: I Integer 'Nothing ('Just r)
-> I Integer 'Nothing ('Just r) -> I Integer 'Nothing ('Just r)
`plus` I Integer 'Nothing ('Just r)
b = Integer -> I Integer 'Nothing ('Just r)
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI (I Integer 'Nothing ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer 'Nothing ('Just r)
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ I Integer 'Nothing ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer 'Nothing ('Just r)
b)

instance Plus P.Integer 'Nothing 'Nothing where
  I Integer 'Nothing 'Nothing
a plus :: I Integer 'Nothing 'Nothing
-> I Integer 'Nothing 'Nothing -> I Integer 'Nothing 'Nothing
`plus` I Integer 'Nothing 'Nothing
b = Integer -> I Integer 'Nothing 'Nothing
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI (I Integer 'Nothing 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer 'Nothing 'Nothing
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ I Integer 'Nothing 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer 'Nothing 'Nothing
b)

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

instance
  ( Interval P.Integer ('Just l) 'Nothing, K.P 0 <= l
  ) => Mult P.Integer ('Just l) 'Nothing where
  I Integer ('Just l) 'Nothing
a mult :: I Integer ('Just l) 'Nothing
-> I Integer ('Just l) 'Nothing -> I Integer ('Just l) 'Nothing
`mult` I Integer ('Just l) 'Nothing
b = Integer -> I Integer ('Just l) 'Nothing
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI (I Integer ('Just l) 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) 'Nothing
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* I Integer ('Just l) 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer ('Just l) 'Nothing
b)

instance Mult P.Integer 'Nothing 'Nothing where
  I Integer 'Nothing 'Nothing
a mult :: I Integer 'Nothing 'Nothing
-> I Integer 'Nothing 'Nothing -> I Integer 'Nothing 'Nothing
`mult` I Integer 'Nothing 'Nothing
b = Integer -> I Integer 'Nothing 'Nothing
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI (I Integer 'Nothing 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer 'Nothing 'Nothing
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* I Integer 'Nothing 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer 'Nothing 'Nothing
b)

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

instance Minus P.Integer 'Nothing 'Nothing where
  I Integer 'Nothing 'Nothing
a minus :: I Integer 'Nothing 'Nothing
-> I Integer 'Nothing 'Nothing -> I Integer 'Nothing 'Nothing
`minus` I Integer 'Nothing 'Nothing
b = Integer -> I Integer 'Nothing 'Nothing
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI (I Integer 'Nothing 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer 'Nothing 'Nothing
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- I Integer 'Nothing 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I Integer 'Nothing 'Nothing
b)

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

instance
  ( Interval P.Integer ('Just l) ('Just r), l <= K.P 0, K.P 0 <= r
  ) => Zero  P.Integer ('Just l) ('Just r) where
  zero :: I Integer ('Just l) ('Just r)
zero = Integer -> I Integer ('Just l) ('Just r)
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI Integer
0

instance
  ( Interval P.Integer ('Just l) 'Nothing, l <= K.P 0
  ) => Zero  P.Integer ('Just l) 'Nothing where
  zero :: I Integer ('Just l) 'Nothing
zero = Integer -> I Integer ('Just l) 'Nothing
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI Integer
0

instance
  ( Interval P.Integer 'Nothing ('Just r), K.P 0 <= r
  ) => Zero  P.Integer 'Nothing ('Just r) where
  zero :: I Integer 'Nothing ('Just r)
zero = Integer -> I Integer 'Nothing ('Just r)
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI Integer
0

instance Zero P.Integer 'Nothing 'Nothing where
  zero :: I Integer 'Nothing 'Nothing
zero = Integer -> I Integer 'Nothing 'Nothing
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI Integer
0

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

instance
  ( Interval P.Integer ('Just l) ('Just r), l <= K.P 1, K.P 1 <= r
  ) => One   P.Integer ('Just l) ('Just r) where
  one :: I Integer ('Just l) ('Just r)
one = Integer -> I Integer ('Just l) ('Just r)
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI Integer
1

instance
  ( Interval P.Integer ('Just l) 'Nothing, l <= K.P 1
  ) => One   P.Integer ('Just l) 'Nothing where
  one :: I Integer ('Just l) 'Nothing
one = Integer -> I Integer ('Just l) 'Nothing
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI Integer
1

instance
  ( Interval P.Integer 'Nothing ('Just r), K.P 1 <= r
  ) => One   P.Integer 'Nothing ('Just r) where
  one :: I Integer 'Nothing ('Just r)
one = Integer -> I Integer 'Nothing ('Just r)
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI Integer
1

instance One P.Integer 'Nothing 'Nothing where
  one :: I Integer 'Nothing 'Nothing
one = Integer -> I Integer 'Nothing 'Nothing
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI Integer
1

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

instance
  ( Zero      P.Integer ('Just l) ('Just r), l K.== K.Negate r
  ) => Negate P.Integer ('Just l) ('Just r) where
  negate :: I Integer ('Just l) ('Just r) -> I Integer ('Just l) ('Just r)
negate = Integer -> I Integer ('Just l) ('Just r)
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI (Integer -> I Integer ('Just l) ('Just r))
-> (I Integer ('Just l) ('Just r) -> Integer)
-> I Integer ('Just l) ('Just r)
-> I Integer ('Just l) ('Just r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
forall a. Num a => a -> a
P.negate (Integer -> Integer)
-> (I Integer ('Just l) ('Just r) -> Integer)
-> I Integer ('Just l) ('Just r)
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I Integer ('Just l) ('Just r) -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap

instance Negate P.Integer 'Nothing 'Nothing where
  negate :: I Integer 'Nothing 'Nothing -> I Integer 'Nothing 'Nothing
negate = Integer -> I Integer 'Nothing 'Nothing
forall x (l :: L x) (r :: R x). x -> I x l r
UnsafeI (Integer -> I Integer 'Nothing 'Nothing)
-> (I Integer 'Nothing 'Nothing -> Integer)
-> I Integer 'Nothing 'Nothing
-> I Integer 'Nothing 'Nothing
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
forall a. Num a => a -> a
P.negate (Integer -> Integer)
-> (I Integer 'Nothing 'Nothing -> Integer)
-> I Integer 'Nothing 'Nothing
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I Integer 'Nothing 'Nothing -> Integer
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap

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

instance
  ( Interval Integer ('Just l) ('Just r)
  ) => Shove Integer ('Just l) ('Just r) where
  shove :: Integer -> I Integer ('Just l) ('Just r)
shove = \Integer
x -> Integer -> I Integer ('Just l) ('Just r)
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Integer -> I Integer ('Just l) ('Just r))
-> Integer -> I Integer ('Just l) ('Just r)
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
mod Integer
x (Integer
r Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
l
    where l :: Integer
l = I Integer ('Just l) ('Just r) -> Integer
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 @Integer @('Just l) @('Just r))
          r :: Integer
r = I Integer ('Just l) ('Just r) -> Integer
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 @Integer @('Just l) @('Just r))

instance
  ( Interval Integer ('Just l) 'Nothing
  ) => Shove Integer ('Just l) 'Nothing where
  shove :: Integer -> I Integer ('Just l) 'Nothing
shove = \Integer
x -> Integer -> I Integer ('Just l) 'Nothing
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Integer -> I Integer ('Just l) 'Nothing)
-> Integer -> I Integer ('Just l) 'Nothing
forall a b. (a -> b) -> a -> b
$ if Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
l then Integer
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ (Integer
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
x) else Integer
x
    where l :: Integer
l = I Integer ('Just l) 'Nothing -> Integer
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 @Integer @('Just l) @'Nothing)

instance
  ( Interval Integer 'Nothing ('Just r)
  ) => Shove Integer 'Nothing ('Just r) where
  shove :: Integer -> I Integer 'Nothing ('Just r)
shove = \Integer
x -> Integer -> I Integer 'Nothing ('Just r)
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (Integer -> I Integer 'Nothing ('Just r))
-> Integer -> I Integer 'Nothing ('Just r)
forall a b. (a -> b) -> a -> b
$ if Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
r then Integer
r Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
r) else Integer
x
    where r :: Integer
r = I Integer 'Nothing ('Just r) -> Integer
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 @Integer @'Nothing @('Just r))

instance
  ( Interval Integer 'Nothing 'Nothing
  ) => Shove Integer 'Nothing 'Nothing where
  shove :: Integer -> I Integer 'Nothing 'Nothing
shove = Integer -> I Integer 'Nothing 'Nothing
Integer -> I Integer (MinL Integer) (MaxR Integer)
forall x.
Interval x (MinL x) (MaxR x) =>
x -> I x (MinL x) (MaxR x)
wrap