Synopsis
module sparse | : | { type t = i32 type contrib = {c: i64, r: i64, v: i32} type contr = {s: i64, tc: i64, tr: i64, v: i32} val zero_val: i32 val one_val: i32 val eq: (a: i32) -> (b: i32) -> bool 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 msr | : | { type t = i32 val scale [n] [m]: (v: i32) -> {col_idx: [n]i64, dummy_m: [m](), vals: [n]i32} -> {col_idx: [n]i64, dummy_m: [m](), vals: [n]i32} val sparse [nnz0]: (n: i64) -> (m: i64) -> (coo: [nnz0](i64, i64, i32)) -> {col_idx: [n]i64, dummy_m: [m](), vals: [n]i32} val + [n] [m]: {col_idx: [n]i64, dummy_m: [m](), vals: [n]i32} -> {col_idx: [n]i64, dummy_m: [m](), vals: [n]i32} -> {col_idx: [n]i64, dummy_m: [m](), vals: [n]i32} val - [n] [m]: {col_idx: [n]i64, dummy_m: [m](), vals: [n]i32} -> {col_idx: [n]i64, dummy_m: [m](), vals: [n]i32} -> {col_idx: [n]i64, dummy_m: [m](), vals: [n]i32} } |
val test_msr_eye | : | (n: i64) -> (m: i64) -> *[n][m]i32 |
val test_msr_sparse | [k] : | (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> *[n][m]i32 |
val test_msr_smvm | [k] : | (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> (v: *[m]i32) -> *[n]msr.t |
val test_msr_nnz | [k] : | (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> i64 |
val test_msr_coo | [k] : | (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> ([]i64, []i64, []msr.t) |
module msc | : | { type t = i32 val scale [n] [m]: (v: i32) -> (mat: {col_idx: [n]i64, dummy_m: [m](), vals: [n]i32}) -> {col_idx: [n]i64, dummy_m: [m](), vals: [n]i32} val coo [n] [m]: (mat: {col_idx: [n]i64, dummy_m: [m](), vals: [n]i32}) -> ?[n₄].[n₄](i64, i64, i32) val sparse [nnz]: (n: i64) -> (m: i64) -> (coo: [nnz](i64, i64, i32)) -> {col_idx: [m]i64, dummy_m: [n](), vals: [m]i32} val + [n₂] [m₃]: (x: {col_idx: [n₂]i64, dummy_m: [m₃](), vals: [n₂]i32}) -> (y: {col_idx: [n₂]i64, dummy_m: [m₃](), vals: [n₂]i32}) -> {col_idx: [n₂]i64, dummy_m: [m₃](), vals: [n₂]i32} } |
val test_msc_eye | : | (n: i64) -> (m: i64) -> *[n][m]i32 |
val test_msc_sparse | [k] : | (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> *[n][m]i32 |
val test_msc_nnz | [k] : | (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> i64 |
val test_msc_coo | [k] : | (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> ([]i64, []i64, []msc.t) |
val test_msr_transpose | [k] : | (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> [][]msc.t |
val test_msc_transpose | [k] : | (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> [][]msr.t |
Description
- ↑val test_msr_eye: (n: i64) -> (m: i64) -> *[n][m]i32
- ↑val test_msr_sparse [k]: (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> *[n][m]i32
- ↑val test_msr_smvm [k]: (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> (v: *[m]i32) -> *[n]msr.t
- ↑val test_msr_nnz [k]: (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> i64
- ↑val test_msr_coo [k]: (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> ([]i64, []i64, []msr.t)
- ↑val test_msc_eye: (n: i64) -> (m: i64) -> *[n][m]i32
- ↑val test_msc_sparse [k]: (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> *[n][m]i32
- ↑val test_msc_nnz [k]: (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> i64
- ↑val test_msc_coo [k]: (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> ([]i64, []i64, []msc.t)
- ↑val test_msr_transpose [k]: (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> [][]msc.t
- ↑val test_msc_transpose [k]: (n: i64) -> (m: i64) -> (xs: [k]i64) -> (ys: [k]i64) -> (vs: [k]i32) -> [][]msr.t