diff --git a/src/Data/NumIdr/Array/Order.idr b/src/Data/NumIdr/Array/Order.idr new file mode 100644 index 0000000..022ffdc --- /dev/null +++ b/src/Data/NumIdr/Array/Order.idr @@ -0,0 +1,30 @@ +module Data.NumIdr.Array.Order + +import Data.Vect +import Data.Permutation + +%default total + + +export +Order : (rk : Nat) -> Type +Order = Permutation + +export +COrder : {rk : Nat} -> Order rk +COrder = identity + +export +FOrder : {rk : Nat} -> Order rk +FOrder = reversed + + +scanr : (el -> res -> res) -> res -> Vect len el -> Vect (S len) res +scanr _ q0 [] = [q0] +scanr f q0 (x::xs) = f x (head qs) :: qs + where qs : Vect len res + qs = scanr f q0 xs + +export +calcStrides : Order rk -> Vect rk Nat -> Vect rk Nat +calcStrides ord v = permuteVect ord $ tail $ scanr (*) 1 v diff --git a/src/Data/NumIdr/Array/Utils.idr b/src/Data/NumIdr/Array/Utils.idr new file mode 100644 index 0000000..5364a5a --- /dev/null +++ b/src/Data/NumIdr/Array/Utils.idr @@ -0,0 +1,12 @@ +module Data.NumIdr.Array.Utils + +import Data.NumIdr.Array.Array + + +export +zeros : Num a => (s : Vect rk Nat) -> Array s a +zeros = constant 0 + +export +ones : Num a => (s : Vect rk Nat) -> Array s a +ones = constant 1