Add Matrix type

lib/Matrix.fm

@@ -0,0 +1,31 @@
+// An attempt at a matrix library
+T Matrix <A: Type> ~ (rows : Nat, cols : Nat)
+| Matrix.new<rows: Nat, cols: Nat>(vec: Vector(Vector(A, cols), rows)) ~ (rows, cols);
+
+Matrix.fill<A : Type>(value : A, rows: Nat, cols: Nat): Matrix(A, rows, cols)
+    let row = Vector.fill<A>(cols, value)
+    let rows_vec = Vector.fill<Vector(A,cols)>(rows, row)
+    Matrix.new<A, rows, cols>(rows_vec)
+
+
+Matrix.show<A : Type, rows : Nat, cols : Nat>(f : A -> String, m : Matrix(A, rows, cols)): String
+  case m:
+    | Vector.show<Vector(A,m.cols), m.rows>(Vector.show<A, m.cols>(f), m.vec);
+    : String;
+
+Matrix.test: IO(Unit)
+  do IO {
+    let m = Matrix.fill<Nat>(10,2,2);
+    IO.print(Matrix.show<Nat,2,2>(Nat.show, m));
+  }
+
+
+Matrix.add<A : Type,  (m1: Matrix(A, r, c), m2: Matrix(A, r, c)): Matrix(A, r, c)
+  case m1:
+  | Matrix.new(vec1) =>
+    case m2:
+    | Matrix.new(vec2) =>
+      for (r1, r2) in zip(vec1, vec2)
+        Vector.add(r1, r2)
+      end
+

lib/Vector.add.fm

@@ -0,0 +1,15 @@
+Vector.add<size : Nat>(u: Vector(Nat, size), v: Vector(Nat,size)): Vector(Nat, size)
+  case u:
+  with v : Vector(Nat,u.size) = v;
+  | Vector.nil<Nat>;
+  | get v.head v.tail = Vector.extract<Nat, u.size>(v)
+  Vector.ext<Nat, u.size>(Nat.add(u.head, v.head), Vector.add<u.size>(u.tail, v.tail));
+  : Vector(Nat, u.size);
+
+Vector.add.test: IO(Unit)
+  do IO {
+    let size = 3;
+    let u = Vector.fill<Nat>(size, 3);
+    let v = Vector.fill<Nat>(size, 4);
+    IO.print(Vector.show<Nat,size>(Nat.show, Vector.add<size>(u, v)));
+  }

lib/Vector.map.fm

@@ -0,0 +1,4 @@
+Vector.map<A: Type, B: Type, size: Nat>(f: A -> B, vec: Vector(A, size)): List(B)
+  case vec:
+  | List.nil<B>;
+  | List.cons<B>(f(vec.head), Vector.map<A,B,vec.size>(f,vec.tail));

lib/Vector.show.fm

@@ -0,0 +1,3 @@
+// Print a vector
+Vector.show<A : Type, size: Nat>(f: A -> String, vec : Vector(A, size)): String
+  String.flatten(["[", String.intercalate(",", Vector.map<A,String,size>(f,vec)), "]"])