diff --git a/src/Data/NumIdr/Array/Array.idr b/src/Data/NumIdr/Array/Array.idr index 704b9e5..81d0e2c 100644 --- a/src/Data/NumIdr/Array/Array.idr +++ b/src/Data/NumIdr/Array/Array.idr @@ -326,6 +326,15 @@ export arr !!.. rs = indexRange rs arr +export +indexUnsafe : Vect rk Nat -> Array {rk} s a -> a +indexUnsafe is arr = index (getLocation' (strides arr) is) (getPrim arr) + +export +(!#) : Array {rk} s a -> Vect rk Nat -> a +(!#) = flip indexUnsafe + + -------------------------------------------------------------------------------- -- Operations on arrays -------------------------------------------------------------------------------- @@ -338,7 +347,7 @@ arr !!.. rs = indexRange rs arr ||| @ ord The order to reinterpret the array by export reshape' : (s' : Vect rk' Nat) -> (ord : Order) -> Array {rk} s a -> - product s = product s' => Array s' a + (0 ok : product s = product s') => Array s' a reshape' s' ord' arr = MkArray ord' (calcStrides ord' s') s' (getPrim arr) ||| Reshape the array into the given shape. @@ -346,7 +355,7 @@ reshape' s' ord' arr = MkArray ord' (calcStrides ord' s') s' (getPrim arr) ||| @ s' The shape to convert the array to export reshape : (s' : Vect rk' Nat) -> Array {rk} s a -> - product s = product s' => Array s' a + (0 ok : product s = product s') => Array s' a reshape s' arr = reshape' s' (getOrder arr) arr diff --git a/src/Data/NumIdr/Homogeneous.idr b/src/Data/NumIdr/Homogeneous.idr index 2cd7e8a..724e666 100644 --- a/src/Data/NumIdr/Homogeneous.idr +++ b/src/Data/NumIdr/Homogeneous.idr @@ -37,31 +37,75 @@ 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] +-------------------------------------------------------------------------------- +-- Conversion functions +-------------------------------------------------------------------------------- + export -fromVectorL : Num a => Vector n a -> HVector n a -fromVectorL v = rewrite plusCommutative 1 n in v ++ vector [0] +vectorToH : Num a => Vector n a -> HVector n a +vectorToH v = rewrite plusCommutative 1 n in v ++ vector [1] export -toVector : HVector n a -> Vector n a -toVector = vector . init . toVect --- TODO: Find an implementation for `toVector` that doesn't suck +vectorToHLinear : Num a => Vector n a -> HVector n a +vectorToHLinear v = rewrite plusCommutative 1 n in v ++ vector [0] +export +hvector : Num a => Vect n a -> HVector n a +hvector v = rewrite plusCommutative 1 n in vector (v ++ [1]) + +export +hvectorLinear : Num a => Vect n a -> HVector n a +hvectorLinear v = rewrite plusCommutative 1 n in vector (v ++ [0]) + + +export +fromHomogeneous : HVector n a -> Vector n a +fromHomogeneous = vector . init . toVect +-- TODO: Find an implementation for `fromHomogeneous` that doesn't suck + + +export +hmatrix : Num a => Matrix m n a -> Vector m a -> HMatrix m n a +hmatrix mat tr with (viewShape mat) + _ | Shape [m,n] = indexSet [last,last] 1 $ + resize [S m, S n] 0 $ + mat `hconcat` reshape + {ok = sym $ multOneRightNeutral _} [m,1] tr + +export +matrixToH : Num a => Matrix m n a -> HMatrix m n a +matrixToH mat with (viewShape mat) + _ | Shape [m,n] = indexSet [last,last] 1 $ resize [S m, S n] 0 mat 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) +getMatrix : HMatrix m n a -> Matrix m n a +getMatrix mat with (viewShape mat) _ | Shape [S m, S n] = resizeLTE [m,n] mat {ok = [lteSuccRight reflexive,lteSuccRight reflexive]} + +export +getTranslationVector : HMatrix m n a -> Vector m a +getTranslationVector mat with (viewShape mat) + _ | Shape [S m, S n] = resizeLTE [m] {ok = [lteSuccRight reflexive]} $ + getColumn last mat + + +-------------------------------------------------------------------------------- +-- Constructors of homogeneous matrices +-------------------------------------------------------------------------------- + + +export +scalingH : Num a => {n : _} -> a -> HMatrix' n a +scalingH x = indexSet [last,last] 1 $ repeatDiag x 0 + +export +translationH : Num a => {n : _} -> Vector n a -> HMatrix' n a +translationH = hmatrix identity + +export +rotation2DH : Double -> HMatrix' 2 Double +rotation2DH = matrixToH . rotation2D diff --git a/src/Data/NumIdr/Matrix.idr b/src/Data/NumIdr/Matrix.idr index 5d5c8a5..3a456c1 100644 --- a/src/Data/NumIdr/Matrix.idr +++ b/src/Data/NumIdr/Matrix.idr @@ -65,7 +65,7 @@ identity : Num a => {n : _} -> Matrix' n a identity = repeatDiag 1 0 -||| Calculate the matrix that scales a vector by the given value. +||| Construct the matrix that scales a vector by the given value. export scaling : Num a => {n : _} -> a -> Matrix' n a scaling x = repeatDiag x 0 @@ -104,6 +104,17 @@ getColumn : Fin n -> Matrix m n a -> Vector m a getColumn c mat = rewrite sym (minusZeroRight m) in indexRange [All, One c] mat +export +diagonal' : Matrix m n a -> Vector (minimum m n) a +diagonal' mat with (viewShape mat) + _ | Shape [m,n] = fromFunctionNB _ (\[i] => indexUnsafe [i,i] mat) + +export +diagonal : Matrix' n a -> Vector n a +diagonal mat with (viewShape mat) + _ | Shape [n,n] = fromFunctionNB [n] (\[i] => indexUnsafe [i,i] mat) + + -------------------------------------------------------------------------------- -- Operations --------------------------------------------------------------------------------