diff --git a/numidr.ipkg b/numidr.ipkg index c093b40..fc52cc8 100644 --- a/numidr.ipkg +++ b/numidr.ipkg @@ -4,7 +4,7 @@ version = 0.1.0 authors = "Kiana Sheibani" license = "MIT" -langversion >= 0.4.0 +langversion >= 0.5.1 sourcedir = "src" readme = "README.md" diff --git a/src/Data/NumIdr/Array/Array.idr b/src/Data/NumIdr/Array/Array.idr index 14323e8..dfd9c00 100644 --- a/src/Data/NumIdr/Array/Array.idr +++ b/src/Data/NumIdr/Array/Array.idr @@ -280,7 +280,7 @@ indexSet is = indexUpdate is . const ||| Index the array using the given range of coordinates, returning a new array. export indexRange : (rs : CoordsRange s) -> Array s a -> Array (newShape rs) a -indexRange rs arr with (viewShape arr) +indexRange {s} rs arr with (viewShape arr) _ | Shape s = let ord = getOrder arr sts = calcStrides ord s' @@ -350,7 +350,7 @@ indexSetNB is = indexUpdateNB is . const export indexRangeNB : (rs : Vect rk CRangeNB) -> Array s a -> Array (newShape s rs) a -indexRangeNB rs arr with (viewShape arr) +indexRangeNB {s} rs arr with (viewShape arr) _ | Shape s = let ord = getOrder arr sts = calcStrides ord s' @@ -403,7 +403,7 @@ reshape s' arr = reshape' s' (getOrder arr) arr ||| Change the internal order of the array's elements. export reorder : Order -> Array s a -> Array s a -reorder ord' arr with (viewShape arr) +reorder {s} ord' arr with (viewShape arr) _ | Shape s = let sts = calcStrides ord' s in MkArray ord' sts _ (unsafeFromIns (product s) $ map (\is => (getLocation' sts is, index (getLocation' (strides arr) is) (getPrim arr))) $ @@ -450,7 +450,7 @@ enumerateNB (MkArray _ sts sh p) = ||| List all of the values in an array along with their coordinates. export enumerate : Array s a -> List (Coords s, a) -enumerate arr with (viewShape arr) +enumerate {s} arr with (viewShape arr) _ | Shape s = map (\is => (is, index is arr)) (getAllCoords s) @@ -487,7 +487,7 @@ stack axis arrs = rewrite sym (lengthCorrect arrs) in export transpose : Array s a -> Array (reverse s) a -transpose arr with (viewShape arr) +transpose {s} arr with (viewShape arr) _ | Shape s = fromFunctionNB (reverse s) (\is => arr !# reverse is) export @@ -497,22 +497,22 @@ export export swapAxes : (i,j : Fin rk) -> Array s a -> Array (swapElems i j s) a -swapAxes i j arr with (viewShape arr) +swapAxes {s} i j arr with (viewShape arr) _ | Shape s = fromFunctionNB _ (\is => arr !# swapElems i j is) export permuteAxes : (p : Permutation rk) -> Array s a -> Array (permuteVect p s) a -permuteAxes p arr with (viewShape arr) +permuteAxes {s} p arr with (viewShape arr) _ | Shape s = fromFunctionNB _ (\is => arr !# permuteVect p s) export swapInAxis : (ax : Fin rk) -> (i,j : Fin (index ax s)) -> Array s a -> Array s a -swapInAxis ax i j arr with (viewShape arr) +swapInAxis {s} ax i j arr with (viewShape arr) _ | Shape s = fromFunctionNB _ (\is => arr !# updateAt ax (swapValues i j) is) export permuteInAxis : (ax : Fin rk) -> Permutation (index ax s) -> Array s a -> Array s a -permuteInAxis ax p arr with (viewShape arr) +permuteInAxis {s} ax p arr with (viewShape arr) _ | Shape s = fromFunctionNB _ (\is => arr !# updateAt ax (permuteValues p) is) @@ -528,25 +528,25 @@ permuteInAxis ax p arr with (viewShape arr) export Zippable (Array s) where - zipWith f a b with (viewShape a) + zipWith {s} f a b with (viewShape a) _ | Shape s = MkArray (getOrder a) (strides a) s $ if getOrder a == getOrder b then unsafeZipWith f (getPrim a) (getPrim b) else unsafeZipWith f (getPrim a) (getPrim $ reorder (getOrder a) b) - zipWith3 f a b c with (viewShape a) + zipWith3 {s} f a b c with (viewShape a) _ | Shape s = MkArray (getOrder a) (strides a) s $ if (getOrder a == getOrder b) && (getOrder b == getOrder c) then unsafeZipWith3 f (getPrim a) (getPrim b) (getPrim c) else unsafeZipWith3 f (getPrim a) (getPrim $ reorder (getOrder a) b) (getPrim $ reorder (getOrder a) c) - unzipWith f arr with (viewShape arr) + unzipWith {s} f arr with (viewShape arr) _ | Shape s = case unzipWith f (getPrim arr) of (a, b) => (MkArray (getOrder arr) (strides arr) s a, MkArray (getOrder arr) (strides arr) s b) - unzipWith3 f arr with (viewShape arr) + unzipWith3 {s} f arr with (viewShape arr) _ | Shape s = case unzipWith3 f (getPrim arr) of (a, b, c) => (MkArray (getOrder arr) (strides arr) s a, MkArray (getOrder arr) (strides arr) s b, diff --git a/src/Data/NumIdr/Array/Order.idr b/src/Data/NumIdr/Array/Order.idr index 41c35be..339fc25 100644 --- a/src/Data/NumIdr/Array/Order.idr +++ b/src/Data/NumIdr/Array/Order.idr @@ -27,12 +27,6 @@ Eq Order where FOrder == COrder = False -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 - ||| Calculate an array's strides given its order and shape. export calcStrides : Order -> Vect rk Nat -> Vect rk Nat diff --git a/src/Data/NumIdr/Homogeneous.idr b/src/Data/NumIdr/Homogeneous.idr index 2473af5..e91f466 100644 --- a/src/Data/NumIdr/Homogeneous.idr +++ b/src/Data/NumIdr/Homogeneous.idr @@ -67,7 +67,7 @@ fromHomogeneous = vector . init . toVect export hmatrix : Num a => Matrix m n a -> Vector m a -> HMatrix m n a -hmatrix mat tr with (viewShape mat) +hmatrix {m,n} mat tr with (viewShape mat) _ | Shape [m,n] = indexSet [last,last] 1 $ resize [S m, S n] 0 $ mat `hconcat` reshape @@ -75,20 +75,20 @@ hmatrix mat tr with (viewShape mat) export matrixToH : Num a => Matrix m n a -> HMatrix m n a -matrixToH mat with (viewShape mat) +matrixToH {m,n} mat with (viewShape mat) _ | Shape [m,n] = indexSet [last,last] 1 $ resize [S m, S n] 0 mat export getMatrix : HMatrix m n a -> Matrix m n a -getMatrix mat with (viewShape mat) +getMatrix {m,n} mat with (viewShape mat) _ | Shape [S m, S n] = resizeLTE [m,n] mat {ok = [lteSuccRight reflexive,lteSuccRight reflexive]} export getTranslationVector : HMatrix m n a -> Vector m a -getTranslationVector mat with (viewShape mat) +getTranslationVector {m,n} mat with (viewShape mat) _ | Shape [S m, S n] = resizeLTE [m] {ok = [lteSuccRight reflexive]} $ getColumn last mat diff --git a/src/Data/NumIdr/Interfaces.idr b/src/Data/NumIdr/Interfaces.idr index 0d9f4a1..f092408 100644 --- a/src/Data/NumIdr/Interfaces.idr +++ b/src/Data/NumIdr/Interfaces.idr @@ -14,12 +14,12 @@ Field a = (Eq a, Neg a, Fractional a) public export -interface (Eq a, Neg a, Fractional a) => Scalar a where +interface (Eq a, Neg a, Fractional a) => FieldCmp a where abscmp : a -> a -> Ordering export -(Ord a, Abs a, Neg a, Fractional a) => Scalar a where +(Ord a, Abs a, Neg a, Fractional a) => FieldCmp a where abscmp x y = compare (abs x) (abs y) diff --git a/src/Data/NumIdr/Matrix.idr b/src/Data/NumIdr/Matrix.idr index 1d0048a..37352f7 100644 --- a/src/Data/NumIdr/Matrix.idr +++ b/src/Data/NumIdr/Matrix.idr @@ -107,12 +107,12 @@ getColumn c mat = rewrite sym (rangeLenZ m) in mat!!..[All, One c] export diagonal' : Matrix m n a -> Vector (minimum m n) a -diagonal' mat with (viewShape mat) +diagonal' {m,n} mat with (viewShape mat) _ | Shape [m,n] = fromFunctionNB _ (\[i] => mat!#[i,i]) export diagonal : Matrix' n a -> Vector n a -diagonal mat with (viewShape mat) +diagonal {n} mat with (viewShape mat) _ | Shape [n,n] = fromFunctionNB [n] (\[i] => mat!#[i,i]) @@ -123,7 +123,7 @@ minor i j mat = believe_me $ mat!!..[Filter (/=i), Filter (/=j)] filterInd : Num a => (Nat -> Nat -> Bool) -> Matrix m n a -> Matrix m n a -filterInd p mat with (viewShape mat) +filterInd {m,n} p mat with (viewShape mat) _ | Shape [m,n] = fromFunctionNB [m,n] (\[i,j] => if p i j then mat!#[i,j] else 0) export @@ -187,7 +187,7 @@ permuteColumns = permuteInAxis 1 ||| Calculate the outer product of two vectors as a matrix. export outer : Num a => Vector m a -> Vector n a -> Matrix m n a -outer a b with (viewShape a, viewShape b) +outer {m,n} a b with (viewShape a, viewShape b) _ | (Shape [m], Shape [n]) = fromFunction [m,n] (\[i,j] => a!!i * b!!j) @@ -203,13 +203,13 @@ trace = sum . diagonal' export Num a => Mult (Matrix m n a) (Vector n a) (Vector m a) where - mat *. v with (viewShape mat) + (*.) {m,n} mat v with (viewShape mat) _ | Shape [m,n] = fromFunction [m] (\[i] => sum $ map (\j => mat!![i,j] * v!!j) range) export Num a => Mult (Matrix m n a) (Matrix n p a) (Matrix m p a) where - m1 *. m2 with (viewShape m1, viewShape m2) + (*.) {m,n,p} m1 m2 with (viewShape m1, viewShape m2) _ | (Shape [m,n], Shape [n,p]) = fromFunction [m,p] (\[i,j] => sum $ map (\k => m1!![i,k] * m2!![k,j]) range) @@ -233,7 +233,7 @@ record DecompLU {0 m,n,a : _} (mat : Matrix m n a) where namespace DecompLU export lower : Num a => DecompLU {m,n,a} mat -> Matrix m (minimum m n) a - lower (MkLU lu) with (viewShape lu) + lower {m,n} (MkLU lu) with (viewShape lu) _ | Shape [m,n] = fromFunctionNB _ (\[i,j] => case compare i j of LT => 0 @@ -255,7 +255,7 @@ namespace DecompLU export upper : Num a => DecompLU {m,n,a} mat -> Matrix (minimum m n) n a - upper (MkLU lu) with (viewShape lu) + upper {m,n} (MkLU lu) with (viewShape lu) _ | Shape [m,n] = fromFunctionNB _ (\[i,j] => if i <= j then lu!#[i,j] else 0) @@ -313,7 +313,7 @@ gaussStep i lu = export decompLU : Field a => (mat : Matrix m n a) -> Maybe (DecompLU mat) -decompLU mat with (viewShape mat) +decompLU {m,n} mat with (viewShape mat) _ | Shape [m,n] = map MkLU $ iterateN (minimum m n) (\i => (>>= gaussStepMaybe i)) (Just mat) where gaussStepMaybe : Fin (minimum m n) -> Matrix m n a -> Maybe (Matrix m n a) @@ -332,7 +332,7 @@ record DecompLUP {0 m,n,a : _} (mat : Matrix m n a) where namespace DecompLUP export lower : Num a => DecompLUP {m,n,a} mat -> Matrix m (minimum m n) a - lower (MkLUP lu _ _) with (viewShape lu) + lower {m,n} (MkLUP lu _ _) with (viewShape lu) _ | Shape [m,n] = fromFunctionNB _ (\[i,j] => case compare i j of LT => 0 @@ -354,7 +354,7 @@ namespace DecompLUP export upper : Num a => DecompLUP {m,n,a} mat -> Matrix (minimum m n) n a - upper (MkLUP lu _ _) with (viewShape lu) + upper {m,n} (MkLUP lu _ _) with (viewShape lu) _ | Shape [m,n] = fromFunctionNB _ (\[i,j] => if i <= j then lu!#[i,j] else 0) @@ -389,7 +389,7 @@ fromLU (MkLU lu) = MkLUP lu identity 0 export -decompLUP : Scalar a => (mat : Matrix m n a) -> DecompLUP mat +decompLUP : FieldCmp a => (mat : Matrix m n a) -> DecompLUP mat decompLUP {m,n} mat with (viewShape mat) decompLUP {m=0,n} mat | Shape [0,n] = MkLUP mat identity 0 decompLUP {m=S m,n=0} mat | Shape [S m,0] = MkLUP mat identity 0 @@ -426,7 +426,7 @@ detWithLUP mat lup = * product (diagonal lup.lu) export -det : Scalar a => Matrix' n a -> a +det : FieldCmp a => Matrix' n a -> a det {n} mat with (viewShape mat) det {n=0} mat | Shape [0,0] = 1 det {n=1} mat | Shape [1,1] = mat!![0,0] @@ -441,7 +441,7 @@ det {n} mat with (viewShape mat) export solveLowerTri : Field a => Matrix' n a -> Vector n a -> Maybe (Vector n a) -solveLowerTri mat b with (viewShape b) +solveLowerTri {n} mat b with (viewShape b) _ | Shape [n] = if all (/=0) (diagonal mat) then Just $ vector $ reverse $ construct $ reverse $ toVect b @@ -457,7 +457,7 @@ solveLowerTri mat b with (viewShape b) export solveUpperTri : Field a => Matrix' n a -> Vector n a -> Maybe (Vector n a) -solveUpperTri mat b with (viewShape b) +solveUpperTri {n} mat b with (viewShape b) _ | Shape [n] = if all (/=0) (diagonal mat) then Just $ vector $ construct Z $ toVect b @@ -479,5 +479,5 @@ solveWithLUP mat lup b = in solveLowerTri lup.lower' b' >>= solveUpperTri lup.upper' export -solve : Scalar a => Matrix' n a -> Vector n a -> Maybe (Vector n a) +solve : FieldCmp a => Matrix' n a -> Vector n a -> Maybe (Vector n a) solve mat = solveWithLUP mat (decompLUP mat)