Create Data.NP

src/Data/NP.idr

@@ -0,0 +1,24 @@
+module Data.NP
+
+import Data.Vect
+
+%default total
+
+
+public export
+data NP : (f : k -> Type) -> (ts : Vect n k) -> Type where
+  Nil  : NP {k} f []
+  (::) : f t -> NP {k} f ts -> NP {k} f (t :: ts)
+
+
+public export
+(all : NP (Eq . f) ts) => Eq (NP f ts) where
+  (==) {all = []} [] [] = True
+  (==) {all = _ :: _} (x :: xs) (y :: ys) = (x == y) && (xs == ys)
+
+
+
+public export
+index : (i : Fin n) -> NP {n} f ts -> f (index i ts)
+index FZ (x :: xs) = x
+index (FS i) (x :: xs) = index i xs

src/Data/NumIdr/Array/Coords.idr

@@ -2,6 +2,7 @@ module Data.NumIdr.Array.Coords
 
 import Data.Either
 import Data.Vect
+import public Data.NP
 
 %default total
 
@@ -11,9 +12,8 @@ namespace Coords
   ||| A type-safe coordinate system for an array. The coordinates are
   ||| values of `Fin dim`, where `dim` is the dimension of each axis.
   public export
-  data Coords : (s : Vect rk Nat) -> Type where
+  Coords : (s : Vect rk Nat) -> Type
-    Nil  : Coords Nil
+  Coords = NP Fin
-    (::) : Fin dim -> Coords s -> Coords (dim :: s)
 
   ||| Forget the shape of the array by converting each index to type `Nat`.
   export
@@ -29,7 +29,7 @@ namespace Coords
 
   export
   collapse : {s : _} -> Vects s a -> List a
-  collapse {s=[]} = (::[])
+  collapse {s=[]} = pure
   collapse {s=_::_} = concat . map collapse
 
 
@@ -72,10 +72,8 @@ namespace CoordsRange
 
 
   public export
-  data CoordsRange : Vect rk Nat -> Type where
+  CoordsRange : (s : Vect rk Nat) -> Type
-    Nil  : CoordsRange []
+  CoordsRange = NP CRange
-    (::) : CRange d -> CoordsRange s -> CoordsRange (d :: s)
-
 
   public export
   cRangeToBounds : {n : Nat} -> CRange n -> Either Nat (Nat, Nat)