From 3e1250537790cc6e6a3a9669f060c39fb1ee3fe9 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Tue, 6 Sep 2022 13:37:50 -0400
Subject: [PATCH] Create Field and Scalar interfaces

---
 numidr.ipkg                                   |  2 +-
 src/Data/NumIdr/Array/Array.idr               |  2 +-
 src/Data/NumIdr/Homogeneous.idr               |  2 +-
 .../NumIdr/{Multiply.idr => Interfaces.idr}   | 26 ++++++++++++++++++-
 src/Data/NumIdr/Matrix.idr                    | 25 ++++++++++--------
 src/Data/NumIdr/Scalar.idr                    |  2 +-
 src/Data/NumIdr/Vector.idr                    | 13 ++++++++--
 src/Data/Permutation.idr                      |  3 ++-
 8 files changed, 56 insertions(+), 19 deletions(-)
 rename src/Data/NumIdr/{Multiply.idr => Interfaces.idr} (73%)

diff --git a/numidr.ipkg b/numidr.ipkg
index 8202ba4..c093b40 100644
--- a/numidr.ipkg
+++ b/numidr.ipkg
@@ -17,7 +17,7 @@ modules = Data.NP,
           Data.NumIdr.Array.Order,
           Data.NumIdr.Homogeneous,
           Data.NumIdr.Matrix,
-          Data.NumIdr.Multiply,
+          Data.NumIdr.Interfaces,
           Data.NumIdr.PrimArray,
           Data.NumIdr.Scalar,
           Data.NumIdr.Vector
diff --git a/src/Data/NumIdr/Array/Array.idr b/src/Data/NumIdr/Array/Array.idr
index 696ad3c..14323e8 100644
--- a/src/Data/NumIdr/Array/Array.idr
+++ b/src/Data/NumIdr/Array/Array.idr
@@ -6,7 +6,7 @@ import Data.Vect
 import Data.Zippable
 import Data.NP
 import Data.Permutation
-import Data.NumIdr.Multiply
+import Data.NumIdr.Interfaces
 import Data.NumIdr.PrimArray
 import Data.NumIdr.Array.Order
 import Data.NumIdr.Array.Coords
diff --git a/src/Data/NumIdr/Homogeneous.idr b/src/Data/NumIdr/Homogeneous.idr
index ebde046..2473af5 100644
--- a/src/Data/NumIdr/Homogeneous.idr
+++ b/src/Data/NumIdr/Homogeneous.idr
@@ -1,7 +1,7 @@
 module Data.NumIdr.Homogeneous
 
 import Data.Vect
-import Data.NumIdr.Multiply
+import Data.NumIdr.Interfaces
 import Data.NumIdr.Vector
 import Data.NumIdr.Matrix
 
diff --git a/src/Data/NumIdr/Multiply.idr b/src/Data/NumIdr/Interfaces.idr
similarity index 73%
rename from src/Data/NumIdr/Multiply.idr
rename to src/Data/NumIdr/Interfaces.idr
index 6c0f062..0d9f4a1 100644
--- a/src/Data/NumIdr/Multiply.idr
+++ b/src/Data/NumIdr/Interfaces.idr
@@ -1,8 +1,32 @@
-module Data.NumIdr.Multiply
+module Data.NumIdr.Interfaces
 
 %default total
 
 
+--------------------------------------------------------------------------------
+-- Field
+--------------------------------------------------------------------------------
+
+
+public export
+Field : Type -> Type
+Field a = (Eq a, Neg a, Fractional a)
+
+
+public export
+interface (Eq a, Neg a, Fractional a) => Scalar a where
+  abscmp : a -> a -> Ordering
+
+
+export
+(Ord a, Abs a, Neg a, Fractional a) => Scalar a where
+  abscmp x y = compare (abs x) (abs y)
+
+
+--------------------------------------------------------------------------------
+-- Multiplication
+--------------------------------------------------------------------------------
+
 infixr 9 *.
 infixr 10 ^
 
diff --git a/src/Data/NumIdr/Matrix.idr b/src/Data/NumIdr/Matrix.idr
index 65daa20..c019323 100644
--- a/src/Data/NumIdr/Matrix.idr
+++ b/src/Data/NumIdr/Matrix.idr
@@ -3,7 +3,7 @@ module Data.NumIdr.Matrix
 import Data.List
 import Data.Vect
 import Data.Permutation
-import Data.NumIdr.Multiply
+import Data.NumIdr.Interfaces
 import public Data.NumIdr.Array
 import Data.NumIdr.Vector
 
@@ -278,7 +278,7 @@ iterateN 1 f x = f FZ x
 iterateN (S n@(S _)) f x = iterateN n (f . FS) $ f FZ x
 
 
-gaussStep : {m,n : _} -> (Eq a, Neg a, Fractional a) =>
+gaussStep : {m,n : _} -> Field a =>
             Fin (minimum m n) -> Matrix m n a -> Matrix m n a
 gaussStep i lu =
     if all (==0) $ getColumn (minWeakenRight i) lu then lu else
@@ -294,7 +294,7 @@ gaussStep i lu =
             (flip (-) offsets) lu'
 
 export
-decompLU : (Eq a, Neg a, Fractional a) => (mat : Matrix m n a) -> Maybe (DecompLU mat)
+decompLU : Field a => (mat : Matrix m n a) -> Maybe (DecompLU mat)
 decompLU mat with (viewShape mat)
   _ | Shape [m,n] = map MkLU $ iterateN (minimum m n) (\i => (>>= gaussStepMaybe i)) (Just mat)
   where
@@ -353,8 +353,7 @@ fromLU (MkLU lu) = MkLUP lu identity 0
 
 
 export
-decompLUP : (Ord a, Abs a, Neg a, Fractional a) =>
-            (mat : Matrix m n a) -> DecompLUP mat
+decompLUP : Scalar a => (mat : Matrix m n a) -> DecompLUP mat
 decompLUP {m,n} mat with (viewShape mat)
   decompLUP {m=0,n} mat | Shape [0,n] = MkLUP mat identity 0
   decompLUP {m=S m,n=0} mat | Shape [S m,0] = MkLUP mat identity 0
@@ -365,8 +364,8 @@ decompLUP {m,n} mat with (viewShape mat)
     maxIndex x [] = x
     maxIndex _ [x] = x
     maxIndex x ((a,b)::(c,d)::xs) =
-      if abs b < abs d then assert_total $ maxIndex x ((c,d)::xs)
-                       else assert_total $ maxIndex x ((a,b)::xs)
+      if abscmp b d == LT then assert_total $ maxIndex x ((c,d)::xs)
+                          else assert_total $ maxIndex x ((a,b)::xs)
 
     gaussStepSwap : Fin (minimum (S m) (S n)) -> DecompLUP mat -> DecompLUP mat
     gaussStepSwap i (MkLUP lu p sw) =
@@ -385,16 +384,20 @@ decompLUP {m,n} mat with (viewShape mat)
 
 
 export
-detWithLUP : (Ord a, Abs a, Neg a, Fractional a) =>
-            (mat : Matrix' n a) -> DecompLUP mat -> a
-detWithLUP {n} mat lup =
+detWithLUP : Scalar a => (mat : Matrix' n a) -> DecompLUP mat -> a
+detWithLUP  mat lup =
   (if numSwaps lup `mod` 2 == 0 then 1 else -1)
     * product (diagonal lup.lu)
 
 export
-det : (Ord a, Abs a, Neg a, Fractional a) => Matrix' n a -> a
+det : Scalar a => Matrix' n a -> a
 det {n} mat with (viewShape mat)
   det {n=0} mat | Shape [0,0] = 1
   det {n=1} mat | Shape [1,1] = mat!![0,0]
   det {n=2} mat | Shape [2,2] = let [a,b,c,d] = elements mat in a*d - b*c
   _ | Shape [n,n] = detWithLUP mat (decompLUP mat)
+
+
+solveWithLUP : Scalar a => (mat : Matrix m n a) -> DecompLUP mat ->
+                Vector m a -> Maybe (Vector n a)
+solveWithLUP mat lup b = ?h
diff --git a/src/Data/NumIdr/Scalar.idr b/src/Data/NumIdr/Scalar.idr
index d4f9d42..b2bdbd0 100644
--- a/src/Data/NumIdr/Scalar.idr
+++ b/src/Data/NumIdr/Scalar.idr
@@ -1,7 +1,7 @@
 module Data.NumIdr.Scalar
 
 import Data.Vect
-import Data.NumIdr.Multiply
+import Data.NumIdr.Interfaces
 import Data.NumIdr.PrimArray
 import public Data.NumIdr.Array
 
diff --git a/src/Data/NumIdr/Vector.idr b/src/Data/NumIdr/Vector.idr
index 5cb2640..620d5d6 100644
--- a/src/Data/NumIdr/Vector.idr
+++ b/src/Data/NumIdr/Vector.idr
@@ -1,7 +1,8 @@
 module Data.NumIdr.Vector
 
 import Data.Vect
-import Data.NumIdr.Multiply
+import Data.Permutation
+import Data.NumIdr.Interfaces
 import public Data.NumIdr.Array
 
 %default total
@@ -117,7 +118,7 @@ export
 
 
 --------------------------------------------------------------------------------
--- Swizzling
+-- Swizzling & permuting elements
 --------------------------------------------------------------------------------
 
 
@@ -130,6 +131,14 @@ swizzle p v = rewrite sym (lengthCorrect p)
               )
 
 
+export
+swapCoords : (i,j : Fin n) -> Vector n a -> Vector n a
+swapCoords = swapInAxis 0
+
+export
+permuteCoords : Permutation n -> Vector n a -> Vector n a
+permuteCoords = permuteInAxis 0
+
 
 --------------------------------------------------------------------------------
 -- Vector operations
diff --git a/src/Data/Permutation.idr b/src/Data/Permutation.idr
index 4f3a48b..731661f 100644
--- a/src/Data/Permutation.idr
+++ b/src/Data/Permutation.idr
@@ -2,8 +2,9 @@ module Data.Permutation
 
 import Data.List
 import Data.Vect
-import Data.NumIdr.Multiply
+import Data.NumIdr.Interfaces
 
+%default total
 
 export
 record Permutation n where