Add more utility functions
This commit is contained in:
parent
524486bb58
commit
eddb0e318c
|
@ -1,5 +1,5 @@
|
||||||
package numidr
|
package numidr
|
||||||
version = 0.2.0
|
version = 0.2.1
|
||||||
|
|
||||||
authors = "Kiana Sheibani"
|
authors = "Kiana Sheibani"
|
||||||
license = "MIT"
|
license = "MIT"
|
||||||
|
|
|
@ -516,6 +516,25 @@ stack axis arrs = rewrite sym (lengthCorrect arrs) in
|
||||||
getAxisInd FZ (i :: is) = (i, is)
|
getAxisInd FZ (i :: is) = (i, is)
|
||||||
getAxisInd {s=_::_} (FS ax) (i :: is) = mapSnd (i::) (getAxisInd ax is)
|
getAxisInd {s=_::_} (FS ax) (i :: is) = mapSnd (i::) (getAxisInd ax is)
|
||||||
|
|
||||||
|
export
|
||||||
|
joinAxes : {s' : _} -> Array s (Array s' a) -> Array (s ++ s') a
|
||||||
|
joinAxes {s} arr with (viewShape arr)
|
||||||
|
_ | Shape s = fromFunctionNB (s ++ s') (\is => arr !# takeUpTo s is !# dropUpTo s is)
|
||||||
|
where
|
||||||
|
takeUpTo : Vect rk Nat -> Vect (rk + rk') Nat -> Vect rk Nat
|
||||||
|
takeUpTo [] ys = []
|
||||||
|
takeUpTo (x::xs) (y::ys) = y :: takeUpTo xs ys
|
||||||
|
|
||||||
|
dropUpTo : Vect rk Nat -> Vect (rk + rk') Nat -> Vect rk' Nat
|
||||||
|
dropUpTo [] ys = ys
|
||||||
|
dropUpTo (x::xs) (y::ys) = dropUpTo xs ys
|
||||||
|
|
||||||
|
|
||||||
|
export
|
||||||
|
splitAxes : (rk : Nat) -> {0 rk' : Nat} -> {s : _} ->
|
||||||
|
Array {rk=rk+rk'} s a -> Array (take {m=rk'} rk s) (Array (drop {m=rk'} rk s) a)
|
||||||
|
splitAxes _ {s} arr = fromFunctionNB _ (\is => fromFunctionNB _ (\is' => arr !# (is ++ is')))
|
||||||
|
|
||||||
|
|
||||||
||| Construct the transpose of an array by reversing the order of its axes.
|
||| Construct the transpose of an array by reversing the order of its axes.
|
||||||
export
|
export
|
||||||
|
|
|
@ -120,6 +120,19 @@ setTranslation : Num a => Vector n a -> Transform ty n a
|
||||||
setTranslation v (MkTrans _ mat) = MkTrans _ (hmatrix (getMatrix mat) v)
|
setTranslation v (MkTrans _ mat) = MkTrans _ (hmatrix (getMatrix mat) v)
|
||||||
|
|
||||||
|
|
||||||
|
namespace Vector
|
||||||
|
export
|
||||||
|
applyInv : FieldCmp a => Transform ty n a -> Vector n a -> Vector n a
|
||||||
|
applyInv tr v = assert_total $ case solve (getMatrix tr) v of Just v' => v'
|
||||||
|
|
||||||
|
namespace Point
|
||||||
|
export
|
||||||
|
applyInv : FieldCmp a => Transform ty n a -> Point n a -> Point n a
|
||||||
|
applyInv (MkTrans _ mat) p = assert_total $
|
||||||
|
case solve (getMatrix mat) (zipWith (-) (toVector p) (getTranslationVector mat)) of
|
||||||
|
Just v => fromVector v
|
||||||
|
|
||||||
|
|
||||||
--------------------------------------------------------------------------------
|
--------------------------------------------------------------------------------
|
||||||
-- Interface implementations
|
-- Interface implementations
|
||||||
--------------------------------------------------------------------------------
|
--------------------------------------------------------------------------------
|
||||||
|
|
Loading…
Reference in a new issue