union <'a> list with nat {
 Nil(0);
 {n:nat} Cons(n+1) of 'a * <'a> list(n)
}

{m:nat,n:nat}
record <'a> sparseArray(m, n) {
  row: int(m);
  col: int(n);
  data[m]: <int[0,n) * 'a> list
}

{n:nat}
float
list_vec_mult (xs: <int[0,n) * float> list, vec[n]: float) {
  var: int i; float f, sum;;

  sum = 0.0;
  while (true) {
    switch (xs) {
      case Nil: return sum;
      case Cons((i, f), xs): sum = sum +. f *. vec[i];      
    }
  }
  exit;    
}

{m:nat,n:nat}
float[m]
mat_vec_mult (mat: <float> sparseArray(m, n), vec[n]: float) {
  var: nat i; float result[];;

  result = alloc(mat.row, 0.0);

  for (i = 0; i < mat.row; i = i + 1) {
    result[i] = list_vec_mult (mat.data[i], vec);
  }
  return result;
}

{n:nat}
unit print_array (size: int(n), a[n]: float) {
  var: nat i;;
  for (i = 0; i < size; i = i + 1) {
      print_float (a[i]); print_string ("\t");
    }
    print_newline ();
}

unit main () {
  var: nat i; a: <float> sparseArray; float vec[], result[];;

  a = sparseArray { row = 3; col = 100; data = alloc (3, Nil) };
  a.data[0] = Cons ((6, 2.7183), Cons ((23, 3.1416), Nil));
  a.data[1] = Cons ((6, 3.1416), Cons ((23, 2.7183), Nil));
  a.data[2] = Cons ((3, 3.0), Cons ((5, 5.0), Cons ((7, 7.0), Cons ((9, 9.0), Nil))));

  vec = alloc (a.col, 0.0);
  for (i = 0; i < a.col; i = i + 1) {
    vec[i] = float_of_int (i);
  }

  result = mat_vec_mult (a, vec);
  print_array (a.row, result);
}