{-# 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 (
type FinMat,
fmPos,
fmNS,
pattern FinMat,
pattern FinMatU,
FinMatC (..),
mkFinMat,
mkFinMatC,
finMat,
toFinMatFromPos,
finMatToNonEmpty,
nonEmptyToFinMat,
nonEmptyToFinMat',
showFinMat,
readFinMatP,
readFinMat,
showFinMat',
NS (..),
NSRangeC,
relPos,
finMatFinSet,
finMatFinGet,
_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
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)
fmPos :: FinMat ns -> Int
fmPos :: FinMat ns -> Int
fmPos (FinMatUnsafe Int
i NonEmpty Pos
_) = Int
i
fmNS :: FinMat ns -> NonEmpty Pos
fmNS :: FinMat ns -> NonEmpty Pos
fmNS (FinMatUnsafe Int
_ NonEmpty Pos
ns) = NonEmpty Pos
ns
{-# 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 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
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)
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)
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)
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)
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)
)
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
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)
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
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)
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
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
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
"}"
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
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)
_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)
_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)
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
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
_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
_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
_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
_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
_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
_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
_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
_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
_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
_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