From 1ad4c1f13cd80978bd02e1d622c6deace057f5d9 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Fri, 21 Oct 2022 10:03:43 -0400
Subject: [PATCH] Rename rotation constructors

---
 src/Data/NumIdr/Array/Array.idr           |  4 +-
 src/Data/NumIdr/Homogeneous.idr           | 18 +++---
 src/Data/NumIdr/Matrix.idr                | 20 +++----
 src/Data/NumIdr/Transform/Affine.idr      |  6 +-
 src/Data/NumIdr/Transform/Isometry.idr    |  3 +
 src/Data/NumIdr/Transform/Orthonormal.idr | 10 ++--
 src/Data/NumIdr/Transform/Point.idr       | 30 +++++-----
 src/Data/NumIdr/Transform/Rigid.idr       |  2 +
 src/Data/NumIdr/Transform/Rotation.idr    | 26 ++++++++-
 src/Data/NumIdr/Transform/Transform.idr   | 71 +++++++++--------------
 src/Data/NumIdr/Transform/Translation.idr |  6 +-
 src/Data/NumIdr/Transform/Trivial.idr     |  2 +-
 src/Data/Permutation.idr                  |  4 +-
 13 files changed, 108 insertions(+), 94 deletions(-)

diff --git a/src/Data/NumIdr/Array/Array.idr b/src/Data/NumIdr/Array/Array.idr
index c17d08d..bcbeda5 100644
--- a/src/Data/NumIdr/Array/Array.idr
+++ b/src/Data/NumIdr/Array/Array.idr
@@ -273,8 +273,6 @@ export %inline
 (!!) : Array s a -> Coords s -> a
 arr !! is = index is arr
 
--- TODO: Create set/update at index functions
-
 ||| Update the entry at the given coordinates using the function.
 export
 indexUpdate : Coords s -> (a -> a) -> Array s a -> Array s a
@@ -452,7 +450,7 @@ resize s' def arr = fromFunction' s' (getOrder arr) (fromMaybe def . (arr !?) .
 |||
 ||| @ s' The shape to resize the array to
 export
--- TODO: Come up with a solution that doesn't use `believe_me` or trip over some
+-- HACK: Come up with a solution that doesn't use `believe_me` or trip over some
 -- weird bug in the type-checker
 resizeLTE : (s' : Vect rk Nat) -> (0 ok : NP Prelude.id (zipWith LTE s' s)) =>
             Array {rk} s a -> Array s' a
diff --git a/src/Data/NumIdr/Homogeneous.idr b/src/Data/NumIdr/Homogeneous.idr
index ca78360..2977c93 100644
--- a/src/Data/NumIdr/Homogeneous.idr
+++ b/src/Data/NumIdr/Homogeneous.idr
@@ -62,7 +62,7 @@ hvectorLinear v = rewrite plusCommutative 1 n in vector (v ++ [0])
 export
 fromHomogeneous : HVector n a -> Vector n a
 fromHomogeneous = vector . init . toVect
--- TODO: Find an implementation for `fromHomogeneous` that doesn't suck
+-- HACK: Find an implementation for `fromHomogeneous` that doesn't suck
 
 
 export
@@ -116,17 +116,17 @@ translationH {n} v with (viewShape v)
   _ | Shape [n] = hmatrix identity v
 
 export
-rotation2DH : Double -> HMatrix' 2 Double
-rotation2DH = matrixToH . rotation2D
+rotate2DH : Double -> HMatrix' 2 Double
+rotate2DH = matrixToH . rotate2D
 
 export
-rotation3DXH : Double -> HMatrix' 3 Double
-rotation3DXH = matrixToH . rotation3DX
+rotate3DXH : Double -> HMatrix' 3 Double
+rotate3DXH = matrixToH . rotate3DX
 
 export
-rotation3DYH : Double -> HMatrix' 3 Double
-rotation3DYH = matrixToH . rotation3DY
+rotate3DYH : Double -> HMatrix' 3 Double
+rotate3DYH = matrixToH . rotate3DY
 
 export
-rotation3DZH : Double -> HMatrix' 3 Double
-rotation3DZH = matrixToH . rotation3DZ
+rotate3DZH : Double -> HMatrix' 3 Double
+rotate3DZH = matrixToH . rotate3DZ
diff --git a/src/Data/NumIdr/Matrix.idr b/src/Data/NumIdr/Matrix.idr
index e336eca..865ea46 100644
--- a/src/Data/NumIdr/Matrix.idr
+++ b/src/Data/NumIdr/Matrix.idr
@@ -71,26 +71,26 @@ permuteM p = permuteInAxis 0 p (repeatDiag 1 0)
 
 ||| Construct the matrix that scales a vector by the given value.
 export
-scaling : {n : _} -> Num a => a -> Matrix' n a
-scaling x = repeatDiag x 0
+scale : {n : _} -> Num a => a -> Matrix' n a
+scale x = repeatDiag x 0
 
 ||| Calculate the rotation matrix of an angle.
 export
-rotation2D : Double -> Matrix' 2 Double
-rotation2D a = matrix [[cos a, - sin a], [sin a, cos a]]
+rotate2D : Double -> Matrix' 2 Double
+rotate2D a = matrix [[cos a, - sin a], [sin a, cos a]]
 
 
 export
-rotation3DX : Double -> Matrix' 3 Double
-rotation3DX a = matrix [[1,0,0], [0, cos a, - sin a], [0, sin a, cos a]]
+rotate3DX : Double -> Matrix' 3 Double
+rotate3DX a = matrix [[1,0,0], [0, cos a, - sin a], [0, sin a, cos a]]
 
 export
-rotation3DY : Double -> Matrix' 3 Double
-rotation3DY a = matrix [[cos a, 0, sin a], [0,1,0], [- sin a, 0, cos a]]
+rotate3DY : Double -> Matrix' 3 Double
+rotate3DY a = matrix [[cos a, 0, sin a], [0,1,0], [- sin a, 0, cos a]]
 
 export
-rotation3DZ : Double -> Matrix' 3 Double
-rotation3DZ a = matrix [[cos a, - sin a, 0], [sin a, cos a, 0], [0,0,1]]
+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 7aaab74..58f2ee6 100644
--- a/src/Data/NumIdr/Transform/Affine.idr
+++ b/src/Data/NumIdr/Transform/Affine.idr
@@ -16,8 +16,12 @@ public export
 Affine : Nat -> Type -> Type
 Affine = Transform TAffine
 
+export
+isAffine : FieldCmp a => HMatrix' n a -> Bool
+isAffine mat = isHMatrix mat && invertible (getMatrix mat)
+
 export
 fromHMatrix : FieldCmp a => HMatrix' n a -> Maybe (Affine n a)
-fromHMatrix mat = if invertible (getMatrix mat)
+fromHMatrix mat = if isAffine mat
                   then Just (unsafeMkTrans mat)
                   else Nothing
diff --git a/src/Data/NumIdr/Transform/Isometry.idr b/src/Data/NumIdr/Transform/Isometry.idr
index 726fb07..bc7369a 100644
--- a/src/Data/NumIdr/Transform/Isometry.idr
+++ b/src/Data/NumIdr/Transform/Isometry.idr
@@ -15,3 +15,6 @@ import Data.NumIdr.Transform.Transform
 public export
 Isometry : Nat -> Type -> Type
 Isometry = Transform TIsometry
+
+
+-- TODO: Add Isometry constructors
diff --git a/src/Data/NumIdr/Transform/Orthonormal.idr b/src/Data/NumIdr/Transform/Orthonormal.idr
index e63e21d..0286283 100644
--- a/src/Data/NumIdr/Transform/Orthonormal.idr
+++ b/src/Data/NumIdr/Transform/Orthonormal.idr
@@ -18,14 +18,14 @@ Orthonormal = Transform TOrthonormal
 
 
 export
-isOrthonormal : Eq a => Num a => Matrix' n a -> Bool
-isOrthonormal {n} mat with (viewShape mat)
+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)
 
 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
+fromMatrix mat = if isOrthonormal' mat then Just (unsafeMkTrans (matrixToH mat))
+                                       else Nothing
 
 
 export
@@ -48,4 +48,4 @@ reflectZ = reflect 2
 export
 reflectNormal : (Neg a, Fractional a) => Vector n a -> Orthonormal n a
 reflectNormal {n} v with (viewShape v)
-  _ | Shape [n] = unsafeMkTrans $ matrixToH $ (identity - (2 / normSq v) *. outer v v)
+  _ | Shape [n] = unsafeMkTrans $ matrixToH $ identity - (2 / normSq v) *. outer v v
diff --git a/src/Data/NumIdr/Transform/Point.idr b/src/Data/NumIdr/Transform/Point.idr
index 7979f5b..98cc76c 100644
--- a/src/Data/NumIdr/Transform/Point.idr
+++ b/src/Data/NumIdr/Transform/Point.idr
@@ -90,24 +90,26 @@ export
 -- Arithmetic operations
 --------------------------------------------------------------------------------
 
+infixr 8 +.
+infixl 8 .+
+infixl 8 -.
 
 -- Affine space operations
--- These seem to cause issues with interface resolution
+-- These would have been named simply (+) and (-), but that caused
+-- too many issues with interface resolution.
 
--- namespace Left
---   export
---   (+) : Num a => Vector n a -> Point n a -> Point n a
---   a + MkPoint b = MkPoint (zipWith (+) a b)
+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
+(.+) : 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
--- MkPoint a - MkPoint b = zipWith (-) a b
+export
+(-.) : Neg a => Point n a -> Point n a -> Vector n a
+MkPoint a -. MkPoint b = zipWith (-) a b
 
 
 --------------------------------------------------------------------------------
@@ -150,8 +152,8 @@ Traversable (Point n) where
 
 export
 Show a => Show (Point n a) where
-  showPrec d (MkPoint v) = showCon d "point " $
-    show $ PrimArray.toList $ getPrim v
+  showPrec d (MkPoint v) = showCon d "point" $
+    showArg $ PrimArray.toList $ getPrim v
 
 export
 Cast a b => Cast (Point n a) (Point n b) where
diff --git a/src/Data/NumIdr/Transform/Rigid.idr b/src/Data/NumIdr/Transform/Rigid.idr
index d89b2b1..a4f6732 100644
--- a/src/Data/NumIdr/Transform/Rigid.idr
+++ b/src/Data/NumIdr/Transform/Rigid.idr
@@ -15,3 +15,5 @@ import Data.NumIdr.Transform.Transform
 public export
 Rigid : Nat -> Type -> Type
 Rigid = Transform TRigid
+
+-- TODO: Add Rigid constructors
diff --git a/src/Data/NumIdr/Transform/Rotation.idr b/src/Data/NumIdr/Transform/Rotation.idr
index 1a1812b..a425c33 100644
--- a/src/Data/NumIdr/Transform/Rotation.idr
+++ b/src/Data/NumIdr/Transform/Rotation.idr
@@ -8,6 +8,7 @@ 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
 
@@ -17,6 +18,27 @@ Rotation : Nat -> Type -> Type
 Rotation = Transform TRotation
 
 
+-- HACK: Replace with more efficient method
 export
-isRotation' : Matrix' n a -> Bool
-isRotation' mat =
+isRotation' : FieldCmp a => Matrix' n a -> Bool
+isRotation' mat = isOrthonormal mat && det mat == 1
+
+fromMatrix : FieldCmp a => Matrix' n a -> Maybe (Rotation n a)
+fromMatrix mat = if isRotation' mat then Just (unsafeMkTrans $ matrixToH mat)
+                                    else Nothing
+
+export
+rotate2D : Num a => Double -> Rotation 2 Double
+rotate2D = unsafeMkTrans . rotate2DH
+
+export
+rotate3DX : Num a => Double -> Rotation 3 Double
+rotate3DX = unsafeMkTrans . rotate3DXH
+
+export
+rotate3DY : Num a => Double -> Rotation 3 Double
+rotate3DY = unsafeMkTrans . rotate3DYH
+
+export
+rotate3DZ : Num a => Double -> Rotation 3 Double
+rotate3DZ = unsafeMkTrans . rotate3DZH
diff --git a/src/Data/NumIdr/Transform/Transform.idr b/src/Data/NumIdr/Transform/Transform.idr
index 9e22769..439cd69 100644
--- a/src/Data/NumIdr/Transform/Transform.idr
+++ b/src/Data/NumIdr/Transform/Transform.idr
@@ -16,46 +16,22 @@ import Data.NumIdr.Transform.Point
 --------------------------------------------------------------------------------
 
 
-public export
-data TransType = TAffine | TIsometry | TRigid | TTranslation
-               | TLinear | TOrthonormal | TRotation | TTrivial
+export
+TransType : Type
+TransType = (Fin 4, Bool)
 
-%name TransType ty
-
-
-public export
-Show TransType where
-  show TAffine = "TAffine"
-  show TIsometry = "TIsometry"
-  show TRigid = "TRigid"
-  show TTranslation = "TTranslation"
-  show TLinear = "TLinear"
-  show TOrthonormal = "TOrthonormal"
-  show TRotation = "TRotation"
-  show TTrivial = "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
+namespace TransType
+  export
+  TAffine, TIsometry, TRigid, TTranslation,
+    TLinear, TOrthonormal, TRotation, TTrivial : TransType
+  TAffine = (3, True)
+  TIsometry = (2, True)
+  TRigid = (1, True)
+  TTranslation = (0, True)
+  TLinear = (3, False)
+  TOrthonormal = (2, False)
+  TRotation = (1, False)
+  TTrivial = (0, False)
 
 
 --------------------------------------------------------------------------------
@@ -65,17 +41,19 @@ fromSignature (0, False) = TTrivial
 
 public export
 (:<) : TransType -> TransType -> Bool
-x :< y with (toSignature x, toSignature y)
-  _ | ((xn, xb), (yn, yb)) = (xn <= yn) && (xb >= yb)
+(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)
+transMult (xn, xb) (yn, yb) = (max xn yn, xb && yb)
 
 public export
 linearizeType : TransType -> TransType
-linearizeType = fromSignature . mapSnd (const False) . toSignature
+linearizeType = mapSnd (const False)
+
+public export
+delinearizeType : TransType -> TransType
+delinearizeType = mapSnd (const True)
 
 
 export
@@ -98,6 +76,11 @@ 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 _))
 
+export
+setTranslation : Num a => Vector n a -> Transform ty n a
+                  -> Transform (delinearizeType ty) n a
+setTranslation v (MkTrans _ mat) = MkTrans _ (hmatrix (getMatrix mat) v)
+
 
 --------------------------------------------------------------------------------
 -- Interface implementations
diff --git a/src/Data/NumIdr/Transform/Translation.idr b/src/Data/NumIdr/Transform/Translation.idr
index 3175989..ed34b59 100644
--- a/src/Data/NumIdr/Transform/Translation.idr
+++ b/src/Data/NumIdr/Transform/Translation.idr
@@ -18,13 +18,13 @@ Translation = Transform TTranslation
 
 
 export
-isTranslation : (Eq a, Num a) => HMatrix' n a -> Bool
+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
 
 export
-fromVector : Num a => Vector n a -> Translation n a
-fromVector v = unsafeMkTrans (translationH v)
+translate : Num a => Vector n a -> Translation n a
+translate v = unsafeMkTrans (translationH v)
 
 export
 fromHMatrix : (Eq a, Num a) => HMatrix' n a -> Maybe (Translation n a)
diff --git a/src/Data/NumIdr/Transform/Trivial.idr b/src/Data/NumIdr/Transform/Trivial.idr
index 30ee812..7a8ecf3 100644
--- a/src/Data/NumIdr/Transform/Trivial.idr
+++ b/src/Data/NumIdr/Transform/Trivial.idr
@@ -18,6 +18,6 @@ Trivial = Transform TTrivial
 
 
 export
-isTrivial : (Eq a, Num a) => HMatrix' n a -> Bool
+isTrivial : Eq a => Num a => HMatrix' n a -> Bool
 isTrivial {n} mat with (viewShape mat)
   _ | Shape [S n,S n] = mat == identity
diff --git a/src/Data/Permutation.idr b/src/Data/Permutation.idr
index 731661f..78b6f83 100644
--- a/src/Data/Permutation.idr
+++ b/src/Data/Permutation.idr
@@ -43,7 +43,7 @@ swapElems i j v =
 
 export
 permuteVect : Permutation n -> Vect n a -> Vect n a
-permuteVect p = foldMap @{%search} @{mon} (\(i,j) => swapElems i j) p.swaps
+permuteVect p = foldMap @{%search} @{mon} (uncurry swapElems) p.swaps
 
 
 export
@@ -54,7 +54,7 @@ swapValues i j x = if x == cast i then cast j
 
 export
 permuteValues : Permutation n -> Nat -> Nat
-permuteValues p = foldMap @{%search} @{mon} (\(i,j) => swapValues i j) p.swaps
+permuteValues p = foldMap @{%search} @{mon} (uncurry swapValues) p.swaps