Data.NumIdr.Array.Coords

Reexports

Definitions

range : Nat -> Nat -> List Nat

Totality: total
Visibility: public export

rangeLen : (x : Nat) -> (y : Nat) -> length (range x y) = minus y x

Totality: total
Visibility: export

rangeLenZ : (x : Nat) -> length (range 0 x) = x

Totality: total
Visibility: export

assertFin : Nat -> Fin n

Totality: total
Visibility: export

Coords : Vect rk Nat -> Type

  A type-safe coordinate system for an array. The coordinates are
  values of `Fin dim`, where `dim` is the dimension of each axis.

Totality: total
Visibility: public export

toNB : Coords s -> Vect rk Nat

  Forget the shape of the array by converting each index to type `Nat`.

Totality: total
Visibility: export

validateCoords : (s : Vect rk Nat) -> Vect rk Nat -> Maybe (Coords s)

Totality: total
Visibility: export

data CRange : Nat -> Type

Totality: total
Visibility: public export
Constructors:

One : Fin n -> CRange n

One' : Fin n -> CRange n

All : CRange n

StartBound : Fin (S n) -> CRange n

EndBound : Fin (S n) -> CRange n

Bounds : Fin (S n) -> Fin (S n) -> CRange n

Indices : List (Fin n) -> CRange n

Filter : (Fin n -> Bool) -> CRange n

CoordsRange : Vect rk Nat -> Type

Totality: total
Visibility: public export

data CRangeNB : Type

Totality: total
Visibility: public export
Constructors:

One : Nat -> CRangeNB

One' : Nat -> CRangeNB

All : CRangeNB

StartBound : Nat -> CRangeNB

EndBound : Nat -> CRangeNB

Bounds : Nat -> Nat -> CRangeNB

Indices : List Nat -> CRangeNB

Filter : (Nat -> Bool) -> CRangeNB

Vects : Vect rk Nat -> Type -> Type

Totality: total
Visibility: public export

collapse : Vects s a -> List a

Totality: total
Visibility: export

mapWithIndex : (Vect rk Nat -> a -> b) -> Vects s a -> Vects s b

Totality: total
Visibility: export

getLocation' : Vect rk Nat -> Vect rk Nat -> Nat

Totality: total
Visibility: export

getLocation : Vect rk Nat -> Coords s -> Nat

  Compute the memory location of an array element
  given its coordinate and the strides of the array.

Totality: total
Visibility: export

cRangeToList : CRange n -> Either Nat (List Nat)

Totality: total
Visibility: public export

newRank : CoordsRange s -> Nat

Totality: total
Visibility: public export

newShape : (rs : CoordsRange s) -> Vect (newRank rs) Nat

  Calculate the new shape given by a coordinate range.

Totality: total
Visibility: public export

getCoordsList : (rs : CoordsRange s) -> List (Vect rk Nat, Vect (newRank rs) Nat)

Totality: total
Visibility: export

validateCRange : (s : Vect rk Nat) -> Vect rk CRangeNB -> Maybe (CoordsRange s)

Totality: total
Visibility: export

assertCRange : (s : Vect rk Nat) -> Vect rk CRangeNB -> CoordsRange s

Totality: total
Visibility: export

cRangeNBToList : Nat -> CRangeNB -> Either Nat (List Nat)

Totality: total
Visibility: public export

newRank : Vect rk Nat -> Vect rk CRangeNB -> Nat

Totality: total
Visibility: public export

newShape : (s : Vect rk Nat) -> (is : Vect rk CRangeNB) -> Vect (newRank s is) Nat

  Calculate the new shape given by a coordinate range.

Totality: total
Visibility: public export

getAllCoords' : Vect rk Nat -> List (Vect rk Nat)

Totality: total
Visibility: export

getAllCoords : (s : Vect rk Nat) -> List (Coords s)

Totality: total
Visibility: export