From b924d960b50433b57540834da0cb606793fe0d83 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Mon, 25 Sep 2023 23:47:58 -0400 Subject: [PATCH] Tweak library functions to match reps --- src/Data/NumIdr/Array/Array.idr | 15 ++-- src/Data/NumIdr/Homogeneous.idr | 32 ++++---- src/Data/NumIdr/Matrix.idr | 97 ++++++++++++++----------- src/Data/NumIdr/PrimArray.idr | 26 +++---- src/Data/NumIdr/Scalar.idr | 2 +- src/Data/NumIdr/Transform/Point.idr | 3 +- src/Data/NumIdr/Transform/Transform.idr | 4 + src/Data/NumIdr/Vector.idr | 47 ++++++------ 8 files changed, 123 insertions(+), 103 deletions(-) diff --git a/src/Data/NumIdr/Array/Array.idr b/src/Data/NumIdr/Array/Array.idr index 4768843..8b55505 100644 --- a/src/Data/NumIdr/Array/Array.idr +++ b/src/Data/NumIdr/Array/Array.idr @@ -70,6 +70,7 @@ export getRep : Array s a -> Rep getRep (MkArray rep _ _) = rep +export getRepC : (arr : Array s a) -> RepConstraint (getRep arr) a getRepC (MkArray _ @{rc} _ _) = rc @@ -242,7 +243,7 @@ export indexSetRange : (rs : CoordsRange s) -> Array (newShape rs) a -> Array s a -> Array s a indexSetRange rs (MkArray _ _ rpl) (MkArray rep s arr) = - MkArray rep s (PrimArray.indexSetRange {rep} rs (convertRep rpl) arr) + MkArray rep s (PrimArray.indexSetRange {rep} rs (convertRepPrim rpl) arr) ||| Update the sub-array at the given range of coordinates by applying @@ -302,7 +303,7 @@ arr !?.. rs = indexRangeNB rs arr ||| Index the array using the given coordinates. ||| WARNING: This function does not perform any bounds check on its inputs. ||| Misuse of this function can easily break memory safety. -export +export %unsafe indexUnsafe : Vect rk Nat -> Array {rk} s a -> a indexUnsafe is (MkArray _ _ arr) = PrimArray.indexUnsafe is arr @@ -311,7 +312,7 @@ indexUnsafe is (MkArray _ _ arr) = PrimArray.indexUnsafe is arr ||| Misuse of this function can easily break memory safety. ||| ||| This is the operator form of `indexUnsafe`. -export %inline +export %inline %unsafe (!#) : Array {rk} s a -> Vect rk Nat -> a arr !# is = indexUnsafe is arr @@ -371,10 +372,10 @@ reshape : (s' : Vect rk' Nat) -> (arr : Array {rk} s a) -> LinearRep (getRep arr (0 ok : product s = product s') => Array s' a reshape s' (MkArray rep _ arr) = MkArray rep s' (PrimArray.reshape s' arr) -||| Change the internal order of the array's elements. +||| Change the internal representation of the array's elements. export convertRep : (rep : Rep) -> RepConstraint rep a => Array s a -> Array s a -convertRep rep (MkArray _ s arr) = MkArray rep s (PrimArray.convertRep arr) +convertRep rep (MkArray _ s arr) = MkArray rep s (convertRepPrim arr) ||| Resize the array to a new shape, preserving the coordinates of the original ||| elements. New coordinates are filled with a default value. @@ -563,7 +564,7 @@ export Functor (Array s) where map f (MkArray rep @{rc} s arr) = MkArray (forceRepNC rep) @{forceRepConstraint} s (mapPrim @{forceRepConstraint} @{forceRepConstraint} f - $ convertRep @{rc} @{forceRepConstraint} arr) + $ convertRepPrim @{rc} @{forceRepConstraint} arr) export {s : _} -> Applicative (Array s) where @@ -591,7 +592,7 @@ Traversable (Array s) where map (MkArray (forceRepNC rep) @{forceRepConstraint} s) (PrimArray.traverse {rep=forceRepNC rep} @{%search} @{forceRepConstraint} @{forceRepConstraint} f - (PrimArray.convertRep @{rc} @{forceRepConstraint} arr)) + (convertRepPrim @{rc} @{forceRepConstraint} arr)) export diff --git a/src/Data/NumIdr/Homogeneous.idr b/src/Data/NumIdr/Homogeneous.idr index a40fe7f..09b70c8 100644 --- a/src/Data/NumIdr/Homogeneous.idr +++ b/src/Data/NumIdr/Homogeneous.idr @@ -78,8 +78,7 @@ hmatrix : Num a => Matrix m n a -> Vector m a -> HMatrix m n a hmatrix {m,n} 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 + mat `hconcat` hstack [tr] ||| Convert a regular matrix to a homogeneous matrix. export @@ -120,8 +119,9 @@ getTranslationVector {m,n} mat with (viewShape mat) ||| Construct a homogeneous matrix that scales a vector by the input. export -scalingH : {n : _} -> Num a => a -> HMatrix' n a -scalingH x = indexSet [last,last] 1 $ repeatDiag x 0 +scalingH : {default B rep : Rep} -> RepConstraint rep a => + {n : _} -> Num a => a -> HMatrix' n a +scalingH x = indexSet [last,last] 1 $ repeatDiag {rep} x 0 ||| Construct a homogeneous matrix that translates by the given vector. export @@ -132,23 +132,27 @@ translationH {n} v with (viewShape v) ||| Construct a 2D homogeneous matrix that rotates by the given angle (in radians). export -rotate2DH : Double -> HMatrix' 2 Double -rotate2DH = matrixToH . rotate2D +rotate2DH : {default B rep : Rep} -> RepConstraint rep Double => + Double -> HMatrix' 2 Double +rotate2DH = matrixToH . rotate2D {rep} ||| Construct a 3D homogeneous matrix that rotates around the x-axis. export -rotate3DXH : Double -> HMatrix' 3 Double -rotate3DXH = matrixToH . rotate3DX +rotate3DXH : {default B rep : Rep} -> RepConstraint rep Double => + Double -> HMatrix' 3 Double +rotate3DXH = matrixToH . rotate3DX {rep} ||| Construct a 3D homogeneous matrix that rotates around the y-axis. export -rotate3DYH : Double -> HMatrix' 3 Double -rotate3DYH = matrixToH . rotate3DY +rotate3DYH : {default B rep : Rep} -> RepConstraint rep Double => + Double -> HMatrix' 3 Double +rotate3DYH = matrixToH . rotate3DY {rep} ||| Construct a 3D homogeneous matrix that rotates around the z-axis. export -rotate3DZH : Double -> HMatrix' 3 Double -rotate3DZH = matrixToH . rotate3DZ +rotate3DZH : {default B rep : Rep} -> RepConstraint rep Double => + Double -> HMatrix' 3 Double +rotate3DZH = matrixToH . rotate3DZ {rep} export @@ -161,8 +165,8 @@ reflectXH = reflectH 0 export reflectYH : {n : _} -> Neg a => HMatrix' (2 + n) a -reflectYH = reflectH 0 +reflectYH = reflectH 1 export reflectZH : {n : _} -> Neg a => HMatrix' (3 + n) a -reflectZH = reflectH 0 +reflectZH = reflectH 2 diff --git a/src/Data/NumIdr/Matrix.idr b/src/Data/NumIdr/Matrix.idr index 0da3f27..461a213 100644 --- a/src/Data/NumIdr/Matrix.idr +++ b/src/Data/NumIdr/Matrix.idr @@ -5,8 +5,8 @@ import Data.Vect import Data.Permutation import Data.NumIdr.Interfaces import public Data.NumIdr.Array +import Data.NumIdr.PrimArray import Data.NumIdr.Vector -import Data.NumIdr.LArray %default total @@ -31,13 +31,9 @@ Matrix' n = Array [n,n] ||| Construct a matrix with the given order and elements. export -matrix' : {m, n : _} -> Order -> Vect m (Vect n a) -> Matrix m n a -matrix' ord x = array' [m,n] ord x - -||| Construct a matrix with the given elements. -export -matrix : {m, n : _} -> Vect m (Vect n a) -> Matrix m n a -matrix = matrix' COrder +matrix : {default B rep : Rep} -> RepConstraint rep a => {m, n : _} -> + Vect m (Vect n a) -> Matrix m n a +matrix x = array' {rep} [m,n] x ||| Construct a matrix with a specific value along the diagonal. @@ -45,8 +41,9 @@ matrix = matrix' COrder ||| @ diag The value to repeat along the diagonal ||| @ other The value to repeat elsewhere export -repeatDiag : {m, n : _} -> (diag, other : a) -> Matrix m n a -repeatDiag d o = fromFunctionNB [m,n] +repeatDiag : {default B rep : Rep} -> RepConstraint rep a => {m, n : _} -> + (diag, other : a) -> Matrix m n a +repeatDiag d o = fromFunctionNB {rep} [m,n] (\[i,j] => if i == j then d else o) ||| Construct a matrix given its diagonal elements. @@ -54,8 +51,9 @@ repeatDiag d o = fromFunctionNB [m,n] ||| @ diag The elements of the matrix's diagonal ||| @ other The value to repeat elsewhere export -fromDiag : {m, n : _} -> (diag : Vect (minimum m n) a) -> (other : a) -> Matrix m n a -fromDiag ds o = fromFunction [m,n] (\[i,j] => maybe o (`index` ds) $ i `eq` j) +fromDiag : {default B rep : Rep} -> RepConstraint rep a => {m, n : _} -> + (diag : Vect (minimum m n) a) -> (other : a) -> Matrix m n a +fromDiag ds o = fromFunction {rep} [m,n] (\[i,j] => maybe o (`index` ds) $ i `eq` j) where eq : {0 m,n : Nat} -> Fin m -> Fin n -> Maybe (Fin (minimum m n)) eq FZ FZ = Just FZ @@ -66,52 +64,62 @@ fromDiag ds o = fromFunction [m,n] (\[i,j] => maybe o (`index` ds) $ i `eq` j) ||| Construct a permutation matrix based on the given permutation. export -permuteM : {n : _} -> Num a => Permutation n -> Matrix' n a -permuteM p = permuteInAxis 0 p (repeatDiag 1 0) +permuteM : {default B rep : Rep} -> RepConstraint rep a => {n : _} -> Num a => + Permutation n -> Matrix' n a +permuteM p = permuteInAxis 0 p (repeatDiag {rep} 1 0) ||| Construct the matrix that scales a vector by the given value. export -scale : {n : _} -> Num a => a -> Matrix' n a -scale x = repeatDiag x 0 +scale : {default B rep : Rep} -> RepConstraint rep a => {n : _} -> Num a => + a -> Matrix' n a +scale x = repeatDiag {rep} x 0 ||| Construct a 2D rotation matrix that rotates by the given angle (in radians). export -rotate2D : Double -> Matrix' 2 Double -rotate2D a = matrix [[cos a, - sin a], [sin a, cos a]] +rotate2D : {default B rep : Rep} -> RepConstraint rep Double => + Double -> Matrix' 2 Double +rotate2D a = matrix {rep} [[cos a, - sin a], [sin a, cos a]] ||| Construct a 3D rotation matrix around the x-axis. export -rotate3DX : Double -> Matrix' 3 Double -rotate3DX a = matrix [[1,0,0], [0, cos a, - sin a], [0, sin a, cos a]] +rotate3DX : {default B rep : Rep} -> RepConstraint rep Double => + Double -> Matrix' 3 Double +rotate3DX a = matrix {rep} [[1,0,0], [0, cos a, - sin a], [0, sin a, cos a]] ||| Construct a 3D rotation matrix around the y-axis. export -rotate3DY : Double -> Matrix' 3 Double -rotate3DY a = matrix [[cos a, 0, sin a], [0,1,0], [- sin a, 0, cos a]] +rotate3DY : {default B rep : Rep} -> RepConstraint rep Double => + Double -> Matrix' 3 Double +rotate3DY a = matrix {rep} [[cos a, 0, sin a], [0,1,0], [- sin a, 0, cos a]] ||| Construct a 3D rotation matrix around the z-axis. export -rotate3DZ : Double -> Matrix' 3 Double -rotate3DZ a = matrix [[cos a, - sin a, 0], [sin a, cos a, 0], [0,0,1]] +rotate3DZ : {default B rep : Rep} -> RepConstraint rep Double => + Double -> Matrix' 3 Double +rotate3DZ a = matrix {rep} [[cos a, - sin a, 0], [sin a, cos a, 0], [0,0,1]] export -reflect : {n : _} -> Neg a => Fin n -> Matrix' n a -reflect i = indexSet [i, i] (-1) (repeatDiag 1 0) +reflect : {default B rep : Rep} -> RepConstraint rep a => + {n : _} -> Neg a => Fin n -> Matrix' n a +reflect i = indexSet [i, i] (-1) (repeatDiag {rep} 1 0) export -reflectX : {n : _} -> Neg a => Matrix' (1 + n) a -reflectX = reflect 0 +reflectX : {default B rep : Rep} -> RepConstraint rep a => + {n : _} -> Neg a => Matrix' (1 + n) a +reflectX = reflect {rep} 0 export -reflectY : {n : _} -> Neg a => Matrix' (2 + n) a -reflectY = reflect 1 +reflectY : {default B rep : Rep} -> RepConstraint rep a => + {n : _} -> Neg a => Matrix' (2 + n) a +reflectY = reflect {rep} 1 export -reflectZ : {n : _} -> Neg a => Matrix' (3 + n) a -reflectZ = reflect 2 +reflectZ : {default B rep : Rep} -> RepConstraint rep a => + {n : _} -> Neg a => Matrix' (3 + n) a +reflectZ = reflect {rep} 2 -------------------------------------------------------------------------------- @@ -146,13 +154,13 @@ getColumn c mat = rewrite sym (rangeLenZ m) in mat!!..[All, One c] export diagonal' : Matrix m n a -> Vector (minimum m n) a diagonal' {m,n} mat with (viewShape mat) - _ | Shape [m,n] = fromFunctionNB _ (\[i] => mat!#[i,i]) + _ | Shape [m,n] = fromFunctionNB {rep=_} @{getRepC mat} _ (\[i] => mat!#[i,i]) ||| Return the diagonal elements of the matrix as a vector. export diagonal : Matrix' n a -> Vector n a diagonal {n} mat with (viewShape mat) - _ | Shape [n,n] = fromFunctionNB [n] (\[i] => mat!#[i,i]) + _ | Shape [n,n] = fromFunctionNB {rep=_} @{getRepC mat} [n] (\[i] => mat!#[i,i]) ||| Return a minor of the matrix, i.e. the matrix formed by removing a @@ -165,7 +173,8 @@ minor i j mat = believe_me $ mat!!..[Filter (/=i), Filter (/=j)] filterInd : Num a => (Nat -> Nat -> Bool) -> Matrix m n a -> Matrix m n a filterInd {m,n} p mat with (viewShape mat) - _ | Shape [m,n] = fromFunctionNB [m,n] (\[i,j] => if p i j then mat!#[i,j] else 0) + _ | Shape [m,n] = fromFunctionNB {rep=_} @{getRepC mat} + [m,n] (\[i,j] => if p i j then mat!#[i,j] else 0) export upperTriangle : Num a => Matrix m n a -> Matrix m n a @@ -259,13 +268,15 @@ reflectNormal {n} v with (viewShape v) export Num a => Mult (Matrix m n a) (Vector n a) (Vector m a) where (*.) {m,n} mat v with (viewShape mat) - _ | Shape [m,n] = fromFunction [m] + _ | Shape [m,n] = fromFunction {rep=_} + @{mergeRepConstraint (getRepC mat) (getRepC v)} [m] (\[i] => sum $ map (\j => mat!![i,j] * v!!j) range) export Num a => Mult (Matrix m n a) (Matrix n p a) (Matrix m p a) where (*.) {m,n,p} m1 m2 with (viewShape m1, viewShape m2) - _ | (Shape [m,n], Shape [n,p]) = fromFunction [m,p] + _ | (Shape [m,n], Shape [n,p]) = fromFunction {rep=_} + @{mergeRepConstraint (getRepC m1) (getRepC m2)} [m,p] (\[i,j] => sum $ map (\k => m1!![i,k] * m2!![k,j]) range) export @@ -295,7 +306,7 @@ namespace DecompLU export lower : Num a => DecompLU {m,n,a} mat -> Matrix m (minimum m n) a lower {m,n} (MkLU lu) with (viewShape lu) - _ | Shape [m,n] = fromFunctionNB _ (\[i,j] => + _ | Shape [m,n] = fromFunctionNB {rep=_} @{getRepC lu} _ (\[i,j] => case compare i j of LT => 0 EQ => 1 @@ -325,7 +336,7 @@ namespace DecompLU export upper : Num a => DecompLU {m,n,a} mat -> Matrix (minimum m n) n a upper {m,n} (MkLU lu) with (viewShape lu) - _ | Shape [m,n] = fromFunctionNB _ (\[i,j] => + _ | Shape [m,n] = fromFunctionNB {rep=_} @{getRepC lu} _ (\[i,j] => if i <= j then lu!#[i,j] else 0) ||| The upper triangular matrix U of the LU decomposition. @@ -392,7 +403,8 @@ gaussStep i lu = export decompLU : Field a => (mat : Matrix m n a) -> Maybe (DecompLU mat) decompLU {m,n} mat with (viewShape mat) - _ | Shape [m,n] = map MkLU $ iterateN (minimum m n) (\i => (>>= gaussStepMaybe i)) (Just mat) + _ | Shape [m,n] = map (MkLU . convertRep _ @{getRepC mat}) + $ iterateN (minimum m n) (\i => (>>= gaussStepMaybe i)) (Just (convertRep Delayed mat)) where gaussStepMaybe : Fin (minimum m n) -> Matrix m n a -> Maybe (Matrix m n a) gaussStepMaybe i mat = if mat!#[cast i,cast i] == 0 then Nothing @@ -417,7 +429,7 @@ namespace DecompLUP export lower : Num a => DecompLUP {m,n,a} mat -> Matrix m (minimum m n) a lower {m,n} (MkLUP lu _ _) with (viewShape lu) - _ | Shape [m,n] = fromFunctionNB _ (\[i,j] => + _ | Shape [m,n] = fromFunctionNB {rep=_} @{getRepC lu} _ (\[i,j] => case compare i j of LT => 0 EQ => 1 @@ -447,7 +459,7 @@ namespace DecompLUP export upper : Num a => DecompLUP {m,n,a} mat -> Matrix (minimum m n) n a upper {m,n} (MkLUP lu _ _) with (viewShape lu) - _ | Shape [m,n] = fromFunctionNB _ (\[i,j] => + _ | Shape [m,n] = fromFunctionNB {rep=_} @{getRepC lu} _ (\[i,j] => if i <= j then lu!#[i,j] else 0) ||| The upper triangular matrix U of the LUP decomposition. @@ -634,4 +646,3 @@ export {n : _} -> FieldCmp a => MultGroup (Matrix' n a) where inverse mat = let lup = decompLUP mat in hstack $ map (solveWithLUP' mat lup . basis) range - diff --git a/src/Data/NumIdr/PrimArray.idr b/src/Data/NumIdr/PrimArray.idr index d7d1009..3fe2480 100644 --- a/src/Data/NumIdr/PrimArray.idr +++ b/src/Data/NumIdr/PrimArray.idr @@ -152,18 +152,18 @@ indexUnsafe {rep = Delayed} is arr = assert_total $ case validateCoords s is of Just is' => arr is' export -convertRep : {r1,r2,s : _} -> RepConstraint r1 a => RepConstraint r2 a => PrimArray r1 s a -> PrimArray r2 s a -convertRep {r1 = Bytes o, r2 = Bytes o'} @{rc} arr = reorder @{rc} arr -convertRep {r1 = Boxed o, r2 = Boxed o'} arr = reorder arr -convertRep {r1 = Linked, r2 = Linked} arr = arr -convertRep {r1 = Linked, r2 = Bytes COrder} @{_} @{rc} arr = fromList @{rc} s (collapse arr) -convertRep {r1 = Linked, r2 = Boxed COrder} arr = fromList s (collapse arr) -convertRep {r1 = Delayed, r2 = Delayed} arr = arr -convertRep {r1, r2} arr = fromFunction s (\is => PrimArray.index is arr) +convertRepPrim : {r1,r2,s : _} -> RepConstraint r1 a => RepConstraint r2 a => PrimArray r1 s a -> PrimArray r2 s a +convertRepPrim {r1 = Bytes o, r2 = Bytes o'} @{rc} arr = reorder @{rc} arr +convertRepPrim {r1 = Boxed o, r2 = Boxed o'} arr = reorder arr +convertRepPrim {r1 = Linked, r2 = Linked} arr = arr +convertRepPrim {r1 = Linked, r2 = Bytes COrder} @{_} @{rc} arr = fromList @{rc} s (collapse arr) +convertRepPrim {r1 = Linked, r2 = Boxed COrder} arr = fromList s (collapse arr) +convertRepPrim {r1 = Delayed, r2 = Delayed} arr = arr +convertRepPrim {r1, r2} arr = fromFunction s (\is => PrimArray.index is arr) export fromVects : {rep : Rep} -> RepConstraint rep a => (s : Vect rk Nat) -> Vects s a -> PrimArray rep s a -fromVects s v = convertRep {r1=Linked} v +fromVects s v = convertRepPrim {r1=Linked} v export fromList : {rep : Rep} -> LinearRep rep => RepConstraint rep a => (s : Vect rk Nat) -> List a -> PrimArray rep s a @@ -184,14 +184,14 @@ foldl : {rep,s : _} -> RepConstraint rep a => (b -> a -> b) -> b -> PrimArray re foldl {rep = Bytes _} = Bytes.foldl foldl {rep = Boxed _} = Boxed.foldl foldl {rep = Linked} = Linked.foldl -foldl {rep = Delayed} = \f,z => Boxed.foldl f z . convertRep {r1=Delayed,r2=B} +foldl {rep = Delayed} = \f,z => Boxed.foldl f z . convertRepPrim {r1=Delayed,r2=B} export foldr : {rep,s : _} -> RepConstraint rep a => (a -> b -> b) -> b -> PrimArray rep s a -> b foldr {rep = Bytes _} = Bytes.foldr foldr {rep = Boxed _} = Boxed.foldr foldr {rep = Linked} = Linked.foldr -foldr {rep = Delayed} = \f,z => Boxed.foldr f z . convertRep {r1=Delayed,r2=B} +foldr {rep = Delayed} = \f,z => Boxed.foldr f z . convertRepPrim {r1=Delayed,r2=B} export traverse : {rep,s : _} -> Applicative f => RepConstraint rep a => RepConstraint rep b => @@ -199,6 +199,6 @@ traverse : {rep,s : _} -> Applicative f => RepConstraint rep a => RepConstraint traverse {rep = Bytes o} = Bytes.traverse traverse {rep = Boxed o} = Boxed.traverse traverse {rep = Linked} = Linked.traverse -traverse {rep = Delayed} = \f => map (convertRep @{()} @{()} {r1=B,r2=Delayed}) . +traverse {rep = Delayed} = \f => map (convertRepPrim @{()} @{()} {r1=B,r2=Delayed}) . Boxed.traverse f . - convertRep @{()} @{()} {r1=Delayed,r2=B} + convertRepPrim @{()} @{()} {r1=Delayed,r2=B} diff --git a/src/Data/NumIdr/Scalar.idr b/src/Data/NumIdr/Scalar.idr index b2bdbd0..0320bf5 100644 --- a/src/Data/NumIdr/Scalar.idr +++ b/src/Data/NumIdr/Scalar.idr @@ -23,7 +23,7 @@ scalar x = fromVect _ [x] ||| Unwrap the single value from a scalar. export unwrap : Scalar a -> a -unwrap = index 0 . getPrim +unwrap s = s !# [] export diff --git a/src/Data/NumIdr/Transform/Point.idr b/src/Data/NumIdr/Transform/Point.idr index e4d149e..40f4d2b 100644 --- a/src/Data/NumIdr/Transform/Point.idr +++ b/src/Data/NumIdr/Transform/Point.idr @@ -176,8 +176,7 @@ Traversable (Point n) where export Show a => Show (Point n a) where - showPrec d (MkPoint v) = showCon d "point" $ - showArg $ PrimArray.toList $ getPrim v + showPrec d (MkPoint v) = showCon d "point" $ showArg $ elements v export Cast a b => Cast (Point n a) (Point n b) where diff --git a/src/Data/NumIdr/Transform/Transform.idr b/src/Data/NumIdr/Transform/Transform.idr index cdb851b..2692b11 100644 --- a/src/Data/NumIdr/Transform/Transform.idr +++ b/src/Data/NumIdr/Transform/Transform.idr @@ -101,6 +101,10 @@ export getMatrix : Transform ty n a -> Matrix' n a getMatrix (MkTrans _ mat) = getMatrix mat +export +convertRep : (rep : Rep) -> RepConstraint rep a => Transform ty n a -> Transform ty n a +convertRep rep (MkTrans _ mat) = MkTrans _ (convertRep rep mat) + ||| Linearize a transform by removing its translation component. ||| If the transform is already linear, then this function does nothing. export diff --git a/src/Data/NumIdr/Vector.idr b/src/Data/NumIdr/Vector.idr index 0adad52..0ca6de3 100644 --- a/src/Data/NumIdr/Vector.idr +++ b/src/Data/NumIdr/Vector.idr @@ -32,43 +32,45 @@ dimEq v = cong head $ shapeEq v ||| Construct a vector from a `Vect`. export -vector : Vect n a -> Vector n a +vector : {default B rep : Rep} -> RepConstraint rep a => Vect n a -> Vector n a vector v = rewrite sym (lengthCorrect v) - in fromVect [length v] $ -- the order doesn't matter here, as - rewrite lengthCorrect v in -- there is only 1 axis - rewrite multOneLeftNeutral n in v + in array {rep,s=[length v]} $ + rewrite lengthCorrect v in v ||| Convert a vector into a `Vect`. export toVect : Vector n a -> Vect n a -toVect v = believe_me $ Vect.fromList $ toList v - +toVect v = believe_me $ Vect.fromList $ Prelude.toList v ||| Return the `i`-th basis vector. export -basis : Num a => {n : _} -> (i : Fin n) -> Vector n a -basis i = fromFunction _ (\[j] => if i == j then 1 else 0) +basis : {default B rep : Rep} -> RepConstraint rep a => + Num a => {n : _} -> (i : Fin n) -> Vector n a +basis i = fromFunction {rep} _ (\[j] => if i == j then 1 else 0) ||| The first basis vector. export -basisX : {n : _} -> Num a => Vector (1 + n) a -basisX = basis FZ +basisX : {default B rep : Rep} -> RepConstraint rep a => + {n : _} -> Num a => Vector (1 + n) a +basisX = basis {rep} FZ ||| The second basis vector. export -basisY : {n : _} -> Num a => Vector (2 + n) a -basisY = basis (FS FZ) +basisY : {default B rep : Rep} -> RepConstraint rep a => + {n : _} -> Num a => Vector (2 + n) a +basisY = basis {rep} (FS FZ) ||| The third basis vector. export -basisZ : {n : _} -> Num a => Vector (3 + n) a -basisZ = basis (FS (FS FZ)) - +basisZ : {default B rep : Rep} -> RepConstraint rep a => + {n : _} -> Num a => Vector (3 + n) a +basisZ = basis {rep} (FS (FS FZ)) ||| Calculate the 2D unit vector with the given angle off the x-axis. export -unit2D : (ang : Double) -> Vector 2 Double -unit2D ang = vector [cos ang, sin ang] +unit2D : {default B rep : Rep} -> RepConstraint rep Double => + (ang : Double) -> Vector 2 Double +unit2D ang = vector {rep} [cos ang, sin ang] ||| Calculate the 3D unit vector corresponding to the given spherical coordinates, ||| where the polar axis is the z-axis. @@ -76,8 +78,9 @@ unit2D ang = vector [cos ang, sin ang] ||| @ pol The polar angle of the vector ||| @ az The azimuthal angle of the vector export -unit3D : (pol, az : Double) -> Vector 3 Double -unit3D pol az = vector [cos az * sin pol, sin az * sin pol, cos pol] +unit3D : {default B rep : Rep} -> RepConstraint rep Double => + (pol, az : Double) -> Vector 3 Double +unit3D pol az = vector {rep} [cos az * sin pol, sin az * sin pol, cos pol] @@ -142,9 +145,8 @@ export export swizzle : Vect n (Fin m) -> Vector m a -> Vector n a swizzle p v = rewrite sym (lengthCorrect p) - in fromFunction [length p] (\[i] => - index (index (rewrite sym (lengthCorrect p) in i) p) v - ) + in fromFunction {rep=_} @{getRepC v} [length p] (\[i] => + index (index (rewrite sym (lengthCorrect p) in i) p) v) ||| Swap two coordinates in a vector. @@ -168,7 +170,6 @@ export (++) : Vector m a -> Vector n a -> Vector (m + n) a (++) = concat 0 - ||| Calculate the dot product of the two vectors. export dot : Num a => Vector n a -> Vector n a -> a