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

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

module I.Autogen.CPtrdiff () 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 CPtrdiff = MinT CPtrdiff
type instance MaxR CPtrdiff = MaxT CPtrdiff

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

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

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

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

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

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

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

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