{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

{- |
Module      : Cybus.FinMat
Description : fixed-sized indices for a matrix
Copyright   : (c) Grant Weyburne, 2022
License     : BSD-3
-}
module Cybus.FinMat (
  -- * core type
  type FinMat,
  fmPos,
  fmNS,
  pattern FinMat,
  pattern FinMatU,

  -- * constructors
  FinMatC (..),
  mkFinMat,
  mkFinMatC,
  finMat,
  toFinMatFromPos,

  -- * conversions
  finMatToNonEmpty,
  nonEmptyToFinMat,
  nonEmptyToFinMat',

  -- * read/show methods
  showFinMat,
  readFinMatP,
  readFinMat,
  showFinMat',

  -- * miscellaneous
  NS (..),
  NSRangeC,
  relPos,
  finMatFinSet,
  finMatFinGet,

  -- * lens into the matrix indices
  _finMatCons,
  _finMatFin,
  _i1,
  _i2,
  _i3,
  _i4,
  _i5,
  _i6,
  _i7,
  _i8,
  _i9,
  _i10,
) where

import Control.DeepSeq
import Cybus.Fin
import Cybus.NatHelper
import Data.Kind
import qualified Data.List as L
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty as N
import Data.Pos
import Data.Semigroup.Foldable
import Data.These
import GHC.Enum
import GHC.Generics (Generic, Generic1)
import GHC.Read (readPrec)
import GHC.Stack
import qualified GHC.TypeLits as GL
import GHC.TypeNats (Nat)
import qualified GHC.TypeNats as GN
import Primus.Enum
import Primus.Error
import Primus.Lens
import Primus.NonEmpty
import Primus.Num1
import qualified Primus.TypeLevel as TP (LengthT, pnat)
import qualified Text.ParserCombinators.ReadP as P
import qualified Text.ParserCombinators.ReadPrec as PC

-- | definition of the indices of a matrix
type FinMat :: [Nat] -> Type
data FinMat ns = FinMatUnsafe !Int !(NonEmpty Pos)
  deriving stock (FinMat ns -> FinMat ns -> Bool
(FinMat ns -> FinMat ns -> Bool)
-> (FinMat ns -> FinMat ns -> Bool) -> Eq (FinMat ns)
forall (ns :: [Nat]). FinMat ns -> FinMat ns -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FinMat ns -> FinMat ns -> Bool
$c/= :: forall (ns :: [Nat]). FinMat ns -> FinMat ns -> Bool
== :: FinMat ns -> FinMat ns -> Bool
$c== :: forall (ns :: [Nat]). FinMat ns -> FinMat ns -> Bool
Eq, Eq (FinMat ns)
Eq (FinMat ns)
-> (FinMat ns -> FinMat ns -> Ordering)
-> (FinMat ns -> FinMat ns -> Bool)
-> (FinMat ns -> FinMat ns -> Bool)
-> (FinMat ns -> FinMat ns -> Bool)
-> (FinMat ns -> FinMat ns -> Bool)
-> (FinMat ns -> FinMat ns -> FinMat ns)
-> (FinMat ns -> FinMat ns -> FinMat ns)
-> Ord (FinMat ns)
FinMat ns -> FinMat ns -> Bool
FinMat ns -> FinMat ns -> Ordering
FinMat ns -> FinMat ns -> FinMat ns
forall (ns :: [Nat]). Eq (FinMat ns)
forall (ns :: [Nat]). FinMat ns -> FinMat ns -> Bool
forall (ns :: [Nat]). FinMat ns -> FinMat ns -> Ordering
forall (ns :: [Nat]). FinMat ns -> FinMat ns -> FinMat ns
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: FinMat ns -> FinMat ns -> FinMat ns
$cmin :: forall (ns :: [Nat]). FinMat ns -> FinMat ns -> FinMat ns
max :: FinMat ns -> FinMat ns -> FinMat ns
$cmax :: forall (ns :: [Nat]). FinMat ns -> FinMat ns -> FinMat ns
>= :: FinMat ns -> FinMat ns -> Bool
$c>= :: forall (ns :: [Nat]). FinMat ns -> FinMat ns -> Bool
> :: FinMat ns -> FinMat ns -> Bool
$c> :: forall (ns :: [Nat]). FinMat ns -> FinMat ns -> Bool
<= :: FinMat ns -> FinMat ns -> Bool
$c<= :: forall (ns :: [Nat]). FinMat ns -> FinMat ns -> Bool
< :: FinMat ns -> FinMat ns -> Bool
$c< :: forall (ns :: [Nat]). FinMat ns -> FinMat ns -> Bool
compare :: FinMat ns -> FinMat ns -> Ordering
$ccompare :: forall (ns :: [Nat]). FinMat ns -> FinMat ns -> Ordering
$cp1Ord :: forall (ns :: [Nat]). Eq (FinMat ns)
Ord, (forall x. FinMat ns -> Rep (FinMat ns) x)
-> (forall x. Rep (FinMat ns) x -> FinMat ns)
-> Generic (FinMat ns)
forall (ns :: [Nat]) x. Rep (FinMat ns) x -> FinMat ns
forall (ns :: [Nat]) x. FinMat ns -> Rep (FinMat ns) x
forall x. Rep (FinMat ns) x -> FinMat ns
forall x. FinMat ns -> Rep (FinMat ns) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall (ns :: [Nat]) x. Rep (FinMat ns) x -> FinMat ns
$cfrom :: forall (ns :: [Nat]) x. FinMat ns -> Rep (FinMat ns) x
Generic, (forall (a :: [Nat]). FinMat a -> Rep1 FinMat a)
-> (forall (a :: [Nat]). Rep1 FinMat a -> FinMat a)
-> Generic1 FinMat
forall (a :: [Nat]). Rep1 FinMat a -> FinMat a
forall (a :: [Nat]). FinMat a -> Rep1 FinMat a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cto1 :: forall (a :: [Nat]). Rep1 FinMat a -> FinMat a
$cfrom1 :: forall (a :: [Nat]). FinMat a -> Rep1 FinMat a
Generic1)
  deriving anyclass (FinMat ns -> ()
(FinMat ns -> ()) -> NFData (FinMat ns)
forall (ns :: [Nat]). FinMat ns -> ()
forall a. (a -> ()) -> NFData a
rnf :: FinMat ns -> ()
$crnf :: forall (ns :: [Nat]). FinMat ns -> ()
NFData)

-- | accessor for the relative position within a matrix
fmPos :: FinMat ns -> Int
fmPos :: FinMat ns -> Int
fmPos (FinMatUnsafe Int
i NonEmpty Pos
_) = Int
i

-- | accessor for the indices of a matrix
fmNS :: FinMat ns -> NonEmpty Pos
fmNS :: FinMat ns -> NonEmpty Pos
fmNS (FinMatUnsafe Int
_ NonEmpty Pos
ns) = NonEmpty Pos
ns

-- | readonly pattern synonym for finmatrix
{-# COMPLETE FinMat #-}

pattern FinMat ::
  forall (ns :: [Nat]).
  Int ->
  NonEmpty Pos ->
  FinMat ns
pattern $mFinMat :: forall r (ns :: [Nat]).
FinMat ns -> (Int -> NonEmpty Pos -> r) -> (Void# -> r) -> r
FinMat i ps <- FinMatUnsafe i ps

{-# COMPLETE FinMatU #-}

-- | pattern synonym for validating the finmatrix before construction but uses an extra 'NS' constraint to check "ns"
pattern FinMatU ::
  forall (ns :: [Nat]).
  (HasCallStack, NS ns) =>
  Int ->
  NonEmpty Pos ->
  FinMat ns
pattern $bFinMatU :: Int -> NonEmpty Pos -> FinMat ns
$mFinMatU :: forall r (ns :: [Nat]).
(HasCallStack, NS ns) =>
FinMat ns -> (Int -> NonEmpty Pos -> r) -> (Void# -> r) -> r
FinMatU i ps <-
  FinMatUnsafe i ps
  where
    FinMatU = Either String (FinMat ns) -> FinMat ns
forall a. HasCallStack => Either String a -> a
frp (Either String (FinMat ns) -> FinMat ns)
-> (Int -> NonEmpty Pos -> Either String (FinMat ns))
-> Int
-> NonEmpty Pos
-> FinMat ns
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
.@ Int -> NonEmpty Pos -> Either String (FinMat ns)
forall (ns :: [Nat]).
NS ns =>
Int -> NonEmpty Pos -> Either String (FinMat ns)
mkFinMatC

-- | create a FinMat value level "i" and "ns" values and validate that "i" is in range
mkFinMat :: Int -> NonEmpty Pos -> Either String (FinMat ns)
mkFinMat :: Int -> NonEmpty Pos -> Either String (FinMat ns)
mkFinMat Int
i NonEmpty Pos
ps = String -> Either String (FinMat ns) -> Either String (FinMat ns)
forall a. String -> Either String a -> Either String a
lmsg String
"mkFinMat" (Either String (FinMat ns) -> Either String (FinMat ns))
-> Either String (FinMat ns) -> Either String (FinMat ns)
forall a b. (a -> b) -> a -> b
$ do
  let tot :: Int
tot = NonEmpty Pos -> Int
forall (t :: * -> *). Foldable t => t Pos -> Int
productPInt NonEmpty Pos
ps
  if
      | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 -> String -> Either String (FinMat ns)
forall a b. a -> Either a b
Left (String -> Either String (FinMat ns))
-> String -> Either String (FinMat ns)
forall a b. (a -> b) -> a -> b
$ String
"cant be less than 0: i=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
      | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
tot -> String -> Either String (FinMat ns)
forall a b. a -> Either a b
Left (String -> Either String (FinMat ns))
-> String -> Either String (FinMat ns)
forall a b. (a -> b) -> a -> b
$ String
"is too large: maximum is " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
tot Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" but found " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
      | Bool
otherwise -> FinMat ns -> Either String (FinMat ns)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> NonEmpty Pos -> FinMat ns
forall (ns :: [Nat]). Int -> NonEmpty Pos -> FinMat ns
FinMatUnsafe Int
i NonEmpty Pos
ps)

-- | create a FinMat value level "i" and "ns" values and validate against expected "ns"
mkFinMatC :: forall ns. NS ns => Int -> NonEmpty Pos -> Either String (FinMat ns)
mkFinMatC :: Int -> NonEmpty Pos -> Either String (FinMat ns)
mkFinMatC Int
i NonEmpty Pos
ps = do
  let ns :: NonEmpty Pos
ns = NS ns => NonEmpty Pos
forall (ns :: [Nat]). NS ns => NonEmpty Pos
fromNSP @ns
  if NonEmpty Pos
ns NonEmpty Pos -> NonEmpty Pos -> Bool
forall a. Eq a => a -> a -> Bool
== NonEmpty Pos
ps
    then Int -> NonEmpty Pos -> Either String (FinMat ns)
forall (ns :: [Nat]).
Int -> NonEmpty Pos -> Either String (FinMat ns)
mkFinMat Int
i NonEmpty Pos
ps
    else String -> Either String (FinMat ns)
forall a b. a -> Either a b
Left (String -> Either String (FinMat ns))
-> String -> Either String (FinMat ns)
forall a b. (a -> b) -> a -> b
$ String
"mkFinMatC: invalid indices: typelevel " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Int] -> String
forall a. Show a => a -> String
show (NonEmpty Pos -> [Int]
forall (t :: * -> *). Foldable t => t Pos -> [Int]
fromPositives NonEmpty Pos
ns) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" /= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Int] -> String
forall a. Show a => a -> String
show (NonEmpty Pos -> [Int]
forall (t :: * -> *). Foldable t => t Pos -> [Int]
fromPositives NonEmpty Pos
ps)

-- | create a FinMat using a relative type level index
toFinMatFromPos :: forall (i :: Nat) ns. (NS ns, i <! ProductT ns) => FinMat ns
toFinMatFromPos :: FinMat ns
toFinMatFromPos = Int -> NonEmpty Pos -> FinMat ns
forall (ns :: [Nat]).
(HasCallStack, NS ns) =>
Int -> NonEmpty Pos -> FinMat ns
FinMatU (KnownNat i => Int
forall (n :: Nat). KnownNat n => Int
TP.pnat @i) (NS ns => NonEmpty Pos
forall (ns :: [Nat]). NS ns => NonEmpty Pos
fromNSP @ns)

-- | convenience function for conversion from 'Int' to 'FinMat'
finMat :: forall ns. NS ns => Int -> Either String (FinMat ns)
finMat :: Int -> Either String (FinMat ns)
finMat Int
i = Int -> NonEmpty Pos -> Either String (FinMat ns)
forall (ns :: [Nat]).
NS ns =>
Int -> NonEmpty Pos -> Either String (FinMat ns)
mkFinMatC Int
i (NS ns => NonEmpty Pos
forall (ns :: [Nat]). NS ns => NonEmpty Pos
fromNSP @ns)

-- | convert type level indices into a FinMat
class FinMatC is ns where
  finMatC :: FinMat ns

instance GL.TypeError ( 'GL.Text "FinMatC '[] '[]: empty index 'is' and 'ns'") => FinMatC '[] '[] where
  finMatC :: FinMat '[]
finMatC = String -> FinMat '[]
forall a. HasCallStack => String -> a
compileError String
"FinMatC '[] '[]: finMatC"
instance GL.TypeError ( 'GL.Text "FinMatC '[] (n ': ns): empty index 'is'") => FinMatC '[] (n ': ns) where
  finMatC :: FinMat (n : ns)
finMatC = String -> FinMat (n : ns)
forall a. HasCallStack => String -> a
compileError String
"FinMatC '[] (n ': ns): finMatC"
instance GL.TypeError ( 'GL.Text "FinMatC (i ': is) '[]: empty index 'ns'") => FinMatC (i ': is) '[] where
  finMatC :: FinMat '[]
finMatC = String -> FinMat '[]
forall a. HasCallStack => String -> a
compileError String
"FinMatC (i ': is) '[]: finMatC"

instance (is' ~ (i ': is), ns' ~ (n ': ns), NS is', NS ns', FinMatT is' ns' 1 is' ns') => FinMatC (i ': is) (n ': ns) where
  finMatC :: FinMat (n : ns)
finMatC = Either String (FinMat (n : ns)) -> FinMat (n : ns)
forall a. HasCallStack => Either String a -> a
frp (Either String (FinMat (n : ns)) -> FinMat (n : ns))
-> Either String (FinMat (n : ns)) -> FinMat (n : ns)
forall a b. (a -> b) -> a -> b
$ NonEmpty Pos -> NonEmpty Pos -> Either String (FinMat (n : ns))
forall (ns :: [Nat]).
NonEmpty Pos -> NonEmpty Pos -> Either String (FinMat ns)
nonEmptyToFinMat' (NS is' => NonEmpty Pos
forall (ns :: [Nat]). NS ns => NonEmpty Pos
fromNSP @is') (NS ns' => NonEmpty Pos
forall (ns :: [Nat]). NS ns => NonEmpty Pos
fromNSP @ns')

type FinMatT :: [Nat] -> [Nat] -> Nat -> [Nat] -> [Nat] -> Constraint
type family FinMatT is0 ns0 ind is ns where
  FinMatT _is0 _ns0 ind '[] (_ ': _) =
    GL.TypeError ( 'GL.Text "FinMatT: empty index 'is' " 'GL.:<>: 'GL.ShowType ind)
  FinMatT _is0 _ns0 ind (_ ': _) '[] =
    GL.TypeError ( 'GL.Text "FinMatT: empty index 'ns' " 'GL.:<>: 'GL.ShowType ind)
  FinMatT _is0 _ns0 ind '[] '[] =
    GL.TypeError ( 'GL.Text "FinMatT: empty index 'is' and 'ns' " 'GL.:<>: 'GL.ShowType ind)
  FinMatT _is0 _ns0 ind '[i] '[n] =
    FinWithMessageC ( 'GL.Text " at index " 'GL.:<>: 'GL.ShowType ind) i n
  FinMatT is0 ns0 ind (i ': i' ': is) (n ': n' ': ns) =
    (FinWithMessageC ( 'GL.Text " at index=" 'GL.:<>: 'GL.ShowType ind) i n, FinMatT is0 ns0 (ind GN.+ 1) (i' ': is) (n' ': ns))
  FinMatT is0 ns0 _ind (_ ': _ ': _) '[_] =
    GL.TypeError
      ( 'GL.Text "too many indices: length is > length ns:"
          'GL.:<>: 'GL.Text " found "
          'GL.:<>: 'GL.ShowType (TP.LengthT is0)
          'GL.:<>: 'GL.Text " expected "
          'GL.:<>: 'GL.ShowType (TP.LengthT ns0)
      )
  FinMatT is0 ns0 _ind '[_] (_ ': _ ': _) =
    GL.TypeError
      ( 'GL.Text "not enough indices: length is < length ns: "
          'GL.:<>: 'GL.Text " found "
          'GL.:<>: 'GL.ShowType (TP.LengthT is0)
          'GL.:<>: 'GL.Text " expected "
          'GL.:<>: 'GL.ShowType (TP.LengthT ns0)
      )

-- | convert a FinMat into a list of indices
finMatToNonEmpty :: forall ns. FinMat ns -> NonEmpty Pos
finMatToNonEmpty :: FinMat ns -> NonEmpty Pos
finMatToNonEmpty (FinMat Int
i NonEmpty Pos
ns) = (Int, NonEmpty Pos) -> NonEmpty Pos
forall a b. (a, b) -> b
snd ((Int, NonEmpty Pos) -> NonEmpty Pos)
-> (Int, NonEmpty Pos) -> NonEmpty Pos
forall a b. (a -> b) -> a -> b
$ (Int -> Pos -> (Int, Pos))
-> Int -> NonEmpty Pos -> (Int, NonEmpty Pos)
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
L.mapAccumR Int -> Pos -> (Int, Pos)
divModNextP Int
i NonEmpty Pos
ns

-- | try to convert a list of indices into a FinMat
nonEmptyToFinMat :: forall ns. NS ns => NonEmpty Pos -> Either String (FinMat ns)
nonEmptyToFinMat :: NonEmpty Pos -> Either String (FinMat ns)
nonEmptyToFinMat NonEmpty Pos
is = NonEmpty Pos -> NonEmpty Pos -> Either String (FinMat ns)
forall (ns :: [Nat]).
NonEmpty Pos -> NonEmpty Pos -> Either String (FinMat ns)
nonEmptyToFinMat' NonEmpty Pos
is (NS ns => NonEmpty Pos
forall (ns :: [Nat]). NS ns => NonEmpty Pos
fromNSP @ns)

-- | try to convert a list of indices into a FinMat
nonEmptyToFinMat' :: NonEmpty Pos -> NonEmpty Pos -> Either String (FinMat ns)
nonEmptyToFinMat' :: NonEmpty Pos -> NonEmpty Pos -> Either String (FinMat ns)
nonEmptyToFinMat' NonEmpty Pos
is NonEmpty Pos
ns =
  String -> Either String (FinMat ns) -> Either String (FinMat ns)
forall a. String -> Either String a -> Either String a
lmsg String
"nonEmptyToFinMat" (Either String (FinMat ns) -> Either String (FinMat ns))
-> Either String (FinMat ns) -> Either String (FinMat ns)
forall a b. (a -> b) -> a -> b
$
    let (NonEmpty (Either String (Pos, Pos))
lrs, MLR Pos Pos
mlr) = (Pos -> Pos -> Either String (Pos, Pos))
-> NonEmpty Pos
-> NonEmpty Pos
-> (NonEmpty (Either String (Pos, Pos)), MLR Pos Pos)
forall a b c.
(a -> b -> c) -> NonEmpty a -> NonEmpty b -> (NonEmpty c, MLR a b)
zipWithExtras1 Pos -> Pos -> Either String (Pos, Pos)
g NonEmpty Pos
is NonEmpty Pos
ns
        g :: Pos -> Pos -> Either String (Pos, Pos)
        g :: Pos -> Pos -> Either String (Pos, Pos)
g Pos
x Pos
y =
          if Pos
x Pos -> Pos -> Bool
forall a. Ord a => a -> a -> Bool
<= Pos
y
            then (Pos, Pos) -> Either String (Pos, Pos)
forall a b. b -> Either a b
Right (Pos
x, Pos
y)
            else String -> Either String (Pos, Pos)
forall a b. a -> Either a b
Left (String -> Either String (Pos, Pos))
-> String -> Either String (Pos, Pos)
forall a b. (a -> b) -> a -> b
$ String
"outofbounds " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Pos, Pos) -> String
forall a. Show a => a -> String
show (Pos
x, Pos
y)
     in case MLR Pos Pos
mlr of
          MLR Pos Pos
MLREqual -> case NonEmpty (Either String (Pos, Pos))
-> These (NonEmpty String) (NonEmpty (Pos, Pos))
forall a b.
NonEmpty (Either a b) -> These (NonEmpty a) (NonEmpty b)
partitionEithersNE NonEmpty (Either String (Pos, Pos))
lrs of
            That NonEmpty (Pos, Pos)
xys -> FinMat ns -> Either String (FinMat ns)
forall a b. b -> Either a b
Right (FinMat ns -> Either String (FinMat ns))
-> FinMat ns -> Either String (FinMat ns)
forall a b. (a -> b) -> a -> b
$ Either String (FinMat ns) -> FinMat ns
forall a. HasCallStack => Either String a -> a
frp (Either String (FinMat ns) -> FinMat ns)
-> Either String (FinMat ns) -> FinMat ns
forall a b. (a -> b) -> a -> b
$ Int -> NonEmpty Pos -> Either String (FinMat ns)
forall (ns :: [Nat]).
Int -> NonEmpty Pos -> Either String (FinMat ns)
mkFinMat ((Pos, Int) -> Int
forall a b. (a, b) -> b
snd ((Pos, Int) -> Int) -> (Pos, Int) -> Int
forall a b. (a -> b) -> a -> b
$ NonEmpty (Pos, Pos) -> (Pos, Int)
forall (t :: * -> *). Foldable1 t => t (Pos, Pos) -> (Pos, Int)
relPos NonEmpty (Pos, Pos)
xys) NonEmpty Pos
ns
            This NonEmpty String
es -> String -> Either String (FinMat ns)
forall a b. a -> Either a b
Left (String -> Either String (FinMat ns))
-> String -> Either String (FinMat ns)
forall a b. (a -> b) -> a -> b
$ String
"This " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
L.intercalate String
"\n" (NonEmpty String -> [String]
forall a. NonEmpty a -> [a]
N.toList NonEmpty String
es)
            These NonEmpty String
es NonEmpty (Pos, Pos)
as -> String -> Either String (FinMat ns)
forall a b. a -> Either a b
Left (String -> Either String (FinMat ns))
-> String -> Either String (FinMat ns)
forall a b. (a -> b) -> a -> b
$ String
"These es=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
L.intercalate String
"\n" (NonEmpty String -> [String]
forall a. NonEmpty a -> [a]
N.toList NonEmpty String
es) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" as=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ NonEmpty (Pos, Pos) -> String
forall a. Show a => a -> String
show NonEmpty (Pos, Pos)
as
          MLRLeft{} -> String -> Either String (FinMat ns)
forall a b. a -> Either a b
Left (String -> Either String (FinMat ns))
-> String -> Either String (FinMat ns)
forall a b. (a -> b) -> a -> b
$ String
"too many indices: expected " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Pos -> Int
unP (NonEmpty Pos -> Pos
forall (t :: * -> *) a. Foldable1 t => t a -> Pos
lengthP NonEmpty Pos
ns)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ NonEmpty Pos -> String
forall a. Show a => a -> String
show NonEmpty Pos
is String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ns=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ NonEmpty Pos -> String
forall a. Show a => a -> String
show NonEmpty Pos
ns
          MLRRight{} -> String -> Either String (FinMat ns)
forall a b. a -> Either a b
Left (String -> Either String (FinMat ns))
-> String -> Either String (FinMat ns)
forall a b. (a -> b) -> a -> b
$ String
"not enough indices: expected " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Pos -> Int
unP (NonEmpty Pos -> Pos
forall (t :: * -> *) a. Foldable1 t => t a -> Pos
lengthP NonEmpty Pos
ns)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ NonEmpty Pos -> String
forall a. Show a => a -> String
show NonEmpty Pos
is String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ns=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ NonEmpty Pos -> String
forall a. Show a => a -> String
show NonEmpty Pos
ns

-- | find the relative position in a matrix index
relPos :: Foldable1 t => t (Pos, Pos) -> (Pos, Int)
relPos :: t (Pos, Pos) -> (Pos, Int)
relPos t (Pos, Pos)
xys =
  let ret :: (Pos, Int)
ret@(Pos Int
a, Int
b) = ((Pos, Pos) -> (Pos, Int) -> (Pos, Int))
-> (Pos, Int) -> t (Pos, Pos) -> (Pos, Int)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Pos Int
x, Pos
y) (Pos
z, Int
tot) -> (Pos
z Pos -> Pos -> Pos
*! Pos
y, (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Int -> Int -> Int
forall a. Num a => a -> a -> a
* Pos -> Int
unP Pos
z Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
tot)) (Pos
_1P, Int
0) t (Pos, Pos)
xys
   in if Int
b Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
a
        then String -> (Pos, Int)
forall a. HasCallStack => String -> a
programmError (String -> (Pos, Int)) -> String -> (Pos, Int)
forall a b. (a -> b) -> a -> b
$ String
"relPos " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Pos, Int) -> String
forall a. Show a => a -> String
show (Pos, Int)
ret
        else (Pos, Int)
ret

instance NS ns => Monoid (FinMat ns) where
  mempty :: FinMat ns
mempty = FinMat ns
forall a. Bounded a => a
minBound

instance Semigroup (FinMat ns) where
  <> :: FinMat ns -> FinMat ns -> FinMat ns
(<>) = FinMat ns -> FinMat ns -> FinMat ns
forall a. Ord a => a -> a -> a
max

instance NS ns => Num (FinMat ns) where
  + :: FinMat ns -> FinMat ns -> FinMat ns
(+) = String -> Either String (FinMat ns) -> FinMat ns
forall a. HasCallStack => String -> Either String a -> a
forceRight String
"(+)" (Either String (FinMat ns) -> FinMat ns)
-> (FinMat ns -> FinMat ns -> Either String (FinMat ns))
-> FinMat ns
-> FinMat ns
-> FinMat ns
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
.@ (Integer -> Integer -> Integer)
-> FinMat ns -> FinMat ns -> Either String (FinMat ns)
forall a.
Num1 a =>
(Integer -> Integer -> Integer) -> a -> a -> Either String a
withOp2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+)
  (-) = String -> Either String (FinMat ns) -> FinMat ns
forall a. HasCallStack => String -> Either String a -> a
forceRight String
"(-)" (Either String (FinMat ns) -> FinMat ns)
-> (FinMat ns -> FinMat ns -> Either String (FinMat ns))
-> FinMat ns
-> FinMat ns
-> FinMat ns
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
.@ (Integer -> Integer -> Integer)
-> FinMat ns -> FinMat ns -> Either String (FinMat ns)
forall a.
Num1 a =>
(Integer -> Integer -> Integer) -> a -> a -> Either String a
withOp2 (-)
  * :: FinMat ns -> FinMat ns -> FinMat ns
(*) = String -> Either String (FinMat ns) -> FinMat ns
forall a. HasCallStack => String -> Either String a -> a
forceRight String
"(*)" (Either String (FinMat ns) -> FinMat ns)
-> (FinMat ns -> FinMat ns -> Either String (FinMat ns))
-> FinMat ns
-> FinMat ns
-> FinMat ns
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
.@ (Integer -> Integer -> Integer)
-> FinMat ns -> FinMat ns -> Either String (FinMat ns)
forall a.
Num1 a =>
(Integer -> Integer -> Integer) -> a -> a -> Either String a
withOp2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(*)
  abs :: FinMat ns -> FinMat ns
abs = FinMat ns -> FinMat ns
forall a. a -> a
id
  signum :: FinMat ns -> FinMat ns
signum (FinMat Int
i NonEmpty Pos
ns) = Int -> NonEmpty Pos -> FinMat ns
forall (ns :: [Nat]).
(HasCallStack, NS ns) =>
Int -> NonEmpty Pos -> FinMat ns
FinMatU (Int -> Int
forall a. Num a => a -> a
signum Int
i) NonEmpty Pos
ns
  negate :: FinMat ns -> FinMat ns
negate = String -> FinMat ns -> FinMat ns
forall a. HasCallStack => String -> a
normalError String
"Num (FinMat ns):negate is undefined"
  fromInteger :: Integer -> FinMat ns
fromInteger Integer
i = String -> Either String (FinMat ns) -> FinMat ns
forall a. HasCallStack => String -> Either String a -> a
forceRight String
"Num (FinMat ns):fromInteger" (Either String (FinMat ns) -> FinMat ns)
-> Either String (FinMat ns) -> FinMat ns
forall a b. (a -> b) -> a -> b
$ do
    if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0
      then String -> Either String (FinMat ns)
forall a b. a -> Either a b
Left String
"undefined for negative numbers"
      else do
        Int
ii <- Integer -> Either String Int
integerToIntSafe Integer
i
        Int -> NonEmpty Pos -> Either String (FinMat ns)
forall (ns :: [Nat]).
NS ns =>
Int -> NonEmpty Pos -> Either String (FinMat ns)
mkFinMatC Int
ii (NS ns => NonEmpty Pos
forall (ns :: [Nat]). NS ns => NonEmpty Pos
fromNSP @ns)

instance NS ns => Num1 (FinMat ns) where
  fromInteger1 :: FinMat ns -> Integer -> Either String (FinMat ns)
fromInteger1 (FinMat Int
_ NonEmpty Pos
ns) Integer
i = do
    Int
ii <- Integer -> Either String Int
integerToIntSafe Integer
i
    Int -> NonEmpty Pos -> Either String (FinMat ns)
forall (ns :: [Nat]).
NS ns =>
Int -> NonEmpty Pos -> Either String (FinMat ns)
mkFinMatC Int
ii NonEmpty Pos
ns

instance NS ns => Enum (FinMat ns) where
  toEnum :: Int -> FinMat ns
toEnum = String -> Either String (FinMat ns) -> FinMat ns
forall a. HasCallStack => String -> Either String a -> a
forceRight String
"Enum(FinMat ns):toEnum" (Either String (FinMat ns) -> FinMat ns)
-> (Int -> Either String (FinMat ns)) -> Int -> FinMat ns
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> NonEmpty Pos -> Either String (FinMat ns))
-> NonEmpty Pos -> Int -> Either String (FinMat ns)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> NonEmpty Pos -> Either String (FinMat ns)
forall (ns :: [Nat]).
NS ns =>
Int -> NonEmpty Pos -> Either String (FinMat ns)
mkFinMatC (NS ns => NonEmpty Pos
forall (ns :: [Nat]). NS ns => NonEmpty Pos
fromNSP @ns)
  fromEnum :: FinMat ns -> Int
fromEnum = FinMat ns -> Int
forall (ns :: [Nat]). FinMat ns -> Int
fmPos
  enumFrom :: FinMat ns -> [FinMat ns]
enumFrom = FinMat ns -> [FinMat ns]
forall a. (Enum a, Bounded a) => a -> [a]
boundedEnumFrom
  enumFromThen :: FinMat ns -> FinMat ns -> [FinMat ns]
enumFromThen = FinMat ns -> FinMat ns -> [FinMat ns]
forall a. (Enum a, Bounded a) => a -> a -> [a]
boundedEnumFromThen

instance NS ns => Bounded (FinMat ns) where
  minBound :: FinMat ns
minBound = Int -> NonEmpty Pos -> FinMat ns
forall (ns :: [Nat]).
(HasCallStack, NS ns) =>
Int -> NonEmpty Pos -> FinMat ns
FinMatU Int
0 (NS ns => NonEmpty Pos
forall (ns :: [Nat]). NS ns => NonEmpty Pos
fromNSP @ns)
  maxBound :: FinMat ns
maxBound = Int -> NonEmpty Pos -> FinMat ns
forall (ns :: [Nat]).
(HasCallStack, NS ns) =>
Int -> NonEmpty Pos -> FinMat ns
FinMatU (Pos -> Int
unP (NS ns => Pos
forall (ns :: [Nat]). NS ns => Pos
fromNSTotalP @ns) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (NS ns => NonEmpty Pos
forall (ns :: [Nat]). NS ns => NonEmpty Pos
fromNSP @ns)

instance NS ns => Read (FinMat ns) where
  readPrec :: ReadPrec (FinMat ns)
readPrec = (Int -> ReadP (FinMat ns)) -> ReadPrec (FinMat ns)
forall a. (Int -> ReadP a) -> ReadPrec a
PC.readP_to_Prec (ReadP (FinMat ns) -> Int -> ReadP (FinMat ns)
forall a b. a -> b -> a
const ReadP (FinMat ns)
forall (ns :: [Nat]). NS ns => ReadP (FinMat ns)
readFinMatP)

-- | reader for 'FinMat'
readFinMat :: NS ns => ReadS (FinMat ns)
readFinMat :: ReadS (FinMat ns)
readFinMat = ReadP (FinMat ns) -> ReadS (FinMat ns)
forall a. ReadP a -> ReadS a
P.readP_to_S ReadP (FinMat ns)
forall (ns :: [Nat]). NS ns => ReadP (FinMat ns)
readFinMatP

-- | reader for 'showFin'
readFinMatP :: forall ns. NS ns => P.ReadP (FinMat ns)
readFinMatP :: ReadP (FinMat ns)
readFinMatP = do
  ReadP ()
P.skipSpaces
  String
_ <- String -> ReadP String
P.string String
"FinMat@"
  (Int
i, NonEmpty Pos
ns) <- (,) (Int -> NonEmpty Pos -> (Int, NonEmpty Pos))
-> ReadP Int -> ReadP (NonEmpty Pos -> (Int, NonEmpty Pos))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReadP Int
pInt ReadP (NonEmpty Pos -> (Int, NonEmpty Pos))
-> ReadP (NonEmpty Pos) -> ReadP (Int, NonEmpty Pos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Char -> Char -> ReadP (NonEmpty Pos)
pPositives Char
'{' Char
'}'
  (String -> ReadP (FinMat ns))
-> (FinMat ns -> ReadP (FinMat ns))
-> Either String (FinMat ns)
-> ReadP (FinMat ns)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (ReadP (FinMat ns) -> String -> ReadP (FinMat ns)
forall a b. a -> b -> a
const ReadP (FinMat ns)
forall a. ReadP a
P.pfail) FinMat ns -> ReadP (FinMat ns)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either String (FinMat ns) -> ReadP (FinMat ns))
-> Either String (FinMat ns) -> ReadP (FinMat ns)
forall a b. (a -> b) -> a -> b
$ Int -> NonEmpty Pos -> Either String (FinMat ns)
forall (ns :: [Nat]).
NS ns =>
Int -> NonEmpty Pos -> Either String (FinMat ns)
mkFinMatC @ns Int
i NonEmpty Pos
ns

neToString :: NonEmpty Pos -> String
neToString :: NonEmpty Pos -> String
neToString = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
L.intercalate String
"," ([String] -> String)
-> (NonEmpty Pos -> [String]) -> NonEmpty Pos -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
forall a. Show a => a -> String
show ([Int] -> [String])
-> (NonEmpty Pos -> [Int]) -> NonEmpty Pos -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty Pos -> [Int]
forall (t :: * -> *). Foldable t => t Pos -> [Int]
fromPositives

-- | pretty print FinMat
showFinMat :: FinMat ns -> String
showFinMat :: FinMat ns -> String
showFinMat (FinMat Int
i NonEmpty Pos
ns) =
  String
"FinMat@" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ NonEmpty Pos -> String
neToString NonEmpty Pos
ns String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}"

-- | more detailed pretty print FinMat
showFinMat' :: forall ns. FinMat ns -> String
showFinMat' :: FinMat ns -> String
showFinMat' w :: FinMat ns
w@(FinMat Int
i NonEmpty Pos
ns) =
  String
"FinMat@" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ NonEmpty Pos -> String
neToString (FinMat ns -> NonEmpty Pos
forall (ns :: [Nat]). FinMat ns -> NonEmpty Pos
finMatToNonEmpty FinMat ns
w) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"|" String -> String -> String
forall a. [a] -> [a] -> [a]
++ NonEmpty Pos -> String
neToString NonEmpty Pos
ns String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}"

instance Show (FinMat ns) where
  show :: FinMat ns -> String
show = FinMat ns -> String
forall (ns :: [Nat]). FinMat ns -> String
showFinMat

-- | constrain i within the size of the indices ie "i >= 1 && i <= LengthT ns"
type NSRangeC :: Peano -> [Nat] -> Constraint
class NSRangeC i ns

instance GL.TypeError ( 'GL.Text "NSRangeC '[]: empty indices") => NSRangeC p '[]
instance NSRangeC ( 'S 'Z) (n ': ns)
instance NSRangeC ( 'S i) (m ': ns) => NSRangeC ( 'S ( 'S i)) (n ': m ': ns)
instance
  GL.TypeError ( 'GL.Text "NSRangeC: index is larger than the number of matrix indices ns") =>
  NSRangeC ( 'S ( 'S i)) '[n]

instance
  GL.TypeError ( 'GL.Text "NSRangeC: zero is not a valid index: index must be one or greater") =>
  NSRangeC 'Z (n ': ns)

-- | iso that conses out the 'Fin' from 'FinMat'
_finMatCons :: forall n n1 ns . (NS (n1 ': ns), PosC n) => Iso' (FinMat (n ': n1 ': ns)) (Fin n, FinMat (n1 ': ns))
_finMatCons :: Iso' (FinMat (n : n1 : ns)) (Fin n, FinMat (n1 : ns))
_finMatCons = (FinMat (n : n1 : ns) -> (Fin n, FinMat (n1 : ns)))
-> ((Fin n, FinMat (n1 : ns)) -> FinMat (n : n1 : ns))
-> Iso' (FinMat (n : n1 : ns)) (Fin n, FinMat (n1 : ns))
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso FinMat (n : n1 : ns) -> (Fin n, FinMat (n1 : ns))
f (Fin n, FinMat (n1 : ns)) -> FinMat (n : n1 : ns)
g
  where f :: FinMat (n : n1 : ns) -> (Fin n, FinMat (n1 : ns))
f (FinMat Int
is (Pos
_:|[Pos]
ns)) = String
-> Either String (Fin n, FinMat (n1 : ns))
-> (Fin n, FinMat (n1 : ns))
forall a. HasCallStack => String -> Either String a -> a
forceRightP String
"_finMatCons lhs" (Either String (Fin n, FinMat (n1 : ns))
 -> (Fin n, FinMat (n1 : ns)))
-> Either String (Fin n, FinMat (n1 : ns))
-> (Fin n, FinMat (n1 : ns))
forall a b. (a -> b) -> a -> b
$ do
           let (Int
a,Pos Int
b) = Int -> Pos -> (Int, Pos)
divModNextP Int
is ([Pos] -> Pos
forall (t :: * -> *). Foldable t => t Pos -> Pos
productP [Pos]
ns)
           (,) (Fin n -> FinMat (n1 : ns) -> (Fin n, FinMat (n1 : ns)))
-> Either String (Fin n)
-> Either String (FinMat (n1 : ns) -> (Fin n, FinMat (n1 : ns)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Either String (Fin n)
forall (n :: Nat). PosC n => Int -> Either String (Fin n)
fin @n (Int
aInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Either String (FinMat (n1 : ns) -> (Fin n, FinMat (n1 : ns)))
-> Either String (FinMat (n1 : ns))
-> Either String (Fin n, FinMat (n1 : ns))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> Either String (FinMat (n1 : ns))
forall (ns :: [Nat]). NS ns => Int -> Either String (FinMat ns)
finMat @(n1 ': ns) (Int
bInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
        g :: (Fin n, FinMat (n1 : ns)) -> FinMat (n : n1 : ns)
g (Fin (Pos Int
i) Pos
_, FinMat Int
is NonEmpty Pos
ns) = String
-> Either String (FinMat (n : n1 : ns)) -> FinMat (n : n1 : ns)
forall a. HasCallStack => String -> Either String a -> a
forceRightP String
"_finMatCons rhs" (Either String (FinMat (n : n1 : ns)) -> FinMat (n : n1 : ns))
-> Either String (FinMat (n : n1 : ns)) -> FinMat (n : n1 : ns)
forall a b. (a -> b) -> a -> b
$ Int -> Either String (FinMat (n : n1 : ns))
forall (ns :: [Nat]). NS ns => Int -> Either String (FinMat ns)
finMat @(n ': n1 ': ns) (Int
is Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Int -> Int -> Int
forall a. Num a => a -> a -> a
* NonEmpty Pos -> Int
forall (t :: * -> *). Foldable t => t Pos -> Int
productPInt NonEmpty Pos
ns)

-- | a lens for accessing the "i" index in a indices of FinMat
_finMatFin ::
  forall i n ns.
  (PosC i, NSRangeC (NatToPeanoT i) ns) =>
  Lens' (FinMat ns) (Fin n)
_finMatFin :: Lens' (FinMat ns) (Fin n)
_finMatFin = (FinMat ns -> Fin n)
-> (FinMat ns -> Fin n -> FinMat ns) -> Lens' (FinMat ns) (Fin n)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens ((PosC i, NSRangeC (NatToPeanoT i) ns) => FinMat ns -> Fin n
forall (i :: Nat) (n :: Nat) (ns :: [Nat]).
(PosC i, NSRangeC (NatToPeanoT i) ns) =>
FinMat ns -> Fin n
finMatFinGet @i @n @ns) ((PosC i, NSRangeC (NatToPeanoT i) ns) =>
FinMat ns -> Fin n -> FinMat ns
forall (i :: Nat) (n :: Nat) (ns :: [Nat]).
(PosC i, NSRangeC (NatToPeanoT i) ns) =>
FinMat ns -> Fin n -> FinMat ns
finMatFinSet @i @n @ns)

-- | set the 'Fin' at index "i" for the FinMat
finMatFinSet ::
  forall i n ns.
  (PosC i, NSRangeC (NatToPeanoT i) ns) =>
  FinMat ns ->
  Fin n ->
  FinMat ns
finMatFinSet :: FinMat ns -> Fin n -> FinMat ns
finMatFinSet fm :: FinMat ns
fm@(FinMat Int
_ NonEmpty Pos
ns) (Fin Pos
ind Pos
_) = String -> Either String (FinMat ns) -> FinMat ns
forall a. HasCallStack => String -> Either String a -> a
forceRightP String
"finMatFinSet" (Either String (FinMat ns) -> FinMat ns)
-> Either String (FinMat ns) -> FinMat ns
forall a b. (a -> b) -> a -> b
$
  let i :: Pos
i = PosC i => Pos
forall (n :: Nat). PosC n => Pos
fromNP @i
      ps :: NonEmpty Pos
ps = FinMat ns -> NonEmpty Pos
forall (ns :: [Nat]). FinMat ns -> NonEmpty Pos
finMatToNonEmpty FinMat ns
fm
   in case Pos -> Pos -> NonEmpty Pos -> Maybe (NonEmpty Pos)
forall a. Pos -> a -> NonEmpty a -> Maybe (NonEmpty a)
setAt1 Pos
i Pos
ind NonEmpty Pos
ps of
        Maybe (NonEmpty Pos)
Nothing -> String -> Either String (FinMat ns)
forall a b. a -> Either a b
Left (String -> Either String (FinMat ns))
-> String -> Either String (FinMat ns)
forall a b. (a -> b) -> a -> b
$ String
"index out of bounds: index is " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Pos -> String
forall a. Show a => a -> String
show Pos
i
        Just NonEmpty Pos
ps1 -> NonEmpty Pos -> NonEmpty Pos -> Either String (FinMat ns)
forall (ns :: [Nat]).
NonEmpty Pos -> NonEmpty Pos -> Either String (FinMat ns)
nonEmptyToFinMat' NonEmpty Pos
ps1 NonEmpty Pos
ns

{- | get the 'Fin' at index "i" from FinMat
 must rely on FinMat to get "n at index i "which saves us pulling "n" from the typelevel ie we can omit PosC n
-}
finMatFinGet ::
  forall i n ns.
  (PosC i, NSRangeC (NatToPeanoT i) ns) =>
  FinMat ns ->
  Fin n
finMatFinGet :: FinMat ns -> Fin n
finMatFinGet fm :: FinMat ns
fm@(FinMat Int
_ NonEmpty Pos
ns) = String -> Either String (Fin n) -> Fin n
forall a. HasCallStack => String -> Either String a -> a
forceRightP String
"finMatFinGet" (Either String (Fin n) -> Fin n) -> Either String (Fin n) -> Fin n
forall a b. (a -> b) -> a -> b
$
  let i :: Pos
i = PosC i => Pos
forall (n :: Nat). PosC n => Pos
fromNP @i
      ps :: NonEmpty Pos
ps = FinMat ns -> NonEmpty Pos
forall (ns :: [Nat]). FinMat ns -> NonEmpty Pos
finMatToNonEmpty FinMat ns
fm
   in case (Pos -> NonEmpty Pos -> Maybe Pos
forall a. Pos -> NonEmpty a -> Maybe a
at1 Pos
i NonEmpty Pos
ps, Pos -> NonEmpty Pos -> Maybe Pos
forall a. Pos -> NonEmpty a -> Maybe a
at1 Pos
i NonEmpty Pos
ns) of
        (Maybe Pos
Nothing, Maybe Pos
_) -> String -> Either String (Fin n)
forall a b. a -> Either a b
Left String
"invalid index!"
        (Maybe Pos
_, Maybe Pos
Nothing) -> String -> Either String (Fin n)
forall a b. a -> Either a b
Left (String -> Either String (Fin n))
-> String -> Either String (Fin n)
forall a b. (a -> b) -> a -> b
$ String
"FinMat is corrupt: doesnt have the index at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Pos -> String
forall a. Show a => a -> String
show Pos
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ FinMat ns -> String
forall a. Show a => a -> String
show FinMat ns
fm
        (Just Pos
p, Just Pos
n) -> Pos -> Pos -> Either String (Fin n)
forall (n :: Nat). Pos -> Pos -> Either String (Fin n)
mkFin Pos
p Pos
n

-- | lens for index 1
_i1 :: Lens' (FinMat (n ': ns)) (Fin n)
_i1 :: (Fin n -> f (Fin n)) -> FinMat (n : ns) -> f (FinMat (n : ns))
_i1 = forall (n :: Nat) (ns :: [Nat]).
(PosC 1, NSRangeC (NatToPeanoT 1) ns) =>
Lens' (FinMat ns) (Fin n)
forall (i :: Nat) (n :: Nat) (ns :: [Nat]).
(PosC i, NSRangeC (NatToPeanoT i) ns) =>
Lens' (FinMat ns) (Fin n)
_finMatFin @1

-- | lens for index 2
_i2 :: Lens' (FinMat (n1 ': n ': ns)) (Fin n)
_i2 :: (Fin n -> f (Fin n))
-> FinMat (n1 : n : ns) -> f (FinMat (n1 : n : ns))
_i2 = forall (n :: Nat) (ns :: [Nat]).
(PosC 2, NSRangeC (NatToPeanoT 2) ns) =>
Lens' (FinMat ns) (Fin n)
forall (i :: Nat) (n :: Nat) (ns :: [Nat]).
(PosC i, NSRangeC (NatToPeanoT i) ns) =>
Lens' (FinMat ns) (Fin n)
_finMatFin @2

-- | lens for index 3
_i3 :: Lens' (FinMat (n1 ': n2 ': n ': ns)) (Fin n)
_i3 :: (Fin n -> f (Fin n))
-> FinMat (n1 : n2 : n : ns) -> f (FinMat (n1 : n2 : n : ns))
_i3 = forall (n :: Nat) (ns :: [Nat]).
(PosC 3, NSRangeC (NatToPeanoT 3) ns) =>
Lens' (FinMat ns) (Fin n)
forall (i :: Nat) (n :: Nat) (ns :: [Nat]).
(PosC i, NSRangeC (NatToPeanoT i) ns) =>
Lens' (FinMat ns) (Fin n)
_finMatFin @3

-- | lens for index 4
_i4 :: Lens' (FinMat (n1 ': n2 ': n3 ': n ': ns)) (Fin n)
_i4 :: (Fin n -> f (Fin n))
-> FinMat (n1 : n2 : n3 : n : ns)
-> f (FinMat (n1 : n2 : n3 : n : ns))
_i4 = forall (n :: Nat) (ns :: [Nat]).
(PosC 4, NSRangeC (NatToPeanoT 4) ns) =>
Lens' (FinMat ns) (Fin n)
forall (i :: Nat) (n :: Nat) (ns :: [Nat]).
(PosC i, NSRangeC (NatToPeanoT i) ns) =>
Lens' (FinMat ns) (Fin n)
_finMatFin @4

-- | lens for index 5
_i5 :: Lens' (FinMat (n1 ': n2 ': n3 ': n4 ': n ': ns)) (Fin n)
_i5 :: (Fin n -> f (Fin n))
-> FinMat (n1 : n2 : n3 : n4 : n : ns)
-> f (FinMat (n1 : n2 : n3 : n4 : n : ns))
_i5 = forall (n :: Nat) (ns :: [Nat]).
(PosC 5, NSRangeC (NatToPeanoT 5) ns) =>
Lens' (FinMat ns) (Fin n)
forall (i :: Nat) (n :: Nat) (ns :: [Nat]).
(PosC i, NSRangeC (NatToPeanoT i) ns) =>
Lens' (FinMat ns) (Fin n)
_finMatFin @5

-- | lens for index 6
_i6 :: Lens' (FinMat (n1 ': n2 ': n3 ': n4 ': n5 ': n ': ns)) (Fin n)
_i6 :: (Fin n -> f (Fin n))
-> FinMat (n1 : n2 : n3 : n4 : n5 : n : ns)
-> f (FinMat (n1 : n2 : n3 : n4 : n5 : n : ns))
_i6 = forall (n :: Nat) (ns :: [Nat]).
(PosC 6, NSRangeC (NatToPeanoT 6) ns) =>
Lens' (FinMat ns) (Fin n)
forall (i :: Nat) (n :: Nat) (ns :: [Nat]).
(PosC i, NSRangeC (NatToPeanoT i) ns) =>
Lens' (FinMat ns) (Fin n)
_finMatFin @6

-- | lens for index 7
_i7 :: Lens' (FinMat (n1 ': n2 ': n3 ': n4 ': n5 ': n6 ': n ': ns)) (Fin n)
_i7 :: (Fin n -> f (Fin n))
-> FinMat (n1 : n2 : n3 : n4 : n5 : n6 : n : ns)
-> f (FinMat (n1 : n2 : n3 : n4 : n5 : n6 : n : ns))
_i7 = forall (n :: Nat) (ns :: [Nat]).
(PosC 7, NSRangeC (NatToPeanoT 7) ns) =>
Lens' (FinMat ns) (Fin n)
forall (i :: Nat) (n :: Nat) (ns :: [Nat]).
(PosC i, NSRangeC (NatToPeanoT i) ns) =>
Lens' (FinMat ns) (Fin n)
_finMatFin @7

-- | lens for index 8
_i8 :: Lens' (FinMat (n1 ': n2 ': n3 ': n4 ': n5 ': n6 ': n7 ': n ': ns)) (Fin n)
_i8 :: (Fin n -> f (Fin n))
-> FinMat (n1 : n2 : n3 : n4 : n5 : n6 : n7 : n : ns)
-> f (FinMat (n1 : n2 : n3 : n4 : n5 : n6 : n7 : n : ns))
_i8 = forall (n :: Nat) (ns :: [Nat]).
(PosC 8, NSRangeC (NatToPeanoT 8) ns) =>
Lens' (FinMat ns) (Fin n)
forall (i :: Nat) (n :: Nat) (ns :: [Nat]).
(PosC i, NSRangeC (NatToPeanoT i) ns) =>
Lens' (FinMat ns) (Fin n)
_finMatFin @8

-- | lens for index 9
_i9 :: Lens' (FinMat (n1 ': n2 ': n3 ': n4 ': n5 ': n6 ': n7 ': n8 ': n ': ns)) (Fin n)
_i9 :: (Fin n -> f (Fin n))
-> FinMat (n1 : n2 : n3 : n4 : n5 : n6 : n7 : n8 : n : ns)
-> f (FinMat (n1 : n2 : n3 : n4 : n5 : n6 : n7 : n8 : n : ns))
_i9 = forall (n :: Nat) (ns :: [Nat]).
(PosC 9, NSRangeC (NatToPeanoT 9) ns) =>
Lens' (FinMat ns) (Fin n)
forall (i :: Nat) (n :: Nat) (ns :: [Nat]).
(PosC i, NSRangeC (NatToPeanoT i) ns) =>
Lens' (FinMat ns) (Fin n)
_finMatFin @9

-- | lens for index 10
_i10 :: Lens' (FinMat (n1 ': n2 ': n3 ': n4 ': n5 ': n6 ': n7 ': n8 ': n9 ': n ': ns)) (Fin n)
_i10 :: (Fin n -> f (Fin n))
-> FinMat (n1 : n2 : n3 : n4 : n5 : n6 : n7 : n8 : n9 : n : ns)
-> f (FinMat (n1 : n2 : n3 : n4 : n5 : n6 : n7 : n8 : n9 : n : ns))
_i10 = forall (n :: Nat) (ns :: [Nat]).
(PosC 10, NSRangeC (NatToPeanoT 10) ns) =>
Lens' (FinMat ns) (Fin n)
forall (i :: Nat) (n :: Nat) (ns :: [Nat]).
(PosC i, NSRangeC (NatToPeanoT i) ns) =>
Lens' (FinMat ns) (Fin n)
_finMatFin @10