toki/numidr
1
0
Fork 0
Code Issues Pull requests Activity

Add function for delaying array modification

Browse source
This commit is contained in:
Kiana Sheibani 2024-04-28 00:00:06 -04:00
parent 3b361caeb7
commit 76e4137d37
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
2 changed files with 12 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Data/NumIdr/Array/Array.idr
View file

@ -388,6 +388,12 @@ export
convertRep : (rep : Rep) -> RepConstraint rep a => Array s a -> Array s a convertRep : (rep : Rep) -> RepConstraint rep a => Array s a -> Array s a
convertRep rep (MkArray _ s arr) = MkArray rep s (convertRepPrim arr) convertRep rep (MkArray _ s arr) = MkArray rep s (convertRepPrim arr)
||| Temporarily convert an array to a delayed representation to make modifying
||| it more efficient, then convert it back to its original representation.
export
delayed : (Array s a -> Array s' a) -> Array s a -> Array s' a
delayed f arr = convertRep (getRep arr) @{getRepC arr} $ f $ convertRep Delayed arr
||| Resize the array to a new shape, preserving the coordinates of the original ||| Resize the array to a new shape, preserving the coordinates of the original
||| elements. New coordinates are filled with a default value. ||| elements. New coordinates are filled with a default value.
||| |||

15
src/Data/NumIdr/Matrix.idr
View file

@ -403,12 +403,12 @@ gaussStep i lu =
export export
decompLU : Field a => (mat : Matrix m n a) -> Maybe (DecompLU mat) decompLU : Field a => (mat : Matrix m n a) -> Maybe (DecompLU mat)
decompLU {m,n} mat with (viewShape mat) decompLU {m,n} mat with (viewShape mat)
_ | Shape [m,n] = map (MkLU . convertRep _ @{getRepC mat}) _ | Shape [m,n] = map MkLU
$ iterateN (minimum m n) (\i => (>>= gaussStepMaybe i)) (Just (convertRep Delayed mat)) $ iterateN (minimum m n) (\i => (>>= gaussStepMaybe i)) (Just mat)
where where
gaussStepMaybe : Fin (minimum m n) -> Matrix m n a -> Maybe (Matrix m n a) gaussStepMaybe : Fin (minimum m n) -> Matrix m n a -> Maybe (Matrix m n a)
gaussStepMaybe i mat = if mat!#[cast i,cast i] == 0 then Nothing gaussStepMaybe i mat = if mat!#[cast i,cast i] == 0 then Nothing
else Just (gaussStep i mat) else Just $ gaussStep i mat
||| The LUP decomposition of a matrix. ||| The LUP decomposition of a matrix.
@ -512,17 +512,14 @@ decompLUP : FieldCmp a => (mat : Matrix m n a) -> DecompLUP mat
decompLUP {m,n} mat with (viewShape mat) decompLUP {m,n} mat with (viewShape mat)
decompLUP {m=0,n} mat | Shape [0,n] = MkLUP mat identity 0 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 decompLUP {m=S m,n=0} mat | Shape [S m,0] = MkLUP mat identity 0
decompLUP {m=S m,n=S n} mat | Shape [S m,S n] = undelay $ decompLUP {m=S m,n=S n} mat | Shape [S m,S n] =
iterateN (S $ minimum m n) gaussStepSwap (MkLUP (convertRep Delayed mat) identity 0) iterateN (S $ minimum m n) gaussStepSwap (MkLUP mat identity 0)
where where
undelay : DecompLUP mat -> DecompLUP mat
undelay (MkLUP mat' p sw) = MkLUP (convertRep _ @{getRepC mat} mat') p sw
maxIndex : (s,a) -> List (s,a) -> (s,a) maxIndex : (s,a) -> List (s,a) -> (s,a)
maxIndex x [] = x maxIndex x [] = x
maxIndex _ [x] = x maxIndex _ [x] = x
maxIndex x ((a,b)::(c,d)::xs) = maxIndex x ((a,b)::(c,d)::xs) =
if abslt b d then assert_total $ maxIndex x ((c,d)::xs) if abslt b d then maxIndex x ((c,d)::xs)
else assert_total $ maxIndex x ((a,b)::xs) else assert_total $ maxIndex x ((a,b)::xs)
gaussStepSwap : Fin (S $ minimum m n) -> DecompLUP mat -> DecompLUP mat gaussStepSwap : Fin (S $ minimum m n) -> DecompLUP mat -> DecompLUP mat