{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE DeriveDataTypeable   #-}
{-# LANGUAGE EmptyCase            #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE KindSignatures       #-}
{-# LANGUAGE Safe                 #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE StandaloneDeriving   #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}
-- | Finite numbers.
--
-- This module is designed to be imported as
--
-- @
-- import Data.Fin (Fin (..))
-- import qualified Data.Fin as Fin
-- @
--
module Data.Fin (
    Fin (..),
    cata,
    -- * Showing
    explicitShow,
    explicitShowsPrec,
    -- * Conversions
    toNat,
    fromNat,
    toNatural,
    toInteger,
    -- * Interesting
    mirror,
    inverse,
    universe,
    inlineUniverse,
    universe1,
    inlineUniverse1,
    absurd,
    boring,
    -- * Plus
    weakenLeft,
    weakenLeft1,
    weakenRight,
    weakenRight1,
    append,
    split,
    -- * Min and max
    isMin,
    isMax,
    -- * Aliases
    fin0, fin1, fin2, fin3, fin4, fin5, fin6, fin7, fin8, fin9,
    ) where

import Control.DeepSeq    (NFData (..))
import Data.Bifunctor     (bimap)
import Data.Hashable      (Hashable (..))
import Data.List.NonEmpty (NonEmpty (..))
import Data.Proxy         (Proxy (..))
import Data.Type.Nat      (Nat (..))
import Data.Typeable      (Typeable)
import GHC.Exception      (ArithException (..), throw)
import Numeric.Natural    (Natural)

import qualified Data.List.NonEmpty    as NE
import qualified Data.Type.Nat         as N
import qualified Data.Universe.Class   as U
import qualified Data.Universe.Helpers as U
import qualified Test.QuickCheck       as QC

-- $setup
-- >>> import Data.List (genericLength)
-- >>> import Data.List.NonEmpty (NonEmpty (..))
-- >>> import Numeric.Natural (Natural)
-- >>> import qualified Data.Type.Nat as N
-- >>> import qualified Data.Universe.Class as U
-- >>> import qualified Data.Universe.Helpers as U

-------------------------------------------------------------------------------
-- Type
-------------------------------------------------------------------------------

-- | Finite numbers: @[0..n-1]@.
data Fin (n :: Nat) where
    FZ :: Fin ('S n)
    FS :: Fin n -> Fin ('S n)
  deriving (Typeable)

-------------------------------------------------------------------------------
-- Instances
-------------------------------------------------------------------------------

deriving instance Eq (Fin n)
deriving instance Ord (Fin n)

-- | 'Fin' is printed as 'Natural'.
--
-- To see explicit structure, use 'explicitShow' or 'explicitShowsPrec'
instance Show (Fin n) where
    showsPrec :: Int -> Fin n -> ShowS
showsPrec Int
d  = Int -> Natural -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d (Natural -> ShowS) -> (Fin n -> Natural) -> Fin n -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> Natural
forall (n :: Nat). Fin n -> Natural
toNatural

-- | Operations module @n@.
--
-- >>> map fromInteger [0, 1, 2, 3, 4, -5] :: [Fin N.Nat3]
-- [0,1,2,0,1,1]
--
-- >>> fromInteger 42 :: Fin N.Nat0
-- *** Exception: divide by zero
-- ...
--
-- >>> signum (FZ :: Fin N.Nat1)
-- 0
--
-- >>> signum (3 :: Fin N.Nat4)
-- 1
--
-- >>> 2 + 3 :: Fin N.Nat4
-- 1
--
-- >>> 2 * 3 :: Fin N.Nat4
-- 2
--
instance N.SNatI n => Num (Fin n) where
    abs :: Fin n -> Fin n
abs = Fin n -> Fin n
forall a. a -> a
id

    signum :: Fin n -> Fin n
signum Fin n
FZ          = Fin n
forall (n :: Nat). Fin ('S n)
FZ
    signum (FS Fin n
FZ)     = Fin ('S n) -> Fin ('S ('S n))
forall (n :: Nat). Fin n -> Fin ('S n)
FS Fin ('S n)
forall (n :: Nat). Fin ('S n)
FZ
    signum (FS (FS Fin n
_)) = Fin ('S n) -> Fin ('S ('S n))
forall (n :: Nat). Fin n -> Fin ('S n)
FS Fin ('S n)
forall (n :: Nat). Fin ('S n)
FZ

    fromInteger :: Integer -> Fin n
fromInteger = Integer -> Fin n
forall (n :: Nat) i. (Num i, Ord i, SNatI n) => i -> Fin n
unsafeFromNum (Integer -> Fin n) -> (Integer -> Integer) -> Integer -> Fin n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Proxy @Nat n -> Integer
forall (n :: Nat) m (proxy :: Nat -> *).
(SNatI n, Num m) =>
proxy n -> m
N.reflectToNum (Proxy @Nat n
forall k (t :: k). Proxy @k t
Proxy :: Proxy n))

    Fin n
n + :: Fin n -> Fin n -> Fin n
+ Fin n
m = Integer -> Fin n
forall a. Num a => Integer -> a
fromInteger (Fin n -> Integer
forall a. Integral a => a -> Integer
toInteger Fin n
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Fin n -> Integer
forall a. Integral a => a -> Integer
toInteger Fin n
m)
    Fin n
n * :: Fin n -> Fin n -> Fin n
* Fin n
m = Integer -> Fin n
forall a. Num a => Integer -> a
fromInteger (Fin n -> Integer
forall a. Integral a => a -> Integer
toInteger Fin n
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Fin n -> Integer
forall a. Integral a => a -> Integer
toInteger Fin n
m)
    Fin n
n - :: Fin n -> Fin n -> Fin n
- Fin n
m = Integer -> Fin n
forall a. Num a => Integer -> a
fromInteger (Fin n -> Integer
forall a. Integral a => a -> Integer
toInteger Fin n
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Fin n -> Integer
forall a. Integral a => a -> Integer
toInteger Fin n
m)

    negate :: Fin n -> Fin n
negate = Integer -> Fin n
forall a. Num a => Integer -> a
fromInteger (Integer -> Fin n) -> (Fin n -> Integer) -> Fin n -> Fin n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
forall a. Num a => a -> a
negate (Integer -> Integer) -> (Fin n -> Integer) -> Fin n -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> Integer
forall a. Integral a => a -> Integer
toInteger

instance N.SNatI n => Real (Fin n) where
    toRational :: Fin n -> Rational
toRational = Rational -> (Rational -> Rational) -> Fin n -> Rational
forall a (n :: Nat). a -> (a -> a) -> Fin n -> a
cata Rational
0 Rational -> Rational
forall a. Enum a => a -> a
succ

-- | 'quot' works only on @'Fin' n@ where @n@ is prime.
instance N.SNatI n => Integral (Fin n) where
    toInteger :: Fin n -> Integer
toInteger = Integer -> (Integer -> Integer) -> Fin n -> Integer
forall a (n :: Nat). a -> (a -> a) -> Fin n -> a
cata Integer
0 Integer -> Integer
forall a. Enum a => a -> a
succ

    quotRem :: Fin n -> Fin n -> (Fin n, Fin n)
quotRem Fin n
a Fin n
b = (Fin n -> Fin n -> Fin n
forall a. Integral a => a -> a -> a
quot Fin n
a Fin n
b, Fin n
0)
    quot :: Fin n -> Fin n -> Fin n
quot Fin n
a Fin n
b = Fin n
a Fin n -> Fin n -> Fin n
forall a. Num a => a -> a -> a
* Fin n -> Fin n
forall (n :: Nat). SNatI n => Fin n -> Fin n
inverse Fin n
b

-- | Mirror the values, 'minBound' becomes 'maxBound', etc.
--
-- >>> map mirror universe :: [Fin N.Nat4]
-- [3,2,1,0]
--
-- >>> reverse universe :: [Fin N.Nat4]
-- [3,2,1,0]
--
-- @since 0.1.1
--
mirror :: forall n. N.SNatI n => Fin n -> Fin n
mirror :: Fin n -> Fin n
mirror = Mirror n -> Fin n -> Fin n
forall (n :: Nat). Mirror n -> Fin n -> Fin n
getMirror (Mirror 'Z
-> (forall (m :: Nat). SNatI m => Mirror m -> Mirror ('S m))
-> Mirror n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction Mirror 'Z
start forall (m :: Nat). SNatI m => Mirror m -> Mirror ('S m)
step) where
    start :: Mirror 'Z
    start :: Mirror 'Z
start = (Fin 'Z -> Fin 'Z) -> Mirror 'Z
forall (n :: Nat). (Fin n -> Fin n) -> Mirror n
Mirror Fin 'Z -> Fin 'Z
forall a. a -> a
id

    step :: forall m. N.SNatI m => Mirror m -> Mirror ('S m)
    step :: Mirror m -> Mirror ('S m)
step (Mirror Fin m -> Fin m
rec) = (Fin ('S m) -> Fin ('S m)) -> Mirror ('S m)
forall (n :: Nat). (Fin n -> Fin n) -> Mirror n
Mirror ((Fin ('S m) -> Fin ('S m)) -> Mirror ('S m))
-> (Fin ('S m) -> Fin ('S m)) -> Mirror ('S m)
forall a b. (a -> b) -> a -> b
$ \Fin ('S m)
n -> case Fin ('S m)
n of
        Fin ('S m)
FZ   -> MaxBound m -> Fin ('S m)
forall (n :: Nat). MaxBound n -> Fin ('S n)
getMaxBound (MaxBound 'Z
-> (forall (m :: Nat). SNatI m => MaxBound m -> MaxBound ('S m))
-> MaxBound m
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction (Fin ('S 'Z) -> MaxBound 'Z
forall (n :: Nat). Fin ('S n) -> MaxBound n
MaxBound Fin ('S 'Z)
forall (n :: Nat). Fin ('S n)
FZ) (Fin ('S ('S m)) -> MaxBound ('S m)
forall (n :: Nat). Fin ('S n) -> MaxBound n
MaxBound (Fin ('S ('S m)) -> MaxBound ('S m))
-> (MaxBound m -> Fin ('S ('S m))) -> MaxBound m -> MaxBound ('S m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin ('S m) -> Fin ('S ('S m))
forall (n :: Nat). Fin n -> Fin ('S n)
FS (Fin ('S m) -> Fin ('S ('S m)))
-> (MaxBound m -> Fin ('S m)) -> MaxBound m -> Fin ('S ('S m))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MaxBound m -> Fin ('S m)
forall (n :: Nat). MaxBound n -> Fin ('S n)
getMaxBound))
        FS Fin n
m -> Fin m -> Fin ('S m)
forall (n :: Nat). SNatI n => Fin n -> Fin ('S n)
weakenLeft1 (Fin m -> Fin m
rec Fin m
Fin n
m)

newtype Mirror n = Mirror { Mirror n -> Fin n -> Fin n
getMirror :: Fin n -> Fin n }

-- | Multiplicative inverse.
--
-- Works for @'Fin' n@ where @n@ is coprime with an argument, i.e. in general when @n@ is prime.
--
-- >>> map inverse universe :: [Fin N.Nat5]
-- [0,1,3,2,4]
--
-- >>> zipWith (*) universe (map inverse universe) :: [Fin N.Nat5]
-- [0,1,1,1,1]
--
-- Adaptation of [pseudo-code in Wikipedia](https://en.wikipedia.org/wiki/Extended_Euclidean_algorithm#Modular_integers)
--
inverse :: forall n. N.SNatI n => Fin n -> Fin n
inverse :: Fin n -> Fin n
inverse = Integer -> Fin n
forall a. Num a => Integer -> a
fromInteger (Integer -> Fin n) -> (Fin n -> Integer) -> Fin n -> Fin n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> Integer -> Integer -> Integer
iter Integer
0 Integer
n Integer
1 (Integer -> Integer) -> (Fin n -> Integer) -> Fin n -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> Integer
forall a. Integral a => a -> Integer
toInteger where
    n :: Integer
n = Proxy @Nat n -> Integer
forall (n :: Nat) m (proxy :: Nat -> *).
(SNatI n, Num m) =>
proxy n -> m
N.reflectToNum (Proxy @Nat n
forall k (t :: k). Proxy @k t
Proxy :: Proxy n)

    iter :: Integer -> Integer -> Integer -> Integer -> Integer
iter Integer
t Integer
_ Integer
_  Integer
0
        | Integer
t Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0     = Integer
t Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
n
        | Bool
otherwise = Integer
t
    iter Integer
t Integer
r Integer
t' Integer
r' =
        let q :: Integer
q = Integer
r Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
r'
        in Integer -> Integer -> Integer -> Integer -> Integer
iter Integer
t' Integer
r' (Integer
t Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
q Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
t') (Integer
r Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
q Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
r')

instance N.SNatI n => Enum (Fin n) where
    fromEnum :: Fin n -> Int
fromEnum = Fin n -> Int
forall (m :: Nat). Fin m -> Int
go where
        go :: Fin m -> Int
        go :: Fin m -> Int
go Fin m
FZ     = Int
0
        go (FS Fin n
n) = Int -> Int
forall a. Enum a => a -> a
succ (Fin n -> Int
forall (m :: Nat). Fin m -> Int
go Fin n
n)

    toEnum :: Int -> Fin n
toEnum = Int -> Fin n
forall (n :: Nat) i. (Num i, Ord i, SNatI n) => i -> Fin n
unsafeFromNum

instance (n ~ 'S m, N.SNatI m) => Bounded (Fin n) where
    minBound :: Fin n
minBound = Fin n
forall (n :: Nat). Fin ('S n)
FZ
    maxBound :: Fin n
maxBound = MaxBound m -> Fin ('S m)
forall (n :: Nat). MaxBound n -> Fin ('S n)
getMaxBound (MaxBound m -> Fin ('S m)) -> MaxBound m -> Fin ('S m)
forall a b. (a -> b) -> a -> b
$ MaxBound 'Z
-> (forall (m :: Nat). SNatI m => MaxBound m -> MaxBound ('S m))
-> MaxBound m
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction
        (Fin ('S 'Z) -> MaxBound 'Z
forall (n :: Nat). Fin ('S n) -> MaxBound n
MaxBound Fin ('S 'Z)
forall (n :: Nat). Fin ('S n)
FZ)
        (Fin ('S ('S m)) -> MaxBound ('S m)
forall (n :: Nat). Fin ('S n) -> MaxBound n
MaxBound (Fin ('S ('S m)) -> MaxBound ('S m))
-> (MaxBound m -> Fin ('S ('S m))) -> MaxBound m -> MaxBound ('S m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin ('S m) -> Fin ('S ('S m))
forall (n :: Nat). Fin n -> Fin ('S n)
FS (Fin ('S m) -> Fin ('S ('S m)))
-> (MaxBound m -> Fin ('S m)) -> MaxBound m -> Fin ('S ('S m))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MaxBound m -> Fin ('S m)
forall (n :: Nat). MaxBound n -> Fin ('S n)
getMaxBound)

newtype MaxBound n = MaxBound { MaxBound n -> Fin ('S n)
getMaxBound :: Fin ('S n) }

instance NFData (Fin n) where
    rnf :: Fin n -> ()
rnf Fin n
FZ     = ()
    rnf (FS Fin n
n) = Fin n -> ()
forall a. NFData a => a -> ()
rnf Fin n
n

instance Hashable (Fin n) where
    hashWithSalt :: Int -> Fin n -> Int
hashWithSalt Int
salt = Int -> Integer -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
salt (Integer -> Int) -> (Fin n -> Integer) -> Fin n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> (Integer -> Integer) -> Fin n -> Integer
forall a (n :: Nat). a -> (a -> a) -> Fin n -> a
cata (Integer
0 :: Integer) Integer -> Integer
forall a. Enum a => a -> a
succ

-------------------------------------------------------------------------------
-- QuickCheck
-------------------------------------------------------------------------------

instance (n ~ 'S m, N.SNatI m) => QC.Arbitrary (Fin n) where
    arbitrary :: Gen (Fin n)
arbitrary = Arb m -> Gen (Fin ('S m))
forall (n :: Nat). Arb n -> Gen (Fin ('S n))
getArb (Arb m -> Gen (Fin ('S m))) -> Arb m -> Gen (Fin ('S m))
forall a b. (a -> b) -> a -> b
$ Arb 'Z
-> (forall (m :: Nat). SNatI m => Arb m -> Arb ('S m)) -> Arb m
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction (Gen (Fin ('S 'Z)) -> Arb 'Z
forall (n :: Nat). Gen (Fin ('S n)) -> Arb n
Arb (Fin ('S 'Z) -> Gen (Fin ('S 'Z))
forall (m :: * -> *) a. Monad m => a -> m a
return Fin ('S 'Z)
forall (n :: Nat). Fin ('S n)
FZ)) forall (m :: Nat). SNatI m => Arb m -> Arb ('S m)
step where
        step :: forall p. N.SNatI p => Arb p -> Arb ('S p)
        step :: Arb p -> Arb ('S p)
step (Arb Gen (Fin ('S p))
p) = Gen (Fin ('S ('S p))) -> Arb ('S p)
forall (n :: Nat). Gen (Fin ('S n)) -> Arb n
Arb (Gen (Fin ('S ('S p))) -> Arb ('S p))
-> Gen (Fin ('S ('S p))) -> Arb ('S p)
forall a b. (a -> b) -> a -> b
$ [(Int, Gen (Fin ('S ('S p))))] -> Gen (Fin ('S ('S p)))
forall a. [(Int, Gen a)] -> Gen a
QC.frequency
            [ (Int
1,                                 Fin ('S ('S p)) -> Gen (Fin ('S ('S p)))
forall (m :: * -> *) a. Monad m => a -> m a
return Fin ('S ('S p))
forall (n :: Nat). Fin ('S n)
FZ)
            , (Proxy @Nat p -> Int
forall (n :: Nat) m (proxy :: Nat -> *).
(SNatI n, Num m) =>
proxy n -> m
N.reflectToNum (Proxy @Nat p
forall k (t :: k). Proxy @k t
Proxy :: Proxy p), (Fin ('S p) -> Fin ('S ('S p)))
-> Gen (Fin ('S p)) -> Gen (Fin ('S ('S p)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fin ('S p) -> Fin ('S ('S p))
forall (n :: Nat). Fin n -> Fin ('S n)
FS Gen (Fin ('S p))
p)
            ]

    shrink :: Fin n -> [Fin n]
shrink = Fin n -> [Fin n]
forall (n :: Nat). Fin n -> [Fin n]
shrink

shrink :: Fin n -> [Fin n]
shrink :: Fin n -> [Fin n]
shrink Fin n
FZ      = []
shrink (FS Fin n
FZ) = [Fin n
forall (n :: Nat). Fin ('S n)
FZ]
shrink (FS Fin n
n)  = (Fin n -> Fin ('S n)) -> [Fin n] -> [Fin ('S n)]
forall a b. (a -> b) -> [a] -> [b]
map Fin n -> Fin ('S n)
forall (n :: Nat). Fin n -> Fin ('S n)
FS (Fin n -> [Fin n]
forall (n :: Nat). Fin n -> [Fin n]
shrink Fin n
n)

newtype Arb n = Arb { Arb n -> Gen (Fin ('S n))
getArb :: QC.Gen (Fin ('S n)) }

instance QC.CoArbitrary (Fin n) where
    coarbitrary :: Fin n -> Gen b -> Gen b
coarbitrary Fin n
FZ     = Int -> Gen b -> Gen b
forall n a. Integral n => n -> Gen a -> Gen a
QC.variant (Int
0 :: Int)
    coarbitrary (FS Fin n
n) = Int -> Gen b -> Gen b
forall n a. Integral n => n -> Gen a -> Gen a
QC.variant (Int
1 :: Int) (Gen b -> Gen b) -> (Gen b -> Gen b) -> Gen b -> Gen b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> Gen b -> Gen b
forall a b. CoArbitrary a => a -> Gen b -> Gen b
QC.coarbitrary Fin n
n

instance (n ~ 'S m, N.SNatI m) => QC.Function (Fin n) where
    function :: (Fin n -> b) -> Fin n :-> b
function = case SNat m
forall (n :: Nat). SNatI n => SNat n
N.snat :: N.SNat m of
        SNat m
N.SZ -> (Fin ('S 'Z) -> ())
-> (() -> Fin ('S 'Z)) -> (Fin ('S 'Z) -> b) -> Fin ('S 'Z) :-> b
forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap (\Fin ('S 'Z)
FZ -> ()) (\() -> Fin ('S 'Z)
forall (n :: Nat). Fin ('S n)
FZ)
        SNat m
N.SS -> (Fin ('S ('S n)) -> Maybe (Fin ('S n)))
-> (Maybe (Fin ('S n)) -> Fin ('S ('S n)))
-> (Fin ('S ('S n)) -> b)
-> Fin ('S ('S n)) :-> b
forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap Fin ('S ('S n)) -> Maybe (Fin ('S n))
forall (n :: Nat). Fin ('S n) -> Maybe (Fin n)
isMin       (Fin ('S ('S n))
-> (Fin ('S n) -> Fin ('S ('S n)))
-> Maybe (Fin ('S n))
-> Fin ('S ('S n))
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Fin ('S ('S n))
forall (n :: Nat). Fin ('S n)
FZ Fin ('S n) -> Fin ('S ('S n))
forall (n :: Nat). Fin n -> Fin ('S n)
FS)

-- TODO: https://github.com/nick8325/quickcheck/pull/283
-- newtype Fun b m = Fun { getFun :: (Fin ('S m) -> b) -> Fin ('S m) QC.:-> b }

-------------------------------------------------------------------------------
-- universe-base
-------------------------------------------------------------------------------

-- | @since 0.1.2
instance N.SNatI n => U.Universe (Fin n) where
    universe :: [Fin n]
universe = [Fin n]
forall (n :: Nat). SNatI n => [Fin n]
universe

-- |
--
-- >>> (U.cardinality :: U.Tagged (Fin N.Nat3) Natural) == U.Tagged (genericLength (U.universeF :: [Fin N.Nat3]))
-- True
--
-- @since 0.1.2
--
instance N.SNatI n => U.Finite   (Fin n) where
    universeF :: [Fin n]
universeF   = [Fin n]
forall a. Universe a => [a]
U.universe
    cardinality :: Tagged @* (Fin n) Natural
cardinality = Natural -> Tagged @* (Fin n) Natural
forall k (s :: k) b. b -> Tagged @k s b
U.Tagged (Natural -> Tagged @* (Fin n) Natural)
-> Natural -> Tagged @* (Fin n) Natural
forall a b. (a -> b) -> a -> b
$ Proxy @Nat n -> Natural
forall (n :: Nat) m (proxy :: Nat -> *).
(SNatI n, Num m) =>
proxy n -> m
N.reflectToNum (Proxy @Nat n
forall k (t :: k). Proxy @k t
Proxy :: Proxy n)

-------------------------------------------------------------------------------
-- Showing
-------------------------------------------------------------------------------

-- | 'show' displaying a structure of 'Fin'.
--
-- >>> explicitShow (0 :: Fin N.Nat1)
-- "FZ"
--
-- >>> explicitShow (2 :: Fin N.Nat3)
-- "FS (FS FZ)"
--
explicitShow :: Fin n -> String
explicitShow :: Fin n -> String
explicitShow Fin n
n = Int -> Fin n -> ShowS
forall (n :: Nat). Int -> Fin n -> ShowS
explicitShowsPrec Int
0 Fin n
n String
""

-- | 'showsPrec' displaying a structure of 'Fin'.
explicitShowsPrec :: Int -> Fin n -> ShowS
explicitShowsPrec :: Int -> Fin n -> ShowS
explicitShowsPrec Int
_ Fin n
FZ     = String -> ShowS
showString String
"FZ"
explicitShowsPrec Int
d (FS Fin n
n) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10)
    (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"FS "
    ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Fin n -> ShowS
forall (n :: Nat). Int -> Fin n -> ShowS
explicitShowsPrec Int
11 Fin n
n

-------------------------------------------------------------------------------
-- Conversions
-------------------------------------------------------------------------------

-- | Fold 'Fin'.
cata :: forall a n. a -> (a -> a) -> Fin n -> a
cata :: a -> (a -> a) -> Fin n -> a
cata a
z a -> a
f = Fin n -> a
forall (m :: Nat). Fin m -> a
go where
    go :: Fin m -> a
    go :: Fin m -> a
go Fin m
FZ = a
z
    go (FS Fin n
n) = a -> a
f (Fin n -> a
forall (m :: Nat). Fin m -> a
go Fin n
n)

-- | Convert to 'Nat'.
toNat :: Fin n -> N.Nat
toNat :: Fin n -> Nat
toNat = Nat -> (Nat -> Nat) -> Fin n -> Nat
forall a (n :: Nat). a -> (a -> a) -> Fin n -> a
cata Nat
Z Nat -> Nat
S

-- | Convert from 'Nat'.
--
-- >>> fromNat N.nat1 :: Maybe (Fin N.Nat2)
-- Just 1
--
-- >>> fromNat N.nat1 :: Maybe (Fin N.Nat1)
-- Nothing
--
fromNat :: N.SNatI n => N.Nat -> Maybe (Fin n)
fromNat :: Nat -> Maybe (Fin n)
fromNat = NatToFin n -> Nat -> Maybe (Fin n)
forall (n :: Nat). NatToFin n -> Nat -> Maybe (Fin n)
appNatToFin (NatToFin 'Z
-> (forall (m :: Nat). SNatI m => NatToFin m -> NatToFin ('S m))
-> NatToFin n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction NatToFin 'Z
start forall (m :: Nat). SNatI m => NatToFin m -> NatToFin ('S m)
forall (n :: Nat). NatToFin n -> NatToFin ('S n)
step) where
    start :: NatToFin 'Z
    start :: NatToFin 'Z
start = (Nat -> Maybe (Fin 'Z)) -> NatToFin 'Z
forall (n :: Nat). (Nat -> Maybe (Fin n)) -> NatToFin n
NatToFin ((Nat -> Maybe (Fin 'Z)) -> NatToFin 'Z)
-> (Nat -> Maybe (Fin 'Z)) -> NatToFin 'Z
forall a b. (a -> b) -> a -> b
$ Maybe (Fin 'Z) -> Nat -> Maybe (Fin 'Z)
forall a b. a -> b -> a
const Maybe (Fin 'Z)
forall a. Maybe a
Nothing

    step :: NatToFin n -> NatToFin ('S n)
    step :: NatToFin n -> NatToFin ('S n)
step (NatToFin Nat -> Maybe (Fin n)
f) = (Nat -> Maybe (Fin ('S n))) -> NatToFin ('S n)
forall (n :: Nat). (Nat -> Maybe (Fin n)) -> NatToFin n
NatToFin ((Nat -> Maybe (Fin ('S n))) -> NatToFin ('S n))
-> (Nat -> Maybe (Fin ('S n))) -> NatToFin ('S n)
forall a b. (a -> b) -> a -> b
$ \Nat
n -> case Nat
n of
        Nat
Z   -> Fin ('S n) -> Maybe (Fin ('S n))
forall a. a -> Maybe a
Just Fin ('S n)
forall (n :: Nat). Fin ('S n)
FZ
        S Nat
m -> (Fin n -> Fin ('S n)) -> Maybe (Fin n) -> Maybe (Fin ('S n))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fin n -> Fin ('S n)
forall (n :: Nat). Fin n -> Fin ('S n)
FS (Nat -> Maybe (Fin n)
f Nat
m)

newtype NatToFin n = NatToFin { NatToFin n -> Nat -> Maybe (Fin n)
appNatToFin :: N.Nat -> Maybe (Fin n) }

-- | Convert to 'Natural'.
toNatural :: Fin n -> Natural
toNatural :: Fin n -> Natural
toNatural = Natural -> (Natural -> Natural) -> Fin n -> Natural
forall a (n :: Nat). a -> (a -> a) -> Fin n -> a
cata Natural
0 Natural -> Natural
forall a. Enum a => a -> a
succ

-- | Convert from any 'Ord' 'Num'.
unsafeFromNum :: forall n i. (Num i, Ord i, N.SNatI n) => i -> Fin n
unsafeFromNum :: i -> Fin n
unsafeFromNum = UnsafeFromNum i n -> i -> Fin n
forall i (n :: Nat). UnsafeFromNum i n -> i -> Fin n
appUnsafeFromNum (UnsafeFromNum i 'Z
-> (forall (m :: Nat).
    SNatI m =>
    UnsafeFromNum i m -> UnsafeFromNum i ('S m))
-> UnsafeFromNum i n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction UnsafeFromNum i 'Z
start forall (m :: Nat).
SNatI m =>
UnsafeFromNum i m -> UnsafeFromNum i ('S m)
forall (m :: Nat). UnsafeFromNum i m -> UnsafeFromNum i ('S m)
step) where
    start :: UnsafeFromNum i 'Z
    start :: UnsafeFromNum i 'Z
start = (i -> Fin 'Z) -> UnsafeFromNum i 'Z
forall i (n :: Nat). (i -> Fin n) -> UnsafeFromNum i n
UnsafeFromNum ((i -> Fin 'Z) -> UnsafeFromNum i 'Z)
-> (i -> Fin 'Z) -> UnsafeFromNum i 'Z
forall a b. (a -> b) -> a -> b
$ \i
n -> case i -> i -> Ordering
forall a. Ord a => a -> a -> Ordering
compare i
n i
0 of
        Ordering
LT -> ArithException -> Fin 'Z
forall a e. Exception e => e -> a
throw ArithException
Underflow
        Ordering
EQ -> ArithException -> Fin 'Z
forall a e. Exception e => e -> a
throw ArithException
Overflow
        Ordering
GT -> ArithException -> Fin 'Z
forall a e. Exception e => e -> a
throw ArithException
Overflow

    step :: UnsafeFromNum i m -> UnsafeFromNum i ('S m)
    step :: UnsafeFromNum i m -> UnsafeFromNum i ('S m)
step (UnsafeFromNum i -> Fin m
f) = (i -> Fin ('S m)) -> UnsafeFromNum i ('S m)
forall i (n :: Nat). (i -> Fin n) -> UnsafeFromNum i n
UnsafeFromNum ((i -> Fin ('S m)) -> UnsafeFromNum i ('S m))
-> (i -> Fin ('S m)) -> UnsafeFromNum i ('S m)
forall a b. (a -> b) -> a -> b
$ \i
n -> case i -> i -> Ordering
forall a. Ord a => a -> a -> Ordering
compare i
n i
0 of
        Ordering
EQ -> Fin ('S m)
forall (n :: Nat). Fin ('S n)
FZ
        Ordering
GT -> Fin m -> Fin ('S m)
forall (n :: Nat). Fin n -> Fin ('S n)
FS (i -> Fin m
f (i
n i -> i -> i
forall a. Num a => a -> a -> a
- i
1))
        Ordering
LT -> ArithException -> Fin ('S m)
forall a e. Exception e => e -> a
throw ArithException
Underflow

newtype UnsafeFromNum i n = UnsafeFromNum { UnsafeFromNum i n -> i -> Fin n
appUnsafeFromNum :: i -> Fin n }

-------------------------------------------------------------------------------
-- "Interesting" stuff
-------------------------------------------------------------------------------

-- | All values. @[minBound .. maxBound]@ won't work for @'Fin' 'N.Nat0'@.
--
-- >>> universe :: [Fin N.Nat3]
-- [0,1,2]
universe :: N.SNatI n => [Fin n]
universe :: [Fin n]
universe = Universe n -> [Fin n]
forall (n :: Nat). Universe n -> [Fin n]
getUniverse (Universe n -> [Fin n]) -> Universe n -> [Fin n]
forall a b. (a -> b) -> a -> b
$ Universe 'Z
-> (forall (m :: Nat). SNatI m => Universe m -> Universe ('S m))
-> Universe n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction ([Fin 'Z] -> Universe 'Z
forall (n :: Nat). [Fin n] -> Universe n
Universe []) forall (m :: Nat). SNatI m => Universe m -> Universe ('S m)
forall (n :: Nat). Universe n -> Universe ('S n)
step where
    step :: Universe n -> Universe ('S n)
    step :: Universe n -> Universe ('S n)
step (Universe [Fin n]
xs) = [Fin ('S n)] -> Universe ('S n)
forall (n :: Nat). [Fin n] -> Universe n
Universe (Fin ('S n)
forall (n :: Nat). Fin ('S n)
FZ Fin ('S n) -> [Fin ('S n)] -> [Fin ('S n)]
forall a. a -> [a] -> [a]
: (Fin n -> Fin ('S n)) -> [Fin n] -> [Fin ('S n)]
forall a b. (a -> b) -> [a] -> [b]
map Fin n -> Fin ('S n)
forall (n :: Nat). Fin n -> Fin ('S n)
FS [Fin n]
xs)

-- | Like 'universe' but 'NonEmpty'.
--
-- >>> universe1 :: NonEmpty (Fin N.Nat3)
-- 0 :| [1,2]
universe1 :: N.SNatI n => NonEmpty (Fin ('S n))
universe1 :: NonEmpty (Fin ('S n))
universe1 = Universe1 n -> NonEmpty (Fin ('S n))
forall (n :: Nat). Universe1 n -> NonEmpty (Fin ('S n))
getUniverse1 (Universe1 n -> NonEmpty (Fin ('S n)))
-> Universe1 n -> NonEmpty (Fin ('S n))
forall a b. (a -> b) -> a -> b
$ Universe1 'Z
-> (forall (m :: Nat). SNatI m => Universe1 m -> Universe1 ('S m))
-> Universe1 n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction (NonEmpty (Fin ('S 'Z)) -> Universe1 'Z
forall (n :: Nat). NonEmpty (Fin ('S n)) -> Universe1 n
Universe1 (Fin ('S 'Z)
forall (n :: Nat). Fin ('S n)
FZ Fin ('S 'Z) -> [Fin ('S 'Z)] -> NonEmpty (Fin ('S 'Z))
forall a. a -> [a] -> NonEmpty a
:| [])) forall (m :: Nat). SNatI m => Universe1 m -> Universe1 ('S m)
forall (n :: Nat). Universe1 n -> Universe1 ('S n)
step where
    step :: Universe1 n -> Universe1 ('S n)
    step :: Universe1 n -> Universe1 ('S n)
step (Universe1 NonEmpty (Fin ('S n))
xs) = NonEmpty (Fin ('S ('S n))) -> Universe1 ('S n)
forall (n :: Nat). NonEmpty (Fin ('S n)) -> Universe1 n
Universe1 (Fin ('S ('S n))
-> NonEmpty (Fin ('S ('S n))) -> NonEmpty (Fin ('S ('S n)))
forall a. a -> NonEmpty a -> NonEmpty a
NE.cons Fin ('S ('S n))
forall (n :: Nat). Fin ('S n)
FZ ((Fin ('S n) -> Fin ('S ('S n)))
-> NonEmpty (Fin ('S n)) -> NonEmpty (Fin ('S ('S n)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fin ('S n) -> Fin ('S ('S n))
forall (n :: Nat). Fin n -> Fin ('S n)
FS NonEmpty (Fin ('S n))
xs))

-- | 'universe' which will be fully inlined, if @n@ is known at compile time.
--
-- >>> inlineUniverse :: [Fin N.Nat3]
-- [0,1,2]
inlineUniverse :: N.SNatI n => [Fin n]
inlineUniverse :: [Fin n]
inlineUniverse = Universe n -> [Fin n]
forall (n :: Nat). Universe n -> [Fin n]
getUniverse (Universe n -> [Fin n]) -> Universe n -> [Fin n]
forall a b. (a -> b) -> a -> b
$ Universe 'Z
-> (forall (m :: Nat). SNatI m => Universe m -> Universe ('S m))
-> Universe n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction ([Fin 'Z] -> Universe 'Z
forall (n :: Nat). [Fin n] -> Universe n
Universe []) forall (m :: Nat). SNatI m => Universe m -> Universe ('S m)
forall (n :: Nat). Universe n -> Universe ('S n)
step where
    step :: Universe n -> Universe ('S n)
    step :: Universe n -> Universe ('S n)
step (Universe [Fin n]
xs) = [Fin ('S n)] -> Universe ('S n)
forall (n :: Nat). [Fin n] -> Universe n
Universe (Fin ('S n)
forall (n :: Nat). Fin ('S n)
FZ Fin ('S n) -> [Fin ('S n)] -> [Fin ('S n)]
forall a. a -> [a] -> [a]
: (Fin n -> Fin ('S n)) -> [Fin n] -> [Fin ('S n)]
forall a b. (a -> b) -> [a] -> [b]
map Fin n -> Fin ('S n)
forall (n :: Nat). Fin n -> Fin ('S n)
FS [Fin n]
xs)

-- | >>> inlineUniverse1 :: NonEmpty (Fin N.Nat3)
-- 0 :| [1,2]
inlineUniverse1 :: N.SNatI n => NonEmpty (Fin ('S n))
inlineUniverse1 :: NonEmpty (Fin ('S n))
inlineUniverse1 = Universe1 n -> NonEmpty (Fin ('S n))
forall (n :: Nat). Universe1 n -> NonEmpty (Fin ('S n))
getUniverse1 (Universe1 n -> NonEmpty (Fin ('S n)))
-> Universe1 n -> NonEmpty (Fin ('S n))
forall a b. (a -> b) -> a -> b
$ Universe1 'Z
-> (forall (m :: Nat). SNatI m => Universe1 m -> Universe1 ('S m))
-> Universe1 n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction (NonEmpty (Fin ('S 'Z)) -> Universe1 'Z
forall (n :: Nat). NonEmpty (Fin ('S n)) -> Universe1 n
Universe1 (Fin ('S 'Z)
forall (n :: Nat). Fin ('S n)
FZ Fin ('S 'Z) -> [Fin ('S 'Z)] -> NonEmpty (Fin ('S 'Z))
forall a. a -> [a] -> NonEmpty a
:| [])) forall (m :: Nat). SNatI m => Universe1 m -> Universe1 ('S m)
forall (n :: Nat). Universe1 n -> Universe1 ('S n)
step where
    step :: Universe1 n -> Universe1 ('S n)
    step :: Universe1 n -> Universe1 ('S n)
step (Universe1 NonEmpty (Fin ('S n))
xs) = NonEmpty (Fin ('S ('S n))) -> Universe1 ('S n)
forall (n :: Nat). NonEmpty (Fin ('S n)) -> Universe1 n
Universe1 (Fin ('S ('S n))
-> NonEmpty (Fin ('S ('S n))) -> NonEmpty (Fin ('S ('S n)))
forall a. a -> NonEmpty a -> NonEmpty a
NE.cons Fin ('S ('S n))
forall (n :: Nat). Fin ('S n)
FZ ((Fin ('S n) -> Fin ('S ('S n)))
-> NonEmpty (Fin ('S n)) -> NonEmpty (Fin ('S ('S n)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fin ('S n) -> Fin ('S ('S n))
forall (n :: Nat). Fin n -> Fin ('S n)
FS NonEmpty (Fin ('S n))
xs))

newtype Universe  n = Universe  { Universe n -> [Fin n]
getUniverse  :: [Fin n] }
newtype Universe1 n = Universe1 { Universe1 n -> NonEmpty (Fin ('S n))
getUniverse1 :: NonEmpty (Fin ('S n)) }

-- | @'Fin' 'N.Nat0'@ is not inhabited.
absurd :: Fin N.Nat0 -> b
absurd :: Fin 'Z -> b
absurd Fin 'Z
n = case Fin 'Z
n of {}

-- | Counting to one is boring.
--
-- >>> boring
-- 0
boring :: Fin N.Nat1
boring :: Fin ('S 'Z)
boring = Fin ('S 'Z)
forall (n :: Nat). Fin ('S n)
FZ

-------------------------------------------------------------------------------
-- min and max
-------------------------------------------------------------------------------

-- | Return a one less.
--
-- >>> isMin (FZ :: Fin N.Nat1)
-- Nothing
--
-- >>> map isMin universe :: [Maybe (Fin N.Nat3)]
-- [Nothing,Just 0,Just 1,Just 2]
--
-- @since 0.1.1
--
isMin :: Fin ('S n) -> Maybe (Fin n)
isMin :: Fin ('S n) -> Maybe (Fin n)
isMin Fin ('S n)
FZ     = Maybe (Fin n)
forall a. Maybe a
Nothing
isMin (FS Fin n
n) = Fin n -> Maybe (Fin n)
forall a. a -> Maybe a
Just Fin n
n

-- | Return a one less.
--
-- >>> isMax (FZ :: Fin N.Nat1)
-- Nothing
--
-- >>> map isMax universe :: [Maybe (Fin N.Nat3)]
-- [Just 0,Just 1,Just 2,Nothing]
--
-- @since 0.1.1
--
isMax :: forall n. N.SNatI n => Fin ('S n) -> Maybe (Fin n)
isMax :: Fin ('S n) -> Maybe (Fin n)
isMax = IsMax n -> Fin ('S n) -> Maybe (Fin n)
forall (n :: Nat). IsMax n -> Fin ('S n) -> Maybe (Fin n)
getIsMax (IsMax 'Z
-> (forall (m :: Nat). SNatI m => IsMax m -> IsMax ('S m))
-> IsMax n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction IsMax 'Z
start forall (m :: Nat). SNatI m => IsMax m -> IsMax ('S m)
forall (m :: Nat). IsMax m -> IsMax ('S m)
step) where
    start :: IsMax 'Z
    start :: IsMax 'Z
start = (Fin ('S 'Z) -> Maybe (Fin 'Z)) -> IsMax 'Z
forall (n :: Nat). (Fin ('S n) -> Maybe (Fin n)) -> IsMax n
IsMax ((Fin ('S 'Z) -> Maybe (Fin 'Z)) -> IsMax 'Z)
-> (Fin ('S 'Z) -> Maybe (Fin 'Z)) -> IsMax 'Z
forall a b. (a -> b) -> a -> b
$ \Fin ('S 'Z)
_ -> Maybe (Fin 'Z)
forall a. Maybe a
Nothing

    step :: IsMax m -> IsMax ('S m)
    step :: IsMax m -> IsMax ('S m)
step (IsMax Fin ('S m) -> Maybe (Fin m)
rec) = (Fin ('S ('S m)) -> Maybe (Fin ('S m))) -> IsMax ('S m)
forall (n :: Nat). (Fin ('S n) -> Maybe (Fin n)) -> IsMax n
IsMax ((Fin ('S ('S m)) -> Maybe (Fin ('S m))) -> IsMax ('S m))
-> (Fin ('S ('S m)) -> Maybe (Fin ('S m))) -> IsMax ('S m)
forall a b. (a -> b) -> a -> b
$ \Fin ('S ('S m))
n -> case Fin ('S ('S m))
n of
        Fin ('S ('S m))
FZ   -> Fin ('S m) -> Maybe (Fin ('S m))
forall a. a -> Maybe a
Just Fin ('S m)
forall (n :: Nat). Fin ('S n)
FZ
        FS Fin n
m -> (Fin m -> Fin ('S m)) -> Maybe (Fin m) -> Maybe (Fin ('S m))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fin m -> Fin ('S m)
forall (n :: Nat). Fin n -> Fin ('S n)
FS (Fin ('S m) -> Maybe (Fin m)
rec Fin n
Fin ('S m)
m)

newtype IsMax n = IsMax { IsMax n -> Fin ('S n) -> Maybe (Fin n)
getIsMax :: Fin ('S n) -> Maybe (Fin n) }

-------------------------------------------------------------------------------
-- Append & Split
-------------------------------------------------------------------------------

-- | >>> map weakenRight1 universe :: [Fin N.Nat5]
-- [1,2,3,4]
--
-- @since 0.1.1
weakenRight1 :: Fin n -> Fin ('S n)
weakenRight1 :: Fin n -> Fin ('S n)
weakenRight1 = Fin n -> Fin ('S n)
forall (n :: Nat). Fin n -> Fin ('S n)
FS

-- | >>> map weakenLeft1 universe :: [Fin N.Nat5]
-- [0,1,2,3]
--
-- @since 0.1.1
weakenLeft1 :: N.SNatI n => Fin n -> Fin ('S n)
weakenLeft1 :: Fin n -> Fin ('S n)
weakenLeft1 = Weaken1 n -> Fin n -> Fin ('S n)
forall (n :: Nat). Weaken1 n -> Fin n -> Fin ('S n)
getWeaken1 (Weaken1 'Z
-> (forall (m :: Nat). SNatI m => Weaken1 m -> Weaken1 ('S m))
-> Weaken1 n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction Weaken1 'Z
start forall (m :: Nat). SNatI m => Weaken1 m -> Weaken1 ('S m)
forall (n :: Nat). Weaken1 n -> Weaken1 ('S n)
step) where
    start :: Weaken1 'Z
    start :: Weaken1 'Z
start = (Fin 'Z -> Fin ('S 'Z)) -> Weaken1 'Z
forall (n :: Nat). (Fin n -> Fin ('S n)) -> Weaken1 n
Weaken1 Fin 'Z -> Fin ('S 'Z)
forall b. Fin 'Z -> b
absurd

    step :: Weaken1 n -> Weaken1 ('S n)
    step :: Weaken1 n -> Weaken1 ('S n)
step (Weaken1 Fin n -> Fin ('S n)
go) = (Fin ('S n) -> Fin ('S ('S n))) -> Weaken1 ('S n)
forall (n :: Nat). (Fin n -> Fin ('S n)) -> Weaken1 n
Weaken1 ((Fin ('S n) -> Fin ('S ('S n))) -> Weaken1 ('S n))
-> (Fin ('S n) -> Fin ('S ('S n))) -> Weaken1 ('S n)
forall a b. (a -> b) -> a -> b
$ \Fin ('S n)
n -> case Fin ('S n)
n of
        Fin ('S n)
FZ    -> Fin ('S ('S n))
forall (n :: Nat). Fin ('S n)
FZ
        FS Fin n
n' -> Fin ('S n) -> Fin ('S ('S n))
forall (n :: Nat). Fin n -> Fin ('S n)
FS (Fin n -> Fin ('S n)
go Fin n
Fin n
n')

newtype Weaken1 n = Weaken1 { Weaken1 n -> Fin n -> Fin ('S n)
getWeaken1 :: Fin n -> Fin ('S n) }

-- | >>> map (weakenLeft (Proxy :: Proxy N.Nat2)) (universe :: [Fin N.Nat3])
-- [0,1,2]
weakenLeft :: forall n m. N.SNatI n => Proxy m -> Fin n -> Fin (N.Plus n m)
weakenLeft :: Proxy @Nat m -> Fin n -> Fin (Plus n m)
weakenLeft Proxy @Nat m
_ = WeakenLeft m n -> Fin n -> Fin (Plus n m)
forall (m :: Nat) (n :: Nat).
WeakenLeft m n -> Fin n -> Fin (Plus n m)
getWeakenLeft (WeakenLeft m 'Z
-> (forall (m :: Nat).
    SNatI m =>
    WeakenLeft m m -> WeakenLeft m ('S m))
-> WeakenLeft m n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction WeakenLeft m 'Z
start forall (m :: Nat). SNatI m => WeakenLeft m m -> WeakenLeft m ('S m)
forall (p :: Nat). WeakenLeft m p -> WeakenLeft m ('S p)
step :: WeakenLeft m n) where
    start :: WeakenLeft m 'Z
    start :: WeakenLeft m 'Z
start = (Fin 'Z -> Fin (Plus 'Z m)) -> WeakenLeft m 'Z
forall (m :: Nat) (n :: Nat).
(Fin n -> Fin (Plus n m)) -> WeakenLeft m n
WeakenLeft Fin 'Z -> Fin (Plus 'Z m)
forall b. Fin 'Z -> b
absurd

    step :: WeakenLeft m p -> WeakenLeft m ('S p)
    step :: WeakenLeft m p -> WeakenLeft m ('S p)
step (WeakenLeft Fin p -> Fin (Plus p m)
go) = (Fin ('S p) -> Fin (Plus ('S p) m)) -> WeakenLeft m ('S p)
forall (m :: Nat) (n :: Nat).
(Fin n -> Fin (Plus n m)) -> WeakenLeft m n
WeakenLeft ((Fin ('S p) -> Fin (Plus ('S p) m)) -> WeakenLeft m ('S p))
-> (Fin ('S p) -> Fin (Plus ('S p) m)) -> WeakenLeft m ('S p)
forall a b. (a -> b) -> a -> b
$ \Fin ('S p)
n -> case Fin ('S p)
n of
        Fin ('S p)
FZ    -> Fin (Plus ('S p) m)
forall (n :: Nat). Fin ('S n)
FZ
        FS Fin n
n' -> Fin (Plus p m) -> Fin ('S (Plus p m))
forall (n :: Nat). Fin n -> Fin ('S n)
FS (Fin p -> Fin (Plus p m)
go Fin p
Fin n
n')

newtype WeakenLeft m n = WeakenLeft { WeakenLeft m n -> Fin n -> Fin (Plus n m)
getWeakenLeft :: Fin n -> Fin (N.Plus n m) }

-- | >>> map (weakenRight (Proxy :: Proxy N.Nat2)) (universe :: [Fin N.Nat3])
-- [2,3,4]
weakenRight :: forall n m. N.SNatI n => Proxy n -> Fin m -> Fin (N.Plus n m)
weakenRight :: Proxy @Nat n -> Fin m -> Fin (Plus n m)
weakenRight Proxy @Nat n
_ = WeakenRight m n -> Fin m -> Fin (Plus n m)
forall (m :: Nat) (n :: Nat).
WeakenRight m n -> Fin m -> Fin (Plus n m)
getWeakenRight (WeakenRight m 'Z
-> (forall (m :: Nat).
    SNatI m =>
    WeakenRight m m -> WeakenRight m ('S m))
-> WeakenRight m n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction WeakenRight m 'Z
start forall (m :: Nat).
SNatI m =>
WeakenRight m m -> WeakenRight m ('S m)
forall (n :: Nat) (m :: Nat) (n :: Nat).
((Plus n m :: Nat) ~ ('S (Plus n m) :: Nat)) =>
WeakenRight m n -> WeakenRight m n
step :: WeakenRight m n) where
    start :: WeakenRight m 'Z
start = (Fin m -> Fin (Plus 'Z m)) -> WeakenRight m 'Z
forall (m :: Nat) (n :: Nat).
(Fin m -> Fin (Plus n m)) -> WeakenRight m n
WeakenRight Fin m -> Fin (Plus 'Z m)
forall a. a -> a
id
    step :: WeakenRight m n -> WeakenRight m n
step (WeakenRight Fin m -> Fin (Plus n m)
go) = (Fin m -> Fin (Plus n m)) -> WeakenRight m n
forall (m :: Nat) (n :: Nat).
(Fin m -> Fin (Plus n m)) -> WeakenRight m n
WeakenRight ((Fin m -> Fin (Plus n m)) -> WeakenRight m n)
-> (Fin m -> Fin (Plus n m)) -> WeakenRight m n
forall a b. (a -> b) -> a -> b
$ \Fin m
x -> Fin (Plus n m) -> Fin ('S (Plus n m))
forall (n :: Nat). Fin n -> Fin ('S n)
FS (Fin (Plus n m) -> Fin ('S (Plus n m)))
-> Fin (Plus n m) -> Fin ('S (Plus n m))
forall a b. (a -> b) -> a -> b
$ Fin m -> Fin (Plus n m)
go Fin m
x

newtype WeakenRight m n = WeakenRight { WeakenRight m n -> Fin m -> Fin (Plus n m)
getWeakenRight :: Fin m -> Fin (N.Plus n m) }

-- | Append two 'Fin's together.
--
-- >>> append (Left fin2 :: Either (Fin N.Nat5) (Fin N.Nat4))
-- 2
--
-- >>> append (Right fin2 :: Either (Fin N.Nat5) (Fin N.Nat4))
-- 7
--
append :: forall n m. N.SNatI n => Either (Fin n) (Fin m) -> Fin (N.Plus n m)
append :: Either (Fin n) (Fin m) -> Fin (Plus n m)
append (Left Fin n
n)  = Proxy @Nat m -> Fin n -> Fin (Plus n m)
forall (n :: Nat) (m :: Nat).
SNatI n =>
Proxy @Nat m -> Fin n -> Fin (Plus n m)
weakenLeft (Proxy @Nat m
forall k (t :: k). Proxy @k t
Proxy :: Proxy m) Fin n
n
append (Right Fin m
m) = Proxy @Nat n -> Fin m -> Fin (Plus n m)
forall (n :: Nat) (m :: Nat).
SNatI n =>
Proxy @Nat n -> Fin m -> Fin (Plus n m)
weakenRight (Proxy @Nat n
forall k (t :: k). Proxy @k t
Proxy :: Proxy n) Fin m
m

-- | Inverse of 'append'.
--
-- >>> split fin2 :: Either (Fin N.Nat2) (Fin N.Nat3)
-- Right 0
--
-- >>> split fin1 :: Either (Fin N.Nat2) (Fin N.Nat3)
-- Left 1
--
-- >>> map split universe :: [Either (Fin N.Nat2) (Fin N.Nat3)]
-- [Left 0,Left 1,Right 0,Right 1,Right 2]
--
split :: forall n m. N.SNatI n => Fin (N.Plus n m) -> Either (Fin n) (Fin m)
split :: Fin (Plus n m) -> Either (Fin n) (Fin m)
split = Split m n -> Fin (Plus n m) -> Either (Fin n) (Fin m)
forall (m :: Nat) (n :: Nat).
Split m n -> Fin (Plus n m) -> Either (Fin n) (Fin m)
getSplit (Split m 'Z
-> (forall (m :: Nat). SNatI m => Split m m -> Split m ('S m))
-> Split m n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction Split m 'Z
start forall (m :: Nat). SNatI m => Split m m -> Split m ('S m)
forall (p :: Nat). Split m p -> Split m ('S p)
step) where
    start :: Split m 'Z
    start :: Split m 'Z
start = (Fin (Plus 'Z m) -> Either (Fin 'Z) (Fin m)) -> Split m 'Z
forall (m :: Nat) (n :: Nat).
(Fin (Plus n m) -> Either (Fin n) (Fin m)) -> Split m n
Split Fin (Plus 'Z m) -> Either (Fin 'Z) (Fin m)
forall a b. b -> Either a b
Right

    step :: Split m p -> Split m ('S p)
    step :: Split m p -> Split m ('S p)
step (Split Fin (Plus p m) -> Either (Fin p) (Fin m)
go) = (Fin (Plus ('S p) m) -> Either (Fin ('S p)) (Fin m))
-> Split m ('S p)
forall (m :: Nat) (n :: Nat).
(Fin (Plus n m) -> Either (Fin n) (Fin m)) -> Split m n
Split ((Fin (Plus ('S p) m) -> Either (Fin ('S p)) (Fin m))
 -> Split m ('S p))
-> (Fin (Plus ('S p) m) -> Either (Fin ('S p)) (Fin m))
-> Split m ('S p)
forall a b. (a -> b) -> a -> b
$ \Fin (Plus ('S p) m)
x -> case Fin (Plus ('S p) m)
x of
        Fin (Plus ('S p) m)
FZ    -> Fin ('S p) -> Either (Fin ('S p)) (Fin m)
forall a b. a -> Either a b
Left Fin ('S p)
forall (n :: Nat). Fin ('S n)
FZ
        FS Fin n
x' -> (Fin p -> Fin ('S p))
-> (Fin m -> Fin m)
-> Either (Fin p) (Fin m)
-> Either (Fin ('S p)) (Fin m)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Fin p -> Fin ('S p)
forall (n :: Nat). Fin n -> Fin ('S n)
FS Fin m -> Fin m
forall a. a -> a
id (Either (Fin p) (Fin m) -> Either (Fin ('S p)) (Fin m))
-> Either (Fin p) (Fin m) -> Either (Fin ('S p)) (Fin m)
forall a b. (a -> b) -> a -> b
$ Fin (Plus p m) -> Either (Fin p) (Fin m)
go Fin n
Fin (Plus p m)
x'

newtype Split m n = Split { Split m n -> Fin (Plus n m) -> Either (Fin n) (Fin m)
getSplit :: Fin (N.Plus n m) -> Either (Fin n) (Fin m) }

-------------------------------------------------------------------------------
-- Aliases
-------------------------------------------------------------------------------

fin0 :: Fin (N.Plus N.Nat0 ('S n))
fin1 :: Fin (N.Plus N.Nat1 ('S n))
fin2 :: Fin (N.Plus N.Nat2 ('S n))
fin3 :: Fin (N.Plus N.Nat3 ('S n))
fin4 :: Fin (N.Plus N.Nat4 ('S n))
fin5 :: Fin (N.Plus N.Nat5 ('S n))
fin6 :: Fin (N.Plus N.Nat6 ('S n))
fin7 :: Fin (N.Plus N.Nat7 ('S n))
fin8 :: Fin (N.Plus N.Nat8 ('S n))
fin9 :: Fin (N.Plus N.Nat9 ('S n))

fin0 :: Fin (Plus 'Z ('S n))
fin0 = Fin (Plus 'Z ('S n))
forall (n :: Nat). Fin ('S n)
FZ
fin1 :: Fin (Plus ('S 'Z) ('S n))
fin1 = Fin ('S n) -> Fin ('S ('S n))
forall (n :: Nat). Fin n -> Fin ('S n)
FS Fin ('S n)
forall (n :: Nat). Fin (Plus 'Z ('S n))
fin0
fin2 :: Fin (Plus Nat2 ('S n))
fin2 = Fin ('S ('S n)) -> Fin ('S ('S ('S n)))
forall (n :: Nat). Fin n -> Fin ('S n)
FS Fin ('S ('S n))
forall (n :: Nat). Fin (Plus ('S 'Z) ('S n))
fin1
fin3 :: Fin (Plus Nat3 ('S n))
fin3 = Fin ('S ('S ('S n))) -> Fin ('S ('S ('S ('S n))))
forall (n :: Nat). Fin n -> Fin ('S n)
FS Fin ('S ('S ('S n)))
forall (n :: Nat). Fin (Plus Nat2 ('S n))
fin2
fin4 :: Fin (Plus Nat4 ('S n))
fin4 = Fin ('S ('S ('S ('S n)))) -> Fin ('S ('S ('S ('S ('S n)))))
forall (n :: Nat). Fin n -> Fin ('S n)
FS Fin ('S ('S ('S ('S n))))
forall (n :: Nat). Fin (Plus Nat3 ('S n))
fin3
fin5 :: Fin (Plus Nat5 ('S n))
fin5 = Fin ('S ('S ('S ('S ('S n)))))
-> Fin ('S ('S ('S ('S ('S ('S n))))))
forall (n :: Nat). Fin n -> Fin ('S n)
FS Fin ('S ('S ('S ('S ('S n)))))
forall (n :: Nat). Fin (Plus Nat4 ('S n))
fin4
fin6 :: Fin (Plus Nat6 ('S n))
fin6 = Fin ('S ('S ('S ('S ('S ('S n))))))
-> Fin ('S ('S ('S ('S ('S ('S ('S n)))))))
forall (n :: Nat). Fin n -> Fin ('S n)
FS Fin ('S ('S ('S ('S ('S ('S n))))))
forall (n :: Nat). Fin (Plus Nat5 ('S n))
fin5
fin7 :: Fin (Plus Nat7 ('S n))
fin7 = Fin ('S ('S ('S ('S ('S ('S ('S n)))))))
-> Fin ('S ('S ('S ('S ('S ('S ('S ('S n))))))))
forall (n :: Nat). Fin n -> Fin ('S n)
FS Fin ('S ('S ('S ('S ('S ('S ('S n)))))))
forall (n :: Nat). Fin (Plus Nat6 ('S n))
fin6
fin8 :: Fin (Plus Nat8 ('S n))
fin8 = Fin ('S ('S ('S ('S ('S ('S ('S ('S n))))))))
-> Fin ('S ('S ('S ('S ('S ('S ('S ('S ('S n)))))))))
forall (n :: Nat). Fin n -> Fin ('S n)
FS Fin ('S ('S ('S ('S ('S ('S ('S ('S n))))))))
forall (n :: Nat). Fin (Plus Nat7 ('S n))
fin7
fin9 :: Fin (Plus Nat9 ('S n))
fin9 = Fin ('S ('S ('S ('S ('S ('S ('S ('S ('S n)))))))))
-> Fin ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))))
forall (n :: Nat). Fin n -> Fin ('S n)
FS Fin ('S ('S ('S ('S ('S ('S ('S ('S ('S n)))))))))
forall (n :: Nat). Fin (Plus Nat8 ('S n))
fin8