{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UnboxedTuples #-}

module Arithmetic.Fin
  ( -- * Modification
    incrementL
  , incrementL#
  , incrementR
  , incrementR#
  , weaken
  , weaken#
  , weakenL
  , weakenL#
  , weakenR
  , weakenR#
  , succ
  , succ#

    -- * Traverse

    -- | These use the terms @ascend@ and @descend@ rather than the
    -- more popular @l@ (left) and @r@ (right) that pervade the Haskell
    -- ecosystem. The general rule is that ascending functions pair
    -- the initial accumulator with zero with descending functions
    -- pair the initial accumulator with the last index.
  , ascend
  , ascend'
  , ascendFrom'
  , ascendFrom'#
  , ascendM
  , ascendM#
  , ascendM_
  , ascendM_#
  , ascendFromToM_#
  , descend
  , descend#
  , descend'
  , descendM
  , descendM_
  , ascending
  , descending
  , ascendingSlice
  , descendingSlice

    -- * Absurdities
  , absurd

    -- * Demote
  , demote
  , demote#
  , demote32#

    -- * Deconstruct
  , with
  , with#

    -- * Construct
  , construct#
  , nativeTo32#
  , nativeFrom32#
  , remInt#
  , remWord#
  , fromInt
  , fromInt#
  , constant#
  , greatest#

    -- * Compare
  , equals#

    -- * Substitute Bound
  , substitute#

    -- * Lift and Unlift
  , lift
  , unlift
  ) where

import Prelude hiding (last, succ)

import Arithmetic.Nat ((<?),(<?#))
import Arithmetic.Types (Difference (..), Fin (..), Nat, Nat#, pattern MaybeFinJust#, pattern MaybeFinNothing#, type (:=:), type (<), type (<#), type (<=), (:=:#))
import Arithmetic.Types (type (<=#))
import Arithmetic.Unsafe (Fin# (Fin#), MaybeFin#, Nat# (Nat#), Fin32#(Fin32#))
import Data.Maybe.Void (pattern JustVoid#)
import GHC.Exts (Int (I#), Int32#, Int#, Word#, (+#), (==#))
import GHC.TypeNats (CmpNat, type (+))

import qualified Arithmetic.Equal as Eq
import qualified Arithmetic.Lt as Lt
import qualified Arithmetic.Lte as Lte
import qualified Arithmetic.Nat as Nat
import qualified Arithmetic.Plus as Plus
import qualified Arithmetic.Unsafe as Unsafe
import qualified GHC.Exts as Exts
import qualified GHC.TypeNats as GHC

{- | Raise the index by @m@ and weaken the bound by @m@, adding
@m@ to the right-hand side of @n@.
-}
incrementR :: forall n m. Nat m -> Fin n -> Fin (n + m)
{-# INLINE incrementR #-}
incrementR :: forall (n :: Nat) (m :: Nat). Nat m -> Fin n -> Fin (n + m)
incrementR Nat m
m (Fin Nat m
i m < n
pf) = Nat (m + m) -> ((m + m) < (n + m)) -> Fin (n + m)
forall (m :: Nat) (a :: Nat). Nat m -> (m < a) -> Fin a
Fin (Nat m -> Nat m -> Nat (m + m)
forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Nat (a + b)
Nat.plus Nat m
i Nat m
m) (forall (c :: Nat) (a :: Nat) (b :: Nat).
(a < b) -> (a + c) < (b + c)
Lt.incrementR @m m < n
pf)

incrementR# :: forall n m. Nat# m -> Fin# n -> Fin# (n + m)
{-# INLINE incrementR# #-}
incrementR# :: forall (n :: Nat) (m :: Nat). Nat# m -> Fin# n -> Fin# (n + m)
incrementR# (Nat# Int#
n) (Fin# Int#
i) = Int# -> Fin# (n + m)
forall (a :: Nat). Int# -> Fin# a
Fin# (Int#
n Int# -> Int# -> Int#
+# Int#
i)

{- | Raise the index by @m@ and weaken the bound by @m@, adding
@m@ to the left-hand side of @n@.
-}
incrementL :: forall n m. Nat m -> Fin n -> Fin (m + n)
{-# INLINE incrementL #-}
incrementL :: forall (n :: Nat) (m :: Nat). Nat m -> Fin n -> Fin (m + n)
incrementL Nat m
m (Fin Nat m
i m < n
pf) = Nat (m + m) -> ((m + m) < (m + n)) -> Fin (m + n)
forall (m :: Nat) (a :: Nat). Nat m -> (m < a) -> Fin a
Fin (Nat m -> Nat m -> Nat (m + m)
forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Nat (a + b)
Nat.plus Nat m
m Nat m
i) (forall (c :: Nat) (a :: Nat) (b :: Nat).
(a < b) -> (c + a) < (c + b)
Lt.incrementL @m m < n
pf)

incrementL# :: forall n m. Nat# m -> Fin# n -> Fin# (m + n)
{-# INLINE incrementL# #-}
incrementL# :: forall (n :: Nat) (m :: Nat). Nat# m -> Fin# n -> Fin# (m + n)
incrementL# (Nat# Int#
n) (Fin# Int#
i) = Int# -> Fin# (m + n)
forall (a :: Nat). Int# -> Fin# a
Fin# (Int#
n Int# -> Int# -> Int#
+# Int#
i)

{- | Weaken the bound by @m@, adding it to the left-hand side of
the existing bound. This does not change the index.
-}
weakenL :: forall n m. Fin n -> Fin (m + n)
{-# INLINE weakenL #-}
weakenL :: forall (n :: Nat) (m :: Nat). Fin n -> Fin (m + n)
weakenL (Fin Nat m
i m < n
pf) =
  Nat m -> (m < (m + n)) -> Fin (m + n)
forall (m :: Nat) (a :: Nat). Nat m -> (m < a) -> Fin a
Fin
    Nat m
i
    ( ((n + m) :=: (m + n)) -> (m < (n + m)) -> m < (m + n)
forall (b :: Nat) (c :: Nat) (a :: Nat).
(b :=: c) -> (a < b) -> a < c
Lt.substituteR
        (forall (a :: Nat) (b :: Nat). (a + b) :=: (b + a)
Plus.commutative @n @m)
        ((m < n) -> (0 <= m) -> (m + 0) < (n + m)
forall (a :: Nat) (b :: Nat) (c :: Nat) (d :: Nat).
(a < b) -> (c <= d) -> (a + c) < (b + d)
Lt.plus m < n
pf (forall (a :: Nat). 0 <= a
Lte.zero @m))
    )

{- | Unboxed variant of 'weakenL'.
-}
weakenL# :: forall n m. Fin# n -> Fin# (m + n)
{-# INLINE weakenL# #-}
weakenL# :: forall (n :: Nat) (m :: Nat). Fin# n -> Fin# (m + n)
weakenL# (Fin# Int#
i) = Int# -> Fin# (m + n)
forall (a :: Nat). Int# -> Fin# a
Fin# Int#
i

{- | Weaken the bound by @m@, adding it to the right-hand side of
the existing bound. This does not change the index.
-}
weakenR :: forall n m. Fin n -> Fin (n + m)
{-# INLINE weakenR #-}
weakenR :: forall (n :: Nat) (m :: Nat). Fin n -> Fin (n + m)
weakenR (Fin Nat m
i m < n
pf) = Nat m -> (m < (n + m)) -> Fin (n + m)
forall (m :: Nat) (a :: Nat). Nat m -> (m < a) -> Fin a
Fin Nat m
i ((m < n) -> (0 <= m) -> (m + 0) < (n + m)
forall (a :: Nat) (b :: Nat) (c :: Nat) (d :: Nat).
(a < b) -> (c <= d) -> (a + c) < (b + d)
Lt.plus m < n
pf 0 <= m
forall (a :: Nat). 0 <= a
Lte.zero)

{- | Unboxed variant of 'weakenR'.
-}
weakenR# :: forall n m. Fin# n -> Fin# (n + m)
{-# INLINE weakenR# #-}
weakenR# :: forall (n :: Nat) (m :: Nat). Fin# n -> Fin# (n + m)
weakenR# (Fin# Int#
i) = Int# -> Fin# (n + m)
forall (a :: Nat). Int# -> Fin# a
Fin# Int#
i

{- | Weaken the bound, replacing it by another number greater than
or equal to itself. This does not change the index.
-}
weaken :: forall n m. (n <= m) -> Fin n -> Fin m
{-# INLINE weaken #-}
weaken :: forall (n :: Nat) (m :: Nat). (n <= m) -> Fin n -> Fin m
weaken n <= m
lt (Fin Nat m
i m < n
pf) = Nat m -> (m < m) -> Fin m
forall (m :: Nat) (a :: Nat). Nat m -> (m < a) -> Fin a
Fin Nat m
i ((m < n) -> (n <= m) -> m < m
forall (a :: Nat) (b :: Nat) (c :: Nat).
(a < b) -> (b <= c) -> a < c
Lt.transitiveNonstrictR m < n
pf n <= m
lt)

weaken# :: forall n m. (n <=# m) -> Fin# n -> Fin# m
{-# INLINE weaken# #-}
weaken# :: forall (n :: Nat) (m :: Nat). (n <=# m) -> Fin# n -> Fin# m
weaken# n <=# m
_ (Fin# Int#
x) = Int# -> Fin# m
forall (a :: Nat). Int# -> Fin# a
Fin# Int#
x

-- | A finite set of no values is impossible.
absurd :: Fin 0 -> void
{-# INLINE absurd #-}
absurd :: forall void. Fin 0 -> void
absurd (Fin Nat m
_ m < 0
pf) = (m < 0) -> void
forall (n :: Nat) void. (n < 0) -> void
Lt.absurd m < 0
pf

{- | Fold over the numbers bounded by @n@ in descending
order. This is lazy in the accumulator. For convenince,
this differs from @foldr@ in the order of the parameters.

> descend 4 z f = f 0 (f 1 (f 2 (f 3 z)))
-}
descend ::
  forall a n.
  -- | Upper bound
  Nat n ->
  -- | Initial accumulator
  a ->
  -- | Update accumulator
  (Fin n -> a -> a) ->
  a
{-# INLINE descend #-}
descend :: forall a (n :: Nat). Nat n -> a -> (Fin n -> a -> a) -> a
descend !Nat n
n a
b0 Fin n -> a -> a
f = Nat 0 -> a
forall (m :: Nat). Nat m -> a
go Nat 0
Nat.zero
 where
  go :: Nat m -> a
  go :: forall (m :: Nat). Nat m -> a
go !Nat m
m = case Nat m
m Nat m -> Nat n -> Maybe (m < n)
forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Maybe (a < b)
<? Nat n
n of
    Maybe (m < n)
Nothing -> a
b0
    Just m < n
lt -> Fin n -> a -> a
f (Nat m -> (m < n) -> Fin n
forall (m :: Nat) (a :: Nat). Nat m -> (m < a) -> Fin a
Fin Nat m
m m < n
lt) (Nat (m + 1) -> a
forall (m :: Nat). Nat m -> a
go (Nat m -> Nat (m + 1)
forall (a :: Nat). Nat a -> Nat (a + 1)
Nat.succ Nat m
m))

descend# ::
  forall a n.
  -- | Upper bound
  Nat# n ->
  -- | Initial accumulator
  a ->
  -- | Update accumulator
  (Fin# n -> a -> a) ->
  a
{-# INLINE descend# #-}
descend# :: forall a (n :: Nat). Nat# n -> a -> (Fin# n -> a -> a) -> a
descend# !Nat# n
n a
b0 Fin# n -> a -> a
f = Nat n -> a -> (Fin n -> a -> a) -> a
forall a (n :: Nat). Nat n -> a -> (Fin n -> a -> a) -> a
descend (Nat# n -> Nat n
forall (n :: Nat). Nat# n -> Nat n
Nat.lift Nat# n
n) a
b0 (\Fin n
ix a
a -> Fin# n -> a -> a
f (Fin n -> Fin# n
forall (n :: Nat). Fin n -> Fin# n
unlift Fin n
ix) a
a)

{- | Fold over the numbers bounded by @n@ in descending
order. This is strict in the accumulator. For convenince,
this differs from @foldr'@ in the order of the parameters.

> descend 4 z f = f 0 (f 1 (f 2 (f 3 z)))
-}
descend' ::
  forall a n.
  -- | Upper bound
  Nat n ->
  -- | Initial accumulator
  a ->
  -- | Update accumulator
  (Fin n -> a -> a) ->
  a
{-# INLINE descend' #-}
descend' :: forall a (n :: Nat). Nat n -> a -> (Fin n -> a -> a) -> a
descend' !Nat n
n !a
b0 Fin n -> a -> a
f = Nat n -> (n <= n) -> a -> a
forall (p :: Nat). Nat p -> (p <= n) -> a -> a
go Nat n
n n <= n
forall (a :: Nat). a <= a
Lte.reflexive a
b0
 where
  go :: Nat p -> p <= n -> a -> a
  go :: forall (p :: Nat). Nat p -> (p <= n) -> a -> a
go !Nat p
m p <= n
pLteEn !a
b = case Nat p -> Nat 1 -> Maybe (Difference p 1)
forall (a :: Nat) (b :: Nat).
Nat a -> Nat b -> Maybe (Difference a b)
Nat.monus Nat p
m Nat 1
Nat.one of
    Maybe (Difference p 1)
Nothing -> a
b
    Just (Difference (Nat c
mpred :: Nat c) (c + 1) :=: p
cPlusOneEqP) ->
      let !cLtEn :: c < n
cLtEn = ((c + 1) :=: p) -> (p <= n) -> c < n
forall (a :: Nat) (b :: Nat) (c :: Nat).
((a + 1) :=: b) -> (b <= c) -> a < c
descendLemma (c + 1) :=: p
cPlusOneEqP p <= n
pLteEn
       in Nat c -> (c <= n) -> a -> a
forall (p :: Nat). Nat p -> (p <= n) -> a -> a
go Nat c
mpred ((c < n) -> c <= n
forall (a :: Nat) (b :: Nat). (a < b) -> a <= b
Lte.fromStrict c < n
cLtEn) (Fin n -> a -> a
f (Nat c -> (c < n) -> Fin n
forall (m :: Nat) (a :: Nat). Nat m -> (m < a) -> Fin a
Fin Nat c
mpred c < n
cLtEn) a
b)

{- | Fold over the numbers bounded by @n@ in ascending order. This
is lazy in the accumulator.

> ascend 4 z f = f 3 (f 2 (f 1 (f 0 z)))
-}
ascend ::
  forall a n.
  Nat n ->
  a ->
  (Fin n -> a -> a) ->
  a
{-# INLINE ascend #-}
ascend :: forall a (n :: Nat). Nat n -> a -> (Fin n -> a -> a) -> a
ascend !Nat n
n !a
b0 Fin n -> a -> a
f = Nat n -> (n <= n) -> a
forall (p :: Nat). Nat p -> (p <= n) -> a
go Nat n
n n <= n
forall (a :: Nat). a <= a
Lte.reflexive
 where
  go :: Nat p -> (p <= n) -> a
  go :: forall (p :: Nat). Nat p -> (p <= n) -> a
go !Nat p
m p <= n
pLteEn = case Nat p -> Nat 1 -> Maybe (Difference p 1)
forall (a :: Nat) (b :: Nat).
Nat a -> Nat b -> Maybe (Difference a b)
Nat.monus Nat p
m Nat 1
Nat.one of
    Maybe (Difference p 1)
Nothing -> a
b0
    Just (Difference (Nat c
mpred :: Nat c) (c + 1) :=: p
cPlusOneEqP) ->
      let !cLtEn :: c < n
cLtEn = ((c + 1) :=: p) -> (p <= n) -> c < n
forall (a :: Nat) (b :: Nat) (c :: Nat).
((a + 1) :=: b) -> (b <= c) -> a < c
descendLemma (c + 1) :=: p
cPlusOneEqP p <= n
pLteEn
       in Fin n -> a -> a
f (Nat c -> (c < n) -> Fin n
forall (m :: Nat) (a :: Nat). Nat m -> (m < a) -> Fin a
Fin Nat c
mpred c < n
cLtEn) (Nat c -> (c <= n) -> a
forall (p :: Nat). Nat p -> (p <= n) -> a
go Nat c
mpred ((c < n) -> c <= n
forall (a :: Nat) (b :: Nat). (a < b) -> a <= b
Lte.fromStrict c < n
cLtEn))

{- | Strict fold over the numbers bounded by @n@ in ascending
order. For convenince, this differs from @foldl'@ in the
order of the parameters.

> ascend' 4 z f = f 3 (f 2 (f 1 (f 0 z)))
-}
ascend' ::
  forall a n.
  -- | Upper bound
  Nat n ->
  -- | Initial accumulator
  a ->
  -- | Update accumulator
  (Fin n -> a -> a) ->
  a
{-# INLINE ascend' #-}
ascend' :: forall a (n :: Nat). Nat n -> a -> (Fin n -> a -> a) -> a
ascend' !Nat n
n !a
b0 Fin n -> a -> a
f = Nat 0 -> a -> a
forall (m :: Nat). Nat m -> a -> a
go Nat 0
Nat.zero a
b0
 where
  go :: Nat m -> a -> a
  go :: forall (m :: Nat). Nat m -> a -> a
go !Nat m
m !a
b = case Nat m
m Nat m -> Nat n -> Maybe (m < n)
forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Maybe (a < b)
<? Nat n
n of
    Maybe (m < n)
Nothing -> a
b
    Just m < n
lt -> Nat (m + 1) -> a -> a
forall (m :: Nat). Nat m -> a -> a
go (Nat m -> Nat (m + 1)
forall (a :: Nat). Nat a -> Nat (a + 1)
Nat.succ Nat m
m) (Fin n -> a -> a
f (Nat m -> (m < n) -> Fin n
forall (m :: Nat) (a :: Nat). Nat m -> (m < a) -> Fin a
Fin Nat m
m m < n
lt) a
b)

{- | Generalization of @ascend'@ that lets the caller pick the starting index:

> ascend' === ascendFrom' 0
-}
ascendFrom' ::
  forall a m n.
  -- | Index to start at
  Nat m ->
  -- | Number of steps to take
  Nat n ->
  -- | Initial accumulator
  a ->
  -- | Update accumulator
  (Fin (m + n) -> a -> a) ->
  a
{-# INLINE ascendFrom' #-}
ascendFrom' :: forall a (m :: Nat) (n :: Nat).
Nat m -> Nat n -> a -> (Fin (m + n) -> a -> a) -> a
ascendFrom' !Nat m
m0 !Nat n
n !a
b0 Fin (m + n) -> a -> a
f = Nat m -> a -> a
forall (k :: Nat). Nat k -> a -> a
go Nat m
m0 a
b0
 where
  end :: Nat (m + n)
end = Nat m -> Nat n -> Nat (m + n)
forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Nat (a + b)
Nat.plus Nat m
m0 Nat n
n
  go :: Nat k -> a -> a
  go :: forall (k :: Nat). Nat k -> a -> a
go !Nat k
m !a
b = case Nat k
m Nat k -> Nat (m + n) -> Maybe (k < (m + n))
forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Maybe (a < b)
<? Nat (m + n)
end of
    Maybe (k < (m + n))
Nothing -> a
b
    Just k < (m + n)
lt -> Nat (k + 1) -> a -> a
forall (k :: Nat). Nat k -> a -> a
go (Nat k -> Nat (k + 1)
forall (a :: Nat). Nat a -> Nat (a + 1)
Nat.succ Nat k
m) (Fin (m + n) -> a -> a
f (Nat k -> (k < (m + n)) -> Fin (m + n)
forall (m :: Nat) (a :: Nat). Nat m -> (m < a) -> Fin a
Fin Nat k
m k < (m + n)
lt) a
b)

-- | Variant of @ascendFrom'@ with unboxed arguments.
ascendFrom'# ::
  forall a m n.
  -- | Index to start at
  Nat# m ->
  -- | Number of steps to take
  Nat# n ->
  -- | Initial accumulator
  a ->
  -- | Update accumulator
  (Fin# (m + n) -> a -> a) ->
  a
{-# INLINE ascendFrom'# #-}
ascendFrom'# :: forall a (m :: Nat) (n :: Nat).
Nat# m -> Nat# n -> a -> (Fin# (m + n) -> a -> a) -> a
ascendFrom'# !Nat# m
m0 !Nat# n
n !a
b0 Fin# (m + n) -> a -> a
f = Nat m -> Nat n -> a -> (Fin (m + n) -> a -> a) -> a
forall a (m :: Nat) (n :: Nat).
Nat m -> Nat n -> a -> (Fin (m + n) -> a -> a) -> a
ascendFrom' (Nat# m -> Nat m
forall (n :: Nat). Nat# n -> Nat n
Nat.lift Nat# m
m0) (Nat# n -> Nat n
forall (n :: Nat). Nat# n -> Nat n
Nat.lift Nat# n
n) a
b0 (\Fin (m + n)
ix -> Fin# (m + n) -> a -> a
f (Fin (m + n) -> Fin# (m + n)
forall (n :: Nat). Fin n -> Fin# n
unlift Fin (m + n)
ix))

{- | Strict monadic left fold over the numbers bounded by @n@
in ascending order. Roughly:

> ascendM 4 z0 f =
>   f 0 z0 >>= \z1 ->
>   f 1 z1 >>= \z2 ->
>   f 2 z2 >>= \z3 ->
>   f 3 z3
-}
ascendM ::
  forall m a n.
  (Monad m) =>
  -- | Upper bound
  Nat n ->
  -- | Initial accumulator
  a ->
  -- | Update accumulator
  (Fin n -> a -> m a) ->
  m a
{-# INLINE ascendM #-}
ascendM :: forall (m :: * -> *) a (n :: Nat).
Monad m =>
Nat n -> a -> (Fin n -> a -> m a) -> m a
ascendM !Nat n
n !a
b0 Fin n -> a -> m a
f = Nat 0 -> a -> m a
forall (p :: Nat). Nat p -> a -> m a
go Nat 0
Nat.zero a
b0
 where
  go :: Nat p -> a -> m a
  go :: forall (p :: Nat). Nat p -> a -> m a
go !Nat p
m !a
b = case Nat p
m Nat p -> Nat n -> Maybe (p < n)
forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Maybe (a < b)
<? Nat n
n of
    Maybe (p < n)
Nothing -> a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
b
    Just p < n
lt -> Nat (p + 1) -> a -> m a
forall (p :: Nat). Nat p -> a -> m a
go (Nat p -> Nat (p + 1)
forall (a :: Nat). Nat a -> Nat (a + 1)
Nat.succ Nat p
m) (a -> m a) -> m a -> m a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Fin n -> a -> m a
f (Nat p -> (p < n) -> Fin n
forall (m :: Nat) (a :: Nat). Nat m -> (m < a) -> Fin a
Fin Nat p
m p < n
lt) a
b

{- | Variant of @ascendM@ that takes an unboxed Nat and provides
an unboxed Fin to the callback.
-}
ascendM# ::
  forall m a n.
  (Monad m) =>
  -- | Upper bound
  Nat# n ->
  -- | Initial accumulator
  a ->
  -- | Update accumulator
  (Fin# n -> a -> m a) ->
  m a
{-# INLINE ascendM# #-}
ascendM# :: forall (m :: * -> *) a (n :: Nat).
Monad m =>
Nat# n -> a -> (Fin# n -> a -> m a) -> m a
ascendM# Nat# n
n !a
a0 Fin# n -> a -> m a
f = Nat n -> a -> (Fin n -> a -> m a) -> m a
forall (m :: * -> *) a (n :: Nat).
Monad m =>
Nat n -> a -> (Fin n -> a -> m a) -> m a
ascendM (Nat# n -> Nat n
forall (n :: Nat). Nat# n -> Nat n
Nat.lift Nat# n
n) a
a0 (\Fin n
ix a
a -> Fin# n -> a -> m a
f (Fin n -> Fin# n
forall (n :: Nat). Fin n -> Fin# n
unlift Fin n
ix) a
a)

{- | Monadic traversal of the numbers bounded by @n@
in ascending order.

> ascendM_ 4 f = f 0 *> f 1 *> f 2 *> f 3
-}
ascendM_ ::
  forall m a n.
  (Applicative m) =>
  -- | Upper bound
  Nat n ->
  -- | Effectful interpretion
  (Fin n -> m a) ->
  m ()
{-# INLINE ascendM_ #-}
ascendM_ :: forall (m :: * -> *) a (n :: Nat).
Applicative m =>
Nat n -> (Fin n -> m a) -> m ()
ascendM_ !Nat n
n Fin n -> m a
f = Nat 0 -> m ()
forall (p :: Nat). Nat p -> m ()
go Nat 0
Nat.zero
 where
  go :: Nat p -> m ()
  go :: forall (p :: Nat). Nat p -> m ()
go !Nat p
m = case Nat p
m Nat p -> Nat n -> Maybe (p < n)
forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Maybe (a < b)
<? Nat n
n of
    Maybe (p < n)
Nothing -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    Just p < n
lt -> Fin n -> m a
f (Nat p -> (p < n) -> Fin n
forall (m :: Nat) (a :: Nat). Nat m -> (m < a) -> Fin a
Fin Nat p
m p < n
lt) m a -> m () -> m ()
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Nat (p + 1) -> m ()
forall (p :: Nat). Nat p -> m ()
go (Nat p -> Nat (p + 1)
forall (a :: Nat). Nat a -> Nat (a + 1)
Nat.succ Nat p
m)

ascendFromToM_# ::
  forall m a i n.
  (Monad m) =>
  -- | Index to start at (inclusive)
  Nat# i ->
  -- | Upper bound (exclusive)
  Nat# n ->
  -- | Update accumulator
  (Fin# n -> m a) ->
  m ()
ascendFromToM_# :: forall (m :: * -> *) a (i :: Nat) (n :: Nat).
Monad m =>
Nat# i -> Nat# n -> (Fin# n -> m a) -> m ()
ascendFromToM_# Nat# i
m0 Nat# n
end Fin# n -> m a
f = Nat# i -> m ()
forall (k :: Nat). Nat# k -> m ()
go Nat# i
m0
  where
  go :: forall k. Nat# k -> m ()
  go :: forall (k :: Nat). Nat# k -> m ()
go Nat# k
m = case Nat# k
m Nat# k -> Nat# n -> MaybeVoid# (k <# n)
forall (a :: Nat) (b :: Nat).
Nat# a -> Nat# b -> MaybeVoid# (a <# b)
<?# Nat# n
end of
    JustVoid# k <# n
lt -> Fin# n -> m a
f ((k <# n) -> Nat# k -> Fin# n
forall (i :: Nat) (n :: Nat). (i <# n) -> Nat# i -> Fin# n
construct# k <# n
lt Nat# k
m) m a -> m () -> m ()
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Nat# (k + 1) -> m ()
forall (k :: Nat). Nat# k -> m ()
go (Nat# k -> Nat# (k + 1)
forall (a :: Nat). Nat# a -> Nat# (a + 1)
Nat.succ# Nat# k
m)
    MaybeVoid# (k <# n)
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

{- | Variant of @ascendM_@ that takes an unboxed Nat and provides
an unboxed Fin to the callback.
-}
ascendM_# ::
  forall m a n.
  (Monad m) =>
  -- | Upper bound
  Nat# n ->
  -- | Update accumulator
  (Fin# n -> m a) ->
  m ()
{-# INLINE ascendM_# #-}
ascendM_# :: forall (m :: * -> *) a (n :: Nat).
Monad m =>
Nat# n -> (Fin# n -> m a) -> m ()
ascendM_# Nat# n
n Fin# n -> m a
f = Nat n -> (Fin n -> m a) -> m ()
forall (m :: * -> *) a (n :: Nat).
Applicative m =>
Nat n -> (Fin n -> m a) -> m ()
ascendM_ (Nat# n -> Nat n
forall (n :: Nat). Nat# n -> Nat n
Nat.lift Nat# n
n) (\Fin n
ix -> Fin# n -> m a
f (Fin n -> Fin# n
forall (n :: Nat). Fin n -> Fin# n
unlift Fin n
ix))

descendLemma :: forall a b c. a + 1 :=: b -> b <= c -> a < c
{-# INLINE descendLemma #-}
descendLemma :: forall (a :: Nat) (b :: Nat) (c :: Nat).
((a + 1) :=: b) -> (b <= c) -> a < c
descendLemma !(a + 1) :=: b
aPlusOneEqB !b <= c
bLteC =
  (a < c) -> a < c
forall a. a -> a
id
    ((a < c) -> a < c) -> (a < c) -> a < c
forall a b. (a -> b) -> a -> b
$ (a < (a + 1)) -> ((a + 1) <= c) -> a < c
forall (a :: Nat) (b :: Nat) (c :: Nat).
(a < b) -> (b <= c) -> a < c
Lt.transitiveNonstrictR
      ( ((1 + a) :=: (a + 1)) -> (a < (1 + a)) -> a < (a + 1)
forall (b :: Nat) (c :: Nat) (a :: Nat).
(b :=: c) -> (a < b) -> a < c
Lt.substituteR
          (forall (a :: Nat) (b :: Nat). (a + b) :=: (b + a)
Plus.commutative @1 @a)
          ((0 < 1) -> (a <= a) -> (0 + a) < (1 + a)
forall (a :: Nat) (b :: Nat) (c :: Nat) (d :: Nat).
(a < b) -> (c <= d) -> (a + c) < (b + d)
Lt.plus 0 < 1
Lt.zero a <= a
forall (a :: Nat). a <= a
Lte.reflexive)
      )
    (((a + 1) <= c) -> a < c) -> ((a + 1) <= c) -> a < c
forall a b. (a -> b) -> a -> b
$ (b :=: (a + 1)) -> (b <= c) -> (a + 1) <= c
forall (b :: Nat) (c :: Nat) (a :: Nat).
(b :=: c) -> (b <= a) -> c <= a
Lte.substituteL (((a + 1) :=: b) -> b :=: (a + 1)
forall (m :: Nat) (n :: Nat). (m :=: n) -> n :=: m
Eq.symmetric (a + 1) :=: b
aPlusOneEqB) b <= c
bLteC

{- | Strict monadic left fold over the numbers bounded by @n@
in descending order. Roughly:

> descendM 4 z f =
>   f 3 z0 >>= \z1 ->
>   f 2 z1 >>= \z2 ->
>   f 1 z2 >>= \z3 ->
>   f 0 z3
-}
descendM ::
  forall m a n.
  (Monad m) =>
  Nat n ->
  a ->
  (Fin n -> a -> m a) ->
  m a
{-# INLINE descendM #-}
descendM :: forall (m :: * -> *) a (n :: Nat).
Monad m =>
Nat n -> a -> (Fin n -> a -> m a) -> m a
descendM !Nat n
n !a
b0 Fin n -> a -> m a
f = Nat n -> (n <= n) -> a -> m a
forall (p :: Nat). Nat p -> (p <= n) -> a -> m a
go Nat n
n n <= n
forall (a :: Nat). a <= a
Lte.reflexive a
b0
 where
  go :: Nat p -> p <= n -> a -> m a
  go :: forall (p :: Nat). Nat p -> (p <= n) -> a -> m a
go !Nat p
m p <= n
pLteEn !a
b = case Nat p -> Nat 1 -> Maybe (Difference p 1)
forall (a :: Nat) (b :: Nat).
Nat a -> Nat b -> Maybe (Difference a b)
Nat.monus Nat p
m Nat 1
Nat.one of
    Maybe (Difference p 1)
Nothing -> a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
b
    Just (Difference (Nat c
mpred :: Nat c) (c + 1) :=: p
cPlusOneEqP) ->
      let !cLtEn :: c < n
cLtEn = ((c + 1) :=: p) -> (p <= n) -> c < n
forall (a :: Nat) (b :: Nat) (c :: Nat).
((a + 1) :=: b) -> (b <= c) -> a < c
descendLemma (c + 1) :=: p
cPlusOneEqP p <= n
pLteEn
       in Nat c -> (c <= n) -> a -> m a
forall (p :: Nat). Nat p -> (p <= n) -> a -> m a
go Nat c
mpred ((c < n) -> c <= n
forall (a :: Nat) (b :: Nat). (a < b) -> a <= b
Lte.fromStrict c < n
cLtEn) (a -> m a) -> m a -> m a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Fin n -> a -> m a
f (Nat c -> (c < n) -> Fin n
forall (m :: Nat) (a :: Nat). Nat m -> (m < a) -> Fin a
Fin Nat c
mpred c < n
cLtEn) a
b

{- | Monadic traversal of the numbers bounded by @n@
in descending order.

> descendM_ 4 f = f 3 *> f 2 *> f 1 *> f 0
-}
descendM_ ::
  forall m a n.
  (Applicative m) =>
  -- | Upper bound
  Nat n ->
  -- | Effectful interpretion
  (Fin n -> m a) ->
  m ()
{-# INLINE descendM_ #-}
descendM_ :: forall (m :: * -> *) a (n :: Nat).
Applicative m =>
Nat n -> (Fin n -> m a) -> m ()
descendM_ !Nat n
n Fin n -> m a
f = Nat n -> (n <= n) -> m ()
forall (p :: Nat). Nat p -> (p <= n) -> m ()
go Nat n
n n <= n
forall (a :: Nat). a <= a
Lte.reflexive
 where
  go :: Nat p -> p <= n -> m ()
  go :: forall (p :: Nat). Nat p -> (p <= n) -> m ()
go !Nat p
m !p <= n
pLteEn = case Nat p -> Nat 1 -> Maybe (Difference p 1)
forall (a :: Nat) (b :: Nat).
Nat a -> Nat b -> Maybe (Difference a b)
Nat.monus Nat p
m Nat 1
Nat.one of
    Maybe (Difference p 1)
Nothing -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    Just (Difference (Nat c
mpred :: Nat c) (c + 1) :=: p
cPlusOneEqP) ->
      let !cLtEn :: c < n
cLtEn = ((c + 1) :=: p) -> (p <= n) -> c < n
forall (a :: Nat) (b :: Nat) (c :: Nat).
((a + 1) :=: b) -> (b <= c) -> a < c
descendLemma (c + 1) :=: p
cPlusOneEqP p <= n
pLteEn
       in Fin n -> m a
f (Nat c -> (c < n) -> Fin n
forall (m :: Nat) (a :: Nat). Nat m -> (m < a) -> Fin a
Fin Nat c
mpred c < n
cLtEn) m a -> m () -> m ()
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Nat c -> (c <= n) -> m ()
forall (p :: Nat). Nat p -> (p <= n) -> m ()
go Nat c
mpred ((c < n) -> c <= n
forall (a :: Nat) (b :: Nat). (a < b) -> a <= b
Lte.fromStrict c < n
cLtEn)

{- | Generate all values of a finite set in ascending order.

>>> ascending (Nat.constant @3)
[Fin 0,Fin 1,Fin 2]
-}
ascending :: forall n. Nat n -> [Fin n]
ascending :: forall (n :: Nat). Nat n -> [Fin n]
ascending !Nat n
n = Nat 0 -> [Fin n]
forall (m :: Nat). Nat m -> [Fin n]
go Nat 0
Nat.zero
 where
  go :: Nat m -> [Fin n]
  go :: forall (m :: Nat). Nat m -> [Fin n]
go !Nat m
m = case Nat m
m Nat m -> Nat n -> Maybe (m < n)
forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Maybe (a < b)
<? Nat n
n of
    Maybe (m < n)
Nothing -> []
    Just m < n
lt -> Nat m -> (m < n) -> Fin n
forall (m :: Nat) (a :: Nat). Nat m -> (m < a) -> Fin a
Fin Nat m
m m < n
lt Fin n -> [Fin n] -> [Fin n]
forall a. a -> [a] -> [a]
: Nat (m + 1) -> [Fin n]
forall (m :: Nat). Nat m -> [Fin n]
go (Nat m -> Nat (m + 1)
forall (a :: Nat). Nat a -> Nat (a + 1)
Nat.succ Nat m
m)

{- | Generate all values of a finite set in descending order.

>>> descending (Nat.constant @3)
[Fin 2,Fin 1,Fin 0]
-}
descending :: forall n. Nat n -> [Fin n]
descending :: forall (n :: Nat). Nat n -> [Fin n]
descending !Nat n
n = Nat n -> (n <= n) -> [Fin n]
forall (p :: Nat). Nat p -> (p <= n) -> [Fin n]
go Nat n
n n <= n
forall (a :: Nat). a <= a
Lte.reflexive
 where
  go :: Nat p -> (p <= n) -> [Fin n]
  go :: forall (p :: Nat). Nat p -> (p <= n) -> [Fin n]
go !Nat p
m !p <= n
pLteEn = case Nat p -> Nat 1 -> Maybe (Difference p 1)
forall (a :: Nat) (b :: Nat).
Nat a -> Nat b -> Maybe (Difference a b)
Nat.monus Nat p
m Nat 1
Nat.one of
    Maybe (Difference p 1)
Nothing -> []
    Just (Difference (Nat c
mpred :: Nat c) (c + 1) :=: p
cPlusOneEqP) ->
      let !cLtEn :: c < n
cLtEn = ((c + 1) :=: p) -> (p <= n) -> c < n
forall (a :: Nat) (b :: Nat) (c :: Nat).
((a + 1) :=: b) -> (b <= c) -> a < c
descendLemma (c + 1) :=: p
cPlusOneEqP p <= n
pLteEn
       in Nat c -> (c < n) -> Fin n
forall (m :: Nat) (a :: Nat). Nat m -> (m < a) -> Fin a
Fin Nat c
mpred c < n
cLtEn Fin n -> [Fin n] -> [Fin n]
forall a. a -> [a] -> [a]
: Nat c -> (c <= n) -> [Fin n]
forall (p :: Nat). Nat p -> (p <= n) -> [Fin n]
go Nat c
mpred ((c < n) -> c <= n
forall (a :: Nat) (b :: Nat). (a < b) -> a <= b
Lte.fromStrict c < n
cLtEn)

{- | Generate 'len' values starting from 'off' in ascending order.

>>> ascendingSlice (Nat.constant @2) (Nat.constant @3) (Lte.constant @_ @6)
[Fin 2,Fin 3,Fin 4]
-}
ascendingSlice ::
  forall n off len.
  Nat off ->
  Nat len ->
  off + len <= n ->
  [Fin n]
{-# INLINE ascendingSlice #-}
ascendingSlice :: forall (n :: Nat) (off :: Nat) (len :: Nat).
Nat off -> Nat len -> ((off + len) <= n) -> [Fin n]
ascendingSlice Nat off
off Nat len
len !(off + len) <= n
offPlusLenLteEn = Nat 0 -> [Fin n]
forall (m :: Nat). Nat m -> [Fin n]
go Nat 0
Nat.zero
 where
  go :: Nat m -> [Fin n]
  go :: forall (m :: Nat). Nat m -> [Fin n]
go !Nat m
m = case Nat m
m Nat m -> Nat len -> Maybe (m < len)
forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Maybe (a < b)
<? Nat len
len of
    Maybe (m < len)
Nothing -> []
    Just m < len
emLtLen ->
      let !offPlusEmLtOffPlusLen :: (off + m) < (off + len)
offPlusEmLtOffPlusLen = forall (c :: Nat) (a :: Nat) (b :: Nat).
(a < b) -> (c + a) < (c + b)
Lt.incrementL @off m < len
emLtLen
          !offPlusEmLtEn :: (off + m) < n
offPlusEmLtEn = ((off + m) < (off + len)) -> ((off + len) <= n) -> (off + m) < n
forall (a :: Nat) (b :: Nat) (c :: Nat).
(a < b) -> (b <= c) -> a < c
Lt.transitiveNonstrictR (off + m) < (off + len)
offPlusEmLtOffPlusLen (off + len) <= n
offPlusLenLteEn
       in Nat (off + m) -> ((off + m) < n) -> Fin n
forall (m :: Nat) (a :: Nat). Nat m -> (m < a) -> Fin a
Fin (Nat off -> Nat m -> Nat (off + m)
forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Nat (a + b)
Nat.plus Nat off
off Nat m
m) (off + m) < n
offPlusEmLtEn Fin n -> [Fin n] -> [Fin n]
forall a. a -> [a] -> [a]
: Nat (m + 1) -> [Fin n]
forall (m :: Nat). Nat m -> [Fin n]
go (Nat m -> Nat (m + 1)
forall (a :: Nat). Nat a -> Nat (a + 1)
Nat.succ Nat m
m)

{- | Generate 'len' values starting from 'off + len - 1' in descending order.

>>> descendingSlice (Nat.constant @2) (Nat.constant @3) (Lt.constant @6)
[Fin 4,Fin 3,Fin 2]
-}
descendingSlice ::
  forall n off len.
  Nat off ->
  Nat len ->
  off + len <= n ->
  [Fin n]
{-# INLINE descendingSlice #-}
descendingSlice :: forall (n :: Nat) (off :: Nat) (len :: Nat).
Nat off -> Nat len -> ((off + len) <= n) -> [Fin n]
descendingSlice !Nat off
off !Nat len
len !(off + len) <= n
offPlusLenLteEn =
  Nat len -> (len <= len) -> [Fin n]
forall (m :: Nat). Nat m -> (m <= len) -> [Fin n]
go Nat len
len len <= len
forall (a :: Nat). a <= a
Lte.reflexive
 where
  go :: Nat m -> m <= len -> [Fin n]
  go :: forall (m :: Nat). Nat m -> (m <= len) -> [Fin n]
go !Nat m
m !m <= len
mLteEn = case Nat m -> Nat 1 -> Maybe (Difference m 1)
forall (a :: Nat) (b :: Nat).
Nat a -> Nat b -> Maybe (Difference a b)
Nat.monus Nat m
m Nat 1
Nat.one of
    Maybe (Difference m 1)
Nothing -> []
    Just (Difference (Nat c
mpred :: Nat c) (c + 1) :=: m
cPlusOneEqEm) ->
      let !cLtLen :: c < len
cLtLen =
            (c < (c + 1)) -> ((c + 1) <= len) -> c < len
forall (a :: Nat) (b :: Nat) (c :: Nat).
(a < b) -> (b <= c) -> a < c
Lt.transitiveNonstrictR
              (((1 + c) :=: (c + 1)) -> (c < (1 + c)) -> c < (c + 1)
forall (b :: Nat) (c :: Nat) (a :: Nat).
(b :=: c) -> (a < b) -> a < c
Lt.substituteR (forall (a :: Nat) (b :: Nat). (a + b) :=: (b + a)
Plus.commutative @1 @c) ((0 < 1) -> (c <= c) -> (0 + c) < (1 + c)
forall (a :: Nat) (b :: Nat) (c :: Nat) (d :: Nat).
(a < b) -> (c <= d) -> (a + c) < (b + d)
Lt.plus 0 < 1
Lt.zero c <= c
forall (a :: Nat). a <= a
Lte.reflexive))
              -- c < c + 1
              ((m :=: (c + 1)) -> (m <= len) -> (c + 1) <= len
forall (b :: Nat) (c :: Nat) (a :: Nat).
(b :=: c) -> (b <= a) -> c <= a
Lte.substituteL (((c + 1) :=: m) -> m :=: (c + 1)
forall (m :: Nat) (n :: Nat). (m :=: n) -> n :=: m
Eq.symmetric (c + 1) :=: m
cPlusOneEqEm) m <= len
mLteEn)
          -- c + 1 <= len
          !cPlusOffLtEn :: (c + off) < n
cPlusOffLtEn =
            ((c + off) < (off + len)) -> ((off + len) <= n) -> (c + off) < n
forall (a :: Nat) (b :: Nat) (c :: Nat).
(a < b) -> (b <= c) -> a < c
Lt.transitiveNonstrictR
              ( ((len + off) :=: (off + len))
-> ((c + off) < (len + off)) -> (c + off) < (off + len)
forall (b :: Nat) (c :: Nat) (a :: Nat).
(b :=: c) -> (a < b) -> a < c
Lt.substituteR
                  (forall (a :: Nat) (b :: Nat). (a + b) :=: (b + a)
Plus.commutative @len @off)
                  ((c < len) -> (off <= off) -> (c + off) < (len + off)
forall (a :: Nat) (b :: Nat) (c :: Nat) (d :: Nat).
(a < b) -> (c <= d) -> (a + c) < (b + d)
Lt.plus c < len
cLtLen (forall (a :: Nat). a <= a
Lte.reflexive @off))
              )
              -- c + off < off + len
              (off + len) <= n
offPlusLenLteEn
       in Nat (c + off) -> ((c + off) < n) -> Fin n
forall (m :: Nat) (a :: Nat). Nat m -> (m < a) -> Fin a
Fin (Nat c
mpred Nat c -> Nat off -> Nat (c + off)
forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Nat (a + b)
`Nat.plus` Nat off
off) (c + off) < n
cPlusOffLtEn Fin n -> [Fin n] -> [Fin n]
forall a. a -> [a] -> [a]
: Nat c -> (c <= len) -> [Fin n]
forall (m :: Nat). Nat m -> (m <= len) -> [Fin n]
go Nat c
mpred ((c < len) -> c <= len
forall (a :: Nat) (b :: Nat). (a < b) -> a <= b
Lte.fromStrict c < len
cLtLen)

{- | Extract the 'Int' from a 'Fin n'. This is intended to be used
at a boundary where a safe interface meets the unsafe primitives
on top of which it is built.
-}
demote :: Fin n -> Int
{-# INLINE demote #-}
demote :: forall (n :: Nat). Fin n -> Int
demote (Fin Nat m
i m < n
_) = Nat m -> Int
forall (n :: Nat). Nat n -> Int
Nat.demote Nat m
i

demote# :: Fin# n -> Int#
{-# INLINE demote# #-}
demote# :: forall (n :: Nat). Fin# n -> Int#
demote# (Fin# Int#
i) = Int#
i

demote32# :: Fin32# n -> Int32#
{-# INLINE demote32# #-}
demote32# :: forall (n :: Nat). Fin32# n -> Int32#
demote32# (Fin32# Int32#
i) = Int32#
i

lift :: Unsafe.Fin# n -> Fin n
{-# INLINE lift #-}
lift :: forall (n :: Nat). Fin# n -> Fin n
lift (Unsafe.Fin# Int#
i) = Nat Any -> (Any < n) -> Fin n
forall (m :: Nat) (a :: Nat). Nat m -> (m < a) -> Fin a
Fin (Int -> Nat Any
forall (n :: Nat). Int -> Nat n
Unsafe.Nat (Int# -> Int
I# Int#
i)) Any < n
forall (a :: Nat) (b :: Nat). a < b
Unsafe.Lt

unlift :: Fin n -> Unsafe.Fin# n
{-# INLINE unlift #-}
unlift :: forall (n :: Nat). Fin n -> Fin# n
unlift (Fin (Unsafe.Nat (I# Int#
i)) m < n
_) = Int# -> Fin# n
forall (a :: Nat). Int# -> Fin# a
Unsafe.Fin# Int#
i

-- | Consume the natural number and the proof in the Fin.
with :: Fin n -> (forall i. (i < n) -> Nat i -> a) -> a
{-# INLINE with #-}
with :: forall (n :: Nat) a.
Fin n -> (forall (i :: Nat). (i < n) -> Nat i -> a) -> a
with (Fin Nat m
i m < n
lt) forall (i :: Nat). (i < n) -> Nat i -> a
f = (m < n) -> Nat m -> a
forall (i :: Nat). (i < n) -> Nat i -> a
f m < n
lt Nat m
i

-- | Variant of 'with' for unboxed argument and result types.
with# :: Fin# n -> (forall i. (i <# n) -> Nat# i -> a) -> a
{-# INLINE with# #-}
with# :: forall (n :: Nat) a.
Fin# n -> (forall (i :: Nat). (i <# n) -> Nat# i -> a) -> a
with# (Unsafe.Fin# Int#
i) forall (i :: Nat). (i <# n) -> Nat# i -> a
f = (Any <# n) -> Nat# Any -> a
forall (i :: Nat). (i <# n) -> Nat# i -> a
f ((# #) -> Any <# n
forall (a :: Nat) (b :: Nat). (# #) -> a <# b
Unsafe.Lt# (# #)) (Int# -> Nat# Any
forall (a :: Nat). Int# -> Nat# a
Unsafe.Nat# Int#
i)

construct# :: (i <# n) -> Nat# i -> Fin# n
{-# INLINE construct# #-}
construct# :: forall (i :: Nat) (n :: Nat). (i <# n) -> Nat# i -> Fin# n
construct# i <# n
_ (Unsafe.Nat# Int#
x) = Int# -> Fin# n
forall (a :: Nat). Int# -> Fin# a
Unsafe.Fin# Int#
x

{- | Return the successor of the Fin or return nothing if the
argument is the greatest inhabitant.
-}
succ :: Nat n -> Fin n -> Maybe (Fin n)
{-# INLINE succ #-}
succ :: forall (n :: Nat). Nat n -> Fin n -> Maybe (Fin n)
succ Nat n
n (Fin Nat m
ix m < n
_) = case Nat (m + 1)
ix' Nat (m + 1) -> Nat n -> Maybe ((m + 1) < n)
forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Maybe (a < b)
<? Nat n
n of
  Maybe ((m + 1) < n)
Nothing -> Maybe (Fin n)
forall a. Maybe a
Nothing
  Just (m + 1) < n
lt -> Fin n -> Maybe (Fin n)
forall a. a -> Maybe a
Just (Nat (m + 1) -> ((m + 1) < n) -> Fin n
forall (m :: Nat) (a :: Nat). Nat m -> (m < a) -> Fin a
Fin Nat (m + 1)
ix' (m + 1) < n
lt)
 where
  ix' :: Nat (m + 1)
ix' = Nat m -> Nat (m + 1)
forall (a :: Nat). Nat a -> Nat (a + 1)
Nat.succ Nat m
ix

-- | Variant of 'succ' for unlifted finite numbers.
succ# :: Nat# n -> Fin# n -> MaybeFin# n
{-# INLINE succ# #-}
succ# :: forall (n :: Nat). Nat# n -> Fin# n -> MaybeFin# n
succ# (Nat# Int#
n) (Fin# Int#
ix) = case Int#
ix' Int# -> Int# -> Int#
Exts.<# Int#
n of
  Int#
0# -> (# #) -> forall (n :: Nat). MaybeFin# n
forall (n :: Nat). MaybeFin# n
MaybeFinNothing#
  Int#
_ -> Fin# n -> MaybeFin# n
forall (n :: Nat). Fin# n -> MaybeFin# n
MaybeFinJust# (Int# -> Fin# n
forall (a :: Nat). Int# -> Fin# a
Fin# Int#
ix')
 where
  !ix' :: Int#
ix' = Int#
ix Int# -> Int# -> Int#
+# Int#
1#

{- | Convert an Int to a finite number, testing that it is
less than the upper bound. This crashes with an uncatchable
exception when given a negative number.
-}
fromInt ::
  -- | exclusive upper bound
  Nat n ->
  Int ->
  Maybe (Fin n)
{-# INLINE fromInt #-}
fromInt :: forall (n :: Nat). Nat n -> Int -> Maybe (Fin n)
fromInt Nat n
bound Int
i
  | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 = [Char] -> Maybe (Fin n)
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"Arithmetic.Fin.fromInt: negative argument"
  | Bool
otherwise = Int -> (forall {n :: Nat}. Nat n -> Maybe (Fin n)) -> Maybe (Fin n)
forall a. Int -> (forall (n :: Nat). Nat n -> a) -> a
Nat.with Int
i ((forall {n :: Nat}. Nat n -> Maybe (Fin n)) -> Maybe (Fin n))
-> (forall {n :: Nat}. Nat n -> Maybe (Fin n)) -> Maybe (Fin n)
forall a b. (a -> b) -> a -> b
$ \Nat n
number -> case Nat n
number Nat n -> Nat n -> Maybe (n < n)
forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Maybe (a < b)
<? Nat n
bound of
      Just n < n
lt -> Fin n -> Maybe (Fin n)
forall a. a -> Maybe a
Just (Nat n -> (n < n) -> Fin n
forall (m :: Nat) (a :: Nat). Nat m -> (m < a) -> Fin a
Fin Nat n
number n < n
lt)
      Maybe (n < n)
Nothing -> Maybe (Fin n)
forall a. Maybe a
Nothing

-- | Unboxed variant of 'fromInt'.
fromInt# ::
  -- | exclusive upper bound
  Nat# n ->
  Int# ->
  MaybeFin# n
{-# INLINE fromInt# #-}
fromInt# :: forall (n :: Nat). Nat# n -> Int# -> MaybeFin# n
fromInt# (Nat# Int#
n) Int#
i
  | Int# -> Bool
Exts.isTrue# (Int#
i Int# -> Int# -> Int#
Exts.<# Int#
0#) =
      [Char] -> MaybeFin# n
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"Arithmetic.Fin.fromInt#: negative argument"
  | Int# -> Bool
Exts.isTrue# (Int#
i Int# -> Int# -> Int#
Exts.<# Int#
n) = Fin# n -> MaybeFin# n
forall (n :: Nat). Fin# n -> MaybeFin# n
MaybeFinJust# (Int# -> Fin# n
forall (a :: Nat). Int# -> Fin# a
Fin# Int#
i)
  | Bool
otherwise = (# #) -> forall (n :: Nat). MaybeFin# n
forall (n :: Nat). MaybeFin# n
MaybeFinNothing#

{- | This crashes if @n = 0@. Divides @i@ by @n@ and takes
the remainder.
-}
remInt# :: Int# -> Nat# n -> Fin# n
remInt# :: forall (n :: Nat). Int# -> Nat# n -> Fin# n
remInt# Int#
i (Nat# Int#
n) = case Int#
n of
  Int#
0# -> [Char] -> Fin# n
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"Arithmetic.Fin.remInt#: cannot divide by zero"
  Int#
_ -> Int# -> Fin# n
forall (a :: Nat). Int# -> Fin# a
Fin# (Int# -> Int# -> Int#
Exts.remInt# Int#
i Int#
n)

{- | This crashes if @n = 0@. Divides @i@ by @n@ and takes
the remainder.
-}
remWord# :: Word# -> Nat# n -> Fin# n
remWord# :: forall (n :: Nat). Word# -> Nat# n -> Fin# n
remWord# Word#
w (Nat# Int#
n) = case Int#
n of
  Int#
0# -> [Char] -> Fin# n
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"Arithmetic.Fin.remWord#: cannot divide by zero"
  Int#
_ -> Int# -> Fin# n
forall (a :: Nat). Int# -> Fin# a
Fin# (Word# -> Int#
Exts.word2Int# (Word# -> Word# -> Word#
Exts.remWord# Word#
w (Int# -> Word#
Exts.int2Word# Int#
n)))

nativeTo32# :: (n <=# 2147483648) -> Fin# n -> Fin32# n
{-# inline nativeTo32# #-}
nativeTo32# :: forall (n :: Nat). (n <=# 2147483648) -> Fin# n -> Fin32# n
nativeTo32# n <=# 2147483648
_ (Fin# Int#
x) = Int32# -> Fin32# n
forall (a :: Nat). Int32# -> Fin32# a
Fin32# (Int# -> Int32#
Exts.intToInt32# Int#
x)

nativeFrom32# :: Fin32# n -> Fin# n
{-# inline nativeFrom32# #-}
nativeFrom32# :: forall (n :: Nat). Fin32# n -> Fin# n
nativeFrom32# (Fin32# Int32#
x) = Int# -> Fin# n
forall (a :: Nat). Int# -> Fin# a
Fin# (Int32# -> Int#
Exts.int32ToInt# Int32#
x)

{- | Create an unlifted finite number from an unlifted natural number.
The upper bound is the first type argument so that user can use
type applications to clarify when it is helpful. For example:

>>> Fin.constant# @10 N4#
-}
constant# :: forall (b :: GHC.Nat) (a :: GHC.Nat). (CmpNat a b ~ 'LT) => Nat# a -> Fin# b
constant# :: forall (b :: Nat) (a :: Nat).
(CmpNat a b ~ 'LT) =>
Nat# a -> Fin# b
constant# (Nat# Int#
i) = Int# -> Fin# b
forall (a :: Nat). Int# -> Fin# a
Fin# Int#
i

equals# :: Fin# n -> Fin# n -> Bool
equals# :: forall (n :: Nat). Fin# n -> Fin# n -> Bool
equals# (Fin# Int#
a) (Fin# Int#
b) = Int# -> Bool
Exts.isTrue# (Int#
a Int# -> Int# -> Int#
==# Int#
b)

substitute# :: (m :=:# n) -> Fin# m -> Fin# n
substitute# :: forall (m :: Nat) (n :: Nat). (m :=:# n) -> Fin# m -> Fin# n
substitute# m :=:# n
_ (Fin# Int#
x) = Int# -> Fin# n
forall (a :: Nat). Int# -> Fin# a
Fin# Int#
x

greatest# :: Nat# n -> Fin# (n + 1)
greatest# :: forall (n :: Nat). Nat# n -> Fin# (n + 1)
greatest# (Nat# Int#
i) = Int# -> Fin# (n + 1)
forall (a :: Nat). Int# -> Fin# a
Fin# Int#
i