Synopsis

module sparse: {
type t = i32
type~ coo [nnz] = [nnz](i64, i64, i32)
type~ csr [n] [m] = ?[nnz].{col_idx: [nnz]i64, dummy_m: [m](), row_off: [n]i64, vals: [nnz]i32}
type~ csc [n] [m] = ?[nnz].{col_idx: [nnz]i64, dummy_m: [n](), row_off: [m]i64, vals: [nnz]i32}
type contrib = {c: i64, r: i64, v: i32}
type option 't = #None | #Some t
type contr = {s: i64, tc: i64, tr: i64, v: i32}
type msr [n] [m] = {col_idx: [n]i64, dummy_m: [m](), vals: [n]i32}
type msc [n] [m] = {col_idx: [m]i64, dummy_m: [n](), vals: [m]i32}
val zero_val: i32
val one_val: i32
val eq: (a: i32) -> (b: i32) -> bool
val sort_coo [nnz]: (coo: [nnz](i64, i64, i32)) -> [nnz](i64, i64, i32)
val merge_coo [nnz]: (coo: [nnz](i64, i64, i32)) -> ?[d₃₂].[d₃₂](i64, i64, i32)
val norm_coo [nnz]: (coo: [nnz](i64, i64, i32)) -> ?[d₅].[d₅](i64, i64, i32)
val swap_rc: {c: i64, r: i64, v: i32} -> {c: i64, r: i64, v: i32}
val szs [n] [m] [nnz]: (csr: {col_idx: [nnz]i64, dummy_m: [m](), row_off: [n]i64, vals: [nnz]i32}) -> [n]i64
val get_contrib [n] [m] [nnz]: (csr: {col_idx: [nnz]i64, dummy_m: [m](), row_off: [n]i64, vals: [nnz]i32}) -> (r: i64) -> (i: i64) -> {c: i64, r: i64, v: i32}
val cmp_contr: (c: {s: i64, tc: i64, tr: i64, v: i32}) -> (c': {s: i64, tc: i64, tr: i64, v: i32}) -> bool
val lte_contr: (c: {s: i64, tc: i64, tr: i64, v: i32}) -> (c': {s: i64, tc: i64, tr: i64, v: i32}) -> bool
val smm [n] [m] [k] [nnz] [nnz]: (A: {col_idx: [nnz]i64, dummy_m: [m](), row_off: [n]i64, vals: [nnz]i32}) -> (B: {col_idx: [nnz]i64, dummy_m: [m](), row_off: [k]i64, vals: [nnz]i32}) -> ?[d₁₆₉].{col_idx: [d₁₆₉]i64, dummy_m: [k](), row_off: [n]i64, vals: [d₁₆₉]i32}
module csrmodule cscmodule msrmodule msc}
module csr: {
type t = i32
type~ mat [n] [m] = ?[nnz].{col_idx: [nnz]i64, dummy_m: [m](), row_off: [n]i64, vals: [nnz]i32}
val zero: (n: i64) -> (m: i64) -> {col_idx: [0]i64, dummy_m: [m](), row_off: [n]i64, vals: [0]i32}
val eye: (n: i64) -> (m: i64) -> ?[d₁₆].{col_idx: [d₁₆]i64, dummy_m: [m](), row_off: [n]i64, vals: [d₁₆]i32}
val dense [n] [m] [nnz]: (csr: {col_idx: [nnz]i64, dummy_m: [m](), row_off: [n]i64, vals: [nnz]i32}) -> [n][m]i32
val smvm [n] [m] [nnz]: (csr: {col_idx: [nnz]i64, dummy_m: [m](), row_off: [n]i64, vals: [nnz]i32}) -> (v: [m]i32) -> [n]i32
val scale [n] [m] [nnz]: (v: i32) -> (csr: {col_idx: [nnz]i64, dummy_m: [m](), row_off: [n]i64, vals: [nnz]i32}) -> ?[d₃].{col_idx: [d₃]i64, dummy_m: [m](), row_off: [n]i64, vals: [d₃]i32}
val sparse [nnz0]: (n: i64) -> (m: i64) -> (coo: [nnz0](i64, i64, i32)) -> ?[d₃₆].{col_idx: [d₃₆]i64, dummy_m: [m](), row_off: [n]i64, vals: [d₃₆]i32}
val nnz [n] [m] [nnz]: (csr: {col_idx: [nnz]i64, dummy_m: [m](), row_off: [n]i64, vals: [nnz]i32}) -> i64
val coo [n] [m] [nnz]: (csr: {col_idx: [nnz]i64, dummy_m: [m](), row_off: [n]i64, vals: [nnz]i32}) -> ?[d₂₄].*[d₂₄](i64, i64, i32)
val + [n] [m] [nnz] [nnz]: (csr1: {col_idx: [nnz]i64, dummy_m: [m](), row_off: [n]i64, vals: [nnz]i32}) -> (csr2: {col_idx: [nnz]i64, dummy_m: [m](), row_off: [n]i64, vals: [nnz]i32}) -> ?[d₁₅].{col_idx: [d₁₅]i64, dummy_m: [m](), row_off: [n]i64, vals: [d₁₅]i32}
val - [n] [m] [nnz] [nnz]: (csr1: {col_idx: [nnz]i64, dummy_m: [m](), row_off: [n]i64, vals: [nnz]i32}) -> (csr2: {col_idx: [nnz]i64, dummy_m: [m](), row_off: [n]i64, vals: [nnz]i32}) -> ?[d₂₀].{col_idx: [d₂₀]i64, dummy_m: [m](), row_off: [n]i64, vals: [d₂₀]i32}
val transpose [n] [m] [nnz]: (mat: {col_idx: [nnz]i64, dummy_m: [m](), row_off: [n]i64, vals: [nnz]i32}) -> {col_idx: [nnz]i64, dummy_m: [m](), row_off: [n]i64, vals: [nnz]i32}
}
val test_csr_eye : (n: i64) -> (m: i64) -> *[n][m]i32
val test_csr_sparse [k] : (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> *[n][m]i32
val test_csr_smvm [k] : (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> (v: *[m]i32) -> *[n]csr.t
val test_csr_nnz [k] : (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> i64
val test_csr_coo [k] : (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> ([]i64, []i64, []csr.t)
module csc: {
type t = i32
type~ mat [n] [m] = ?[nnz].{col_idx: [nnz]i64, dummy_m: [n](), row_off: [m]i64, vals: [nnz]i32}
val zero: (n: i64) -> (m: i64) -> {col_idx: [0]i64, dummy_m: [n](), row_off: [m]i64, vals: [0]i32}
val scale [n] [m] [nnz]: (v: i32) -> (mat: {col_idx: [nnz]i64, dummy_m: [m](), row_off: [n]i64, vals: [nnz]i32}) -> ?[d₃].{col_idx: [d₃]i64, dummy_m: [m](), row_off: [n]i64, vals: [d₃]i32}
val eye: (n: i64) -> (m: i64) -> ?[d₀].{col_idx: [d₀]i64, dummy_m: [n](), row_off: [m]i64, vals: [d₀]i32}
val nnz [n] [m] [nnz]: (mat: {col_idx: [nnz]i64, dummy_m: [m](), row_off: [n]i64, vals: [nnz]i32}) -> i64
val coo [n] [m] [nnz]: (mat: {col_idx: [nnz]i64, dummy_m: [m](), row_off: [n]i64, vals: [nnz]i32}) -> ?[d₅].[d₅](i64, i64, i32)
val sparse [nnz]: (n: i64) -> (m: i64) -> (coo: [nnz](i64, i64, i32)) -> ?[d₉].{col_idx: [d₉]i64, dummy_m: [n](), row_off: [m]i64, vals: [d₉]i32}
val dense [n] [m] [nnz]: (mat: {col_idx: [nnz]i64, dummy_m: [m](), row_off: [n]i64, vals: [nnz]i32}) -> [m][n]i32
val + [n₂] [m₃] [nnz₄] [nnz₅]: (x: {col_idx: [nnz₄]i64, dummy_m: [m₃](), row_off: [n₂]i64, vals: [nnz₄]i32}) -> (y: {col_idx: [nnz₅]i64, dummy_m: [m₃](), row_off: [n₂]i64, vals: [nnz₅]i32}) -> ?[d₆].{col_idx: [d₆]i64, dummy_m: [m₃](), row_off: [n₂]i64, vals: [d₆]i32}
val - [n₂] [m₃] [nnz₄] [nnz₅]: (x: {col_idx: [nnz₄]i64, dummy_m: [m₃](), row_off: [n₂]i64, vals: [nnz₄]i32}) -> (y: {col_idx: [nnz₅]i64, dummy_m: [m₃](), row_off: [n₂]i64, vals: [nnz₅]i32}) -> ?[d₆].{col_idx: [d₆]i64, dummy_m: [m₃](), row_off: [n₂]i64, vals: [d₆]i32}
val transpose [n] [m] [nnz]: (mat: {col_idx: [nnz]i64, dummy_m: [m](), row_off: [n]i64, vals: [nnz]i32}) -> {col_idx: [nnz]i64, dummy_m: [m](), row_off: [n]i64, vals: [nnz]i32}
}
val test_csc_eye : (n: i64) -> (m: i64) -> *[n][m]i32
val test_csc_sparse [k] : (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> *[n][m]i32
val test_csc_nnz [k] : (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> i64
val test_csc_coo [k] : (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> ([]i64, []i64, []csc.t)
val test_csr_transpose [k] : (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> [][]csc.t
val test_csc_transpose [k] : (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> [][]csr.t
val test_smm [k1] [k2] : (n: i64) -> (m: i64) -> (k: i64) -> (xs1: [k1]i64) -> (ys1: [k1]i64) -> (vs1: [k1]i32) -> (xs2: [k2]i64) -> (ys2: [k2]i64) -> (vs2: [k2]i32) -> [][]csr.t

Description

↑module sparse
↑module csr
↑val test_csr_eye: (n: i64) -> (m: i64) -> *[n][m]i32
↑val test_csr_sparse [k]: (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> *[n][m]i32
↑val test_csr_smvm [k]: (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> (v: *[m]i32) -> *[n]csr.t
↑val test_csr_nnz [k]: (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> i64
↑val test_csr_coo [k]: (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> ([]i64, []i64, []csr.t)
↑module csc
↑val test_csc_eye: (n: i64) -> (m: i64) -> *[n][m]i32
↑val test_csc_sparse [k]: (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> *[n][m]i32
↑val test_csc_nnz [k]: (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> i64
↑val test_csc_coo [k]: (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> ([]i64, []i64, []csc.t)
↑val test_csr_transpose [k]: (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> [][]csc.t
↑val test_csc_transpose [k]: (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> [][]csr.t
↑val test_smm [k1] [k2]: (n: i64) -> (m: i64) -> (k: i64) -> (xs1: [k1]i64) -> (ys1: [k1]i64) -> (vs1: [k1]i32) -> (xs2: [k2]i64) -> (ys2: [k2]i64) -> (vs2: [k2]i32) -> [][]csr.t