{-# LANGUAGE TypeApplications #-}

module Data.Fin.Private where

import Prelude (Functor (..), Show (..), Num (..), Enum (..), Bounded (..), Integral (..), Bool (..), Integer, ($), (&&), fst, snd, flip, uncurry, error)
import Control.Applicative
import Control.Arrow (Kleisli (..))
import Control.Category
import Control.Monad (Monad (..))
import Data.Ap
import Data.Eq
import Data.Foldable
import Data.Foldable1
import Data.Function (on)
import Data.Functor.Classes
import Data.Functor.Compose
import Data.Kind (Type)
import qualified Data.List as L
import Data.List.NonEmpty (NonEmpty (..))
import Data.Maybe
import Data.Monoid (Monoid (..))
import Data.Natural.Class
import Data.Ord
import Data.Peano (Peano)
import qualified Data.Peano as P
import Data.Semigroup (Semigroup (..))
import Data.Traversable
import Data.Typeable
import qualified Numeric.Natural as N
import Text.Read (Read (..))

-- | Totally-ordered type with @n@ possible values
data Fin :: Peano -> Type where
    Zero :: Fin (P.Succ n)
    Succ :: Fin n -> Fin (P.Succ n)

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

instance Show (Fin n) where show :: Fin n -> String
show = Natural -> String
forall a. Show a => a -> String
show (Natural -> String) -> (Fin n -> Natural) -> Fin n -> String
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a (n :: Peano). Integral a => Fin n -> a
forall (n :: Peano). Integral Natural => Fin n -> Natural
fromFin @N.Natural

instance Read (Fin P.Zero) where readPrec :: ReadPrec (Fin 'Zero)
readPrec = ReadPrec (Fin 'Zero)
forall (f :: * -> *) a. Alternative f => f a
empty
instance (Natural n, Read (Fin n)) => Read (Fin (P.Succ n)) where
    readPrec :: ReadPrec (Fin ('Succ n))
readPrec = Natural -> Maybe (Fin ('Succ n))
forall (n :: Peano) a.
(Natural n, Integral a) =>
a -> Maybe (Fin n)
toFinMay (Natural -> Maybe (Fin ('Succ n)))
-> ReadPrec Natural -> ReadPrec (Maybe (Fin ('Succ n)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Read Natural => ReadPrec Natural
forall a. Read a => ReadPrec a
readPrec @N.Natural ReadPrec (Maybe (Fin ('Succ n)))
-> (Maybe (Fin ('Succ n)) -> ReadPrec (Fin ('Succ n)))
-> ReadPrec (Fin ('Succ n))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ReadPrec (Fin ('Succ n))
-> (Fin ('Succ n) -> ReadPrec (Fin ('Succ n)))
-> Maybe (Fin ('Succ n))
-> ReadPrec (Fin ('Succ n))
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ReadPrec (Fin ('Succ n))
forall (f :: * -> *) a. Alternative f => f a
empty Fin ('Succ n) -> ReadPrec (Fin ('Succ n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure

instance Natural n => Bounded (Fin (P.Succ n)) where
    minBound :: Fin ('Succ n)
minBound = Fin ('Succ n)
forall (n :: Peano). Fin ('Succ n)
Zero
    maxBound :: Fin ('Succ n)
maxBound = Compose Fin 'Succ n -> Fin ('Succ n)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose Fin 'Succ n -> Fin ('Succ n))
-> Compose Fin 'Succ n -> Fin ('Succ n)
forall a b. (a -> b) -> a -> b
$ Compose Fin 'Succ 'Zero
-> (forall (m :: Peano). Natural m => Compose Fin 'Succ ('Succ m))
-> Compose Fin 'Succ n
forall (n :: Peano) (f :: Peano -> *).
Natural n =>
f 'Zero -> (forall (m :: Peano). Natural m => f ('Succ m)) -> f n
natural (Fin ('Succ 'Zero) -> Compose Fin 'Succ 'Zero
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose Fin ('Succ 'Zero)
forall (n :: Peano). Fin ('Succ n)
Zero) (Fin ('Succ ('Succ m)) -> Compose Fin 'Succ ('Succ m)
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose Fin ('Succ ('Succ m))
forall a. Bounded a => a
maxBound)

instance Natural n => Enum (Fin n) where
    toEnum :: Int -> Fin n
toEnum n :: Int
n = Fin 'Zero
-> (forall (n :: Peano). Natural n => Fin ('Succ n)) -> Fin n
forall (n :: Peano) (f :: Peano -> *).
Natural n =>
f 'Zero -> (forall (m :: Peano). Natural m => f ('Succ m)) -> f n
natural (String -> Fin 'Zero
forall a. HasCallStack => String -> a
error "toEnum @(Fin Zero)") ((forall (n :: Peano). Natural n => Fin ('Succ n)) -> Fin n)
-> (forall (n :: Peano). Natural n => Fin ('Succ n)) -> Fin n
forall a b. (a -> b) -> a -> b
$ case Int
n of
        0 -> Fin ('Succ m)
forall (n :: Peano). Fin ('Succ n)
Zero
        _ -> Fin m -> Fin ('Succ m)
forall (n :: Peano). Fin n -> Fin ('Succ n)
Succ (Int -> Fin m
forall a. Enum a => Int -> a
toEnum (Int -> Int
forall a. Enum a => a -> a
pred Int
n))
    fromEnum :: Fin n -> Int
fromEnum = Flip (->) Int (Fin n) -> Fin n -> Int
forall k k (f :: k -> k -> *) (a :: k) (b :: k).
Flip f a b -> f b a
unFlip (Flip (->) Int (Fin n) -> Fin n -> Int)
-> (Compose (Flip (->) Int) Fin n -> Flip (->) Int (Fin n))
-> Compose (Flip (->) Int) Fin n
-> Fin n
-> Int
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Compose (Flip (->) Int) Fin n -> Flip (->) Int (Fin n)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose (Flip (->) Int) Fin n -> Fin n -> Int)
-> Compose (Flip (->) Int) Fin n -> Fin n -> Int
forall a b. (a -> b) -> a -> b
$ Compose (Flip (->) Int) Fin 'Zero
-> (forall (m :: Peano).
    Natural m =>
    Compose (Flip (->) Int) Fin ('Succ m))
-> Compose (Flip (->) Int) Fin n
forall (n :: Peano) (f :: Peano -> *).
Natural n =>
f 'Zero -> (forall (m :: Peano). Natural m => f ('Succ m)) -> f n
natural (Flip (->) Int (Fin 'Zero) -> Compose (Flip (->) Int) Fin 'Zero
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Flip (->) Int (Fin 'Zero) -> Compose (Flip (->) Int) Fin 'Zero)
-> ((Fin 'Zero -> Int) -> Flip (->) Int (Fin 'Zero))
-> (Fin 'Zero -> Int)
-> Compose (Flip (->) Int) Fin 'Zero
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Fin 'Zero -> Int) -> Flip (->) Int (Fin 'Zero)
forall k k (f :: k -> k -> *) (a :: k) (b :: k).
f b a -> Flip f a b
Flip ((Fin 'Zero -> Int) -> Compose (Flip (->) Int) Fin 'Zero)
-> (Fin 'Zero -> Int) -> Compose (Flip (->) Int) Fin 'Zero
forall a b. (a -> b) -> a -> b
$ \ case) ((forall (m :: Peano).
  Natural m =>
  Compose (Flip (->) Int) Fin ('Succ m))
 -> Compose (Flip (->) Int) Fin n)
-> (forall (m :: Peano).
    Natural m =>
    Compose (Flip (->) Int) Fin ('Succ m))
-> Compose (Flip (->) Int) Fin n
forall a b. (a -> b) -> a -> b
$ Flip (->) Int (Fin ('Succ m))
-> Compose (Flip (->) Int) Fin ('Succ m)
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Flip (->) Int (Fin ('Succ m))
 -> Compose (Flip (->) Int) Fin ('Succ m))
-> ((Fin ('Succ m) -> Int) -> Flip (->) Int (Fin ('Succ m)))
-> (Fin ('Succ m) -> Int)
-> Compose (Flip (->) Int) Fin ('Succ m)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Fin ('Succ m) -> Int) -> Flip (->) Int (Fin ('Succ m))
forall k k (f :: k -> k -> *) (a :: k) (b :: k).
f b a -> Flip f a b
Flip ((Fin ('Succ m) -> Int) -> Compose (Flip (->) Int) Fin ('Succ m))
-> (Fin ('Succ m) -> Int) -> Compose (Flip (->) Int) Fin ('Succ m)
forall a b. (a -> b) -> a -> b
$ \ case
        Zero -> 0
        Succ n :: Fin n
n -> Int -> Int
forall a. Enum a => a -> a
succ (Fin n -> Int
forall a. Enum a => a -> Int
fromEnum Fin n
n)
    succ :: Fin n -> Fin n
succ = Join (->) (Fin n) -> Fin n -> Fin n
forall k (s :: k -> k -> *) (a :: k). Join s a -> s a a
unJoin (Join (->) (Fin n) -> Fin n -> Fin n)
-> (Compose (Join (->)) Fin n -> Join (->) (Fin n))
-> Compose (Join (->)) Fin n
-> Fin n
-> Fin n
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Compose (Join (->)) Fin n -> Join (->) (Fin n)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose (Join (->)) Fin n -> Fin n -> Fin n)
-> Compose (Join (->)) Fin n -> Fin n -> Fin n
forall a b. (a -> b) -> a -> b
$ Compose (Join (->)) Fin 'Zero
-> (forall (m :: Peano).
    Natural m =>
    Compose (Join (->)) Fin ('Succ m))
-> Compose (Join (->)) Fin n
forall (n :: Peano) (f :: Peano -> *).
Natural n =>
f 'Zero -> (forall (m :: Peano). Natural m => f ('Succ m)) -> f n
natural (Join (->) (Fin 'Zero) -> Compose (Join (->)) Fin 'Zero
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Join (->) (Fin 'Zero) -> Compose (Join (->)) Fin 'Zero)
-> ((Fin 'Zero -> Fin 'Zero) -> Join (->) (Fin 'Zero))
-> (Fin 'Zero -> Fin 'Zero)
-> Compose (Join (->)) Fin 'Zero
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Fin 'Zero -> Fin 'Zero) -> Join (->) (Fin 'Zero)
forall k (s :: k -> k -> *) (a :: k). s a a -> Join s a
Join ((Fin 'Zero -> Fin 'Zero) -> Compose (Join (->)) Fin 'Zero)
-> (Fin 'Zero -> Fin 'Zero) -> Compose (Join (->)) Fin 'Zero
forall a b. (a -> b) -> a -> b
$ \ case) ((forall (m :: Peano).
  Natural m =>
  Compose (Join (->)) Fin ('Succ m))
 -> Compose (Join (->)) Fin n)
-> (forall (m :: Peano).
    Natural m =>
    Compose (Join (->)) Fin ('Succ m))
-> Compose (Join (->)) Fin n
forall a b. (a -> b) -> a -> b
$ Join (->) (Fin ('Succ m)) -> Compose (Join (->)) Fin ('Succ m)
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Join (->) (Fin ('Succ m)) -> Compose (Join (->)) Fin ('Succ m))
-> ((Fin ('Succ m) -> Fin ('Succ m)) -> Join (->) (Fin ('Succ m)))
-> (Fin ('Succ m) -> Fin ('Succ m))
-> Compose (Join (->)) Fin ('Succ m)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Fin ('Succ m) -> Fin ('Succ m)) -> Join (->) (Fin ('Succ m))
forall k (s :: k -> k -> *) (a :: k). s a a -> Join s a
Join ((Fin ('Succ m) -> Fin ('Succ m))
 -> Compose (Join (->)) Fin ('Succ m))
-> (Fin ('Succ m) -> Fin ('Succ m))
-> Compose (Join (->)) Fin ('Succ m)
forall a b. (a -> b) -> a -> b
$ \ case
        Zero -> Int -> Fin ('Succ m)
forall a. Enum a => Int -> a
toEnum 1
        Succ n :: Fin n
n -> Fin n -> Fin ('Succ n)
forall (n :: Peano). Fin n -> Fin ('Succ n)
Succ (Fin n -> Fin n
forall a. Enum a => a -> a
succ Fin n
n)
    pred :: Fin n -> Fin n
pred = Join (->) (Fin n) -> Fin n -> Fin n
forall k (s :: k -> k -> *) (a :: k). Join s a -> s a a
unJoin (Join (->) (Fin n) -> Fin n -> Fin n)
-> (Compose (Join (->)) Fin n -> Join (->) (Fin n))
-> Compose (Join (->)) Fin n
-> Fin n
-> Fin n
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Compose (Join (->)) Fin n -> Join (->) (Fin n)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose (Join (->)) Fin n -> Fin n -> Fin n)
-> Compose (Join (->)) Fin n -> Fin n -> Fin n
forall a b. (a -> b) -> a -> b
$ Compose (Join (->)) Fin 'Zero
-> (forall (m :: Peano).
    Natural m =>
    Compose (Join (->)) Fin ('Succ m))
-> Compose (Join (->)) Fin n
forall (n :: Peano) (f :: Peano -> *).
Natural n =>
f 'Zero -> (forall (m :: Peano). Natural m => f ('Succ m)) -> f n
natural (Join (->) (Fin 'Zero) -> Compose (Join (->)) Fin 'Zero
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Join (->) (Fin 'Zero) -> Compose (Join (->)) Fin 'Zero)
-> ((Fin 'Zero -> Fin 'Zero) -> Join (->) (Fin 'Zero))
-> (Fin 'Zero -> Fin 'Zero)
-> Compose (Join (->)) Fin 'Zero
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Fin 'Zero -> Fin 'Zero) -> Join (->) (Fin 'Zero)
forall k (s :: k -> k -> *) (a :: k). s a a -> Join s a
Join ((Fin 'Zero -> Fin 'Zero) -> Compose (Join (->)) Fin 'Zero)
-> (Fin 'Zero -> Fin 'Zero) -> Compose (Join (->)) Fin 'Zero
forall a b. (a -> b) -> a -> b
$ \ case) ((forall (m :: Peano).
  Natural m =>
  Compose (Join (->)) Fin ('Succ m))
 -> Compose (Join (->)) Fin n)
-> (forall (m :: Peano).
    Natural m =>
    Compose (Join (->)) Fin ('Succ m))
-> Compose (Join (->)) Fin n
forall a b. (a -> b) -> a -> b
$ Join (->) (Fin ('Succ m)) -> Compose (Join (->)) Fin ('Succ m)
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Join (->) (Fin ('Succ m)) -> Compose (Join (->)) Fin ('Succ m))
-> ((Fin ('Succ m) -> Fin ('Succ m)) -> Join (->) (Fin ('Succ m)))
-> (Fin ('Succ m) -> Fin ('Succ m))
-> Compose (Join (->)) Fin ('Succ m)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Fin ('Succ m) -> Fin ('Succ m)) -> Join (->) (Fin ('Succ m))
forall k (s :: k -> k -> *) (a :: k). s a a -> Join s a
Join ((Fin ('Succ m) -> Fin ('Succ m))
 -> Compose (Join (->)) Fin ('Succ m))
-> (Fin ('Succ m) -> Fin ('Succ m))
-> Compose (Join (->)) Fin ('Succ m)
forall a b. (a -> b) -> a -> b
$ \ case
        Zero -> String -> Fin ('Succ m)
forall a. HasCallStack => String -> a
error "pred 0"
        Succ n :: Fin n
n -> Fin n -> Fin ('Succ n)
forall (n :: Peano). Fin n -> Fin ('Succ n)
inj₁ Fin n
n
    enumFrom :: Fin n -> [Fin n]
enumFrom = Kleisli [] (Fin n) (Fin n) -> Fin n -> [Fin n]
forall (m :: * -> *) a b. Kleisli m a b -> a -> m b
runKleisli (Kleisli [] (Fin n) (Fin n) -> Fin n -> [Fin n])
-> (Compose (Join (Kleisli [])) Fin n
    -> Kleisli [] (Fin n) (Fin n))
-> Compose (Join (Kleisli [])) Fin n
-> Fin n
-> [Fin n]
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Join (Kleisli []) (Fin n) -> Kleisli [] (Fin n) (Fin n)
forall k (s :: k -> k -> *) (a :: k). Join s a -> s a a
unJoin (Join (Kleisli []) (Fin n) -> Kleisli [] (Fin n) (Fin n))
-> (Compose (Join (Kleisli [])) Fin n -> Join (Kleisli []) (Fin n))
-> Compose (Join (Kleisli [])) Fin n
-> Kleisli [] (Fin n) (Fin n)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Compose (Join (Kleisli [])) Fin n -> Join (Kleisli []) (Fin n)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose (Join (Kleisli [])) Fin n -> Fin n -> [Fin n])
-> Compose (Join (Kleisli [])) Fin n -> Fin n -> [Fin n]
forall a b. (a -> b) -> a -> b
$ Compose (Join (Kleisli [])) Fin 'Zero
-> (forall (m :: Peano).
    Natural m =>
    Compose (Join (Kleisli [])) Fin ('Succ m))
-> Compose (Join (Kleisli [])) Fin n
forall (n :: Peano) (f :: Peano -> *).
Natural n =>
f 'Zero -> (forall (m :: Peano). Natural m => f ('Succ m)) -> f n
natural (Join (Kleisli []) (Fin 'Zero)
-> Compose (Join (Kleisli [])) Fin 'Zero
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Join (Kleisli []) (Fin 'Zero)
 -> Compose (Join (Kleisli [])) Fin 'Zero)
-> ((Fin 'Zero -> [Fin 'Zero]) -> Join (Kleisli []) (Fin 'Zero))
-> (Fin 'Zero -> [Fin 'Zero])
-> Compose (Join (Kleisli [])) Fin 'Zero
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Kleisli [] (Fin 'Zero) (Fin 'Zero) -> Join (Kleisli []) (Fin 'Zero)
forall k (s :: k -> k -> *) (a :: k). s a a -> Join s a
Join (Kleisli [] (Fin 'Zero) (Fin 'Zero)
 -> Join (Kleisli []) (Fin 'Zero))
-> ((Fin 'Zero -> [Fin 'Zero])
    -> Kleisli [] (Fin 'Zero) (Fin 'Zero))
-> (Fin 'Zero -> [Fin 'Zero])
-> Join (Kleisli []) (Fin 'Zero)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Fin 'Zero -> [Fin 'Zero]) -> Kleisli [] (Fin 'Zero) (Fin 'Zero)
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli ((Fin 'Zero -> [Fin 'Zero])
 -> Compose (Join (Kleisli [])) Fin 'Zero)
-> (Fin 'Zero -> [Fin 'Zero])
-> Compose (Join (Kleisli [])) Fin 'Zero
forall a b. (a -> b) -> a -> b
$ \ case) ((forall (m :: Peano).
  Natural m =>
  Compose (Join (Kleisli [])) Fin ('Succ m))
 -> Compose (Join (Kleisli [])) Fin n)
-> (forall (m :: Peano).
    Natural m =>
    Compose (Join (Kleisli [])) Fin ('Succ m))
-> Compose (Join (Kleisli [])) Fin n
forall a b. (a -> b) -> a -> b
$ Join (Kleisli []) (Fin ('Succ m))
-> Compose (Join (Kleisli [])) Fin ('Succ m)
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Join (Kleisli []) (Fin ('Succ m))
 -> Compose (Join (Kleisli [])) Fin ('Succ m))
-> ((Fin ('Succ m) -> [Fin ('Succ m)])
    -> Join (Kleisli []) (Fin ('Succ m)))
-> (Fin ('Succ m) -> [Fin ('Succ m)])
-> Compose (Join (Kleisli [])) Fin ('Succ m)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Kleisli [] (Fin ('Succ m)) (Fin ('Succ m))
-> Join (Kleisli []) (Fin ('Succ m))
forall k (s :: k -> k -> *) (a :: k). s a a -> Join s a
Join (Kleisli [] (Fin ('Succ m)) (Fin ('Succ m))
 -> Join (Kleisli []) (Fin ('Succ m)))
-> ((Fin ('Succ m) -> [Fin ('Succ m)])
    -> Kleisli [] (Fin ('Succ m)) (Fin ('Succ m)))
-> (Fin ('Succ m) -> [Fin ('Succ m)])
-> Join (Kleisli []) (Fin ('Succ m))
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. (a -> [b]) -> Kleisli [] a b
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli @[] ((Fin ('Succ m) -> [Fin ('Succ m)])
 -> Compose (Join (Kleisli [])) Fin ('Succ m))
-> (Fin ('Succ m) -> [Fin ('Succ m)])
-> Compose (Join (Kleisli [])) Fin ('Succ m)
forall a b. (a -> b) -> a -> b
$ \ case
        Zero -> Fin ('Succ m)
forall (n :: Peano). Fin ('Succ n)
Zero Fin ('Succ m) -> [Fin ('Succ m)] -> [Fin ('Succ m)]
forall a. a -> [a] -> [a]
: (Fin m -> Fin ('Succ m)
forall (n :: Peano). Fin n -> Fin ('Succ n)
Succ (Fin m -> Fin ('Succ m)) -> [Fin m] -> [Fin ('Succ m)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List m (Fin m) -> [Fin m]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList List m (Fin m)
forall (n :: Peano). Natural n => List n (Fin n)
enum)
        Succ n :: Fin n
n -> ([Fin ('Succ m)] -> [Fin ('Succ m)]
forall a. [a] -> [a]
L.tail ([Fin ('Succ m)] -> [Fin ('Succ m)])
-> (Fin m -> [Fin ('Succ m)]) -> Fin m -> [Fin ('Succ m)]
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Fin ('Succ m) -> [Fin ('Succ m)]
forall a. Enum a => a -> [a]
enumFrom (Fin ('Succ m) -> [Fin ('Succ m)])
-> (Fin m -> Fin ('Succ m)) -> Fin m -> [Fin ('Succ m)]
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Fin m -> Fin ('Succ m)
forall (n :: Peano). Fin n -> Fin ('Succ n)
inj₁) Fin n
n

newtype Join s a = Join { Join s a -> s a a
unJoin :: s a a }

-- | Enumerate all values of type @'Fin' n@, in ascending order.
enum :: Natural n => List n (Fin n)
enum :: List n (Fin n)
enum = Ap List Fin n -> List n (Fin n)
forall k1 k2 (f :: k2 -> k1 -> *) (x :: k2 -> k1) (a :: k2).
Ap f x a -> f a (x a)
ap (Ap List Fin n -> List n (Fin n))
-> Ap List Fin n -> List n (Fin n)
forall a b. (a -> b) -> a -> b
$ Ap List Fin 'Zero
-> (forall (m :: Peano). Natural m => Ap List Fin ('Succ m))
-> Ap List Fin n
forall (n :: Peano) (f :: Peano -> *).
Natural n =>
f 'Zero -> (forall (m :: Peano). Natural m => f ('Succ m)) -> f n
natural (List 'Zero (Fin 'Zero) -> Ap List Fin 'Zero
forall k2 k1 (f :: k2 -> k1 -> *) (x :: k2 -> k1) (a :: k2).
f a (x a) -> Ap f x a
Ap List 'Zero (Fin 'Zero)
forall a. List 'Zero a
Nil) (List ('Succ m) (Fin ('Succ m)) -> Ap List Fin ('Succ m)
forall k2 k1 (f :: k2 -> k1 -> *) (x :: k2 -> k1) (a :: k2).
f a (x a) -> Ap f x a
Ap (Fin ('Succ m)
forall (n :: Peano). Fin ('Succ n)
Zero Fin ('Succ m)
-> List m (Fin ('Succ m)) -> List ('Succ m) (Fin ('Succ m))
forall a (n :: Peano). a -> List n a -> List ('Succ n) a
:. (Fin m -> Fin ('Succ m)
forall (n :: Peano). Fin n -> Fin ('Succ n)
Succ (Fin m -> Fin ('Succ m))
-> List m (Fin m) -> List m (Fin ('Succ m))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List m (Fin m)
forall (n :: Peano). Natural n => List n (Fin n)
enum)))

instance Natural n => Num (Fin n) where
    + :: Fin n -> Fin n -> Fin n
(+) = Join₂ (->) (Fin n) -> Fin n -> Fin n -> Fin n
forall (s :: * -> * -> *) a. Join₂ s a -> s a (s a a)
unJoin₂ (Join₂ (->) (Fin n) -> Fin n -> Fin n -> Fin n)
-> (Compose (Join₂ (->)) Fin n -> Join₂ (->) (Fin n))
-> Compose (Join₂ (->)) Fin n
-> Fin n
-> Fin n
-> Fin n
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Compose (Join₂ (->)) Fin n -> Join₂ (->) (Fin n)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose (Join₂ (->)) Fin n -> Fin n -> Fin n -> Fin n)
-> Compose (Join₂ (->)) Fin n -> Fin n -> Fin n -> Fin n
forall a b. (a -> b) -> a -> b
$ Compose (Join₂ (->)) Fin 'Zero
-> (forall (m :: Peano).
    Natural m =>
    Compose (Join₂ (->)) Fin ('Succ m))
-> Compose (Join₂ (->)) Fin n
forall (n :: Peano) (f :: Peano -> *).
Natural n =>
f 'Zero -> (forall (m :: Peano). Natural m => f ('Succ m)) -> f n
natural (Join₂ (->) (Fin 'Zero) -> Compose (Join₂ (->)) Fin 'Zero
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Join₂ (->) (Fin 'Zero) -> Compose (Join₂ (->)) Fin 'Zero)
-> ((Fin 'Zero -> Fin 'Zero -> Fin 'Zero)
    -> Join₂ (->) (Fin 'Zero))
-> (Fin 'Zero -> Fin 'Zero -> Fin 'Zero)
-> Compose (Join₂ (->)) Fin 'Zero
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Fin 'Zero -> Fin 'Zero -> Fin 'Zero) -> Join₂ (->) (Fin 'Zero)
forall (s :: * -> * -> *) a. s a (s a a) -> Join₂ s a
Join₂ ((Fin 'Zero -> Fin 'Zero -> Fin 'Zero)
 -> Compose (Join₂ (->)) Fin 'Zero)
-> (Fin 'Zero -> Fin 'Zero -> Fin 'Zero)
-> Compose (Join₂ (->)) Fin 'Zero
forall a b. (a -> b) -> a -> b
$ \ case) ((forall (m :: Peano).
  Natural m =>
  Compose (Join₂ (->)) Fin ('Succ m))
 -> Compose (Join₂ (->)) Fin n)
-> (forall (m :: Peano).
    Natural m =>
    Compose (Join₂ (->)) Fin ('Succ m))
-> Compose (Join₂ (->)) Fin n
forall a b. (a -> b) -> a -> b
$ Join₂ (->) (Fin ('Succ m)) -> Compose (Join₂ (->)) Fin ('Succ m)
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Join₂ (->) (Fin ('Succ m)) -> Compose (Join₂ (->)) Fin ('Succ m))
-> ((Fin ('Succ m) -> Fin ('Succ m) -> Fin ('Succ m))
    -> Join₂ (->) (Fin ('Succ m)))
-> (Fin ('Succ m) -> Fin ('Succ m) -> Fin ('Succ m))
-> Compose (Join₂ (->)) Fin ('Succ m)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Fin ('Succ m) -> Fin ('Succ m) -> Fin ('Succ m))
-> Join₂ (->) (Fin ('Succ m))
forall (s :: * -> * -> *) a. s a (s a a) -> Join₂ s a
Join₂ ((Fin ('Succ m) -> Fin ('Succ m) -> Fin ('Succ m))
 -> Compose (Join₂ (->)) Fin ('Succ m))
-> (Fin ('Succ m) -> Fin ('Succ m) -> Fin ('Succ m))
-> Compose (Join₂ (->)) Fin ('Succ m)
forall a b. (a -> b) -> a -> b
$ \ a :: Fin ('Succ m)
a b :: Fin ('Succ m)
b -> Natural -> Fin ('Succ m)
forall (n :: Peano) a.
(Natural n, Integral a) =>
a -> Fin ('Succ n)
toFin (Natural -> Fin ('Succ m)) -> Natural -> Fin ('Succ m)
forall a b. (a -> b) -> a -> b
$ (Num Natural => Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
(+) @N.Natural (Natural -> Natural -> Natural)
-> (Fin ('Succ m) -> Natural)
-> Fin ('Succ m)
-> Fin ('Succ m)
-> Natural
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Fin ('Succ m) -> Natural
forall a (n :: Peano). Integral a => Fin n -> a
fromFin) Fin ('Succ m)
a Fin ('Succ m)
b
    (-) = Join₂ (->) (Fin n) -> Fin n -> Fin n -> Fin n
forall (s :: * -> * -> *) a. Join₂ s a -> s a (s a a)
unJoin₂ (Join₂ (->) (Fin n) -> Fin n -> Fin n -> Fin n)
-> (Compose (Join₂ (->)) Fin n -> Join₂ (->) (Fin n))
-> Compose (Join₂ (->)) Fin n
-> Fin n
-> Fin n
-> Fin n
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Compose (Join₂ (->)) Fin n -> Join₂ (->) (Fin n)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose (Join₂ (->)) Fin n -> Fin n -> Fin n -> Fin n)
-> Compose (Join₂ (->)) Fin n -> Fin n -> Fin n -> Fin n
forall a b. (a -> b) -> a -> b
$ Compose (Join₂ (->)) Fin 'Zero
-> (forall (m :: Peano).
    Natural m =>
    Compose (Join₂ (->)) Fin ('Succ m))
-> Compose (Join₂ (->)) Fin n
forall (n :: Peano) (f :: Peano -> *).
Natural n =>
f 'Zero -> (forall (m :: Peano). Natural m => f ('Succ m)) -> f n
natural (Join₂ (->) (Fin 'Zero) -> Compose (Join₂ (->)) Fin 'Zero
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Join₂ (->) (Fin 'Zero) -> Compose (Join₂ (->)) Fin 'Zero)
-> ((Fin 'Zero -> Fin 'Zero -> Fin 'Zero)
    -> Join₂ (->) (Fin 'Zero))
-> (Fin 'Zero -> Fin 'Zero -> Fin 'Zero)
-> Compose (Join₂ (->)) Fin 'Zero
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Fin 'Zero -> Fin 'Zero -> Fin 'Zero) -> Join₂ (->) (Fin 'Zero)
forall (s :: * -> * -> *) a. s a (s a a) -> Join₂ s a
Join₂ ((Fin 'Zero -> Fin 'Zero -> Fin 'Zero)
 -> Compose (Join₂ (->)) Fin 'Zero)
-> (Fin 'Zero -> Fin 'Zero -> Fin 'Zero)
-> Compose (Join₂ (->)) Fin 'Zero
forall a b. (a -> b) -> a -> b
$ \ case) ((forall (m :: Peano).
  Natural m =>
  Compose (Join₂ (->)) Fin ('Succ m))
 -> Compose (Join₂ (->)) Fin n)
-> (forall (m :: Peano).
    Natural m =>
    Compose (Join₂ (->)) Fin ('Succ m))
-> Compose (Join₂ (->)) Fin n
forall a b. (a -> b) -> a -> b
$ Join₂ (->) (Fin ('Succ m)) -> Compose (Join₂ (->)) Fin ('Succ m)
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Join₂ (->) (Fin ('Succ m)) -> Compose (Join₂ (->)) Fin ('Succ m))
-> ((Fin ('Succ m) -> Fin ('Succ m) -> Fin ('Succ m))
    -> Join₂ (->) (Fin ('Succ m)))
-> (Fin ('Succ m) -> Fin ('Succ m) -> Fin ('Succ m))
-> Compose (Join₂ (->)) Fin ('Succ m)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Fin ('Succ m) -> Fin ('Succ m) -> Fin ('Succ m))
-> Join₂ (->) (Fin ('Succ m))
forall (s :: * -> * -> *) a. s a (s a a) -> Join₂ s a
Join₂ ((Fin ('Succ m) -> Fin ('Succ m) -> Fin ('Succ m))
 -> Compose (Join₂ (->)) Fin ('Succ m))
-> (Fin ('Succ m) -> Fin ('Succ m) -> Fin ('Succ m))
-> Compose (Join₂ (->)) Fin ('Succ m)
forall a b. (a -> b) -> a -> b
$ \ a :: Fin ('Succ m)
a b :: Fin ('Succ m)
b -> Integer -> Fin ('Succ m)
forall (n :: Peano) a.
(Natural n, Integral a) =>
a -> Fin ('Succ n)
toFin (Integer -> Fin ('Succ m)) -> Integer -> Fin ('Succ m)
forall a b. (a -> b) -> a -> b
$ ((-) @  Integer (Integer -> Integer -> Integer)
-> (Fin ('Succ m) -> Integer)
-> Fin ('Succ m)
-> Fin ('Succ m)
-> Integer
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Fin ('Succ m) -> Integer
forall a (n :: Peano). Integral a => Fin n -> a
fromFin) Fin ('Succ m)
a Fin ('Succ m)
b
    * :: Fin n -> Fin n -> Fin n
(*) = Join₂ (->) (Fin n) -> Fin n -> Fin n -> Fin n
forall (s :: * -> * -> *) a. Join₂ s a -> s a (s a a)
unJoin₂ (Join₂ (->) (Fin n) -> Fin n -> Fin n -> Fin n)
-> (Compose (Join₂ (->)) Fin n -> Join₂ (->) (Fin n))
-> Compose (Join₂ (->)) Fin n
-> Fin n
-> Fin n
-> Fin n
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Compose (Join₂ (->)) Fin n -> Join₂ (->) (Fin n)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose (Join₂ (->)) Fin n -> Fin n -> Fin n -> Fin n)
-> Compose (Join₂ (->)) Fin n -> Fin n -> Fin n -> Fin n
forall a b. (a -> b) -> a -> b
$ Compose (Join₂ (->)) Fin 'Zero
-> (forall (m :: Peano).
    Natural m =>
    Compose (Join₂ (->)) Fin ('Succ m))
-> Compose (Join₂ (->)) Fin n
forall (n :: Peano) (f :: Peano -> *).
Natural n =>
f 'Zero -> (forall (m :: Peano). Natural m => f ('Succ m)) -> f n
natural (Join₂ (->) (Fin 'Zero) -> Compose (Join₂ (->)) Fin 'Zero
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Join₂ (->) (Fin 'Zero) -> Compose (Join₂ (->)) Fin 'Zero)
-> ((Fin 'Zero -> Fin 'Zero -> Fin 'Zero)
    -> Join₂ (->) (Fin 'Zero))
-> (Fin 'Zero -> Fin 'Zero -> Fin 'Zero)
-> Compose (Join₂ (->)) Fin 'Zero
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Fin 'Zero -> Fin 'Zero -> Fin 'Zero) -> Join₂ (->) (Fin 'Zero)
forall (s :: * -> * -> *) a. s a (s a a) -> Join₂ s a
Join₂ ((Fin 'Zero -> Fin 'Zero -> Fin 'Zero)
 -> Compose (Join₂ (->)) Fin 'Zero)
-> (Fin 'Zero -> Fin 'Zero -> Fin 'Zero)
-> Compose (Join₂ (->)) Fin 'Zero
forall a b. (a -> b) -> a -> b
$ \ case) ((forall (m :: Peano).
  Natural m =>
  Compose (Join₂ (->)) Fin ('Succ m))
 -> Compose (Join₂ (->)) Fin n)
-> (forall (m :: Peano).
    Natural m =>
    Compose (Join₂ (->)) Fin ('Succ m))
-> Compose (Join₂ (->)) Fin n
forall a b. (a -> b) -> a -> b
$ Join₂ (->) (Fin ('Succ m)) -> Compose (Join₂ (->)) Fin ('Succ m)
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Join₂ (->) (Fin ('Succ m)) -> Compose (Join₂ (->)) Fin ('Succ m))
-> ((Fin ('Succ m) -> Fin ('Succ m) -> Fin ('Succ m))
    -> Join₂ (->) (Fin ('Succ m)))
-> (Fin ('Succ m) -> Fin ('Succ m) -> Fin ('Succ m))
-> Compose (Join₂ (->)) Fin ('Succ m)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Fin ('Succ m) -> Fin ('Succ m) -> Fin ('Succ m))
-> Join₂ (->) (Fin ('Succ m))
forall (s :: * -> * -> *) a. s a (s a a) -> Join₂ s a
Join₂ ((Fin ('Succ m) -> Fin ('Succ m) -> Fin ('Succ m))
 -> Compose (Join₂ (->)) Fin ('Succ m))
-> (Fin ('Succ m) -> Fin ('Succ m) -> Fin ('Succ m))
-> Compose (Join₂ (->)) Fin ('Succ m)
forall a b. (a -> b) -> a -> b
$ \ a :: Fin ('Succ m)
a b :: Fin ('Succ m)
b -> Natural -> Fin ('Succ m)
forall (n :: Peano) a.
(Natural n, Integral a) =>
a -> Fin ('Succ n)
toFin (Natural -> Fin ('Succ m)) -> Natural -> Fin ('Succ m)
forall a b. (a -> b) -> a -> b
$ (Num Natural => Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
(*) @N.Natural (Natural -> Natural -> Natural)
-> (Fin ('Succ m) -> Natural)
-> Fin ('Succ m)
-> Fin ('Succ m)
-> Natural
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Fin ('Succ m) -> Natural
forall a (n :: Peano). Integral a => Fin n -> a
fromFin) Fin ('Succ m)
a Fin ('Succ m)
b
    abs :: Fin n -> Fin n
abs = Fin n -> Fin n
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
    negate :: Fin n -> Fin n
negate = Join (->) (Fin n) -> Fin n -> Fin n
forall k (s :: k -> k -> *) (a :: k). Join s a -> s a a
unJoin (Join (->) (Fin n) -> Fin n -> Fin n)
-> (Compose (Join (->)) Fin n -> Join (->) (Fin n))
-> Compose (Join (->)) Fin n
-> Fin n
-> Fin n
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Compose (Join (->)) Fin n -> Join (->) (Fin n)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose (Join (->)) Fin n -> Fin n -> Fin n)
-> Compose (Join (->)) Fin n -> Fin n -> Fin n
forall a b. (a -> b) -> a -> b
$ Compose (Join (->)) Fin 'Zero
-> (forall (m :: Peano).
    Natural m =>
    Compose (Join (->)) Fin ('Succ m))
-> Compose (Join (->)) Fin n
forall (n :: Peano) (f :: Peano -> *).
Natural n =>
f 'Zero -> (forall (m :: Peano). Natural m => f ('Succ m)) -> f n
natural (Join (->) (Fin 'Zero) -> Compose (Join (->)) Fin 'Zero
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Join (->) (Fin 'Zero) -> Compose (Join (->)) Fin 'Zero)
-> ((Fin 'Zero -> Fin 'Zero) -> Join (->) (Fin 'Zero))
-> (Fin 'Zero -> Fin 'Zero)
-> Compose (Join (->)) Fin 'Zero
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Fin 'Zero -> Fin 'Zero) -> Join (->) (Fin 'Zero)
forall k (s :: k -> k -> *) (a :: k). s a a -> Join s a
Join ((Fin 'Zero -> Fin 'Zero) -> Compose (Join (->)) Fin 'Zero)
-> (Fin 'Zero -> Fin 'Zero) -> Compose (Join (->)) Fin 'Zero
forall a b. (a -> b) -> a -> b
$ \ case) ((forall (m :: Peano).
  Natural m =>
  Compose (Join (->)) Fin ('Succ m))
 -> Compose (Join (->)) Fin n)
-> (forall (m :: Peano).
    Natural m =>
    Compose (Join (->)) Fin ('Succ m))
-> Compose (Join (->)) Fin n
forall a b. (a -> b) -> a -> b
$ Join (->) (Fin ('Succ m)) -> Compose (Join (->)) Fin ('Succ m)
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Join (->) (Fin ('Succ m)) -> Compose (Join (->)) Fin ('Succ m))
-> ((Fin ('Succ m) -> Fin ('Succ m)) -> Join (->) (Fin ('Succ m)))
-> (Fin ('Succ m) -> Fin ('Succ m))
-> Compose (Join (->)) Fin ('Succ m)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Fin ('Succ m) -> Fin ('Succ m)) -> Join (->) (Fin ('Succ m))
forall k (s :: k -> k -> *) (a :: k). s a a -> Join s a
Join ((Fin ('Succ m) -> Fin ('Succ m))
 -> Compose (Join (->)) Fin ('Succ m))
-> (Fin ('Succ m) -> Fin ('Succ m))
-> Compose (Join (->)) Fin ('Succ m)
forall a b. (a -> b) -> a -> b
$ \ a :: Fin ('Succ m)
a -> Integer -> Fin ('Succ m)
forall (n :: Peano) a.
(Natural n, Integral a) =>
a -> Fin ('Succ n)
toFin (Integer -> Fin ('Succ m)) -> Integer -> Fin ('Succ m)
forall a b. (a -> b) -> a -> b
$ (Num Integer => Integer -> Integer
forall a. Num a => a -> a
negate @Integer (Integer -> Integer)
-> (Fin ('Succ m) -> Integer) -> Fin ('Succ m) -> Integer
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Fin ('Succ m) -> Integer
forall a (n :: Peano). Integral a => Fin n -> a
fromFin) Fin ('Succ m)
a
    signum :: Fin n -> Fin n
signum = Join (->) (Fin n) -> Fin n -> Fin n
forall k (s :: k -> k -> *) (a :: k). Join s a -> s a a
unJoin (Join (->) (Fin n) -> Fin n -> Fin n)
-> (Compose (Join (->)) Fin n -> Join (->) (Fin n))
-> Compose (Join (->)) Fin n
-> Fin n
-> Fin n
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Compose (Join (->)) Fin n -> Join (->) (Fin n)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose (Join (->)) Fin n -> Fin n -> Fin n)
-> Compose (Join (->)) Fin n -> Fin n -> Fin n
forall a b. (a -> b) -> a -> b
$ Compose (Join (->)) Fin 'Zero
-> (forall (m :: Peano).
    Natural m =>
    Compose (Join (->)) Fin ('Succ m))
-> Compose (Join (->)) Fin n
forall (n :: Peano) (f :: Peano -> *).
Natural n =>
f 'Zero -> (forall (m :: Peano). Natural m => f ('Succ m)) -> f n
natural (Join (->) (Fin 'Zero) -> Compose (Join (->)) Fin 'Zero
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Join (->) (Fin 'Zero) -> Compose (Join (->)) Fin 'Zero)
-> ((Fin 'Zero -> Fin 'Zero) -> Join (->) (Fin 'Zero))
-> (Fin 'Zero -> Fin 'Zero)
-> Compose (Join (->)) Fin 'Zero
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Fin 'Zero -> Fin 'Zero) -> Join (->) (Fin 'Zero)
forall k (s :: k -> k -> *) (a :: k). s a a -> Join s a
Join ((Fin 'Zero -> Fin 'Zero) -> Compose (Join (->)) Fin 'Zero)
-> (Fin 'Zero -> Fin 'Zero) -> Compose (Join (->)) Fin 'Zero
forall a b. (a -> b) -> a -> b
$ \ case) ((forall (m :: Peano).
  Natural m =>
  Compose (Join (->)) Fin ('Succ m))
 -> Compose (Join (->)) Fin n)
-> (forall (m :: Peano).
    Natural m =>
    Compose (Join (->)) Fin ('Succ m))
-> Compose (Join (->)) Fin n
forall a b. (a -> b) -> a -> b
$ Join (->) (Fin ('Succ m)) -> Compose (Join (->)) Fin ('Succ m)
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Join (->) (Fin ('Succ m)) -> Compose (Join (->)) Fin ('Succ m))
-> ((Fin ('Succ m) -> Fin ('Succ m)) -> Join (->) (Fin ('Succ m)))
-> (Fin ('Succ m) -> Fin ('Succ m))
-> Compose (Join (->)) Fin ('Succ m)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Fin ('Succ m) -> Fin ('Succ m)) -> Join (->) (Fin ('Succ m))
forall k (s :: k -> k -> *) (a :: k). s a a -> Join s a
Join ((Fin ('Succ m) -> Fin ('Succ m))
 -> Compose (Join (->)) Fin ('Succ m))
-> (Fin ('Succ m) -> Fin ('Succ m))
-> Compose (Join (->)) Fin ('Succ m)
forall a b. (a -> b) -> a -> b
$ \ case
        Zero -> Fin ('Succ m)
forall (n :: Peano). Fin ('Succ n)
Zero
        Succ _ -> Natural -> Fin ('Succ m)
forall (n :: Peano) a.
(Natural n, Integral a) =>
a -> Fin ('Succ n)
toFin (1 :: N.Natural)
    fromInteger :: Integer -> Fin n
fromInteger n :: Integer
n = Fin 'Zero
-> (forall (n :: Peano). Natural n => Fin ('Succ n)) -> Fin n
forall (n :: Peano) (f :: Peano -> *).
Natural n =>
f 'Zero -> (forall (m :: Peano). Natural m => f ('Succ m)) -> f n
natural (String -> Fin 'Zero
forall a. HasCallStack => String -> a
error "fromInteger @(Fin Zero)") (Integer -> Fin ('Succ m)
forall (n :: Peano) a.
(Natural n, Integral a) =>
a -> Fin ('Succ n)
toFin Integer
n)

newtype Join₂ s a = Join₂ { Join₂ s a -> s a (s a a)
unJoin₂ :: s a (s a a) }

inj₁ :: Fin n -> Fin (P.Succ n)
inj₁ :: Fin n -> Fin ('Succ n)
inj₁ Zero = Fin ('Succ n)
forall (n :: Peano). Fin ('Succ n)
Zero
inj₁ (Succ n :: Fin n
n) = Fin ('Succ n) -> Fin ('Succ ('Succ n))
forall (n :: Peano). Fin n -> Fin ('Succ n)
Succ (Fin n -> Fin ('Succ n)
forall (n :: Peano). Fin n -> Fin ('Succ n)
inj₁ Fin n
n)

proj₁ :: Natural n => Fin (P.Succ n) -> Maybe (Fin n)
proj₁ :: Fin ('Succ n) -> Maybe (Fin n)
proj₁ = Proj₁ n -> Fin ('Succ n) -> Maybe (Fin n)
forall (n :: Peano). Proj₁ n -> Fin ('Succ n) -> Maybe (Fin n)
unProj₁ (Proj₁ n -> Fin ('Succ n) -> Maybe (Fin n))
-> Proj₁ n -> Fin ('Succ n) -> Maybe (Fin n)
forall a b. (a -> b) -> a -> b
$ Proj₁ 'Zero
-> (forall (m :: Peano). Natural m => Proj₁ ('Succ m)) -> Proj₁ n
forall (n :: Peano) (f :: Peano -> *).
Natural n =>
f 'Zero -> (forall (m :: Peano). Natural m => f ('Succ m)) -> f n
natural ((Fin ('Succ 'Zero) -> Maybe (Fin 'Zero)) -> Proj₁ 'Zero
forall (n :: Peano). (Fin ('Succ n) -> Maybe (Fin n)) -> Proj₁ n
Proj₁ ((Fin ('Succ 'Zero) -> Maybe (Fin 'Zero)) -> Proj₁ 'Zero)
-> (Fin ('Succ 'Zero) -> Maybe (Fin 'Zero)) -> Proj₁ 'Zero
forall a b. (a -> b) -> a -> b
$ \ case Zero -> Maybe (Fin 'Zero)
forall a. Maybe a
Nothing
                                          Succ n :: Fin n
n -> case Fin n
n of)
                          ((Fin ('Succ ('Succ m)) -> Maybe (Fin ('Succ m))) -> Proj₁ ('Succ m)
forall (n :: Peano). (Fin ('Succ n) -> Maybe (Fin n)) -> Proj₁ n
Proj₁ ((Fin ('Succ ('Succ m)) -> Maybe (Fin ('Succ m)))
 -> Proj₁ ('Succ m))
-> (Fin ('Succ ('Succ m)) -> Maybe (Fin ('Succ m)))
-> Proj₁ ('Succ m)
forall a b. (a -> b) -> a -> b
$ \ case Zero -> Fin ('Succ m) -> Maybe (Fin ('Succ m))
forall a. a -> Maybe a
Just Fin ('Succ m)
forall (n :: Peano). Fin ('Succ n)
Zero
                                          Succ n :: Fin n
n -> Fin m -> Fin ('Succ m)
forall (n :: Peano). Fin n -> Fin ('Succ n)
Succ (Fin m -> Fin ('Succ m)) -> Maybe (Fin m) -> Maybe (Fin ('Succ m))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Fin ('Succ m) -> Maybe (Fin m)
forall (n :: Peano). Natural n => Fin ('Succ n) -> Maybe (Fin n)
proj₁ Fin n
Fin ('Succ m)
n)

newtype Proj₁ n = Proj₁ { Proj₁ n -> Fin ('Succ n) -> Maybe (Fin n)
unProj₁ :: Fin (P.Succ n) -> Maybe (Fin n) }

lift₁ :: (Fin m -> Fin n) -> Fin (P.Succ m) -> Fin (P.Succ n)
lift₁ :: (Fin m -> Fin n) -> Fin ('Succ m) -> Fin ('Succ n)
lift₁ _ Zero = Fin ('Succ n)
forall (n :: Peano). Fin ('Succ n)
Zero
lift₁ f :: Fin m -> Fin n
f (Succ n :: Fin n
n) = Fin n -> Fin ('Succ n)
forall (n :: Peano). Fin n -> Fin ('Succ n)
Succ (Fin m -> Fin n
f Fin m
Fin n
n)

fromFin :: Integral a => Fin n -> a
fromFin :: Fin n -> a
fromFin Zero = 0
fromFin (Succ n :: Fin n
n) = a -> a
forall a. Enum a => a -> a
succ (Fin n -> a
forall a (n :: Peano). Integral a => Fin n -> a
fromFin Fin n
n)

-- | Convert to 'Fin', modulo @n@.
toFin :: ∀ n a . (Natural n, Integral a) => a -> Fin (P.Succ n)
toFin :: a -> Fin ('Succ n)
toFin = Maybe (Fin ('Succ n)) -> Fin ('Succ n)
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Fin ('Succ n)) -> Fin ('Succ n))
-> (a -> Maybe (Fin ('Succ n))) -> a -> Fin ('Succ n)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> Maybe (Fin ('Succ n))
forall (n :: Peano) a.
(Natural n, Integral a) =>
a -> Maybe (Fin n)
toFinMay (a -> Maybe (Fin ('Succ n)))
-> (a -> a) -> a -> Maybe (Fin ('Succ n))
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (a -> a -> a
forall a. Integral a => a -> a -> a
`mod` Const a n -> a
forall a k (b :: k). Const a b -> a
getConst ((a -> a) -> a -> Const a n
forall (n :: Peano) a. Natural n => (a -> a) -> a -> Const a n
iterate @n (a -> a -> a
forall a. Num a => a -> a -> a
+1) 1))

-- | Convert to 'Fin', failing if the argument is out of bounds.
toFinMay :: (Natural n, Integral a) => a -> Maybe (Fin n)
toFinMay :: a -> Maybe (Fin n)
toFinMay = Compose ((->) a) Maybe (Fin n) -> a -> Maybe (Fin n)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose ((->) a) Maybe (Fin n) -> a -> Maybe (Fin n))
-> (Compose (Compose ((->) a) Maybe) Fin n
    -> Compose ((->) a) Maybe (Fin n))
-> Compose (Compose ((->) a) Maybe) Fin n
-> a
-> Maybe (Fin n)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Compose (Compose ((->) a) Maybe) Fin n
-> Compose ((->) a) Maybe (Fin n)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose (Compose ((->) a) Maybe) Fin n -> a -> Maybe (Fin n))
-> Compose (Compose ((->) a) Maybe) Fin n -> a -> Maybe (Fin n)
forall a b. (a -> b) -> a -> b
$
           Compose (Compose ((->) a) Maybe) Fin 'Zero
-> (forall (m :: Peano).
    Natural m =>
    Compose (Compose ((->) a) Maybe) Fin ('Succ m))
-> Compose (Compose ((->) a) Maybe) Fin n
forall (n :: Peano) (f :: Peano -> *).
Natural n =>
f 'Zero -> (forall (m :: Peano). Natural m => f ('Succ m)) -> f n
natural (Compose ((->) a) Maybe (Fin 'Zero)
-> Compose (Compose ((->) a) Maybe) Fin 'Zero
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Compose ((->) a) Maybe (Fin 'Zero)
 -> Compose (Compose ((->) a) Maybe) Fin 'Zero)
-> ((a -> Maybe (Fin 'Zero)) -> Compose ((->) a) Maybe (Fin 'Zero))
-> (a -> Maybe (Fin 'Zero))
-> Compose (Compose ((->) a) Maybe) Fin 'Zero
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (a -> Maybe (Fin 'Zero)) -> Compose ((->) a) Maybe (Fin 'Zero)
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose ((a -> Maybe (Fin 'Zero))
 -> Compose (Compose ((->) a) Maybe) Fin 'Zero)
-> (a -> Maybe (Fin 'Zero))
-> Compose (Compose ((->) a) Maybe) Fin 'Zero
forall a b. (a -> b) -> a -> b
$ Maybe (Fin 'Zero) -> a -> Maybe (Fin 'Zero)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Fin 'Zero)
forall a. Maybe a
Nothing)
                   (Compose ((->) a) Maybe (Fin ('Succ m))
-> Compose (Compose ((->) a) Maybe) Fin ('Succ m)
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Compose ((->) a) Maybe (Fin ('Succ m))
 -> Compose (Compose ((->) a) Maybe) Fin ('Succ m))
-> ((a -> Maybe (Fin ('Succ m)))
    -> Compose ((->) a) Maybe (Fin ('Succ m)))
-> (a -> Maybe (Fin ('Succ m)))
-> Compose (Compose ((->) a) Maybe) Fin ('Succ m)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (a -> Maybe (Fin ('Succ m)))
-> Compose ((->) a) Maybe (Fin ('Succ m))
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose ((a -> Maybe (Fin ('Succ m)))
 -> Compose (Compose ((->) a) Maybe) Fin ('Succ m))
-> (a -> Maybe (Fin ('Succ m)))
-> Compose (Compose ((->) a) Maybe) Fin ('Succ m)
forall a b. (a -> b) -> a -> b
$ \ case 0 -> Fin ('Succ m) -> Maybe (Fin ('Succ m))
forall a. a -> Maybe a
Just Fin ('Succ m)
forall (n :: Peano). Fin ('Succ n)
Zero
                                               n :: a
n -> Fin m -> Fin ('Succ m)
forall (n :: Peano). Fin n -> Fin ('Succ n)
Succ (Fin m -> Fin ('Succ m)) -> Maybe (Fin m) -> Maybe (Fin ('Succ m))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe (Fin m)
forall (n :: Peano) a.
(Natural n, Integral a) =>
a -> Maybe (Fin n)
toFinMay (a
na -> a -> a
forall a. Num a => a -> a -> a
-1))

-- | A list of exactly @n@ values of type @a@
infixr 5 :.
data List n a where
    Nil :: List P.Zero a
    (:.) :: a -> List n a -> List (P.Succ n) a

deriving instance (Eq   a) => Eq   (List n a)
deriving instance (Ord  a) => Ord  (List n a)
deriving instance Functor     (List n)
deriving instance Foldable    (List n)
deriving instance Traversable (List n)
deriving instance Typeable List

instance Show a => Show (List n a) where
    showsPrec :: Int -> List n a -> ShowS
showsPrec = Int -> List n a -> ShowS
forall (f :: * -> *) a. (Show1 f, Show a) => Int -> f a -> ShowS
showsPrec1

instance (Read a, Natural n) => Read (List n a) where
    readPrec :: ReadPrec (List n a)
readPrec = ReadPrec (List n a)
forall (f :: * -> *) a. (Read1 f, Read a) => ReadPrec (f a)
readPrec1

fromList :: Natural n => [a] -> Maybe (List n a)
fromList :: [a] -> Maybe (List n a)
fromList = T a n -> [a] -> Maybe (List n a)
forall a (n :: Peano). T a n -> [a] -> Maybe (List n a)
t (T a n -> [a] -> Maybe (List n a))
-> T a n -> [a] -> Maybe (List n a)
forall a b. (a -> b) -> a -> b
$ T a 'Zero
-> (forall (m :: Peano). Natural m => T a ('Succ m)) -> T a n
forall (n :: Peano) (f :: Peano -> *).
Natural n =>
f 'Zero -> (forall (m :: Peano). Natural m => f ('Succ m)) -> f n
natural (([a] -> Maybe (List 'Zero a)) -> T a 'Zero
forall a (n :: Peano). ([a] -> Maybe (List n a)) -> T a n
T (([a] -> Maybe (List 'Zero a)) -> T a 'Zero)
-> ([a] -> Maybe (List 'Zero a)) -> T a 'Zero
forall a b. (a -> b) -> a -> b
$ \ case [] -> List 'Zero a -> Maybe (List 'Zero a)
forall a. a -> Maybe a
Just List 'Zero a
forall a. List 'Zero a
Nil
                                   _  -> Maybe (List 'Zero a)
forall a. Maybe a
Nothing)
                       (([a] -> Maybe (List ('Succ m) a)) -> T a ('Succ m)
forall a (n :: Peano). ([a] -> Maybe (List n a)) -> T a n
T (([a] -> Maybe (List ('Succ m) a)) -> T a ('Succ m))
-> ([a] -> Maybe (List ('Succ m) a)) -> T a ('Succ m)
forall a b. (a -> b) -> a -> b
$ \ case [] -> Maybe (List ('Succ m) a)
forall a. Maybe a
Nothing
                                   x :: a
x:xs :: [a]
xs -> (a
xa -> List m a -> List ('Succ m) a
forall a (n :: Peano). a -> List n a -> List ('Succ n) a
:.) (List m a -> List ('Succ m) a)
-> Maybe (List m a) -> Maybe (List ('Succ m) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a] -> Maybe (List m a)
forall (n :: Peano) a. Natural n => [a] -> Maybe (List n a)
fromList [a]
xs)

newtype T a n = T { T a n -> [a] -> Maybe (List n a)
t :: [a] -> Maybe (List n a) }

instance Semigroup a => Semigroup (List n a) where
    Nil <> :: List n a -> List n a -> List n a
<> Nil = List n a
forall a. List 'Zero a
Nil
    (x :: a
x:.xs :: List n a
xs) <> (y :: a
y:.ys :: List n a
ys) = a
xa -> a -> a
forall a. Semigroup a => a -> a -> a
<>a
ya -> List n a -> List ('Succ n) a
forall a (n :: Peano). a -> List n a -> List ('Succ n) a
:.List n a
xsList n a -> List n a -> List n a
forall a. Semigroup a => a -> a -> a
<>List n a
List n a
ys

instance (Natural n, Monoid a) => Monoid (List n a) where
    mempty :: List n a
mempty = Flip List a n -> List n a
forall k k (f :: k -> k -> *) (a :: k) (b :: k).
Flip f a b -> f b a
unFlip (Flip List a n -> List n a) -> Flip List a n -> List n a
forall a b. (a -> b) -> a -> b
$ Flip List a 'Zero
-> (forall (m :: Peano). Natural m => Flip List a ('Succ m))
-> Flip List a n
forall (n :: Peano) (f :: Peano -> *).
Natural n =>
f 'Zero -> (forall (m :: Peano). Natural m => f ('Succ m)) -> f n
natural (List 'Zero a -> Flip List a 'Zero
forall k k (f :: k -> k -> *) (a :: k) (b :: k).
f b a -> Flip f a b
Flip List 'Zero a
forall a. List 'Zero a
Nil) (List ('Succ m) a -> Flip List a ('Succ m)
forall k k (f :: k -> k -> *) (a :: k) (b :: k).
f b a -> Flip f a b
Flip (List ('Succ m) a -> Flip List a ('Succ m))
-> List ('Succ m) a -> Flip List a ('Succ m)
forall a b. (a -> b) -> a -> b
$ a
forall a. Monoid a => a
memptya -> List m a -> List ('Succ m) a
forall a (n :: Peano). a -> List n a -> List ('Succ n) a
:.List m a
forall a. Monoid a => a
mempty)
    mappend :: List n a -> List n a -> List n a
mappend = List n a -> List n a -> List n a
forall a. Semigroup a => a -> a -> a
(<>)

instance Natural n => Applicative (List n) where
    pure :: a -> List n a
pure a :: a
a = Flip List a n -> List n a
forall k k (f :: k -> k -> *) (a :: k) (b :: k).
Flip f a b -> f b a
unFlip (Flip List a n -> List n a) -> Flip List a n -> List n a
forall a b. (a -> b) -> a -> b
$ Flip List a 'Zero
-> (forall (m :: Peano). Natural m => Flip List a ('Succ m))
-> Flip List a n
forall (n :: Peano) (f :: Peano -> *).
Natural n =>
f 'Zero -> (forall (m :: Peano). Natural m => f ('Succ m)) -> f n
natural (List 'Zero a -> Flip List a 'Zero
forall k k (f :: k -> k -> *) (a :: k) (b :: k).
f b a -> Flip f a b
Flip List 'Zero a
forall a. List 'Zero a
Nil) (List ('Succ m) a -> Flip List a ('Succ m)
forall k k (f :: k -> k -> *) (a :: k) (b :: k).
f b a -> Flip f a b
Flip (List ('Succ m) a -> Flip List a ('Succ m))
-> List ('Succ m) a -> Flip List a ('Succ m)
forall a b. (a -> b) -> a -> b
$ a
aa -> List m a -> List ('Succ m) a
forall a (n :: Peano). a -> List n a -> List ('Succ n) a
:.a -> List m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a)
    <*> :: List n (a -> b) -> List n a -> List n b
(<*>) = S a b n -> List n (a -> b) -> List n a -> List n b
forall a b (n :: Peano).
S a b n -> List n (a -> b) -> List n a -> List n b
unS (S a b n -> List n (a -> b) -> List n a -> List n b)
-> S a b n -> List n (a -> b) -> List n a -> List n b
forall a b. (a -> b) -> a -> b
$ S a b 'Zero
-> (forall (m :: Peano). Natural m => S a b ('Succ m)) -> S a b n
forall (n :: Peano) (f :: Peano -> *).
Natural n =>
f 'Zero -> (forall (m :: Peano). Natural m => f ('Succ m)) -> f n
natural ((List 'Zero (a -> b) -> List 'Zero a -> List 'Zero b)
-> S a b 'Zero
forall a b (n :: Peano).
(List n (a -> b) -> List n a -> List n b) -> S a b n
S ((List 'Zero (a -> b) -> List 'Zero a -> List 'Zero b)
 -> S a b 'Zero)
-> (List 'Zero (a -> b) -> List 'Zero a -> List 'Zero b)
-> S a b 'Zero
forall a b. (a -> b) -> a -> b
$ \ Nil Nil -> List 'Zero b
forall a. List 'Zero a
Nil)
                          ((List ('Succ m) (a -> b) -> List ('Succ m) a -> List ('Succ m) b)
-> S a b ('Succ m)
forall a b (n :: Peano).
(List n (a -> b) -> List n a -> List n b) -> S a b n
S ((List ('Succ m) (a -> b) -> List ('Succ m) a -> List ('Succ m) b)
 -> S a b ('Succ m))
-> (List ('Succ m) (a -> b)
    -> List ('Succ m) a -> List ('Succ m) b)
-> S a b ('Succ m)
forall a b. (a -> b) -> a -> b
$ \ (f :: a -> b
f:.fs :: List n (a -> b)
fs) (x :: a
x:.xs :: List n a
xs) -> a -> b
f a
x b -> List n b -> List ('Succ n) b
forall a (n :: Peano). a -> List n a -> List ('Succ n) a
:. (List n (a -> b)
fs List n (a -> b) -> List n a -> List n b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> List n a
List n a
xs))

newtype Flip f a b = Flip { Flip f a b -> f b a
unFlip :: f b a }

newtype S a b n = S { S a b n -> List n (a -> b) -> List n a -> List n b
unS :: List n (a -> b) -> List n a -> List n b }

instance Eq1 (List n) where
    liftEq :: (a -> b -> Bool) -> List n a -> List n b -> Bool
liftEq _ Nil Nil = Bool
True
    liftEq == :: a -> b -> Bool
(==) (x :: a
x:.xs :: List n a
xs) (y :: b
y:.ys :: List n b
ys) = a
x a -> b -> Bool
== b
y Bool -> Bool -> Bool
&& (a -> b -> Bool) -> List n a -> List n b -> Bool
forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
(==) List n a
xs List n b
List n b
ys

instance Ord1 (List n) where
    liftCompare :: (a -> b -> Ordering) -> List n a -> List n b -> Ordering
liftCompare _ Nil Nil = Ordering
EQ
    liftCompare cmp :: a -> b -> Ordering
cmp (x :: a
x:.xs :: List n a
xs) (y :: b
y:.ys :: List n b
ys) = a -> b -> Ordering
cmp a
x b
y Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> (a -> b -> Ordering) -> List n a -> List n b -> Ordering
forall (f :: * -> *) a b.
Ord1 f =>
(a -> b -> Ordering) -> f a -> f b -> Ordering
liftCompare a -> b -> Ordering
cmp List n a
xs List n b
List n b
ys

instance Show1 (List n) where
    liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> List n a -> ShowS
liftShowsPrec sp :: Int -> a -> ShowS
sp sl :: [a] -> ShowS
sl n :: Int
n = (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> [a] -> ShowS
forall (f :: * -> *) a.
Show1 f =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
sl Int
n ([a] -> ShowS) -> (List n a -> [a]) -> List n a -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. List n a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList

instance Natural n => Read1 (List n) where
    liftReadPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec (List n a)
liftReadPrec rp :: ReadPrec a
rp rl :: ReadPrec [a]
rl = [a] -> Maybe (List n a)
forall (n :: Peano) a. Natural n => [a] -> Maybe (List n a)
fromList ([a] -> Maybe (List n a))
-> ReadPrec [a] -> ReadPrec (Maybe (List n a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReadPrec a -> ReadPrec [a] -> ReadPrec [a]
forall (f :: * -> *) a.
Read1 f =>
ReadPrec a -> ReadPrec [a] -> ReadPrec (f a)
liftReadPrec ReadPrec a
rp ReadPrec [a]
rl ReadPrec (Maybe (List n a))
-> (Maybe (List n a) -> ReadPrec (List n a)) -> ReadPrec (List n a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ReadPrec (List n a)
-> (List n a -> ReadPrec (List n a))
-> Maybe (List n a)
-> ReadPrec (List n a)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ReadPrec (List n a)
forall (f :: * -> *) a. Alternative f => f a
empty List n a -> ReadPrec (List n a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure

instance Natural n => Foldable1 (List (P.Succ n)) where
    toNonEmpty :: List ('Succ n) a -> NonEmpty a
toNonEmpty (a :: a
a:.as :: List n a
as) = a
aa -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:|List n a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList List n a
as

uncons :: List (P.Succ n) a -> (a, List n a)
uncons :: List ('Succ n) a -> (a, List n a)
uncons (x :: a
x:.xs :: List n a
xs) = (a
x, List n a
List n a
xs)

head :: List (P.Succ n) a -> a
head :: List ('Succ n) a -> a
head = (a, List n a) -> a
forall a b. (a, b) -> a
fst ((a, List n a) -> a)
-> (List ('Succ n) a -> (a, List n a)) -> List ('Succ n) a -> a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. List ('Succ n) a -> (a, List n a)
forall (n :: Peano) a. List ('Succ n) a -> (a, List n a)
uncons

tail :: List (P.Succ n) a -> List n a
tail :: List ('Succ n) a -> List n a
tail = (a, List n a) -> List n a
forall a b. (a, b) -> b
snd ((a, List n a) -> List n a)
-> (List ('Succ n) a -> (a, List n a))
-> List ('Succ n) a
-> List n a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. List ('Succ n) a -> (a, List n a)
forall (n :: Peano) a. List ('Succ n) a -> (a, List n a)
uncons

init :: List (P.Succ n) a -> List n a
init :: List ('Succ n) a -> List n a
init (_:.Nil)       = List n a
forall a. List 'Zero a
Nil
init (x :: a
x:.xs :: List n a
xs@(_:._)) = a
xa -> List n a -> List ('Succ n) a
forall a (n :: Peano). a -> List n a -> List ('Succ n) a
:.List ('Succ n) a -> List n a
forall (n :: Peano) a. List ('Succ n) a -> List n a
init List n a
List ('Succ n) a
xs

last :: List (P.Succ n) a -> a
last :: List ('Succ n) a -> a
last (x :: a
x:.Nil) = a
x
last (_:.xs :: List n a
xs@(_:._)) = List ('Succ n) a -> a
forall (n :: Peano) a. List ('Succ n) a -> a
last List n a
List ('Succ n) a
xs

reverse :: List n a -> List n a
reverse :: List n a -> List n a
reverse Nil = List n a
forall a. List 'Zero a
Nil
reverse xs :: List n a
xs@(_:._) = (a -> List n a -> List ('Succ n) a)
-> (List ('Succ n) a -> a)
-> (List ('Succ n) a -> List n a)
-> List n a
-> List n a
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> List n a -> List ('Succ n) a
forall a (n :: Peano). a -> List n a -> List ('Succ n) a
(:.) List ('Succ n) a -> a
forall (n :: Peano) a. List ('Succ n) a -> a
last (List n a -> List n a
forall (n :: Peano) a. List n a -> List n a
reverse (List n a -> List n a)
-> (List ('Succ n) a -> List n a) -> List ('Succ n) a -> List n a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. List ('Succ n) a -> List n a
forall (n :: Peano) a. List ('Succ n) a -> List n a
init) List n a
xs

-- | Bring givenly many elements from the tail of the list to the front.
rotate :: Fin n -> List n a -> List n a
rotate :: Fin n -> List n a -> List n a
rotate Zero as :: List n a
as = List n a
as
rotate (Succ n :: Fin n
n) as :: List n a
as = Fin ('Succ n) -> List ('Succ n) a -> List ('Succ n) a
forall (n :: Peano) a. Fin n -> List n a -> List n a
rotate (Fin n -> Fin ('Succ n)
forall (n :: Peano). Fin n -> Fin ('Succ n)
inj₁ Fin n
n) (List ('Succ n) a -> List n a) -> List ('Succ n) a -> List n a
forall a b. (a -> b) -> a -> b
$ List ('Succ n) a -> a
forall (n :: Peano) a. List ('Succ n) a -> a
last List n a
List ('Succ n) a
as a -> List n a -> List ('Succ n) a
forall a (n :: Peano). a -> List n a -> List ('Succ n) a
:. List ('Succ n) a -> List n a
forall (n :: Peano) a. List ('Succ n) a -> List n a
init List n a
List ('Succ n) a
as

(!!) :: List n a -> Fin n -> a
Nil !! :: List n a -> Fin n -> a
!! n :: Fin n
n = case Fin n
n of
(x :: a
x:._)  !! Zero = a
x
(_:.xs :: List n a
xs) !! Succ n :: Fin n
n = List n a
xs List n a -> Fin n -> a
forall (n :: Peano) a. List n a -> Fin n -> a
!! Fin n
Fin n
n

-- | Focalize on the giventh element.
at :: Functor f => Fin n -> (a -> f a) -> List n a -> f (List n a)
at :: Fin n -> (a -> f a) -> List n a -> f (List n a)
at Zero f :: a -> f a
f (a :: a
a:.as :: List n a
as) = (a -> List n a -> List ('Succ n) a
forall a (n :: Peano). a -> List n a -> List ('Succ n) a
:.List n a
as) (a -> List ('Succ n) a) -> f a -> f (List ('Succ n) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
f a
a
at (Succ n :: Fin n
n) f :: a -> f a
f (a :: a
a:.as :: List n a
as) = (a
aa -> List n a -> List ('Succ n) a
forall a (n :: Peano). a -> List n a -> List ('Succ n) a
:.) (List n a -> List ('Succ n) a)
-> f (List n a) -> f (List ('Succ n) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Fin n -> (a -> f a) -> List n a -> f (List n a)
forall (f :: * -> *) (n :: Peano) a.
Functor f =>
Fin n -> (a -> f a) -> List n a -> f (List n a)
at Fin n
n a -> f a
f List n a
List n a
as

-- | Swap the 2 giventh elements of the list.
swap :: Fin n -> Fin n -> List n a -> List n a
swap :: Fin n -> Fin n -> List n a -> List n a
swap Zero Zero as :: List n a
as = List n a
as
swap (Succ m :: Fin n
m) (Succ n :: Fin n
n) (a :: a
a:.as :: List n a
as) = a
aa -> List n a -> List ('Succ n) a
forall a (n :: Peano). a -> List n a -> List ('Succ n) a
:.Fin n -> Fin n -> List n a -> List n a
forall (n :: Peano) a. Fin n -> Fin n -> List n a -> List n a
swap Fin n
m Fin n
Fin n
n List n a
List n a
as
swap Zero (Succ n :: Fin n
n) (a :: a
a:.as :: List n a
as) = (a -> List n a -> List ('Succ n) a)
-> (a, List n a) -> List ('Succ n) a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> List n a -> List ('Succ n) a
forall a (n :: Peano). a -> List n a -> List ('Succ n) a
(:.) ((a, List n a) -> List n a) -> (a, List n a) -> List n a
forall a b. (a -> b) -> a -> b
$ Fin n -> (a -> (a, a)) -> List n a -> (a, List n a)
forall (f :: * -> *) (n :: Peano) a.
Functor f =>
Fin n -> (a -> f a) -> List n a -> f (List n a)
at Fin n
n ((a -> a -> (a, a)) -> a -> a -> (a, a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) a
a) List n a
List n a
as
swap (Succ m :: Fin n
m) Zero (a :: a
a:.as :: List n a
as) = (a -> List n a -> List ('Succ n) a)
-> (a, List n a) -> List ('Succ n) a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> List n a -> List ('Succ n) a
forall a (n :: Peano). a -> List n a -> List ('Succ n) a
(:.) ((a, List n a) -> List n a) -> (a, List n a) -> List n a
forall a b. (a -> b) -> a -> b
$ Fin n -> (a -> (a, a)) -> List n a -> (a, List n a)
forall (f :: * -> *) (n :: Peano) a.
Functor f =>
Fin n -> (a -> f a) -> List n a -> f (List n a)
at Fin n
m ((a -> a -> (a, a)) -> a -> a -> (a, a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) a
a) List n a
List n a
as