-- Copyright 2017-2021 Google LLC
-- Copyright 2022 Andrew Pritchard
--
-- Licensed under the Apache License, Version 2.0 (the "License");
-- you may not use this file except in compliance with the License.
-- You may obtain a copy of the License at
--
--      http://www.apache.org/licenses/LICENSE-2.0
--
-- Unless required by applicable law or agreed to in writing, software
-- distributed under the License is distributed on an "AS IS" BASIS,
-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-- See the License for the specific language governing permissions and
-- limitations under the License.

{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}

-- | Finite natural numbers, with upper bound as part of the type.
--
-- A value of type @'Fin' n@ ranges from @0@ to @n - 1@.
--
-- Operations that can cause numbers to be out-of-range come with variants that
-- throw runtime errors, return 'Maybe', or return results modulo the bound.
--
-- In contrast to "Data.Fin.Int", this module provides an API where runtime
-- values of bound parameters are provided explicitly by 'SInt's, which can be
-- more intuitive than passing implicitly via 'KnownNat', and can avoid some
-- runtime 'Numeric.Natural.Natural'-to-'Int' conversions and bounds checks
-- resulting from 'KnownNat', at the cost of making some code more tedious
-- where the bounds "should" be obvious.

module Data.Fin.Int.Explicit
         ( -- * Finite Natural Numbers
           Fin, FinSize
           -- * Conversion
         , fin, finFromIntegral, knownFin, tryFin, finMod, finDivMod, finToInt
           -- * Bound Manipulation
         , embed, unembed, tryUnembed
         , shiftFin, unshiftFin, tryUnshiftFin, splitFin, concatFin
         , weaken, strengthen
         -- * Enumeration
         , minFin, maxFin
         , enumFin, enumFinDown, enumDownFrom, enumDownTo, enumDownFromTo
           -- * Arithmetic
           -- ** In 'Maybe'
         , tryAdd, trySub, tryMul
           -- ** Checked
         , chkAdd, chkSub, chkMul
           -- ** Modular arithmetic
         , modAdd, modSub, modMul, modNegate
           -- ** Miscellaneous
         , divModFin
         , complementFin, twice, half, quarter
         , crossFin
           -- * Attenuations
         , attLT, attPlus, attMinus, attInt
           -- * Unsafe, fast
         , unsafeFin, unsafePred, unsafeSucc, unsafeCoFin, unsafeCoInt
         ) where

import Control.DeepSeq (NFData(rnf))
import Data.Coerce (coerce)
import Data.Data (Data)
import Data.Maybe (mapMaybe)
import Data.Type.Coercion (Coercion(..))
import GHC.Stack (HasCallStack, withFrozenCallStack)
import GHC.TypeNats
         ( type (*), type (+), type (-), type (<=)
         , Nat, KnownNat
         )

import Data.Default.Class (Default(..))
import Data.Portray (Portray)
import Data.Portray.Diff (Diff)
import Data.Type.Attenuation
         ( Attenuation, coercible
#if MIN_VERSION_attenuation(0, 2, 0)
         , Attenuable(..)
#endif
         )
import Test.QuickCheck (Arbitrary(..), arbitraryBoundedEnum)

import Data.SInt (SInt, unSInt, sintVal)

-- We could use representation type Integer.
-- We use Int since this is likely to be the most efficient type,
-- partly because it's the natural word size for the machine, but also
-- because it's the type used to index into containers such as Data.Vector.
type FinRep = Int

-- | Naturals bounded above by @n@.
newtype Fin (n :: Nat) = Fin FinRep
  deriving (Fin n -> Fin n -> Bool
forall (n :: Nat). Fin n -> Fin n -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Fin n -> Fin n -> Bool
$c/= :: forall (n :: Nat). Fin n -> Fin n -> Bool
== :: Fin n -> Fin n -> Bool
$c== :: forall (n :: Nat). Fin n -> Fin n -> Bool
Eq, Fin n -> Fin n -> Bool
Fin n -> Fin n -> Ordering
Fin n -> Fin n -> Fin n
forall (n :: Nat). Eq (Fin n)
forall (n :: Nat). Fin n -> Fin n -> Bool
forall (n :: Nat). Fin n -> Fin n -> Ordering
forall (n :: Nat). Fin n -> Fin n -> Fin n
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Fin n -> Fin n -> Fin n
$cmin :: forall (n :: Nat). Fin n -> Fin n -> Fin n
max :: Fin n -> Fin n -> Fin n
$cmax :: forall (n :: Nat). Fin n -> Fin n -> Fin n
>= :: Fin n -> Fin n -> Bool
$c>= :: forall (n :: Nat). Fin n -> Fin n -> Bool
> :: Fin n -> Fin n -> Bool
$c> :: forall (n :: Nat). Fin n -> Fin n -> Bool
<= :: Fin n -> Fin n -> Bool
$c<= :: forall (n :: Nat). Fin n -> Fin n -> Bool
< :: Fin n -> Fin n -> Bool
$c< :: forall (n :: Nat). Fin n -> Fin n -> Bool
compare :: Fin n -> Fin n -> Ordering
$ccompare :: forall (n :: Nat). Fin n -> Fin n -> Ordering
Ord, Fin n -> DataType
Fin n -> Constr
forall {n :: Nat}. KnownNat n => Typeable (Fin n)
forall (n :: Nat). KnownNat n => Fin n -> DataType
forall (n :: Nat). KnownNat n => Fin n -> Constr
forall (n :: Nat).
KnownNat n =>
(forall b. Data b => b -> b) -> Fin n -> Fin n
forall (n :: Nat) u.
KnownNat n =>
Int -> (forall d. Data d => d -> u) -> Fin n -> u
forall (n :: Nat) u.
KnownNat n =>
(forall d. Data d => d -> u) -> Fin n -> [u]
forall (n :: Nat) r r'.
KnownNat n =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Fin n -> r
forall (n :: Nat) r r'.
KnownNat n =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Fin n -> r
forall (n :: Nat) (m :: Type -> Type).
(KnownNat n, Monad m) =>
(forall d. Data d => d -> m d) -> Fin n -> m (Fin n)
forall (n :: Nat) (m :: Type -> Type).
(KnownNat n, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Fin n -> m (Fin n)
forall (n :: Nat) (c :: Type -> Type).
KnownNat n =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Fin n)
forall (n :: Nat) (c :: Type -> Type).
KnownNat n =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Fin n -> c (Fin n)
forall (n :: Nat) (t :: Type -> Type) (c :: Type -> Type).
(KnownNat n, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Fin n))
forall (n :: Nat) (t :: Type -> Type -> Type) (c :: Type -> Type).
(KnownNat n, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Fin n))
forall a.
Typeable a
-> (forall (c :: Type -> Type).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: Type -> Type).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: Type -> Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: Type -> Type).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Fin n)
forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Fin n -> c (Fin n)
gmapMo :: forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Fin n -> m (Fin n)
$cgmapMo :: forall (n :: Nat) (m :: Type -> Type).
(KnownNat n, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Fin n -> m (Fin n)
gmapMp :: forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Fin n -> m (Fin n)
$cgmapMp :: forall (n :: Nat) (m :: Type -> Type).
(KnownNat n, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Fin n -> m (Fin n)
gmapM :: forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d) -> Fin n -> m (Fin n)
$cgmapM :: forall (n :: Nat) (m :: Type -> Type).
(KnownNat n, Monad m) =>
(forall d. Data d => d -> m d) -> Fin n -> m (Fin n)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Fin n -> u
$cgmapQi :: forall (n :: Nat) u.
KnownNat n =>
Int -> (forall d. Data d => d -> u) -> Fin n -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Fin n -> [u]
$cgmapQ :: forall (n :: Nat) u.
KnownNat n =>
(forall d. Data d => d -> u) -> Fin n -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Fin n -> r
$cgmapQr :: forall (n :: Nat) r r'.
KnownNat n =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Fin n -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Fin n -> r
$cgmapQl :: forall (n :: Nat) r r'.
KnownNat n =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Fin n -> r
gmapT :: (forall b. Data b => b -> b) -> Fin n -> Fin n
$cgmapT :: forall (n :: Nat).
KnownNat n =>
(forall b. Data b => b -> b) -> Fin n -> Fin n
dataCast2 :: forall (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Fin n))
$cdataCast2 :: forall (n :: Nat) (t :: Type -> Type -> Type) (c :: Type -> Type).
(KnownNat n, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Fin n))
dataCast1 :: forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Fin n))
$cdataCast1 :: forall (n :: Nat) (t :: Type -> Type) (c :: Type -> Type).
(KnownNat n, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Fin n))
dataTypeOf :: Fin n -> DataType
$cdataTypeOf :: forall (n :: Nat). KnownNat n => Fin n -> DataType
toConstr :: Fin n -> Constr
$ctoConstr :: forall (n :: Nat). KnownNat n => Fin n -> Constr
gunfold :: forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Fin n)
$cgunfold :: forall (n :: Nat) (c :: Type -> Type).
KnownNat n =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Fin n)
gfoldl :: forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Fin n -> c (Fin n)
$cgfoldl :: forall (n :: Nat) (c :: Type -> Type).
KnownNat n =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Fin n -> c (Fin n)
Data)
  -- Fin Read/Show behave like other numeric newtypes: drop the \"Fin\".
  deriving newtype (Int -> Fin n -> ShowS
[Fin n] -> ShowS
Fin n -> String
forall (n :: Nat). Int -> Fin n -> ShowS
forall (n :: Nat). [Fin n] -> ShowS
forall (n :: Nat). Fin n -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Fin n] -> ShowS
$cshowList :: forall (n :: Nat). [Fin n] -> ShowS
show :: Fin n -> String
$cshow :: forall (n :: Nat). Fin n -> String
showsPrec :: Int -> Fin n -> ShowS
$cshowsPrec :: forall (n :: Nat). Int -> Fin n -> ShowS
Show, [Fin n] -> Portrayal
Fin n -> Portrayal
forall (n :: Nat). [Fin n] -> Portrayal
forall (n :: Nat). Fin n -> Portrayal
forall a. (a -> Portrayal) -> ([a] -> Portrayal) -> Portray a
portrayList :: [Fin n] -> Portrayal
$cportrayList :: forall (n :: Nat). [Fin n] -> Portrayal
portray :: Fin n -> Portrayal
$cportray :: forall (n :: Nat). Fin n -> Portrayal
Portray, Fin n -> Fin n -> Maybe Portrayal
forall (n :: Nat). Fin n -> Fin n -> Maybe Portrayal
forall a. (a -> a -> Maybe Portrayal) -> Diff a
diff :: Fin n -> Fin n -> Maybe Portrayal
$cdiff :: forall (n :: Nat). Fin n -> Fin n -> Maybe Portrayal
Diff)

-- Prevent 'Coercible' across 'Fin's of different bounds.
--
-- For the safe direction, we have 'Attenuable' instead.
type role Fin nominal

-- | Constraint synonym for naturals @n@ s.t. @'Fin' n@ is inhabited.
type FinSize n = (KnownNat n, 1 <= n)

instance KnownNat n => Read (Fin n) where
  readsPrec :: Int -> ReadS (Fin n)
readsPrec Int
p String
s =
    forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\ (Integer
x, String
s') -> (,String
s') forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (n :: Nat). Integral a => SInt n -> a -> Maybe (Fin n)
tryFin forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal Integer
x) forall a b. (a -> b) -> a -> b
$
    forall a. Read a => Int -> ReadS a
readsPrec @Integer Int
p String
s

instance FinSize n => Arbitrary (Fin n) where
  arbitrary :: Gen (Fin n)
arbitrary = forall a. (Bounded a, Enum a) => Gen a
arbitraryBoundedEnum

instance NFData (Fin n) where rnf :: Fin n -> ()
rnf (Fin Int
x) = forall a. NFData a => a -> ()
rnf Int
x

#if MIN_VERSION_attenuation(0,2,0)
instance Attenuable (Fin n) Int
instance m <= n => Attenuable (Fin m) (Fin n)
#endif

-- | Construct a 'Fin' from an 'Int', with bounds checks.
{-# INLINE fin #-}
fin :: HasCallStack => SInt n -> Int -> Fin n
fin :: forall (n :: Nat). HasCallStack => SInt n -> Int -> Fin n
fin (forall (n :: Nat). SInt n -> Int
unSInt -> !Int
n) Int
i
  | Int
i forall a. Ord a => a -> a -> Bool
<  Int
0 = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Fin: number out of range " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
" < 0"
  | Int
i forall a. Ord a => a -> a -> Bool
>= Int
n = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Fin: number out of range " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
" >= " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n
  | Bool
otherwise = forall (n :: Nat). Int -> Fin n
Fin Int
i

-- | Generalized 'fin' that works on any 'Integral' type.
{-# INLINE finFromIntegral #-}
finFromIntegral
  :: (HasCallStack, Integral a, Show a)
  => SInt n -> a -> Fin n
finFromIntegral :: forall a (n :: Nat).
(HasCallStack, Integral a, Show a) =>
SInt n -> a -> Fin n
finFromIntegral SInt n
n =
  -- We make sure to do the comparisons in a large integer type (namely FinRep)
  -- rather than something like Fin. Otherwise we'd always fail in the
  -- conversion @fin :: Fin 3 -> Fin 4@.
  forall (n :: Nat). HasCallStack => SInt n -> Int -> Fin n
fin SInt n
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral

{-# INLINE ufin #-}
ufin :: HasCallStack => SInt n -> FinRep -> Fin n
ufin :: forall (n :: Nat). HasCallStack => SInt n -> Int -> Fin n
ufin SInt n
sn Int
i
  | Int
i forall a. Ord a => a -> a -> Bool
>= Int
n = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Fin: number out of range " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
" >= " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n
  | Bool
otherwise = forall (n :: Nat). Int -> Fin n
Fin Int
i
 where
  n :: Int
n = forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn

-- | Like 'fin', but doesn't do any bounds checks. However, unlike
-- 'unsafeFin', this is safe (by virtue of the type constraints).
knownFin :: (i <= n - 1) => SInt i -> Fin n
knownFin :: forall (i :: Nat) (n :: Nat). (i <= (n - 1)) => SInt i -> Fin n
knownFin = forall a (n :: Nat). Integral a => a -> Fin n
unsafeFin forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). SInt n -> Int
unSInt
{-# INLINE knownFin #-}

-- | Like 'fin', but doesn't do any bounds checks.
{-# INLINE unsafeFin #-}
unsafeFin :: Integral a => a -> Fin n
unsafeFin :: forall a (n :: Nat). Integral a => a -> Fin n
unsafeFin = forall (n :: Nat). Int -> Fin n
Fin forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral

-- | Convert a number to a @Fin@, or @Nothing@ if out of range.
tryFin :: Integral a => SInt n -> a -> Maybe (Fin n)
tryFin :: forall a (n :: Nat). Integral a => SInt n -> a -> Maybe (Fin n)
tryFin SInt n
n a
x =
  if a
x forall a. Ord a => a -> a -> Bool
>= a
0 Bool -> Bool -> Bool
&& a
x forall a. Ord a => a -> a -> Bool
< forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Nat). SInt n -> Int
unSInt SInt n
n)
    then forall a. a -> Maybe a
Just (forall (n :: Nat). Int -> Fin n
Fin (forall a b. (Integral a, Num b) => a -> b
fromIntegral a
x))
    else forall a. Maybe a
Nothing

-- | @finMod \@n x@ is equivalent to @fin \@n (x `mod` (valueOf \@n))@
--
-- This raises an exception iff @n ~ 0@.  It could have been written with a
-- @0 < n@ constraint instead, but that would be annoying to prove repeatedly.
finMod :: forall n a . (HasCallStack, Integral a) => SInt n -> a -> Fin n
finMod :: forall (n :: Nat) a.
(HasCallStack, Integral a) =>
SInt n -> a -> Fin n
finMod SInt n
n = forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat) a.
(HasCallStack, Integral a) =>
SInt n -> a -> (a, Fin n)
finDivMod SInt n
n

-- | Decompose a number into a component modulo @n@ and the rest.
--
-- This raises an exception iff @n ~ 0@.  See 'finMod'.
finDivMod
  :: forall n a
   . (HasCallStack, Integral a)
  => SInt n -> a -> (a, Fin n)
finDivMod :: forall (n :: Nat) a.
(HasCallStack, Integral a) =>
SInt n -> a -> (a, Fin n)
finDivMod SInt n
sn a
x
  | Integer
n forall a. Eq a => a -> a -> Bool
== Integer
0 = forall a. HasCallStack => String -> a
error String
"finDivMod: zero modulus."
  | Bool
otherwise = (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
d, forall (n :: Nat). Int -> Fin n
Fin (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
m))
 where
  -- Do arithmetic in Integer because some types we could get for @a@ can't
  -- represent @valueOf @n@ (specifically, @Fin m@ with m <= n).  We don't use
  -- @FinRep@ because that could make this incorrect for types larger than
  -- @FinRep@.
  (Integer
d, Integer
m) = forall a. Integral a => a -> a -> (a, a)
divMod (forall a b. (Integral a, Num b) => a -> b
fromIntegral a
x :: Integer) Integer
n
  n :: Integer
n = forall a. Integral a => a -> Integer
toInteger forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn

-- | Reverse the order of the values of a 'Fin' type.
complementFin :: SInt n -> Fin n -> Fin n
-- Cannot use (maxBound - x) because it would introduce a spurious (1 <= n)
-- constraint. We're not concerned about the n=0 case here because Fin 0 is
-- uninhabited so x can only ever be bottom. In this case, unsafeFin will
-- briefly create an invalid Fin, but evaluating the subtraction will end up
-- raising the error inside of x, so an invalid Fin can never be returned.
complementFin :: forall (n :: Nat). SInt n -> Fin n -> Fin n
complementFin SInt n
sn Fin n
x = forall a (n :: Nat). Integral a => a -> Fin n
unsafeFin (forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn forall a. Num a => a -> a -> a
- Int
1 forall a. Num a => a -> a -> a
- forall (n :: Nat). Fin n -> Int
finToInt Fin n
x)

-- | Convert a 'Fin' to the underlying 'Int' representing it.
finToInt :: Fin n -> Int
finToInt :: forall (n :: Nat). Fin n -> Int
finToInt (Fin Int
i) = Int
i
{-# INLINE finToInt #-}

-- | (*2), but works even if 2 is out-of-bounds.
twice :: SInt n -> Fin n -> Fin n
twice :: forall (n :: Nat). SInt n -> Fin n -> Fin n
twice SInt n
sn (Fin Int
i) = forall (n :: Nat). HasCallStack => SInt n -> Int -> Fin n
ufin SInt n
sn forall a b. (a -> b) -> a -> b
$ Int
i forall a. Num a => a -> a -> a
* Int
2

-- | Divide by 2, rounding down.
half :: Fin n -> Fin n
half :: forall (n :: Nat). Fin n -> Fin n
half (Fin Int
n) = forall (n :: Nat). Int -> Fin n
Fin (Int
n forall a. Integral a => a -> a -> a
`quot` Int
2)

-- | Divide by 4, rounding down.
quarter :: Fin n -> Fin n
quarter :: forall (n :: Nat). Fin n -> Fin n
quarter (Fin Int
n) = forall (n :: Nat). Int -> Fin n
Fin (Int
n forall a. Integral a => a -> a -> a
`quot` Int
4)

-- | Decrement by 1, without the validity checks of 'pred'.
unsafePred :: Fin n -> Fin n
unsafePred :: forall (n :: Nat). Fin n -> Fin n
unsafePred (Fin Int
x) = forall (n :: Nat). Int -> Fin n
Fin (Int
x forall a. Num a => a -> a -> a
- Int
1)
{-# INLINE unsafePred #-}

-- | Increment by 1, without the validity checks of 'succ'.
unsafeSucc :: Fin n -> Fin n
unsafeSucc :: forall (n :: Nat). Fin n -> Fin n
unsafeSucc (Fin Int
x) = forall (n :: Nat). Int -> Fin n
Fin (Int
x forall a. Num a => a -> a -> a
+ Int
1)
{-# INLINE unsafeSucc #-}

-- Note [Enumerations of Fins]
--
-- Enumerating lists of Fins is implemented by making the corresponding list of
-- Ints and coercing them via @map coerce@. This ensures that these functions
-- are "good list producers" (in the build/foldr fusion sense), by reusing the
-- same property of the Enum instance for Int. Using Fins directly doesn't work
-- (because 0 might be out of range), and coercing the whole list doesn't work
-- either because it interferes with fusion.

-- | Enumerate the entire domain in ascending order. This is equivalent
-- to @enumFrom 0@ or @enumFrom minBound@, but without introducing a
-- spurious @(1 <= n)@ constraint.
enumFin :: SInt n -> [Fin n]
-- See Note [Enumerations of Fins]
enumFin :: forall (n :: Nat). SInt n -> [Fin n]
enumFin SInt n
sn = forall a b. (a -> b) -> [a] -> [b]
map coerce :: forall a b. Coercible a b => a -> b
coerce [Int
0 .. forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn forall a. Num a => a -> a -> a
- Int
1]
{-# INLINE enumFin #-}

-- | Enumerate the entire domain in descending order. This is equivalent
-- to @reverse enumFin@, but without introducing a spurious @(1 <= n)@
-- constraint or breaking list-fusion.
enumFinDown :: SInt n -> [Fin n]
-- See Note [Enumerations of Fins]
enumFinDown :: forall (n :: Nat). SInt n -> [Fin n]
enumFinDown SInt n
sn = forall a b. (a -> b) -> [a] -> [b]
map coerce :: forall a b. Coercible a b => a -> b
coerce [forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn forall a. Num a => a -> a -> a
- Int
1, forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn forall a. Num a => a -> a -> a
- Int
2 .. Int
0]
{-# INLINE enumFinDown #-}

-- | Equivalent to @reverse (enumFromTo 0 x)@ but without introducing
-- a spurious @(1 <= n)@ constraint or breaking list-fusion.
enumDownFrom :: SInt n -> Fin n -> [Fin n]
-- See Note [Enumerations of Fins]
enumDownFrom :: forall (n :: Nat). SInt n -> Fin n -> [Fin n]
enumDownFrom SInt n
_sn (Fin Int
x) = forall a b. (a -> b) -> [a] -> [b]
map coerce :: forall a b. Coercible a b => a -> b
coerce [Int
x, Int
x forall a. Num a => a -> a -> a
- Int
1 .. Int
0]
{-# INLINE enumDownFrom #-}

-- | Equivalent to @reverse (enumFromTo x maxBound)@ but without
-- introducing a spurious @(1 <= n)@ constraint or breaking list-fusion.
enumDownTo :: SInt n -> Fin n -> [Fin n]
-- See Note [Enumerations of Fins]
enumDownTo :: forall (n :: Nat). SInt n -> Fin n -> [Fin n]
enumDownTo SInt n
sn (Fin Int
x) = forall a b. (a -> b) -> [a] -> [b]
map coerce :: forall a b. Coercible a b => a -> b
coerce [forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn forall a. Num a => a -> a -> a
- Int
1, forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn forall a. Num a => a -> a -> a
- Int
2 .. Int
x]
{-# INLINE enumDownTo #-}

-- | Equivalent to @reverse (enumFromTo y x)@ but without introducing
-- a spurious @(1 <= n)@ constraint or breaking list-fusion.
enumDownFromTo :: SInt n -> Fin n -> Fin n -> [Fin n]
-- See Note [Enumerations of Fins]
enumDownFromTo :: forall (n :: Nat). SInt n -> Fin n -> Fin n -> [Fin n]
enumDownFromTo SInt n
_sn (Fin Int
x) (Fin Int
y) = forall a b. (a -> b) -> [a] -> [b]
map coerce :: forall a b. Coercible a b => a -> b
coerce [Int
x, Int
x forall a. Num a => a -> a -> a
- Int
1 .. Int
y]
{-# INLINE enumDownFromTo #-}

instance KnownNat n => Enum (Fin n) where
    pred :: Fin n -> Fin n
pred (Fin Int
x)
        | Int
x forall a. Ord a => a -> a -> Bool
> Int
0     = forall (n :: Nat). Int -> Fin n
Fin (Int
x forall a. Num a => a -> a -> a
- Int
1)
        | Bool
otherwise = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$
            String
"pred @(Fin " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (n :: Nat). SInt n -> Int
unSInt @n forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal) forall a. [a] -> [a] -> [a]
++
            String
"): no predecessor of 0"
    succ :: Fin n -> Fin n
succ (Fin Int
x)
        | Int
x forall a. Ord a => a -> a -> Bool
< Int
n forall a. Num a => a -> a -> a
- Int
1 = forall (n :: Nat). Int -> Fin n
Fin (Int
x forall a. Num a => a -> a -> a
+ Int
1)
        | Bool
otherwise = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$
            String
"succ @(Fin " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n forall a. [a] -> [a] -> [a]
++ String
"): no successor of " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n
        where !n :: Int
n = forall (n :: Nat). SInt n -> Int
unSInt @n forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
    toEnum :: Int -> Fin n
toEnum   = forall (n :: Nat). HasCallStack => SInt n -> Int -> Fin n
fin forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
    fromEnum :: Fin n -> Int
fromEnum = forall (n :: Nat). Fin n -> Int
finToInt
    -- See Note [Enumerations of Fins]
    enumFrom :: Fin n -> [Fin n]
enumFrom       (Fin Int
x)                 =
      forall a b. (a -> b) -> [a] -> [b]
map coerce :: forall a b. Coercible a b => a -> b
coerce [Int
x .. forall (n :: Nat). SInt n -> Int
unSInt @n forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal forall a. Num a => a -> a -> a
- Int
1]
    enumFromThen :: Fin n -> Fin n -> [Fin n]
enumFromThen   (Fin Int
x) (Fin Int
y)         =
      forall a b. (a -> b) -> [a] -> [b]
map coerce :: forall a b. Coercible a b => a -> b
coerce [Int
x, Int
y .. forall (n :: Nat). SInt n -> Int
unSInt @n forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal forall a. Num a => a -> a -> a
- Int
1]
    enumFromTo :: Fin n -> Fin n -> [Fin n]
enumFromTo     (Fin Int
x)         (Fin Int
z) = forall a b. (a -> b) -> [a] -> [b]
map coerce :: forall a b. Coercible a b => a -> b
coerce [Int
x .. Int
z]
    enumFromThenTo :: Fin n -> Fin n -> Fin n -> [Fin n]
enumFromThenTo (Fin Int
x) (Fin Int
y) (Fin Int
z) = forall a b. (a -> b) -> [a] -> [b]
map coerce :: forall a b. Coercible a b => a -> b
coerce [Int
x, Int
y .. Int
z]
    {-# INLINE pred #-}
    {-# INLINE succ #-}
    {-# INLINE toEnum #-}
    {-# INLINE fromEnum #-}
    {-# INLINE enumFrom #-}
    {-# INLINE enumFromThen #-}
    {-# INLINE enumFromTo #-}
    {-# INLINE enumFromThenTo #-}

-- | The minimal value of the given inhabited 'Fin' type (i.e. @0@).
minFin :: 1 <= n => Fin n
minFin :: forall (n :: Nat). (1 <= n) => Fin n
minFin = forall (n :: Nat). Int -> Fin n
Fin Int
0

-- | The maximal value of the given inhabited 'Fin' type (i.e @n - 1@).
maxFin :: 1 <= n => SInt n -> Fin n
maxFin :: forall (n :: Nat). (1 <= n) => SInt n -> Fin n
maxFin SInt n
sn = forall (n :: Nat). Int -> Fin n
Fin (forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn forall a. Num a => a -> a -> a
- Int
1)

instance FinSize n => Bounded (Fin n) where
    minBound :: Fin n
minBound = forall (n :: Nat). (1 <= n) => Fin n
minFin
    maxBound :: Fin n
maxBound = forall (n :: Nat). (1 <= n) => SInt n -> Fin n
maxFin forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
    {-# INLINE minBound #-}
    {-# INLINE maxBound #-}

-- XXX This should have context 1<=n, but that stops deriving from
-- working for types containing a Fin.
instance KnownNat n => Default (Fin n) where
  def :: Fin n
def = forall (n :: Nat). HasCallStack => SInt n -> Int -> Fin n
fin forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal (Int
0 :: FinRep)

overflowedError
  :: forall n a
   . HasCallStack
  => SInt n -> String -> Fin n -> Fin n -> a
overflowedError :: forall (n :: Nat) a.
HasCallStack =>
SInt n -> String -> Fin n -> Fin n -> a
overflowedError SInt n
sn String
nm Fin n
x Fin n
y = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$
  String -> ShowS
showString String
nm forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  String -> ShowS
showString String
" @" forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  forall a. Show a => a -> ShowS
shows (forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  String -> ShowS
showString String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  forall a. Show a => a -> ShowS
shows Fin n
x forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  String -> ShowS
showString String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  forall a. Show a => a -> ShowS
shows Fin n
y forall a b. (a -> b) -> a -> b
$
  String
" overflowed FinRep."

outOfRangeError
  :: forall n a
   . HasCallStack
  => SInt n -> String -> Fin n -> Fin n -> FinRep -> a
outOfRangeError :: forall (n :: Nat) a.
HasCallStack =>
SInt n -> String -> Fin n -> Fin n -> Int -> a
outOfRangeError SInt n
sn String
nm Fin n
x Fin n
y Int
r = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$
  String -> ShowS
showString String
nm forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  String -> ShowS
showString String
" @" forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  forall a. Show a => a -> ShowS
shows (forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  String -> ShowS
showString String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  forall a. Show a => a -> ShowS
shows Fin n
x forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  String -> ShowS
showString String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  forall a. Show a => a -> ShowS
shows Fin n
y forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  String -> ShowS
showString String
" = " forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  forall a. Show a => a -> ShowS
shows Int
r forall a b. (a -> b) -> a -> b
$
  String
" out of range."

add_ :: SInt n -> Fin n -> Fin n -> Maybe (Bool, FinRep)
add_ :: forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Bool, Int)
add_ SInt n
sn = \ (Fin Int
x) (Fin Int
y) ->
  let z :: Int
z = Int
x forall a. Num a => a -> a -> a
+ Int
y
  in  if Int
z forall a. Ord a => a -> a -> Bool
< Int
x
        then forall a. Maybe a
Nothing -- Overflowed Int.
        else forall a. a -> Maybe a
Just (Int
z forall a. Ord a => a -> a -> Bool
< forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn, Int
z)
{-# INLINE add_ #-}

sub_ :: Fin n -> Fin n -> Maybe (Bool, FinRep)
sub_ :: forall (n :: Nat). Fin n -> Fin n -> Maybe (Bool, Int)
sub_ = \ (Fin Int
x) (Fin Int
y) -> let z :: Int
z = Int
x forall a. Num a => a -> a -> a
- Int
y in forall a. a -> Maybe a
Just (Int
z forall a. Ord a => a -> a -> Bool
>= Int
0, Int
z)
{-# INLINE sub_ #-}

mul_ :: SInt n -> Fin n -> Fin n -> Maybe (Bool, FinRep)
mul_ :: forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Bool, Int)
mul_ SInt n
sn = \ (Fin Int
x) (Fin Int
y) ->
  let z :: Int
z = Int
x forall a. Num a => a -> a -> a
* Int
y
  in  if Int
x forall a. Eq a => a -> a -> Bool
/= Int
0 Bool -> Bool -> Bool
&& Int
z forall a. Integral a => a -> a -> a
`div` Int
x forall a. Eq a => a -> a -> Bool
/= Int
y
        then forall a. Maybe a
Nothing -- Overflowed Int.
        else forall a. a -> Maybe a
Just (Int
z forall a. Ord a => a -> a -> Bool
< forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn, Int
z)
{-# INLINE mul_ #-}

mkMod
  :: HasCallStack
  => SInt n
  -> String
  -> (Fin n -> Fin n -> Maybe (Bool, FinRep)) -> Fin n -> Fin n -> Fin n
mkMod :: forall (n :: Nat).
HasCallStack =>
SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n
mkMod SInt n
sn String
nm Fin n -> Fin n -> Maybe (Bool, Int)
op = \ Fin n
x Fin n
y -> case Fin n
x Fin n -> Fin n -> Maybe (Bool, Int)
`op` Fin n
y of
  Just (Bool
_ok, Int
z) -> forall (n :: Nat) a.
(HasCallStack, Integral a) =>
SInt n -> a -> Fin n
finMod SInt n
sn Int
z
  Maybe (Bool, Int)
Nothing       -> forall (n :: Nat) a.
HasCallStack =>
SInt n -> String -> Fin n -> Fin n -> a
overflowedError SInt n
sn String
nm Fin n
x Fin n
y
{-# INLINE mkMod #-}

-- TODO(awpr): it's possible to implement 'modAdd' and 'modSub' without
-- partiality, but it'd be slower.  We should probably improve this somehow.

-- | Add modulo /n/.
--
-- Raises error when intermediate results overflow Int.
modAdd :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n
modAdd :: forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
modAdd SInt n
sn = forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack forall (n :: Nat).
HasCallStack =>
SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n
mkMod SInt n
sn String
"modAdd" (forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Bool, Int)
add_ SInt n
sn)
{-# INLINEABLE modAdd #-}

-- | Subtract modulo /n/.
modSub :: SInt n -> Fin n -> Fin n -> Fin n
-- Cannot fail, so no HasCallStack.
modSub :: forall (n :: Nat). SInt n -> Fin n -> Fin n -> Fin n
modSub SInt n
sn = forall (n :: Nat).
HasCallStack =>
SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n
mkMod SInt n
sn String
"modSub" forall (n :: Nat). Fin n -> Fin n -> Maybe (Bool, Int)
sub_
{-# INLINEABLE modSub #-}

-- | Multiply modulo /n/.
--
-- Raises error when intermediate results overflow Int.
modMul :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n
modMul :: forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
modMul SInt n
sn = forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack forall (n :: Nat).
HasCallStack =>
SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n
mkMod SInt n
sn String
"modMul" (forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Bool, Int)
mul_ SInt n
sn)
{-# INLINEABLE modMul #-}

-- | Negate modulo /n/.
--
-- Compared to 'complementFin', this is shifted by 1:
-- @complementFin 0 :: Fin n = n - 1@, while @modNegate 0 :: Fin n = 0@.
modNegate :: SInt n -> Fin n -> Fin n
modNegate :: forall (n :: Nat). SInt n -> Fin n -> Fin n
modNegate SInt n
_  (Fin Int
0) = forall (n :: Nat). Int -> Fin n
Fin Int
0
modNegate SInt n
sn (Fin Int
x) = forall (n :: Nat). Int -> Fin n
Fin (forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn forall a. Num a => a -> a -> a
- Int
x)

mkTry
  :: (Fin n -> Fin n -> Maybe (Bool, FinRep))
  -> Fin n -> Fin n -> Maybe (Fin n)
mkTry :: forall (n :: Nat).
(Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n -> Fin n -> Maybe (Fin n)
mkTry Fin n -> Fin n -> Maybe (Bool, Int)
op = \Fin n
x Fin n
y -> case Fin n -> Fin n -> Maybe (Bool, Int)
op Fin n
x Fin n
y of
  Just (Bool
True, Int
z) -> forall a. a -> Maybe a
Just (forall (n :: Nat). Int -> Fin n
Fin Int
z)
  Maybe (Bool, Int)
_              -> forall a. Maybe a
Nothing
{-# INLINE mkTry #-}

-- | Add, returning Nothing for out-of-range results.
tryAdd :: SInt n -> Fin n -> Fin n -> Maybe (Fin n)
tryAdd :: forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Fin n)
tryAdd = forall (n :: Nat).
(Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n -> Fin n -> Maybe (Fin n)
mkTry forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Bool, Int)
add_
{-# INLINEABLE tryAdd #-}

-- | Subtract, returning Nothing for out-of-range results.
trySub :: Fin n -> Fin n -> Maybe (Fin n)
trySub :: forall (n :: Nat). Fin n -> Fin n -> Maybe (Fin n)
trySub = forall (n :: Nat).
(Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n -> Fin n -> Maybe (Fin n)
mkTry forall (n :: Nat). Fin n -> Fin n -> Maybe (Bool, Int)
sub_
{-# INLINEABLE trySub #-}

-- | Multiply, returning Nothing for out-of-range results.
tryMul :: SInt n -> Fin n -> Fin n -> Maybe (Fin n)
tryMul :: forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Fin n)
tryMul = forall (n :: Nat).
(Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n -> Fin n -> Maybe (Fin n)
mkTry forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Bool, Int)
mul_
{-# INLINEABLE tryMul #-}

-- | Split a 'Fin' of the form @d*x + y@ into @(x, y)@.
divModFin :: SInt m -> Fin (d * m) -> (Fin d, Fin m)
divModFin :: forall (m :: Nat) (d :: Nat).
SInt m -> Fin (d * m) -> (Fin d, Fin m)
divModFin SInt m
sm (Fin Int
x) = (forall (n :: Nat). Int -> Fin n
Fin Int
d, forall (n :: Nat). Int -> Fin n
Fin Int
r)
 where
  (Int
d, Int
r) = forall a. Integral a => a -> a -> (a, a)
divMod Int
x (forall (n :: Nat). SInt n -> Int
unSInt SInt m
sm)
{-# INLINEABLE divModFin #-}

mkChk
  :: HasCallStack
  => SInt n
  -> String
  -> (Fin n -> Fin n -> Maybe (Bool, FinRep))
  -> Fin n -> Fin n -> Fin n
mkChk :: forall (n :: Nat).
HasCallStack =>
SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n
mkChk SInt n
sn String
nm Fin n -> Fin n -> Maybe (Bool, Int)
op = \Fin n
x Fin n
y -> case Fin n -> Fin n -> Maybe (Bool, Int)
op Fin n
x Fin n
y of
  Just (Bool
ok, Int
z) -> if Bool
ok then forall (n :: Nat). Int -> Fin n
Fin Int
z else forall (n :: Nat) a.
HasCallStack =>
SInt n -> String -> Fin n -> Fin n -> Int -> a
outOfRangeError SInt n
sn String
nm Fin n
x Fin n
y Int
z
  Maybe (Bool, Int)
Nothing -> forall (n :: Nat) a.
HasCallStack =>
SInt n -> String -> Fin n -> Fin n -> a
overflowedError SInt n
sn String
nm Fin n
x Fin n
y
{-# INLINE mkChk #-}

-- | Add and assert the result is in-range.
chkAdd :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n
chkAdd :: forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
chkAdd SInt n
sn = forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack forall (n :: Nat).
HasCallStack =>
SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n
mkChk SInt n
sn String
"chkAdd" (forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Bool, Int)
add_ SInt n
sn)
{-# INLINEABLE chkAdd #-}

-- | Subtract and assert the result is in-range.
chkSub :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n
chkSub :: forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
chkSub SInt n
sn = forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack forall (n :: Nat).
HasCallStack =>
SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n
mkChk SInt n
sn String
"chkSub" forall (n :: Nat). Fin n -> Fin n -> Maybe (Bool, Int)
sub_
{-# INLINEABLE chkSub #-}

-- | Multiply and assert the result is in-range.
chkMul :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n
chkMul :: forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
chkMul SInt n
sn = forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack forall (n :: Nat).
HasCallStack =>
SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n
mkChk SInt n
sn String
"chkMul" (forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Bool, Int)
mul_ SInt n
sn)
{-# INLINEABLE chkMul #-}

-- | Restricted coercion to larger Fin types.
--
-- This is also available as an 'Attenuable' instance.
attLT :: (n <= m) => Attenuation (Fin n) (Fin m)
attLT :: forall (m :: Nat) (n :: Nat).
(m <= n) =>
Attenuation (Fin m) (Fin n)
attLT = forall {k} (a :: k) (b :: k). Coercible a b => Attenuation a b
coercible

-- | Restricted coercion to larger Fin types.
attPlus :: Attenuation (Fin n) (Fin (n + k))
attPlus :: forall (n :: Nat) (k :: Nat). Attenuation (Fin n) (Fin (n + k))
attPlus = forall {k} (a :: k) (b :: k). Coercible a b => Attenuation a b
coercible

-- | Restricted coercion to larger Fin types.
attMinus :: Attenuation (Fin (n - k)) (Fin n)
attMinus :: forall (n :: Nat) (k :: Nat). Attenuation (Fin (n - k)) (Fin n)
attMinus = forall {k} (a :: k) (b :: k). Coercible a b => Attenuation a b
coercible

-- | Restricted coercion to Int.
--
-- This is also available as an 'Attenuable' instance.
attInt :: Attenuation (Fin n) Int
attInt :: forall (n :: Nat). Attenuation (Fin n) Int
attInt = forall {k} (a :: k) (b :: k). Coercible a b => Attenuation a b
coercible

-- | Unsafe coercion between any Fin types.
unsafeCoFin :: Coercion (Fin n) (Fin m)
unsafeCoFin :: forall (n :: Nat) (m :: Nat). Coercion (Fin n) (Fin m)
unsafeCoFin = forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion

-- | Unsafe coercion to and from Int.
unsafeCoInt :: Coercion (Fin n) Int
unsafeCoInt :: forall (n :: Nat). Coercion (Fin n) Int
unsafeCoInt = forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion

-- | 'embed' increasing the bound by exactly one.
weaken :: Fin n -> Fin (n+1)
weaken :: forall (n :: Nat). Fin n -> Fin (n + 1)
weaken (Fin Int
x) = forall (n :: Nat). Int -> Fin n
Fin Int
x

-- | Shrink the bound by one if possible.
strengthen :: SInt n -> Fin (n+1) -> Maybe (Fin n)
strengthen :: forall (n :: Nat). SInt n -> Fin (n + 1) -> Maybe (Fin n)
strengthen SInt n
sn (Fin Int
x) = if Int
x forall a. Eq a => a -> a -> Bool
== forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn then forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just (forall (n :: Nat). Int -> Fin n
Fin Int
x)

-- | 'shiftFin' increases the value and bound of a Fin both by @m@.
shiftFin :: SInt m -> Fin n -> Fin (m+n)
shiftFin :: forall (m :: Nat) (n :: Nat). SInt m -> Fin n -> Fin (m + n)
shiftFin SInt m
sm (Fin Int
x) = forall (n :: Nat). Int -> Fin n
Fin (forall (n :: Nat). SInt n -> Int
unSInt SInt m
sm forall a. Num a => a -> a -> a
+ Int
x)

-- | 'tryUnshiftFin' decreases the value and bound of a Fin both by @m@.
tryUnshiftFin :: SInt m -> SInt n -> Fin (m+n) -> Maybe (Fin n)
tryUnshiftFin :: forall (m :: Nat) (n :: Nat).
SInt m -> SInt n -> Fin (m + n) -> Maybe (Fin n)
tryUnshiftFin SInt m
sm SInt n
sn (Fin Int
x) = forall a (n :: Nat). Integral a => SInt n -> a -> Maybe (Fin n)
tryFin SInt n
sn (Int
x forall a. Num a => a -> a -> a
- forall (n :: Nat). SInt n -> Int
unSInt SInt m
sm)

-- | 'unshiftFin' decreases the value and bound of a Fin both by @m@.
--
-- Raises an exception if the result would be negative.
unshiftFin :: HasCallStack => SInt m -> SInt n -> Fin (m+n) -> Fin n
unshiftFin :: forall (m :: Nat) (n :: Nat).
HasCallStack =>
SInt m -> SInt n -> Fin (m + n) -> Fin n
unshiftFin SInt m
sm SInt n
sn (Fin Int
x) = forall (n :: Nat). HasCallStack => SInt n -> Int -> Fin n
fin SInt n
sn (Int
x forall a. Num a => a -> a -> a
- forall (n :: Nat). SInt n -> Int
unSInt SInt m
sm)

-- | Deconstructs the given Fin into one of two cases depending where it lies
-- in the given range.
splitFin :: SInt m -> Fin (m + n) -> Either (Fin m) (Fin n)
splitFin :: forall (m :: Nat) (n :: Nat).
SInt m -> Fin (m + n) -> Either (Fin m) (Fin n)
splitFin SInt m
sm (Fin Int
x)
  | Int
x forall a. Ord a => a -> a -> Bool
< forall (n :: Nat). SInt n -> Int
unSInt SInt m
sm = forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). Int -> Fin n
Fin Int
x
  | Bool
otherwise     = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). Int -> Fin n
Fin (Int
x forall a. Num a => a -> a -> a
- forall (n :: Nat). SInt n -> Int
unSInt SInt m
sm)

-- | The inverse of 'splitFin'.
concatFin :: SInt m -> Either (Fin m) (Fin n) -> Fin (m + n)
concatFin :: forall (m :: Nat) (n :: Nat).
SInt m -> Either (Fin m) (Fin n) -> Fin (m + n)
concatFin SInt m
sm Either (Fin m) (Fin n)
e = case Either (Fin m) (Fin n)
e of
  Left (Fin Int
x) -> forall (n :: Nat). Int -> Fin n
Fin Int
x
  Right Fin n
x -> forall (m :: Nat) (n :: Nat). SInt m -> Fin n -> Fin (m + n)
shiftFin SInt m
sm Fin n
x

-- | Convert to a 'Fin' with a larger bound.
--
-- This is equivalent to a specialization of 'Data.Type.Attenuation.attenuate'.
{-# INLINE embed #-}
embed :: (m <= n) => Fin m -> Fin n
embed :: forall (m :: Nat) (n :: Nat). (m <= n) => Fin m -> Fin n
embed (Fin Int
i) = forall (n :: Nat). Int -> Fin n
Fin Int
i

-- | Convert to a 'Fin' with a (potentially) smaller bound.
--
-- This function throws an exception if the number is out of range of the
-- target type.
{-# INLINE unembed #-}
unembed :: HasCallStack => SInt n -> Fin m -> Fin n
unembed :: forall (n :: Nat) (m :: Nat).
HasCallStack =>
SInt n -> Fin m -> Fin n
unembed SInt n
sn (Fin Int
i) = forall (n :: Nat). HasCallStack => SInt n -> Int -> Fin n
ufin SInt n
sn Int
i

-- | Convert to a 'Fin' with a (potentially) smaller bound.
--
-- Returns 'Nothing' if the number is out of range of the target type.
tryUnembed :: SInt n -> Fin m -> Maybe (Fin n)
tryUnembed :: forall (n :: Nat) (m :: Nat). SInt n -> Fin m -> Maybe (Fin n)
tryUnembed SInt n
sn (Fin Int
i) = forall a (n :: Nat). Integral a => SInt n -> a -> Maybe (Fin n)
tryFin SInt n
sn Int
i

-- | Given two 'Fin's, returns one the size of the inputs' cartesian product.
--
-- The second argument is the lower-order one, i.e.
--
-- > crossFin @_ @n (x+1) y = n + crossFin @_ @n x y
-- > crossFin @_ @n x (y+1) = 1 + crossFin @_ @n x y
crossFin :: SInt n -> Fin m -> Fin n -> Fin (m * n)
crossFin :: forall (n :: Nat) (m :: Nat).
SInt n -> Fin m -> Fin n -> Fin (m * n)
crossFin SInt n
sn (Fin Int
x) (Fin Int
y) = forall (n :: Nat). Int -> Fin n
Fin (Int
x forall a. Num a => a -> a -> a
* forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn forall a. Num a => a -> a -> a
+ Int
y)