{-# language BangPatterns #-}
{-# language DataKinds #-}
{-# language ExplicitNamespaces #-}
{-# language GADTs #-}
{-# language KindSignatures #-}
{-# language MagicHash #-}
{-# language ScopedTypeVariables #-}
{-# language TypeApplications #-}
{-# language TypeOperators #-}
module Arithmetic.Fin
(
incrementL
, incrementR
, weaken
, weakenL
, weakenR
, ascend
, ascend'
, ascendM
, ascendM_
, descend
, descend'
, descendM
, descendM_
, ascending
, descending
, ascendingSlice
, descendingSlice
, absurd
, demote
, 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
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)
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)
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))
)
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 :: 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)
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
descend :: forall a n.
Nat n
-> a
-> (Fin n -> a -> a)
-> 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))
descend' :: forall a n.
Nat n
-> a
-> (Fin n -> a -> a)
-> 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)
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))
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 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)
ascendM :: forall m a n. Monad m
=> Nat n
-> a
-> (Fin n -> a -> m a)
-> 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
ascendM_ :: forall m a n. Applicative m
=> Nat n
-> (Fin n -> m a)
-> 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
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
descendM_ :: forall m a n. Applicative m
=> Nat n
-> (Fin n -> m a)
-> 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)
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)
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)
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)
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))
((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)
!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)))
(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)
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