cybus 0.2.0.0 → 0.3.0.0

raw patch · 10 files changed

+660/−395 lines, 10 filesdep −pretty-simpledep ~posdep ~primusPVP ok

version bump matches the API change (PVP)

Dependencies removed: pretty-simple

Dependency ranges changed: pos, primus

API changes (from Hackage documentation)

Files

• app/Main.hs +29/−6
• cybus.cabal +7/−8
• src/Cybus/Fin.hs +49/−48
• src/Cybus/FinMat.hs +29/−18
• src/Cybus/Mat.hs +265/−203
• src/Cybus/NatHelper.hs +32/−16
• test/TestFin.hs +4/−4
• test/TestFinMat.hs +37/−27
• test/TestMat.hs +207/−64
• test/TestNatHelper.hs +1/−1

@@ -1,14 +1,17 @@+{-# LANGUAGE GADTs #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeOperators #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TypeApplications #-}  module Main where --import Data.List.NonEmpty (NonEmpty(..)) --import qualified Data.List.NonEmpty as N+import qualified GHC.TypeNats as GN import Cybus  main :: IO ()-main = putStr $ show $ mm @(NN 234)+main = putStr $ show $ mm @'[2,3,4]  tst1 :: Mat '[4,5,3] Int tst1 = gen id@@ -21,22 +24,42 @@  tst4 :: Mat2 4 7 Int tst4 = mat2 @4 @3 [1..] `multMat` mat2 @3 @7 [1..]++tst5 :: Mat (2 ': ns) a -> Mat (1 ': ns) a+tst5 = deleteRow @2++tst6 :: FinC 1 (1 GN.+ n) => Mat (1 GN.+ n ': ns) a -> Mat (n ': ns) a+tst6 = deleteRow @1+ {-->tst3 (mm @234)-Mat@[2]-[Mat@[3,4]+>tst3 (mm @'[2,3,4])+Vec@2 [Mat2@(3,4)   [      [1,2,3,4],      [5,6,7,8],      [9,10,11,12]   ]-,Mat@[3,4]+,Mat2@(3,4)   [      [13,14,15,16],      [17,18,19,20],      [21,22,23,24]   ] ]+it :: Mat '[2] (Mat '[3, 4] Int) -it :: Mat '[2] (Mat '[3,4] Int)+>tst6 (mm @'[9,3])+Mat2@(8,3)+  [+     [4,5,6],+     [7,8,9],+     [10,11,12],+     [13,14,15],+     [16,17,18],+     [19,20,21],+     [22,23,24],+     [25,26,27]+  ]++it :: Mat '[8, 3] Int -}

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           cybus-version:        0.2.0.0+version:        0.3.0.0 synopsis:       multi-dimensional arrays description:    A library for typesafe multi-dimensional arrays . Please see the README on GitHub at <https://github.com/gbwey/cybus#readme> category:       Data, Containers@@ -41,8 +41,8 @@     , distributive     , indexed-traversable     , mtl-    , pos >=0.2.0.0-    , primus >=0.2.0.0+    , pos >=0.3.0.0+    , primus >=0.3.0.0     , profunctors     , semigroupoids     , these@@ -65,8 +65,8 @@     , distributive     , indexed-traversable     , mtl-    , pos >=0.2.0.0-    , primus >=0.2.0.0+    , pos >=0.3.0.0+    , primus >=0.3.0.0     , profunctors     , semigroupoids     , these@@ -99,9 +99,8 @@     , indexed-traversable     , lens     , mtl-    , pos >=0.2.0.0-    , pretty-simple-    , primus >=0.2.0.0+    , pos >=0.3.0.0+    , primus >=0.3.0.0     , profunctors     , semigroupoids     , tasty

@@ -32,9 +32,8 @@   fnN,   pattern Fin,   pattern FinU,-  FinT,-  FinWithMessageT,-  finC,+  FinC (..),+  FinWithMessageC,    -- * read/show methods   showFin,@@ -113,17 +112,17 @@  {-# COMPLETE FinU #-} --- | pattern synonym for validating the fin before construction with a PosT constraint for validating at the typelevel+-- | pattern synonym for validating the fin before construction with a PosC constraint for validating at the typelevel pattern FinU ::   forall (n :: Nat).-  (HasCallStack, PosT n) =>+  (HasCallStack, PosC n) =>   Pos ->   Pos ->   Fin n pattern FinU i n <-   Fin' i n   where-    FinU = frp .@ mkFinC -- dont change this: frp is good else breaking the system+    FinU = frp .@ mkFinC  -- | create a 'Fin' value level "i" and "n" values and validate that "i" is in range mkFin :: Pos -> Pos -> Either String (Fin n)@@ -133,7 +132,7 @@     else Left $ show p ++ " is too large: maximum is " ++ show n  -- | create a 'Fin' value level "i" and "n" values and validate against expected "n"-mkFinC :: forall n. PosT n => Pos -> Pos -> Either String (Fin n)+mkFinC :: forall n. PosC n => Pos -> Pos -> Either String (Fin n) mkFinC p n = do   let n' = fromNP @n   if n == n'@@ -141,21 +140,21 @@     else Left $ "mkFinC: " ++ show n ++ " /= " ++ show n' ++ " at typelevel"  -- | convenience function for conversion from 'Int' to 'Fin'-fin :: PosT n => Int -> Either String (Fin n)+fin :: PosC n => Int -> Either String (Fin n) fin = finP <=< eitherPos  -- | convenience function for conversion from 'Pos' to 'Fin'-finP :: forall n. PosT n => Pos -> Either String (Fin n)+finP :: forall n. PosC n => Pos -> Either String (Fin n) finP = flip mkFinC (fromNP @n) -instance PosT n => Monoid (Fin n) where+instance PosC n => Monoid (Fin n) where   mempty = minBound  instance Semigroup (Fin n) where   (<>) = max --- PosT only needed for fromInteger-instance PosT n => Num (Fin n) where+-- PosC only needed for fromInteger+instance PosC n => Num (Fin n) where   (+) = forceRight "(+)" .@ withOp2 (+)   (-) = forceRight "(-)" .@ withOp2 (-)   (*) = forceRight "(*)" .@ withOp2 (*)@@ -167,18 +166,18 @@     k <- eitherPos ii     mkFinC k (fromNP @n) -instance PosT n => Num1 (Fin n) where+instance PosC n => Num1 (Fin n) where   signum1 = fmap signum -- have to override as 1 is Fin 2 (there is no zero) -instance PosT n => Enum (Fin n) where+instance PosC n => Enum (Fin n) where   toEnum i = forceRight "Enum(Fin n):toEnum" $ do     p <- eitherPos (i + 1)     mkFinC p (fromNP @n)-  fromEnum = subtract 1 . unP . fnPos -- todo: ok subtract one could be a problem+  fromEnum = subtract 1 . unP . fnPos   enumFrom = boundedEnumFrom   enumFromThen = boundedEnumFromThen -instance PosT n => Bounded (Fin n) where+instance PosC n => Bounded (Fin n) where   minBound = FinU _1P (fromNP @n)   maxBound = FinU (fromNP @n) (fromNP @n) @@ -186,15 +185,15 @@ showFin :: Fin n -> String showFin (Fin (Pos i) (Pos n)) = "Fin" ++ show (i, n) -instance PosT n => Read (Fin n) where+instance PosC n => Read (Fin n) where   readPrec = PC.readP_to_Prec (const readFinP)  -- | reader for 'Fin'-readFin :: PosT n => ReadS (Fin n)+readFin :: PosC n => ReadS (Fin n) readFin = P.readP_to_S readFinP  -- | reader for 'showFin'-readFinP :: forall n. PosT n => P.ReadP (Fin n)+readFinP :: forall n. PosC n => P.ReadP (Fin n) readFinP = do   P.skipSpaces   (i, n) <- P.between (P.string "Fin(") (P.string ")") ((,) <$> pPosInt <* P.char ',' <*> pPosInt)@@ -203,94 +202,96 @@ instance Show (Fin n) where   show = showFin --- | create a 'Fin' using typelevel "i" and "n" Nat-finC :: forall (i :: Nat) (n :: Nat). FinT i n => Fin n-finC = Fin' (fromNP @i) (fromNP @n)+-- | class for constraining "i" to positive numbers less than or equal to "n"+type FinC :: Nat -> Nat -> Constraint+class (PosC i, PosC n) => FinC i n where+  finC :: Fin n --- | type constraint for restricting a 'Nat' to positive numbers-type FinT :: Nat -> Nat -> Constraint-type FinT i n = (i <=! n, PosT n)+instance (PosC n, i <=! n) => FinC i n where+  finC = Fin' (fromNP @i) (fromNP @n) --- | type constraint for restricting a 'Nat' to positive numbers with a custom error message-type FinWithMessageT :: GL.ErrorMessage -> Nat -> Nat -> Constraint-type FinWithMessageT msg i n = (LTEQT msg i n, PosT n)+-- | class for constraining "i" to positive numbers less than or equal to "n" with a custom error message+type FinWithMessageC :: GL.ErrorMessage -> Nat -> Nat -> Constraint+class FinWithMessageC msg i n +instance LTEQT msg i n => FinWithMessageC msg i n+ -- | type synonym for index 1-_F1 :: FinT 1 n => Fin n+_F1 :: FinC 1 n => Fin n _F1 = finC @1  -- | type synonym for index 2-_F2 :: FinT 2 n => Fin n+_F2 :: FinC 2 n => Fin n _F2 = finC @2  -- | type synonym for index 3-_F3 :: FinT 3 n => Fin n+_F3 :: FinC 3 n => Fin n _F3 = finC @3  -- | type synonym for index 4-_F4 :: FinT 4 n => Fin n+_F4 :: FinC 4 n => Fin n _F4 = finC @4  -- | type synonym for index 5-_F5 :: FinT 5 n => Fin n+_F5 :: FinC 5 n => Fin n _F5 = finC @5  -- | type synonym for index 6-_F6 :: FinT 6 n => Fin n+_F6 :: FinC 6 n => Fin n _F6 = finC @6  -- | type synonym for index 7-_F7 :: FinT 7 n => Fin n+_F7 :: FinC 7 n => Fin n _F7 = finC @7  -- | type synonym for index 8-_F8 :: FinT 8 n => Fin n+_F8 :: FinC 8 n => Fin n _F8 = finC @8  -- | type synonym for index 9-_F9 :: FinT 9 n => Fin n+_F9 :: FinC 9 n => Fin n _F9 = finC @9  -- | type synonym for index 10-_F10 :: FinT 10 n => Fin n+_F10 :: FinC 10 n => Fin n _F10 = finC @10  -- | type synonym for index 11-_F11 :: FinT 11 n => Fin n+_F11 :: FinC 11 n => Fin n _F11 = finC @11  -- | type synonym for index 12-_F12 :: FinT 12 n => Fin n+_F12 :: FinC 12 n => Fin n _F12 = finC @12  -- | type synonym for index 13-_F13 :: FinT 13 n => Fin n+_F13 :: FinC 13 n => Fin n _F13 = finC @13  -- | type synonym for index 14-_F14 :: FinT 14 n => Fin n+_F14 :: FinC 14 n => Fin n _F14 = finC @14  -- | type synonym for index 15-_F15 :: FinT 15 n => Fin n+_F15 :: FinC 15 n => Fin n _F15 = finC @15  -- | type synonym for index 16-_F16 :: FinT 16 n => Fin n+_F16 :: FinC 16 n => Fin n _F16 = finC @16  -- | type synonym for index 17-_F17 :: FinT 17 n => Fin n+_F17 :: FinC 17 n => Fin n _F17 = finC @17  -- | type synonym for index 18-_F18 :: FinT 18 n => Fin n+_F18 :: FinC 18 n => Fin n _F18 = finC @18  -- | type synonym for index 19-_F19 :: FinT 19 n => Fin n+_F19 :: FinC 19 n => Fin n _F19 = finC @19  -- | type synonym for index 20-_F20 :: FinT 20 n => Fin n+_F20 :: FinC 20 n => Fin n _F20 = finC @20

@@ -59,6 +59,7 @@   finMatFinGet,    -- * lens into the matrix indices+  _finMatCons,   _finMatFin,   _i1,   _i2,@@ -134,7 +135,7 @@ pattern FinMatU i ps <-   FinMatUnsafe i ps   where-    FinMatU = frp .@ mkFinMatC -- dont change this: frp is necessary else breaking the system+    FinMatU = frp .@ 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)@@ -184,9 +185,9 @@   FinMatT _is0 _ns0 ind '[] '[] =     GL.TypeError ( 'GL.Text "FinMatT: empty index 'is' and 'ns' " 'GL.:<>: 'GL.ShowType ind)   FinMatT _is0 _ns0 ind '[i] '[n] =-    FinWithMessageT ( 'GL.Text " at index " 'GL.:<>: 'GL.ShowType ind) i n+    FinWithMessageC ( 'GL.Text " at index " 'GL.:<>: 'GL.ShowType ind) i n   FinMatT is0 ns0 ind (i ': i' ': is) (n ': n' ': ns) =-    (FinWithMessageT ( 'GL.Text " at index=" 'GL.:<>: 'GL.ShowType ind) i n, FinMatT is0 ns0 (ind GN.+ 1) (i' ': is) (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:"@@ -284,7 +285,8 @@ readFinMatP :: forall ns. NS ns => P.ReadP (FinMat ns) readFinMatP = do   P.skipSpaces-  (i, ns) <- (,) <$> pInt <* P.char '@' <*> pPositives '{' '}'+  _ <- P.string "FinMat@"+  (i, ns) <- (,) <$> pInt <*> pPositives '{' '}'   either (const P.pfail) pure $ mkFinMatC @ns i ns  neToString :: NonEmpty Pos -> String@@ -293,12 +295,12 @@ -- | pretty print FinMat showFinMat :: FinMat ns -> String showFinMat (FinMat i ns) =-  show i ++ "@{" ++ neToString ns ++ "}"+  "FinMat@" ++ show i ++ "{" ++ neToString ns ++ "}"  -- | more detailed pretty print FinMat showFinMat' :: forall ns. FinMat ns -> String showFinMat' w@(FinMat i ns) =-  show i ++ "@{" ++ neToString (finMatToNonEmpty w) ++ "|" ++ neToString ns ++ "}"+  "FinMat@" ++ show i ++ "{" ++ neToString (finMatToNonEmpty w) ++ "|" ++ neToString ns ++ "}"  instance Show (FinMat ns) where   show = showFinMat@@ -307,7 +309,7 @@ type NSRangeC :: Peano -> [Nat] -> Constraint class NSRangeC i ns -instance GL.TypeError ('GL.Text "NSRangeC '[]: empty indices") => NSRangeC p '[]+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@@ -318,42 +320,50 @@   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 f g+  where f (FinMat is (_:|ns)) = forceRightP "_finMatCons lhs" $ do+           let (a,Pos b) = divModNextP is (productP ns)+           (,) <$> fin @n (a+1) <*> finMat @(n1 ': ns) (b-1)+        g (Fin (Pos i) _, FinMat is ns) = forceRightP "_finMatCons rhs" $ finMat @(n ': n1 ': ns) (is + (i-1) * productPInt ns)+ -- | a lens for accessing the "i" index in a indices of FinMat _finMatFin ::   forall i n ns.-  (PosT i, NSRangeC (NatToPeanoT i) ns) =>+  (PosC i, NSRangeC (NatToPeanoT i) ns) =>   Lens' (FinMat ns) (Fin n) _finMatFin = lens (finMatFinGet @i @n @ns) (finMatFinSet @i @n @ns)  -- | set the 'Fin' at index "i" for the FinMat finMatFinSet ::   forall i n ns.-  (PosT i, NSRangeC (NatToPeanoT i) ns) =>+  (PosC i, NSRangeC (NatToPeanoT i) ns) =>   FinMat ns ->   Fin n ->   FinMat ns-finMatFinSet fm@(FinMat _ ns) (Fin ind _) =+finMatFinSet fm@(FinMat _ ns) (Fin ind _) = forceRightP "finMatFinSet" $   let i = fromNP @i       ps = finMatToNonEmpty fm    in case setAt1 i ind ps of-        Nothing -> programmError $ "finMatFinSet: index out of bounds: index is " ++ show i-        Just ps1 -> frp $ nonEmptyToFinMat' ps1 ns+        Nothing -> Left $ "index out of bounds: index is " ++ show i+        Just ps1 -> nonEmptyToFinMat' ps1 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 PosT n+ 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.-  (PosT i, NSRangeC (NatToPeanoT i) ns) =>+  (PosC i, NSRangeC (NatToPeanoT i) ns) =>   FinMat ns ->   Fin n-finMatFinGet fm@(FinMat _ ns) =+finMatFinGet fm@(FinMat _ ns) = forceRightP "finMatFinGet" $   let i = fromNP @i       ps = finMatToNonEmpty fm    in case (at1 i ps, at1 i ns) of-        (Nothing, _) -> programmError "finMatFinGet: invalid index!"-        (_, Nothing) -> programmError $ "finMatFinGet: FinMat is corrupt: doesnt have the index at " ++ show i ++ " " ++ show fm-        (Just p, Just n) -> frp $ mkFin p n+        (Nothing, _) -> Left "invalid index!"+        (_, Nothing) -> Left $ "FinMat is corrupt: doesnt have the index at " ++ show i ++ " " ++ show fm+        (Just p, Just n) -> mkFin p n  -- | lens for index 1 _i1 :: Lens' (FinMat (n ': ns)) (Fin n)@@ -394,3 +404,4 @@ -- | lens for index 10 _i10 :: Lens' (FinMat (n1 ': n2 ': n3 ': n4 ': n5 ': n6 ': n7 ': n8 ': n9 ': n ': ns)) (Fin n) _i10 = _finMatFin @10+

@@ -20,6 +20,7 @@ {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE TupleSections #-}  {- | Module      : Cybus.Mat@@ -109,6 +110,10 @@   cartesian,   pureMat,   replicateMat,+  determinant,+--  determinantL,+--  cofactorsL,+deleteColumnL,    -- * row operations   deleteRow,@@ -159,6 +164,8 @@   concatMat,   redim,   reverseDim,+  rotateLeft,+  rotateRight,    -- * subset and slicing   SliceC (..),@@ -297,6 +304,7 @@ import Primus.Error import Primus.Fold import Primus.Lens+import Primus.List import Primus.NonEmpty import Primus.Num1 import Primus.One@@ -343,7 +351,7 @@ type Mat6 :: Nat -> Nat -> Nat -> Nat -> Nat -> Nat -> Type -> Type type Mat6 n m p q r s = Mat '[n, m, p, q, r, s] --- | convenient type synonym for specifying the dimensions of a matrix using the 'NN' type family+-- | convenient type synonym for specifying the dimensions of a matrix using each digit as a dimension type MatN :: Nat -> Type -> Type type MatN n = Mat (NN n) @@ -369,7 +377,7 @@ pattern MatIU v ps <-   MatUnsafe v ps   where-    MatIU = frp .@ mkMat -- dont change this: frp is needed+    MatIU = frp .@ mkMat  {-# COMPLETE MatU #-} @@ -383,7 +391,7 @@ pattern MatU v ps <-   MatUnsafe v ps   where-    MatU = frp .@ mkMatC -- dont change this: frp is needed+    MatU = frp .@ mkMatC  instance (Bounded a, Enum a) => Num1 (Mat ns a) where   fromInteger1 = toEnumTraversable@@ -425,7 +433,7 @@    in MatU (V.replicate (productPInt ns) a) ns  -- | creates a matrix of first dimension "n" by replicating the input matrix "n" times-replicateMat :: forall n n1 ns a. PosT n => Mat (n1 ': ns) a -> Mat (n ': n1 ': ns) a+replicateMat :: forall n n1 ns a. PosC n => Mat (n1 ': ns) a -> Mat (n ': n1 ': ns) a replicateMat (Mat v ns) =   let n = fromNP @n    in MatIU (V.concat (replicate (unP n) v)) (n N.<| ns)@@ -603,11 +611,11 @@  -- | updates a value in a matrix updateMat :: (a -> a) -> FinMat ns -> Mat ns a -> Mat ns a-updateMat f (FinMat i _) (Mat v ps) =+updateMat f (FinMat i _) (Mat v ps) = forceRightP "updateMat" $ do   let (v1, v2) = V.splitAt i v-   in case V.uncons v2 of-        Just (a, v2') -> MatIU (v1 <> V.cons (f a) v2') ps-        Nothing -> programmError $ "updateMat: i=" ++ show i+  case V.uncons v2 of+        Just (a, v2') -> mkMat (v1 <> V.cons (f a) v2') ps+        Nothing -> Left $ "i=" ++ show i  -- | cons a value with a 1d matrix (.:) :: forall n a a'. a ~ a' => a -> Vec n a' -> Vec (1 GN.+ n) a'@@ -642,19 +650,19 @@ se2 (Mat v ps) = MatIU v (_1P N.<| ps)  -- | create a 1d matrix from a list of values-vec :: forall n a. (HasCallStack, PosT n) => [a] -> Vec n a+vec :: forall n a. (HasCallStack, PosC n) => [a] -> Vec n a vec = mat @'[n]  -- | create a 1d matrix from a list of values with the exact number of elements-vec' :: forall n a. (HasCallStack, PosT n) => [a] -> Vec n a+vec' :: forall n a. (HasCallStack, PosC n) => [a] -> Vec n a vec' = mat' @'[n]  -- | create a 2d matrix from a list of values-mat2 :: forall n m a. (HasCallStack, PosT n, PosT m) => [a] -> Mat2 n m a+mat2 :: forall n m a. (HasCallStack, PosC n, PosC m) => [a] -> Mat2 n m a mat2 = mat @'[n, m]  -- | create a 2d matrix from a list of values with the exact number of elements-mat2' :: forall n m a. (HasCallStack, PosT n, PosT m) => [a] -> Mat2 n m a+mat2' :: forall n m a. (HasCallStack, PosC n, PosC m) => [a] -> Mat2 n m a mat2' = mat' @'[n, m]  -- | map each column@@ -863,61 +871,65 @@ instance n ~ n' => SliceC' '[n'] '[n] where   sliceC' (FinMat i _) (Mat v _) =     case v V.!? i of-      Nothing -> programmError $ "sliceC': index " ++ show i ++ " out of bounds"+      Nothing -> programmError $ "sliceC' '[n] '[n]: index " ++ show i ++ " out of bounds"       Just a -> a-  sliceUpdateC' (FinMat i _) (Mat v ps) b =+  sliceUpdateC' (FinMat i _) (Mat v ps) b = forceRightP "sliceUpdateC' '[n] '[n]" $ do     let (v1, v2) = V.splitAt i v-     in case V.uncons v2 of-          Just (_, v3) -> MatIU (v1 <> V.cons b v3) ps-          Nothing -> programmError $ "sliceUpdateC': index " ++ show i ++ " out of bounds"+    case V.uncons v2 of+          Just (_, v3) -> mkMat (v1 <> V.cons b v3) ps+          Nothing -> Left $ "index " ++ show i ++ " out of bounds" instance n ~ n' => SliceC' '[n'] (n ': m ': ns) where-  sliceC' (FinMat i _) (Mat v (_ :| ps)) =+  sliceC' (FinMat i _) (Mat v (_ :| ps)) = forceRightP "sliceC' '[n] (n ': m ': ns)" $ do     case ps of-      m : ns ->+      m : ns -> do         let ps1 = m :| ns             len1 = productPInt ps1-         in MatIU (V.slice (i * len1) len1 v) ps1-      [] -> programmError $ "sliceC': index " ++ show i ++ ": missing indices"+        mkMat (V.slice (i * len1) len1 v) ps1+      [] -> Left $ "index " ++ show i ++ ": missing indices" -  sliceUpdateC' (FinMat i0 _) (Mat v w@(_ :| ps)) b =+  sliceUpdateC' (FinMat i0 _) (Mat v w@(_ :| ps)) b = forceRightP "sliceUpdateC' '[n] (n ': m ': ns)" $ do     let len = productPInt ps         i = i0 + 1         v1 = V.slice 0 ((i - 1) * len) v         v2 = V.slice (i * len) (productPInt w - i * len) v-     in MatIU (v1 <> mVec b <> v2) w+    mkMat (v1 <> mVec b <> v2) w  instance   (n ~ n', SliceC' (n1' ': ns') (n1 ': ns)) =>   SliceC' (n ': n1' ': ns') (n' ': n1 ': ns)   where-  sliceC' fm@(FinMat _ (_ :| n1ns')) w@(Mat _ (n :| _)) =+  sliceC' fm@(FinMat _ (_ :| n1ns')) w@(Mat _ (n :| _)) = forceRightP "sliceC' (n ': n1' ': ns')" $ do     let x :| xs = finMatToNonEmpty fm         i = unP x - 1-     in case (xs, n1ns') of-          (x1 : x1s, n1 : ns') ->-            let fn1 = frp $ nonEmptyToFinMat' (x1 :| x1s) (n1 :| ns')-             in sliceC' @(n1' ': ns') @(n1 ': ns) fn1 (sliceC' @'[n'] @(n ': n1 ': ns) (frp $ mkFinMat i (n :| [])) w)-          ([], _) -> programmError "sliceC': missing ns' indices"-          (_, []) -> programmError "sliceC': missing ns indices"-  sliceUpdateC' fm@(FinMat _ (_ :| n1ns')) (Mat v w@(_ :| ps0)) b =+    case (xs, n1ns') of+          (x1 : x1s, n1 : ns') -> do+            fn1 <- nonEmptyToFinMat' (x1 :| x1s) (n1 :| ns')+            w1 <- mkFinMat i (n :| [])+            pure $ sliceC' @(n1' ': ns') @(n1 ': ns) fn1 (sliceC' @'[n'] @(n ': n1 ': ns) w1 w)+          ([], _) -> Left "missing ns' indices"+          (_, []) -> Left "missing ns indices"+  sliceUpdateC' fm@(FinMat _ (_ :| n1ns')) (Mat v w@(_ :| ps0)) b = forceRightP "sliceUpdateC' (n ': n1' ': ns')" $ do     -- carve out the piece that is to be updated and pass that down then patch it all back together     let x :| xs = finMatToNonEmpty fm         i = unP x-     in case (ps0, xs, n1ns') of-          (_ : ns, x1 : x1s, n1 : ns') ->-            let fn1 = frp $ nonEmptyToFinMat' (x1 :| x1s) (n1 :| ns')-                ps1 = n1 :| ns+    case (ps0, xs, n1ns') of+          (_ : ns, x1 : x1s, n1 : ns') -> do+            fn1 <- nonEmptyToFinMat' (x1 :| x1s) (n1 :| ns')+            let ps1 = n1 :| ns                 len = productPInt ps1                 v1 = V.slice 0 ((i - 1) * len) v                 v2 = V.slice (i * len) (productPInt w - i * len) v-                m1 = MatIU (V.slice ((i - 1) * len) len v) ps1-                mx = sliceUpdateC' @(n1' ': ns') @(n1 ': ns) fn1 m1 b-             in MatIU (v1 <> mVec mx <> v2) w-          ([], _, _) -> programmError "sliceUpdateC': missing matrix indices"-          (_, [], _) -> programmError "sliceUpdateC': missing ns' indices"-          (_, _, []) -> programmError "sliceUpdateC': missing finmat indices"+            m1 <- mkMat (V.slice ((i - 1) * len) len v) ps1+            let mx = sliceUpdateC' @(n1' ': ns') @(n1 ': ns) fn1 m1 b+            mkMat (v1 <> mVec mx <> v2) w+          ([], _, _) -> Left "missing matrix indices"+          (_, [], _) -> Left "missing ns' indices"+          (_, _, []) -> Left "missing finmat indices" -instance (GL.TypeError ( 'GL.Text "SliceC': too many indices ns': length ns' > length ns")) => SliceC' (n' ': n1' ': ns') '[n] where+instance+  GL.TypeError ( 'GL.Text "SliceC': too many indices ns': length ns' > length ns") =>+  SliceC' (n' ': n1' ': ns') '[n]+  where   sliceC' = compileError "sliceC'"   sliceUpdateC' = compileError "sliceUpdateC'" @@ -999,27 +1011,27 @@   sliceC = compileError "SliceC:sliceC"   sliceUpdateC = compileError "SliceC:sliceUpdateC" -instance FinT i n => SliceC '[i] '[n] where+instance FinC i n => SliceC '[i] '[n] where   sliceC (Mat v _) =     let i = fromN @i - 1      in case v V.!? i of           Nothing -> programmError $ "sliceC: index " ++ show i ++ " out of bounds"           Just a -> a-  sliceUpdateC (Mat v ps) b =+  sliceUpdateC (Mat v ps) b = forceRightP "sliceC' '[i] '[n]" $ do     let i = fromN @i - 1         (v1, v2) = V.splitAt i v-     in case V.uncons v2 of-          Just (_, v3) -> MatIU (v1 <> V.cons b v3) ps-          Nothing -> programmError $ "sliceUpdateC: index " ++ show i ++ " out of bounds"-instance FinT i n => SliceC '[i] (n ': m ': ns) where-  sliceC (Mat v (_ :| ps)) =+    case V.uncons v2 of+          Just (_, v3) -> mkMat (v1 <> V.cons b v3) ps+          Nothing -> Left $ "index " ++ show i ++ " out of bounds"+instance FinC i n => SliceC '[i] (n ': m ': ns) where+  sliceC (Mat v (_ :| ps)) =  forceRightP "sliceC' '[i] (n ': m ': ns)" $ do     case ps of-      m : ns ->+      m : ns -> do         let i = fromN @i - 1             ps1 = m :| ns             len1 = productPInt ps1-         in MatIU (V.slice (i * len1) len1 v) ps1-      [] -> programmError $ "sliceUpdateC: index " ++ show (fromN @i) ++ ": missing indices"+        mkMat (V.slice (i * len1) len1 v) ps1+      [] -> Left $ "index " ++ show (fromN @i) ++ ": missing indices"    sliceUpdateC (Mat v w@(_ :| ps)) b =     let i = fromN @i@@ -1029,26 +1041,29 @@      in MatIU (v1 <> mVec b <> v2) w  instance-  (FinT i n, SliceC (i1 ': is) (n1 ': ns)) =>+  (FinC i n, SliceC (i1 ': is) (n1 ': ns)) =>   SliceC (i ': i1 ': is) (n ': n1 ': ns)   where   sliceC w =     sliceC @(i1 ': is) @(n1 ': ns) (sliceC @'[i] @(n ': n1 ': ns) w)-  sliceUpdateC (Mat v w@(_ :| ps0)) b =+  sliceUpdateC (Mat v w@(_ :| ps0)) b = forceRightP "sliceUpdateC' (i ': i1 ': is) (n ': m ': ns)" $ do     -- carve out the piece that is to be updated and pass that down then patch it all back together     case ps0 of-      n1 : ns ->+      n1 : ns -> do         let i = fromN @i             ps1 = n1 :| ns             len = productPInt ps1             v1 = V.slice 0 ((i - 1) * len) v             v2 = V.slice (i * len) (productPInt w - i * len) v-            m1 = MatIU (V.slice ((i - 1) * len) len v) ps1-            mx = sliceUpdateC @(i1 ': is) @(n1 ': ns) m1 b-         in MatIU (v1 <> mVec mx <> v2) w-      [] -> programmError $ "sliceUpdateC: index " ++ show (fromN @i) ++ ": missing indices"+        m1 <- mkMat (V.slice ((i - 1) * len) len v) ps1+        let mx = sliceUpdateC @(i1 ': is) @(n1 ': ns) m1 b+        mkMat (v1 <> mVec mx <> v2) w+      [] -> Left $ "index " ++ show (fromN @i) ++ ": missing indices" -instance (GL.TypeError ( 'GL.Text "too many indices 'is': length is > length ns")) => SliceC (i ': i1 ': is) '[n] where+instance+  GL.TypeError ( 'GL.Text "too many indices 'is': length is > length ns") =>+  SliceC (i ': i1 ': is) '[n]+  where   sliceC = compileError "sliceC (2)"   sliceUpdateC = compileError "sliceUpdateC (2)" @@ -1062,7 +1077,7 @@ -- | a lens for acccessing a column _col ::   forall (i :: Nat) n m ns a.-  (FinT i m) =>+  (FinC i m) =>   Lens' (Mat (n ': m ': ns) a) (Mat (n ': ns) a) _col = _transposeMat . _row @i @@ -1107,14 +1122,14 @@   forall n m ns a.   Mat (n ': m ': ns) a ->   Vec n (Mat (m ': ns) a)-rows w@(Mat _ (n :| ps)) =+rows w@(Mat _ (n :| ps)) = forceRightP "rows" $   case ps of-    m : ns ->-      let zs = frp $ chunkNVMat (unitsF @[] n) (m :| ns) w-       in MatIU (V.fromList zs) (n :| [])-    [] -> programmError "rows: missing indices"+    m : ns -> do+      zs <- chunkNVMat (unitsF @[] n) (m :| ns) w+      mkMat (V.fromList zs) (n :| [])+    [] -> Left "missing indices" --- | unbust from rows @see 'rows'+-- | unbust from rows see 'rows' unrows ::   forall n m ns a.   Vec n (Mat (m ': ns) a) ->@@ -1183,14 +1198,14 @@   Mat2 n m a ->   Mat2 m p b ->   Mat2 n p d-dot f g w1@(Mat _ (n :| ps1)) w2@(Mat _ (_ :| ps2)) =+dot f g w1@(Mat _ (n :| ps1)) w2@(Mat _ (_ :| ps2)) = forceRightP "dot" $   case (ps1, ps2) of-    ([m], [p]) ->-      let z1 = frp $ chunkNLen1 n m w1-          z2 = N.transpose $ frp $ chunkNLen1 m p w2-          w = liftA2 ((g . frp) .@ zipWithExact f) z1 z2-       in MatIU (V.fromList $ N.toList w) (n :| [p])-    o -> programmError $ "dot: missing indices " ++ show o+    ([m], [p]) -> do+      z1 <- chunkNLen1 n m w1+      z2 <- N.transpose <$> chunkNLen1 m p w2+      w <- sequenceA $ liftA2 (fmap g .@ zipWithExact f) z1 z2+      mkMat (V.fromList $ N.toList w) (n :| [p])+    o -> Left $ "missing indices " ++ show o  -- | multiply two matrices together multMat ::@@ -1204,7 +1219,7 @@ -- | delete a row deleteRow ::   forall (i :: Nat) (n :: Nat) (ns :: [Nat]) a.-  FinT i (1 GN.+ n) =>+  FinC i (1 GN.+ n) =>   Mat (1 GN.+ n ': ns) a ->   Mat (n ': ns) a deleteRow = deleteRow' (finC @i @(1 GN.+ n))@@ -1215,18 +1230,18 @@   Fin (1 GN.+ n) ->   Mat (1 GN.+ n ': ns) a ->   Mat (n ': ns) a-deleteRow' (Fin (Pos i) _) (Mat v (sn :| ps)) =-  let n = frp $ predP sn-      n1 = productPInt ps+deleteRow' (Fin (Pos i) _) (Mat v (sn :| ps)) = forceRightP "deleteRow'" $ do+  n <- predP sn+  let n1 = productPInt ps       s = (i - 1) * n1       v1 = V.slice 0 s v       v2 = V.slice (s + n1) (productPInt (sn :| ps) - s - n1) v-   in MatIU (v1 <> v2) (n :| ps)+  mkMat (v1 <> v2) (n :| ps)  -- | delete a row from a matrix insertRow ::   forall i n m ns a.-  FinT i (1 GN.+ n) =>+  FinC i (1 GN.+ n) =>   Mat (m ': ns) a ->   Mat (n ': m ': ns) a ->   Mat (1 GN.+ n ': m ': ns) a@@ -1248,7 +1263,7 @@ -- | delete a column from a matrix (2d or higher) deleteCol ::   forall (i :: Nat) (n :: Nat) (n1 :: Nat) ns a.-  FinT i (1 GN.+ n1) =>+  FinC i (1 GN.+ n1) =>   Mat (n ': (1 GN.+ n1) ': ns) a ->   Mat (n ': n1 ': ns) a deleteCol = deleteCol' (finC @i @(1 GN.+ n1))@@ -1264,7 +1279,7 @@ -- | insert a column into a mat (2d and above) insertCol ::   forall (i :: Nat) (n :: Nat) (n1 :: Nat) ns a.-  FinT i (1 GN.+ n1) =>+  FinC i (1 GN.+ n1) =>   Mat (n ': ns) a ->   Mat (n ': n1 ': ns) a ->   Mat (n ': (1 GN.+ n1) ': ns) a@@ -1282,7 +1297,7 @@ -- | swaps mat rows (1d or more) swapRow ::   forall (i :: Nat) (j :: Nat) (n :: Nat) ns a.-  (FinT i n, FinT j n) =>+  (FinC i n, FinC j n) =>   Mat (n ': ns) a ->   Mat (n ': ns) a swapRow = swapRow' (finC @i) (finC @j)@@ -1312,7 +1327,7 @@ -- | swaps mat rows (2d or more) swapCol ::   forall (i :: Nat) (j :: Nat) (n :: Nat) (n1 :: Nat) ns a.-  (FinT i n1, FinT j n1) =>+  (FinC i n1, FinC j n1) =>   Mat (n ': n1 ': ns) a ->   Mat (n ': n1 ': ns) a swapCol = swapCol' (finC @i) (finC @j)@@ -1358,20 +1373,20 @@   Mat (n ': m ': ns) a ->   Mat (n ': m' ': ns) a ->   Mat (n ': (m GN.+ m') ': ns) a-appendH w@(Mat _ (n :| ps)) w1@(Mat _ (n' :| ps1))-  | n == n' =+appendH w@(Mat _ (n :| ps)) w1@(Mat _ (n' :| ps1)) = forceRightP "appendH" $+  if n == n' then       case (ps, ps1) of-        ([], _) -> programmError "appendH:lhs missing indices"-        (_, []) -> programmError "appendH:rhs missing indices"+        ([], _) -> Left "lhs missing indices"+        (_, []) -> Left "rhs missing indices"         (m : ns, m' : ns')-          | ns == ns' ->-              let x1 = frp $ chunkNV (unitsF n) (productP (m :| ns)) (mVec w)-                  x2 = frp $ chunkNV (unitsF @[] n) (productP (m' :| ns')) (mVec w1)-                  ret = frp $ zipWithExact (<>) x1 x2-                  ps2 = n :| ([m +! m'] <> ns)-               in MatIU (V.concat ret) ps2-          | otherwise -> programmError $ "appendH:ns/=ns' " ++ show (ns, ns')-  | otherwise = programmError $ "appendH: n/=n' " ++ show (n, n')+          | ns == ns' -> do+              x1 <- chunkNV (unitsF n) (productP (m :| ns)) (mVec w)+              x2 <- chunkNV (unitsF @[] n) (productP (m' :| ns')) (mVec w1)+              ret <- zipWithExact (<>) x1 x2+              let ps2 = n :| ([m +! m'] <> ns)+              mkMat (V.concat ret) ps2+          | otherwise -> Left $ "ns/=ns' " ++ show (ns, ns')+  else Left $ "n/=n' " ++ show (n, n')  -- | return a mat as a permutation of a list (1d only) todo: extend to multidimensions permutationsMat :: forall n a. Vec n a -> Mat2 (FacT n) n a@@ -1440,7 +1455,7 @@ -- | convert a matrix to a nested tuple type MatTupleT :: [Nat] -> Type -> Type type family MatTupleT ns a where-  MatTupleT '[] _ = GL.TypeError ('GL.Text "MatTupleT '[]: undefined for empty indices")+  MatTupleT '[] _ = GL.TypeError ( 'GL.Text "MatTupleT '[]: undefined for empty indices")   MatTupleT '[n] a = ListTupleT n a   MatTupleT (n ': n1 ': ns) a = ListTupleT n (MatTupleT (n1 ': ns) a) @@ -1464,14 +1479,14 @@     -- | traversal over a well-formed nested tuple     Traversal (MatTupleT ns a) (MatTupleT ns b) a b -instance GL.TypeError ('GL.Text "MatTupleC '[]: undefined for empty indices") => MatTupleC '[] a where+instance GL.TypeError ( 'GL.Text "MatTupleC '[]: undefined for empty indices") => MatTupleC '[] a where   toTupleC = compileError "MatTupleC:toTupleC"   fromTupleC = compileError "MatTupleC:fromTupleC"   fmapTupleMatC = compileError "MatTupleC:fmapTupleMatC"   traversalTupleMatC = compileError "MatTupleC:traversalTupleMatC"  instance ListTupleCInternal n => MatTupleC '[n] a where-  toTupleC  = toTupleCInternal+  toTupleC = toTupleCInternal   fromTupleC = fromTupleCInternal   fmapTupleMatC = fmapTupleInternal   traversalTupleMatC = traversalTupleCInternal@@ -1562,22 +1577,22 @@  -- | transpose a 2d or larger matrix transposeMat :: forall n m ns a. Mat (n ': m ': ns) a -> Mat (m ': n ': ns) a-transposeMat w@(Mat _ (n :| ps)) =+transposeMat w@(Mat _ (n :| ps)) = forceRightP "transposeMat" $   case ps of-    [] -> programmError "transposeMat"-    m : ns ->-      let ys = frp $ chunkNLen1 n (productP (m :| ns)) w-          zs = N.transpose $ N.map (chunksOf1 (productP ns)) ys-       in MatIU (V.fromList $ N.toList $ sconcat $ sconcat zs) (m :| (n : ns))+    [] -> Left "transposeMat"+    m : ns -> do+      ys <- chunkNLen1 n (productP (m :| ns)) w+      let zs = N.transpose $ N.map (chunksOf1 (productP ns)) ys+      mkMat (V.fromList $ N.toList $ sconcat $ sconcat zs) (m :| (n : ns))  -- | validate and convert from a nested list to a matrix-nestedListToMatValidated :: forall ns x a. (x ~ ListNST ns a, ValidateNestedListC x (ValidateNestedListT x), MatConvertersC ns) => ListNST ns a -> Either String (Mat ns a)+nestedListToMatValidated :: forall ns a x. (x ~ ListNST ns a, ValidateNestedListC x (ValidateNestedListT x), MatConvertersC ns) => ListNST ns a -> Either String (Mat ns a) nestedListToMatValidated w = do   _ <- validateNestedList w   nestedListToMatC w  -- | validate and convert from a nested nonempty list to a matrix-nestedNonEmptyToMatValidated :: forall ns x a. (x ~ NonEmptyNST ns a, ValidateNestedNonEmptyC x (ValidateNestedNonEmptyT x), MatConvertersC ns) => NonEmptyNST ns a -> Either String (Mat ns a)+nestedNonEmptyToMatValidated :: forall ns a x. (x ~ NonEmptyNST ns a, ValidateNestedNonEmptyC x (ValidateNestedNonEmptyT x), MatConvertersC ns) => NonEmptyNST ns a -> Either String (Mat ns a) nestedNonEmptyToMatValidated w = do   _ <- validateNestedNonEmpty w   nestedNonEmptyToMatC w@@ -1602,7 +1617,7 @@   -- | convert a nested nonempty list to a 'Mat'   nestedNonEmptyToMatC :: NonEmptyNST ns a -> Either String (Mat ns a) -instance GL.TypeError ('GL.Text "MatConvertersC '[]: undefined for empty indices") => MatConvertersC '[] where+instance GL.TypeError ( 'GL.Text "MatConvertersC '[]: undefined for empty indices") => MatConvertersC '[] where   matToNestedVecC = compileError "MatConvertersC"   nestedVecToMatC = compileError "MatConvertersC"   matToNestedListC = compileError "MatConvertersC"@@ -1610,14 +1625,14 @@   nestedListToMatC = compileError "MatConvertersC"   nestedNonEmptyToMatC = compileError "MatConvertersC" -instance PosT n => MatConvertersC '[n] where+instance PosC n => MatConvertersC '[n] where   matToNestedVecC = id   nestedVecToMatC = id   matToNestedListC = toListMat   matToNestedNonEmptyC = toNonEmptyMat   nestedListToMatC = matImpl True   nestedNonEmptyToMatC = matImpl True . N.toList-instance (PosT n, MatConvertersC (m ': ns)) => MatConvertersC (n ': m ': ns) where+instance (PosC n, MatConvertersC (m ': ns)) => MatConvertersC (n ': m ': ns) where   matToNestedVecC lst = fmap matToNestedVecC (rows @n lst)   nestedVecToMatC lst@(Mat _ (n :| _)) =     let zs@(Mat _ (m :| ns) :| _) = toNonEmptyMat $ fmap (nestedVecToMatC @(m ': ns)) lst@@ -1631,7 +1646,7 @@   nestedNonEmptyToMatC w = nonEmptyMatsToMat =<< traverse (nestedNonEmptyToMatC @(m ': ns)) w  -- | create a matrix of one dimension higher from rows of a sub matrix-nonEmptyMatsToMat :: forall n m ns a t. (Foldable1 t, PosT n) => t (Mat (m ': ns) a) -> Either String (Mat (n ': m ': ns) a)+nonEmptyMatsToMat :: forall n m ns a t. (Foldable1 t, PosC n) => t (Mat (m ': ns) a) -> Either String (Mat (n ': m ': ns) a) nonEmptyMatsToMat (toNonEmpty -> xs@(Mat _ ps :| _)) = do   let n = fromNP @n   ret <- lengthExact1 n xs@@ -1640,29 +1655,29 @@ -- | converts mat dimensions to a nested list type MatToNestedVecT :: [Nat] -> Type -> Type type family MatToNestedVecT ns a where-  MatToNestedVecT '[] _ = GL.TypeError ('GL.Text "MatToNestedVecT '[]: undefined for empty indices")+  MatToNestedVecT '[] _ = GL.TypeError ( 'GL.Text "MatToNestedVecT '[]: undefined for empty indices")   MatToNestedVecT '[n] a = Vec n a   MatToNestedVecT (n ': n1 ': ns) a = Vec n (MatToNestedVecT (n1 ': ns) a) --- | type synonym for the result of nesting a matrix: @see 'toND'+-- | type synonym for the result of nesting a matrix: see 'toND' type MatToNDT :: Nat -> [Nat] -> Type -> Type type MatToNDT i ns a = Mat (MatToMatNTA (NatToPeanoT i) ns) (Mat (MatToMatNTB (NatToPeanoT i) ns) a)  -- | create a nested matrix going "i" levels down: noop is not supported ie 4D matrix to a 4D matrix matToNDImpl ::   forall (i :: Nat) (ns :: [Nat]) a.-  PosT i =>+  PosC i =>   Mat ns a ->   MatToNDT i ns a-matToNDImpl w@(Mat _ ps) =+matToNDImpl w@(Mat _ ps) = forceRightP "matToNDImpl" $   let i = fromNP @i       (ps1, bs) = splitAt1 i ps    in case bs of-        y : ys ->+        y : ys -> do           let ps2 = y :| ys-              xs = frp $ chunkNVMat (unitsF (productP ps1)) ps2 w-           in MatIU (V.fromList xs) ps1-        [] -> programmError "toND:missing indices to the right"+          xs <- chunkNVMat (unitsF (productP ps1)) ps2 w+          mkMat (V.fromList xs) ps1+        [] -> Left "missing indices to the right"  type MatToMatNTA :: Peano -> [Nat] -> [Nat] type family MatToMatNTA i ns where@@ -1686,19 +1701,19 @@     GL.TypeError ( 'GL.Text "MatToMatNTB: depth is more than the number of indices")   MatToMatNTB ( 'S ( 'S i)) (_ ': m ': ns) = MatToMatNTB ( 'S i) (m ': ns) --- | create a nd matrix using a Nat @see 'toND-toND :: forall i ns a. i <=! i => Mat ns a -> MatToNDT i ns a+-- | create a nd matrix using a Nat see 'toND+toND :: forall i ns a. PosC i => Mat ns a -> MatToNDT i ns a toND = matToNDImpl @i --- | create a nested 1d matrix @see 'toND+-- | create a nested 1d matrix see 'toND toVec :: Mat ns a -> MatToNDT 1 ns a toVec = toND @1 --- | create a nested 2d matrix @see 'toND+-- | create a nested 2d matrix see 'toND toMat2 :: Mat ns a -> MatToNDT 2 ns a toMat2 = toND @2 --- | create a nested 3d matrix @see 'toND+-- | create a nested 3d matrix see 'toND toMat3 :: Mat ns a -> MatToNDT 3 ns a toMat3 = toND @3 @@ -1713,13 +1728,13 @@  -- | gets the diagonal elements of a 2d or greater square matrix: the diagonal of a n * n * ns matrix results in a n * ns matrix diagonal :: Mat (n ': n ': ns) a -> Mat (n ': ns) a-diagonal (Mat v (n :| ps)) =+diagonal (Mat v (n :| ps)) = forceRightP "diagonal" $   case ps of-    _n : ns ->+    _n : ns -> do       let len = productPInt ns           xs = map (\i -> V.slice (i * (unP n + 1) * len) len v) [0 .. unP n - 1]-       in MatIU (V.concat xs) (n :| ns)-    [] -> programmError "diagonal: missing indices"+      mkMat (V.concat xs) (n :| ns)+    [] -> Left "missing indices"  -- | take a subset of a matrix using the start and end rows subsetRows ::@@ -1727,13 +1742,13 @@   DiffTC i j n =>   Mat (n ': ns) a ->   Mat (DiffT i j n ': ns) a-subsetRows (Mat v (_ :| ns)) =+subsetRows (Mat v (_ :| ns)) = forceRightP "subsetRows" $ do   let i = fromNP @i       j = fromNP @j       n1 = (unP i - 1) * productPInt ns-      n' = frp $ withOp2 ((-) . (+ 1)) j i-      ps1 = n' :| ns-   in MatIU (V.slice n1 (productPInt ps1) v) ps1+  n' <- withOp2 ((-) . (+ 1)) j i+  let ps1 = n' :| ns+  mkMat (V.slice n1 (productPInt ps1) v) ps1  -- todo use FinMat versions of subsetRows and subsetCols ie not just typelevel: need typelevel for the count of rows/cols so no point @@ -1764,7 +1779,7 @@ -- | specialised version of 'readMat' for 'Vec' readVec ::   ( MatConvertersC '[n]-  , PosT n+  , PosC n   , Read [a]   ) =>   ReadS (Vec n a)@@ -1773,8 +1788,8 @@ -- | specialised version of 'readMat' for 'Mat2' readMat2 ::   ( MatConvertersC '[n, m]-  , PosT n-  , PosT m+  , PosC n+  , PosC m   , Read [[a]]   ) =>   ReadS (Mat2 n m a)@@ -1940,105 +1955,105 @@   _r10 :: Lens' s a  -- | lens into the first row in a 2d or greater matrix-instance FinT 1 n => Row1 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where+instance FinC 1 n => Row1 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where   _r1 = _row @1  -- |  lens into the first element in a 1d matrix-instance FinT 1 n => Row1 (Vec n a) a where+instance FinC 1 n => Row1 (Vec n a) a where   _r1 = _row @1 -instance (FinT 2 n) => Row2 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where+instance FinC 2 n => Row2 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where   _r2 = _row @2 -instance (FinT 2 n) => Row2 (Vec n a) a where+instance FinC 2 n => Row2 (Vec n a) a where   _r2 = _row @2 -instance (FinT 3 n) => Row3 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where+instance FinC 3 n => Row3 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where   _r3 = _row @3 -instance (FinT 3 n) => Row3 (Vec n a) a where+instance FinC 3 n => Row3 (Vec n a) a where   _r3 = _row @3 -instance (FinT 4 n) => Row4 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where+instance FinC 4 n => Row4 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where   _r4 = _row @4 -instance (FinT 4 n) => Row4 (Vec n a) a where+instance FinC 4 n => Row4 (Vec n a) a where   _r4 = _row @4 -instance (FinT 5 n) => Row5 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where+instance FinC 5 n => Row5 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where   _r5 = _row @5 -instance (FinT 5 n) => Row5 (Vec n a) a where+instance FinC 5 n => Row5 (Vec n a) a where   _r5 = _row @5 -instance (FinT 6 n) => Row6 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where+instance FinC 6 n => Row6 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where   _r6 = _row @6 -instance (FinT 6 n) => Row6 (Vec n a) a where+instance FinC 6 n => Row6 (Vec n a) a where   _r6 = _row @6 -instance (FinT 7 n) => Row7 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where+instance FinC 7 n => Row7 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where   _r7 = _row @7 -instance (FinT 7 n) => Row7 (Vec n a) a where+instance FinC 7 n => Row7 (Vec n a) a where   _r7 = _row @7 -instance (FinT 8 n) => Row8 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where+instance FinC 8 n => Row8 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where   _r8 = _row @8 -instance (FinT 8 n) => Row8 (Vec n a) a where+instance FinC 8 n => Row8 (Vec n a) a where   _r8 = _row @8 -instance (FinT 9 n) => Row9 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where+instance FinC 9 n => Row9 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where   _r9 = _row @9 -instance (FinT 9 n) => Row9 (Vec n a) a where+instance FinC 9 n => Row9 (Vec n a) a where   _r9 = _row @9 -instance (FinT 10 n) => Row10 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where+instance FinC 10 n => Row10 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where   _r10 = _row @10 -instance (FinT 10 n) => Row10 (Vec n a) a where+instance FinC 10 n => Row10 (Vec n a) a where   _r10 = _row @10  -- | lens into column 1 of a matrix-_c1 :: FinT 1 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)+_c1 :: FinC 1 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a) _c1 = _col @1  -- | lens into column 2 of a matrix-_c2 :: FinT 2 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)+_c2 :: FinC 2 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a) _c2 = _col @2  -- | lens into column 3 of a matrix-_c3 :: FinT 3 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)+_c3 :: FinC 3 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a) _c3 = _col @3  -- | lens into column 4 of a matrix-_c4 :: FinT 4 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)+_c4 :: FinC 4 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a) _c4 = _col @4  -- | lens into column 5 of a matrix-_c5 :: FinT 5 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)+_c5 :: FinC 5 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a) _c5 = _col @5  -- | lens into column 6 of a matrix-_c6 :: FinT 6 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)+_c6 :: FinC 6 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a) _c6 = _col @6  -- | lens into column 7 of a matrix-_c7 :: FinT 7 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)+_c7 :: FinC 7 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a) _c7 = _col @7  -- | lens into column 8 of a matrix-_c8 :: FinT 8 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)+_c8 :: FinC 8 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a) _c8 = _col @8  -- | lens into column 9 of a matrix-_c9 :: FinT 9 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)+_c9 :: FinC 9 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a) _c9 = _col @9  -- | lens into column 10 of a matrix-_c10 :: FinT 10 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)+_c10 :: FinC 10 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a) _c10 = _col @10  -- | marker representing the last value in a 1d matrix ie singleton@@ -2099,11 +2114,11 @@   where   consMat =     iso-      ( \(Mat v0 (sn :| ps)) ->-          let n = frp $ predP sn-           in case V.uncons v0 of -- stay within Vector-                Nothing -> programmError "consMat '[1 GN.+ n]: no data"-                Just (a, v) -> (a, MatIU v (n :| ps))+      ( \(Mat v0 (sn :| ps)) -> forceRightP "consMat '[n]" $ do+          n <- predP sn+          case V.uncons v0 of -- stay within Vector+                Nothing -> Left "no data"+                Just (a, v) -> (a,) <$> mkMat v (n :| ps)       )       (\(a, Mat v (p :| ps)) -> MatIU (V.cons a v) (succP p :| ps)) @@ -2118,10 +2133,10 @@   where   consMat =     iso-      ( \(Mat v (_ :| ps)) ->+      ( \(Mat v (_ :| ps)) -> forceRightP "consMat '(1 ': n1 ': ns)" $           case ps of-            m : ns -> (MatIU v (m :| ns), EofN)-            [] -> programmError "consMat (1 ': m ': ns): missing indices"+            m : ns -> (,EofN) <$> mkMat v (m :| ns)+            [] -> Left "missing indices"       )       (\(Mat v ps, EofN) -> MatIU v (_1P N.<| ps)) @@ -2136,17 +2151,15 @@   where   consMat =     iso-      ( \(Mat v (sn :| ps)) ->+      ( \(Mat v (sn :| ps)) -> forceRightP "consMat '(n ': m ': ns)" $ do           case ps of-            m : ns ->-              let n = frp $ predP sn-                  ps1 = m :| ns+            m : ns -> do+              n <- predP sn+              let ps1 = m :| ns                   ps2 = n :| (m : ns)                   (v1, v2) = V.splitAt (productPInt ps1) v-               in ( MatIU v1 ps1-                  , MatIU v2 ps2-                  )-            [] -> programmError "consMat:(1 GN.+ n ': m ': ns): missing indices"+              liftA2 (,) (mkMat v1 ps1) (mkMat v2 ps2)+            [] -> Left "missing indices"       )       (\(Mat v1 _, Mat v2 (p2 :| ps2)) -> MatIU (v1 <> v2) (succP p2 :| ps2)) @@ -2180,22 +2193,22 @@   where   snocMat =     iso-      ( \(Mat v0 (sn :| ps)) ->-          let n = frp $ predP sn-           in case V.unsnoc v0 of-                Nothing -> programmError "snocMat '[1 GN.+ n]: no data"-                Just (v, a) -> (MatIU v (n :| ps), a)+      ( \(Mat v0 (sn :| ps)) -> forceRightP "snocMat '[n]" $ do+          n <- predP sn+          case V.unsnoc v0 of+                Nothing -> Left "no data"+                Just (v, a) -> (,a) <$> mkMat v (n :| ps)       )       (\(Mat v (p :| ps), a) -> MatIU (V.snoc v a) (succP p :| ps))  instance {-# OVERLAPPING #-} SnocMatC (1 ': n1 ': ns) a b where   snocMat =     iso-      ( \(Mat v (_ :| ps)) ->+      ( \(Mat v (_ :| ps)) -> forceRightP "snocMat '(1 ': n1 ': ns)" $ do           case ps of             m : ns ->-              (EofN, MatIU v (m :| ns))-            [] -> programmError "snocMat '[1 GN.+ n]: missing indices"+              (EofN,) <$> mkMat v (m :| ns)+            [] -> Left "missing indices"       )       (\(EofN, Mat v ps) -> MatIU v (_1P N.<| ps)) @@ -2208,17 +2221,15 @@   where   snocMat =     iso-      ( \(Mat v (sn :| ps)) ->+      ( \(Mat v (sn :| ps)) -> forceRightP "snocMat '(n ': m ': ns)" $ do           case ps of-            m : ns ->-              let n = frp $ predP sn-                  ps1 = m :| ns+            m : ns -> do+              n <- predP sn+              let ps1 = m :| ns                   ps2 = n :| (m : ns)                   (v2, v1) = V.splitAt (productPInt ps2) v-               in ( MatIU v2 ps2-                  , MatIU v1 ps1-                  )-            [] -> programmError "snocMat:(1 GN.+ n ': m ': ns): missing indices"+              liftA2 (,) (mkMat v2 ps2) (mkMat v1 ps1)+            [] -> Left "missing indices"       )       (\(Mat v1 (p1 :| ps1), Mat v2 _) -> MatIU (v1 <> v2) (succP p1 :| ps1)) @@ -2233,13 +2244,13 @@  -- | get a row from a matrix using a concrete index see '_row'' indexRow :: Fin n -> Mat (n ': m ': ns) a -> Mat (m ': ns) a-indexRow (Fin (Pos i) _n) (Mat v (_ :| ps)) =+indexRow (Fin (Pos i) _n) (Mat v (_ :| ps)) = forceRightP "indexRow" $   case ps of-    m : ns ->+    m : ns -> do       let s = (i - 1) * len           len = productPInt (m :| ns)-       in MatIU (V.slice s len v) (m :| ns)-    [] -> programmError "indexRow: missing indices"+      mkMat (V.slice s len v) (m :| ns)+    [] -> Left "missing indices"  -- | 'Data.List.scanr' for a vector scanrVec :: forall n a b. (a -> b -> b) -> b -> Vec n a -> Vec (n GN.+ 1) b@@ -2251,14 +2262,14 @@ scanlVec f c (Mat v (p :| ps)) =   MatIU (V.scanl' f c v) (succP p :| ps) -{- | @see 'Data.Vector.postscanr''+{- | see 'Data.Vector.postscanr''  concrete version of 'Primus.Fold.postscanr -} postscanrMat :: forall ns a b. (a -> b -> b) -> b -> Mat ns a -> Mat ns b postscanrMat f c (Mat v ps) =   MatIU (V.postscanr' f c v) ps -{- | @see 'Data.Vector.postscanl''+{- | see 'Data.Vector.postscanl''  concrete version of 'Primus.Fold.postscanl' -} postscanlMat :: forall ns a b. (b -> a -> b) -> b -> Mat ns a -> Mat ns b@@ -2304,3 +2315,54 @@ -- | matrix of dimension 10 dim10 :: Mat '[n, m, p, q, r, s, t, u, v, w] a -> Mat '[n, m, p, q, r, s, t, u, v, w] a dim10 = id++-- | left rotate a matrix+rotateLeft :: Mat2 n m a -> Mat2 m n a+rotateLeft = unrows . sequence1 . fmap reverseT . rows++-- | right rotate a matrix+rotateRight :: Mat2 n m a -> Mat2 m n a+rotateRight = unrows . fmap reverseT . sequence1 . rows++cofactorsL :: forall a . Pos -> [a] -> [(a, [a])]+cofactorsL n xs+  | n <= _2P = programmError $ "cofactorsL: n is too small: must be greater than 2 but found " ++ show n+  | len /= len' = programmError $ "cofactorsL: wrong length: expected " ++ show len' ++ " but found " ++ show len+  | otherwise =+    let (h,t) = splitAt (unP n) xs+    in foldl' (\z (i,a) -> (a,deleteColumnL n i t):z) [] (zip [0..] h)+  where len = length xs+        len' = unP (n *! n)++-- | delete column "i" from a list of width "n"+deleteColumnL :: forall a . Pos -> Int -> [a] -> [a]+deleteColumnL (Pos n) i ys =+  let (as,bs) = splitAt i ys+  in as <> concat (L.unfoldr g bs)+  where+    g :: [a] -> Maybe ([a],[a])+    g = list Nothing (\_ -> Just . splitAt (n-1))++determinantL :: forall a . Num a => Pos -> [a] -> a+determinantL n m0+  | len /= unP (n *! n) = programmError $ "determinantL: wrong length n=" ++ show n ++ " m=" ++ show len+  | otherwise =+  case m0 of+   [a] -> a+   [a,b,c,d] -> a * d - b * c+   _o ->+    snd $ foldl' f (True, 0) (cofactorsL n m0)+   where+    f :: (Bool, a) -> (a, [a]) -> (Bool, a)+    f (sgn, tot) (a, m) =+      let val = bool id negate sgn a * determinantL (frp $ predP n) m+       in (not sgn, tot + val)+    len = length m0++-- | get the determinant of a matrix+determinant :: Num a => Mat2 n n a -> a+determinant (Mat v (n :| _)) =+  bool negate id (n <= _2P) $ determinantL n (V.toList v)+++

@@ -74,14 +74,14 @@ import Data.Pos import Data.Proxy import qualified GHC.TypeLits as GL-import GHC.TypeNats (Nat)+import GHC.TypeNats (Nat,KnownNat) import qualified GHC.TypeNats as GN import Primus.Error import Primus.Fold import Primus.List import Primus.NonEmpty import Primus.One-import qualified Primus.TypeLevel as TP (FailUnless)+import Primus.TypeLevel (FailUnless)  -- | get the factorial of a 'Nat' type FacT :: Nat -> Nat@@ -93,7 +93,7 @@ -- | constraint for ensuring that "i" <= "n" type (<=!) :: Nat -> Nat -> Constraint type i <=! n =-  ( TP.FailUnless+  ( FailUnless       (i GN.<=? n)       ( 'GL.Text "i>n"           'GL.:<>: 'GL.Text ": i="@@ -101,13 +101,13 @@           'GL.:<>: 'GL.Text " n="           'GL.:<>: 'GL.ShowType n       )-  , PosT i+  , PosC i   )  -- | constraint for ensuring that "i" <= "n" with a custom error message type LTEQT :: GL.ErrorMessage -> Nat -> Nat -> Constraint type LTEQT msg i n =-  ( TP.FailUnless+  ( FailUnless       (i GN.<=? n)       ( 'GL.Text "i>n"           'GL.:<>: 'GL.Text ": i="@@ -116,13 +116,13 @@           'GL.:<>: 'GL.ShowType n           'GL.:<>: msg       )-  , PosT i+  , PosC i   )  -- | constraint for ensuring that "i" <= "n" type (<!) :: Nat -> Nat -> Constraint type i <! n =-  ( TP.FailUnless+  ( FailUnless       (i GN.+ 1 GN.<=? n)       ( 'GL.Text "i>=n"           'GL.:<>: 'GL.Text ": i="@@ -130,9 +130,25 @@           'GL.:<>: 'GL.Text " n="           'GL.:<>: 'GL.ShowType n       )-  , GN.KnownNat i+  , KnownNat i   ) +-- | constraint for positive numbers+type LTEQC :: Nat -> Nat -> Constraint+class (KnownNat i, KnownNat n) => LTEQC i n where+instance+  ( KnownNat i+  , KnownNat n+  , FailUnless+      (i GL.<=? n)+      ( 'GL.Text "LTEQC n: requires n >= i but found i="+          'GL.:<>: 'GL.ShowType i+          'GL.:<>: 'GL.Text " n="+          'GL.:<>: 'GL.ShowType n+      )+  ) =>+  LTEQC i n+ -- | constraint for DiffC with better error messages type DiffTC :: Nat -> Nat -> Nat -> Constraint type DiffTC i j n = (i <=! j, j <=! n)@@ -155,7 +171,7 @@ -- | product of a type level list as a 'Nat' type ProductT :: [Nat] -> Nat type family ProductT ns where-  ProductT '[] = GL.TypeError ('GL.Text "ProductT: empty indices")+  ProductT '[] = GL.TypeError ( 'GL.Text "ProductT: empty indices")   ProductT '[n] = n   ProductT (n ': n1 ': ns) = n GN.* ProductT (n1 ': ns) @@ -193,7 +209,7 @@       [] -> programmError "ValidateNestedNonEmptyC: ('S 'Z): empty list of indices" instance ValidateNestedNonEmptyC x ( 'S zs) => ValidateNestedNonEmptyC (NonEmpty x) ( 'S ( 'S zs)) where   validateNestedNonEmptyC ixes x@(n :| ns) xs =-    let cs = map clOrdering $ compareLengths (x :| xs)+    let cs = map clOrdering $ compareLengths x xs      in if all (Just EQ ==) cs           then             let zs = ns <> concatMap N.toList xs@@ -215,7 +231,7 @@ instance ValidateNestedListC x ( 'S n) => ValidateNestedListC [x] ( 'S ( 'S n)) where   validateNestedListC ixes [] _ = Left $ "validateNestedListC: ixes=" ++ show ixes ++ ":no data!"   validateNestedListC ixes x@(n : ns) xs =-    let cs = map clOrdering $ compareLengths (x :| xs)+    let cs = map clOrdering $ compareLengths x xs      in if all (Just EQ ==) cs           then             let zs = ns <> concat xs@@ -240,14 +256,14 @@ -- | convert a matrix index into nested lists type ListNST :: [Nat] -> Type -> Type type family ListNST ns a where-  ListNST '[] _ = GL.TypeError ('GL.Text "ListNST: empty indices")+  ListNST '[] _ = GL.TypeError ( 'GL.Text "ListNST: empty indices")   ListNST '[_] a = [a]   ListNST (_ ': n1 ': ns) a = [ListNST (n1 ': ns) a]  -- | convert a matrix index into nested lists type NonEmptyNST :: [Nat] -> Type -> Type type family NonEmptyNST ns a where-  NonEmptyNST '[] _ = GL.TypeError ('GL.Text "NonEmptyNST: empty indices")+  NonEmptyNST '[] _ = GL.TypeError ( 'GL.Text "NonEmptyNST: empty indices")   NonEmptyNST '[_] a = NonEmpty a   NonEmptyNST (_ ': n1 ': ns) a = NonEmpty (NonEmptyNST (n1 ': ns) a) @@ -270,12 +286,12 @@    flattenNestedListC :: proxy a -> ListNST ns a -> Either String [a] -instance GL.TypeError ('GL.Text "NestedListC '[]: empty indices") => NestedListC '[] where+instance GL.TypeError ( 'GL.Text "NestedListC '[]: empty indices") => NestedListC '[] where   nestedListToNonEmptyC = compileError "NestedListC '[]:nestedListToNonEmptyC"   nestedNonEmptyToListC = compileError "NestedListC '[]:nestedNonEmptyToListC"   flattenNestedListC = compileError "NestedListC '[]:flattenNestedListC" -instance PosT n => NestedListC '[n] where+instance PosC n => NestedListC '[n] where   nestedListToNonEmptyC _ = \case     [] -> Left "nestedListToNonEmptyC 'SZ no data"     x : xs -> lmsg "nestedListToNonEmptyC 'SZ" $ lengthExact1 (fromNP @n) (x :| xs)@@ -284,7 +300,7 @@     [] -> Left "flattenNestedListC 'SZ no data"     x : xs -> lmsg "flattenNestedListC 'SZ" $ lengthExact (fromN @n) (x : xs) -instance (PosT n, NestedListC (n1 ': ns)) => NestedListC (n ': n1 ': ns) where+instance (PosC n, NestedListC (n1 ': ns)) => NestedListC (n ': n1 ': ns) where   nestedListToNonEmptyC p = \case     [] -> Left "nestedListToNonEmptyC 'SS no data"     x : xs -> do

@@ -164,13 +164,13 @@           @?= Right (FinU @5 _4P _5P)     , testCase "_Fin" $         mkFinC @5 _10P _5P-          @?= Left "mkFin:10P is too large: maximum is 5P"+          @?= Left "mkFin:_10P is too large: maximum is _5P"     , testCase "mkFinC" $         mkFinC @9 _4P _10P-          @?= Left "mkFinC: 10P /= 9P at typelevel"+          @?= Left "mkFinC: _10P /= _9P at typelevel"     , testCase "mkFinC" $         mkFinC @9 _12P _10P-          @?= Left "mkFinC: 10P /= 9P at typelevel"+          @?= Left "mkFinC: _10P /= _9P at typelevel"     , testCase "signum1" $         signum1 (Right (FinU @5 _4P _5P))           @?= Right (FinU @5 _1P _5P)@@ -229,7 +229,7 @@     , testCase "fin" $         fin @10 (-5) @?= Left "eitherPos: i<=0: found -5"     , testCase "fin" $-        fin @10 11 @?= Left "mkFin:11P is too large: maximum is 10P"+        fin @10 11 @?= Left "mkFin:_11P is too large: maximum is _10P"     , testCase "fin" $         fin @10 10 @?= Right (FinU _10P _10P)     , testCase "fin" $

@@ -214,16 +214,16 @@               N.last xs @?= maxBound     , testCase "showFinMat" $         map showFinMat [FinMatU @'[2, 3, 5] 0 (_2P :| [_3P, _5P]), toEnum 5 ..]-          @?= ["0@{2,3,5}", "5@{2,3,5}", "10@{2,3,5}", "15@{2,3,5}", "20@{2,3,5}", "25@{2,3,5}"]+          @?= ["FinMat@0{2,3,5}", "FinMat@5{2,3,5}", "FinMat@10{2,3,5}", "FinMat@15{2,3,5}", "FinMat@20{2,3,5}", "FinMat@25{2,3,5}"]     , testCase "nonEmptyToFinMat'" $         nonEmptyToFinMat' (_1P :| [_4P, _3P]) (_1P :| [_3P, _4P])-          @?= Left "nonEmptyToFinMat:These es=outofbounds (4P,3P) as=(1P,1P) :| [(3P,4P)]"+          @?= Left "nonEmptyToFinMat:These es=outofbounds (_4P,_3P) as=(_1P,_1P) :| [(_3P,_4P)]"     , testCase "nonEmptyToFinMat'" $         nonEmptyToFinMat' (_1P :| [_2P, _3P, _6P]) (_1P :| [_3P, _4P])-          @?= Left "nonEmptyToFinMat:too many indices: expected 3 is=1P :| [2P,3P,6P] ns=1P :| [3P,4P]"+          @?= Left "nonEmptyToFinMat:too many indices: expected 3 is=_1P :| [_2P,_3P,_6P] ns=_1P :| [_3P,_4P]"     , testCase "nonEmptyToFinMat'" $         nonEmptyToFinMat' (_1P :| [_2P]) (_1P :| [_3P, _4P])-          @?= Left "nonEmptyToFinMat:not enough indices: expected 3 is=1P :| [2P] ns=1P :| [3P,4P]"+          @?= Left "nonEmptyToFinMat:not enough indices: expected 3 is=_1P :| [_2P] ns=_1P :| [_3P,_4P]"     , testCase "nonEmptyToFinMat'" $         nonEmptyToFinMat' (_3P :| [_1P, _4P]) (_3P :| [_8P, _7P])           @?= Right (FinMatU @'[3, 8, 7] 115 (_3P :| [_8P, _7P]))@@ -370,45 +370,45 @@     , testCase "relPos" $         relPos ((_4P, _7P) :| [(_3P, _5P), (_2P, _5P)]) @?= (_P @175, 86)     , testCase "readFinMat" $-        readFinMat @'[7, 3, 3] "5@{7,3,3}xyz" @?= [(finMatC @'[1, 2, 3] @'[7, 3, 3], "xyz")]+        readFinMat @'[7, 3, 3] "FinMat@5{7,3,3}xyz" @?= [(finMatC @'[1, 2, 3] @'[7, 3, 3], "xyz")]     , testCase "readFinMat" $         let m = finMatC @'[1, 2, 3] @'[7, 3, 3]          in readFinMat @'[7, 3, 3] (show m ++ "  ") @?= [(m, "  ")]     , testCase "readFinMat" $-        readFinMat @'[7, 3, 3] "6@{1,2,3}xyz" @?= []+        readFinMat @'[7, 3, 3] "FinMat@6{1,2,3}xyz" @?= []     , testCase "readFinMat" $-        readFinMat @'[1, 2, 3] "         4@{     1,             2,   3}xy"+        readFinMat @'[1, 2, 3] "   FinMat@4{     1,             2,   3}xy"           @?= [(FinMatU @'[1, 2, 3] 4 (_1P :| [_2P, _3P]), "xy")]     , testCase "showFinMat'" $         showFinMat' (finMatC @'[2, 3, 5] @'[4, 4, 6])-          @?= "40@{2,3,5|4,4,6}"+          @?= "FinMat@40{2,3,5|4,4,6}"     , testCase "showFinMat'" $         showFinMat' (finMatC @'[1] @'[1])-          @?= "0@{1|1}"+          @?= "FinMat@0{1|1}"     , testCase "showFinMat'" $         showFinMat' (finMatC @(NN 123) @(NN 234))-          @?= "6@{1,2,3|2,3,4}"+          @?= "FinMat@6{1,2,3|2,3,4}"     , testCase "showFinMat'" $         showFinMat' (finMatC @(NN 111) @(NN 234))-          @?= "0@{1,1,1|2,3,4}"+          @?= "FinMat@0{1,1,1|2,3,4}"     , testCase "showFinMat'" $         showFinMat' (finMatC @(NN 114) @(NN 234))-          @?= "3@{1,1,4|2,3,4}"+          @?= "FinMat@3{1,1,4|2,3,4}"     , testCase "showFinMat'" $         showFinMat' (finMatC @(NN 9) @(NN 9))-          @?= "8@{9|9}"+          @?= "FinMat@8{9|9}"     , testCase "showFinMat" $         showFinMat (finMatC @'[1] @'[1])-          @?= "0@{1}"+          @?= "FinMat@0{1}"     , testCase "showFinMat" $         showFinMat (finMatC @'[1] @'[10])-          @?= "0@{10}"+          @?= "FinMat@0{10}"     , testCase "showFinMat" $         showFinMat (finMatC @'[10] @'[10])-          @?= "9@{10}"+          @?= "FinMat@9{10}"     , testCase "showFinMat" $         showFinMat (finMatC @'[4] @'[10])-          @?= "3@{10}"+          @?= "FinMat@3{10}"     , testCase "fromInteger1" $         fromInteger1 (minBound @(FinMat '[2, 3, 4])) 0           @?= Right (FinMatU @'[2, 3, 4] 0 (_2P :| [_3P, _4P]))@@ -434,20 +434,29 @@         toInteger1 (FinMatU @'[2, 3, 4] 12 (_2P :| [_3P, _4P]))           @?= 12     , testCase "index lenses" $-         finMatC @'[2,5,3,7] @'[2,12,13,8] ^. _i1-           @?= FinU @2 _2P _2P+        finMatC @'[2, 5, 3, 7] @'[2, 12, 13, 8] ^. _i1+          @?= FinU @2 _2P _2P     , testCase "index lenses" $-         finMatC @'[2,5,3,7] @'[2,12,13,8] ^. _i2-           @?= FinU @12 _5P _12P+        finMatC @'[2, 5, 3, 7] @'[2, 12, 13, 8] ^. _i2+          @?= FinU @12 _5P _12P     , testCase "index lenses" $-         finMatC @'[2,5,3,7] @'[2,12,13,8] ^. _i4-           @?= FinU @8 _7P _8P+        finMatC @'[2, 5, 3, 7] @'[2, 12, 13, 8] ^. _i4+          @?= FinU @8 _7P _8P     , testCase "finMat finMatC" $-         finMat @'[2,12,13,8] (6 + 2*8 + 4*13*8 + 1*12*13*8)-         @?= Right (finMatC @'[2,5,3,7] @'[2,12,13,8])+        finMat @'[2, 12, 13, 8] (6 + 2 * 8 + 4 * 13 * 8 + 1 * 12 * 13 * 8)+          @?= Right (finMatC @'[2, 5, 3, 7] @'[2, 12, 13, 8])     , testCase "finMat finMatC" $-         finMat @'[21] 0-         @?= Right (finMatC @'[1] @'[21])+        finMat @'[21] 0+          @?= Right (finMatC @'[1] @'[21])+    , testCase "_finMatCons" $+      (finMatC @'[2,1] @'[7,1] ^. _finMatCons) @?= (finC @2 @7, finMatC @'[1] @'[1])+    , testCase "_finMatCons" $+      (finMatC @'[2,1] @'[7,4] ^. _finMatCons) @?= (finC @2 @7, finMatC @'[1] @'[4])+    , testCase "_finMatCons" $+      (finMatC @'[2,2] @'[7,2] ^. _finMatCons) @?= (finC @2 @7, finMatC @'[2] @'[2])++    , testCase "_finMatCons" $+      (finMatC @'[2,4] @'[7,4] ^. _finMatCons) @?= (finC @2 @7, finMatC @'[4] @'[4])     ]  fmi237' :: NonEmpty (FinMat '[2, 3, 7])@@ -461,3 +470,4 @@  fmiNS :: NonEmpty Int -> NonEmpty (NonEmpty Int) fmiNS = traverse (N.fromList . enumFromTo 1)+

@@ -1,5 +1,8 @@ {-# OPTIONS -Wno-orphans #-} {-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE OverloadedStrings #-}@@ -7,6 +10,7 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}  module TestMat where @@ -40,6 +44,9 @@ import Test.Tasty import Test.Tasty.HUnit import qualified Test.Tasty.QuickCheck as TQ+import Unsafe.Coerce+import qualified GHC.TypeNats as GN+import Data.Proxy  instance (NS ns, Arbitrary a) => Arbitrary (Mat ns a) where   arbitrary = sequenceA $ mat @ns (repeat arbitrary)@@ -126,16 +133,16 @@         matToNestedListC (fmap (show . succ) m35)           @?= [["2", "3", "4", "5", "6"], ["7", "8", "9", "10", "11"], ["12", "13", "14", "15", "16"]]     , testCase "totuple" $-        toTupleC (mat' @'[2, 3, 2] [1 :: Int .. 12])+        toTupleC (mat' @'[2, 3, 2] @Int [1 .. 12])           @?= (((1, 2), (3, 4), (5, 6)), ((7, 8), (9, 10), (11, 12)))     , testCase "fromtuple" $         fromTupleC (((1, 2), (3, 4), (5, 6)), ((7, 8), (9, 10), (11, 12)))-          @?= mat' @'[2, 3, 2] [1 :: Int .. 12]+          @?= mat' @'[2, 3, 2] @Int [1 .. 12]     , testCase "change row" $-        (mat' @'[3, 4] [1 :: Int .. 12] & ixSlice @'[2, 3] .~ 999)+        (mat' @'[3, 4] @Int [1 .. 12] & ixSlice @'[2, 3] .~ 999)           @?= mat' @'[3, 4] [1, 2, 3, 4, 5, 6, 999, 8, 9, 10, 11, 12]     , testCase "change row" $-        (mat' @'[3, 4] [1 :: Int .. 12] & ixSlice @'[1] *~ 999)+        (mat' @'[3, 4] @Int [1 .. 12] & ixSlice @'[1] *~ 999)           @?= mat' @'[3, 4] [999, 1998, 2997, 3996, 5, 6, 7, 8, 9, 10, 11, 12]     , testCase "change row" $         m345 ^. ixSlice @'[2, 3]@@ -144,16 +151,16 @@         (m35 & ixSlice @'[2] . traverse *~ 100)           @?= mat' @'[3, 5] [1, 2, 3, 4, 5, 600, 700, 800, 900, 1000, 11, 12, 13, 14, 15]     , testCase "change row" $-        (mat' @'[2, 1, 2, 3, 4] [1 :: Int .. 48] & ixSlice @'[2, 1, 1] . traverse *~ 100)+        (mat' @'[2, 1, 2, 3, 4] @Int [1 .. 48] & ixSlice @'[2, 1, 1] . traverse *~ 100)           @?= mat' @'[2, 1, 2, 3, 4] [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 2500, 2600, 2700, 2800, 2900, 3000, 3100, 3200, 3300, 3400, 3500, 3600, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48]     , testCase "change row" $         m345 ^. ixSlice @'[2]           @?= mat' @'[4, 5] ['U' .. 'h']     , testCase "not as useful: nests all stuff" $-        fmap sum (matToNestedVecC @'[2, 3] (mat' [1 :: Int .. 6]))+        fmap sum (matToNestedVecC @'[2, 3] (mat' @_ @Int [1 .. 6]))           @?= 6 .| 15     , testCase "mapLeaf: change the lowest rows into lists" $-        mapLeaf (const sum) (mat' @'[4, 3] [1 :: Int .. 12])+        mapLeaf (const sum) (mat' @'[4, 3] @Int [1 .. 12])           @?= mat' @'[4] [6, 15, 24, 33]     , testCase "mapLeafSimple" $         mapLeafSimple (fmap . (,) . fmPos) (gen' @(NN 43) id)@@ -174,19 +181,19 @@         foldMapLeafR (\i m -> [(fmPos i, sum m, toList m)]) (mm @(NN 234))           @?= [(20, 90, [21, 22, 23, 24]), (16, 74, [17, 18, 19, 20]), (12, 58, [13, 14, 15, 16]), (8, 42, [9, 10, 11, 12]), (4, 26, [5, 6, 7, 8]), (0, 10, [1, 2, 3, 4])]     , testCase "addition" $-        mat' @'[2, 3] [1 .. 6] + mat' [100 :: Int .. 105]+        mat' @'[2, 3] @Int [1 .. 6] + mat' [100 .. 105]           @?= mat' [101, 103, 105, 107, 109, 111]     , testCase "multiplication" $-        mat' @'[2, 3] [1 .. 6] * mat' [100 :: Int .. 105]+        mat' @'[2, 3] @Int [1 .. 6] * mat' [100 .. 105]           @?= mat' [100, 202, 306, 412, 520, 630] -- note: have to use mat' for inference to work     , testCase "transpose" $-        transposeMat (mat' @'[2, 3] [1 :: Int .. 6])+        transposeMat (mat' @'[2, 3] @Int [1 .. 6])           @?= mat' [1, 4, 2, 5, 3, 6]     , testCase "transpose iso" $         transposeMat (transposeMat m345)           @?= m345     , testCase "diagonal" $-        diagonal (mat' @'[3, 3, 4] [1 :: Int .. 36])+        diagonal (mat' @'[3, 3, 4] @Int [1 .. 36])           @?= mat' [1, 2, 3, 4, 17, 18, 19, 20, 33, 34, 35, 36]     , testCase "diagonal" $         diagonal (gen @'[4, 4] succ)@@ -201,31 +208,31 @@         finMatMatrix @'[2, 3, 1]           @?= mat' (toList (N.map (fr . (nonEmptyToFinMat <=< toPositives)) ([1, 1, 1] :| [[1, 2, 1], [1, 3, 1], [2, 1, 1], [2, 2, 1], [2, 3, 1]])))     , testCase "insert row" $-        insertRow @2 (mat' @'[3, 4] [100 .. 111]) (mat' @'[2, 3, 4] [1 :: Int .. 24])+        insertRow @2 (mat' @'[3, 4] [100 .. 111]) (mat' @'[2, 3, 4] @Int [1 .. 24])           @?= mat' [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24]     , testCase "insert column" $-        insertCol @2 (mat' @'[2, 4] [100 .. 107]) (mat' @'[2, 3, 4] [1 :: Int .. 24])+        insertCol @2 (mat' @'[2, 4] [100 .. 107]) (mat' @'[2, 3, 4] @Int [1 .. 24])           @?= mat' [1, 2, 3, 4, 100, 101, 102, 103, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 104, 105, 106, 107, 17, 18, 19, 20, 21, 22, 23, 24]     , testCase "delete row" $-        deleteRow @2 (mat' @'[2, 3, 4] [1 :: Int .. 24])+        deleteRow @2 (mat' @'[2, 3, 4] @Int [1 .. 24])           @?= mat' [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12]     , testCase "insert/delete row" $         deleteRow @2 (insertRow @2 (mat' @'[4, 5] [100 .. 119]) m345')           @?= m345'     , testCase "to nested lists" $-        matToNestedListC (mat' @'[2, 3, 4] [1 :: Int .. 24])+        matToNestedListC (mat' @'[2, 3, 4] @Int [1 .. 24])           @?= [[[1, 2, 3, 4], [5, 6, 7, 8], [9, 10, 11, 12]], [[13, 14, 15, 16], [17, 18, 19, 20], [21, 22, 23, 24]]]     , testCase "concat vertically" $-        matToNestedListC (appendV (mat' @'[2, 3, 2] [1 .. 12]) (mat' @'[5, 3, 2] [100 :: Int .. 129]))+        matToNestedListC (appendV (mat' @'[2, 3, 2] [1 .. 12]) (mat' @'[5, 3, 2] @Int [100 .. 129]))           @?= [[[1, 2], [3, 4], [5, 6]], [[7, 8], [9, 10], [11, 12]], [[100, 101], [102, 103], [104, 105]], [[106, 107], [108, 109], [110, 111]], [[112, 113], [114, 115], [116, 117]], [[118, 119], [120, 121], [122, 123]], [[124, 125], [126, 127], [128, 129]]]     , testCase "concat vertically" $-        matToNestedListC (appendV (mat' @'[2, 3] [1 .. 6]) (mat' @'[7, 3] [100 :: Int .. 120]))+        matToNestedListC (appendV (mat' @'[2, 3] [1 .. 6]) (mat' @'[7, 3] @Int [100 .. 120]))           @?= [[1, 2, 3], [4, 5, 6], [100, 101, 102], [103, 104, 105], [106, 107, 108], [109, 110, 111], [112, 113, 114], [115, 116, 117], [118, 119, 120]]     , testCase "concat horizontally" $-        matToNestedListC (appendH (mat' @'[5, 2, 2] [1 .. 20]) (mat' @'[5, 3, 2] [100 :: Int .. 129]))+        matToNestedListC (appendH (mat' @'[5, 2, 2] [1 .. 20]) (mat' @'[5, 3, 2] @Int [100 .. 129]))           @?= [[[1, 2], [3, 4], [100, 101], [102, 103], [104, 105]], [[5, 6], [7, 8], [106, 107], [108, 109], [110, 111]], [[9, 10], [11, 12], [112, 113], [114, 115], [116, 117]], [[13, 14], [15, 16], [118, 119], [120, 121], [122, 123]], [[17, 18], [19, 20], [124, 125], [126, 127], [128, 129]]]     , testCase "concat horizontally" $-        matToNestedListC (appendH (mat' @'[3, 2] [1 .. 6]) (mat' @'[3, 7] [100 :: Int .. 120]))+        matToNestedListC (appendH (mat' @'[3, 2] @Int [1 .. 6]) (mat' @'[3, 7] @Int [100 .. 120]))           @?= [[1, 2, 100, 101, 102, 103, 104, 105, 106], [3, 4, 107, 108, 109, 110, 111, 112, 113], [5, 6, 114, 115, 116, 117, 118, 119, 120]]     , testCase "consMat" $         (gen @'[3, 4] succ ^. consMat)@@ -282,20 +289,20 @@         nestedVecToMatC (matToNestedVecC m345)           @?= m345 -- works without @'[3,4,5] cos @?= tells us the type     , testCase "delete item from 1d mat'" $-        deleteRow @4 (mat' @'[10] [1 :: Int .. 10])+        deleteRow @4 (mat' @'[10] @Int [1 .. 10])           @?= mat' [1, 2, 3, 5, 6, 7, 8, 9, 10]     , testCase "redim" $-        redim (mat' @'[2, 3, 5] [1 :: Int .. 30])-          @?= mat' @'[6, 5] [1 :: Int .. 30]+        redim (mat' @'[2, 3, 5] @Int [1 .. 30])+          @?= mat' @'[6, 5] @Int [1 .. 30]     , testCase "redim" $-        redim (mat' @'[5, 9, 4] [1 :: Int .. 180])-          @?= mat' @'[3, 6, 10] [1 :: Int .. 180]+        redim (mat' @'[5, 9, 4] @Int [1 .. 180])+          @?= mat' @'[3, 6, 10] @Int [1 .. 180]     , testCase "redim" $-        redim (mat' @'[18] [1 :: Int .. 18])-          @?= mat' @'[3, 2, 3] [1 :: Int .. 18]+        redim (mat' @'[18] @Int [1 .. 18])+          @?= mat' @'[3, 2, 3] @Int [1 .. 18]     , testCase "redim" $-        redim (mat' @'[3, 2, 3] [1 :: Int .. 18])-          @?= mat' @'[18] [1 :: Int .. 18]+        redim (mat' @'[3, 2, 3] @Int [1 .. 18])+          @?= mat' @'[18] @Int [1 .. 18]     , testCase "diagonal" $         diagonal (gen @'[4, 4] succ)           @?= mat' @'[4] [1, 6, 11, 16]@@ -306,7 +313,7 @@         diagonal (mm @(NN 99))           @?= mat' @'[9] [1, 11, 21, 31, 41, 51, 61, 71, 81]     , testCase "multMat" $-        multMat (mat' @'[2, 5] [1 :: Int .. 10]) (mat' @'[5, 6] [1 :: Int .. 30])+        multMat (mat' @'[2, 5] @Int [1 .. 10]) (mat' @'[5, 6] @Int [1 .. 30])           @?= mat' @'[2, 6] [255, 270, 285, 300, 315, 330, 580, 620, 660, 700, 740, 780]     , testCase "universe1 enum" $         toNonEmpty (finMatMatrix @'[2, 3, 7])@@ -315,16 +322,16 @@         toList (finMatMatrix @'[2, 3, 7])           @?= toList fmi237'     , testCase "D3" $-        mat' @(D3 2 3 4) [1 :: Int .. 24]+        mat' @(D3 2 3 4) @Int [1 .. 24]           @?= mat' @'[2, 3, 4] [1 .. 24]     , testCase "ixMat" $-        (mat' @'[2, 3, 4] [1 :: Int .. 24] & ixMat (finMatC @'[2, 3, 1]) +~ 100)+        (mat' @'[2, 3, 4] @Int [1 .. 24] & ixMat (finMatC @'[2, 3, 1]) +~ 100)           @?= mat' @'[2, 3, 4] [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 121, 22, 23, 24]     , testCase "ixMat" $-        (mat' @'[2, 3, 4] [1 :: Int .. 24] & ixMat (finMatC @'[2, 3, 4]) +~ 100)+        (mat' @'[2, 3, 4] @Int [1 .. 24] & ixMat (finMatC @'[2, 3, 4]) +~ 100)           @?= mat' @'[2, 3, 4] [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 124]     , testCase "read" $-        (read @(Mat (D1 4) Int) $ show $ mat' @'[4] [1 :: Int .. 4])+        (read @(Mat (D1 4) Int) $ show $ mat' @'[4] @Int [1 .. 4])           @?= (1 .: 2 .: 3 .| 4)     , testCase "read" $         let m = gen' @'[1] id@@ -345,10 +352,10 @@         let m = ('x', True, ['a' .. 'z'], gen' @'[1, 2, 3] id, False)          in read (show m) @?= m     , testCase "read" $-        let m = mat' @'[4, 5] [1 :: Int .. 20]+        let m = mat' @'[4, 5] @Int [1 .. 20]          in read @(Mat (D2 4 5) Int) (show m) @?= m     , testCase "read" $-        let m = mat' @'[1, 2, 3, 4] [1 :: Int .. 24]+        let m = mat' @'[1, 2, 3, 4] @Int [1 .. 24]          in read (show m) @?= m     , testCase "read" $         let m = toND @1 (mm @(NN 2352))@@ -361,15 +368,15 @@          in read (show m) @?= m     , testCase "sortByRows" $         sortByRows (flip compare) (mat' @'[4, 2] [10, 9, 1, 2, 100, 200, 300, 400])-          @?= mat' [10, 9, 2, 1, 200, 100, 400, 300 :: Int]+          @?= mat' @_ @Int [10, 9, 2, 1, 200, 100, 400, 300]     , testCase "sortByT" $-        sortByT (flip compare) (mat' @'[4] [10 :: Int, 9, 1, 2])+        sortByT (flip compare) (mat' @'[4] @Int [10, 9, 1, 2])           @?= (10 .: 9 .: 2 .| 1)     , testCase "sortByT" $-        sortByT compare (mat' @'[4] [10 :: Int, 9, 1, 2])+        sortByT compare (mat' @'[4] @Int [10, 9, 1, 2])           @?= (1 .: 2 .: 9 .| 10)     , testCase "sortByRows" $-        sortByRows compare (mat' @'[4, 2] [10 :: Int, 9, 1, 2, 100, 200, 300, 400])+        sortByRows compare (mat' @'[4, 2] @Int [10, 9, 1, 2, 100, 200, 300, 400])           @?= mat' [9, 10, 1, 2, 100, 200, 300, 400]     , testCase "totuple" $         toTupleC (vec' "abc")@@ -381,7 +388,7 @@         fromTupleC (One 'a')           @?= se1 'a'     , testCase "fromtuple" $-        fromTupleC (1, 2, 3 :: Int)+        fromTupleC @_ @Int (1, 2, 3)           @?= 1 .: 2 .| 3     , testCase "consMat" $         (mat' @'[1] "x" ^. consMat)@@ -426,19 +433,19 @@         (mat' @'[5, 3] ['A' .. 'O'] ^. snocMat)           @?= (mat' @'[4, 3] ['A' .. 'L'], mat' @'[3] "MNO")     , testCase "field lens" $-        (mat' @'[3, 3, 4] [1 :: Int .. 36] ^. _r3 . _r1)+        (mat' @'[3, 3, 4] @Int [1 .. 36] ^. _r3 . _r1)           @?= vec' @4 [25, 26, 27, 28]     , testCase "field lens" $-        (mat' @'[3, 3, 4] [1 :: Int .. 36] ^. _r3 . _r1)+        (mat' @'[3, 3, 4] @Int [1 .. 36] ^. _r3 . _r1)           @?= vec' @4 [25, 26, 27, 28]     , testCase "field lens update" $         (mat' @'[2, 1, 4] ['A' .. 'H'] & _r2 . _r1 . _r3 %~ toLower)           @?= mat' "ABCDEFgH"     , testCase "field lens" $-        (mat' @'[7] [1 :: Int .. 7] ^. _r3)+        (mat' @'[7] @Int [1 .. 7] ^. _r3)           @?= 3     , testCase "field lens" $-        (mat' @'[7, 4] [1 :: Int .. 28] ^. _r3 . _r2)+        (mat' @'[7, 4] @Int [1 .. 28] ^. _r3 . _r2)           @?= 10     , testCase "subsetRows" $         subsetRows @2 @2 (gen @'[2, 5] succ)@@ -674,13 +681,13 @@         (('x', Eof1) ^. from (consMat @'[1]))           @?= se1 'x'     , testCase "nestedListToMatC" $-        nestedListToMatC @'[2, 3, 5] [[[1 :: Int, 2, 3, 4, 5], [6, 7, 8, 9, 10], [11, 12, 13, 14, 15]], [[16, 17, 18, 19, 20], [21, 22, 23, 24, 25], [26, 27, 28, 29, 30]]]+        nestedListToMatC @'[2, 3, 5] @Int [[[1, 2, 3, 4, 5], [6, 7, 8, 9, 10], [11, 12, 13, 14, 15]], [[16, 17, 18, 19, 20], [21, 22, 23, 24, 25], [26, 27, 28, 29, 30]]]           @?= Right (mat' @'[2, 3, 5] [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30])     , testCase "nestedListToMatC" $-        nestedListToMatC @'[3, 3, 5] [[[1 :: Int, 2, 3, 4, 5], [6, 7, 8, 9, 10], [11, 12, 13, 14, 15]], [[16, 17, 18, 19, 20], [21, 22, 23, 24, 25], [26, 27, 28, 29, 30]]]+        nestedListToMatC @'[3, 3, 5] @Int [[[1, 2, 3, 4, 5], [6, 7, 8, 9, 10], [11, 12, 13, 14, 15]], [[16, 17, 18, 19, 20], [21, 22, 23, 24, 25], [26, 27, 28, 29, 30]]]           @?= Left "LT: not enough elements: expected 3 found 2"     , testCase "nestedListToMatC" $-        nestedListToMatC @'[2, 3, 6] [[[1 :: Int, 2, 3, 4, 5], [6, 7, 8, 9, 10], [11, 12, 13, 14, 15]], [[16, 17, 18, 19, 20], [21, 22, 23, 24, 25], [26, 27, 28, 29, 30]]]+        nestedListToMatC @'[2, 3, 6] @Int [[[1, 2, 3, 4, 5], [6, 7, 8, 9, 10], [11, 12, 13, 14, 15]], [[16, 17, 18, 19, 20], [21, 22, 23, 24, 25], [26, 27, 28, 29, 30]]]           @?= Left "not enough elements: expected 6 found 5"     , testCase "indexRow" $         indexRow (fr $ fin @7 1) (gen' @(NN 73) id)@@ -692,19 +699,19 @@         indexRow (fr $ fin @7 7) (gen' @(NN 73) id)           @?= vec' [[7, 1], [7, 2], [7, 3]]     , testCase "readVec" $-        readVec @5 @Int (show (mm @(NN 5))) @?= [(vec' [1 .. 5], "")]+        readVec @5 @Int (show (vec' @5 [1::Int ..5])) @?= [(vec' [1 .. 5], "")]     , testCase "readMat2" $         let m = mat' @'[3, 7] ['a' .. 'u']          in readMat2 @3 @7 @Char (show m ++ "xyz") @?= [(m, "xyz")]     , testCase "readVec" $         let m = mat' @'[7] ['a' .. 'g']          in readVec @7 @Char (show m ++ " xyz") @?= [(m, " xyz")]-    , testCase "readMat2" $-        let m = mm @(NN 372)-         in readMat @(NN 372) @Int (show m ++ "xyz") @?= [(m, "xyz")] -- dont need type application but here we have inference+    , testCase "readMat" $+        let m = mat' @'[3,7,2] [1::Int .. 42]+         in readMat @'[3,7,2] @Int (show m ++ "xyz") @?= [(m, "xyz")] -- dont need type application but here we have inference     , testCase "readMat12" $-        let m = toVec (mm @(NN 372))-         in readVec @3 @(Mat2 7 2 Int) (show m ++ "xyz") @?= [(m, "xyz")] -- dont need type application but here we have inference+        let m = mat' @'[3,7,2] [1::Int .. 42]+         in readMat @'[3,7,2] @Int (show m ++ "xyz") @?= [(m, "xyz")] -- dont need type application but here we have inference     , testCase "readMat3456" $         let m = toMat2 (mm @(NN 3456))          in readMat2 @3 @4 @(Mat2 5 6 Int) (show m ++ "xyz") @?= [(m, "xyz")] -- dont need type application but here we have inference@@ -722,19 +729,19 @@           @?= vec' @1 [99]     , testCase "(.:)" $         (12 .: 44 .| 99)-          @?= vec' @3 [12 :: Int, 44, 99]+          @?= vec' @3 @Int [12, 44, 99]     , testCase "(.:)" $         (5 .| 10 .:: 15 .| 20 .|| (25 .| 30))-          @?= mat2' @3 @2 [5 :: Int, 10, 15, 20, 25, 30]+          @?= mat2' @3 @2 @Int [5, 10, 15, 20, 25, 30]     , testCase "(.:)" $         se2 (5 .| 10 .:: 15 .| 20 .|| (25 .| 30))-          @?= mat' @'[1, 3, 2] [5 :: Int, 10, 15, 20, 25, 30]+          @?= mat' @'[1, 3, 2] @Int [5, 10, 15, 20, 25, 30]     , testCase "nestedListToMatValidated" $         let x = [[[[1 :: Int, 2, 3, 4], [5, 6, 7, 8], [9, 10, 11, 12]], [[13, 14, 15, 16], [17, 18, 19, 20], [21, 22, 23, 24, 25, 26, 27]]]]-         in nestedListToMatValidated @(NN 1234) x @?= Left "validateNestedListC: lengths=[4,4,4,4,4,7] ixes=[1P,2P,3P]"+         in nestedListToMatValidated @(NN 1234) x @?= Left "validateNestedListC: lengths=[4,4,4,4,4,7] ixes=[_1P,_2P,_3P]"     , testCase "nestedListToMatValidated" $         let x = [[[[1 :: Int, 2, 3, 4], [5, 6, 7, 8], [9, 10, 11, 12]], [[13, 14, 15, 16], [17, 18, 19, 20], []]]]-         in nestedListToMatValidated @(NN 1234) x @?= Left "validateNestedListC: lengths=[4,4,4,4,4,0] ixes=[1P,2P,3P]"+         in nestedListToMatValidated @(NN 1234) x @?= Left "validateNestedListC: lengths=[4,4,4,4,4,0] ixes=[_1P,_2P,_3P]"     , testCase "nestedListToMatValidated" $         let x = [[[[1 :: Int, 2, 3, 4], [5, 6, 7, 8], [9, 10, 11, 12]], [[13, 14, 15, 16], [17, 18, 19, 20], [21, 22, 23, 24]]]]          in nestedListToMatValidated @(NN 1234) x @?= Right (mat' @'[1, 2, 3, 4] [1 .. 24])@@ -812,7 +819,7 @@         unfoldrRep @(Vec 5) (\i s -> (drop 1 s, (fmPos i, head s))) ['a' .. 'h']           @?= ("fgh", vec' @5 [(0, 'e'), (1, 'd'), (2, 'c'), (3, 'b'), (4, 'a')])     , testCase "fillTraversable" $-        fillTraversable @(MatN 234) (pure ()) [1 :: Int .. 40]+        fillTraversable @(MatN 234) @Int (pure ()) [1.. 40]           @?= Right ([25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40], mat' @'[2, 3, 4] [1 .. 24])     , testCase "toInteger1" $         toInteger1 (pure @(Mat2 4 2) EQ)@@ -895,14 +902,98 @@     , testCase "fromInteger1" $         fromInteger1 (minBound @(Mat '[2, 5] Int8)) (-1276136419117121619201)           @?= Left "cap=(-1276136419117121619200,1180591620717411303423):padL: negative fill: would need to truncate the data"-     , testCase "lenses mixed" $-       mm @(NN 1234) ^. _r1 . _r1 . _c2 . snocMat . _1 . consMat-        @?= (2,vec @1 [6])-+        mm @(NN 1234) ^. _r1 . _r1 . _c2 . snocMat . _1 . consMat+          @?= (2, vec @1 [6])     , testCase "lenses mixed" $         mm @(NN 734) ^. _c3 . snocMat . _1 . _c4 . _r5-        @?= 60+          @?= 60+    , testCase "withN" $+        let s = withN 5 $ \(_ :: x n) ->+              withN 3 $ \(_ :: x m) ->+                withN 2 $ \(_ :: x p) ->+                  let w1 :: Mat2 n m Int -- if you use let statements then must have signatures else fails with constraints not satisfied+                      w1 = mat2 @n @m [1 ..]+                      w2 :: Mat2 m p Int+                      w2 = mat2 @m @p [10 ..]+                      z = multMat w1 w2+                   in show (fromNSP @'[n, m, p], z)+         in read @(NonEmpty Pos, Mat2 5 2 Int) s+              @?= (_5P :| [_3P, _2P], mat2 @5 @2 [76, 82, 184, 199, 292, 316, 400, 433, 508, 550])+    , testCase "withN" $+        let s = withN 5 $ \(_ :: x n) ->+              withN 3 $ \(_ :: x m) ->+                show (mat2 @n @m @Int [1 ..] `multMat` mat2 @m @n @Int [10 ..])+         in read @(Mat2 5 5 Int) s @?= mat2' @5 @5 [100, 106, 112, 118, 124, 235, 250, 265, 280, 295, 370, 394, 418, 442, 466, 505, 538, 571, 604, 637, 640, 682, 724, 766, 808]+    , testCase "withN" $+        let s = withN 5 $ \(_ :: x n) -> show (vec @n @Int [1 ..])+         in read @(Vec 5 Int) s @?= vec' @5 [1 .. 5]+    , testCase "withN" $+        let s = withN 5 $ \(_ :: x n) ->+              withN 7 $ \(_ :: x m) -> show (mat2 @n @m @Int [1 ..], mat2 @m @n ['a' ..])+         in read @(Mat2 5 7 Int, Mat2 7 5 Char) s @?= (mat2' @5 @7 [1 .. 35], mat2 @7 @5 ['a' ..])+    , testCase "withN2" $+        let z = withN2 4 5 $ \(_ :: p n) (_ :: p m) -> show (mat2 @n @m ['a' ..])+         in read @(Mat2 4 5 Char) z @?= mat2' @4 @5 ['a' .. 't']+    , testCase "withN3" $+        withN3 2 3 4 (\(_ :: z n) (_ :: z m) (_ :: z q) -> fromNSP @'[n, m, q])+          @?= _2P :| [_3P, _4P]+    , testCase "withN3" $+        let z = withN 4 $ \(_ :: p n) -> show (mat2 @2 @n @Int [1..] ^. _row @1)+         in read @(Vec 4 Int) z @?= vec' @4 [1 .. 4]+    , testCase "withN3" $+        let z = withN 4 $ \(_ :: p n) -> show (mat2 @2 @n @Int [1 ..] ^. _row @2)+         in read @(Vec 4 Int) z @?= vec' @4 [5 .. 8]++    , testCase "withNMin3" $+         let z = withNMin3 5 (\(_ :: p n) -> withNMin3 4 (\(_ :: p m) -> show (mat2 @n @m [1::Int ..] ^. _c2)))+         in read @(Vec 5 Int) z @?= vec' @5 [2,6,10,14,18]++    , testCase "rotateLeft rotateRight" $+        let z = mm @(NN 57)+        in rotateLeft (rotateRight z) @?= z+    , testCase "rotateLeft" $+        rotateLeft (mm @(NN 35))+          @?= mat2' @5 @3 [5,10,15,4,9,14,3,8,13,2,7,12,1,6,11]+      ,testCase "rotateRight" $+        rotateRight (mm @(NN 35))+          @?= mat2' @5 @3 [11,6,1,12,7,2,13,8,3,14,9,4,15,10,5]+    , testCase "rotateRight transpose rotateRight" $+        let z = mm @(NN 57)+        in (transposeMat . rotateLeft . transposeMat) z  @?= rotateRight z++    , testCase "determinant" $+        determinant (mat2' @3 @3 @Int [2, -3, 1, 2, 0, -1, 1, 4, 5])+          @?= 49+    , testCase "determinant" $+        determinant (mat2' @3 @3 @Int [1, 3, 2, -3, -1, -3, 2, 3, 1])+          @?= (-15)+    , testCase "determinant" $+        determinant (mat2' @4 @4 @Int [3, 2, 0, 1, 4, 0, 1, 2, 3, 0, 2, 1, 9, 2, 3, 1])+          @?= 24+    , testCase "determinant" $+        determinant (mat2' @4 @4 @Int [1, 0, 2, -1, 3, 0, 0, 5, 2, 1, 4, -3, 1, 0, 5, 0])+          @?= 30+    , testCase "determinant" $+        determinant (mat2' @4 @4 @Int [1, 0, 4, -6, 2, 5, 0, 3, -1, 2, 3, 5, 2, 1, -2, 3])+          @?= 318+    , testCase "determinant" $+        determinant (mat2' @2 @2 @Int [1, 2, 3, 4])+          @?= (-2)++    , testCase "determinant" $+        determinant (mat2' @1 @1 @Int [-5])+          @?= (-5)+    , testCase "deleteColumnL" $+        deleteColumnL _2P 1 [1,2::Int] @?= [1]+    , testCase "deleteColumnL" $+        deleteColumnL _2P 0 [1,2::Int] @?= [2]+    , testCase "deleteColumnL" $+        deleteColumnL _3P 1 [1::Int .. 12] @?= [1,3,4,6,7,9,10,12]+    , testCase "deleteColumnL" $+        deleteColumnL _2P 1 [1..10::Int] @?=  [1,3,5,7,9]+    , testCase "deleteColumnL" $+        deleteColumnL _1P 0 [1::Int] @?= []     ]  suiteCheckers :: TestTree@@ -920,3 +1011,55 @@  fmi237 :: NonEmpty (NonEmpty Int) fmi237 = fmap N.fromList ([1, 1, 1] :| [[1, 1, 2], [1, 1, 3], [1, 1, 4], [1, 1, 5], [1, 1, 6], [1, 1, 7], [1, 2, 1], [1, 2, 2], [1, 2, 3], [1, 2, 4], [1, 2, 5], [1, 2, 6], [1, 2, 7], [1, 3, 1], [1, 3, 2], [1, 3, 3], [1, 3, 4], [1, 3, 5], [1, 3, 6], [1, 3, 7], [2, 1, 1], [2, 1, 2], [2, 1, 3], [2, 1, 4], [2, 1, 5], [2, 1, 6], [2, 1, 7], [2, 2, 1], [2, 2, 2], [2, 2, 3], [2, 2, 4], [2, 2, 5], [2, 2, 6], [2, 2, 7], [2, 3, 1], [2, 3, 2], [2, 3, 3], [2, 3, 4], [2, 3, 5], [2, 3, 6], [2, 3, 7]])++-- ghc 9.2 needs explicit kinds for "i" and "n"+overrideDictPositive :: forall (i :: Nat) (n :: Nat) p . p n -> (i GN.<=? n) :~: 'True+overrideDictPositive _ = unsafeCoerce Refl++-- | lift a positive number to the typelevel+withN :: Int -> (forall n. FinC 1 n => Proxy n -> x) -> x+withN i f+  | i <= 1 = normalError $ "withN: index must be at least 1:found " ++ show i+  | otherwise =+      case GN.someNatVal (toEnum i) of+        GN.SomeNat (pn :: Proxy n) ->+          case overrideDictPositive @1 pn of+            Refl -> f (Proxy @n)++-- | lift a positive number to the typelevel+withNMin2 :: Int -> (forall n . (FinC 2 n, FinC 1 n) => Proxy n -> x) -> x+withNMin2 i f+  | i < 2 = normalError $ "withNMin2: index must be at least 2:found " ++ show i+  | otherwise =+      case GN.someNatVal (toEnum i) of+        GN.SomeNat (pn :: Proxy n) ->+          case overrideDictPositive @1 pn of+            Refl ->+              case overrideDictPositive @2 pn of+                 Refl -> f (Proxy @n)++withNMin3 :: Int -> (forall n . (FinC 3 n, FinC 2 n, FinC 1 n) => Proxy n -> x) -> x+withNMin3 i f+  | i < 3 = normalError $ "withNMin3: index must be at least 3:found " ++ show i+  | otherwise =+      case GN.someNatVal (toEnum i) of+        GN.SomeNat (pn :: Proxy n) ->+          case overrideDictPositive @1 pn of+            Refl ->+              case overrideDictPositive @2 pn of+                Refl ->+                  case overrideDictPositive @3 pn of+                    Refl -> f (Proxy @n)++-- | lift two positive numbers to the typelevel+withN2 :: Int -> Int -> (forall n m. (FinC 1 n, FinC 1 m) => Proxy n -> Proxy m -> x) -> x+withN2 i j f = withN i $ \p1 -> withN j $ \p2 -> f p1 p2++-- | lift three positive numbers to the typelevel+withN3 :: Int -> Int -> Int -> (forall n m p. (FinC 1 n, FinC 1 m, FinC 1 p) => Proxy n -> Proxy m -> Proxy p -> x) -> x+withN3 i j k f = withN i $ \p1 -> withN j $ \p2 -> withN k $ \p3 -> f p1 p2 p3++-- | lift four positive numbers to the typelevel+withN4 :: Int -> Int -> Int -> Int -> (forall n m p q. (FinC 1 n, FinC 1 m, FinC 1 p, FinC 1 q) => Proxy n -> Proxy m -> Proxy p -> Proxy q -> x) -> x+withN4 i j k l f = withN i $ \p1 -> withN j $ \p2 -> withN k $ \p3 -> withN l $ \p4 -> f p1 p2 p3 p4+

@@ -43,5 +43,5 @@         validateNestedList ([] :: [()])           @?= Left "validateNestedListC: ixes=[]:no data!"     , testCase "validateNestedList" $-        validateNestedList [[1 :: Int, 2], [1, 2], [1, 2, 3]] @?= Left "validateNestedListC: lengths=[2,2,3] ixes=[3P]"+        validateNestedList [[1 :: Int, 2], [1, 2], [1, 2, 3]] @?= Left "validateNestedListC: lengths=[2,2,3] ixes=[_3P]"     ]