Introduce homogeneous coordinates

src/Data/NumIdr/Array/Array.idr

@@ -87,6 +87,10 @@ export
 shapeEq : (arr : Array s a) -> s = shape arr
 shapeEq (MkArray _ _ _ _) = Refl
 
+export
+withShape : {0 s' : Vect rk Nat} -> Array s' a -> ((s : Vect rk Nat) -> Array s a -> b) -> b
+withShape arr f = f (shape arr) (rewrite sym (shapeEq arr) in arr)
+
 -- Get a list of all coordinates
 getAllCoords' : Vect rk Nat -> List (Vect rk Nat)
 getAllCoords' = traverse (\case Z => []; S n => [0..n])

src/Data/NumIdr/Homogeneous/Matrix.idr

@@ -0,0 +1,23 @@
+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 = withDims mat $ \m,n,mat => ?h2 -- rewrite plusCommutative 1 m in ?h -- (mat `vconcat` repeat [1,n] 0) `hconcat` repeat [m,1] 0
+
+export
+toMatrix : HMatrix m n a -> Matrix m n a
+toMatrix = ?h

src/Data/NumIdr/Homogeneous/Vector.idr

@@ -0,0 +1,29 @@
+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
+

src/Data/NumIdr/Matrix.idr

@@ -17,6 +17,10 @@ Matrix' : Nat -> Type -> Type
 Matrix' n = Matrix n n
 
 
+export
+withDims : {0 m',n' : Nat} -> {0 b : Nat -> Nat -> Type} -> Matrix m' n' a -> ((m,n : Nat) -> Matrix m n a -> b m n) -> b m' n'
+withDims mat f = rewrite shapeEq mat in f (head $ shape mat) (index 1 $ shape mat) (rewrite sym (shapeEq mat) in mat)
+
 --------------------------------------------------------------------------------
 -- Matrix constructors
 --------------------------------------------------------------------------------

src/Data/NumIdr/Vector.idr

@@ -19,6 +19,10 @@ export
 dimEq : (v : Vector n a) -> n = dim v
 dimEq v = cong head $ shapeEq v
 
+export
+withDim : {0 n' : Nat} -> Vector n' a -> ((n : Nat) -> Vector n a -> b) -> b
+withDim v f = f (dim v) (rewrite sym (dimEq v) in v)
+
 --------------------------------------------------------------------------------
 -- Vector constructors
 --------------------------------------------------------------------------------
@@ -31,6 +35,11 @@ vector v = rewrite sym (lengthCorrect v)
            rewrite lengthCorrect v in        -- there is only 1 axis
            rewrite multOneLeftNeutral n in v
 
+export
+toVect : Vector n a -> Vect n a
+toVect v = believe_me $ Vect.fromList $ toList v
+
+
 export
 basis : Num a => {n : _} -> (i : Fin n) -> Vector n a
 basis i = fromFunction _ (\[j] => if i == j then 1 else 0)