Update package to Idris2 0.5.1
This commit is contained in:
parent
1f2a870a2c
commit
f72826b329
GPG key ID:
6CB106C25E86A9F7
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -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,
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
Loading…
Reference in a new issue