Remove Data.NP

Data.Vect.Quantifiers.All is entirely equivalent.
This commit is contained in:
Kiana Sheibani 2024-03-01 18:56:27 -05:00
parent 4e3c524b08
commit 741e389496
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
10 changed files with 16 additions and 57 deletions

View file

@ -10,8 +10,7 @@ langversion >= 0.6.0
sourcedir = "src" sourcedir = "src"
readme = "README.md" readme = "README.md"
modules = Data.NP, modules = Data.Permutation,
Data.Permutation,
Data.NumIdr, Data.NumIdr,
Data.NumIdr.PrimArray, Data.NumIdr.PrimArray,
Data.NumIdr.PrimArray.Bytes, Data.NumIdr.PrimArray.Bytes,

View file

@ -4,7 +4,6 @@
"version": "1.0.0", "version": "1.0.0",
"deps": [], "deps": [],
"modules": [ "modules": [
"Data.NP",
"Data.Permutation", "Data.Permutation",
"Data.NumIdr", "Data.NumIdr",
"Data.NumIdr.Array", "Data.NumIdr.Array",

View file

@ -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

View file

@ -1,6 +1,5 @@
module Data.NumIdr module Data.NumIdr
import public Data.NP
import public Data.Permutation import public Data.Permutation
import public Data.NumIdr.Interfaces import public Data.NumIdr.Interfaces

View file

@ -1,6 +1,5 @@
module Data.NumIdr.Array module Data.NumIdr.Array
import public Data.NP
import public Data.NumIdr.Array.Array import public Data.NumIdr.Array.Array
import public Data.NumIdr.Array.Coords import public Data.NumIdr.Array.Coords
import public Data.NumIdr.Array.Rep import public Data.NumIdr.Array.Rep

View file

@ -3,7 +3,6 @@ module Data.NumIdr.Array.Array
import Data.List import Data.List
import Data.Vect import Data.Vect
import Data.Zippable import Data.Zippable
import Data.NP
import Data.Permutation import Data.Permutation
import Data.NumIdr.Interfaces import Data.NumIdr.Interfaces
import Data.NumIdr.PrimArray import Data.NumIdr.PrimArray
@ -411,7 +410,7 @@ resize s' def arr = fromFunction {rep=getRep arr} @{getRepC arr} s' (fromMaybe d
export export
-- HACK: Come up with a solution that doesn't use `believe_me` or trip over some -- HACK: Come up with a solution that doesn't use `believe_me` or trip over some
-- weird bug in the type-checker -- 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 Array {rk} s a -> Array s' a
resizeLTE s' arr = resize s' (believe_me ()) arr resizeLTE s' arr = resize s' (believe_me ()) arr

View file

@ -4,7 +4,8 @@ import Data.Either
import Data.List import Data.List
import Data.List1 import Data.List1
import Data.Vect import Data.Vect
import Data.NP
import public Data.Vect.Quantifiers
%default total %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. ||| values of `Fin dim`, where `dim` is the dimension of each axis.
public export public export
Coords : (s : Vect rk Nat) -> Type 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`. ||| Forget the shape of the array by converting each index to type `Nat`.
export export
@ -63,7 +73,7 @@ namespace Strict
public export public export
CoordsRange : (s : Vect rk Nat) -> Type CoordsRange : (s : Vect rk Nat) -> Type
CoordsRange = NP CRange CoordsRange = All CRange
namespace NB namespace NB

View file

@ -3,7 +3,6 @@ module Data.NumIdr.PrimArray
import Data.Buffer import Data.Buffer
import Data.Vect import Data.Vect
import Data.Fin import Data.Fin
import Data.NP
import Data.NumIdr.Array.Rep import Data.NumIdr.Array.Rep
import Data.NumIdr.Array.Coords import Data.NumIdr.Array.Coords
import public Data.NumIdr.PrimArray.Bytes 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 = indexUpdate {rep = Delayed} is f arr =
\is' => \is' =>
let x = 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 export
indexRange : {rep,s : _} -> RepConstraint rep a => (rs : CoordsRange s) -> PrimArray rep s a indexRange : {rep,s : _} -> RepConstraint rep a => (rs : CoordsRange s) -> PrimArray rep s a

View file

@ -2,7 +2,6 @@ module Data.NumIdr.PrimArray.Delayed
import Data.List import Data.List
import Data.Vect import Data.Vect
import Data.NP
import Data.NumIdr.Array.Rep import Data.NumIdr.Array.Rep
import Data.NumIdr.Array.Coords import Data.NumIdr.Array.Coords

View file

@ -2,7 +2,6 @@ module Data.NumIdr.PrimArray.Linked
import Data.Vect import Data.Vect
import Data.DPair import Data.DPair
import Data.NP
import Data.NumIdr.Array.Rep import Data.NumIdr.Array.Rep
import Data.NumIdr.Array.Coords import Data.NumIdr.Array.Coords