{-# 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.EqP (EqP (..))
import Data.GADT.Show (GShow (..))
import Data.Hashable (Hashable (..))
import Data.List.NonEmpty (NonEmpty (..))
import Data.OrdP (OrdP (..))
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.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)
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) = Fin n -> Fin n -> Bool
forall k (f :: k -> *) (a :: k) (b :: k).
EqP @k f =>
f a -> f b -> Bool
forall (a :: Nat) (b :: Nat). Fin a -> Fin 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) = Fin n -> Fin n -> Ordering
forall k (f :: k -> *) (a :: k) (b :: k).
OrdP @k f =>
f a -> f b -> Ordering
forall (a :: Nat) (b :: Nat). Fin a -> Fin b -> Ordering
comparep Fin n
n Fin n
m
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
instance GShow Fin where
gshowsPrec :: forall (n :: Nat). Int -> Fin n -> ShowS
gshowsPrec = Int -> Fin a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec
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
Fin ('S 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
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 :: forall n. N.SNatI n => Fin n -> Fin n
mirror :: forall (n :: Nat). SNatI n => 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
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction Mirror 'Z
start Mirror m -> Mirror ('S m)
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 :: forall (m :: Nat). SNatI m => 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
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f m
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 { 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 = 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 :: forall (m :: Nat). 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
Fin ('S m)
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
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f m
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 { 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) = 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
instance n ~ 'Z => Boring.Absurd (Fin n) where
absurd :: forall b. Fin n -> b
absurd = Fin n -> b
Fin 'Z -> b
forall b. Fin 'Z -> b
absurd
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
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f m
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 a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return Fin ('S 'Z)
forall (n :: Nat). Fin ('S n)
FZ)) Arb m -> Arb ('S m)
forall (m :: Nat). SNatI m => Arb m -> Arb ('S m)
step where
step :: forall p. N.SNatI p => Arb p -> Arb ('S p)
step :: forall (m :: Nat). SNatI m => Arb m -> Arb ('S m)
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. HasCallStack => [(Int, Gen a)] -> Gen a
QC.frequency
[ (Int
1, Fin ('S ('S p)) -> Gen (Fin ('S ('S p)))
forall a. a -> Gen a
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 a b. (a -> b) -> Gen a -> Gen b
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 :: forall (n :: Nat). Fin n -> [Fin n]
shrink Fin n
FZ = []
shrink (FS Fin n
FZ) = [Fin n
Fin ('S ('S n))
forall (n :: Nat). Fin ('S n)
FZ]
shrink (FS Fin n
n) = (Fin n -> Fin n) -> [Fin n] -> [Fin n]
forall a b. (a -> b) -> [a] -> [b]
map Fin n -> Fin n
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 { 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 = 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
forall b. Fin n -> 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 SNat m
forall (n :: Nat). SNatI n => SNat n
N.snat :: N.SNat m of
SNat m
N.SZ -> (Fin n -> ()) -> (() -> Fin n) -> (Fin n -> b) -> Fin n :-> b
forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap (\Fin n
_ -> ()) (\() -> Fin n
Fin ('S 'Z)
forall (n :: Nat). Fin ('S n)
FZ)
SNat m
N.SS -> (Fin n -> Maybe (Fin ('S n1)))
-> (Maybe (Fin ('S n1)) -> Fin n) -> (Fin n -> b) -> Fin n :-> b
forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap Fin n -> Maybe (Fin ('S n1))
Fin ('S ('S n1)) -> Maybe (Fin ('S n1))
forall (n :: Nat). Fin ('S n) -> Maybe (Fin n)
isMin (Fin n -> (Fin ('S n1) -> Fin n) -> Maybe (Fin ('S n1)) -> Fin n
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Fin n
Fin ('S ('S n1))
forall (n :: Nat). Fin ('S n)
FZ Fin ('S n1) -> Fin n
Fin ('S n1) -> Fin ('S ('S n1))
forall (n :: Nat). Fin n -> Fin ('S n)
FS)
instance N.SNatI n => U.Universe (Fin n) where
universe :: [Fin n]
universe = [Fin n]
forall (n :: Nat). SNatI n => [Fin n]
universe
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)
explicitShow :: Fin n -> String
explicitShow :: forall (n :: Nat). 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
""
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 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
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 = Fin n -> a
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 (Fin n -> a
forall (m :: Nat). Fin m -> a
go Fin n
n)
toNat :: Fin n -> N.Nat
toNat :: forall (n :: Nat). 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
fromNat :: N.SNatI n => N.Nat -> Maybe (Fin n)
fromNat :: forall (n :: Nat). SNatI n => 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
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction NatToFin 'Z
start NatToFin m -> NatToFin ('S m)
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 :: forall (n :: Nat). 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 a b. (a -> b) -> Maybe a -> Maybe b
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 { 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 = 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
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 = 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
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction UnsafeFromNum i 'Z
start UnsafeFromNum i m -> UnsafeFromNum i ('S m)
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 :: forall (m :: Nat). 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 { 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 = 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
forall (f :: Nat -> *).
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 []) Universe m -> Universe ('S m)
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 :: forall (n :: Nat). 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)
universe1 :: N.SNatI n => NonEmpty (Fin ('S n))
universe1 :: forall (n :: Nat). SNatI n => 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
forall (f :: Nat -> *).
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
:| [])) Universe1 m -> Universe1 ('S m)
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 :: forall (n :: Nat). 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 a b. (a -> b) -> NonEmpty a -> NonEmpty b
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))
inlineUniverse :: N.SNatI n => [Fin n]
inlineUniverse :: forall (n :: Nat). SNatI n => [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
forall (f :: Nat -> *).
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 []) Universe m -> Universe ('S m)
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 :: forall (n :: Nat). 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 :: N.SNatI n => NonEmpty (Fin ('S n))
inlineUniverse1 :: forall (n :: Nat). SNatI n => 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
forall (f :: Nat -> *).
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
:| [])) Universe1 m -> Universe1 ('S m)
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 :: forall (n :: Nat). 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 a b. (a -> b) -> NonEmpty a -> NonEmpty b
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 { 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 = Fin ('S 'Z)
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 = 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
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 = 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
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction IsMax 'Z
start IsMax m -> IsMax ('S m)
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 :: forall (m :: Nat). 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 a b. (a -> b) -> Maybe a -> Maybe b
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 { 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 = Fin n -> Fin ('S n)
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 = 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
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction Weaken1 'Z
start Weaken1 m -> Weaken1 ('S m)
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 :: forall (n :: Nat). 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 { 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
_ = 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
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction WeakenLeft m 'Z
start WeakenLeft m m -> WeakenLeft m ('S m)
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 m
Fin 'Z -> Fin (Plus 'Z m)
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) = (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 ('S (Plus p m))
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 { 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
_ = 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
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction WeakenRight m 'Z
start WeakenRight m m -> WeakenRight m ('S m)
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 m
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 { 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) = 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
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 = 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
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction Split m 'Z
start Split m m -> Split m ('S m)
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 m -> Either (Fin 'Z) (Fin m)
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 :: forall (p :: Nat). 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 a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
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 { 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 = Fin ('S n)
Fin (Plus 'Z ('S n))
forall (n :: Nat). Fin ('S n)
FZ
fin1 :: forall (n :: Nat). 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)
Fin (Plus 'Z ('S n))
forall (n :: Nat). Fin (Plus 'Z ('S n))
fin0
fin2 :: forall (n :: Nat). 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))
Fin (Plus ('S 'Z) ('S n))
forall (n :: Nat). Fin (Plus ('S 'Z) ('S n))
fin1
fin3 :: forall (n :: Nat). 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)))
Fin (Plus Nat2 ('S n))
forall (n :: Nat). Fin (Plus Nat2 ('S n))
fin2
fin4 :: forall (n :: Nat). 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))))
Fin (Plus Nat3 ('S n))
forall (n :: Nat). Fin (Plus Nat3 ('S n))
fin3
fin5 :: forall (n :: Nat). 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)))))
Fin (Plus Nat4 ('S n))
forall (n :: Nat). Fin (Plus Nat4 ('S n))
fin4
fin6 :: forall (n :: Nat). 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))))))
Fin (Plus Nat5 ('S n))
forall (n :: Nat). Fin (Plus Nat5 ('S n))
fin5
fin7 :: forall (n :: Nat). 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)))))))
Fin (Plus Nat6 ('S n))
forall (n :: Nat). Fin (Plus Nat6 ('S n))
fin6
fin8 :: forall (n :: Nat). 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))))))))
Fin (Plus Nat7 ('S n))
forall (n :: Nat). Fin (Plus Nat7 ('S n))
fin7
fin9 :: forall (n :: Nat). 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)))))))))
Fin (Plus Nat8 ('S n))
forall (n :: Nat). Fin (Plus Nat8 ('S n))
fin8