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

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

module I.Autogen.CULLong () where

import Control.Monad
import Data.Constraint
import Data.Maybe
import Data.Proxy
import Data.Word
import Data.Type.Ord
import Foreign.C.Types
import GHC.TypeLits qualified as L
import KindInteger (type (/=))
import Prelude hiding (min, max, div)

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, Word)
_ignore :: (CSize, Word)
_ignore = (CSize
0, Word
0)

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


type instance MinL CULLong = MinT CULLong
type instance MaxR CULLong = MaxT CULLong

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

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

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

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

instance forall l r. (Interval CULLong l r) => With CULLong l r where
  with :: forall b.
I CULLong l r
-> (forall (t :: T CULLong). Known CULLong l r t => Proxy t -> b)
-> b
with I CULLong l r
x forall (t :: T CULLong). Known CULLong l r t => Proxy t -> b
g = 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
    L.SomeNat (Proxy n
pt :: Proxy t) <- Integer -> Maybe SomeNat
L.someNatVal (CULLong -> Integer
forall a. Integral a => a -> Integer
toInteger (I CULLong l r -> CULLong
forall x (l :: L x) (r :: R x). I x l r -> x
unwrap I CULLong l r
x))
    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 CULLong). Known CULLong l r t => Proxy t -> b
g Proxy n
Proxy n
pt)

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

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

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

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