diff --git a/src/Data/NumIdr/Transform/Point.idr b/src/Data/NumIdr/Transform/Point.idr new file mode 100644 index 0000000..4f5b0f4 --- /dev/null +++ b/src/Data/NumIdr/Transform/Point.idr @@ -0,0 +1,121 @@ +module Data.NumIdr.Transform.Point + +import Data.Vect +import Data.NumIdr.PrimArray +import Data.NumIdr.Array +import Data.NumIdr.Vector +import Data.NumIdr.Matrix +import Data.NumIdr.Multiply + +%default total + + +export +record Point n a where + constructor MkPoint + vec : Vector n a + + +-------------------------------------------------------------------------------- +-- Point constructors +-------------------------------------------------------------------------------- + + +export +fromVector : Vector n a -> Point n a +fromVector = MkPoint + +export +point : Vect n a -> Point n a +point = fromVector . vector + + +export +origin : Num a => {n : Nat} -> Point n a +origin = fromVector $ zeros [n] + + +-------------------------------------------------------------------------------- +-- Point indexing +-------------------------------------------------------------------------------- + + +infixl 10 !! +infixl 10 !? + +export +index : Fin n -> Point n a -> a +index n (MkPoint v) = index n v + +export +(!!) : Point n a -> Fin n -> a +(!!) = flip index + +export +indexNB : Nat -> Point n a -> Maybe a +indexNB n (MkPoint v) = indexNB n v + +export +(!?) : Point n a -> Nat -> Maybe a +(!?) = flip indexNB + + +export +toVect : Point n a -> Vect n a +toVect = toVect . vec + + +-- Named projections + +export +(.x) : Point (1 + n) a -> a +(.x) = index FZ + +export +(.y) : Point (2 + n) a -> a +(.y) = index (FS FZ) + +export +(.z) : Point (3 + n) a -> a +(.z) = index (FS (FS FZ)) + + +-------------------------------------------------------------------------------- +-- Interface implementations +-------------------------------------------------------------------------------- + + +namespace Right + export + (+) : Num a => Point n a -> Vector n a -> Point n a + MkPoint a + b = MkPoint (zipWith (+) a b) + +namespace Left + export + (+) : Num a => Vector n a -> Point n a -> Point n a + a + MkPoint b = MkPoint (zipWith (+) a b) + + +export +(-) : Neg a => Point n a -> Point n a -> Vector n a +MkPoint a - MkPoint b = zipWith (-) a b + + +-------------------------------------------------------------------------------- +-- Interface implementations +-------------------------------------------------------------------------------- + + +export +Show a => Show (Point n a) where + showPrec d (MkPoint v) = showCon d "point " $ + show $ PrimArray.toList $ getPrim v + +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/Rotation.idr b/src/Data/NumIdr/Transform/Rotation.idr new file mode 100644 index 0000000..e69de29 diff --git a/src/Data/NumIdr/Transform/Translation.idr b/src/Data/NumIdr/Transform/Translation.idr new file mode 100644 index 0000000..5c7c1dd --- /dev/null +++ b/src/Data/NumIdr/Transform/Translation.idr @@ -0,0 +1,36 @@ +module Data.NumIdr.Transform.Translation + +import Data.Vect +import Data.NumIdr.Multiply +import Data.NumIdr.Array +import Data.NumIdr.Vector +import Data.NumIdr.Transform.Point + +%default total + + +export +record Translation n a where + constructor MkTrl + offset : Vector n a + +export +fromVector : Vector n a -> Translation n a +fromVector = MkTrl + + +export +Cast a b => Cast (Translation n a) (Translation n b) where + cast (MkTrl v) = MkTrl (cast v) + +export +Num a => Mult (Translation n a) (Translation n a) (Translation n a) where + MkTrl a *. MkTrl b = MkTrl (zipWith (+) a b) + +export +{n : _} -> Num a => MultMonoid (Translation n a) where + identity = MkTrl $ zeros [n] + +export +{n : _} -> Neg a => MultGroup (Translation n a) where + inverse (MkTrl v) = MkTrl (-v)