{-# 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
(
incrementL
, incrementR
, incrementR#
, weaken
, weakenL
, weakenR
, succ
, succ#
, ascend
, ascend'
, ascendFrom'
, ascendFrom'#
, ascendM
, ascendM#
, ascendM_
, ascendM_#
, descend
, descend#
, descend'
, descendM
, descendM_
, ascending
, descending
, ascendingSlice
, descendingSlice
, absurd
, demote
, demote#
, with
, with#
, construct#
, remInt#
, remWord#
, fromInt
, fromInt#
, 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.Unsafe (Fin# (Fin#), MaybeFin#, Nat# (Nat#))
import GHC.Exts (Int (I#), Int#, Word#, (+#))
import GHC.TypeNats (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
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)
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)
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))
)
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)
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)
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
descend ::
forall a n.
Nat n ->
a ->
(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.
Nat# n ->
a ->
(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)
descend' ::
forall a n.
Nat n ->
a ->
(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)
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))
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 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)
ascendFrom' ::
forall a m n.
Nat m ->
Nat n ->
a ->
(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)
ascendFrom'# ::
forall a m n.
Nat# m ->
Nat# n ->
a ->
(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))
ascendM ::
forall m a n.
(Monad m) =>
Nat n ->
a ->
(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
ascendM# ::
forall m a n.
(Monad m) =>
Nat# n ->
a ->
(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)
ascendM_ ::
forall m a n.
(Applicative m) =>
Nat n ->
(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)
ascendM_# ::
forall m a n.
(Monad m) =>
Nat# n ->
(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
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
descendM_ ::
forall m a n.
(Applicative m) =>
Nat n ->
(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)
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)
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)
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)
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))
((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
(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))
)
(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)
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
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
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
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
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
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#
fromInt ::
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
fromInt# ::
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#
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)
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)))