{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Module    : Termonad.Config.Vec
-- Description : A small library of dependent types
-- Copyright   : (c) Dennis Gosnell, 2018
-- License     : BSD3
-- Stability   : experimental
-- Portability : POSIX
--
-- This is a small library of dependent types.  It provides indexed types like
-- 'Fin', 'Vec', and 'Matrix'.
--
-- This is mainly used in Termonad for "Termonad.Config.Colour" to represent
-- length-indexed colour lists.
--
-- This module implements a subset of the functionality from the abandoned
-- <http://hackage.haskell.org/package/type-combinators type-combinators> library.
-- Ideally this module would be split out to a separate package.
-- If you're interested in working on something like this, please see
-- <https://github.com/cdepillabout/termonad/issues/70 this issue> on Github.

module Termonad.Config.Vec
  -- ( Fin
  -- , I(I)
  -- , M(M)
  -- , N3
  -- , N24
  -- , N6
  -- , N8
  -- , Prod((:<), Ø)
  -- , Range
  -- , Vec
  -- , VecT((:+), (:*), ØV, EmptyV)
  -- , fin
  -- , genMatrix_
  -- , setSubmatrix
  -- , genVec_
  -- , vSetAt'
  -- )
    where

import Termonad.Prelude hiding ((\\), index)

import Data.Distributive (Distributive(distribute))
import qualified Data.Foldable as Data.Foldable
import Data.Functor.Rep (Representable(..), apRep, bindRep, distributeRep, pureRep)
import Data.Kind (Type)
import Data.Singletons.Prelude
import Data.Singletons.TH
import Text.Show (showParen, showString)
import Unsafe.Coerce (unsafeCoerce)

--------------------------
-- Misc VecT Operations --
--------------------------

-- TODO: These could be implemented?

-- data Range n l m = Range (IFin ('S n) l) (IFin ('S n) (l + m))
--   deriving (Show, Eq)

-- instance (Known (IFin ('S n)) l, Known (IFin ('S n)) (l + m))
--   => Known (Range n l) m where
--   type KnownC (Range n l) m
--     = (Known (IFin ('S n)) l, Known (IFin ('S n)) (l + m))
--   known = Range known known

-- updateRange :: Range n l m -> (Fin m -> f a -> f a) -> VecT n f a -> VecT n f a
-- updateRange = \case
--   Range  IFZ     IFZ    -> \_ -> id
--   Range (IFS l) (IFS m) -> \f -> onTail (updateRange (Range l m) f) \\ m
--   Range  IFZ    (IFS m) -> \f -> onTail (updateRange (Range IFZ m) $ f . FS)
--                                . onHead (f FZ) \\ m

-- setRange :: Range n l m -> VecT m f a -> VecT n f a -> VecT n f a
-- setRange r nv = updateRange r (\i _ -> index i nv)

-- updateSubmatrix
--   :: (ns ~ Fsts3 nlms, ms ~ Thds3 nlms)
--   => HList (Uncur3 Range) nlms -> (HList Fin ms -> a -> a) -> M ns a -> M ns a
-- updateSubmatrix = \case
--   Ø              -> \f -> (f Ø <$>)
--   Uncur3 r :< rs -> \f -> onMatrix . updateRange r $ \i ->
--     asM . updateSubmatrix rs $ f . (i :<)

-- setSubmatrix
--   :: (ns ~ Fsts3 nlms, ms ~ Thds3 nlms)
--   => HList (Uncur3 Range) nlms -> M ms a -> M ns a -> M ns a
-- setSubmatrix rs sm = updateSubmatrix rs $ \is _ -> indexMatrix is sm

-----------
-- Peano --
-----------

$(singletons [d|

  data Peano = Z | S Peano deriving (Eq, Ord, Show)

  addPeano :: Peano -> Peano -> Peano
  addPeano Z a = a
  addPeano (S a) b = S (addPeano a b)

  subtractPeano :: Peano -> Peano -> Peano
  subtractPeano Z _ = Z
  subtractPeano a Z = a
  subtractPeano (S a) (S b) = subtractPeano a b

  multPeano :: Peano -> Peano -> Peano
  multPeano Z _ = Z
  multPeano (S a) b = addPeano (multPeano a b) b

  n0 :: Peano
  n0 = Z

  n1 :: Peano
  n1 = S n0

  n2 :: Peano
  n2 = S n1

  n3 :: Peano
  n3 = S n2

  n4 :: Peano
  n4 = S n3

  n5 :: Peano
  n5 = S n4

  n6 :: Peano
  n6 = S n5

  n7 :: Peano
  n7 = S n6

  n8 :: Peano
  n8 = S n7

  n9 :: Peano
  n9 = S n8

  n10 :: Peano
  n10 = S n9

  n24 :: Peano
  n24 = multPeano n4 n6

  instance Num Peano where
    (+) = addPeano

    (-) = subtractPeano

    (*) = multPeano

    abs = id

    signum Z = Z
    signum (S _) = S Z

    fromInteger n =
      if n < 0
        then error "Num Peano fromInteger: n is negative"
        else
          if n == 0 then Z else S (fromInteger (n - 1))
  |])

-- | This is a proof that if we know @'S' n@ is less than @'S' m@, then we
-- know @n@ is also less than @m@.
--
-- >>> ltSuccProof (sing :: Sing N4) (sing :: Sing N5)
-- Refl
ltSuccProof ::
     forall (n :: Peano) (m :: Peano) proxy. ('S n < 'S m) ~ 'True
  => proxy n
  -> proxy m
  -> (n < m) :~: 'True
ltSuccProof :: proxy n -> proxy m -> (n < m) :~: 'True
ltSuccProof _ _ = (Int :~: Int)
-> Case_6989586621679804986 n m (Compare_6989586621679501810 n m)
   :~: 'True
forall a b. a -> b
unsafeCoerce (Int :~: Int
forall k (a :: k). a :~: a
Refl :: Int :~: Int)

---------
-- Fin --
---------

data Fin :: Peano -> Type where
  FZ :: forall (n :: Peano). Fin ('S n)
  FS :: forall (n :: Peano). !(Fin n) -> Fin ('S n)

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

toIntFin :: Fin n -> Int
toIntFin :: Fin n -> Int
toIntFin FZ = 0
toIntFin (FS x :: Fin n
x) = Int -> Int
forall a. Enum a => a -> a
succ (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$ Fin n -> Int
forall (n :: Peano). Fin n -> Int
toIntFin Fin n
x

-- | Similar to 'ifin' but for 'Fin'.
--
-- >>> fin (sing :: Sing N5) (sing :: Sing N1) :: Fin N5
-- FS FZ
fin ::
     forall total n. (n < total) ~ 'True
  => Sing total
  -> Sing n
  -> Fin total
fin :: Sing total -> Sing n -> Fin total
fin total :: Sing total
total n :: Sing n
n = IFin total n -> Fin total
forall (n :: Peano) (m :: Peano). IFin n m -> Fin n
toFinIFin (IFin total n -> Fin total) -> IFin total n -> Fin total
forall a b. (a -> b) -> a -> b
$ Sing total -> Sing n -> IFin total n
forall (total :: Peano) (n :: Peano).
((n < total) ~ 'True) =>
Sing total -> Sing n -> IFin total n
ifin Sing total
total Sing n
n

-- | Similar to 'ifin_' but for 'Fin'.
--
-- >>> fin_ @N4 (sing :: Sing N2) :: Fin N4
-- FS (FS FZ)
fin_ ::
     forall total n. (SingI total, (n < total) ~ 'True)
  => Sing n
  -> Fin total
fin_ :: Sing n -> Fin total
fin_ n :: Sing n
n = IFin total n -> Fin total
forall (n :: Peano) (m :: Peano). IFin n m -> Fin n
toFinIFin (IFin total n -> Fin total) -> IFin total n -> Fin total
forall a b. (a -> b) -> a -> b
$ Sing n -> IFin total n
forall (total :: Peano) (n :: Peano).
(SingI total, (n < total) ~ 'True) =>
Sing n -> IFin total n
ifin_ Sing n
n

data SFin :: forall n. Fin n -> Type where
  SFZ :: SFin 'FZ
  SFS :: SFin n -> SFin ('FS n)

type instance Sing @(Fin n) = SFin

instance SingI 'FZ where
  sing :: Sing 'FZ
sing = Sing 'FZ
forall (n :: Peano). SFin 'FZ
SFZ

instance SingI n => SingI ('FS n) where
  sing :: Sing ('FS n)
sing = SFin n -> SFin ('FS n)
forall (n :: Peano) (n :: Fin n). SFin n -> SFin ('FS n)
SFS SFin n
forall k (a :: k). SingI a => Sing a
sing

instance SingKind (Fin n) where
  type Demote (Fin n) = Fin n
  fromSing :: forall (a :: Fin n). Sing a -> Fin n
  fromSing :: Sing a -> Fin n
fromSing SFZ = Fin n
forall (n :: Peano). Fin ('S n)
FZ
  fromSing (SFS fin') = Fin n -> Fin ('S n)
forall (n :: Peano). Fin n -> Fin ('S n)
FS (Sing n -> Demote (Fin n)
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing n
SFin n
fin')

  toSing :: Fin n -> SomeSing (Fin n)
  toSing :: Fin n -> SomeSing (Fin n)
toSing FZ = Sing 'FZ -> SomeSing (Fin n)
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'FZ
forall (n :: Peano). SFin 'FZ
SFZ
  toSing (FS fin' :: Fin n
fin') =
    case Demote (Fin n) -> SomeSing (Fin n)
forall k. SingKind k => Demote k -> SomeSing k
toSing Demote (Fin n)
Fin n
fin' of
      SomeSing n :: Sing a
n -> Sing ('FS a) -> SomeSing (Fin n)
forall k (a :: k). Sing a -> SomeSing k
SomeSing (SFin a -> SFin ('FS a)
forall (n :: Peano) (n :: Fin n). SFin n -> SFin ('FS n)
SFS Sing a
SFin a
n)

instance Show (SFin 'FZ) where
  show :: SFin 'FZ -> String
show SFZ = "SFZ"

instance Show (SFin n) => Show (SFin ('FS n)) where
  showsPrec :: Int -> SFin ('FS n) -> ShowS
showsPrec d :: Int
d (SFS n :: SFin n
n) =
    Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    String -> ShowS
showString "SFS " ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> SFin n -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec 11 SFin n
n

----------
-- IFin --
----------

data IFin :: Peano -> Peano -> Type where
  IFZ :: forall (n :: Peano). IFin ('S n) 'Z
  IFS :: forall (n :: Peano) (m :: Peano). !(IFin n m) -> IFin ('S n) ('S m)

deriving instance Eq   (IFin x y)
deriving instance Ord  (IFin x y)
deriving instance Show (IFin x y)

toFinIFin :: IFin n m -> Fin n
toFinIFin :: IFin n m -> Fin n
toFinIFin IFZ = Fin n
forall (n :: Peano). Fin ('S n)
FZ
toFinIFin (IFS n :: IFin n m
n) = Fin n -> Fin ('S n)
forall (n :: Peano). Fin n -> Fin ('S n)
FS (IFin n m -> Fin n
forall (n :: Peano) (m :: Peano). IFin n m -> Fin n
toFinIFin IFin n m
n)

toIntIFin :: IFin n m -> Int
toIntIFin :: IFin n m -> Int
toIntIFin = Fin n -> Int
forall (n :: Peano). Fin n -> Int
toIntFin (Fin n -> Int) -> (IFin n m -> Fin n) -> IFin n m -> Int
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IFin n m -> Fin n
forall (n :: Peano) (m :: Peano). IFin n m -> Fin n
toFinIFin

-- | Create an 'IFin'.
--
-- >>> ifin (sing :: Sing N5) (sing :: Sing N2) :: IFin N5 N2
-- IFS (IFS IFZ)
ifin ::
     forall total n. ((n < total) ~ 'True)
  => Sing total
  -> Sing n
  -> IFin total n
ifin :: Sing total -> Sing n -> IFin total n
ifin (SS _) SZ = IFin total n
forall (n :: Peano). IFin ('S n) 'Z
IFZ
ifin (SS total') (SS n') =
  IFin n n -> IFin total n
forall (x :: Peano) (m :: Peano). IFin x m -> IFin ('S x) ('S m)
IFS (IFin n n -> IFin total n) -> IFin n n -> IFin total n
forall a b. (a -> b) -> a -> b
$
    case SPeano n -> SPeano n -> (n < n) :~: 'True
forall (n :: Peano) (m :: Peano) (proxy :: Peano -> *).
(('S n < 'S m) ~ 'True) =>
proxy n -> proxy m -> (n < m) :~: 'True
ltSuccProof Sing n
SPeano n
n' Sing n
SPeano n
total' of
      Refl -> Sing n -> Sing n -> IFin n n
forall (total :: Peano) (n :: Peano).
((n < total) ~ 'True) =>
Sing total -> Sing n -> IFin total n
ifin Sing n
total' Sing n
n'
ifin _ _ = String -> IFin total n
forall a. HasCallStack => String -> a
error "ifin: pattern impossible but GHC doesn't realize it"

-- | Create an 'IFin', but take the total implicitly.
--
-- >>> ifin_ @N5 (sing :: Sing N3) :: IFin N5 N3
-- IFS (IFS (IFS IFZ))
ifin_ ::
     forall total n. (SingI total, (n < total) ~ 'True)
  => Sing n
  -> IFin total n
ifin_ :: Sing n -> IFin total n
ifin_ = Sing total -> Sing n -> IFin total n
forall (total :: Peano) (n :: Peano).
((n < total) ~ 'True) =>
Sing total -> Sing n -> IFin total n
ifin Sing total
forall k (a :: k). SingI a => Sing a
sing

data SIFin :: forall n m. IFin n m -> Type where
  SIFZ :: SIFin 'IFZ
  SIFS :: SIFin x -> SIFin ('IFS x)

type instance Sing @(IFin n m) = SIFin

instance SingI 'IFZ where
  sing :: Sing 'IFZ
  sing :: Sing 'IFZ
sing = Sing 'IFZ
forall (n :: Peano). SIFin 'IFZ
SIFZ

instance SingI n => SingI ('IFS n) where
  sing :: Sing ('IFS n)
sing = SIFin n -> SIFin ('IFS n)
forall (n :: Peano) (m :: Peano) (x :: IFin n m).
SIFin x -> SIFin ('IFS x)
SIFS SIFin n
forall k (a :: k). SingI a => Sing a
sing

instance SingKind (IFin n m) where
  type Demote (IFin n m) = IFin n m
  fromSing :: forall (a :: IFin n m). Sing a -> IFin n m
  fromSing :: Sing a -> IFin n m
fromSing SIFZ = IFin n m
forall (n :: Peano). IFin ('S n) 'Z
IFZ
  fromSing (SIFS fin') = IFin n m -> IFin ('S n) ('S m)
forall (x :: Peano) (m :: Peano). IFin x m -> IFin ('S x) ('S m)
IFS (Sing x -> Demote (IFin n m)
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
SIFin x
fin')

  toSing :: IFin n m -> SomeSing (IFin n m)
  toSing :: IFin n m -> SomeSing (IFin n m)
toSing IFZ = Sing 'IFZ -> SomeSing (IFin n m)
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'IFZ
forall (n :: Peano). SIFin 'IFZ
SIFZ
  toSing (IFS fin' :: IFin n m
fin') =
    case Demote (IFin n m) -> SomeSing (IFin n m)
forall k. SingKind k => Demote k -> SomeSing k
toSing Demote (IFin n m)
IFin n m
fin' of
      SomeSing n :: Sing a
n -> Sing ('IFS a) -> SomeSing (IFin n m)
forall k (a :: k). Sing a -> SomeSing k
SomeSing (SIFin a -> SIFin ('IFS a)
forall (n :: Peano) (m :: Peano) (x :: IFin n m).
SIFin x -> SIFin ('IFS x)
SIFS Sing a
SIFin a
n)

instance Show (SIFin 'IFZ) where
  show :: SIFin 'IFZ -> String
show SIFZ = "SIFZ"

instance Show (SIFin n) => Show (SIFin ('IFS n)) where
  showsPrec :: Int -> SIFin ('IFS n) -> ShowS
showsPrec d :: Int
d (SIFS n :: SIFin x
n) =
    Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    String -> ShowS
showString "SIFS " ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> SIFin x -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec 11 SIFin x
n

-----------
-- HList --
-----------

data HList :: (k -> Type) -> [k] -> Type where
  EmptyHList :: HList f '[]
  (:<) :: forall (f :: k -> Type) (a :: k) (as :: [k]). f a -> HList f as -> HList f (a ': as)

infixr 6 :<

-- | Data constructor for ':<'.
pattern ConsHList :: (f a :: Type) -> HList f as -> HList f (a ': as)
pattern $bConsHList :: f a1 -> HList f as -> HList f (a1 : as)
$mConsHList :: forall r a (f :: a -> *) (a1 :: a) (as :: [a]).
HList f (a1 : as) -> (f a1 -> HList f as -> r) -> (Void# -> r) -> r
ConsHList fa hlist = fa :< hlist

---------
-- Vec --
---------

data Vec (n :: Peano) :: Type -> Type where
  EmptyVec :: Vec 'Z a
  (:*) :: !a -> !(Vec n a) -> Vec ('S n) a
  deriving anyclass Eq (Element (Vec n a)) => Element (Vec n a) -> Vec n a -> Bool
Vec n a -> Bool
Vec n a -> Int
Vec n a -> Int64
Vec n a -> [Element (Vec n a)]
Vec n a -> Element (Vec n a)
(Element (Vec n a) -> Bool) -> Vec n a -> Bool
(Element (Vec n a) -> Element (Vec n a) -> Ordering)
-> Vec n a -> Element (Vec n a)
(Element (Vec n a) -> Element (Vec n a) -> Element (Vec n a))
-> Vec n a -> Element (Vec n a)
(forall m. Monoid m => (Element (Vec n a) -> m) -> Vec n a -> m)
-> (forall b. (Element (Vec n a) -> b -> b) -> b -> Vec n a -> b)
-> (forall a. (a -> Element (Vec n a) -> a) -> a -> Vec n a -> a)
-> (Vec n a -> [Element (Vec n a)])
-> ((Element (Vec n a) -> Bool) -> Vec n a -> Bool)
-> ((Element (Vec n a) -> Bool) -> Vec n a -> Bool)
-> (Vec n a -> Bool)
-> (Vec n a -> Int)
-> (Vec n a -> Int64)
-> (forall i. Integral i => Vec n a -> i -> Ordering)
-> (forall (f :: * -> *) b.
    Applicative f =>
    (Element (Vec n a) -> f b) -> Vec n a -> f ())
-> (forall (f :: * -> *) b.
    Applicative f =>
    Vec n a -> (Element (Vec n a) -> f b) -> f ())
-> (forall (m :: * -> *).
    Applicative m =>
    (Element (Vec n a) -> m ()) -> Vec n a -> m ())
-> (forall (m :: * -> *).
    Applicative m =>
    Vec n a -> (Element (Vec n a) -> m ()) -> m ())
-> (forall (m :: * -> *) a.
    Monad m =>
    (a -> Element (Vec n a) -> m a) -> a -> Vec n a -> m a)
-> (forall m.
    Semigroup m =>
    (Element (Vec n a) -> m) -> Vec n a -> m)
-> ((Element (Vec n a) -> Element (Vec n a) -> Element (Vec n a))
    -> Vec n a -> Element (Vec n a))
-> ((Element (Vec n a) -> Element (Vec n a) -> Element (Vec n a))
    -> Vec n a -> Element (Vec n a))
-> (Vec n a -> Element (Vec n a))
-> (Vec n a -> Element (Vec n a))
-> (Vec n a -> Element (Vec n a))
-> (Vec n a -> Element (Vec n a))
-> ((Element (Vec n a) -> Element (Vec n a) -> Ordering)
    -> Vec n a -> Element (Vec n a))
-> ((Element (Vec n a) -> Element (Vec n a) -> Ordering)
    -> Vec n a -> Element (Vec n a))
-> (Eq (Element (Vec n a)) => Element (Vec n a) -> Vec n a -> Bool)
-> (Eq (Element (Vec n a)) => Element (Vec n a) -> Vec n a -> Bool)
-> MonoFoldable (Vec n a)
forall i. Integral i => Vec n a -> i -> Ordering
forall m. Semigroup m => (Element (Vec n a) -> m) -> Vec n a -> m
forall m. Monoid m => (Element (Vec n a) -> m) -> Vec n a -> m
forall a. (a -> Element (Vec n a) -> a) -> a -> Vec n a -> a
forall b. (Element (Vec n a) -> b -> b) -> b -> Vec n a -> b
forall mono.
(forall m. Monoid m => (Element mono -> m) -> mono -> m)
-> (forall b. (Element mono -> b -> b) -> b -> mono -> b)
-> (forall a. (a -> Element mono -> a) -> a -> mono -> a)
-> (mono -> [Element mono])
-> ((Element mono -> Bool) -> mono -> Bool)
-> ((Element mono -> Bool) -> mono -> Bool)
-> (mono -> Bool)
-> (mono -> Int)
-> (mono -> Int64)
-> (forall i. Integral i => mono -> i -> Ordering)
-> (forall (f :: * -> *) b.
    Applicative f =>
    (Element mono -> f b) -> mono -> f ())
-> (forall (f :: * -> *) b.
    Applicative f =>
    mono -> (Element mono -> f b) -> f ())
-> (forall (m :: * -> *).
    Applicative m =>
    (Element mono -> m ()) -> mono -> m ())
-> (forall (m :: * -> *).
    Applicative m =>
    mono -> (Element mono -> m ()) -> m ())
-> (forall (m :: * -> *) a.
    Monad m =>
    (a -> Element mono -> m a) -> a -> mono -> m a)
-> (forall m. Semigroup m => (Element mono -> m) -> mono -> m)
-> ((Element mono -> Element mono -> Element mono)
    -> mono -> Element mono)
-> ((Element mono -> Element mono -> Element mono)
    -> mono -> Element mono)
-> (mono -> Element mono)
-> (mono -> Element mono)
-> (mono -> Element mono)
-> (mono -> Element mono)
-> ((Element mono -> Element mono -> Ordering)
    -> mono -> Element mono)
-> ((Element mono -> Element mono -> Ordering)
    -> mono -> Element mono)
-> (Eq (Element mono) => Element mono -> mono -> Bool)
-> (Eq (Element mono) => Element mono -> mono -> Bool)
-> MonoFoldable mono
forall (n :: Peano) a.
Eq (Element (Vec n a)) =>
Element (Vec n a) -> Vec n a -> Bool
forall (n :: Peano) a. Vec n a -> Bool
forall (n :: Peano) a. Vec n a -> Int
forall (n :: Peano) a. Vec n a -> Int64
forall (n :: Peano) a. Vec n a -> [Element (Vec n a)]
forall (n :: Peano) a. Vec n a -> Element (Vec n a)
forall (n :: Peano) a.
(Element (Vec n a) -> Bool) -> Vec n a -> Bool
forall (n :: Peano) a.
(Element (Vec n a) -> Element (Vec n a) -> Ordering)
-> Vec n a -> Element (Vec n a)
forall (n :: Peano) a.
(Element (Vec n a) -> Element (Vec n a) -> Element (Vec n a))
-> Vec n a -> Element (Vec n a)
forall (n :: Peano) a i. Integral i => Vec n a -> i -> Ordering
forall (n :: Peano) a m.
Semigroup m =>
(Element (Vec n a) -> m) -> Vec n a -> m
forall (n :: Peano) a m.
Monoid m =>
(Element (Vec n a) -> m) -> Vec n a -> m
forall (n :: Peano) a a.
(a -> Element (Vec n a) -> a) -> a -> Vec n a -> a
forall (n :: Peano) a b.
(Element (Vec n a) -> b -> b) -> b -> Vec n a -> b
forall (n :: Peano) a (m :: * -> *).
Applicative m =>
Vec n a -> (Element (Vec n a) -> m ()) -> m ()
forall (n :: Peano) a (m :: * -> *).
Applicative m =>
(Element (Vec n a) -> m ()) -> Vec n a -> m ()
forall (n :: Peano) a (m :: * -> *) a.
Monad m =>
(a -> Element (Vec n a) -> m a) -> a -> Vec n a -> m a
forall (n :: Peano) a (f :: * -> *) b.
Applicative f =>
Vec n a -> (Element (Vec n a) -> f b) -> f ()
forall (n :: Peano) a (f :: * -> *) b.
Applicative f =>
(Element (Vec n a) -> f b) -> Vec n a -> f ()
forall (m :: * -> *).
Applicative m =>
Vec n a -> (Element (Vec n a) -> m ()) -> m ()
forall (m :: * -> *).
Applicative m =>
(Element (Vec n a) -> m ()) -> Vec n a -> m ()
forall (m :: * -> *) a.
Monad m =>
(a -> Element (Vec n a) -> m a) -> a -> Vec n a -> m a
forall (f :: * -> *) b.
Applicative f =>
Vec n a -> (Element (Vec n a) -> f b) -> f ()
forall (f :: * -> *) b.
Applicative f =>
(Element (Vec n a) -> f b) -> Vec n a -> f ()
onotElem :: Element (Vec n a) -> Vec n a -> Bool
$conotElem :: forall (n :: Peano) a.
Eq (Element (Vec n a)) =>
Element (Vec n a) -> Vec n a -> Bool
oelem :: Element (Vec n a) -> Vec n a -> Bool
$coelem :: forall (n :: Peano) a.
Eq (Element (Vec n a)) =>
Element (Vec n a) -> Vec n a -> Bool
minimumByEx :: (Element (Vec n a) -> Element (Vec n a) -> Ordering)
-> Vec n a -> Element (Vec n a)
$cminimumByEx :: forall (n :: Peano) a.
(Element (Vec n a) -> Element (Vec n a) -> Ordering)
-> Vec n a -> Element (Vec n a)
maximumByEx :: (Element (Vec n a) -> Element (Vec n a) -> Ordering)
-> Vec n a -> Element (Vec n a)
$cmaximumByEx :: forall (n :: Peano) a.
(Element (Vec n a) -> Element (Vec n a) -> Ordering)
-> Vec n a -> Element (Vec n a)
unsafeLast :: Vec n a -> Element (Vec n a)
$cunsafeLast :: forall (n :: Peano) a. Vec n a -> Element (Vec n a)
unsafeHead :: Vec n a -> Element (Vec n a)
$cunsafeHead :: forall (n :: Peano) a. Vec n a -> Element (Vec n a)
lastEx :: Vec n a -> Element (Vec n a)
$clastEx :: forall (n :: Peano) a. Vec n a -> Element (Vec n a)
headEx :: Vec n a -> Element (Vec n a)
$cheadEx :: forall (n :: Peano) a. Vec n a -> Element (Vec n a)
ofoldl1Ex' :: (Element (Vec n a) -> Element (Vec n a) -> Element (Vec n a))
-> Vec n a -> Element (Vec n a)
$cofoldl1Ex' :: forall (n :: Peano) a.
(Element (Vec n a) -> Element (Vec n a) -> Element (Vec n a))
-> Vec n a -> Element (Vec n a)
ofoldr1Ex :: (Element (Vec n a) -> Element (Vec n a) -> Element (Vec n a))
-> Vec n a -> Element (Vec n a)
$cofoldr1Ex :: forall (n :: Peano) a.
(Element (Vec n a) -> Element (Vec n a) -> Element (Vec n a))
-> Vec n a -> Element (Vec n a)
ofoldMap1Ex :: (Element (Vec n a) -> m) -> Vec n a -> m
$cofoldMap1Ex :: forall (n :: Peano) a m.
Semigroup m =>
(Element (Vec n a) -> m) -> Vec n a -> m
ofoldlM :: (a -> Element (Vec n a) -> m a) -> a -> Vec n a -> m a
$cofoldlM :: forall (n :: Peano) a (m :: * -> *) a.
Monad m =>
(a -> Element (Vec n a) -> m a) -> a -> Vec n a -> m a
oforM_ :: Vec n a -> (Element (Vec n a) -> m ()) -> m ()
$coforM_ :: forall (n :: Peano) a (m :: * -> *).
Applicative m =>
Vec n a -> (Element (Vec n a) -> m ()) -> m ()
omapM_ :: (Element (Vec n a) -> m ()) -> Vec n a -> m ()
$comapM_ :: forall (n :: Peano) a (m :: * -> *).
Applicative m =>
(Element (Vec n a) -> m ()) -> Vec n a -> m ()
ofor_ :: Vec n a -> (Element (Vec n a) -> f b) -> f ()
$cofor_ :: forall (n :: Peano) a (f :: * -> *) b.
Applicative f =>
Vec n a -> (Element (Vec n a) -> f b) -> f ()
otraverse_ :: (Element (Vec n a) -> f b) -> Vec n a -> f ()
$cotraverse_ :: forall (n :: Peano) a (f :: * -> *) b.
Applicative f =>
(Element (Vec n a) -> f b) -> Vec n a -> f ()
ocompareLength :: Vec n a -> i -> Ordering
$cocompareLength :: forall (n :: Peano) a i. Integral i => Vec n a -> i -> Ordering
olength64 :: Vec n a -> Int64
$colength64 :: forall (n :: Peano) a. Vec n a -> Int64
olength :: Vec n a -> Int
$colength :: forall (n :: Peano) a. Vec n a -> Int
onull :: Vec n a -> Bool
$conull :: forall (n :: Peano) a. Vec n a -> Bool
oany :: (Element (Vec n a) -> Bool) -> Vec n a -> Bool
$coany :: forall (n :: Peano) a.
(Element (Vec n a) -> Bool) -> Vec n a -> Bool
oall :: (Element (Vec n a) -> Bool) -> Vec n a -> Bool
$coall :: forall (n :: Peano) a.
(Element (Vec n a) -> Bool) -> Vec n a -> Bool
otoList :: Vec n a -> [Element (Vec n a)]
$cotoList :: forall (n :: Peano) a. Vec n a -> [Element (Vec n a)]
ofoldl' :: (a -> Element (Vec n a) -> a) -> a -> Vec n a -> a
$cofoldl' :: forall (n :: Peano) a a.
(a -> Element (Vec n a) -> a) -> a -> Vec n a -> a
ofoldr :: (Element (Vec n a) -> b -> b) -> b -> Vec n a -> b
$cofoldr :: forall (n :: Peano) a b.
(Element (Vec n a) -> b -> b) -> b -> Vec n a -> b
ofoldMap :: (Element (Vec n a) -> m) -> Vec n a -> m
$cofoldMap :: forall (n :: Peano) a m.
Monoid m =>
(Element (Vec n a) -> m) -> Vec n a -> m
MonoFoldable

infixr 6 :*

-- | Data constructor for ':*'.
pattern ConsVec :: (a :: Type) -> Vec n a -> Vec ('S n) a
pattern $bConsVec :: a -> Vec n a -> Vec ('S n) a
$mConsVec :: forall r a (n :: Peano).
Vec ('S n) a -> (a -> Vec n a -> r) -> (Void# -> r) -> r
ConsVec a vec = a :* vec

deriving instance Eq a => Eq (Vec n a)
deriving instance Ord a => Ord (Vec n a)
deriving instance Show a => Show (Vec n a)

deriving instance Functor (Vec n)
deriving instance Foldable (Vec n)

instance MonoFunctor (Vec n a)

instance SingI n => MonoPointed (Vec n a)

instance SingI n => Applicative (Vec n) where
  pure :: a -> Vec n a
pure a :: a
a = a -> Vec n a
forall (n :: Peano) a. SingI n => a -> Vec n a
replaceVec_ a
a

  <*> :: Vec n (a -> b) -> Vec n a -> Vec n b
(<*>) = ((a -> b) -> a -> b) -> Vec n (a -> b) -> Vec n a -> Vec n b
forall a b c (n :: Peano).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
apVec (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
($)

instance SingI n => Distributive (Vec n) where
  distribute :: Functor f => f (Vec n a) -> Vec n (f a)
  distribute :: f (Vec n a) -> Vec n (f a)
distribute = f (Vec n a) -> Vec n (f a)
forall (f :: * -> *) (w :: * -> *) a.
(Representable f, Functor w) =>
w (f a) -> f (w a)
distributeRep

instance SingI n => Representable (Vec n) where
  type Rep (Vec n) = Fin n

  tabulate :: (Fin n -> a) -> Vec n a
  tabulate :: (Fin n -> a) -> Vec n a
tabulate = (Fin n -> a) -> Vec n a
forall (n :: Peano) a. SingI n => (Fin n -> a) -> Vec n a
genVec_

  index :: Vec n a -> Fin n -> a
  index :: Vec n a -> Fin n -> a
index = (Fin n -> Vec n a -> a) -> Vec n a -> Fin n -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Fin n -> Vec n a -> a
forall (n :: Peano) a. Fin n -> Vec n a -> a
indexVec

instance SingI n => Monad (Vec n) where
  (>>=) :: Vec n a -> (a -> Vec n b) -> Vec n b
  >>= :: Vec n a -> (a -> Vec n b) -> Vec n b
(>>=) = Vec n a -> (a -> Vec n b) -> Vec n b
forall (f :: * -> *) a b.
Representable f =>
f a -> (a -> f b) -> f b
bindRep

type instance Element (Vec n a) = a

genVec_ :: SingI n => (Fin n -> a) -> Vec n a
genVec_ :: (Fin n -> a) -> Vec n a
genVec_ = SPeano n -> (Fin n -> a) -> Vec n a
forall (n :: Peano) a. SPeano n -> (Fin n -> a) -> Vec n a
genVec SPeano n
forall k (a :: k). SingI a => Sing a
sing

genVec :: SPeano n -> (Fin n -> a) -> Vec n a
genVec :: SPeano n -> (Fin n -> a) -> Vec n a
genVec SZ _ = Vec n a
forall a. Vec 'Z a
EmptyVec
genVec (SS n :: Sing n
n) f :: Fin n -> a
f = Fin n -> a
f Fin n
forall (n :: Peano). Fin ('S n)
FZ a -> Vec n a -> Vec ('S n) a
forall a (n :: Peano). a -> Vec n a -> Vec ('S n) a
:* SPeano n -> (Fin n -> a) -> Vec n a
forall (n :: Peano) a. SPeano n -> (Fin n -> a) -> Vec n a
genVec Sing n
SPeano n
n (Fin n -> a
Fin ('S n) -> a
f (Fin ('S n) -> a) -> (Fin n -> Fin ('S n)) -> Fin n -> a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Fin n -> Fin ('S n)
forall (n :: Peano). Fin n -> Fin ('S n)
FS)

indexVec :: Fin n -> Vec n a -> a
indexVec :: Fin n -> Vec n a -> a
indexVec FZ (a :: a
a :* _) = a
a
indexVec (FS n :: Fin n
n) (_ :* vec :: Vec n a
vec) = Fin n -> Vec n a -> a
forall (n :: Peano) a. Fin n -> Vec n a -> a
indexVec Fin n
n Vec n a
Vec n a
vec

singletonVec :: a -> Vec N1 a
singletonVec :: a -> Vec N1Sym0 a
singletonVec a :: a
a = a -> Vec 'Z a -> Vec ('S 'Z) a
forall a (n :: Peano). a -> Vec n a -> Vec ('S n) a
ConsVec a
a Vec 'Z a
forall a. Vec 'Z a
EmptyVec

replaceVec :: Sing n -> a -> Vec n a
replaceVec :: Sing n -> a -> Vec n a
replaceVec SZ _ = Vec n a
forall a. Vec 'Z a
EmptyVec
replaceVec (SS n) a :: a
a = a
a a -> Vec n a -> Vec ('S n) a
forall a (n :: Peano). a -> Vec n a -> Vec ('S n) a
:* Sing n -> a -> Vec n a
forall (n :: Peano) a. Sing n -> a -> Vec n a
replaceVec Sing n
n a
a

imapVec :: forall n a b. (Fin n -> a -> b) -> Vec n a -> Vec n b
imapVec :: (Fin n -> a -> b) -> Vec n a -> Vec n b
imapVec _ EmptyVec = Vec n b
forall a. Vec 'Z a
EmptyVec
imapVec f :: Fin n -> a -> b
f (a :: a
a :* as :: Vec n a
as) = Fin n -> a -> b
f Fin n
forall (n :: Peano). Fin ('S n)
FZ a
a b -> Vec n b -> Vec ('S n) b
forall a (n :: Peano). a -> Vec n a -> Vec ('S n) a
:* (Fin n -> a -> b) -> Vec n a -> Vec n b
forall (n :: Peano) a b. (Fin n -> a -> b) -> Vec n a -> Vec n b
imapVec (\fin' :: Fin n
fin' vec :: a
vec -> Fin n -> a -> b
f (Fin n -> Fin ('S n)
forall (n :: Peano). Fin n -> Fin ('S n)
FS Fin n
fin') a
vec) Vec n a
as

replaceVec_ :: SingI n => a -> Vec n a
replaceVec_ :: a -> Vec n a
replaceVec_ = Sing n -> a -> Vec n a
forall (n :: Peano) a. Sing n -> a -> Vec n a
replaceVec Sing n
forall k (a :: k). SingI a => Sing a
sing

apVec :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
apVec :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
apVec _ EmptyVec _ = Vec n c
forall a. Vec 'Z a
EmptyVec
apVec f :: a -> b -> c
f (a :: a
a :* as :: Vec n a
as) (b :: b
b :* bs :: Vec n b
bs) = a -> b -> c
f a
a b
b c -> Vec n c -> Vec ('S n) c
forall a (n :: Peano). a -> Vec n a -> Vec ('S n) a
:* (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
forall a b c (n :: Peano).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
apVec a -> b -> c
f Vec n a
as Vec n b
Vec n b
bs

onHeadVec :: (a -> a) -> Vec ('S n) a -> Vec ('S n) a
onHeadVec :: (a -> a) -> Vec ('S n) a -> Vec ('S n) a
onHeadVec f :: a -> a
f (a :: a
a :* as :: Vec n a
as) = a -> a
f a
a a -> Vec n a -> Vec ('S n) a
forall a (n :: Peano). a -> Vec n a -> Vec ('S n) a
:* Vec n a
as

dropVec :: Sing m -> Vec (m + n) a -> Vec n a
dropVec :: Sing m -> Vec (m + n) a -> Vec n a
dropVec SZ vec :: Vec (m + n) a
vec = Vec n a
Vec (m + n) a
vec
dropVec (SS n) (_ :* vec :: Vec n a
vec) = Sing n -> Vec (n + n) a -> Vec n a
forall (m :: Peano) (n :: Peano) a.
Sing m -> Vec (m + n) a -> Vec n a
dropVec Sing n
n Vec n a
Vec (n + n) a
vec

takeVec :: IFin n m -> Vec n a -> Vec m a
takeVec :: IFin n m -> Vec n a -> Vec m a
takeVec IFZ _ = Vec m a
forall a. Vec 'Z a
EmptyVec
takeVec (IFS n :: IFin n m
n) (a :: a
a :* vec :: Vec n a
vec) = a
a a -> Vec m a -> Vec ('S m) a
forall a (n :: Peano). a -> Vec n a -> Vec ('S n) a
:* IFin n m -> Vec n a -> Vec m a
forall (n :: Peano) (m :: Peano) a. IFin n m -> Vec n a -> Vec m a
takeVec IFin n m
n Vec n a
Vec n a
vec

updateAtVec :: Fin n -> (a -> a) -> Vec n a -> Vec n a
updateAtVec :: Fin n -> (a -> a) -> Vec n a -> Vec n a
updateAtVec FZ f :: a -> a
f (a :: a
a :* vec :: Vec n a
vec)  = a -> a
f a
a a -> Vec n a -> Vec ('S n) a
forall a (n :: Peano). a -> Vec n a -> Vec ('S n) a
:* Vec n a
vec
updateAtVec (FS n :: Fin n
n) f :: a -> a
f (a :: a
a :* vec :: Vec n a
vec)  = a
a a -> Vec n a -> Vec ('S n) a
forall a (n :: Peano). a -> Vec n a -> Vec ('S n) a
:* Fin n -> (a -> a) -> Vec n a -> Vec n a
forall (n :: Peano) a. Fin n -> (a -> a) -> Vec n a -> Vec n a
updateAtVec Fin n
n a -> a
f Vec n a
Vec n a
vec

setAtVec :: Fin n -> a -> Vec n a -> Vec n a
setAtVec :: Fin n -> a -> Vec n a -> Vec n a
setAtVec fin' :: Fin n
fin' a :: a
a = Fin n -> (a -> a) -> Vec n a -> Vec n a
forall (n :: Peano) a. Fin n -> (a -> a) -> Vec n a -> Vec n a
updateAtVec Fin n
fin' (a -> a -> a
forall a b. a -> b -> a
const a
a)

fromListVec :: Sing n -> [a] -> Maybe (Vec n a)
fromListVec :: Sing n -> [a] -> Maybe (Vec n a)
fromListVec SZ _ = Vec 'Z a -> Maybe (Vec 'Z a)
forall a. a -> Maybe a
Just Vec 'Z a
forall a. Vec 'Z a
EmptyVec
fromListVec (SS _) [] = Maybe (Vec n a)
forall a. Maybe a
Nothing
fromListVec (SS n) (a :: a
a:as :: [a]
as) = do
  Vec n a
tailVec <- Sing n -> [a] -> Maybe (Vec n a)
forall (n :: Peano) a. Sing n -> [a] -> Maybe (Vec n a)
fromListVec Sing n
n [a]
as
  Vec ('S n) a -> Maybe (Vec n a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Vec ('S n) a -> Maybe (Vec n a))
-> Vec ('S n) a -> Maybe (Vec n a)
forall a b. (a -> b) -> a -> b
$ a -> Vec n a -> Vec ('S n) a
forall a (n :: Peano). a -> Vec n a -> Vec ('S n) a
ConsVec a
a Vec n a
tailVec

fromListVec_ :: SingI n => [a] -> Maybe (Vec n a)
fromListVec_ :: [a] -> Maybe (Vec n a)
fromListVec_ = Sing n -> [a] -> Maybe (Vec n a)
forall (n :: Peano) a. Sing n -> [a] -> Maybe (Vec n a)
fromListVec Sing n
forall k (a :: k). SingI a => Sing a
sing

unsafeFromListVec :: Sing n -> [a] -> Vec n a
unsafeFromListVec :: Sing n -> [a] -> Vec n a
unsafeFromListVec n :: Sing n
n as :: [a]
as =
  case Sing n -> [a] -> Maybe (Vec n a)
forall (n :: Peano) a. Sing n -> [a] -> Maybe (Vec n a)
fromListVec Sing n
n [a]
as of
    Just vec :: Vec n a
vec -> Vec n a
vec
    Nothing ->
      String -> Vec n a
forall a. HasCallStack => String -> a
error (String -> Vec n a) -> String -> Vec n a
forall a b. (a -> b) -> a -> b
$
        "unsafeFromListVec: couldn't create a length " String -> ShowS
forall a. Semigroup a => a -> a -> a
<>
        SPeano n -> String
forall a. Show a => a -> String
show Sing n
SPeano n
n String -> ShowS
forall a. Semigroup a => a -> a -> a
<> " vector from the input list"

unsafeFromListVec_ :: SingI n => [a] -> Vec n a
unsafeFromListVec_ :: [a] -> Vec n a
unsafeFromListVec_ = Sing n -> [a] -> Vec n a
forall (n :: Peano) a. Sing n -> [a] -> Vec n a
unsafeFromListVec Sing n
forall k (a :: k). SingI a => Sing a
sing

------------
-- Matrix --
------------

type family MatrixTF (ns :: [Peano]) (a :: Type) :: Type where
  MatrixTF '[] a = a
  MatrixTF (n ': ns) a = Vec n (MatrixTF ns a)

newtype Matrix ns a = Matrix
  { Matrix ns a -> MatrixTF ns a
unMatrix :: MatrixTF ns a
  }
  deriving anyclass (Eq (Element (Matrix ns a)) =>
Element (Matrix ns a) -> Matrix ns a -> Bool
Matrix ns a -> Bool
Matrix ns a -> Int
Matrix ns a -> Int64
Matrix ns a -> [Element (Matrix ns a)]
Matrix ns a -> Element (Matrix ns a)
(Element (Matrix ns a) -> Bool) -> Matrix ns a -> Bool
(Element (Matrix ns a) -> Element (Matrix ns a) -> Ordering)
-> Matrix ns a -> Element (Matrix ns a)
(Element (Matrix ns a)
 -> Element (Matrix ns a) -> Element (Matrix ns a))
-> Matrix ns a -> Element (Matrix ns a)
(forall m.
 Monoid m =>
 (Element (Matrix ns a) -> m) -> Matrix ns a -> m)
-> (forall b.
    (Element (Matrix ns a) -> b -> b) -> b -> Matrix ns a -> b)
-> (forall a.
    (a -> Element (Matrix ns a) -> a) -> a -> Matrix ns a -> a)
-> (Matrix ns a -> [Element (Matrix ns a)])
-> ((Element (Matrix ns a) -> Bool) -> Matrix ns a -> Bool)
-> ((Element (Matrix ns a) -> Bool) -> Matrix ns a -> Bool)
-> (Matrix ns a -> Bool)
-> (Matrix ns a -> Int)
-> (Matrix ns a -> Int64)
-> (forall i. Integral i => Matrix ns a -> i -> Ordering)
-> (forall (f :: * -> *) b.
    Applicative f =>
    (Element (Matrix ns a) -> f b) -> Matrix ns a -> f ())
-> (forall (f :: * -> *) b.
    Applicative f =>
    Matrix ns a -> (Element (Matrix ns a) -> f b) -> f ())
-> (forall (m :: * -> *).
    Applicative m =>
    (Element (Matrix ns a) -> m ()) -> Matrix ns a -> m ())
-> (forall (m :: * -> *).
    Applicative m =>
    Matrix ns a -> (Element (Matrix ns a) -> m ()) -> m ())
-> (forall (m :: * -> *) a.
    Monad m =>
    (a -> Element (Matrix ns a) -> m a) -> a -> Matrix ns a -> m a)
-> (forall m.
    Semigroup m =>
    (Element (Matrix ns a) -> m) -> Matrix ns a -> m)
-> ((Element (Matrix ns a)
     -> Element (Matrix ns a) -> Element (Matrix ns a))
    -> Matrix ns a -> Element (Matrix ns a))
-> ((Element (Matrix ns a)
     -> Element (Matrix ns a) -> Element (Matrix ns a))
    -> Matrix ns a -> Element (Matrix ns a))
-> (Matrix ns a -> Element (Matrix ns a))
-> (Matrix ns a -> Element (Matrix ns a))
-> (Matrix ns a -> Element (Matrix ns a))
-> (Matrix ns a -> Element (Matrix ns a))
-> ((Element (Matrix ns a) -> Element (Matrix ns a) -> Ordering)
    -> Matrix ns a -> Element (Matrix ns a))
-> ((Element (Matrix ns a) -> Element (Matrix ns a) -> Ordering)
    -> Matrix ns a -> Element (Matrix ns a))
-> (Eq (Element (Matrix ns a)) =>
    Element (Matrix ns a) -> Matrix ns a -> Bool)
-> (Eq (Element (Matrix ns a)) =>
    Element (Matrix ns a) -> Matrix ns a -> Bool)
-> MonoFoldable (Matrix ns a)
forall (ns :: [Peano]) a.
(SingI ns, Eq (Element (Matrix ns a))) =>
Element (Matrix ns a) -> Matrix ns a -> Bool
forall (ns :: [Peano]) a. SingI ns => Matrix ns a -> Bool
forall (ns :: [Peano]) a. SingI ns => Matrix ns a -> Int
forall (ns :: [Peano]) a. SingI ns => Matrix ns a -> Int64
forall (ns :: [Peano]) a.
SingI ns =>
Matrix ns a -> [Element (Matrix ns a)]
forall (ns :: [Peano]) a.
SingI ns =>
Matrix ns a -> Element (Matrix ns a)
forall (ns :: [Peano]) a.
SingI ns =>
(Element (Matrix ns a) -> Bool) -> Matrix ns a -> Bool
forall (ns :: [Peano]) a.
SingI ns =>
(Element (Matrix ns a) -> Element (Matrix ns a) -> Ordering)
-> Matrix ns a -> Element (Matrix ns a)
forall (ns :: [Peano]) a.
SingI ns =>
(Element (Matrix ns a)
 -> Element (Matrix ns a) -> Element (Matrix ns a))
-> Matrix ns a -> Element (Matrix ns a)
forall (ns :: [Peano]) a i.
(SingI ns, Integral i) =>
Matrix ns a -> i -> Ordering
forall (ns :: [Peano]) a m.
(SingI ns, Semigroup m) =>
(Element (Matrix ns a) -> m) -> Matrix ns a -> m
forall (ns :: [Peano]) a m.
(SingI ns, Monoid m) =>
(Element (Matrix ns a) -> m) -> Matrix ns a -> m
forall (ns :: [Peano]) a a.
SingI ns =>
(a -> Element (Matrix ns a) -> a) -> a -> Matrix ns a -> a
forall (ns :: [Peano]) a b.
SingI ns =>
(Element (Matrix ns a) -> b -> b) -> b -> Matrix ns a -> b
forall (ns :: [Peano]) a (m :: * -> *).
(SingI ns, Applicative m) =>
Matrix ns a -> (Element (Matrix ns a) -> m ()) -> m ()
forall (ns :: [Peano]) a (m :: * -> *).
(SingI ns, Applicative m) =>
(Element (Matrix ns a) -> m ()) -> Matrix ns a -> m ()
forall (ns :: [Peano]) a (m :: * -> *) a.
(SingI ns, Monad m) =>
(a -> Element (Matrix ns a) -> m a) -> a -> Matrix ns a -> m a
forall (ns :: [Peano]) a (f :: * -> *) b.
(SingI ns, Applicative f) =>
Matrix ns a -> (Element (Matrix ns a) -> f b) -> f ()
forall (ns :: [Peano]) a (f :: * -> *) b.
(SingI ns, Applicative f) =>
(Element (Matrix ns a) -> f b) -> Matrix ns a -> f ()
forall i. Integral i => Matrix ns a -> i -> Ordering
forall m.
Semigroup m =>
(Element (Matrix ns a) -> m) -> Matrix ns a -> m
forall m.
Monoid m =>
(Element (Matrix ns a) -> m) -> Matrix ns a -> m
forall a.
(a -> Element (Matrix ns a) -> a) -> a -> Matrix ns a -> a
forall b.
(Element (Matrix ns a) -> b -> b) -> b -> Matrix ns a -> b
forall mono.
(forall m. Monoid m => (Element mono -> m) -> mono -> m)
-> (forall b. (Element mono -> b -> b) -> b -> mono -> b)
-> (forall a. (a -> Element mono -> a) -> a -> mono -> a)
-> (mono -> [Element mono])
-> ((Element mono -> Bool) -> mono -> Bool)
-> ((Element mono -> Bool) -> mono -> Bool)
-> (mono -> Bool)
-> (mono -> Int)
-> (mono -> Int64)
-> (forall i. Integral i => mono -> i -> Ordering)
-> (forall (f :: * -> *) b.
    Applicative f =>
    (Element mono -> f b) -> mono -> f ())
-> (forall (f :: * -> *) b.
    Applicative f =>
    mono -> (Element mono -> f b) -> f ())
-> (forall (m :: * -> *).
    Applicative m =>
    (Element mono -> m ()) -> mono -> m ())
-> (forall (m :: * -> *).
    Applicative m =>
    mono -> (Element mono -> m ()) -> m ())
-> (forall (m :: * -> *) a.
    Monad m =>
    (a -> Element mono -> m a) -> a -> mono -> m a)
-> (forall m. Semigroup m => (Element mono -> m) -> mono -> m)
-> ((Element mono -> Element mono -> Element mono)
    -> mono -> Element mono)
-> ((Element mono -> Element mono -> Element mono)
    -> mono -> Element mono)
-> (mono -> Element mono)
-> (mono -> Element mono)
-> (mono -> Element mono)
-> (mono -> Element mono)
-> ((Element mono -> Element mono -> Ordering)
    -> mono -> Element mono)
-> ((Element mono -> Element mono -> Ordering)
    -> mono -> Element mono)
-> (Eq (Element mono) => Element mono -> mono -> Bool)
-> (Eq (Element mono) => Element mono -> mono -> Bool)
-> MonoFoldable mono
forall (m :: * -> *).
Applicative m =>
Matrix ns a -> (Element (Matrix ns a) -> m ()) -> m ()
forall (m :: * -> *).
Applicative m =>
(Element (Matrix ns a) -> m ()) -> Matrix ns a -> m ()
forall (m :: * -> *) a.
Monad m =>
(a -> Element (Matrix ns a) -> m a) -> a -> Matrix ns a -> m a
forall (f :: * -> *) b.
Applicative f =>
Matrix ns a -> (Element (Matrix ns a) -> f b) -> f ()
forall (f :: * -> *) b.
Applicative f =>
(Element (Matrix ns a) -> f b) -> Matrix ns a -> f ()
onotElem :: Element (Matrix ns a) -> Matrix ns a -> Bool
$conotElem :: forall (ns :: [Peano]) a.
(SingI ns, Eq (Element (Matrix ns a))) =>
Element (Matrix ns a) -> Matrix ns a -> Bool
oelem :: Element (Matrix ns a) -> Matrix ns a -> Bool
$coelem :: forall (ns :: [Peano]) a.
(SingI ns, Eq (Element (Matrix ns a))) =>
Element (Matrix ns a) -> Matrix ns a -> Bool
minimumByEx :: (Element (Matrix ns a) -> Element (Matrix ns a) -> Ordering)
-> Matrix ns a -> Element (Matrix ns a)
$cminimumByEx :: forall (ns :: [Peano]) a.
SingI ns =>
(Element (Matrix ns a) -> Element (Matrix ns a) -> Ordering)
-> Matrix ns a -> Element (Matrix ns a)
maximumByEx :: (Element (Matrix ns a) -> Element (Matrix ns a) -> Ordering)
-> Matrix ns a -> Element (Matrix ns a)
$cmaximumByEx :: forall (ns :: [Peano]) a.
SingI ns =>
(Element (Matrix ns a) -> Element (Matrix ns a) -> Ordering)
-> Matrix ns a -> Element (Matrix ns a)
unsafeLast :: Matrix ns a -> Element (Matrix ns a)
$cunsafeLast :: forall (ns :: [Peano]) a.
SingI ns =>
Matrix ns a -> Element (Matrix ns a)
unsafeHead :: Matrix ns a -> Element (Matrix ns a)
$cunsafeHead :: forall (ns :: [Peano]) a.
SingI ns =>
Matrix ns a -> Element (Matrix ns a)
lastEx :: Matrix ns a -> Element (Matrix ns a)
$clastEx :: forall (ns :: [Peano]) a.
SingI ns =>
Matrix ns a -> Element (Matrix ns a)
headEx :: Matrix ns a -> Element (Matrix ns a)
$cheadEx :: forall (ns :: [Peano]) a.
SingI ns =>
Matrix ns a -> Element (Matrix ns a)
ofoldl1Ex' :: (Element (Matrix ns a)
 -> Element (Matrix ns a) -> Element (Matrix ns a))
-> Matrix ns a -> Element (Matrix ns a)
$cofoldl1Ex' :: forall (ns :: [Peano]) a.
SingI ns =>
(Element (Matrix ns a)
 -> Element (Matrix ns a) -> Element (Matrix ns a))
-> Matrix ns a -> Element (Matrix ns a)
ofoldr1Ex :: (Element (Matrix ns a)
 -> Element (Matrix ns a) -> Element (Matrix ns a))
-> Matrix ns a -> Element (Matrix ns a)
$cofoldr1Ex :: forall (ns :: [Peano]) a.
SingI ns =>
(Element (Matrix ns a)
 -> Element (Matrix ns a) -> Element (Matrix ns a))
-> Matrix ns a -> Element (Matrix ns a)
ofoldMap1Ex :: (Element (Matrix ns a) -> m) -> Matrix ns a -> m
$cofoldMap1Ex :: forall (ns :: [Peano]) a m.
(SingI ns, Semigroup m) =>
(Element (Matrix ns a) -> m) -> Matrix ns a -> m
ofoldlM :: (a -> Element (Matrix ns a) -> m a) -> a -> Matrix ns a -> m a
$cofoldlM :: forall (ns :: [Peano]) a (m :: * -> *) a.
(SingI ns, Monad m) =>
(a -> Element (Matrix ns a) -> m a) -> a -> Matrix ns a -> m a
oforM_ :: Matrix ns a -> (Element (Matrix ns a) -> m ()) -> m ()
$coforM_ :: forall (ns :: [Peano]) a (m :: * -> *).
(SingI ns, Applicative m) =>
Matrix ns a -> (Element (Matrix ns a) -> m ()) -> m ()
omapM_ :: (Element (Matrix ns a) -> m ()) -> Matrix ns a -> m ()
$comapM_ :: forall (ns :: [Peano]) a (m :: * -> *).
(SingI ns, Applicative m) =>
(Element (Matrix ns a) -> m ()) -> Matrix ns a -> m ()
ofor_ :: Matrix ns a -> (Element (Matrix ns a) -> f b) -> f ()
$cofor_ :: forall (ns :: [Peano]) a (f :: * -> *) b.
(SingI ns, Applicative f) =>
Matrix ns a -> (Element (Matrix ns a) -> f b) -> f ()
otraverse_ :: (Element (Matrix ns a) -> f b) -> Matrix ns a -> f ()
$cotraverse_ :: forall (ns :: [Peano]) a (f :: * -> *) b.
(SingI ns, Applicative f) =>
(Element (Matrix ns a) -> f b) -> Matrix ns a -> f ()
ocompareLength :: Matrix ns a -> i -> Ordering
$cocompareLength :: forall (ns :: [Peano]) a i.
(SingI ns, Integral i) =>
Matrix ns a -> i -> Ordering
olength64 :: Matrix ns a -> Int64
$colength64 :: forall (ns :: [Peano]) a. SingI ns => Matrix ns a -> Int64
olength :: Matrix ns a -> Int
$colength :: forall (ns :: [Peano]) a. SingI ns => Matrix ns a -> Int
onull :: Matrix ns a -> Bool
$conull :: forall (ns :: [Peano]) a. SingI ns => Matrix ns a -> Bool
oany :: (Element (Matrix ns a) -> Bool) -> Matrix ns a -> Bool
$coany :: forall (ns :: [Peano]) a.
SingI ns =>
(Element (Matrix ns a) -> Bool) -> Matrix ns a -> Bool
oall :: (Element (Matrix ns a) -> Bool) -> Matrix ns a -> Bool
$coall :: forall (ns :: [Peano]) a.
SingI ns =>
(Element (Matrix ns a) -> Bool) -> Matrix ns a -> Bool
otoList :: Matrix ns a -> [Element (Matrix ns a)]
$cotoList :: forall (ns :: [Peano]) a.
SingI ns =>
Matrix ns a -> [Element (Matrix ns a)]
ofoldl' :: (a -> Element (Matrix ns a) -> a) -> a -> Matrix ns a -> a
$cofoldl' :: forall (ns :: [Peano]) a a.
SingI ns =>
(a -> Element (Matrix ns a) -> a) -> a -> Matrix ns a -> a
ofoldr :: (Element (Matrix ns a) -> b -> b) -> b -> Matrix ns a -> b
$cofoldr :: forall (ns :: [Peano]) a b.
SingI ns =>
(Element (Matrix ns a) -> b -> b) -> b -> Matrix ns a -> b
ofoldMap :: (Element (Matrix ns a) -> m) -> Matrix ns a -> m
$cofoldMap :: forall (ns :: [Peano]) a m.
(SingI ns, Monoid m) =>
(Element (Matrix ns a) -> m) -> Matrix ns a -> m
MonoFoldable)

type instance Element (Matrix ns a) = a

---------------------------------
-- Defunctionalization Symbols --
---------------------------------

type MatrixTFSym2 (ns :: [Peano]) (t :: Type) = (MatrixTF ns t :: Type)

data MatrixTFSym1 (ns :: [Peano]) (z :: TyFun Type Type)
  = forall (arg :: Type).  SameKind (Apply (MatrixTFSym1 ns) arg) (MatrixTFSym2 ns arg) => MatrixTFSym1KindInference

type instance Apply (MatrixTFSym1 l1) l2 = MatrixTF l1 l2

type role MatrixTFSym0 phantom

data MatrixTFSym0 (l :: TyFun [Peano] (Type ~> Type))
  = forall (arg :: [Peano]).  SameKind (Apply MatrixTFSym0 arg) (MatrixTFSym1 arg) => MatrixTFSym0KindInference

type instance Apply MatrixTFSym0 l = MatrixTFSym1 l

type role MatrixTFSym1 phantom phantom

----------------------
-- Matrix Functions --
----------------------

eqSingMatrix :: forall (peanos :: [Peano]) (a :: Type). Eq a => Sing peanos -> Matrix peanos a -> Matrix peanos a -> Bool
eqSingMatrix :: Sing peanos -> Matrix peanos a -> Matrix peanos a -> Bool
eqSingMatrix = (a -> a -> Bool)
-> Bool
-> (Bool -> Bool -> Bool)
-> Sing peanos
-> Matrix peanos a
-> Matrix peanos a
-> Bool
forall (peanos :: [Peano]) a c.
(a -> a -> c)
-> c
-> (c -> c -> c)
-> Sing peanos
-> Matrix peanos a
-> Matrix peanos a
-> c
compareSingMatrix a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==) Bool
True Bool -> Bool -> Bool
(&&)

ordSingMatrix :: forall (peanos :: [Peano]) (a :: Type). Ord a => Sing peanos -> Matrix peanos a -> Matrix peanos a -> Ordering
ordSingMatrix :: Sing peanos -> Matrix peanos a -> Matrix peanos a -> Ordering
ordSingMatrix = (a -> a -> Ordering)
-> Ordering
-> (Ordering -> Ordering -> Ordering)
-> Sing peanos
-> Matrix peanos a
-> Matrix peanos a
-> Ordering
forall (peanos :: [Peano]) a c.
(a -> a -> c)
-> c
-> (c -> c -> c)
-> Sing peanos
-> Matrix peanos a
-> Matrix peanos a
-> c
compareSingMatrix a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Ordering
EQ Ordering -> Ordering -> Ordering
f
  where
    f :: Ordering -> Ordering -> Ordering
    f :: Ordering -> Ordering -> Ordering
f EQ o :: Ordering
o = Ordering
o
    f o :: Ordering
o _ = Ordering
o

compareSingMatrix ::
     forall (peanos :: [Peano]) (a :: Type) (c :: Type)
   . (a -> a -> c)
  -> c
  -> (c -> c -> c)
  -> Sing peanos
  -> Matrix peanos a
  -> Matrix peanos a
  -> c
compareSingMatrix :: (a -> a -> c)
-> c
-> (c -> c -> c)
-> Sing peanos
-> Matrix peanos a
-> Matrix peanos a
-> c
compareSingMatrix f :: a -> a -> c
f _ _ SNil (Matrix a :: MatrixTF peanos a
a) (Matrix b :: MatrixTF peanos a
b) = a -> a -> c
f a
MatrixTF peanos a
a a
MatrixTF peanos a
b
compareSingMatrix _ empt :: c
empt _ (SCons SZ _) (Matrix EmptyVec) (Matrix EmptyVec) = c
empt
compareSingMatrix f :: a -> a -> c
f empt :: c
empt combine :: c -> c -> c
combine (SCons (SS peanoSingle) moreN) (Matrix (a :* moreA)) (Matrix (b :* moreB)) =
  c -> c -> c
combine
    ((a -> a -> c)
-> c -> (c -> c -> c) -> Sing n2 -> Matrix n2 a -> Matrix n2 a -> c
forall (peanos :: [Peano]) a c.
(a -> a -> c)
-> c
-> (c -> c -> c)
-> Sing peanos
-> Matrix peanos a
-> Matrix peanos a
-> c
compareSingMatrix a -> a -> c
f c
empt c -> c -> c
combine Sing n2
moreN (MatrixTF n2 a -> Matrix n2 a
forall (ns :: [Peano]) a. MatrixTF ns a -> Matrix ns a
Matrix MatrixTF n2 a
a) (MatrixTF n2 a -> Matrix n2 a
forall (ns :: [Peano]) a. MatrixTF ns a -> Matrix ns a
Matrix MatrixTF n2 a
b))
    ((a -> a -> c)
-> c
-> (c -> c -> c)
-> Sing (n : n2)
-> Matrix (n : n2) a
-> Matrix (n : n2) a
-> c
forall (peanos :: [Peano]) a c.
(a -> a -> c)
-> c
-> (c -> c -> c)
-> Sing peanos
-> Matrix peanos a
-> Matrix peanos a
-> c
compareSingMatrix a -> a -> c
f c
empt c -> c -> c
combine (Sing n -> Sing n2 -> SList (n : n2)
forall a0 (n1 :: a0) (n2 :: [a0]).
Sing n1 -> Sing n2 -> SList (n1 : n2)
SCons Sing n
peanoSingle Sing n2
moreN) (MatrixTF (n : n2) a -> Matrix (n : n2) a
forall (ns :: [Peano]) a. MatrixTF ns a -> Matrix ns a
Matrix MatrixTF (n : n2) a
Vec n (MatrixTF n2 a)
moreA) (MatrixTF (n : n2) a -> Matrix (n : n2) a
forall (ns :: [Peano]) a. MatrixTF ns a -> Matrix ns a
Matrix MatrixTF (n : n2) a
Vec n (MatrixTF n2 a)
moreB))

fmapSingMatrix :: forall (peanos :: [Peano]) (a :: Type) (b ::Type). Sing peanos -> (a -> b) -> Matrix peanos a -> Matrix peanos b
fmapSingMatrix :: Sing peanos -> (a -> b) -> Matrix peanos a -> Matrix peanos b
fmapSingMatrix SNil f :: a -> b
f (Matrix a :: MatrixTF peanos a
a) = MatrixTF peanos b -> Matrix peanos b
forall (ns :: [Peano]) a. MatrixTF ns a -> Matrix ns a
Matrix (MatrixTF peanos b -> Matrix peanos b)
-> MatrixTF peanos b -> Matrix peanos b
forall a b. (a -> b) -> a -> b
$ a -> b
f a
MatrixTF peanos a
a
fmapSingMatrix (SCons SZ _) _ (Matrix EmptyVec) = MatrixTF peanos b -> Matrix peanos b
forall (ns :: [Peano]) a. MatrixTF ns a -> Matrix ns a
Matrix MatrixTF peanos b
forall a. Vec 'Z a
EmptyVec
fmapSingMatrix (SCons (SS peanoSingle) moreN) f :: a -> b
f (Matrix (a :* moreA)) =
  let matA :: Matrix n2 b
matA = Sing n2 -> (a -> b) -> Matrix n2 a -> Matrix n2 b
forall (peanos :: [Peano]) a b.
Sing peanos -> (a -> b) -> Matrix peanos a -> Matrix peanos b
fmapSingMatrix Sing n2
moreN a -> b
f (MatrixTF n2 a -> Matrix n2 a
forall (ns :: [Peano]) a. MatrixTF ns a -> Matrix ns a
Matrix MatrixTF n2 a
a)
      matB :: Matrix (n : n2) b
matB = Sing (n : n2) -> (a -> b) -> Matrix (n : n2) a -> Matrix (n : n2) b
forall (peanos :: [Peano]) a b.
Sing peanos -> (a -> b) -> Matrix peanos a -> Matrix peanos b
fmapSingMatrix (Sing n -> Sing n2 -> SList (n : n2)
forall a0 (n1 :: a0) (n2 :: [a0]).
Sing n1 -> Sing n2 -> SList (n1 : n2)
SCons Sing n
peanoSingle Sing n2
moreN) a -> b
f (MatrixTF (n : n2) a -> Matrix (n : n2) a
forall (ns :: [Peano]) a. MatrixTF ns a -> Matrix ns a
Matrix MatrixTF (n : n2) a
Vec n (MatrixTF n2 a)
moreA)
  in Matrix n2 b -> Matrix (n : n2) b -> Matrix ('S n : n2) b
forall (ns :: [Peano]) a (n :: Peano).
Matrix ns a -> Matrix (n : ns) a -> Matrix ('S n : ns) a
consMatrix Matrix n2 b
matA Matrix (n : n2) b
matB

consMatrix :: Matrix ns a -> Matrix (n ': ns) a -> Matrix ('S n ': ns) a
consMatrix :: Matrix ns a -> Matrix (n : ns) a -> Matrix ('S n : ns) a
consMatrix (Matrix a :: MatrixTF ns a
a) (Matrix as :: MatrixTF (n : ns) a
as) = MatrixTF ('S n : ns) a -> Matrix ('S n : ns) a
forall (ns :: [Peano]) a. MatrixTF ns a -> Matrix ns a
Matrix (MatrixTF ('S n : ns) a -> Matrix ('S n : ns) a)
-> MatrixTF ('S n : ns) a -> Matrix ('S n : ns) a
forall a b. (a -> b) -> a -> b
$ MatrixTF ns a
-> Vec n (MatrixTF ns a) -> Vec ('S n) (MatrixTF ns a)
forall a (n :: Peano). a -> Vec n a -> Vec ('S n) a
ConsVec MatrixTF ns a
a MatrixTF (n : ns) a
Vec n (MatrixTF ns a)
as

toListMatrix ::
     forall (peanos :: [Peano]) (a :: Type).
     Sing peanos
  -> Matrix peanos a
  -> [a]
toListMatrix :: Sing peanos -> Matrix peanos a -> [a]
toListMatrix SNil (Matrix a :: MatrixTF peanos a
a) = [Item [a]
MatrixTF peanos a
a]
toListMatrix (SCons SZ _) (Matrix EmptyVec) = []
toListMatrix (SCons (SS peanoSingle) moreN) (Matrix (a :* moreA)) =
  Sing n2 -> Matrix n2 a -> [a]
forall (peanos :: [Peano]) a. Sing peanos -> Matrix peanos a -> [a]
toListMatrix Sing n2
moreN (MatrixTF n2 a -> Matrix n2 a
forall (ns :: [Peano]) a. MatrixTF ns a -> Matrix ns a
Matrix MatrixTF n2 a
a) [a] -> [a] -> [a]
forall a. Semigroup a => a -> a -> a
<> Sing (n : n2) -> Matrix (n : n2) a -> [a]
forall (peanos :: [Peano]) a. Sing peanos -> Matrix peanos a -> [a]
toListMatrix (Sing n -> Sing n2 -> SList (n : n2)
forall a0 (n1 :: a0) (n2 :: [a0]).
Sing n1 -> Sing n2 -> SList (n1 : n2)
SCons Sing n
peanoSingle Sing n2
moreN) (MatrixTF (n : n2) a -> Matrix (n : n2) a
forall (ns :: [Peano]) a. MatrixTF ns a -> Matrix ns a
Matrix MatrixTF (n : n2) a
Vec n (MatrixTF n2 a)
moreA)

genMatrix ::
     forall (ns :: [Peano]) (a :: Type).
     Sing ns
  -> (HList Fin ns -> a)
  -> Matrix ns a
genMatrix :: Sing ns -> (HList Fin ns -> a) -> Matrix ns a
genMatrix SNil f :: HList Fin ns -> a
f = MatrixTF ns a -> Matrix ns a
forall (ns :: [Peano]) a. MatrixTF ns a -> Matrix ns a
Matrix (MatrixTF ns a -> Matrix ns a) -> MatrixTF ns a -> Matrix ns a
forall a b. (a -> b) -> a -> b
$ HList Fin ns -> a
f HList Fin ns
forall k (f :: k -> *). HList f '[]
EmptyHList
genMatrix (SCons (n :: SPeano foo) (ns' :: Sing oaoa)) f :: HList Fin ns -> a
f =
  MatrixTF ns a -> Matrix ns a
forall (ns :: [Peano]) a. MatrixTF ns a -> Matrix ns a
Matrix (MatrixTF ns a -> Matrix ns a) -> MatrixTF ns a -> Matrix ns a
forall a b. (a -> b) -> a -> b
$ (SPeano n1 -> (Fin n1 -> MatrixTF n2 a) -> Vec n1 (MatrixTF n2 a)
forall (n :: Peano) a. SPeano n -> (Fin n -> a) -> Vec n a
genVec SPeano n1
n ((Fin n1 -> MatrixTF n2 a) -> Vec n1 (MatrixTF n2 a))
-> (Fin n1 -> MatrixTF n2 a) -> Vec n1 (MatrixTF n2 a)
forall a b. (a -> b) -> a -> b
$ (Fin n1 -> MatrixTF n2 a
gagaga :: Fin foo -> MatrixTF oaoa a) :: Vec foo (MatrixTF oaoa a))
  where
    gagaga :: Fin foo -> MatrixTF oaoa a
    gagaga :: Fin n1 -> MatrixTF n2 a
gagaga faaa :: Fin n1
faaa = Matrix n2 a -> MatrixTF n2 a
forall (ns :: [Peano]) a. Matrix ns a -> MatrixTF ns a
unMatrix (Matrix n2 a -> MatrixTF n2 a) -> Matrix n2 a -> MatrixTF n2 a
forall a b. (a -> b) -> a -> b
$ (Sing n2 -> (HList Fin n2 -> a) -> Matrix n2 a
forall (ns :: [Peano]) a.
Sing ns -> (HList Fin ns -> a) -> Matrix ns a
genMatrix Sing n2
ns' ((HList Fin n2 -> a) -> Matrix n2 a)
-> (HList Fin n2 -> a) -> Matrix n2 a
forall a b. (a -> b) -> a -> b
$ Fin n1 -> HList Fin n2 -> a
byebye Fin n1
faaa :: Matrix oaoa a)

    byebye :: Fin foo -> HList Fin oaoa -> a
    byebye :: Fin n1 -> HList Fin n2 -> a
byebye faaa :: Fin n1
faaa = HList Fin ns -> a
HList Fin (n1 : n2) -> a
f (HList Fin (n1 : n2) -> a)
-> (HList Fin n2 -> HList Fin (n1 : n2)) -> HList Fin n2 -> a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Fin n1 -> HList Fin n2 -> HList Fin (n1 : n2)
forall a (f :: a -> *) (a1 :: a) (as :: [a]).
f a1 -> HList f as -> HList f (a1 : as)
ConsHList Fin n1
faaa

genMatrix_ :: SingI ns => (HList Fin ns -> a) -> Matrix ns a
genMatrix_ :: (HList Fin ns -> a) -> Matrix ns a
genMatrix_ = Sing ns -> (HList Fin ns -> a) -> Matrix ns a
forall (ns :: [Peano]) a.
Sing ns -> (HList Fin ns -> a) -> Matrix ns a
genMatrix Sing ns
forall k (a :: k). SingI a => Sing a
sing

indexMatrix :: HList Fin ns -> Matrix ns a -> a
indexMatrix :: HList Fin ns -> Matrix ns a -> a
indexMatrix EmptyHList (Matrix a :: MatrixTF ns a
a) = a
MatrixTF ns a
a
indexMatrix (i :: Fin a
i :< is :: HList Fin as
is) (Matrix vec :: MatrixTF ns a
vec) = HList Fin as -> Matrix as a -> a
forall (ns :: [Peano]) a. HList Fin ns -> Matrix ns a -> a
indexMatrix HList Fin as
is (Matrix as a -> a) -> Matrix as a -> a
forall a b. (a -> b) -> a -> b
$ MatrixTF as a -> Matrix as a
forall (ns :: [Peano]) a. MatrixTF ns a -> Matrix ns a
Matrix (Fin a -> Vec a (MatrixTF as a) -> MatrixTF as a
forall (n :: Peano) a. Fin n -> Vec n a -> a
indexVec Fin a
i MatrixTF ns a
Vec a (MatrixTF as a)
vec)

imapMatrix :: forall (ns :: [Peano]) a b. Sing ns -> (HList Fin ns -> a -> b) -> Matrix ns a -> Matrix ns b
imapMatrix :: Sing ns -> (HList Fin ns -> a -> b) -> Matrix ns a -> Matrix ns b
imapMatrix SNil f :: HList Fin ns -> a -> b
f (Matrix a :: MatrixTF ns a
a) = MatrixTF ns b -> Matrix ns b
forall (ns :: [Peano]) a. MatrixTF ns a -> Matrix ns a
Matrix (HList Fin ns -> a -> b
f HList Fin ns
forall k (f :: k -> *). HList f '[]
EmptyHList a
MatrixTF ns a
a)
imapMatrix (SCons _ ns) f :: HList Fin ns -> a -> b
f matrix :: Matrix ns a
matrix =
  (MatrixTF ns a -> MatrixTF ns b) -> Matrix ns a -> Matrix ns b
forall (ns :: [Peano]) a (ms :: [Peano]) b.
(MatrixTF ns a -> MatrixTF ms b) -> Matrix ns a -> Matrix ms b
onMatrixTF
    ((Fin n1 -> MatrixTF n2 a -> MatrixTF n2 b)
-> Vec n1 (MatrixTF n2 a) -> Vec n1 (MatrixTF n2 b)
forall (n :: Peano) a b. (Fin n -> a -> b) -> Vec n a -> Vec n b
imapVec (\fin' :: Fin n1
fin' -> (Matrix n2 a -> Matrix n2 b) -> MatrixTF n2 a -> MatrixTF n2 b
forall (ns :: [Peano]) a (ms :: [Peano]) b.
(Matrix ns a -> Matrix ms b) -> MatrixTF ns a -> MatrixTF ms b
onMatrix (Sing n2 -> (HList Fin n2 -> a -> b) -> Matrix n2 a -> Matrix n2 b
forall (ns :: [Peano]) a b.
Sing ns -> (HList Fin ns -> a -> b) -> Matrix ns a -> Matrix ns b
imapMatrix Sing n2
ns (\hlist :: HList Fin n2
hlist -> HList Fin ns -> a -> b
f (Fin n1 -> HList Fin n2 -> HList Fin (n1 : n2)
forall a (f :: a -> *) (a1 :: a) (as :: [a]).
f a1 -> HList f as -> HList f (a1 : as)
ConsHList Fin n1
fin' HList Fin n2
hlist)))))
    Matrix ns a
matrix

imapMatrix_ :: SingI ns => (HList Fin ns -> a -> b) -> Matrix ns a -> Matrix ns b
imapMatrix_ :: (HList Fin ns -> a -> b) -> Matrix ns a -> Matrix ns b
imapMatrix_ = Sing ns -> (HList Fin ns -> a -> b) -> Matrix ns a -> Matrix ns b
forall (ns :: [Peano]) a b.
Sing ns -> (HList Fin ns -> a -> b) -> Matrix ns a -> Matrix ns b
imapMatrix Sing ns
forall k (a :: k). SingI a => Sing a
sing

onMatrixTF :: (MatrixTF ns a -> MatrixTF ms b) -> Matrix ns a -> Matrix ms b
onMatrixTF :: (MatrixTF ns a -> MatrixTF ms b) -> Matrix ns a -> Matrix ms b
onMatrixTF f :: MatrixTF ns a -> MatrixTF ms b
f (Matrix mat :: MatrixTF ns a
mat) = MatrixTF ms b -> Matrix ms b
forall (ns :: [Peano]) a. MatrixTF ns a -> Matrix ns a
Matrix (MatrixTF ms b -> Matrix ms b) -> MatrixTF ms b -> Matrix ms b
forall a b. (a -> b) -> a -> b
$ MatrixTF ns a -> MatrixTF ms b
f MatrixTF ns a
mat

onMatrix :: (Matrix ns a -> Matrix ms b) -> MatrixTF ns a -> MatrixTF ms b
onMatrix :: (Matrix ns a -> Matrix ms b) -> MatrixTF ns a -> MatrixTF ms b
onMatrix f :: Matrix ns a -> Matrix ms b
f = Matrix ms b -> MatrixTF ms b
forall (ns :: [Peano]) a. Matrix ns a -> MatrixTF ns a
unMatrix (Matrix ms b -> MatrixTF ms b)
-> (MatrixTF ns a -> Matrix ms b) -> MatrixTF ns a -> MatrixTF ms b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Matrix ns a -> Matrix ms b
f (Matrix ns a -> Matrix ms b)
-> (MatrixTF ns a -> Matrix ns a) -> MatrixTF ns a -> Matrix ms b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. MatrixTF ns a -> Matrix ns a
forall (ns :: [Peano]) a. MatrixTF ns a -> Matrix ns a
Matrix

updateAtMatrix :: HList Fin ns -> (a -> a) -> Matrix ns a -> Matrix ns a
updateAtMatrix :: HList Fin ns -> (a -> a) -> Matrix ns a -> Matrix ns a
updateAtMatrix EmptyHList _ mat :: Matrix ns a
mat = Matrix ns a
mat
updateAtMatrix (n :: Fin a
n :< ns :: HList Fin as
ns) f :: a -> a
f mat :: Matrix ns a
mat =
  (MatrixTF ns a -> MatrixTF ns a) -> Matrix ns a -> Matrix ns a
forall (ns :: [Peano]) a (ms :: [Peano]) b.
(MatrixTF ns a -> MatrixTF ms b) -> Matrix ns a -> Matrix ms b
onMatrixTF (Fin a
-> (MatrixTF as a -> MatrixTF as a)
-> Vec a (MatrixTF as a)
-> Vec a (MatrixTF as a)
forall (n :: Peano) a. Fin n -> (a -> a) -> Vec n a -> Vec n a
updateAtVec Fin a
n ((Matrix as a -> Matrix as a) -> MatrixTF as a -> MatrixTF as a
forall (ns :: [Peano]) a (ms :: [Peano]) b.
(Matrix ns a -> Matrix ms b) -> MatrixTF ns a -> MatrixTF ms b
onMatrix (HList Fin as -> (a -> a) -> Matrix as a -> Matrix as a
forall (ns :: [Peano]) a.
HList Fin ns -> (a -> a) -> Matrix ns a -> Matrix ns a
updateAtMatrix HList Fin as
ns a -> a
f))) Matrix ns a
mat

setAtMatrix :: HList Fin ns -> a -> Matrix ns a -> Matrix ns a
setAtMatrix :: HList Fin ns -> a -> Matrix ns a -> Matrix ns a
setAtMatrix fins :: HList Fin ns
fins a :: a
a = HList Fin ns -> (a -> a) -> Matrix ns a -> Matrix ns a
forall (ns :: [Peano]) a.
HList Fin ns -> (a -> a) -> Matrix ns a -> Matrix ns a
updateAtMatrix HList Fin ns
fins (a -> a -> a
forall a b. a -> b -> a
const a
a)

----------------------
-- Matrix Instances --
----------------------

deriving instance (Eq (MatrixTF ns a)) => Eq (Matrix ns a)

deriving instance (Ord (MatrixTF ns a)) => Ord (Matrix ns a)

deriving instance (Show (MatrixTF ns a)) => Show (Matrix ns a)

instance SingI ns => Functor (Matrix ns) where
  fmap :: (a -> b) -> Matrix ns a -> Matrix ns b
  fmap :: (a -> b) -> Matrix ns a -> Matrix ns b
fmap = Sing ns -> (a -> b) -> Matrix ns a -> Matrix ns b
forall (peanos :: [Peano]) a b.
Sing peanos -> (a -> b) -> Matrix peanos a -> Matrix peanos b
fmapSingMatrix Sing ns
forall k (a :: k). SingI a => Sing a
sing

instance SingI ns => Data.Foldable.Foldable (Matrix ns) where
  foldr :: (a -> b -> b) -> b -> Matrix ns a -> b
  foldr :: (a -> b -> b) -> b -> Matrix ns a -> b
foldr comb :: a -> b -> b
comb b :: b
b = (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
Data.Foldable.foldr a -> b -> b
comb b
b ([a] -> b) -> (Matrix ns a -> [a]) -> Matrix ns a -> b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Sing ns -> Matrix ns a -> [a]
forall (peanos :: [Peano]) a. Sing peanos -> Matrix peanos a -> [a]
toListMatrix Sing ns
forall k (a :: k). SingI a => Sing a
sing

  toList :: Matrix ns a -> [a]
  toList :: Matrix ns a -> [a]
toList = Sing ns -> Matrix ns a -> [a]
forall (peanos :: [Peano]) a. Sing peanos -> Matrix peanos a -> [a]
toListMatrix Sing ns
forall k (a :: k). SingI a => Sing a
sing

instance SingI ns => Distributive (Matrix ns) where
  distribute :: Functor f => f (Matrix ns a) -> Matrix ns (f a)
  distribute :: f (Matrix ns a) -> Matrix ns (f a)
distribute = f (Matrix ns a) -> Matrix ns (f a)
forall (f :: * -> *) (w :: * -> *) a.
(Representable f, Functor w) =>
w (f a) -> f (w a)
distributeRep

instance SingI ns => Representable (Matrix ns) where
  type Rep (Matrix ns) = HList Fin ns

  tabulate :: (HList Fin ns -> a) -> Matrix ns a
  tabulate :: (HList Fin ns -> a) -> Matrix ns a
tabulate = (HList Fin ns -> a) -> Matrix ns a
forall (ns :: [Peano]) a.
SingI ns =>
(HList Fin ns -> a) -> Matrix ns a
genMatrix_

  index :: Matrix ns a -> HList Fin ns -> a
  index :: Matrix ns a -> HList Fin ns -> a
index = (HList Fin ns -> Matrix ns a -> a)
-> Matrix ns a -> HList Fin ns -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip HList Fin ns -> Matrix ns a -> a
forall (ns :: [Peano]) a. HList Fin ns -> Matrix ns a -> a
indexMatrix

instance Num a => Num (Matrix '[] a) where
  Matrix a :: MatrixTF '[] a
a + :: Matrix '[] a -> Matrix '[] a -> Matrix '[] a
+ Matrix b :: MatrixTF '[] a
b = MatrixTF '[] a -> Matrix '[] a
forall (ns :: [Peano]) a. MatrixTF ns a -> Matrix ns a
Matrix (a
MatrixTF '[] a
a a -> a -> a
forall a. Num a => a -> a -> a
+ a
MatrixTF '[] a
b)

  Matrix a :: MatrixTF '[] a
a * :: Matrix '[] a -> Matrix '[] a -> Matrix '[] a
* Matrix b :: MatrixTF '[] a
b = MatrixTF '[] a -> Matrix '[] a
forall (ns :: [Peano]) a. MatrixTF ns a -> Matrix ns a
Matrix (a
MatrixTF '[] a
a a -> a -> a
forall a. Num a => a -> a -> a
* a
MatrixTF '[] a
b)

  Matrix a :: MatrixTF '[] a
a - :: Matrix '[] a -> Matrix '[] a -> Matrix '[] a
- Matrix b :: MatrixTF '[] a
b = MatrixTF '[] a -> Matrix '[] a
forall (ns :: [Peano]) a. MatrixTF ns a -> Matrix ns a
Matrix (a
MatrixTF '[] a
a a -> a -> a
forall a. Num a => a -> a -> a
- a
MatrixTF '[] a
b)

  abs :: Matrix '[] a -> Matrix '[] a
abs (Matrix a :: MatrixTF '[] a
a) = MatrixTF '[] a -> Matrix '[] a
forall (ns :: [Peano]) a. MatrixTF ns a -> Matrix ns a
Matrix (a -> a
forall a. Num a => a -> a
abs a
MatrixTF '[] a
a)

  signum :: Matrix '[] a -> Matrix '[] a
signum (Matrix a :: MatrixTF '[] a
a) = MatrixTF '[] a -> Matrix '[] a
forall (ns :: [Peano]) a. MatrixTF ns a -> Matrix ns a
Matrix (a -> a
forall a. Num a => a -> a
signum a
MatrixTF '[] a
a)

  fromInteger :: Integer -> Matrix '[] a
  fromInteger :: Integer -> Matrix '[] a
fromInteger = a -> Matrix '[] a
forall (ns :: [Peano]) a. MatrixTF ns a -> Matrix ns a
Matrix (a -> Matrix '[] a) -> (Integer -> a) -> Integer -> Matrix '[] a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Integer -> a
forall a. Num a => Integer -> a
fromInteger

instance SingI ns => Applicative (Matrix ns) where
  pure :: a -> Matrix ns a
  pure :: a -> Matrix ns a
pure = a -> Matrix ns a
forall (f :: * -> *) a. Representable f => a -> f a
pureRep

  (<*>) :: Matrix ns (a -> b) -> Matrix ns a -> Matrix ns b
  <*> :: Matrix ns (a -> b) -> Matrix ns a -> Matrix ns b
(<*>) = Matrix ns (a -> b) -> Matrix ns a -> Matrix ns b
forall (f :: * -> *) a b.
Representable f =>
f (a -> b) -> f a -> f b
apRep

instance SingI ns => Monad (Matrix ns) where
  (>>=) :: Matrix ns a -> (a -> Matrix ns b) -> Matrix ns b
  >>= :: Matrix ns a -> (a -> Matrix ns b) -> Matrix ns b
(>>=) = Matrix ns a -> (a -> Matrix ns b) -> Matrix ns b
forall (f :: * -> *) a b.
Representable f =>
f a -> (a -> f b) -> f b
bindRep