From 03d06a42aa6e161d54c5c6a256cca6258cfbad56 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Mon, 13 Jun 2022 14:42:35 -0400 Subject: [PATCH] Rename stack to concat --- src/Data/NumIdr/Array/Array.idr | 22 +++++++++++----------- src/Data/NumIdr/Matrix.idr | 8 ++++---- src/Data/NumIdr/Vector.idr | 4 ++-- 3 files changed, 17 insertions(+), 17 deletions(-) diff --git a/src/Data/NumIdr/Array/Array.idr b/src/Data/NumIdr/Array/Array.idr index 59677f9..2519a9d 100644 --- a/src/Data/NumIdr/Array/Array.idr +++ b/src/Data/NumIdr/Array/Array.idr @@ -289,18 +289,18 @@ enumerate arr = map (\is => (is, index is arr)) (rewrite shapeEq arr in getAllCoords $ shape arr) export -stack : (axis : Fin rk) -> Array {rk} s a -> Array (replaceAt axis d s) a -> +concat : (axis : Fin rk) -> Array {rk} s a -> Array (replaceAt axis d s) a -> Array (updateAt axis (+d) s) a -stack axis a b = let sA = shape a - sB = shape b - dA = index axis sA - dB = index axis sB - s = replaceAt axis (dA + dB) sA - sts = calcStrides COrder s - ins = map (mapFst $ getLocation' sts . toNats) (enumerate a) - ++ map (mapFst $ getLocation' sts . updateAt axis (+dA) . toNats) (enumerate b) - -- TODO: prove that the type-level shape and `s` are equivalent - in believe_me $ MkArray COrder sts s (unsafeFromIns (product s) ins) +concat axis a b = let sA = shape a + sB = shape b + dA = index axis sA + dB = index axis sB + s = replaceAt axis (dA + dB) sA + sts = calcStrides COrder s + ins = map (mapFst $ getLocation' sts . toNats) (enumerate a) + ++ map (mapFst $ getLocation' sts . updateAt axis (+dA) . toNats) (enumerate b) + -- TODO: prove that the type-level shape and `s` are equivalent + in believe_me $ MkArray COrder sts s (unsafeFromIns (product s) ins) diff --git a/src/Data/NumIdr/Matrix.idr b/src/Data/NumIdr/Matrix.idr index 41bc346..2011a83 100644 --- a/src/Data/NumIdr/Matrix.idr +++ b/src/Data/NumIdr/Matrix.idr @@ -95,10 +95,10 @@ getColumn c mat = rewrite sym (minusZeroRight m) in indexRange [All, One c] mat -------------------------------------------------------------------------------- export -vstack : Matrix m n a -> Matrix m' n a -> Matrix (m + m') n a -vstack = stack 0 +vconcat : Matrix m n a -> Matrix m' n a -> Matrix (m + m') n a +vconcat = concat 0 export -hstack : Matrix m n a -> Matrix m n' a -> Matrix m (n + n') a -hstack = stack 1 +hconcat : Matrix m n a -> Matrix m n' a -> Matrix m (n + n') a +hconcat = concat 1 diff --git a/src/Data/NumIdr/Vector.idr b/src/Data/NumIdr/Vector.idr index 64ec077..c768dc2 100644 --- a/src/Data/NumIdr/Vector.idr +++ b/src/Data/NumIdr/Vector.idr @@ -94,8 +94,8 @@ swizzle p v = rewrite sym (lengthCorrect p) export -concat : Vector m a -> Vector n a -> Vector (m + n) a -concat = stack 0 +(++) : Vector m a -> Vector n a -> Vector (m + n) a +(++) = concat 0 export