Libraries.Data.SparseMatrix

Definitions

Vector : Type -> Type

  A sparse vector is a list of pairs consisting of an index and its
  corresponding element.
  
  Invariants:
  - indices must appear in order and should to be duplicate-free,
  - elements must be additively non-neutral,
  - missing entries are assumed to be neutral.

Totality: total
Visibility: public export

fromList : (Eq a, Semiring a) => List a -> Vector a

  Turns a list into a sparse vector, discarding neutral elements in
  the process.

Totality: total
Visibility: export

insert : Nat -> a -> Vector a -> Vector a

  Insert `x` at index `i`. Ignore if the `i`th element already
  exists.
  
  @ x must not be neutral

Totality: total
Visibility: export

lookupOrd : Ord k => k -> List (k, a) -> Maybe a

Totality: total
Visibility: export

maxIndex : Vector a -> Maybe Nat

Totality: total
Visibility: export

length : Vector a -> Nat

Totality: total
Visibility: export

dot : Semiring a => Vector a -> Vector a -> a

Totality: total
Visibility: export

Vector1 : Type -> Type

Totality: total
Visibility: public export

fromList : (Eq a, Semiring a) => List a -> Maybe (Vector1 a)

Totality: total
Visibility: export

insert : Nat -> a -> Vector1 a -> Vector1 a

Totality: total
Visibility: export

lookupOrd : Ord k => k -> List1 (k, a) -> Maybe a

Totality: total
Visibility: export

maxIndex : Vector1 a -> Nat

Totality: total
Visibility: export

Matrix : Type -> Type

  A sparse matrix is a sparse vector of (non-empty) sparse vectors.

Totality: total
Visibility: public export

fromListList : (Eq a, Semiring a) => List (List a) -> Matrix a

Totality: total
Visibility: export

transpose : Matrix a -> Matrix a

Totality: total
Visibility: export

mult : (Eq a, Semiring a) => Matrix a -> Matrix a -> Matrix a

Totality: total
Visibility: export

prettyTable : Pretty ann a => String -> String -> Nat -> Matrix a -> Doc ann

  Renders a matrix as an ASCII table of the following shape:
  
  ```
                 columnSpacing
                       __
          columnDesc  0  1  ...
  rowDesc +--------------------
  0       |           a  b
  1       |           c  d
  ...     |           ...
  ```
  
  Note: everything is sadly left-aligned.
  
  @ maxWidthA Maximal length rendering something of type `a` might reach.

Totality: total
Visibility: export