Synopsis

module mk_sparse: (T: field) -> {
type t = T.t
type coo [nnz] = [nnz](i64, i64, T.t)
type~ csr [n] [m] = ?[nnz].{col_idx: [nnz]i64, dummy_m: [m](), row_off: [n]i64, vals: [nnz]T.t}
type~ csc [n] [m] = ?[nnz].{col_idx: [nnz]i64, dummy_m: [n](), row_off: [m]i64, vals: [nnz]T.t}
type contrib = {c: i64, r: i64, v: T.t}
type option 't = #None | #Some t
type contr = {s: i64, tc: i64, tr: i64, v: T.t}
type msr [n] [m] = {col_idx: [n]i64, dummy_m: [m](), vals: [n]T.t}
type msc [n] [m] = {col_idx: [m]i64, dummy_m: [n](), vals: [m]T.t}
val zero_val: T.t
val one_val: T.t
val eq: (a: T.t) -> (b: T.t) -> bool
val sort_coo [nnz]: (coo: [nnz](i64, i64, T.t)) -> [nnz](i64, i64, T.t)
val merge_coo [nnz]: (coo: [nnz](i64, i64, T.t)) -> ?[d₃₂].[d₃₂](i64, i64, T.t)
val norm_coo [nnz]: (coo: [nnz](i64, i64, T.t)) -> ?[d₅].[d₅](i64, i64, T.t)
val swap_rc: {c: i64, r: i64, v: T.t} -> {c: i64, r: i64, v: T.t}
val szs [n] [m] [nnz]: (csr: {col_idx: [nnz]i64, dummy_m: [m](), row_off: [n]i64, vals: [nnz]T.t}) -> [n]i64
val get_contrib [n] [m] [nnz]: (csr: {col_idx: [nnz]i64, dummy_m: [m](), row_off: [n]i64, vals: [nnz]T.t}) -> (r: i64) -> (i: i64) -> {c: i64, r: i64, v: T.t}
val cmp_contr: (c: {s: i64, tc: i64, tr: i64, v: T.t}) -> (c': {s: i64, tc: i64, tr: i64, v: T.t}) -> bool
val lte_contr: (c: {s: i64, tc: i64, tr: i64, v: T.t}) -> (c': {s: i64, tc: i64, tr: i64, v: T.t}) -> bool
val smm [n] [m] [k] [nnz] [nnz]: (A: {col_idx: [nnz]i64, dummy_m: [m](), row_off: [n]i64, vals: [nnz]T.t}) -> (B: {col_idx: [nnz]i64, dummy_m: [m](), row_off: [k]i64, vals: [nnz]T.t}) -> ?[d₁₆₉].{col_idx: [d₁₆₉]i64, dummy_m: [k](), row_off: [n]i64, vals: [d₁₆₉]T.t}
module csrmodule cscmodule msrmodule msc}

Description

↑module mk_sparse

Parameterised sparse matrix module with different representations, including a compressed sparse row (CSR) representation and a mono sparse row (MSR) representation. The module is parameterised over a field (defined in the linalg package). The residual module includes submodules for the different representations, including a csr module, a csc module, an msr module, and an msc module. Sparse matrix-vector multiplication is available in the csr and msr modules.