{-# language BangPatterns #-}
{-# language DataKinds #-}
{-# language ExplicitNamespaces #-}
{-# language GADTs #-}
{-# language KindSignatures #-}
{-# language MagicHash #-}
{-# language ScopedTypeVariables #-}
{-# language TypeApplications #-}
{-# language TypeOperators #-}
module Arithmetic.Fin
  ( -- * Modification
    incrementL
  , incrementR
  , weaken
  , weakenL
  , weakenR
    -- * 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'
  , ascendM
  , ascendM_
  , descend
  , descend'
  , descendM
  , descendM_
  , ascending
  , descending
  , ascendingSlice
  , descendingSlice
    -- * Absurdities
  , absurd
    -- * Demote
  , demote
    -- * Lift and Unlift
  , lift
  , unlift
  ) where

import Prelude hiding (last)

import Arithmetic.Nat ((<?))
import Arithmetic.Types (Fin(..),Difference(..),Nat,type (<), type (<=), type (:=:))
import GHC.Exts (Int(I#))
import GHC.TypeNats (type (+))

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

-- | 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 :: 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) (n :: Nat). Nat m -> (m < n) -> Fin n
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) ((m < n) -> (m + m) < (n + m)
forall (c :: Nat) (a :: Nat) (b :: Nat).
(a < b) -> (a + c) < (b + c)
Lt.incrementR @m m < n
pf)

-- | 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 :: 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) (n :: Nat). Nat m -> (m < n) -> Fin n
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) ((m < n) -> (m + m) < (m + n)
forall (c :: Nat) (a :: Nat) (b :: Nat).
(a < b) -> (c + a) < (c + b)
Lt.incrementL @m m < n
pf)

-- | 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 :: Fin n -> Fin (m + n)
weakenL (Fin Nat m
i m < n
pf) = Nat m -> (m < (m + n)) -> Fin (m + n)
forall (m :: Nat) (n :: Nat). Nat m -> (m < n) -> Fin n
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
    ((n + m) :=: (m + n)
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 (0 <= m
forall (a :: Nat). 0 <= a
Lte.zero @m))
  )

-- | 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 :: Fin n -> Fin (n + m)
weakenR (Fin Nat m
i m < n
pf) = Nat m -> (m < (n + m)) -> Fin (n + m)
forall (m :: Nat) (n :: Nat). Nat m -> (m < n) -> Fin n
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)

-- | 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 :: (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) (n :: Nat). Nat m -> (m < n) -> Fin n
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)

-- | A finite set of no values is impossible.
absurd :: Fin 0 -> void
{-# inline absurd #-}
absurd :: 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.
     Nat n -- ^ Upper bound
  -> a -- ^ Initial accumulator
  -> (Fin n -> a -> a) -- ^ Update accumulator
  -> a
{-# inline descend #-}
descend :: 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 :: 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) (n :: Nat). Nat m -> (m < n) -> Fin n
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))

-- | 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.
     Nat n -- ^ Upper bound
  -> a -- ^ Initial accumulator
  -> (Fin n -> a -> a) -- ^ Update accumulator
  -> a
{-# inline descend' #-}
descend' :: 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 :: 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) (n :: Nat). Nat m -> (m < n) -> Fin n
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 :: 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 :: 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) (n :: Nat). Nat m -> (m < n) -> Fin n
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.
     Nat n -- ^ Upper bound
  -> a -- ^ Initial accumulator
  -> (Fin n -> a -> a) -- ^ Update accumulator
  -> a
{-# inline ascend' #-}
ascend' :: 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 :: 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) (n :: Nat). Nat m -> (m < n) -> Fin n
Fin Nat m
m m < n
lt) a
b)

-- | 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
  => Nat n -- ^ Upper bound
  -> a -- ^ Initial accumulator
  -> (Fin n -> a -> m a) -- ^ Update accumulator
  -> m a
{-# inline ascendM #-}
ascendM :: 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 :: 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 (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) (n :: Nat). Nat m -> (m < n) -> Fin n
Fin Nat p
m p < n
lt) a
b

-- | 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
  => Nat n -- ^ Upper bound
  -> (Fin n -> m a) -- ^ Effectful interpretion
  -> m ()
{-# inline ascendM_ #-}
ascendM_ :: 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 :: 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 (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) (n :: Nat). Nat m -> (m < n) -> Fin n
Fin Nat p
m p < n
lt) m a -> m () -> m ()
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)

descendLemma :: forall a b c. a + 1 :=: b -> b <= c -> a < c
{-# inline descendLemma #-}
descendLemma :: ((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 ((1 + a) :=: (a + 1)
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 :: 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 :: 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 (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) (n :: Nat). Nat m -> (m < n) -> Fin n
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
  => Nat n -- ^ Upper bound
  -> (Fin n -> m a) -- ^ Effectful interpretion
  -> m ()
{-# inline descendM_ #-}
descendM_ :: 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 :: 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 (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) (n :: Nat). Nat m -> (m < n) -> Fin n
Fin Nat c
mpred c < n
cLtEn) m a -> m () -> m ()
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 :: 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 :: 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) (n :: Nat). Nat m -> (m < n) -> Fin n
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 :: 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 :: 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) (n :: Nat). Nat m -> (m < n) -> Fin n
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 :: 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 :: 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 = (m < len) -> (off + m) < (off + len)
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) (n :: Nat). Nat m -> (m < n) -> Fin n
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 :: 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 :: 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 ((1 + c) :=: (c + 1)
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
                ((len + off) :=: (off + len)
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 (off <= off
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) (n :: Nat). Nat m -> (m < n) -> Fin n
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 :: Fin n -> Int
demote (Fin Nat m
i m < n
_) = Nat m -> Int
forall (n :: Nat). Nat n -> Int
Nat.demote Nat m
i

lift :: Unsafe.Fin# n -> Fin n
{-# inline lift #-}
lift :: Fin# n -> Fin n
lift (Unsafe.Fin# Int#
i) = Nat Any -> (Any < n) -> Fin n
forall (m :: Nat) (n :: Nat). Nat m -> (m < n) -> Fin n
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 :: Fin n -> Fin# n
unlift (Fin (Unsafe.Nat (I# Int#
i)) m < n
_) = Int# -> Fin# n
forall (n :: Nat). Int# -> Fin# n
Unsafe.Fin# Int#
i