Cybus.NatHelper

peano

type family NatToPeanoT n where ...

convert Nat to Peano

Equations

NatToPeanoT 0 = 'Z

NatToPeanoT n = 'S (NatToPeanoT (n - 1))

type family PeanoToNatT n where ...

convert Peano to Nat

Equations

PeanoToNatT 'Z = 0

PeanoToNatT ('S n) = 1 + PeanoToNatT n

data Peano

peano numbers for converting between Nat and peano

Constructors

Z

S !Peano

Instances

Eq Peano

Defined in Cybus.NatHelper

Methods

(==) :: Peano -> Peano -> Bool

(/=) :: Peano -> Peano -> Bool

Ord Peano

Defined in Cybus.NatHelper

Methods

compare :: Peano -> Peano -> Ordering

(<) :: Peano -> Peano -> Bool

(<=) :: Peano -> Peano -> Bool

(>) :: Peano -> Peano -> Bool

(>=) :: Peano -> Peano -> Bool

max :: Peano -> Peano -> Peano

min :: Peano -> Peano -> Peano

Show Peano

Defined in Cybus.NatHelper

Methods

showsPrec :: Int -> Peano -> ShowS

show :: Peano -> String

showList :: [Peano] -> ShowS

arithmetic

type DiffT i j n = (j + 1) - i

find the number of N between "i" and "j" while ensuring i<=j and j<=n

type DiffTC i j n = (i <=! j, j <=! n)

constraint for DiffC with better error messages

type family FacT x where ...

get the factorial of a Nat

Equations

FacT 0 = 1

FacT 1 = 1

FacT n = n * FacT (n - 1)

type (<=!) i n = (FailUnless (i <=? n) (((('Text "i>n" :<>: 'Text ": i=") :<>: 'ShowType i) :<>: 'Text " n=") :<>: 'ShowType n), PosT i)

constraint for ensuring that "i" <= "n"

type (<!) i n = (FailUnless ((i + 1) <=? n) (((('Text "i>=n" :<>: 'Text ": i=") :<>: 'ShowType i) :<>: 'Text " n=") :<>: 'ShowType n), KnownNat i)

constraint for ensuring that "i" <= "n"

type LTEQT msg i n = (FailUnless (i <=? n) ((((('Text "i>n" :<>: 'Text ": i=") :<>: 'ShowType i) :<>: 'Text " n=") :<>: 'ShowType n) :<>: msg), PosT i)

constraint for ensuring that "i" <= "n" with a custom error message

matrix dimension synonyms

type D1 a = a :| '[]

matrix dimension of degree 1

type D2 a b = a :| '[b]

matrix dimension of degree 2

type D3 a b c = a :| '[b, c]

matrix dimension of degree 3

type D4 a b c d = a :| '[b, c, d]

matrix dimension of degree 4

type D5 a b c d e = a :| '[b, c, d, e]

matrix dimension of degree 5

type D6 a b c d e f = a :| '[b, c, d, e, f]

matrix dimension of degree 6

type D7 a b c d e f g = a :| '[b, c, d, e, f, g]

matrix dimension of degree 7

type D8 a b c d e f g h = a :| '[b, c, d, e, f, g, h]

matrix dimension of degree 8

type D9 a b c d e f g h i = a :| '[b, c, d, e, f, g, h, i]

matrix dimension of degree 9

type D10 a b c d e f g h i j = a :| '[b, c, d, e, f, g, h, i, j]

matrix dimension of degree 10

matrix helpers

type family NS ns where ...

convert a list of Nat into a nonempty list of Nat

Equations

NS '[] = TypeError ('Text "NS: must have at least one Nat value for NonEmpty Nat")

NS (n ': '[]) = n :| '[]

NS (n ': (m ': ns)) = Cons1T n (NS (m ': ns))

type family Product1T ns where ...

product of a type level nonempty list as a Nat

Equations

Product1T (n :| '[]) = n

Product1T (n :| (n1 ': ns)) = n * Product1T (n1 :| ns)

type NN n = NS (NN' '[] n)

generates a nonempty list of indices using each digit of the given Nat

type family NN' ns n where ...

generates a list of indices using the individual digits of the given Nat

Equations

NN' ns 0 = ns

NN' ns n = NN' (Mod n 10 ': ns) (Div n 10)

type family Reverse1T ns where ...

used for reversing the indices of a matrix using type level list of nonempty indices

Equations

Reverse1T (n :| ns) = Reverse1T' (n ': ns) '[]

type family ListTupleT n a = result | result -> n a where ...

translates a type of size "n" to a tuple of size "n"

Equations

ListTupleT 1 a = One a

ListTupleT 2 a = (a, a)

ListTupleT 3 a = (a, a, a)

ListTupleT 4 a = (a, a, a, a)

ListTupleT 5 a = (a, a, a, a, a)

ListTupleT 6 a = (a, a, a, a, a, a)

ListTupleT 7 a = (a, a, a, a, a, a, a)

ListTupleT 8 a = (a, a, a, a, a, a, a, a)

ListTupleT 9 a = (a, a, a, a, a, a, a, a, a)

ListTupleT 10 a = (a, a, a, a, a, a, a, a, a, a)

ListTupleT 11 a = (a, a, a, a, a, a, a, a, a, a, a)

ListTupleT 12 a = (a, a, a, a, a, a, a, a, a, a, a, a)

ListTupleT 13 a = (a, a, a, a, a, a, a, a, a, a, a, a, a)

ListTupleT 14 a = (a, a, a, a, a, a, a, a, a, a, a, a, a, a)

ListTupleT 15 a = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a)

ListTupleT 16 a = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a)

ListTupleT 17 a = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a)

ListTupleT 18 a = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a)

ListTupleT 19 a = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a)

ListTupleT 20 a = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a)

list and nonempty conversions

class ValidateNestedListC x y where

extracts the dimensions of a nested list: doesnt allow empty dimensions

Methods

validateNestedListC :: [Pos] -> x -> [x] -> Either String (NonEmpty Pos)

Instances

(TypeError ('Text "ValidateNestedListC: not defined at 0") :: Constraint) => ValidateNestedListC x 'Z

Defined in Cybus.NatHelper

Methods

validateNestedListC :: [Pos] -> x -> [x] -> Either String (NonEmpty Pos)

ValidateNestedListC x ('S 'Z)

Defined in Cybus.NatHelper

Methods

validateNestedListC :: [Pos] -> x -> [x] -> Either String (NonEmpty Pos)

ValidateNestedListC x ('S n) => ValidateNestedListC [x] ('S ('S n))

Defined in Cybus.NatHelper

Methods

validateNestedListC :: [Pos] -> [x] -> [[x]] -> Either String (NonEmpty Pos)

class ValidateNestedNonEmptyC x y where

extracts the dimensions of a nested nonempty list: doesnt allow empty dimensions

Methods

validateNestedNonEmptyC :: [Pos] -> x -> [x] -> Either String (NonEmpty Pos)

Instances

(TypeError ('Text "ValidateNestedNonEmptyC: not defined at 'Z") :: Constraint) => ValidateNestedNonEmptyC x 'Z

Defined in Cybus.NatHelper

Methods

validateNestedNonEmptyC :: [Pos] -> x -> [x] -> Either String (NonEmpty Pos)

ValidateNestedNonEmptyC x ('S 'Z)

Defined in Cybus.NatHelper

Methods

validateNestedNonEmptyC :: [Pos] -> x -> [x] -> Either String (NonEmpty Pos)

ValidateNestedNonEmptyC x ('S zs) => ValidateNestedNonEmptyC (NonEmpty x) ('S ('S zs))

Defined in Cybus.NatHelper

Methods

validateNestedNonEmptyC :: [Pos] -> NonEmpty x -> [NonEmpty x] -> Either String (NonEmpty Pos)

validateNestedList :: forall x. ValidateNestedListC x (ValidateNestedListT x) => x -> Either String (NonEmpty Pos)

validate that the nested list is consistent in size along all dimensions

validateNestedNonEmpty :: forall x. ValidateNestedNonEmptyC x (ValidateNestedNonEmptyT x) => x -> Either String (NonEmpty Pos)

validate that the nested nonempty list is consistent in size along all dimensions

type family ValidateNestedListT x where ...

extracts the dimensions of a nested list

Equations

ValidateNestedListT [x] = 'S (ValidateNestedListT x)

ValidateNestedListT _ = 'S 'Z

type family ValidateNestedNonEmptyT x where ...

extracts the dimensions of a nested nonempty list

Equations

ValidateNestedNonEmptyT (NonEmpty x) = 'S (ValidateNestedNonEmptyT x)

ValidateNestedNonEmptyT _ = 'S 'Z

nestedNonEmptyToList :: forall ns a. NestedListC ns => NonEmptyNST ns a -> Either String (ListNST ns a)

convert a nested nonempty list into a nested list

nestedListToNonEmpty :: forall ns a. NestedListC ns => ListNST ns a -> Either String (NonEmptyNST ns a)

convert a nested list into a nested nonempty list

class NestedListC ns where

methods for working with nested lists

Methods

nestedListToNonEmptyC :: proxy a -> ListNST ns a -> Either String (NonEmptyNST ns a)

convert a nested list to a nested nonempty list

nestedNonEmptyToListC :: proxy a -> NonEmptyNST ns a -> Either String (ListNST ns a)

convert a nested nonempty list to a nested list

flattenNestedListC :: proxy a -> ListNST ns a -> Either String [a]

Instances

(PosT n, NestedListC (n1 :| ns)) => NestedListC (n :| (n1 ': ns))

Defined in Cybus.NatHelper

Methods

nestedListToNonEmptyC :: proxy a -> ListNST (n :| (n1 ': ns)) a -> Either String (NonEmptyNST (n :| (n1 ': ns)) a)

nestedNonEmptyToListC :: proxy a -> NonEmptyNST (n :| (n1 ': ns)) a -> Either String (ListNST (n :| (n1 ': ns)) a)

flattenNestedListC :: proxy a -> ListNST (n :| (n1 ': ns)) a -> Either String [a]

PosT n => NestedListC (n :| ('[] :: [Nat]))

Defined in Cybus.NatHelper

Methods

nestedListToNonEmptyC :: proxy a -> ListNST (n :| '[]) a -> Either String (NonEmptyNST (n :| '[]) a)

nestedNonEmptyToListC :: proxy a -> NonEmptyNST (n :| '[]) a -> Either String (ListNST (n :| '[]) a)

flattenNestedListC :: proxy a -> ListNST (n :| '[]) a -> Either String [a]

type family NonEmptyNST ns a where ...

convert a matrix index into nested lists

Equations

NonEmptyNST (_ :| '[]) a = NonEmpty a

NonEmptyNST (_ :| (n1 ': ns)) a = NonEmpty (NonEmptyNST (n1 :| ns) a)

type family ListNST ns a where ...

convert a matrix index into nested lists

Equations

ListNST (_ :| '[]) a = [a]

ListNST (_ :| (n1 ': ns)) a = [ListNST (n1 :| ns) a]