Copyright | (c) Grant Weyburne 2022 |
---|---|
License | BSD-3 |
Safe Haskell | None |
Language | Haskell2010 |
Synopsis
- data FinMat ns
- fmPos :: FinMat ns -> Int
- fmNS :: FinMat ns -> NonEmpty Pos
- pattern FinMat :: forall (ns :: [Nat]). Int -> NonEmpty Pos -> FinMat ns
- pattern FinMatU :: forall (ns :: [Nat]). (HasCallStack, NS ns) => Int -> NonEmpty Pos -> FinMat ns
- class FinMatC is ns where
- mkFinMat :: Int -> NonEmpty Pos -> Either String (FinMat ns)
- mkFinMatC :: forall ns. NS ns => Int -> NonEmpty Pos -> Either String (FinMat ns)
- finMat :: forall ns. NS ns => Int -> Either String (FinMat ns)
- toFinMatFromPos :: forall (i :: Nat) ns. (NS ns, i <! ProductT ns) => FinMat ns
- finMatToNonEmpty :: forall ns. FinMat ns -> NonEmpty Pos
- nonEmptyToFinMat :: forall ns. NS ns => NonEmpty Pos -> Either String (FinMat ns)
- nonEmptyToFinMat' :: NonEmpty Pos -> NonEmpty Pos -> Either String (FinMat ns)
- showFinMat :: FinMat ns -> String
- readFinMatP :: forall ns. NS ns => ReadP (FinMat ns)
- readFinMat :: NS ns => ReadS (FinMat ns)
- showFinMat' :: forall ns. FinMat ns -> String
- class NS (ns :: [Nat]) where
- class NSRangeC i ns
- relPos :: Foldable1 t => t (Pos, Pos) -> (Pos, Int)
- finMatFinSet :: forall i n ns. (PosC i, NSRangeC (NatToPeanoT i) ns) => FinMat ns -> Fin n -> FinMat ns
- finMatFinGet :: forall i n ns. (PosC i, NSRangeC (NatToPeanoT i) ns) => FinMat ns -> Fin n
- _finMatCons :: forall n n1 ns. (NS (n1 ': ns), PosC n) => Iso' (FinMat (n ': (n1 ': ns))) (Fin n, FinMat (n1 ': ns))
- _finMatFin :: forall i n ns. (PosC i, NSRangeC (NatToPeanoT i) ns) => Lens' (FinMat ns) (Fin n)
- _i1 :: Lens' (FinMat (n ': ns)) (Fin n)
- _i2 :: Lens' (FinMat (n1 ': (n ': ns))) (Fin n)
- _i3 :: Lens' (FinMat (n1 ': (n2 ': (n ': ns)))) (Fin n)
- _i4 :: Lens' (FinMat (n1 ': (n2 ': (n3 ': (n ': ns))))) (Fin n)
- _i5 :: Lens' (FinMat (n1 ': (n2 ': (n3 ': (n4 ': (n ': ns)))))) (Fin n)
- _i6 :: Lens' (FinMat (n1 ': (n2 ': (n3 ': (n4 ': (n5 ': (n ': ns))))))) (Fin n)
- _i7 :: Lens' (FinMat (n1 ': (n2 ': (n3 ': (n4 ': (n5 ': (n6 ': (n ': ns)))))))) (Fin n)
- _i8 :: Lens' (FinMat (n1 ': (n2 ': (n3 ': (n4 ': (n5 ': (n6 ': (n7 ': (n ': ns))))))))) (Fin n)
- _i9 :: Lens' (FinMat (n1 ': (n2 ': (n3 ': (n4 ': (n5 ': (n6 ': (n7 ': (n8 ': (n ': ns)))))))))) (Fin n)
- _i10 :: Lens' (FinMat (n1 ': (n2 ': (n3 ': (n4 ': (n5 ': (n6 ': (n7 ': (n8 ': (n9 ': (n ': ns))))))))))) (Fin n)
core type
definition of the indices of a matrix
Instances
pattern FinMat :: forall (ns :: [Nat]). Int -> NonEmpty Pos -> FinMat ns Source #
readonly pattern synonym for finmatrix
pattern FinMatU :: forall (ns :: [Nat]). (HasCallStack, NS ns) => Int -> NonEmpty Pos -> FinMat ns Source #
pattern synonym for validating the finmatrix before construction but uses an extra NS
constraint to check "ns"
constructors
class FinMatC is ns where Source #
convert type level indices into a FinMat
Instances
(TypeError ('Text "FinMatC '[] '[]: empty index 'is' and 'ns'") :: Constraint) => FinMatC ('[] :: [k]) ('[] :: [Nat]) Source # | |
Defined in Cybus.FinMat | |
(TypeError ('Text "FinMatC '[] (n ': ns): empty index 'is'") :: Constraint) => FinMatC ('[] :: [k]) (n ': ns) Source # | |
Defined in Cybus.FinMat | |
(TypeError ('Text "FinMatC (i ': is) '[]: empty index 'ns'") :: Constraint) => FinMatC (i ': is :: [a]) ('[] :: [Nat]) Source # | |
Defined in Cybus.FinMat | |
(is' ~ (i ': is), ns' ~ (n ': ns), NS is', NS ns', FinMatT is' ns' 1 is' ns') => FinMatC (i ': is :: [Nat]) (n ': ns) Source # | |
Defined in Cybus.FinMat |
mkFinMat :: Int -> NonEmpty Pos -> Either String (FinMat ns) Source #
create a FinMat value level "i" and "ns" values and validate that "i" is in range
mkFinMatC :: forall ns. NS ns => Int -> NonEmpty Pos -> Either String (FinMat ns) Source #
create a FinMat value level "i" and "ns" values and validate against expected "ns"
toFinMatFromPos :: forall (i :: Nat) ns. (NS ns, i <! ProductT ns) => FinMat ns Source #
create a FinMat using a relative type level index
conversions
finMatToNonEmpty :: forall ns. FinMat ns -> NonEmpty Pos Source #
convert a FinMat into a list of indices
nonEmptyToFinMat :: forall ns. NS ns => NonEmpty Pos -> Either String (FinMat ns) Source #
try to convert a list of indices into a FinMat
nonEmptyToFinMat' :: NonEmpty Pos -> NonEmpty Pos -> Either String (FinMat ns) Source #
try to convert a list of indices into a FinMat
read/show methods
showFinMat :: FinMat ns -> String Source #
pretty print FinMat
showFinMat' :: forall ns. FinMat ns -> String Source #
more detailed pretty print FinMat
miscellaneous
class NS (ns :: [Nat]) where #
conversion from list of Nats to Positives
constrain i within the size of the indices ie "i >= 1 && i <= LengthT ns"
Instances
(TypeError ('Text "NSRangeC '[]: empty indices") :: Constraint) => NSRangeC p ('[] :: [Nat]) Source # | |
Defined in Cybus.FinMat | |
(TypeError ('Text "NSRangeC: zero is not a valid index: index must be one or greater") :: Constraint) => NSRangeC 'Z (n ': ns) Source # | |
Defined in Cybus.FinMat | |
NSRangeC ('S 'Z) (n ': ns) Source # | |
Defined in Cybus.FinMat | |
(TypeError ('Text "NSRangeC: index is larger than the number of matrix indices ns") :: Constraint) => NSRangeC ('S ('S i)) '[n] Source # | |
Defined in Cybus.FinMat | |
NSRangeC ('S i) (m ': ns) => NSRangeC ('S ('S i)) (n ': (m ': ns)) Source # | |
Defined in Cybus.FinMat |
relPos :: Foldable1 t => t (Pos, Pos) -> (Pos, Int) Source #
find the relative position in a matrix index
finMatFinSet :: forall i n ns. (PosC i, NSRangeC (NatToPeanoT i) ns) => FinMat ns -> Fin n -> FinMat ns Source #
set the Fin
at index "i" for the FinMat
finMatFinGet :: forall i n ns. (PosC i, NSRangeC (NatToPeanoT i) ns) => FinMat ns -> Fin n Source #
get the Fin
at index "i" from FinMat
must rely on FinMat to get "n at index i "which saves us pulling "n" from the typelevel ie we can omit PosC n
lens into the matrix indices
_finMatCons :: forall n n1 ns. (NS (n1 ': ns), PosC n) => Iso' (FinMat (n ': (n1 ': ns))) (Fin n, FinMat (n1 ': ns)) Source #
_finMatFin :: forall i n ns. (PosC i, NSRangeC (NatToPeanoT i) ns) => Lens' (FinMat ns) (Fin n) Source #
a lens for accessing the "i" index in a indices of FinMat
_i6 :: Lens' (FinMat (n1 ': (n2 ': (n3 ': (n4 ': (n5 ': (n ': ns))))))) (Fin n) Source #
lens for index 6
_i7 :: Lens' (FinMat (n1 ': (n2 ': (n3 ': (n4 ': (n5 ': (n6 ': (n ': ns)))))))) (Fin n) Source #
lens for index 7
_i8 :: Lens' (FinMat (n1 ': (n2 ': (n3 ': (n4 ': (n5 ': (n6 ': (n7 ': (n ': ns))))))))) (Fin n) Source #
lens for index 8