diff --git a/src/Data/NumIdr/Homogeneous.idr b/src/Data/NumIdr/Homogeneous.idr index e91f466..16b4708 100644 --- a/src/Data/NumIdr/Homogeneous.idr +++ b/src/Data/NumIdr/Homogeneous.idr @@ -103,8 +103,9 @@ scalingH : {n : _} -> Num a => a -> HMatrix' n a scalingH x = indexSet [last,last] 1 $ repeatDiag x 0 export -translationH : {n : _} -> Num a => Vector n a -> HMatrix' n a -translationH = hmatrix identity +translationH : Num a => Vector n a -> HMatrix' n a +translationH {n} v with (viewShape v) + _ | Shape [n] = hmatrix identity v export rotation2DH : Double -> HMatrix' 2 Double diff --git a/src/Data/NumIdr/Transform/Point.idr b/src/Data/NumIdr/Transform/Point.idr index fdb9f06..b7cdf95 100644 --- a/src/Data/NumIdr/Transform/Point.idr +++ b/src/Data/NumIdr/Transform/Point.idr @@ -27,6 +27,10 @@ export fromVector : Vector n a -> Point n a fromVector = MkPoint +export +toVector : Point n a -> Vector n a +toVector = vec + export point : Vect n a -> Point n a point = fromVector . vector @@ -83,20 +87,22 @@ export -------------------------------------------------------------------------------- --- Interface implementations +-- Arithmetic operations -------------------------------------------------------------------------------- -namespace Right - export - (+) : Num a => Point n a -> Vector n a -> Point n a - MkPoint a + b = MkPoint (zipWith (+) a b) +-- Affine space operations namespace Left export (+) : Num a => Vector n a -> Point n a -> Point n a a + MkPoint b = MkPoint (zipWith (+) a b) +namespace Right + export + (+) : Num a => Point n a -> Vector n a -> Point n a + MkPoint a + b = MkPoint (zipWith (+) a b) + export (-) : Neg a => Point n a -> Point n a -> Vector n a @@ -108,6 +114,39 @@ MkPoint a - MkPoint b = zipWith (-) a b -------------------------------------------------------------------------------- +export +Zippable (Point n) where + zipWith f (MkPoint v1) (MkPoint v2) = MkPoint (zipWith f v1 v2) + zipWith3 f (MkPoint v1) (MkPoint v2) (MkPoint v3) = MkPoint (zipWith3 f v1 v2 v3) + unzipWith f (MkPoint v) = bimap MkPoint MkPoint (unzipWith f v) + unzipWith3 f (MkPoint v) = bimap MkPoint (bimap MkPoint MkPoint) (unzipWith3 f v) + +export +Functor (Point n) where + map f (MkPoint v) = MkPoint (map f v) + +export +{n : _} -> Applicative (Point n) where + pure = MkPoint . pure + MkPoint f <*> MkPoint v = MkPoint (f <*> v) + +{n : _} -> Monad (Point n) where + join (MkPoint v) = MkPoint $ join $ map unwrap v + where + unwrap : Point n a -> Vector n a + unwrap (MkPoint x) = x + +export +Foldable (Point n) where + foldl f z (MkPoint v) = foldl f z v + foldr f z (MkPoint v) = foldr f z v + null (MkPoint v) = null v + toList (MkPoint v) = toList v + +export +Traversable (Point n) where + traverse f (MkPoint v) = map MkPoint (traverse f v) + export Show a => Show (Point n a) where showPrec d (MkPoint v) = showCon d "point " $ @@ -117,7 +156,6 @@ export Cast a b => Cast (Point n a) (Point n b) where cast (MkPoint v) = MkPoint (cast v) - export Num a => Mult (Matrix m n a) (Point n a) (Point m a) where mat *. MkPoint v = MkPoint (mat *. v) diff --git a/src/Data/NumIdr/Transform/Transform.idr b/src/Data/NumIdr/Transform/Transform.idr new file mode 100644 index 0000000..0a0d594 --- /dev/null +++ b/src/Data/NumIdr/Transform/Transform.idr @@ -0,0 +1,78 @@ +module Data.NumIdr.Transform.Transform + +import Data.Vect +import Data.NumIdr.Interfaces +import Data.NumIdr.Array +import Data.NumIdr.Vector +import Data.NumIdr.Matrix +import Data.NumIdr.Homogeneous +import Data.NumIdr.Transform.Point + +public export +data TransType = TAffine | TIsometry | TRigid | TTranslation + | TLinear | TOrthonormal | TRotation | TTrivial + + +-- Lower numbers can be coerced to higher numbers +toSignature : TransType -> (Fin 4, Bool) +toSignature TAffine = (3, True) +toSignature TIsometry = (2, True) +toSignature TRigid = (1, True) +toSignature TTranslation = (0, True) +toSignature TLinear = (3, False) +toSignature TOrthonormal = (2, False) +toSignature TRotation = (1, False) +toSignature TTrivial = (0, False) + +public export +fromSignature : (Fin 4, Bool) -> TransType +fromSignature (3, True) = TAffine +fromSignature (2, True) = TIsometry +fromSignature (1, True) = TRigid +fromSignature (0, True) = TTranslation +fromSignature (3, False) = TLinear +fromSignature (2, False) = TOrthonormal +fromSignature (1, False) = TRotation +fromSignature (0, False) = TTrivial + +public export +(:<) : TransType -> TransType -> Bool +x :< y with (toSignature x, toSignature y) + _ | ((xn, xb), (yn, yb)) = (xn <= yn) && (xb >= yb) + +public export +transMult : TransType -> TransType -> TransType +transMult x y with (toSignature x, toSignature y) + _ | ((xn, xb), (yn, yb)) = fromSignature (max xn yn, xb && yb) + +public export +linearize : TransType -> TransType +linearize = fromSignature . mapSnd (const False) . toSignature + +export +data Transform : TransType -> Nat -> Type -> Type where + MkTrans : (type : TransType) -> HMatrix' n a -> Transform type n a + + +mulPoint : Num a => HMatrix' n a -> Point n a -> Point n a +mulPoint m p = fromVector $ zipWith (+) (getMatrix m *. toVector p) + (getTranslationVector m) + +mulVector : Num a => HMatrix' n a -> Vector n a -> Vector n a +mulVector m v = getMatrix m *. v + +export +Num a => Mult (Transform type n a) (Point n a) (Point n a) where + MkTrans _ m *. p = mulPoint m p + +export +Num a => Mult (Transform type n a) (Vector n a) (Vector n a) where + MkTrans _ m *. v = mulVector m v + +export +Num a => Mult (Transform t1 n a) (Transform t2 n a) (Transform (transMult t1 t2) n a) where + MkTrans _ m1 *. MkTrans _ m2 = MkTrans _ (m1 *. m2) + +export +{t2 : _} -> So (t1 :< t2) => Cast (Transform t1 n a) (Transform t2 n a) where + cast (MkTrans t1 m) = MkTrans t2 m