Tweak library functions to match reps

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

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
+                    mat `hconcat` hstack [tr]
-                      {ok = sym $ multOneRightNeutral _} [m,1] 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 : {default B rep : Rep} -> RepConstraint rep a =>
-scalingH x = indexSet [last,last] 1 $ repeatDiag x 0
+            {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 : {default B rep : Rep} -> RepConstraint rep Double =>
-rotate2DH = matrixToH . rotate2D
+            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 : {default B rep : Rep} -> RepConstraint rep Double =>
-rotate3DXH = matrixToH . rotate3DX
+              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 : {default B rep : Rep} -> RepConstraint rep Double =>
-rotate3DYH = matrixToH . rotate3DY
+              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 : {default B rep : Rep} -> RepConstraint rep Double =>
-rotate3DZH = matrixToH . rotate3DZ
+              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

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 : {default B rep : Rep} -> RepConstraint rep a => {m, n : _} ->
-matrix' ord x = array' [m,n] ord x
+          Vect m (Vect n a) -> Matrix m n a
-
+matrix x = array' {rep} [m,n] x
-||| Construct a matrix with the given elements.
-export
-matrix : {m, n : _} -> Vect m (Vect n a) -> Matrix m n a
-matrix = matrix' COrder
 
 
 ||| 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 : {default B rep : Rep} -> RepConstraint rep a => {m, n : _} ->
-repeatDiag d o = fromFunctionNB [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 : {default B rep : Rep} -> RepConstraint rep a => {m, n : _} ->
-fromDiag ds o = fromFunction [m,n] (\[i,j] => maybe o (`index` ds) $ i `eq` j)
+            (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 : {default B rep : Rep} -> RepConstraint rep a => {n : _} -> Num a =>
-permuteM p = permuteInAxis 0 p (repeatDiag 1 0)
+            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 : {default B rep : Rep} -> RepConstraint rep a => {n : _} -> Num a =>
-scale x = repeatDiag x 0
+          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 : {default B rep : Rep} -> RepConstraint rep Double =>
-rotate2D a = matrix [[cos a, - sin a], [sin a, cos a]]
+            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 : {default B rep : Rep} -> RepConstraint rep Double =>
-rotate3DX a = matrix [[1,0,0], [0, cos a, - sin a], [0, sin a, cos a]]
+            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 : {default B rep : Rep} -> RepConstraint rep Double =>
-rotate3DY a = matrix [[cos a, 0, sin a], [0,1,0], [- sin a, 0, cos a]]
+            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 : {default B rep : Rep} -> RepConstraint rep Double =>
-rotate3DZ a = matrix [[cos a, - sin a, 0], [sin a, cos a, 0], [0,0,1]]
+            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 : {default B rep : Rep} -> RepConstraint rep a =>
-reflect i = indexSet [i, i] (-1) (repeatDiag 1 0)
+          {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 : {default B rep : Rep} -> RepConstraint rep a =>
-reflectX = reflect 0
+            {n : _} -> Neg a => Matrix' (1 + n) a
+reflectX = reflect {rep} 0
 
 export
-reflectY : {n : _} -> Neg a => Matrix' (2 + n) a
+reflectY : {default B rep : Rep} -> RepConstraint rep a =>
-reflectY = reflect 1
+            {n : _} -> Neg a => Matrix' (2 + n) a
+reflectY = reflect {rep} 1
 
 export
-reflectZ : {n : _} -> Neg a => Matrix' (3 + n) a
+reflectZ : {default B rep : Rep} -> RepConstraint rep a =>
-reflectZ = reflect 2
+            {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
-

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
+convertRepPrim : {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
+convertRepPrim {r1 = Bytes o, r2 = Bytes o'} @{rc} arr = reorder @{rc} arr
-convertRep {r1 = Boxed o, r2 = Boxed o'} arr = reorder arr
+convertRepPrim {r1 = Boxed o, r2 = Boxed o'} arr = reorder arr
-convertRep {r1 = Linked, r2 = Linked} arr = arr
+convertRepPrim {r1 = Linked, r2 = Linked} arr = arr
-convertRep {r1 = Linked, r2 = Bytes COrder} @{_} @{rc} arr = fromList @{rc} s (collapse arr)
+convertRepPrim {r1 = Linked, r2 = Bytes COrder} @{_} @{rc} arr = fromList @{rc} s (collapse arr)
-convertRep {r1 = Linked, r2 = Boxed COrder} arr = fromList s (collapse arr)
+convertRepPrim {r1 = Linked, r2 = Boxed COrder} arr = fromList s (collapse arr)
-convertRep {r1 = Delayed, r2 = Delayed} arr = arr
+convertRepPrim {r1 = Delayed, r2 = Delayed} arr = arr
-convertRep {r1, r2} arr = fromFunction s (\is => PrimArray.index is 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}

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

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" $
+  showPrec d (MkPoint v) = showCon d "point" $ showArg $ elements v
-    showArg $ PrimArray.toList $ getPrim v
 
 export
 Cast a b => Cast (Point n a) (Point n b) where

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

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
+           in array {rep,s=[length v]} $
-           rewrite lengthCorrect v in        -- there is only 1 axis
+           rewrite lengthCorrect v in v
-           rewrite multOneLeftNeutral n 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 : {default B rep : Rep} -> RepConstraint rep a =>
-basis i = fromFunction _ (\[j] => if i == j then 1 else 0)
+          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 : {default B rep : Rep} -> RepConstraint rep a =>
-basisX = basis FZ
+          {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 : {default B rep : Rep} -> RepConstraint rep a =>
-basisY = basis (FS FZ)
+          {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 : {default B rep : Rep} -> RepConstraint rep a =>
-basisZ = basis (FS (FS FZ))
+          {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 : {default B rep : Rep} -> RepConstraint rep Double =>
-unit2D ang = vector [cos ang, sin ang]
+          (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 : {default B rep : Rep} -> RepConstraint rep Double =>
-unit3D pol az = vector [cos az * sin pol, sin az * sin pol, cos pol]
+          (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] =>
+              in fromFunction {rep=_} @{getRepC v} [length p] (\[i] =>
-                index (index (rewrite sym (lengthCorrect p) in i) p) v
+                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