From 741e389496590f55add1bc348ebe19c409f46051 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Fri, 1 Mar 2024 18:56:27 -0500 Subject: [PATCH] Remove Data.NP Data.Vect.Quantifiers.All is entirely equivalent. --- numidr.ipkg | 3 +- sirdi.json | 1 - src/Data/NP.idr | 43 --------------------------- src/Data/NumIdr.idr | 1 - src/Data/NumIdr/Array.idr | 1 - src/Data/NumIdr/Array/Array.idr | 3 +- src/Data/NumIdr/Array/Coords.idr | 16 ++++++++-- src/Data/NumIdr/PrimArray.idr | 3 +- src/Data/NumIdr/PrimArray/Delayed.idr | 1 - src/Data/NumIdr/PrimArray/Linked.idr | 1 - 10 files changed, 16 insertions(+), 57 deletions(-) delete mode 100644 src/Data/NP.idr diff --git a/numidr.ipkg b/numidr.ipkg index 02c5245..f1a722a 100644 --- a/numidr.ipkg +++ b/numidr.ipkg @@ -10,8 +10,7 @@ langversion >= 0.6.0 sourcedir = "src" readme = "README.md" -modules = Data.NP, - Data.Permutation, +modules = Data.Permutation, Data.NumIdr, Data.NumIdr.PrimArray, Data.NumIdr.PrimArray.Bytes, diff --git a/sirdi.json b/sirdi.json index 815929b..b65971f 100644 --- a/sirdi.json +++ b/sirdi.json @@ -4,7 +4,6 @@ "version": "1.0.0", "deps": [], "modules": [ - "Data.NP", "Data.Permutation", "Data.NumIdr", "Data.NumIdr.Array", diff --git a/src/Data/NP.idr b/src/Data/NP.idr deleted file mode 100644 index 6ee76e4..0000000 --- a/src/Data/NP.idr +++ /dev/null @@ -1,43 +0,0 @@ -module Data.NP - -import Data.Vect - -%default total - - -||| A type constructor for heterogenous lists. -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 -(all : NP (Show . f) ts) => Show (NP f ts) where - show xs = "[" ++ elems xs ++ "]" - where - elems : {0 f,ts : _} -> (all : NP (Show . f) ts) => NP f ts -> String - elems {all=[]} [] = "" - elems {all=[_]} [x] = show x - elems {all=_::_} (x :: xs) = show x ++ ", " ++ elems xs - --- use this when idris can't figure out the constraint above -public export -eqNP : forall f. (forall t. Eq (f t)) => (x, y : NP f ts) -> Bool -eqNP [] [] = True -eqNP (x :: xs) (y :: ys) = x == y && eqNP xs ys - - -public export -head : NP f (t :: ts) -> f t -head (x :: _) = x - -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 diff --git a/src/Data/NumIdr.idr b/src/Data/NumIdr.idr index 2c5bc5f..9634f05 100644 --- a/src/Data/NumIdr.idr +++ b/src/Data/NumIdr.idr @@ -1,6 +1,5 @@ module Data.NumIdr -import public Data.NP import public Data.Permutation import public Data.NumIdr.Interfaces diff --git a/src/Data/NumIdr/Array.idr b/src/Data/NumIdr/Array.idr index 9efe967..12d6a1d 100644 --- a/src/Data/NumIdr/Array.idr +++ b/src/Data/NumIdr/Array.idr @@ -1,6 +1,5 @@ module Data.NumIdr.Array -import public Data.NP import public Data.NumIdr.Array.Array import public Data.NumIdr.Array.Coords import public Data.NumIdr.Array.Rep diff --git a/src/Data/NumIdr/Array/Array.idr b/src/Data/NumIdr/Array/Array.idr index e9ec0d9..fb33630 100644 --- a/src/Data/NumIdr/Array/Array.idr +++ b/src/Data/NumIdr/Array/Array.idr @@ -3,7 +3,6 @@ module Data.NumIdr.Array.Array import Data.List import Data.Vect import Data.Zippable -import Data.NP import Data.Permutation import Data.NumIdr.Interfaces import Data.NumIdr.PrimArray @@ -411,7 +410,7 @@ resize s' def arr = fromFunction {rep=getRep arr} @{getRepC arr} s' (fromMaybe d export -- HACK: Come up with a solution that doesn't use `believe_me` or trip over some -- weird bug in the type-checker -resizeLTE : (s' : Vect rk Nat) -> (0 ok : NP Prelude.id (zipWith LTE s' s)) => +resizeLTE : (s' : Vect rk Nat) -> (0 ok : All Prelude.id (zipWith LTE s' s)) => Array {rk} s a -> Array s' a resizeLTE s' arr = resize s' (believe_me ()) arr diff --git a/src/Data/NumIdr/Array/Coords.idr b/src/Data/NumIdr/Array/Coords.idr index 03b021e..669471a 100644 --- a/src/Data/NumIdr/Array/Coords.idr +++ b/src/Data/NumIdr/Array/Coords.idr @@ -4,7 +4,8 @@ import Data.Either import Data.List import Data.List1 import Data.Vect -import Data.NP + +import public Data.Vect.Quantifiers %default total @@ -35,7 +36,16 @@ rangeLenZ x = rangeLen 0 x `trans` minusZeroRight x ||| values of `Fin dim`, where `dim` is the dimension of each axis. public export Coords : (s : Vect rk Nat) -> Type -Coords = NP Fin +Coords = All Fin + + +-- Occasionally necessary for reasons of Idris not being great at +-- resolving interface constraints +public export +[eqCoords] Eq (Coords s) where + [] == [] = True + (x :: xs) == (y :: ys) = x == y && xs == ys + ||| Forget the shape of the array by converting each index to type `Nat`. export @@ -63,7 +73,7 @@ namespace Strict public export CoordsRange : (s : Vect rk Nat) -> Type - CoordsRange = NP CRange + CoordsRange = All CRange namespace NB diff --git a/src/Data/NumIdr/PrimArray.idr b/src/Data/NumIdr/PrimArray.idr index 3fe2480..4ce2eb7 100644 --- a/src/Data/NumIdr/PrimArray.idr +++ b/src/Data/NumIdr/PrimArray.idr @@ -3,7 +3,6 @@ module Data.NumIdr.PrimArray import Data.Buffer import Data.Vect import Data.Fin -import Data.NP import Data.NumIdr.Array.Rep import Data.NumIdr.Array.Coords import public Data.NumIdr.PrimArray.Bytes @@ -98,7 +97,7 @@ indexUpdate {rep = Linked} is f arr = update is f arr indexUpdate {rep = Delayed} is f arr = \is' => let x = arr is' - in if eqNP is is' then f x else x + in if (==) @{eqCoords} is is' then f x else x export indexRange : {rep,s : _} -> RepConstraint rep a => (rs : CoordsRange s) -> PrimArray rep s a diff --git a/src/Data/NumIdr/PrimArray/Delayed.idr b/src/Data/NumIdr/PrimArray/Delayed.idr index 96030e8..e90ae86 100644 --- a/src/Data/NumIdr/PrimArray/Delayed.idr +++ b/src/Data/NumIdr/PrimArray/Delayed.idr @@ -2,7 +2,6 @@ module Data.NumIdr.PrimArray.Delayed import Data.List import Data.Vect -import Data.NP import Data.NumIdr.Array.Rep import Data.NumIdr.Array.Coords diff --git a/src/Data/NumIdr/PrimArray/Linked.idr b/src/Data/NumIdr/PrimArray/Linked.idr index 2e9817e..1fbce1b 100644 --- a/src/Data/NumIdr/PrimArray/Linked.idr +++ b/src/Data/NumIdr/PrimArray/Linked.idr @@ -2,7 +2,6 @@ module Data.NumIdr.PrimArray.Linked import Data.Vect import Data.DPair -import Data.NP import Data.NumIdr.Array.Rep import Data.NumIdr.Array.Coords