From 11d771b92659104a85981790cd70093cf3e1db39 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Thu, 23 Jun 2022 19:11:12 -0400
Subject: [PATCH] Merge homogeneous modules

---
 src/Data/NumIdr/Homogeneous.idr        | 48 ++++++++++++++++++++++++++
 src/Data/NumIdr/Homogeneous/Matrix.idr | 24 -------------
 src/Data/NumIdr/Homogeneous/Vector.idr | 29 ----------------
 3 files changed, 48 insertions(+), 53 deletions(-)
 create mode 100644 src/Data/NumIdr/Homogeneous.idr
 delete mode 100644 src/Data/NumIdr/Homogeneous/Matrix.idr
 delete mode 100644 src/Data/NumIdr/Homogeneous/Vector.idr

diff --git a/src/Data/NumIdr/Homogeneous.idr b/src/Data/NumIdr/Homogeneous.idr
new file mode 100644
index 0000000..32ba267
--- /dev/null
+++ b/src/Data/NumIdr/Homogeneous.idr
@@ -0,0 +1,48 @@
+module Data.NumIdr.Homogeneous
+
+import Data.Vect
+import Data.NumIdr.Multiply
+import Data.NumIdr.Vector
+import Data.NumIdr.Matrix
+
+%default total
+
+
+public export
+HVector : Nat -> Type -> Type
+HVector n = Vector (S n)
+
+public export
+HMatrix : Nat -> Nat -> Type -> Type
+HMatrix m n = Matrix (S m) (S n)
+
+
+
+export
+fromVector : Num a => Vector n a -> HVector n a
+fromVector v = rewrite plusCommutative 1 n in v ++ vector [1]
+
+export
+fromVectorL : Num a => Vector n a -> HVector n a
+fromVectorL v = rewrite plusCommutative 1 n in v ++ vector [0]
+
+export
+toVector : HVector n a -> Vector n a
+toVector = vector . init . toVect
+-- TODO: Find an implementation for `toVector` that doesn't suck
+
+
+
+
+export
+toHomogeneous : Num a => Matrix m n a -> HMatrix m n a
+toHomogeneous mat with (viewShape mat)
+  _ | Shape [m,n] = indexSet [last, last] 1 $ resize [S m, S n] 0 mat
+
+
+
+export
+toMatrix : HMatrix m n a -> Matrix m n a
+toMatrix mat with (viewShape mat)
+  _ | Shape [S m, S n] = resizeLTE [m,n] mat
+                          {ok = [lteSuccRight reflexive,lteSuccRight reflexive]}
diff --git a/src/Data/NumIdr/Homogeneous/Matrix.idr b/src/Data/NumIdr/Homogeneous/Matrix.idr
deleted file mode 100644
index a7ad0f1..0000000
--- a/src/Data/NumIdr/Homogeneous/Matrix.idr
+++ /dev/null
@@ -1,24 +0,0 @@
-module Data.NumIdr.Homogeneous.Matrix
-
-import Data.Vect
-import Data.NumIdr.Multiply
-import public Data.NumIdr.Matrix
-
-%default total
-
-
-public export
-HMatrix : Nat -> Nat -> Type -> Type
-HMatrix m n = Matrix (S m) (S n)
-
-
-
-
-export
-fromMatrix : Num a => Matrix m n a -> HMatrix m n a
-fromMatrix mat with (viewShape mat)
-  _ | Shape [m,n] = ?h2
-
-export
-toMatrix : HMatrix m n a -> Matrix m n a
-toMatrix = ?h
diff --git a/src/Data/NumIdr/Homogeneous/Vector.idr b/src/Data/NumIdr/Homogeneous/Vector.idr
deleted file mode 100644
index 4e05b23..0000000
--- a/src/Data/NumIdr/Homogeneous/Vector.idr
+++ /dev/null
@@ -1,29 +0,0 @@
-module Data.NumIdr.Homogeneous.Vector
-
-import Data.Vect
-import Data.NumIdr.Multiply
-import public Data.NumIdr.Vector
-
-%default total
-
-
-public export
-HVector : Nat -> Type -> Type
-HVector n = Vector (S n)
-
-
-
-
-export
-fromVector : Num a => Vector n a -> HVector n a
-fromVector v = rewrite plusCommutative 1 n in v ++ vector [1]
-
-export
-fromVectorL : Num a => Vector n a -> HVector n a
-fromVectorL v = rewrite plusCommutative 1 n in v ++ vector [0]
-
-export
-toVector : HVector n a -> Vector n a
-toVector = vector . init . toVect
--- TODO: Find an implementation for `toVector` that doesn't suck
-