{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Fin (
Fin (..),
cata,
explicitShow,
explicitShowsPrec,
toNat,
fromNat,
toNatural,
toInteger,
mirror,
inverse,
universe,
inlineUniverse,
universe1,
inlineUniverse1,
absurd,
boring,
weakenLeft,
weakenLeft1,
weakenRight,
weakenRight1,
append,
split,
isMin,
isMax,
fin0, fin1, fin2, fin3, fin4, fin5, fin6, fin7, fin8, fin9,
) where
import Control.DeepSeq (NFData (..))
import Data.Bifunctor (bimap)
import Data.GADT.Show (GShow (..))
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)
#if MIN_VERSION_some(1,0,5)
import Data.EqP (EqP (..))
import Data.OrdP (OrdP (..))
#endif
import qualified Data.Boring as Boring
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
data Fin (n :: Nat) where
FZ :: Fin ('S n)
FS :: Fin n -> Fin ('S n)
deriving (Typeable)
deriving instance Eq (Fin n)
deriving instance Ord (Fin n)
#if MIN_VERSION_some(1,0,5)
instance EqP Fin where
eqp :: forall (a :: Nat) (b :: Nat). Fin a -> Fin b -> Bool
eqp Fin a
FZ Fin b
FZ = Bool
True
eqp Fin a
FZ (FS Fin n
_) = Bool
False
eqp (FS Fin n
_) Fin b
FZ = Bool
False
eqp (FS Fin n
n) (FS Fin n
m) = forall k (f :: k -> *) (a :: k) (b :: k).
EqP @k f =>
f a -> f b -> Bool
eqp Fin n
n Fin n
m
instance OrdP Fin where
comparep :: forall (a :: Nat) (b :: Nat). Fin a -> Fin b -> Ordering
comparep Fin a
FZ Fin b
FZ = Ordering
EQ
comparep Fin a
FZ (FS Fin n
_) = Ordering
LT
comparep (FS Fin n
_) Fin b
FZ = Ordering
GT
comparep (FS Fin n
n) (FS Fin n
m) = forall k (f :: k -> *) (a :: k) (b :: k).
OrdP @k f =>
f a -> f b -> Ordering
comparep Fin n
n Fin n
m
#endif
instance Show (Fin n) where
showsPrec :: Int -> Fin n -> ShowS
showsPrec Int
d = forall a. Show a => Int -> a -> ShowS
showsPrec Int
d forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). Fin n -> Natural
toNatural
instance GShow Fin where
gshowsPrec :: forall (n :: Nat). Int -> Fin n -> ShowS
gshowsPrec = forall a. Show a => Int -> a -> ShowS
showsPrec
instance N.SNatI n => Num (Fin n) where
abs :: Fin n -> Fin n
abs = forall a. a -> a
id
signum :: Fin n -> Fin n
signum Fin n
FZ = forall (n :: Nat). Fin ('S n)
FZ
signum (FS Fin n
FZ) = forall (n :: Nat). Fin n -> Fin ('S n)
FS forall (n :: Nat). Fin ('S n)
FZ
signum (FS (FS Fin n
_)) = forall (n :: Nat). Fin n -> Fin ('S n)
FS forall (n :: Nat). Fin ('S n)
FZ
fromInteger :: Integer -> Fin n
fromInteger = forall (n :: Nat) i. (Num i, Ord i, SNatI n) => i -> Fin n
unsafeFromNum forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Integral a => a -> a -> a
`mod` forall (n :: Nat) m (proxy :: Nat -> *).
(SNatI n, Num m) =>
proxy n -> m
N.reflectToNum (forall {k} (t :: k). Proxy @k t
Proxy :: Proxy n))
Fin n
n + :: Fin n -> Fin n -> Fin n
+ Fin n
m = forall a. Num a => Integer -> a
fromInteger (forall a. Integral a => a -> Integer
toInteger Fin n
n forall a. Num a => a -> a -> a
+ forall a. Integral a => a -> Integer
toInteger Fin n
m)
Fin n
n * :: Fin n -> Fin n -> Fin n
* Fin n
m = forall a. Num a => Integer -> a
fromInteger (forall a. Integral a => a -> Integer
toInteger Fin n
n forall a. Num a => a -> a -> a
* forall a. Integral a => a -> Integer
toInteger Fin n
m)
Fin n
n - :: Fin n -> Fin n -> Fin n
- Fin n
m = forall a. Num a => Integer -> a
fromInteger (forall a. Integral a => a -> Integer
toInteger Fin n
n forall a. Num a => a -> a -> a
- forall a. Integral a => a -> Integer
toInteger Fin n
m)
negate :: Fin n -> Fin n
negate = forall a. Num a => Integer -> a
fromInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => a -> a
negate forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger
instance N.SNatI n => Real (Fin n) where
toRational :: Fin n -> Rational
toRational = forall a (n :: Nat). a -> (a -> a) -> Fin n -> a
cata Rational
0 forall a. Enum a => a -> a
succ
instance N.SNatI n => Integral (Fin n) where
toInteger :: Fin n -> Integer
toInteger = forall a (n :: Nat). a -> (a -> a) -> Fin n -> a
cata Integer
0 forall a. Enum a => a -> a
succ
quotRem :: Fin n -> Fin n -> (Fin n, Fin n)
quotRem Fin n
a Fin n
b = (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 forall a. Num a => a -> a -> a
* forall (n :: Nat). SNatI n => Fin n -> Fin n
inverse Fin n
b
mirror :: forall n. N.SNatI n => Fin n -> Fin n
mirror :: forall (n :: Nat). SNatI n => Fin n -> Fin n
mirror = forall (n :: Nat). Mirror n -> Fin n -> Fin n
getMirror (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 = forall (n :: Nat). (Fin n -> Fin n) -> Mirror n
Mirror forall a. a -> a
id
step :: forall m. N.SNatI m => Mirror m -> Mirror ('S m)
step :: forall (m :: Nat). SNatI m => Mirror m -> Mirror ('S m)
step (Mirror Fin m -> Fin m
rec) = forall (n :: Nat). (Fin n -> Fin n) -> Mirror n
Mirror forall a b. (a -> b) -> a -> b
$ \Fin ('S m)
n -> case Fin ('S m)
n of
Fin ('S m)
FZ -> forall (n :: Nat). MaxBound n -> Fin ('S n)
getMaxBound (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction (forall (n :: Nat). Fin ('S n) -> MaxBound n
MaxBound forall (n :: Nat). Fin ('S n)
FZ) (forall (n :: Nat). Fin ('S n) -> MaxBound n
MaxBound forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). Fin n -> Fin ('S n)
FS forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). MaxBound n -> Fin ('S n)
getMaxBound))
FS Fin n
m -> forall (n :: Nat). SNatI n => Fin n -> Fin ('S n)
weakenLeft1 (Fin m -> Fin m
rec Fin n
m)
newtype Mirror n = Mirror { forall (n :: Nat). Mirror n -> Fin n -> Fin n
getMirror :: Fin n -> Fin n }
inverse :: forall n. N.SNatI n => Fin n -> Fin n
inverse :: forall (n :: Nat). SNatI n => Fin n -> Fin n
inverse = forall a. Num a => Integer -> a
fromInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> Integer -> Integer -> Integer
iter Integer
0 Integer
n Integer
1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger where
n :: Integer
n = forall (n :: Nat) m (proxy :: Nat -> *).
(SNatI n, Num m) =>
proxy n -> m
N.reflectToNum (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 forall a. Ord a => a -> a -> Bool
< Integer
0 = Integer
t 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 forall a. Integral a => a -> a -> a
`div` Integer
r'
in Integer -> Integer -> Integer -> Integer -> Integer
iter Integer
t' Integer
r' (Integer
t forall a. Num a => a -> a -> a
- Integer
q forall a. Num a => a -> a -> a
* Integer
t') (Integer
r forall a. Num a => a -> a -> a
- Integer
q forall a. Num a => a -> a -> a
* Integer
r')
instance N.SNatI n => Enum (Fin n) where
fromEnum :: Fin n -> Int
fromEnum = forall (m :: Nat). Fin m -> Int
go where
go :: Fin m -> Int
go :: forall (m :: Nat). Fin m -> Int
go Fin m
FZ = Int
0
go (FS Fin n
n) = forall a. Enum a => a -> a
succ (forall (m :: Nat). Fin m -> Int
go Fin n
n)
toEnum :: Int -> Fin n
toEnum = 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 = forall (n :: Nat). Fin ('S n)
FZ
maxBound :: Fin n
maxBound = forall (n :: Nat). MaxBound n -> Fin ('S n)
getMaxBound forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction
(forall (n :: Nat). Fin ('S n) -> MaxBound n
MaxBound forall (n :: Nat). Fin ('S n)
FZ)
(forall (n :: Nat). Fin ('S n) -> MaxBound n
MaxBound forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). Fin n -> Fin ('S n)
FS forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). MaxBound n -> Fin ('S n)
getMaxBound)
newtype MaxBound n = MaxBound { forall (n :: Nat). 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) = forall a. NFData a => a -> ()
rnf Fin n
n
instance Hashable (Fin n) where
hashWithSalt :: Int -> Fin n -> Int
hashWithSalt Int
salt = forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
salt forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (n :: Nat). a -> (a -> a) -> Fin n -> a
cata (Integer
0 :: Integer) forall a. Enum a => a -> a
succ
instance n ~ 'Z => Boring.Absurd (Fin n) where
absurd :: forall b. Fin n -> b
absurd = forall b. Fin 'Z -> b
absurd
instance (n ~ 'S m, N.SNatI m) => QC.Arbitrary (Fin n) where
arbitrary :: Gen (Fin n)
arbitrary = forall (n :: Nat). Arb n -> Gen (Fin ('S n))
getArb forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction (forall (n :: Nat). Gen (Fin ('S n)) -> Arb n
Arb (forall (m :: * -> *) a. Monad m => a -> m a
return forall (n :: Nat). Fin ('S n)
FZ)) forall (p :: Nat). SNatI p => Arb p -> Arb ('S p)
step where
step :: forall p. N.SNatI p => Arb p -> Arb ('S p)
step :: forall (p :: Nat). SNatI p => Arb p -> Arb ('S p)
step (Arb Gen (Fin ('S p))
p) = forall (n :: Nat). Gen (Fin ('S n)) -> Arb n
Arb forall a b. (a -> b) -> a -> b
$ forall a. [(Int, Gen a)] -> Gen a
QC.frequency
[ (Int
1, forall (m :: * -> *) a. Monad m => a -> m a
return forall (n :: Nat). Fin ('S n)
FZ)
, (forall (n :: Nat) m (proxy :: Nat -> *).
(SNatI n, Num m) =>
proxy n -> m
N.reflectToNum (forall {k} (t :: k). Proxy @k t
Proxy :: Proxy p), forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (n :: Nat). Fin n -> Fin ('S n)
FS Gen (Fin ('S p))
p)
]
shrink :: Fin n -> [Fin n]
shrink = forall (n :: Nat). Fin n -> [Fin n]
shrink
shrink :: Fin n -> [Fin n]
shrink :: forall (n :: Nat). Fin n -> [Fin n]
shrink Fin n
FZ = []
shrink (FS Fin n
FZ) = [forall (n :: Nat). Fin ('S n)
FZ]
shrink (FS Fin n
n) = forall a b. (a -> b) -> [a] -> [b]
map forall (n :: Nat). Fin n -> Fin ('S n)
FS (forall (n :: Nat). Fin n -> [Fin n]
shrink Fin n
n)
newtype Arb n = Arb { forall (n :: Nat). Arb n -> Gen (Fin ('S n))
getArb :: QC.Gen (Fin ('S n)) }
instance QC.CoArbitrary (Fin n) where
coarbitrary :: forall b. Fin n -> Gen b -> Gen b
coarbitrary Fin n
FZ = forall n a. Integral n => n -> Gen a -> Gen a
QC.variant (Int
0 :: Int)
coarbitrary (FS Fin n
n) = forall n a. Integral n => n -> Gen a -> Gen a
QC.variant (Int
1 :: Int) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall b. (Fin n -> b) -> Fin n :-> b
function = case forall (n :: Nat). SNatI n => SNat n
N.snat :: N.SNat m of
SNat m
N.SZ -> forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap (\Fin n
_ -> ()) (\() -> forall (n :: Nat). Fin ('S n)
FZ)
SNat m
N.SS -> forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap forall (n :: Nat). Fin ('S n) -> Maybe (Fin n)
isMin (forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall (n :: Nat). Fin ('S n)
FZ forall (n :: Nat). Fin n -> Fin ('S n)
FS)
instance N.SNatI n => U.Universe (Fin n) where
universe :: [Fin n]
universe = forall (n :: Nat). SNatI n => [Fin n]
universe
instance N.SNatI n => U.Finite (Fin n) where
universeF :: [Fin n]
universeF = forall a. Universe a => [a]
U.universe
cardinality :: Tagged @(*) (Fin n) Natural
cardinality = forall {k} (s :: k) b. b -> Tagged @k s b
U.Tagged forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) m (proxy :: Nat -> *).
(SNatI n, Num m) =>
proxy n -> m
N.reflectToNum (forall {k} (t :: k). Proxy @k t
Proxy :: Proxy n)
explicitShow :: Fin n -> String
explicitShow :: forall (n :: Nat). Fin n -> String
explicitShow Fin n
n = forall (n :: Nat). Int -> Fin n -> ShowS
explicitShowsPrec Int
0 Fin n
n String
""
explicitShowsPrec :: Int -> Fin n -> ShowS
explicitShowsPrec :: forall (n :: Nat). 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 forall a. Ord a => a -> a -> Bool
> Int
10)
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"FS "
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). Int -> Fin n -> ShowS
explicitShowsPrec Int
11 Fin n
n
cata :: forall a n. a -> (a -> a) -> Fin n -> a
cata :: forall a (n :: Nat). a -> (a -> a) -> Fin n -> a
cata a
z a -> a
f = forall (m :: Nat). Fin m -> a
go where
go :: Fin m -> a
go :: forall (m :: Nat). Fin m -> a
go Fin m
FZ = a
z
go (FS Fin n
n) = a -> a
f (forall (m :: Nat). Fin m -> a
go Fin n
n)
toNat :: Fin n -> N.Nat
toNat :: forall (n :: Nat). Fin n -> Nat
toNat = forall a (n :: Nat). a -> (a -> a) -> Fin n -> a
cata Nat
Z Nat -> Nat
S
fromNat :: N.SNatI n => N.Nat -> Maybe (Fin n)
fromNat :: forall (n :: Nat). SNatI n => Nat -> Maybe (Fin n)
fromNat = forall (n :: Nat). NatToFin n -> Nat -> Maybe (Fin n)
appNatToFin (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 (n :: Nat). NatToFin n -> NatToFin ('S n)
step) where
start :: NatToFin 'Z
start :: NatToFin 'Z
start = forall (n :: Nat). (Nat -> Maybe (Fin n)) -> NatToFin n
NatToFin forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a. Maybe a
Nothing
step :: NatToFin n -> NatToFin ('S n)
step :: forall (n :: Nat). NatToFin n -> NatToFin ('S n)
step (NatToFin Nat -> Maybe (Fin n)
f) = forall (n :: Nat). (Nat -> Maybe (Fin n)) -> NatToFin n
NatToFin forall a b. (a -> b) -> a -> b
$ \Nat
n -> case Nat
n of
Nat
Z -> forall a. a -> Maybe a
Just forall (n :: Nat). Fin ('S n)
FZ
S Nat
m -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (n :: Nat). Fin n -> Fin ('S n)
FS (Nat -> Maybe (Fin n)
f Nat
m)
newtype NatToFin n = NatToFin { forall (n :: Nat). NatToFin n -> Nat -> Maybe (Fin n)
appNatToFin :: N.Nat -> Maybe (Fin n) }
toNatural :: Fin n -> Natural
toNatural :: forall (n :: Nat). Fin n -> Natural
toNatural = forall a (n :: Nat). a -> (a -> a) -> Fin n -> a
cata Natural
0 forall a. Enum a => a -> a
succ
unsafeFromNum :: forall n i. (Num i, Ord i, N.SNatI n) => i -> Fin n
unsafeFromNum :: forall (n :: Nat) i. (Num i, Ord i, SNatI n) => i -> Fin n
unsafeFromNum = forall i (n :: Nat). UnsafeFromNum i n -> i -> Fin n
appUnsafeFromNum (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). UnsafeFromNum i m -> UnsafeFromNum i ('S m)
step) where
start :: UnsafeFromNum i 'Z
start :: UnsafeFromNum i 'Z
start = forall i (n :: Nat). (i -> Fin n) -> UnsafeFromNum i n
UnsafeFromNum forall a b. (a -> b) -> a -> b
$ \i
n -> case forall a. Ord a => a -> a -> Ordering
compare i
n i
0 of
Ordering
LT -> forall a e. Exception e => e -> a
throw ArithException
Underflow
Ordering
EQ -> forall a e. Exception e => e -> a
throw ArithException
Overflow
Ordering
GT -> forall a e. Exception e => e -> a
throw ArithException
Overflow
step :: UnsafeFromNum i m -> UnsafeFromNum i ('S m)
step :: forall (m :: Nat). UnsafeFromNum i m -> UnsafeFromNum i ('S m)
step (UnsafeFromNum i -> Fin m
f) = forall i (n :: Nat). (i -> Fin n) -> UnsafeFromNum i n
UnsafeFromNum forall a b. (a -> b) -> a -> b
$ \i
n -> case forall a. Ord a => a -> a -> Ordering
compare i
n i
0 of
Ordering
EQ -> forall (n :: Nat). Fin ('S n)
FZ
Ordering
GT -> forall (n :: Nat). Fin n -> Fin ('S n)
FS (i -> Fin m
f (i
n forall a. Num a => a -> a -> a
- i
1))
Ordering
LT -> forall a e. Exception e => e -> a
throw ArithException
Underflow
newtype UnsafeFromNum i n = UnsafeFromNum { forall i (n :: Nat). UnsafeFromNum i n -> i -> Fin n
appUnsafeFromNum :: i -> Fin n }
universe :: N.SNatI n => [Fin n]
universe :: forall (n :: Nat). SNatI n => [Fin n]
universe = forall (n :: Nat). Universe n -> [Fin n]
getUniverse forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction (forall (n :: Nat). [Fin n] -> Universe n
Universe []) forall (n :: Nat). Universe n -> Universe ('S n)
step where
step :: Universe n -> Universe ('S n)
step :: forall (n :: Nat). Universe n -> Universe ('S n)
step (Universe [Fin n]
xs) = forall (n :: Nat). [Fin n] -> Universe n
Universe (forall (n :: Nat). Fin ('S n)
FZ forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall (n :: Nat). Fin n -> Fin ('S n)
FS [Fin n]
xs)
universe1 :: N.SNatI n => NonEmpty (Fin ('S n))
universe1 :: forall (n :: Nat). SNatI n => NonEmpty (Fin ('S n))
universe1 = forall (n :: Nat). Universe1 n -> NonEmpty (Fin ('S n))
getUniverse1 forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction (forall (n :: Nat). NonEmpty (Fin ('S n)) -> Universe1 n
Universe1 (forall (n :: Nat). Fin ('S n)
FZ forall a. a -> [a] -> NonEmpty a
:| [])) forall (n :: Nat). Universe1 n -> Universe1 ('S n)
step where
step :: Universe1 n -> Universe1 ('S n)
step :: forall (n :: Nat). Universe1 n -> Universe1 ('S n)
step (Universe1 NonEmpty (Fin ('S n))
xs) = forall (n :: Nat). NonEmpty (Fin ('S n)) -> Universe1 n
Universe1 (forall a. a -> NonEmpty a -> NonEmpty a
NE.cons forall (n :: Nat). Fin ('S n)
FZ (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (n :: Nat). Fin n -> Fin ('S n)
FS NonEmpty (Fin ('S n))
xs))
inlineUniverse :: N.SNatI n => [Fin n]
inlineUniverse :: forall (n :: Nat). SNatI n => [Fin n]
inlineUniverse = forall (n :: Nat). Universe n -> [Fin n]
getUniverse forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction (forall (n :: Nat). [Fin n] -> Universe n
Universe []) forall (n :: Nat). Universe n -> Universe ('S n)
step where
step :: Universe n -> Universe ('S n)
step :: forall (n :: Nat). Universe n -> Universe ('S n)
step (Universe [Fin n]
xs) = forall (n :: Nat). [Fin n] -> Universe n
Universe (forall (n :: Nat). Fin ('S n)
FZ forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall (n :: Nat). Fin n -> Fin ('S n)
FS [Fin n]
xs)
inlineUniverse1 :: N.SNatI n => NonEmpty (Fin ('S n))
inlineUniverse1 :: forall (n :: Nat). SNatI n => NonEmpty (Fin ('S n))
inlineUniverse1 = forall (n :: Nat). Universe1 n -> NonEmpty (Fin ('S n))
getUniverse1 forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction (forall (n :: Nat). NonEmpty (Fin ('S n)) -> Universe1 n
Universe1 (forall (n :: Nat). Fin ('S n)
FZ forall a. a -> [a] -> NonEmpty a
:| [])) forall (n :: Nat). Universe1 n -> Universe1 ('S n)
step where
step :: Universe1 n -> Universe1 ('S n)
step :: forall (n :: Nat). Universe1 n -> Universe1 ('S n)
step (Universe1 NonEmpty (Fin ('S n))
xs) = forall (n :: Nat). NonEmpty (Fin ('S n)) -> Universe1 n
Universe1 (forall a. a -> NonEmpty a -> NonEmpty a
NE.cons forall (n :: Nat). Fin ('S n)
FZ (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (n :: Nat). Fin n -> Fin ('S n)
FS NonEmpty (Fin ('S n))
xs))
newtype Universe n = Universe { forall (n :: Nat). Universe n -> [Fin n]
getUniverse :: [Fin n] }
newtype Universe1 n = Universe1 { forall (n :: Nat). Universe1 n -> NonEmpty (Fin ('S n))
getUniverse1 :: NonEmpty (Fin ('S n)) }
absurd :: Fin N.Nat0 -> b
absurd :: forall b. Fin 'Z -> b
absurd Fin 'Z
n = case Fin 'Z
n of {}
boring :: Fin N.Nat1
boring :: Fin ('S 'Z)
boring = forall (n :: Nat). Fin ('S n)
FZ
isMin :: Fin ('S n) -> Maybe (Fin n)
isMin :: forall (n :: Nat). Fin ('S n) -> Maybe (Fin n)
isMin Fin ('S n)
FZ = forall a. Maybe a
Nothing
isMin (FS Fin n
n) = forall a. a -> Maybe a
Just Fin n
n
isMax :: forall n. N.SNatI n => Fin ('S n) -> Maybe (Fin n)
isMax :: forall (n :: Nat). SNatI n => Fin ('S n) -> Maybe (Fin n)
isMax = forall (n :: Nat). IsMax n -> Fin ('S n) -> Maybe (Fin n)
getIsMax (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). IsMax m -> IsMax ('S m)
step) where
start :: IsMax 'Z
start :: IsMax 'Z
start = forall (n :: Nat). (Fin ('S n) -> Maybe (Fin n)) -> IsMax n
IsMax forall a b. (a -> b) -> a -> b
$ \Fin ('S 'Z)
_ -> forall a. Maybe a
Nothing
step :: IsMax m -> IsMax ('S m)
step :: forall (m :: Nat). IsMax m -> IsMax ('S m)
step (IsMax Fin ('S m) -> Maybe (Fin m)
rec) = forall (n :: Nat). (Fin ('S n) -> Maybe (Fin n)) -> IsMax n
IsMax forall a b. (a -> b) -> a -> b
$ \Fin ('S ('S m))
n -> case Fin ('S ('S m))
n of
Fin ('S ('S m))
FZ -> forall a. a -> Maybe a
Just forall (n :: Nat). Fin ('S n)
FZ
FS Fin n
m -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (n :: Nat). Fin n -> Fin ('S n)
FS (Fin ('S m) -> Maybe (Fin m)
rec Fin n
m)
newtype IsMax n = IsMax { forall (n :: Nat). IsMax n -> Fin ('S n) -> Maybe (Fin n)
getIsMax :: Fin ('S n) -> Maybe (Fin n) }
weakenRight1 :: Fin n -> Fin ('S n)
weakenRight1 :: forall (n :: Nat). Fin n -> Fin ('S n)
weakenRight1 = forall (n :: Nat). Fin n -> Fin ('S n)
FS
weakenLeft1 :: N.SNatI n => Fin n -> Fin ('S n)
weakenLeft1 :: forall (n :: Nat). SNatI n => Fin n -> Fin ('S n)
weakenLeft1 = forall (n :: Nat). Weaken1 n -> Fin n -> Fin ('S n)
getWeaken1 (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 (n :: Nat). Weaken1 n -> Weaken1 ('S n)
step) where
start :: Weaken1 'Z
start :: Weaken1 'Z
start = forall (n :: Nat). (Fin n -> Fin ('S n)) -> Weaken1 n
Weaken1 forall b. Fin 'Z -> b
absurd
step :: Weaken1 n -> Weaken1 ('S n)
step :: forall (n :: Nat). Weaken1 n -> Weaken1 ('S n)
step (Weaken1 Fin n -> Fin ('S n)
go) = forall (n :: Nat). (Fin n -> Fin ('S n)) -> Weaken1 n
Weaken1 forall a b. (a -> b) -> a -> b
$ \Fin ('S n)
n -> case Fin ('S n)
n of
Fin ('S n)
FZ -> forall (n :: Nat). Fin ('S n)
FZ
FS Fin n
n' -> forall (n :: Nat). Fin n -> Fin ('S n)
FS (Fin n -> Fin ('S n)
go Fin n
n')
newtype Weaken1 n = Weaken1 { forall (n :: Nat). Weaken1 n -> Fin n -> Fin ('S n)
getWeaken1 :: Fin n -> Fin ('S n) }
weakenLeft :: forall n m. N.SNatI n => Proxy m -> Fin n -> Fin (N.Plus n m)
weakenLeft :: forall (n :: Nat) (m :: Nat).
SNatI n =>
Proxy @Nat m -> Fin n -> Fin (Plus n m)
weakenLeft Proxy @Nat m
_ = forall (m :: Nat) (n :: Nat).
WeakenLeft m n -> Fin n -> Fin (Plus n m)
getWeakenLeft (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 (p :: Nat). WeakenLeft m p -> WeakenLeft m ('S p)
step :: WeakenLeft m n) where
start :: WeakenLeft m 'Z
start :: WeakenLeft m 'Z
start = forall (m :: Nat) (n :: Nat).
(Fin n -> Fin (Plus n m)) -> WeakenLeft m n
WeakenLeft forall b. Fin 'Z -> b
absurd
step :: WeakenLeft m p -> WeakenLeft m ('S p)
step :: forall (p :: Nat). WeakenLeft m p -> WeakenLeft m ('S p)
step (WeakenLeft Fin p -> Fin (Plus p m)
go) = forall (m :: Nat) (n :: Nat).
(Fin n -> Fin (Plus n m)) -> WeakenLeft m n
WeakenLeft forall a b. (a -> b) -> a -> b
$ \Fin ('S p)
n -> case Fin ('S p)
n of
Fin ('S p)
FZ -> forall (n :: Nat). Fin ('S n)
FZ
FS Fin n
n' -> forall (n :: Nat). Fin n -> Fin ('S n)
FS (Fin p -> Fin (Plus p m)
go Fin n
n')
newtype WeakenLeft m n = WeakenLeft { forall (m :: Nat) (n :: Nat).
WeakenLeft m n -> Fin n -> Fin (Plus n m)
getWeakenLeft :: Fin n -> Fin (N.Plus n m) }
weakenRight :: forall n m. N.SNatI n => Proxy n -> Fin m -> Fin (N.Plus n m)
weakenRight :: forall (n :: Nat) (m :: Nat).
SNatI n =>
Proxy @Nat n -> Fin m -> Fin (Plus n m)
weakenRight Proxy @Nat n
_ = forall (m :: Nat) (n :: Nat).
WeakenRight m n -> Fin m -> Fin (Plus n m)
getWeakenRight (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 {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 = forall (m :: Nat) (n :: Nat).
(Fin m -> Fin (Plus n m)) -> WeakenRight m n
WeakenRight forall a. a -> a
id
step :: WeakenRight m n -> WeakenRight m n
step (WeakenRight Fin m -> Fin (Plus n m)
go) = forall (m :: Nat) (n :: Nat).
(Fin m -> Fin (Plus n m)) -> WeakenRight m n
WeakenRight forall a b. (a -> b) -> a -> b
$ \Fin m
x -> forall (n :: Nat). Fin n -> Fin ('S n)
FS forall a b. (a -> b) -> a -> b
$ Fin m -> Fin (Plus n m)
go Fin m
x
newtype WeakenRight m n = WeakenRight { forall (m :: Nat) (n :: Nat).
WeakenRight m n -> Fin m -> Fin (Plus n m)
getWeakenRight :: Fin m -> Fin (N.Plus n m) }
append :: forall n m. N.SNatI n => Either (Fin n) (Fin m) -> Fin (N.Plus n m)
append :: forall (n :: Nat) (m :: Nat).
SNatI n =>
Either (Fin n) (Fin m) -> Fin (Plus n m)
append (Left Fin n
n) = forall (n :: Nat) (m :: Nat).
SNatI n =>
Proxy @Nat m -> Fin n -> Fin (Plus n m)
weakenLeft (forall {k} (t :: k). Proxy @k t
Proxy :: Proxy m) Fin n
n
append (Right Fin m
m) = forall (n :: Nat) (m :: Nat).
SNatI n =>
Proxy @Nat n -> Fin m -> Fin (Plus n m)
weakenRight (forall {k} (t :: k). Proxy @k t
Proxy :: Proxy n) Fin m
m
split :: forall n m. N.SNatI n => Fin (N.Plus n m) -> Either (Fin n) (Fin m)
split :: forall (n :: Nat) (m :: Nat).
SNatI n =>
Fin (Plus n m) -> Either (Fin n) (Fin m)
split = forall (m :: Nat) (n :: Nat).
Split m n -> Fin (Plus n m) -> Either (Fin n) (Fin m)
getSplit (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 (p :: Nat). Split m p -> Split m ('S p)
step) where
start :: Split m 'Z
start :: Split m 'Z
start = forall (m :: Nat) (n :: Nat).
(Fin (Plus n m) -> Either (Fin n) (Fin m)) -> Split m n
Split forall a b. b -> Either a b
Right
step :: Split m p -> Split m ('S p)
step :: forall (p :: Nat). Split m p -> Split m ('S p)
step (Split Fin (Plus p m) -> Either (Fin p) (Fin m)
go) = forall (m :: Nat) (n :: Nat).
(Fin (Plus n m) -> Either (Fin n) (Fin m)) -> Split m n
Split 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 -> forall a b. a -> Either a b
Left forall (n :: Nat). Fin ('S n)
FZ
FS Fin n
x' -> forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap forall (n :: Nat). Fin n -> Fin ('S n)
FS forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ Fin (Plus p m) -> Either (Fin p) (Fin m)
go Fin n
x'
newtype Split m n = Split { forall (m :: Nat) (n :: Nat).
Split m n -> Fin (Plus n m) -> Either (Fin n) (Fin m)
getSplit :: Fin (N.Plus n m) -> Either (Fin n) (Fin m) }
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 :: forall (n :: Nat). Fin (Plus 'Z ('S n))
fin0 = forall (n :: Nat). Fin ('S n)
FZ
fin1 :: forall (n :: Nat). Fin (Plus ('S 'Z) ('S n))
fin1 = forall (n :: Nat). Fin n -> Fin ('S n)
FS forall (n :: Nat). Fin (Plus 'Z ('S n))
fin0
fin2 :: forall (n :: Nat). Fin (Plus Nat2 ('S n))
fin2 = forall (n :: Nat). Fin n -> Fin ('S n)
FS forall (n :: Nat). Fin (Plus ('S 'Z) ('S n))
fin1
fin3 :: forall (n :: Nat). Fin (Plus Nat3 ('S n))
fin3 = forall (n :: Nat). Fin n -> Fin ('S n)
FS forall (n :: Nat). Fin (Plus Nat2 ('S n))
fin2
fin4 :: forall (n :: Nat). Fin (Plus Nat4 ('S n))
fin4 = forall (n :: Nat). Fin n -> Fin ('S n)
FS forall (n :: Nat). Fin (Plus Nat3 ('S n))
fin3
fin5 :: forall (n :: Nat). Fin (Plus Nat5 ('S n))
fin5 = forall (n :: Nat). Fin n -> Fin ('S n)
FS forall (n :: Nat). Fin (Plus Nat4 ('S n))
fin4
fin6 :: forall (n :: Nat). Fin (Plus Nat6 ('S n))
fin6 = forall (n :: Nat). Fin n -> Fin ('S n)
FS forall (n :: Nat). Fin (Plus Nat5 ('S n))
fin5
fin7 :: forall (n :: Nat). Fin (Plus Nat7 ('S n))
fin7 = forall (n :: Nat). Fin n -> Fin ('S n)
FS forall (n :: Nat). Fin (Plus Nat6 ('S n))
fin6
fin8 :: forall (n :: Nat). Fin (Plus Nat8 ('S n))
fin8 = forall (n :: Nat). Fin n -> Fin ('S n)
FS forall (n :: Nat). Fin (Plus Nat7 ('S n))
fin7
fin9 :: forall (n :: Nat). Fin (Plus Nat9 ('S n))
fin9 = forall (n :: Nat). Fin n -> Fin ('S n)
FS forall (n :: Nat). Fin (Plus Nat8 ('S n))
fin8