From 077b393bd18f8fbffd4794010b377c2eccfad3c6 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Fri, 21 Oct 2022 17:12:43 -0400 Subject: [PATCH] Document everything --- numidr.ipkg | 14 +++++- src/Data/NumIdr.idr | 12 +++++ src/Data/NumIdr/Homogeneous.idr | 24 ++++++++-- src/Data/NumIdr/Interfaces.idr | 2 +- src/Data/NumIdr/Matrix.idr | 5 +- src/Data/NumIdr/Transform/Affine.idr | 5 ++ src/Data/NumIdr/Transform/Isometry.idr | 12 ++++- src/Data/NumIdr/Transform/Linear.idr | 5 ++ src/Data/NumIdr/Transform/Orthonormal.idr | 15 ++++++ src/Data/NumIdr/Transform/Point.idr | 26 ++++++++++- src/Data/NumIdr/Transform/Rigid.idr | 26 +++++++++++ src/Data/NumIdr/Transform/Rotation.idr | 39 ++++++++++++++-- src/Data/NumIdr/Transform/Transform.idr | 56 ++++++++++++++++++----- src/Data/NumIdr/Transform/Translation.idr | 7 ++- src/Data/NumIdr/Transform/Trivial.idr | 4 ++ src/Data/NumIdr/Vector.idr | 15 +++++- src/Data/Permutation.idr | 17 +++++++ 17 files changed, 258 insertions(+), 26 deletions(-) create mode 100644 src/Data/NumIdr.idr diff --git a/numidr.ipkg b/numidr.ipkg index fc52cc8..41268e6 100644 --- a/numidr.ipkg +++ b/numidr.ipkg @@ -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 diff --git a/src/Data/NumIdr.idr b/src/Data/NumIdr.idr new file mode 100644 index 0000000..2c5bc5f --- /dev/null +++ b/src/Data/NumIdr.idr @@ -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 diff --git a/src/Data/NumIdr/Homogeneous.idr b/src/Data/NumIdr/Homogeneous.idr index 2977c93..87f5a39 100644 --- a/src/Data/NumIdr/Homogeneous.idr +++ b/src/Data/NumIdr/Homogeneous.idr @@ -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 diff --git a/src/Data/NumIdr/Interfaces.idr b/src/Data/NumIdr/Interfaces.idr index 406774c..506f146 100644 --- a/src/Data/NumIdr/Interfaces.idr +++ b/src/Data/NumIdr/Interfaces.idr @@ -36,7 +36,7 @@ export -- Multiplication -------------------------------------------------------------------------------- -infixr 9 *. +infixl 9 *. infixr 10 ^ ||| A generalized multiplication/application operator. This interface is diff --git a/src/Data/NumIdr/Matrix.idr b/src/Data/NumIdr/Matrix.idr index 865ea46..7cace16 100644 --- a/src/Data/NumIdr/Matrix.idr +++ b/src/Data/NumIdr/Matrix.idr @@ -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]] diff --git a/src/Data/NumIdr/Transform/Affine.idr b/src/Data/NumIdr/Transform/Affine.idr index 58f2ee6..2438ea5 100644 --- a/src/Data/NumIdr/Transform/Affine.idr +++ b/src/Data/NumIdr/Transform/Affine.idr @@ -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 diff --git a/src/Data/NumIdr/Transform/Isometry.idr b/src/Data/NumIdr/Transform/Isometry.idr index bc7369a..93efb8d 100644 --- a/src/Data/NumIdr/Transform/Isometry.idr +++ b/src/Data/NumIdr/Transform/Isometry.idr @@ -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 diff --git a/src/Data/NumIdr/Transform/Linear.idr b/src/Data/NumIdr/Transform/Linear.idr index d58142c..6766053 100644 --- a/src/Data/NumIdr/Transform/Linear.idr +++ b/src/Data/NumIdr/Transform/Linear.idr @@ -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)) diff --git a/src/Data/NumIdr/Transform/Orthonormal.idr b/src/Data/NumIdr/Transform/Orthonormal.idr index 0286283..9209dca 100644 --- a/src/Data/NumIdr/Transform/Orthonormal.idr +++ b/src/Data/NumIdr/Transform/Orthonormal.idr @@ -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) diff --git a/src/Data/NumIdr/Transform/Point.idr b/src/Data/NumIdr/Transform/Point.idr index 98cc76c..e4d149e 100644 --- a/src/Data/NumIdr/Transform/Point.idr +++ b/src/Data/NumIdr/Transform/Point.idr @@ -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 diff --git a/src/Data/NumIdr/Transform/Rigid.idr b/src/Data/NumIdr/Transform/Rigid.idr index a4f6732..7a6de96 100644 --- a/src/Data/NumIdr/Transform/Rigid.idr +++ b/src/Data/NumIdr/Transform/Rigid.idr @@ -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) diff --git a/src/Data/NumIdr/Transform/Rotation.idr b/src/Data/NumIdr/Transform/Rotation.idr index a425c33..b4f32e1 100644 --- a/src/Data/NumIdr/Transform/Rotation.idr +++ b/src/Data/NumIdr/Transform/Rotation.idr @@ -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] diff --git a/src/Data/NumIdr/Transform/Transform.idr b/src/Data/NumIdr/Transform/Transform.idr index 439cd69..e60931c 100644 --- a/src/Data/NumIdr/Transform/Transform.idr +++ b/src/Data/NumIdr/Transform/Transform.idr @@ -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 diff --git a/src/Data/NumIdr/Transform/Translation.idr b/src/Data/NumIdr/Transform/Translation.idr index ed34b59..6ebdbcb 100644 --- a/src/Data/NumIdr/Transform/Translation.idr +++ b/src/Data/NumIdr/Transform/Translation.idr @@ -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 diff --git a/src/Data/NumIdr/Transform/Trivial.idr b/src/Data/NumIdr/Transform/Trivial.idr index 7a8ecf3..c0d26e8 100644 --- a/src/Data/NumIdr/Transform/Trivial.idr +++ b/src/Data/NumIdr/Transform/Trivial.idr @@ -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) diff --git a/src/Data/NumIdr/Vector.idr b/src/Data/NumIdr/Vector.idr index 41c8cfb..84ebac1 100644 --- a/src/Data/NumIdr/Vector.idr +++ b/src/Data/NumIdr/Vector.idr @@ -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) diff --git a/src/Data/Permutation.idr b/src/Data/Permutation.idr index 78b6f83..56cf355 100644 --- a/src/Data/Permutation.idr +++ b/src/Data/Permutation.idr @@ -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