Create Data.NumIdr.Transform.Transform

This commit is contained in:
Kiana Sheibani 2022-09-16 12:46:36 -04:00
parent 8839dd049a
commit 33f64c69d9
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
3 changed files with 125 additions and 8 deletions

View file

@ -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

View file

@ -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)

View file

@ -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