Idris2Doc : JS.Array

JS.Array

(source)
Primitive Javascript arrays. This offers an alternative
to the functionality provided by `Data.IOArray.Prims` from base.

In addition to mutable arrays, we also provide linear arrays
for imperatively filling arrays in a pure envirionment,
as well as immutable arrays, the latter being guaranteed to always
return a value if an index is within bounds.

We use `Bits32` for indexing, as this is the type reflecting
most exactly the kinds of indices use to access array elements.
However, right now, `Bits32` is represented by `BigInt` at the Javascript
backend. This might negatively affect performance, as we always have
to convert to `Number` first (that's `Double` in Idris2).
Hopefully, the backend representation will change in the future, and
this will be no longer an issue.

In addition, `Bits32` does not offer a lot of functionality when
it comes to available proofs for it being in bounds. This
module provides a minimal amount of utilities for this, but again,
these might hopefully go elswhere, where the whole topic is treated
more thoroughly.

Definitions

Ix : Bits32 -> Type
  Type for indexing into an array of known size.

Totality: total
Visibility: public export
len32 : List a -> Bits32
  Calculates the length of a list as an array index.

Totality: total
Visibility: public export
zipWithIndex : (as : List a) -> List (Ix (len32 as), a)
  Zips a list of elements with the corresponding
  array indices.

Totality: total
Visibility: public export
toIx : (size : Bits32) -> Bits32 -> Maybe (Ix size)
  Tries to convert a number into an index for
  an array of the given size.

Totality: total
Visibility: public export
data Array : Type -> Type
Totality: total
Visibility: export
Hints:
ArrayLike (Array a) a
FromFFI (Array a) (Array a)
ToFFI (Array a) (Array a)
ToFFI a b => ToFFI (List a) (IO (Array b))
interface ArrayLike : Type -> Type -> Type
  Witness, that a given value represents an Array-like object.
  Array-like objects must provide the following functionality in
  the Javascript backend:
  
   * a `length` property, returning the value's length as an unsigned 32bit
     integer
   * the ability to access values of the given `elem` type`
     at a given index by means of the following syntax: `arr[12]`.
  
  Javascript Arrays are, of course, Array-like, as are Strings.
  Some other Array-likes include `NodeList` in the DOM.
  
  Note, that this is just a witnessing interface. All functionality
  is already implemented through functions `sizeIO` and `readIO`.
  It is possible to clone an `ArrayLike` to an actual Javascript
  Array by invoking `Array.from(v)` at the backend. This functionality
  is available through `arrayDataFrom` for mutable arrays and
  `arrayFrom` for immutable arrays.

Parameters: arr, el
Implementations:
ArrayLike String Char
ArrayLike (Array a) a
ArrayLike UInt8ClampedArray Bits8
ArrayLike UInt8Array Bits8
ArrayLike UInt16Array Bits16
ArrayLike UInt32Array Bits32
ArrayLike Int8Array Int8
ArrayLike Int16Array Int16
ArrayLike Int32Array Int32
ArrayLike Float64Array Double
ArrayLike (IArray a) a
sizeIO : (HasIO io, ArrayLike arr el) => arr -> io Bits32
Totality: total
Visibility: export
readIO : (HasIO io, ArrayLike arr e) => arr -> Bits32 -> io (Maybe e)
Totality: total
Visibility: export
interface IArrayLike : Type -> Type -> Type
  Witness, that a given value represents an immutable
  Array-like object. The same rules as for `ArrayLike`
  hold, with the addition, that values of types implementing
  this interface must be immutable.
  It is then safe to provide pure versions of `readIO` and `sizeIO`.

Parameters: arr, el
Constraints: ArrayLike arr el
Implementations:
IArrayLike String Char
IArrayLike (IArray a) a
size : IArrayLike arr el => arr -> Bits32
Totality: total
Visibility: export
read : {auto {conArg:7478} : IArrayLike arr el} -> (elems : arr) -> Ix (size elems) -> el
Totality: total
Visibility: export
readMaybe : IArrayLike arr el => arr -> Bits32 -> Maybe el
Totality: total
Visibility: export
sameElements : (IArrayLike arr el, Eq el) => arr -> arr -> Bool
  Returns true if the given immutable arrays contain
  the same elements in the same order.

Totality: total
Visibility: export
foldlArray : IArrayLike arr el => (acc -> el -> acc) -> acc -> arr -> acc
Totality: total
Visibility: export
foldrArray : IArrayLike arr el => (el -> acc -> acc) -> acc -> arr -> acc
Totality: total
Visibility: export
arrayToList : IArrayLike arr el => arr -> List el
Totality: total
Visibility: export
isArray : anyVal -> Bool
Totality: total
Visibility: export
writeIO : HasIO io => Array a -> Bits32 -> a -> io ()
Totality: total
Visibility: export
newArrayIO : HasIO io => Bits32 -> io (Array a)
Totality: total
Visibility: export
arrayDataFrom : (HasIO io, ArrayLike arr e) => arr -> io (Array e)
Totality: total
Visibility: export
fromListIO : HasIO io => List a -> io (Array a)
Totality: total
Visibility: export
fromFoldableIO : (HasIO io, Foldable t) => t a -> io (Array a)
Totality: total
Visibility: export
record LinArray : Bits32 -> Type -> Type
  A linear wrapper around a primitive array.

Totality: total
Visibility: export
Constructor: 
MkLinArray : Array a -> LinArray sze a

Projection: 
.array : LinArray sze a -> Array a
thaw : (1 _ : LinArray sze a) -> IO (Array a)
Totality: total
Visibility: export
emptyArray : (1 _ : ((1 _ : LinArray 0 a) -> b)) -> b
Totality: total
Visibility: export
newArray : a -> (sze : Bits32) -> (1 _ : ((1 _ : LinArray sze a) -> b)) -> b
Totality: total
Visibility: export
withArray : {auto {conArg:8509} : IArrayLike arr el} -> (v : arr) -> (1 _ : ((1 _ : LinArray (size v) el) -> a)) -> a
Totality: total
Visibility: export
write : (1 _ : LinArray sze a) -> Ix sze -> a -> LinArray sze a
Totality: total
Visibility: export
lread : (1 _ : LinArray sze a) -> Ix sze -> Res a (const (LinArray sze a))
Totality: total
Visibility: export
lsize : (1 _ : LinArray sze a) -> Res Bits32 (\s => LinArray s a)
Totality: total
Visibility: export
iterate' : (sze : Bits32) -> (Ix sze -> a) -> ((1 _ : LinArray sze a) -> b) -> b
Totality: total
Visibility: export
fromList' : (as : List a) -> ((1 _ : LinArray (len32 as) a) -> b) -> b
Totality: total
Visibility: export
map' : {auto {conArg:8773} : IArrayLike arr a} -> (vs : arr) -> ((1 _ : LinArray (size vs) b) -> c) -> (a -> b) -> c
Totality: total
Visibility: export
totalSize : (IArrayLike arr1 arr2, IArrayLike arr2 el) => arr1 -> Bits32
Totality: total
Visibility: export
join' : {auto {conArg:8860} : IArrayLike arr1 arr2} -> {auto {conArg:8863} : IArrayLike arr2 el} -> (vss : arr1) -> ((1 _ : LinArray (totalSize vss) el) -> a) -> a
  Concatenates to nested layers of immutable
  array-like objects.

Totality: total
Visibility: export
record IArray : Type -> Type
  An immutable array from a resource that guarantees, that
  this will not be modified any more.
  
  Typically, these are generated by freezing a `LinArray`
  or by cloning an `ArrayLike` value.

Totality: total
Visibility: export
Constructor: 
MkIArray : Array a -> IArray a

Projection: 
.array : IArray a -> Array a

Hints:
Alternative IArray
Applicative IArray
ArrayLike (IArray a) a
Eq el => Eq (IArray el)
Foldable IArray
FromString (IArray Char)
Functor IArray
IArrayLike (IArray a) a
Monad IArray
Monoid (IArray a)
Semigroup (IArray a)
Show a => Show (IArray a)
Traversable IArray
freezeCloneIO : (HasIO io, ArrayLike arr el) => arr -> io (IArray el)
Totality: total
Visibility: export
freeze : (1 _ : LinArray sze a) -> IArray a
Totality: total
Visibility: export
fromList : List a -> IArray a
Totality: total
Visibility: export
singleton : a -> IArray a
Totality: total
Visibility: export
concat : IArray (IArray a) -> IArray a
Totality: total
Visibility: export