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

Document everything

Browse source
This commit is contained in:
Kiana Sheibani 2022-10-21 17:12:43 -04:00
parent 1ad4c1f13c
commit 077b393bd1
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
17 changed files with 258 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
numidr.ipkg
View file

@ -11,6 +11,7 @@ readme = "README.md"
modules = Data.NP,
Data.Permutation,
Data.NumIdr,
Data.NumIdr.Array,
Data.NumIdr.Array.Array,
Data.NumIdr.Array.Coords,
@ -20,4 +21,15 @@ modules = Data.NP,
Data.NumIdr.Interfaces,
Data.NumIdr.PrimArray,
Data.NumIdr.Scalar,
Data.NumIdr.Vector
Data.NumIdr.Vector,
Data.NumIdr.Transform,
Data.NumIdr.Transform.Affine,
Data.NumIdr.Transform.Isometry,
Data.NumIdr.Transform.Linear,
Data.NumIdr.Transform.Orthonormal,
Data.NumIdr.Transform.Point,
Data.NumIdr.Transform.Rigid,
Data.NumIdr.Transform.Rotation,
Data.NumIdr.Transform.Transform,
Data.NumIdr.Transform.Translation,
Data.NumIdr.Transform.Trivial

12
src/Data/NumIdr.idr Normal file
View file

@ -0,0 +1,12 @@
module Data.NumIdr
import public Data.NP
import public Data.Permutation
import public Data.NumIdr.Interfaces
import public Data.NumIdr.Array
import public Data.NumIdr.Scalar
import public Data.NumIdr.Vector
import public Data.NumIdr.Matrix
import public Data.NumIdr.Homogeneous
import public Data.NumIdr.Transform

24
src/Data/NumIdr/Homogeneous.idr
View file

@ -42,29 +42,37 @@ HVector n = Vector (S n)
--------------------------------------------------------------------------------
||| Convert a vector to a homogeneous vector.
export
vectorToH : Num a => Vector n a -> HVector n a
vectorToH v = rewrite plusCommutative 1 n in v ++ vector [1]
||| Convert a vector to a homogeneous vector that ignores the translation
||| component of homogeneous matrices.
export
vectorToHLinear : Num a => Vector n a -> HVector n a
vectorToHLinear v = rewrite plusCommutative 1 n in v ++ vector [0]
||| Construct a homogeneous vector given its coordinates.
export
hvector : Num a => Vect n a -> HVector n a
hvector v = rewrite plusCommutative 1 n in vector (v ++ [1])
||| Construct a homogeneous vector that ignores translations given its
||| coordinates.
export
hvectorLinear : Num a => Vect n a -> HVector n a
hvectorLinear v = rewrite plusCommutative 1 n in vector (v ++ [0])
||| Extract a normal vector from a homogeneous vector.
export
fromHomogeneous : HVector n a -> Vector n a
fromHomogeneous = vector . init . toVect
-- HACK: Find an implementation for `fromHomogeneous` that doesn't suck
fromHomogeneous {n} v with (viewShape v)
_ | Shape [S n] = resizeLTE [n] v {ok = [lteSuccRight reflexive]}
||| Construct a homogeneous matrix given a matrix and a translation vector.
export
hmatrix : Num a => Matrix m n a -> Vector m a -> HMatrix m n a
hmatrix {m,n} mat tr with (viewShape mat)
@ -73,14 +81,16 @@ hmatrix {m,n} mat tr with (viewShape mat)
mat `hconcat` reshape
{ok = sym $ multOneRightNeutral _} [m,1] tr
||| Convert a regular matrix to a homogeneous matrix.
export
matrixToH : Num a => Matrix m n a -> HMatrix m n a
matrixToH {m,n} mat with (viewShape mat)
_ | Shape [m,n] = indexSet [last,last] 1 $ resize [S m, S n] 0 mat
||| Determine if a matrix fits the pattern of a homogeneous matrix.
export
isHMatrix : (Eq a, Num a) => Matrix m n a -> Bool
isHMatrix : Eq a => Num a => Matrix m n a -> Bool
isHMatrix {m,n} mat with (viewShape mat)
isHMatrix {m=Z,n} mat | Shape [Z,n] = False
isHMatrix {m=S m,n=Z} mat | Shape [S m,Z] = False
@ -88,12 +98,14 @@ isHMatrix {m,n} mat with (viewShape mat)
getRow last mat == resize _ 1 (zeros [n])
||| Get the regular matrix component of a homogeneous matrix.
export
getMatrix : HMatrix m n a -> Matrix m n a
getMatrix {m,n} mat with (viewShape mat)
_ | Shape [S m, S n] = resizeLTE [m,n] mat
{ok = [lteSuccRight reflexive,lteSuccRight reflexive]}
||| Get the translation vector from a homogeneous matrix.
export
getTranslationVector : HMatrix m n a -> Vector m a
getTranslationVector {m,n} mat with (viewShape mat)
@ -106,27 +118,33 @@ getTranslationVector {m,n} mat with (viewShape mat)
--------------------------------------------------------------------------------
||| Construct a homogeneous matrix that scales a vector by the input.
export
scalingH : {n : _} -> Num a => a -> HMatrix' n a
scalingH x = indexSet [last,last] 1 $ repeatDiag x 0
||| Construct a homogeneous matrix that translates by the given vector.
export
translationH : Num a => Vector n a -> HMatrix' n a
translationH {n} v with (viewShape v)
_ | Shape [n] = hmatrix identity v
||| Construct a 2D homogeneous matrix that rotates by the given angle (in radians).
export
rotate2DH : Double -> HMatrix' 2 Double
rotate2DH = matrixToH . rotate2D
||| Construct a 3D homogeneous matrix that rotates around the x-axis.
export
rotate3DXH : Double -> HMatrix' 3 Double
rotate3DXH = matrixToH . rotate3DX
||| Construct a 3D homogeneous matrix that rotates around the y-axis.
export
rotate3DYH : Double -> HMatrix' 3 Double
rotate3DYH = matrixToH . rotate3DY
||| Construct a 3D homogeneous matrix that rotates around the z-axis.
export
rotate3DZH : Double -> HMatrix' 3 Double
rotate3DZH = matrixToH . rotate3DZ

2
src/Data/NumIdr/Interfaces.idr
View file

@ -36,7 +36,7 @@ export
-- Multiplication
--------------------------------------------------------------------------------
infixr 9 *.
infixl 9 *.
infixr 10 ^
||| A generalized multiplication/application operator. This interface is

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

@ -74,20 +74,23 @@ export
scale : {n : _} -> Num a => a -> Matrix' n a
scale x = repeatDiag x 0
||| Calculate the rotation matrix of an angle.
||| Construct a 2D rotation matrix that rotates by the given angle (in radians).
export
rotate2D : Double -> Matrix' 2 Double
rotate2D a = matrix [[cos a, - sin a], [sin a, cos a]]
||| Construct a 3D rotation matrix around the x-axis.
export
rotate3DX : Double -> Matrix' 3 Double
rotate3DX a = matrix [[1,0,0], [0, cos a, - sin a], [0, sin a, cos a]]
||| Construct a 3D rotation matrix around the y-axis.
export
rotate3DY : Double -> Matrix' 3 Double
rotate3DY a = matrix [[cos a, 0, sin a], [0,1,0], [- sin a, 0, cos a]]
||| Construct a 3D rotation matrix around the z-axis.
export
rotate3DZ : Double -> Matrix' 3 Double
rotate3DZ a = matrix [[cos a, - sin a, 0], [sin a, cos a, 0], [0,0,1]]

5
src/Data/NumIdr/Transform/Affine.idr
View file

@ -12,14 +12,19 @@ import Data.NumIdr.Transform.Transform
%default total
||| An affine transform can contain any invertible affine map.
public export
Affine : Nat -> Type -> Type
Affine = Transform TAffine
||| Determine if a homogeneous matrix represents an affine transform
||| (i.e. is invertible).
export
isAffine : FieldCmp a => HMatrix' n a -> Bool
isAffine mat = isHMatrix mat && invertible (getMatrix mat)
||| Try to construct an affine transform from a homogeneous matrix.
export
fromHMatrix : FieldCmp a => HMatrix' n a -> Maybe (Affine n a)
fromHMatrix mat = if isAffine mat

12
src/Data/NumIdr/Transform/Isometry.idr
View file

@ -8,13 +8,23 @@ import Data.NumIdr.Matrix
import Data.NumIdr.Homogeneous
import Data.NumIdr.Transform.Point
import Data.NumIdr.Transform.Transform
import Data.NumIdr.Transform.Orthonormal
%default total
||| An isometry is an affine transformation that preserves distance between
||| points. It encompasses translations, rotations, and reflections.
public export
Isometry : Nat -> Type -> Type
Isometry = Transform TIsometry
||| Determine if a matrix represents an isometry.
export
isIsometry : Eq a => Num a => HMatrix' n a -> Bool
isIsometry mat = isHMatrix mat && isOrthonormal' (getMatrix mat)
-- TODO: Add Isometry constructors
||| Try to construct an isometry from a homogeneous matrix.
export
fromHMatrix : Eq a => Num a => HMatrix' n a -> Maybe (Isometry n a)
fromHMatrix mat = if isIsometry mat then Just (unsafeMkTrans mat) else Nothing

5
src/Data/NumIdr/Transform/Linear.idr
View file

@ -12,20 +12,25 @@ import Data.NumIdr.Transform.Transform
%default total
||| A linear transform can contain any invertible linear map.
public export
Linear : Nat -> Type -> Type
Linear = Transform TLinear
||| Determine if a homogeneous matrix represents a linear transform.
export
isLinear : FieldCmp a => HMatrix' n a -> Bool
isLinear mat = isHMatrix mat && invertible (getMatrix mat)
&& all (==0) (getTranslationVector mat)
||| Try to construct a linear transform from a homogeneous matrix.
export
fromHMatrix : FieldCmp a => HMatrix' n a -> Maybe (Linear n a)
fromHMatrix mat = if isLinear mat then Just (unsafeMkTrans mat) else Nothing
||| Try to construct a linear transform from a matrix.
||| This will fail if the matrix is not invertible.
export
fromMatrix : FieldCmp a => Matrix' n a -> Maybe (Linear n a)
fromMatrix mat = if invertible mat then Just (unsafeMkTrans (matrixToH mat))

15
src/Data/NumIdr/Transform/Orthonormal.idr
View file

@ -12,39 +12,54 @@ import Data.NumIdr.Transform.Transform
%default total
||| An orthonormal transform is one that contains an orthonormal matrix,
||| also known as an improper rotation or rotoreflection.
public export
Orthonormal : Nat -> Type -> Type
Orthonormal = Transform TOrthonormal
||| Determine if a matrix represents an orthonormal transform.
export
isOrthonormal' : Eq a => Num a => Matrix' n a -> Bool
isOrthonormal' {n} mat with (viewShape mat)
_ | Shape [n,n] = identity == fromFunction [n,n] (\[i,j] => getColumn i mat `dot` getColumn j mat)
||| Try to construct an orthonormal transform from a matrix.
export
fromMatrix : Eq a => Num a => Matrix' n a -> Maybe (Orthonormal n a)
fromMatrix mat = if isOrthonormal' mat then Just (unsafeMkTrans (matrixToH mat))
else Nothing
--------------------------------------------------------------------------------
-- Reflections
--------------------------------------------------------------------------------
||| Construct an orthonormal transform that reflects a particular coordinate.
export
reflect : {n : _} -> Neg a => Fin n -> Orthonormal n a
reflect i = unsafeMkTrans $ indexSet [weaken i,weaken i] (-1) identity
||| The orthonormal transform that reflects on the x-coordinate (first coordinate).
export
reflectX : {n : _} -> Neg a => Orthonormal (1 + n) a
reflectX = reflect 0
||| The orthonormal transform that reflects on the y-coordinate (second coordinate).
export
reflectY : {n : _} -> Neg a => Orthonormal (2 + n) a
reflectY = reflect 1
||| The orthonormal transform that reflects on the z-coordinate (third coordinate).
export
reflectZ : {n : _} -> Neg a => Orthonormal (3 + n) a
reflectZ = reflect 2
||| Construct an orthonormal transform that reflects along a hyperplane of the
||| given normal vector. The input does not have to be a unit vector.
export
reflectNormal : (Neg a, Fractional a) => Vector n a -> Orthonormal n a
reflectNormal {n} v with (viewShape v)

26
src/Data/NumIdr/Transform/Point.idr
View file

@ -10,6 +10,9 @@ import Data.NumIdr.Interfaces
%default total
||| A point is a wrapper around the basic vector type, intended to be used with
||| `Transform`. These contain the exact same information as a vector, but
||| behave differently when transforms are applied to them.
export
record Point n a where
constructor MkPoint
@ -23,19 +26,23 @@ record Point n a where
--------------------------------------------------------------------------------
||| Construct a point from a vector.
export
fromVector : Vector n a -> Point n a
fromVector = MkPoint
||| Convert a point to a vector.
export
toVector : Point n a -> Vector n a
toVector = vec
||| Construct a point given its coordinates.
export
point : Vect n a -> Point n a
point = fromVector . vector
||| The origin point.
export
origin : Num a => {n : Nat} -> Point n a
origin = fromVector $ zeros [n]
@ -49,23 +56,34 @@ origin = fromVector $ zeros [n]
infixl 10 !!
infixl 10 !?
||| Index the point at the given coordinate.
export
index : Fin n -> Point n a -> a
index n (MkPoint v) = index n v
index i (MkPoint v) = index i v
||| Index the point at the given coordinate.
|||
||| This is the operator form of `index`.
export
(!!) : Point n a -> Fin n -> a
(!!) = flip index
||| Index the point at the given coordinate, returning `Nothing` if the index
||| is out of bounds.
export
indexNB : Nat -> Point n a -> Maybe a
indexNB n (MkPoint v) = indexNB n v
||| Index the point at the given coordinate, returning `Nothing` if the index
||| is out of bounds.
|||
||| This is the operator form of `indexNB`.
export
(!?) : Point n a -> Nat -> Maybe a
(!?) = flip indexNB
||| Return a `Vect` of the coordinates in the point.
export
toVect : Point n a -> Vect n a
toVect = toVect . vec
@ -73,14 +91,17 @@ toVect = toVect . vec
-- Named projections
||| Return the x-coordinate (the first value) of the vector.
export
(.x) : Point (1 + n) a -> a
(.x) = index FZ
||| Return the y-coordinate (the second value) of the vector.
export
(.y) : Point (2 + n) a -> a
(.y) = index (FS FZ)
||| Return the z-coordinate (the third value) of the vector.
export
(.z) : Point (3 + n) a -> a
(.z) = index (FS (FS FZ))
@ -98,15 +119,18 @@ infixl 8 -.
-- These would have been named simply (+) and (-), but that caused
-- too many issues with interface resolution.
||| Add a vector to a point.
export
(+.) : Num a => Vector n a -> Point n a -> Point n a
a +. MkPoint b = MkPoint (zipWith (+) a b)
||| Add a point to a vector.
export
(.+) : Num a => Point n a -> Vector n a -> Point n a
MkPoint a .+ b = MkPoint (zipWith (+) a b)
||| Subtract two points to get the vector between them.
export
(-.) : Neg a => Point n a -> Point n a -> Vector n a
MkPoint a -. MkPoint b = zipWith (-) a b

26
src/Data/NumIdr/Transform/Rigid.idr
View file

@ -8,12 +8,38 @@ import Data.NumIdr.Matrix
import Data.NumIdr.Homogeneous
import Data.NumIdr.Transform.Point
import Data.NumIdr.Transform.Transform
import Data.NumIdr.Transform.Rotation
%default total
||| A rigid transform encodes a (proper) rigid transformation, also known as a
||| rototranslation.
public export
Rigid : Nat -> Type -> Type
Rigid = Transform TRigid
-- TODO: Add Rigid constructors
||| Determine if a homogeneous matrix represents a rigid transform.
export
isRigid : FieldCmp a => HMatrix' n a -> Bool
isRigid mat = isHMatrix mat && isRotation' (getMatrix mat)
export
rigid2D : Vector 2 Double -> Double -> Rigid 2 Double
rigid2D v a = setTranslation v (rotate2D a)
||| Construct a 3D rigid transform representing an observer standing at `orig`
||| and facing towards `target`.
|||
||| @ orig The origin point, i.e. the point that the origin is mapped to.
||| @ target The point that the z-axis is directed towards.
||| @ up The vertical direction, the direction that the y-axis faces.
export
faceTowards : (orig, target : Point 3 Double) -> (up : Vector 3 Double)
-> Rigid 3 Double
faceTowards orig target up = setTranslation (toVector orig)
(faceTowards (orig -. target) up)

39
src/Data/NumIdr/Transform/Rotation.idr
View file

@ -13,32 +13,63 @@ import Data.NumIdr.Transform.Orthonormal
%default total
||| A transform that contains a rotation.
public export
Rotation : Nat -> Type -> Type
Rotation = Transform TRotation
||| Determine if a matrix represents a rotation.
-- HACK: Replace with more efficient method
export
isRotation' : FieldCmp a => Matrix' n a -> Bool
isRotation' mat = isOrthonormal mat && det mat == 1
isRotation' mat = isOrthonormal' mat && det mat == 1
||| Try to constuct a rotation from a matrix.
fromMatrix : FieldCmp a => Matrix' n a -> Maybe (Rotation n a)
fromMatrix mat = if isRotation' mat then Just (unsafeMkTrans $ matrixToH mat)
else Nothing
||| Determine if a homogeneous matrix represents a rotation.
export
isRotation : FieldCmp a => HMatrix' n a -> Bool
isRotation {n} mat with (viewShape mat)
_ | Shape [S n, S n] = isHMatrix mat && all (==0) (mat !!.. [EndBound last, One last])
||| Construct a 2D rotation that rotates by the given angle (in radians).
export
rotate2D : Num a => Double -> Rotation 2 Double
rotate2D = unsafeMkTrans . rotate2DH
--------------------------------------------------------------------------------
-- 3D rotations
--------------------------------------------------------------------------------
||| Construct a 3D rotation around the x-axis.
export
rotate3DX : Num a => Double -> Rotation 3 Double
rotate3DX : Double -> Rotation 3 Double
rotate3DX = unsafeMkTrans . rotate3DXH
||| Construct a 3D rotation around the y-axis.
export
rotate3DY : Num a => Double -> Rotation 3 Double
rotate3DY : Double -> Rotation 3 Double
rotate3DY = unsafeMkTrans . rotate3DYH
||| Construct a 3D rotation around the z-axis.
export
rotate3DZ : Num a => Double -> Rotation 3 Double
rotate3DZ : Double -> Rotation 3 Double
rotate3DZ = unsafeMkTrans . rotate3DZH
||| Construct a rotation representing an observer facing towards `dir`.
|||
||| @ dir The facing direction, aligned with the z-axis.
||| @ up The vertical direction, the direction that the y-axis faces.
export
faceTowards : (dir, up : Vector 3 Double) -> Rotation 3 Double
faceTowards dir up = let z = normalize dir
x = normalize (up `cross` z)
y = normalize (z `cross` x)
in unsafeMkTrans $ matrixToH $ hstack [x,y,z]

56
src/Data/NumIdr/Transform/Transform.idr
View file

@ -16,12 +16,14 @@ import Data.NumIdr.Transform.Point
--------------------------------------------------------------------------------
||| A transform type encodes the properties of a transform. There are 8 transform
||| types, and together with the coersion relation `(:<)` they form a semilattice.
export
TransType : Type
TransType = (Fin 4, Bool)
namespace TransType
export
public export
TAffine, TIsometry, TRigid, TTranslation,
TLinear, TOrthonormal, TRotation, TTrivial : TransType
TAffine = (3, True)
@ -39,26 +41,46 @@ namespace TransType
--------------------------------------------------------------------------------
||| Coersion relation for transform types.
||| `a :< b` is `True` if and only if any transform of type `a` can be cast into
||| a transform of type `b`.
public export
(:<) : TransType -> TransType -> Bool
(xn, xb) :< (yn, yb) = (xn <= yn) && (xb >= yb)
(xn, xb) :< (yn, yb) = (xn <= yn) && (xb <= yb)
||| Return the type of transform resulting from multiplying transforms of
||| the two input types.
public export
transMult : TransType -> TransType -> TransType
transMult (xn, xb) (yn, yb) = (max xn yn, xb && yb)
transMult (xn, xb) (yn, yb) = (max xn yn, xb || yb)
||| Return the linearized transform type, i.e. the transform type resulting
||| from removing the translation component of the original transform.
public export
linearizeType : TransType -> TransType
linearizeType = mapSnd (const False)
||| Return the delinearized transform type, i.e. the transform type resulting
||| from adding a translation to the original transform.
public export
delinearizeType : TransType -> TransType
delinearizeType = mapSnd (const True)
||| A transform is a wrapper for a homogeneous matrix subject to certain
||| restrictions, such as a rotation, an isometry, or a rigid transform.
||| The restriction on the transform is encoded by the transform's *type*.
|||
||| Transforms have special behavior over matrices when it comes to multiplication.
||| When a transform is applied to a vector, only the linear part of the transform
||| is applied, as if `linearize` were called on the transform before the operation.
|||
||| In order for non-linear transformations to be used, the transform should be
||| applied to the special wrapper type `Point`. This separates the concepts of
||| point and vector, which is often useful when working with affine maps.
export
data Transform : TransType -> Nat -> Type -> Type where
MkTrans : (type : TransType) -> HMatrix' n a -> Transform type n a
MkTrans : (ty : TransType) -> HMatrix' n a -> Transform ty n a
%name Transform t
@ -67,15 +89,31 @@ export
unsafeMkTrans : {ty : _} -> HMatrix' n a -> Transform ty n a
unsafeMkTrans = MkTrans _
export
toHMatrix : Transform ty n a -> HMatrix' n a
toHMatrix (MkTrans _ mat) = mat
||| Unwrap the inner homogeneous matrix from a transform.
export
getHMatrix : Transform ty n a -> HMatrix' n a
getHMatrix (MkTrans _ mat) = mat
||| Unwrap the inner matrix from a transform, ignoring the translation component
||| if one exists.
export
getMatrix : Transform ty n a -> Matrix' n a
getMatrix (MkTrans _ mat) = getMatrix mat
||| Linearize a transform by removing its translation component.
||| If the transform is already linear, then this function does nothing.
export
linearize : Num a => Transform ty n a -> Transform (linearizeType ty) n a
linearize {n} (MkTrans _ mat) with (viewShape mat)
_ | Shape [S n,S n] = MkTrans _ (hmatrix (getMatrix mat) (zeros _))
||| Set the translation component of a transform.
|||
||| `setTranslation v tr == translate v *. linearize tr`
|||
||| If `tr` is linear:
||| `setTranslation v tr == translate v *. tr`
export
setTranslation : Num a => Vector n a -> Transform ty n a
-> Transform (delinearizeType ty) n a
@ -124,7 +162,3 @@ export
export
{t2 : _} -> So (t1 :< t2) => Cast a b => Cast (Transform t1 n a) (Transform t2 n b) where
cast (MkTrans t1 mat) = MkTrans t2 (cast mat)
export
Show a => Show (Transform ty n a) where
showPrec p (MkTrans ty mat) = showCon p "MkTrans" $ showArg ty ++ showArg mat

7
src/Data/NumIdr/Transform/Translation.idr
View file

@ -12,20 +12,25 @@ import Data.NumIdr.Transform.Transform
%default total
||| A translation is a transform that adds a constant vector value
||| to its input point.
public export
Translation : Nat -> Type -> Type
Translation = Transform TTranslation
||| Determine if a homogeneous matrix encodes a translation.
export
isTranslation : Eq a => Num a => HMatrix' n a -> Bool
isTranslation {n} mat with (viewShape mat)
_ | Shape [S n,S n] = isHMatrix mat && getMatrix mat == identity
||| Construct a translation given a vector.
export
translate : Num a => Vector n a -> Translation n a
translate v = unsafeMkTrans (translationH v)
||| Try to construct a translation from a homogeneous matrix.
export
fromHMatrix : (Eq a, Num a) => HMatrix' n a -> Maybe (Translation n a)
fromHMatrix : Eq a => Num a => HMatrix' n a -> Maybe (Translation n a)
fromHMatrix mat = if isTranslation mat then Just (unsafeMkTrans mat) else Nothing

4
src/Data/NumIdr/Transform/Trivial.idr
View file

@ -12,11 +12,15 @@ import Data.NumIdr.Transform.Transform
%default total
||| A trivial transform is a transform that must leave all points unchanged.
||| This transform type only exists so that `linearize` can take a translation
||| as input.
public export
Trivial : Nat -> Type -> Type
Trivial = Transform TTrivial
||| Determine if a homogeneous matrix is trivial.
export
isTrivial : Eq a => Num a => HMatrix' n a -> Bool
isTrivial {n} mat with (viewShape mat)

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

@ -132,12 +132,12 @@ swizzle p v = rewrite sym (lengthCorrect p)
)
||| Swap two entries in a vector.
||| Swap two coordinates in a vector.
export
swapCoords : (i,j : Fin n) -> Vector n a -> Vector n a
swapCoords = swapInAxis 0
||| Permute the entries in a vector.
||| Permute the coordinates in a vector.
export
permuteCoords : Permutation n -> Vector n a -> Vector n a
permuteCoords = permuteInAxis 0
@ -166,3 +166,14 @@ perp : Neg a => Vector 2 a -> Vector 2 a -> a
perp a b = a.x * b.y - a.y * b.x
||| Calculate the cross product of the two vectors.
export
cross : Neg a => Vector 3 a -> Vector 3 a -> Vector 3 a
cross v1 v2 = let [a, b, c] = elements v1
[x, y, z] = elements v2
in vector [b*z - c*y, c*x - a*z, a*y - b*x]
||| Calculate the triple product of the three vectors.
export
triple : Neg a => Vector 3 a -> Vector 3 a -> Vector 3 a -> a
triple a b c = a `dot` (b `cross` c)

17
src/Data/Permutation.idr
View file

@ -6,24 +6,37 @@ import Data.NumIdr.Interfaces
%default total
||| A permutation in `n` elements.
|||
||| Permutations are internally stored as a list of elements to swap in
||| right-to-left order. This allows for easy composition and inversion of
||| permutation values.
export
record Permutation n where
constructor MkPerm
swaps : List (Fin n, Fin n)
||| Construct a permutation that swaps two elements.
export
swap : (i,j : Fin n) -> Permutation n
swap x y = MkPerm [(x,y)]
||| Construct a permutation that makes the listed swaps in right-to-left order.
export
swaps : List (Fin n, Fin n) -> Permutation n
swaps = MkPerm
||| Add a swap to the end of a permutation.
|||
||| `appendSwap sw p = swap sw *. p`
export
appendSwap : (i,j : Fin n) -> Permutation n -> Permutation n
appendSwap i j (MkPerm a) = MkPerm ((i,j)::a)
||| Add a swap to the beginning of a permutation.
|||
||| `prependSwap sw p = p *. swap sw`
export
prependSwap : (i,j : Fin n) -> Permutation n -> Permutation n
prependSwap i j (MkPerm a) = MkPerm (a `snoc` (i,j))
@ -33,6 +46,7 @@ mon : Monoid (a -> a)
mon = MkMonoid @{MkSemigroup (.)} id
||| Swap two elements of a `Vect`.
export
swapElems : (i,j : Fin n) -> Vect n a -> Vect n a
swapElems i j v =
@ -41,17 +55,20 @@ swapElems i j v =
y = index j v
in replaceAt j x $ replaceAt i y v
||| Permute the elements of a `Vect`.
export
permuteVect : Permutation n -> Vect n a -> Vect n a
permuteVect p = foldMap @{%search} @{mon} (uncurry swapElems) p.swaps
||| Construct a function that swaps two values.
export
swapValues : (i,j : Fin n) -> Nat -> Nat
swapValues i j x = if x == cast i then cast j
else if x == cast j then cast i
else x
||| Construct a function that permutes values.
export
permuteValues : Permutation n -> Nat -> Nat
permuteValues p = foldMap @{%search} @{mon} (uncurry swapValues) p.swaps