diff --git a/src/Data/NumIdr/Array/Array.idr b/src/Data/NumIdr/Array/Array.idr index a479500..d32141d 100644 --- a/src/Data/NumIdr/Array/Array.idr +++ b/src/Data/NumIdr/Array/Array.idr @@ -243,6 +243,7 @@ array v = MkArray COrder (calcStrides COrder s) s (fromList $ collapse v) infixl 10 !! infixl 10 !? +infixl 10 !# infixl 11 !!.. infixl 11 !?.. @@ -395,6 +396,7 @@ export elements : Array {rk} s a -> Vect (product s) a elements (MkArray _ sts sh p) = let elems = map (flip index p . getLocation' sts) (getAllCoords' sh) + -- TODO: prove that the number of elements is `product s` in assert_total $ case toVect (product sh) elems of Just v => v diff --git a/src/Data/NumIdr/Matrix.idr b/src/Data/NumIdr/Matrix.idr index 493e0cd..1e5f582 100644 --- a/src/Data/NumIdr/Matrix.idr +++ b/src/Data/NumIdr/Matrix.idr @@ -101,12 +101,12 @@ 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) + _ | Shape [m,n] = fromFunctionNB _ (\[i] => mat!#[i,i]) export diagonal : Matrix' n a -> Vector n a diagonal mat with (viewShape mat) - _ | Shape [n,n] = fromFunctionNB [n] (\[i] => indexUnsafe [i,i] mat) + _ | Shape [n,n] = fromFunctionNB [n] (\[i] => mat!#[i,i]) -------------------------------------------------------------------------------- diff --git a/src/Data/NumIdr/Vector.idr b/src/Data/NumIdr/Vector.idr index 97c8015..5cb2640 100644 --- a/src/Data/NumIdr/Vector.idr +++ b/src/Data/NumIdr/Vector.idr @@ -121,6 +121,7 @@ export -------------------------------------------------------------------------------- +||| Construct a vector by pulling coordinates from another vector. export swizzle : Vect n (Fin m) -> Vector m a -> Vector n a swizzle p v = rewrite sym (lengthCorrect p)