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

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

module I.Autogen.CIntMax () where

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

import I.Internal

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

-- | This is so that GHC doesn't complain about the unused modules,
-- which we import here so that `genmodules.sh` doesn't have to add it
-- to the generated modules.
_ignore :: (CSize, Int)
_ignore :: (CSize, Int)
_ignore = (CSize
0, Int
0)

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

type instance MinL CIntMax = MinT CIntMax
type instance MaxR CIntMax = MaxT CIntMax

instance forall (l :: K.Integer) (r :: K.Integer).
  ( IntervalCtx CIntMax l r
  ) => Interval CIntMax l r where
  type IntervalCtx CIntMax l r =
    ( K.KnownInteger l
    , K.KnownInteger r
    , MinT CIntMax <= l
    , l <= r
    , r <= MaxT CIntMax )
  type MinI CIntMax l r = l
  type MaxI CIntMax l r = r
  inhabitant :: I CIntMax l r
inhabitant = I CIntMax l r
forall x (l :: L x) (r :: R x). Known x l r (MinI x l r) => I x l r
min
  from :: CIntMax -> Maybe (I CIntMax l r)
from = \CIntMax
x -> CIntMax -> I CIntMax l r
forall x (l :: L x) (r :: R x). x -> I x l r
unsafest CIntMax
x I CIntMax l r -> Maybe () -> Maybe (I CIntMax l 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 (CIntMax
l CIntMax -> CIntMax -> Bool
forall a. Ord a => a -> a -> Bool
<= CIntMax
x Bool -> Bool -> Bool
&& CIntMax
x CIntMax -> CIntMax -> Bool
forall a. Ord a => a -> a -> Bool
<= CIntMax
r)
    where l :: CIntMax
l = Integer -> CIntMax
forall a. Num a => Integer -> a
fromInteger (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)) :: CIntMax
          r :: CIntMax
r = Integer -> CIntMax
forall a. Num a => Integer -> a
fromInteger (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)) :: CIntMax
  negate' :: I CIntMax l r -> Maybe (I CIntMax l r)
negate' (I CIntMax l r -> CIntMax
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap -> CIntMax
x) = do
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (CIntMax
x CIntMax -> CIntMax -> Bool
forall a. Eq a => a -> a -> Bool
/= CIntMax
forall a. Bounded a => a
minBound)
    CIntMax -> Maybe (I CIntMax l r)
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (CIntMax -> CIntMax
forall a. Num a => a -> a
P.negate CIntMax
x)
  (I CIntMax l r -> CIntMax
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap -> CIntMax
a) plus' :: I CIntMax l r -> I CIntMax l r -> Maybe (I CIntMax l r)
`plus'` (I CIntMax l r -> CIntMax
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap -> CIntMax
b)
    | CIntMax
b CIntMax -> CIntMax -> Bool
forall a. Ord a => a -> a -> Bool
> CIntMax
0 Bool -> Bool -> Bool
&& CIntMax
a CIntMax -> CIntMax -> Bool
forall a. Ord a => a -> a -> Bool
> CIntMax
forall a. Bounded a => a
maxBound CIntMax -> CIntMax -> CIntMax
forall a. Num a => a -> a -> a
- CIntMax
b = Maybe (I CIntMax l r)
forall a. Maybe a
Nothing
    | CIntMax
b CIntMax -> CIntMax -> Bool
forall a. Ord a => a -> a -> Bool
< CIntMax
0 Bool -> Bool -> Bool
&& CIntMax
a CIntMax -> CIntMax -> Bool
forall a. Ord a => a -> a -> Bool
< CIntMax
forall a. Bounded a => a
minBound CIntMax -> CIntMax -> CIntMax
forall a. Num a => a -> a -> a
- CIntMax
b = Maybe (I CIntMax l r)
forall a. Maybe a
Nothing
    | Bool
otherwise                 = CIntMax -> Maybe (I CIntMax l r)
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (CIntMax
a CIntMax -> CIntMax -> CIntMax
forall a. Num a => a -> a -> a
+ CIntMax
b)
  (I CIntMax l r -> CIntMax
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap -> CIntMax
a) mult' :: I CIntMax l r -> I CIntMax l r -> Maybe (I CIntMax l r)
`mult'` (I CIntMax l r -> CIntMax
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap -> CIntMax
b) = do
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ case CIntMax
a CIntMax -> CIntMax -> Bool
forall a. Ord a => a -> a -> Bool
<= CIntMax
0 of
      Bool
True  | CIntMax
b CIntMax -> CIntMax -> Bool
forall a. Ord a => a -> a -> Bool
<= CIntMax
0    -> CIntMax
a CIntMax -> CIntMax -> Bool
forall a. Eq a => a -> a -> Bool
== CIntMax
0 Bool -> Bool -> Bool
|| CIntMax
b CIntMax -> CIntMax -> Bool
forall a. Ord a => a -> a -> Bool
>= (CIntMax
forall a. Bounded a => a
maxBound CIntMax -> CIntMax -> CIntMax
forall a. Integral a => a -> a -> a
`quot` CIntMax
a)
            | Bool
otherwise -> CIntMax
a CIntMax -> CIntMax -> Bool
forall a. Ord a => a -> a -> Bool
>= (CIntMax
forall a. Bounded a => a
minBound CIntMax -> CIntMax -> CIntMax
forall a. Integral a => a -> a -> a
`quot` CIntMax
b)
      Bool
False | CIntMax
b CIntMax -> CIntMax -> Bool
forall a. Ord a => a -> a -> Bool
<= CIntMax
0    -> CIntMax
b CIntMax -> CIntMax -> Bool
forall a. Ord a => a -> a -> Bool
>= (CIntMax
forall a. Bounded a => a
minBound CIntMax -> CIntMax -> CIntMax
forall a. Integral a => a -> a -> a
`quot` CIntMax
a)
            | Bool
otherwise -> CIntMax
a CIntMax -> CIntMax -> Bool
forall a. Ord a => a -> a -> Bool
<= (CIntMax
forall a. Bounded a => a
maxBound CIntMax -> CIntMax -> CIntMax
forall a. Integral a => a -> a -> a
`quot` CIntMax
b)
    CIntMax -> Maybe (I CIntMax l r)
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (CIntMax
a CIntMax -> CIntMax -> CIntMax
forall a. Num a => a -> a -> a
* CIntMax
b)
  (I CIntMax l r -> CIntMax
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap -> CIntMax
a) minus' :: I CIntMax l r -> I CIntMax l r -> Maybe (I CIntMax l r)
`minus'` (I CIntMax l r -> CIntMax
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap -> CIntMax
b)
    | CIntMax
b CIntMax -> CIntMax -> Bool
forall a. Ord a => a -> a -> Bool
> CIntMax
0 Bool -> Bool -> Bool
&& CIntMax
a CIntMax -> CIntMax -> Bool
forall a. Ord a => a -> a -> Bool
< CIntMax
forall a. Bounded a => a
minBound CIntMax -> CIntMax -> CIntMax
forall a. Num a => a -> a -> a
+ CIntMax
b = Maybe (I CIntMax l r)
forall a. Maybe a
Nothing
    | CIntMax
b CIntMax -> CIntMax -> Bool
forall a. Ord a => a -> a -> Bool
< CIntMax
0 Bool -> Bool -> Bool
&& CIntMax
a CIntMax -> CIntMax -> Bool
forall a. Ord a => a -> a -> Bool
> CIntMax
forall a. Bounded a => a
maxBound CIntMax -> CIntMax -> CIntMax
forall a. Num a => a -> a -> a
+ CIntMax
b = Maybe (I CIntMax l r)
forall a. Maybe a
Nothing
    | Bool
otherwise                 = CIntMax -> Maybe (I CIntMax l r)
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (CIntMax
a CIntMax -> CIntMax -> CIntMax
forall a. Num a => a -> a -> a
- CIntMax
b)
  (I CIntMax l r -> CIntMax
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap -> CIntMax
a) div' :: I CIntMax l r -> I CIntMax l r -> Maybe (I CIntMax l r)
`div'` (I CIntMax l r -> CIntMax
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap -> CIntMax
b) = do
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (CIntMax
b CIntMax -> CIntMax -> Bool
forall a. Eq a => a -> a -> Bool
/= CIntMax
0 Bool -> Bool -> Bool
&& (CIntMax
b CIntMax -> CIntMax -> Bool
forall a. Eq a => a -> a -> Bool
/= -CIntMax
1 Bool -> Bool -> Bool
|| CIntMax
a CIntMax -> CIntMax -> Bool
forall a. Eq a => a -> a -> Bool
/= CIntMax
forall a. Bounded a => a
minBound))
    let (CIntMax
q, CIntMax
m) = CIntMax -> CIntMax -> (CIntMax, CIntMax)
forall a. Integral a => a -> a -> (a, a)
divMod CIntMax
a CIntMax
b
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (CIntMax
m CIntMax -> CIntMax -> Bool
forall a. Eq a => a -> a -> Bool
== CIntMax
0)
    CIntMax -> Maybe (I CIntMax l r)
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from CIntMax
q

instance (Interval CIntMax l r) => Clamp CIntMax l r

instance (Interval CIntMax ld rd, Interval CIntMax lu ru, lu <= ld, rd <= ru)
  => Up CIntMax ld rd lu ru

instance forall l r t.
  ( Interval CIntMax l r, KnownCtx CIntMax l r t
  ) => Known CIntMax l r t where
  type KnownCtx CIntMax l r t = (K.KnownInteger t, l <= t, t <= r)
  known' :: Proxy t -> I CIntMax l r
known' = CIntMax -> I CIntMax l r
forall x (l :: L x) (r :: R x).
(HasCallStack, Interval x l r) =>
x -> I x l r
unsafe (CIntMax -> I CIntMax l r)
-> (Proxy t -> CIntMax) -> Proxy t -> I CIntMax l r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> CIntMax
forall a. Num a => Integer -> a
fromInteger (Integer -> CIntMax) -> (Proxy t -> Integer) -> Proxy t -> CIntMax
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 CIntMax l r) => With CIntMax l r where
  with :: forall b.
I CIntMax l r
-> (forall (t :: T CIntMax). Known CIntMax l r t => Proxy t -> b)
-> b
with I CIntMax l r
x forall (t :: T CIntMax). Known CIntMax l r t => Proxy t -> b
g = case Integer -> SomeInteger
K.someIntegerVal (CIntMax -> Integer
forall a. Integral a => a -> Integer
toInteger (I CIntMax l r -> CIntMax
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I CIntMax l 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: 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 CIntMax). Known CIntMax l r t => Proxy t -> b
g Proxy n
Proxy n
pt)

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

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

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

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

instance forall l r. (Interval CIntMax l r) => Shove CIntMax l r where
  shove :: CIntMax -> I CIntMax l r
shove = \CIntMax
x -> I CIntMax l r -> Maybe (I CIntMax l r) -> I CIntMax l r
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> I CIntMax l r
forall a. HasCallStack => [Char] -> a
error [Char]
"shove(CIntMax): impossible") (Maybe (I CIntMax l r) -> I CIntMax l r)
-> Maybe (I CIntMax l r) -> I CIntMax l r
forall a b. (a -> b) -> a -> b
$
                  CIntMax -> Maybe (I CIntMax l r)
forall x (l :: L x) (r :: R x).
Interval x l r =>
x -> Maybe (I x l r)
from (CIntMax -> Maybe (I CIntMax l r))
-> CIntMax -> Maybe (I CIntMax l r)
forall a b. (a -> b) -> a -> b
$ Integer -> CIntMax
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
mod (CIntMax -> Integer
forall a. Integral a => a -> Integer
toInteger CIntMax
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 = CIntMax -> Integer
forall a. Integral a => a -> Integer
toInteger (I CIntMax l r -> CIntMax
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 @CIntMax @l @r))
          r :: Integer
r = CIntMax -> Integer
forall a. Integral a => a -> Integer
toInteger (I CIntMax l r -> CIntMax
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 @CIntMax @l @r))