
  0 | module Dinwiddy.Array
  1 | 
  2 | import Data.Vect
  3 | 
  4 | ||| A type-safe array, based on Vect.
  5 | ||| Example usage:
  6 | ||| ```idris
  7 | ||| x : Array 3 [5, 5, 6] Bool
  8 | ||| ```
  9 | ||| Will create a 3-dimensional Array with the size of 5x5x6.
 10 | |||
 11 | ||| As another example,
 12 | ||| ```
 13 | ||| x : Array 2 [2, 3] Bool
 14 | ||| ```
 15 | ||| Will create an array that looks like this:
 16 | ||| ```
 17 | ||| ###
 18 | ||| ###
 19 | ||| ```
 20 | ||| Full of booleans. It's value could be, for example:
 21 | ||| x = [[ True,  True,  True ],
 22 | |||      [ False, False, True ]]
 23 | |||
 24 | ||| This type has an advantage over `UnsafeArray`, because it's
 25 | ||| indexed in the type like `Vect`s.
 26 | public export
 27 | Array : (dimension : Nat) -> (dimensions : Vect dimension Nat) -> (type : Type) -> Type
 28 | Array (S Z) ds t = Vect (head ds) t
 29 | Array (S k) ds t = Vect (head ds) (Array k (tail ds) t)
 30 | Array Z     _  _ = ()
 31 |